VCD dump for PASS

[marvintau]

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]

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/