Heya everyone,
I’m working with povik and some other contributors (namely mndstrmr) to yosys-slang to add better support for SVA assertions over there (Rebase SVA support into main by mlyoung101 · Pull Request #317 · povik/yosys-slang · GitHub).
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.
Basically, I want to ask: How do you folks (YosysHQ devs) verify your Verific SVA emitter? This one: yosys/frontends/verific/verificsva.cc at main · YosysHQ/yosys · GitHub
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.
Any thoughts are welcome!