tests: Run async2sync before sat and/or sim to handle $check cells

Right now neither `sat` nor `sim` have support for the `$check` cell.
For formal verification it is a good idea to always run either
async2sync or clk2fflogic which will (in a future commit) lower `$check`
to `$assert`, etc.

While `sim` should eventually support `$check` directly, using
`async2sync` is ok for the current tests that use `sim`, so this commit
also runs `async2sync` before running sim on designs containing
assertions.

tests/arch/quicklogic/qlf_k6n10f/dsp.ys

@@ -107,7 +107,7 @@ reg [7:0] i = 0;
 always @(posedge clk) begin
 	if (i < VECTORLEN) begin
 		// FIXME: for some reason the first assert fails (despite comparing zero to zero)
-		if (i > 0) 
+		if (i > 0)
 			assert(y == y_expected);
 		i <= i + 1;
 	end
@@ -117,4 +117,5 @@ EOF
 read_verilog +/quicklogic/qlf_k6n10f/dsp_sim.v
 hierarchy -top testbench
 proc
+async2sync
 sim -assert -q -clock clk -n 20

tests/arch/quicklogic/qlf_k6n10f/mem_gen.py

@@ -36,7 +36,7 @@ blockram_tests: "list[tuple[list[tuple[str, int]], str, list[str]]]" = [
     ([("ADDRESS_WIDTH", 14), ("DATA_WIDTH",  2)], "sync_ram_*dp", ["-assert-count 1 t:TDP36K", "-assert-count 1 t:TDP36K a:port_a_width=2 %i"]),
     ([("ADDRESS_WIDTH", 15), ("DATA_WIDTH",  1)], "sync_ram_*dp", ["-assert-count 1 t:TDP36K", "-assert-count 1 t:TDP36K a:port_a_width=1 %i"]),
 
-    # 2x asymmetric (1024x36bit write / 2048x18bit read or vice versa = 1TDP36K) 
+    # 2x asymmetric (1024x36bit write / 2048x18bit read or vice versa = 1TDP36K)
     ([("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 18), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
     ([("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 16), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
     ([("ADDRESS_WIDTH", 12), ("DATA_WIDTH",  9), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
@@ -131,6 +131,7 @@ read_verilog -defer -formal mem_tb.v
 chparam{param_str} -set VECTORLEN {vectorlen} TB
 hierarchy -top TB -check
 prep
+async2sync
 log ** CHECKING SIMULATION FOR TEST {top} WITH PARAMS{param_str}
 sim -clock clk -n {vectorlen} -assert
 """
@@ -254,16 +255,16 @@ sim_tests: list[TestClass] = [
             {"rq_a": 0x5678},
         ]
     ),
-    TestClass( # basic TDP test 
+    TestClass( # basic TDP test
         # note that the testbench uses ra and wa, while the common TDP model
         # uses a shared address
         params={"ADDRESS_WIDTH": 10, "DATA_WIDTH": 36},
         top="sync_ram_tdp",
         assertions=[],
         test_steps=[
-            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA, 
+            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xdeadbeef,            "wd_b": 0x5a5a5a5a},
-            {"wce_a": 1, "ra_a": 0xFF, 
+            {"wce_a": 1, "ra_a": 0xFF,
              "wd_a": 0},
             {"rce_a": 1, "ra_a": 0x0A,      "rce_b": 1, "ra_b": 0x0A},
             {"rq_a": 0xdeadbeef,            "rq_b": 0xdeadbeef},
@@ -276,9 +277,9 @@ sim_tests: list[TestClass] = [
         top="sync_ram_tdp",
         assertions=[],
         test_steps=[
-            {"wce_a": 1, "ra_a": 0x0F,      "wce_b": 1, "ra_b": 0xBA, 
+            {"wce_a": 1, "ra_a": 0x0F,      "wce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xdeadbeef,            "wd_b": 0x5a5a5a5a},
-            {"wce_a": 1, "ra_a": 0xFF, 
+            {"wce_a": 1, "ra_a": 0xFF,
              "wd_a": 0},
             {"rce_a": 1, "ra_a": 0x0F,      "rce_b": 1, "ra_b": 0x0A},
             {"rq_a": 0,                     "rq_b": 0x00005a5a},
@@ -291,7 +292,7 @@ sim_tests: list[TestClass] = [
         top="sync_ram_tdp",
         assertions=[],
         test_steps=[
-            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA, 
+            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xdeadbeef,            "wd_b": 0x5a5a5a5a},
             {"wce_a": 1, "ra_a": 0xBA,      "rce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xa5a5a5a5},
@@ -409,7 +410,7 @@ for sim_test in sim_tests:
             fn = f"t_mem{i}.ys"
             f = open(fn, mode="w")
             j = 0
-        
+
         # output yosys script test file
         print(
             blockram_template.format(param_str=param_str, top=top),

tests/arch/quicklogic/qlf_k6n10f/meminit.ys

@@ -10,5 +10,6 @@ select -assert-count 1 t:TDP36K a:is_split=0 %i
 select -assert-count 1 t:TDP36K a:was_split_candidate=0 %i
 read_verilog +/quicklogic/common/cells_sim.v +/quicklogic/qlf_k6n10f/cells_sim.v +/quicklogic/qlf_k6n10f/brams_sim.v +/quicklogic/qlf_k6n10f/sram1024x18_mem.v +/quicklogic/qlf_k6n10f/ufifo_ctl.v +/quicklogic/qlf_k6n10f/TDP18K_FIFO.v
 prep
+async2sync
 hierarchy -top top
 sim -assert -q -n 12 -clock clk

tests/arch/xilinx/dsp_abc9.ys

@@ -30,6 +30,7 @@ module top(output [42:0] P);
 assert property (P == 42*42);
 endmodule
 EOT
+async2sync
 techmap -map +/xilinx/xc7_dsp_map.v
 verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
 synth_xilinx -abc9

tests/gen-tests-makefile.sh

@@ -75,7 +75,7 @@ generate_tests() {
 	if [[ $do_sv = true ]]; then
 		for x in *.sv; do
 			if [ ! -f "${x%.sv}.ys"  ]; then
-				generate_ys_test "$x" "-p \"prep -top top; sat -enable_undef -verify -prove-asserts\" $yosys_args"
+				generate_ys_test "$x" "-p \"prep -top top; async2sync; sat -enable_undef -verify -prove-asserts\" $yosys_args"
 			fi;
 		done
 	fi;

tests/sat/asserts.ys

@@ -1,3 +1,3 @@
 read_verilog -sv asserts.v
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts

tests/sat/asserts_seq.ys

@@ -1,5 +1,5 @@
 read_verilog -sv asserts_seq.v
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 
 sat -verify  -prove-asserts -tempinduct -seq 1 test_001
 sat -falsify -prove-asserts -tempinduct -seq 1 test_002

tests/sat/initval.ys

@@ -1,5 +1,5 @@
 read_verilog -sv initval.v
-proc;;
+proc; async2sync;;
 
 sat -seq 10 -prove-asserts
 

tests/sat/sizebits.ys

@@ -1,2 +1,2 @@
 read_verilog -sv sizebits.sv
-prep; sat -verify -prove-asserts
+prep; async2sync; sat -verify -prove-asserts

tests/svtypes/enum_simple.ys

@@ -1,5 +1,5 @@
 
 read_verilog -sv enum_simple.sv
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts -show-all
 

tests/svtypes/struct_dynamic_range.ys

@@ -4,4 +4,5 @@ select -assert-count 2 t:$shift
 select -assert-count 2 t:$shiftx
 prep -top top
 flatten
+async2sync
 sat -enable_undef -verify -prove-asserts

tests/svtypes/typedef_initial_and_assign.ys

@@ -9,6 +9,6 @@ logger -expect warning "reg '\\var_18' is assigned in a continuous assignment" 1
 logger -expect warning "reg '\\var_19' is assigned in a continuous assignment" 1
 
 read_verilog -sv typedef_initial_and_assign.sv
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 select -module top
-sat -verify -seq 1 -tempinduct -prove-asserts -show-all
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/svtypes/typedef_struct_port.ys

@@ -1,5 +1,5 @@
 read_verilog -sv typedef_struct_port.sv
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all
 select -module test_parser

tests/various/chformal_coverenable.ys

@@ -13,6 +13,8 @@ EOT
 
 prep -top top
 
+async2sync
+
 select -assert-count 1 t:$cover
 
 chformal -cover -coverenable

tests/various/chparam.sh

@@ -37,14 +37,17 @@ EOT
 
 if ../../yosys -q -p 'verific -sv chparam1.sv'; then
 	../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+			-p 'async2sync' \
 			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
 			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
 
 	../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+			-p 'async2sync' \
 			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
 			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
 fi
 ../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+		-p 'async2sync' \
 		-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
 		-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
 

tests/various/const_arg_loop.ys

@@ -3,4 +3,5 @@ hierarchy
 proc
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/const_func.ys

@@ -4,4 +4,5 @@ proc
 flatten
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/countbits.ys

@@ -4,4 +4,5 @@ proc
 flatten
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/param_struct.ys

@@ -47,4 +47,5 @@ end
 endmodule
 EOF
 hierarchy; proc; opt
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/struct_access.ys

@@ -2,4 +2,5 @@ read_verilog -sv struct_access.sv
 hierarchy
 proc
 opt
+async2sync
 sat -verify -seq 1 -prove-asserts -show-all

tests/verilog/asgn_expr.ys

@@ -1,3 +1,4 @@
 read_verilog -sv asgn_expr.sv
 proc
+async2sync
 sat -verify -prove-asserts -show-all

tests/verilog/atom_type_signedness.ys

@@ -14,6 +14,6 @@ always_comb begin
 end
 endmodule
 EOT
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 select -module dut
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/bug2042-sv.ys

@@ -17,6 +17,7 @@ output reg b
 endmodule
 EOT
 proc
+async2sync
 sat -verify -prove-asserts
 
 
@@ -42,6 +43,7 @@ output b, c
 endmodule
 EOT
 proc
+async2sync
 sat -verify -prove-asserts
 
 

tests/verilog/func_tern_hint.ys

@@ -1,4 +1,5 @@
 read_verilog -sv func_tern_hint.sv
 proc
 opt
+async2sync
 sat -verify -seq 1 -prove-asserts -show-all

tests/verilog/func_upto.ys

@@ -3,5 +3,6 @@ hierarchy -top top
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -prove-asserts -enable_undef

tests/verilog/int_types.ys

@@ -3,5 +3,6 @@ hierarchy
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/mem_bounds.ys

@@ -3,4 +3,5 @@ proc
 flatten
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all -enable_undef

tests/verilog/net_types.ys

@@ -2,4 +2,5 @@ read_verilog -sv net_types.sv
 hierarchy
 proc
 opt -full
+async2sync
 sat -verify -prove-asserts -show-all

tests/verilog/package_task_func.ys

@@ -1,4 +1,5 @@
 read_verilog -sv package_task_func.sv
 proc
 opt -full
+async2sync
 sat -verify -seq 1 -prove-asserts -show-all

tests/verilog/param_no_default.ys

@@ -3,5 +3,6 @@ hierarchy
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/parameters_across_files.ys

@@ -16,5 +16,6 @@ hierarchy
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/past_signedness.ys

@@ -14,6 +14,7 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk
 
 design -reset
@@ -32,4 +33,5 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk

tests/verilog/prefix.ys

@@ -2,4 +2,5 @@ read_verilog -sv prefix.sv
 hierarchy
 proc
 select -module top
+async2sync
 sat -verify -seq 1 -prove-asserts -show-all

tests/verilog/sign_array_query.ys

@@ -14,6 +14,7 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk
 
 design -reset
@@ -32,6 +33,7 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk
 
 design -reset
@@ -49,4 +51,5 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk

tests/verilog/size_cast.ys

@@ -2,4 +2,5 @@ read_verilog -sv size_cast.sv
 proc
 opt -full
 select -module top
+async2sync
 sat -verify -prove-asserts -show-all

tests/verilog/struct_access.ys

@@ -1,4 +1,5 @@
 read_verilog -formal -sv struct_access.sv
 proc
 opt -full
+async2sync
 sat -verify -seq 1 -prove-asserts -show-all

tests/verilog/typedef_across_files.ys

@@ -19,5 +19,6 @@ EOF
 
 proc
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/typedef_legacy_conflict.ys

@@ -33,5 +33,6 @@ hierarchy
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/unbased_unsized.ys

@@ -3,5 +3,6 @@ hierarchy
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/unbased_unsized_shift.ys

@@ -3,5 +3,6 @@ hierarchy
 proc
 flatten
 opt -full
+async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/verilog/unreachable_case_sign.ys

@@ -12,6 +12,7 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk
 
 design -reset
@@ -29,5 +30,6 @@ endmodule
 EOT
 
 prep -top top
+async2sync
 sim -n 3 -clock clk