I’ve come to realise that it’s actually quite important to verify that you’re constructing the RTLIL for the SVA assertions correctly. Users assume that the proofs they get are “perfect”, and I’ll go ahead and assume that although the SMT solvers don’t have bugs in them, we could easily accidentally create bugs when we’re parsing SVA and invalidate the proofs.
Povik suggested sequential equivalence checking against manually constructed circuitry that contains equivalent circuitry for the property, which seems like a good idea but also very time consuming. I had figured we could do the same but for Verific emitted RTLIL and our RTLIL, but I’m not sure that’s within the terms of my Tabby CAD licence.
We have some ideas for how we want to test the correctness of the new Property IR verification flow. (Although that is not exactly “verifying” in the sense of a definite proof that it is correct.)
We plan to generate property & word (= trace) pairs (finite words, or with an infinite suffix consisting of top/bottom symbols, or maybe even with a periodic suffix) that we can compute the results for, since we can evaluate them on the syntactic level of the property by following the definition of the formal semantics for SVA. (These pairs could be generated together in a way that we get the pass/fail result that we want, to avoid that we only generate pairs where the word does not satisfy the property.) Then we can evaluate that same word on different stages of the construction of the checker circuit (for example also for an intermediate automata representation) to ensure that the transformations do not change the result.
(As far as I can see, the tests for the current implementation (verificsva.cc) check for handwritten properties whether SBY gives the correct result - not sure if anything else is done.)
Equivalence checking against the RTLIL coming from the verific frontend sounds like a good idea. It shouldn’t pose any license issues unless you’re making a profit off the work, and it’s definitely more practical than manually creating them. Also do let us know if you identify any discrepancies or bugs in the verific frontend checker circuits!
From the technical side, just off the top of my head, it would probably still require a little bit of manual netlist manipulation: for each $assert/$assume/$cover/$live you’d have to and together the A and EN ports to get the “property active” condition (since these ports are used differently between frontends) - I don’t know if there’s any way to create $and cells with the current script commands… but after that you could use expose to add them as module ports and miter -equiv -assert to compare all the exposed conditions. (Maybe also run delete -output before expose to avoid the solver effort of comparing the normal module outputs, if your test circuits have any.)
BTW what are your plans regarding the property IR? We have had the vague plan of first completing that project before tackling SVA in yosys-slang. Since porting over the verific flow to that IR will already involve creating a frontend-independent yosys pass constructing checker circuits from $property cells, we expect it’ll be much less work to add property support to other frontends after that, because only the frontend → IR import portion is needed, and the IR concepts are much closer to SVA. In fact the motivation in that project is to be able to use CIRCT as a second frontend to import properties from, and be able to reuse the same checker generation pass in both the verific and CIRCT flows. You can of course get a head start on yosys-slang now, but I worry that some of the work might turn out redundant in the end…
@nak I’m glad to hear that licencing wouldn’t be an issue my idea of a Verific-based cross-check, I’ll forward this onto povik and we might be able to use this.
Regarding the manual netlist manipulation, hm, that’s good to know; it sounds complicated to attack via scripting so what we may end up doing is just writing a simple custom command for testing purposes. I ended up doing that in my undergrad thesis for similar reasons and it seems to work well enough. But in any case, running a miter -equiv check seems to be a good idea, thanks.
Regarding property IR, I think this is a really good idea and the ideal target for yosys-slang. At the time of working with povik, I wanted to get ahead on pushing SVA support to yosys-slang because I needed it for my dissertation. However, I’ve since been able to get a TabbyCAD licence so it’s not as big of a priority for me personally.
Purely from a technical POV, the property IR sounds really nice and would massively reduce the work on our side, so I’d really like to wait for it to be released and target that. However, I also know that we have a lot of downstream users who want SVA support: the github issue is very active. Some work was done last year by a user to add basic SVA support, so my role was purely going to be to migrate that work over to main and get it merged in, so it wouldn’t be a particularly large amount of work on my side.
Anyways, I think for certain we target the property IR once it gets merged in even experimentally.