Identifying clock signals

[stevehoover]

Thanks, @nakengelhardt for the answer to #3477. I'm still struggling with the basics today, though, for that same example. I'm not sure how to communicate to Yosys which signal is the clock. Without a ridiculous string of -set-at args on the clock, I'm getting counterexamples with the clock flatlined. I do see how to use $initstate (using riscv-formal as an example) for reset. Clocks seem to be determined automatically for other examples, but not in my case, and embarrassingly, I haven't figured out the magic after hours of noodling/reading/Googling today.

[nakengelhardt]

sat doesn't detect any clock signals, it just converts any FF-type cells into state for the sat solver regardless of what's on the clock port. So the clock would be flat, but unless you use the clock signal as something other than the clock input to an FF cell (which isn't recommended design practice anyway) this is only cosmetic. (SBY will in fact "fake" the clock signal after the fact when generating the VCD from the solver witness.)
Somewhat relatedly, it's recommended to run either async2sync (for a single clock) or clk2fflogic (for multiclock designs) before sat to set things up to be converted to smt in a way that makes sense. In the multiclock case, the clock signals are also not forced, the solver is left the choice to toggle them in any order that might be useful for the proof.

You can also take a look at equiv_opt which we use in the development of yosys to validate our optimization passes. It only does the induction step and not the basecase but it's a bit less fiddly. Both of these are very low-level tools though, and the integrated solver isn't very powerful so it'll only work on small circuit fragments. Another option would be to set up a miter circuit and then use SBY to check it (which will automatically do all the setup things like call async2sync, or clk2fflogic if you set the multiclock option, and give you access to more powerful solvers).

We don't have an equivalence checking tool yet that is user-facing in the sense of really usable for checking entire designs, but we're working on it - we hope to have it ready for release by Q2 2023.

[stevehoover]

Ah. I see. Thanks for a very complete answer. With this understanding, things are behaving as expected for me today. I'm much happier.

So, I guess functional clock gating would be problematic, then. Luckily, I'm using this with TL-Verilog tools, and I can disable functional clock gating for formal runs, so this becomes yet another benefit of using TL-Verilog :).

I'm inspired to add Yosys into Makerchip.com. This will be quite powerful.

[nakengelhardt]

If you have relevant logic on the clock signal like for clock gating, I believe this should be handled if you run clk2fflogic on the design first (or use the multiclock option in sby). Try it?