How to use `pono` correctly with `clk2fflogic`?

[Isweet]

I'm attempting to verify a synchronous hardware design, written in Verilog, and expressed in BTOR2 using Yosys. I've followed the guidance in the 'Generating BTOR2 from Verilog' section of the README.

The issue that I'm having is that my design is producing $aldff cells in Yosys. I used the clk2fflogic pass to eliminate these cells and produced syntactically valid BTOR2. However, I'm not getting the results I expect from executing the BTOR using pono.

I'm wondering if someone could clarify the meaning of the "IMPORTANT NOTE" in the README above the clk2fflogic pass:

# (optional) use an "explicit" clock
# e.g. every state is a half cycle of the
# fastest clock
# use this option if you see errors that
# refer to "adff" or asynchronous components
# IMPORTANT NOTE: the clocks are not
# automatically toggled if you use this option
# clk2fflogic;

Does this mean that even if I point pono at the appropriate symbol using the -c flag, the bounded model checking will not correctly toggle the input on each iteration?

Thanks in advance for the help, I really appreciate it!

[makaimann]

Hey Ian,

Sorry for the delayed response. Great question! Your original understanding is correct: after clk2fflogic, the clock is not automatically toggled for you (as it is in the case you don't use that pass), but targeting it with -c should toggle it for you. Here are a few things to try:

1. Ensure you're targeting the correct clock. Sometimes several symbols have similar names after running transformation passes
2. Try creating a wrapper module (in Verilog) that toggles the clock for you and then also run the resulting btor2 through another model checker, like btormc. This is just to make sure the issue is with the Verilog>btor2 conversion and not with Pono. This one I'm not positive about, because you might always end up with a "parent" clock that needs to be toggled in the BTOR. Alternatively, you could try manually updating the btor2 to toggle the clock. Or check if btormc has clock toggling logic now.
3. Look through the Yosys log file for anything odd. In particular, Yosys can sometimes blackbox entire modules if there's an issue without crashing. It will let you know in the log though.

Hope that helps and good luck!

[Isweet]

@makaimann Maybe you could help clarify some things, to ensure I'm doing everything as expected.

1. The clock signal should be represented as a BTOR2 input, e.g., as follows. Is that right?

...
i bitvec 1
...
j input i clk
...

2. Each transition in the state transition system specified by the BTOR2 should correspond to a half-cycle. Is that right? If so, is the first half cycle a negative or positive edge of the clock?

3. The units of the -s flag are state transitions. Is that right? For example, if each state transition corresponds to a half-cycle, then -s 2 should be interpreted as holding the design in reset for one clock cycle. Right?

4. How should I expect concurrent SVA to be encoded in BTOR2? E.g., assert property (@(posedge clk) p);

Since a safety property is encoded in BTOR2 as a predicate over the state variables, should I expect the predicate to be guarded by the clock? E.g., maybe it looks something like:

i bitvec 1
...
j input i clk
...
k state i p
...
l not i k
...
m and i j l ; ~(clk => p)
...
n bad m

Thanks for your help, and sorry for all the questions. There's a relative lack of documentation on the write_btor pass in Yosys.

[makaimann]

Hey Ian, no problem! Yes your understanding is correct to the best of my knowledge.

1. The clock should be that input, yes. I would make sure there are not multiple symbols labeled clk though and that it is actually used in the BTOR2. I saw one case where it didn't seem to be wired properly, but that may have been a fluke.
2. That's correct -- each transition should be a half cycle of the fastest clock (so if you only have on clock, then it is trivially always a half cycle of that clock). The clock should start at zero -- that's done here
3. Yes, those are state transitions so -s 2 after clk2fflogic would mean one cycle.
4. This I'm less confident in, but it being guarded by a clock as you suggested makes sense to me. Any SVA should get compiled into some form of state machine with a single bit output for whether the property passes or fails. In this case, it should be one on the negative edge of the clock, and only be checked on the positive edge.