search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
390 stars 74 forks source link

VCD dump for PASS #233

Open marvintau opened 1 year ago

marvintau commented 1 year ago

I know that sby can dump a VCD for a counter example for either BMC or k-Induction. I'm wondering if I can dump a VCD file as a good (or false positive) case when pass the verification. How should I do that if it's possible?

Thank you!

nakengelhardt commented 1 year ago

You can use cover to ask for a trace fulfilling some criteria while still respecting the assumptions. But you need to at least give the solver some end goal - or run simulation instead. This app note on witness covers has a lot of details on how to use cover to see if your checks are working as expected: https://yosyshq.readthedocs.io/projects/ap120/en/latest/