Verification of designs involving multiple clocks

Users
1

Hello! I’ve been using yosys to convert designs into AIGs for model checking with rIC3 for the past few weeks. Recently, I ecountered some weird counterexamples reported by the model checker. For these counterexamples, the simlation of the Verilog modules seems to suggest the property is not violated. I understand there are many potential causes for inaccurate simulation traces in such cases, but I’m wondering if there’s any known issue with the conversion in the presence of multiple clocks. I read there’s also this command clk2fflogic which seems helpful in this scenario, but is it strictly necessary for faithful conversion?

For a bit more context, my design comes with a top-level clock input which is used to derive two other clock signals for two submodules.

Thanks!

2

We have added rIC3 support to sby, which is a complete model checking work flow. For the formal verification clock situation in sby, see this clock signals FAQ. The sby multiclock option selects between the async2sync and clk2fflogic yosys passes. I don’t have a practical formal verification background but I would assume that separate clock domains would get formally verified separately if possible, for managable solver runtime and counterexample traces

3

Thanks a lot for the insight on async2sync and clk2fflogic! I had a more custom flow without using Symbiyosys, but I tried it out this morning with multiclock option, and it seemed to produce more reasonable result.