No bad property in btor2 file generated from verilog (`write_btor` should error for `$check` cells)

[gipsyh]

Version

Yosys 0.41 (git sha1 c1ad37779, g++ 13.2.0-23ubuntu4 -fPIC -Os)

On which OS did this happen?

Linux

Reproduction Steps

./yosys -p "read_verilog -formal example.v; write_btor example.btor2"

example.v:

module main (clk);
input clk;
reg [250:0] a,b;    

initial a = 1;
initial b = 0;

always @ (posedge clock) begin
    if (a<100) 
       a<=b+a;

    b <=a;
end

// assert property (a < 200);
wire prop = (a < 200);
wire prop_neg = !prop;
assert property ( prop );

endmodule

Expected Behavior

bad property in example.btor2

yosys-0.35 has the bad property but 0.41 not

example.btor2 generated from 0.35 with the same command:

; BTOR description generated by Yosys 0.35 (git sha1 cc31c6ebc, clang 18.1.3 -fPIC -Os) for module main.
1 sort bitvec 1
2 input 1 clk ; example.v:2.7-2.10
3 sort bitvec 251
4 input 3
5 sort bitvec 32
6 const 5 00000000000000000000000011001000
7 uext 3 6 219
8 ult 1 4 7
9 const 1 1
10 not 1 8
11 and 1 9 10
12 bad 11 example.v:18.23-19.25
13 input 1
14 uext 1 13 0 clock ; example.v:9.19-9.24
15 not 1 8
16 uext 1 15 0 prop_neg ; example.v:18.6-18.14
17 uext 1 8 0 prop ; example.v:17.6-17.10
18 input 3
19 uext 3 18 0 b ; example.v:3.15-3.16
20 uext 3 4 0 a ; example.v:3.13-3.14
; end of yosys output

Actual Behavior

not bad property in example.btor2 generated from 0.41

; BTOR description generated by Yosys 0.41 (git sha1 c1ad37779, g++ 13.2.0-23ubuntu4 -fPIC -Os) for module main.
1 sort bitvec 1
2 input 1 clk ; example.v:2.7-2.10
3 input 1
4 uext 1 3 0 clock ; example.v:9.19-9.24
5 sort bitvec 251
6 input 5
7 sort bitvec 32
8 const 7 00000000000000000000000011001000
9 uext 5 8 219
10 ult 1 6 9
11 not 1 10
12 uext 1 11 0 prop_neg ; example.v:18.6-18.14
13 uext 1 10 0 prop ; example.v:17.6-17.10
14 input 5
15 uext 5 14 0 b ; example.v:3.15-3.16
16 uext 5 6 0 a ; example.v:3.13-3.14
; end of yosys output

[gipsyh]

I also tried some options in write_btor, but the result are same.

[jix]

In general, you need to run additional passes to prepare the design for the btor backend.

The recommended way to make sure you're always using the up to date flow for this (which can change from time to time) is to use SBY. You can use the engine none and use the make_model btor option. A working SBY config for this example (after fixing the clk vs clock typo in the verilog code) would be:

[options]
mode bmc
make_model btor
expect unknown

[engines]
none

[script]
read_verilog -formal example.v
prep -top main

[files]
example.v

Running sby -f example.sby then results in a btor output in example/model/design_btor.btor. This is generated by running the yosys scripts example/model/design.ys, example/model/design_prep.ys and example/model/design_btor.ys in that order, and you can use these as reference for the passes of our current btor based FV flow. Note that some SBY options (like multiclock on) do affect the generated scripts.

The change in behavior you observed is because you are missing either async2sync (assume all FFs share the same clock that has an active edge for each single btor step, no matter what signal is actually connected to the clocks; also assume async resets are only asserted synchronized with that clock) or alternatively clk2fflogic (don't make any assumptions and detect when a signal changes between btor steps to implement FFs). Running either has been the recommendation for a long time, but recently became a requirement. If for some reason you don't want to run either pass but otherwise get the exact same behavior as before you can run chformal -lower instead.

If you do want to keep a rather minimal flow to produce btor, in addition to async2sync or clk2fflogic, you're also at least missing either a prep (recommended) or a hierarchy -top main; proc (a subset of prep, more likely to leave the design in a still FV incompatible state) which should always be the first step after read_verilog.

I'll still leave this issue open, since for this particular case, write_btor could detect that the design isn't sufficiently prepared and produce a helpful error instead of silently producing something unexpected.

[gipsyh]

Thank you, I'll have a try.