diff --git a/tests/arch/quicklogic/qlf_k6n10f/dsp.ys b/tests/arch/quicklogic/qlf_k6n10f/dsp.ys index 023ff0d89..1e652855b 100644 --- a/tests/arch/quicklogic/qlf_k6n10f/dsp.ys +++ b/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 diff --git a/tests/arch/quicklogic/qlf_k6n10f/mem_gen.py b/tests/arch/quicklogic/qlf_k6n10f/mem_gen.py index 226d6a1a0..b608e66eb 100644 --- a/tests/arch/quicklogic/qlf_k6n10f/mem_gen.py +++ b/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), diff --git a/tests/arch/quicklogic/qlf_k6n10f/meminit.ys b/tests/arch/quicklogic/qlf_k6n10f/meminit.ys index 2949e1590..8e9849c3b 100644 --- a/tests/arch/quicklogic/qlf_k6n10f/meminit.ys +++ b/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 diff --git a/tests/arch/xilinx/dsp_abc9.ys b/tests/arch/xilinx/dsp_abc9.ys index ae4839d7f..1d74cfa89 100644 --- a/tests/arch/xilinx/dsp_abc9.ys +++ b/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 diff --git a/tests/gen-tests-makefile.sh b/tests/gen-tests-makefile.sh index 3df36a963..6bf91b4dc 100755 --- a/tests/gen-tests-makefile.sh +++ b/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; diff --git a/tests/sat/asserts.ys b/tests/sat/asserts.ys index d8f994925..7df8dade3 100644 --- a/tests/sat/asserts.ys +++ b/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 diff --git a/tests/sat/asserts_seq.ys b/tests/sat/asserts_seq.ys index e97686644..db94f94ea 100644 --- a/tests/sat/asserts_seq.ys +++ b/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 diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 1436724b0..6fa94d52b 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -1,5 +1,5 @@ read_verilog -sv initval.v -proc;; +proc; async2sync;; sat -seq 10 -prove-asserts diff --git a/tests/sat/sizebits.ys b/tests/sat/sizebits.ys index 689227a41..61e1d6f70 100644 --- a/tests/sat/sizebits.ys +++ b/tests/sat/sizebits.ys @@ -1,2 +1,2 @@ read_verilog -sv sizebits.sv -prep; sat -verify -prove-asserts +prep; async2sync; sat -verify -prove-asserts diff --git a/tests/svtypes/enum_simple.ys b/tests/svtypes/enum_simple.ys index 79981657b..36922f5e0 100644 --- a/tests/svtypes/enum_simple.ys +++ b/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 diff --git a/tests/svtypes/struct_dynamic_range.ys b/tests/svtypes/struct_dynamic_range.ys index 9606e7384..c090b6e7c 100644 --- a/tests/svtypes/struct_dynamic_range.ys +++ b/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 diff --git a/tests/svtypes/typedef_initial_and_assign.ys b/tests/svtypes/typedef_initial_and_assign.ys index de456bb82..e778a49bb 100644 --- a/tests/svtypes/typedef_initial_and_assign.ys +++ b/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 \ No newline at end of file +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/svtypes/typedef_struct_port.ys b/tests/svtypes/typedef_struct_port.ys index 5b75c3105..dd0775b9f 100644 --- a/tests/svtypes/typedef_struct_port.ys +++ b/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 diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys index 52b3ee6bf..c052f6dba 100644 --- a/tests/various/chformal_coverenable.ys +++ b/tests/various/chformal_coverenable.ys @@ -13,6 +13,8 @@ EOT prep -top top +async2sync + select -assert-count 1 t:$cover chformal -cover -coverenable diff --git a/tests/various/chparam.sh b/tests/various/chparam.sh index d7712b807..0c237112e 100644 --- a/tests/various/chparam.sh +++ b/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' diff --git a/tests/various/const_arg_loop.ys b/tests/various/const_arg_loop.ys index 392532213..01bea7044 100644 --- a/tests/various/const_arg_loop.ys +++ b/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 diff --git a/tests/various/const_func.ys b/tests/various/const_func.ys index 2f60acfe6..d982c3a43 100644 --- a/tests/various/const_func.ys +++ b/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 diff --git a/tests/various/countbits.ys b/tests/various/countbits.ys index a556f7c5d..f2db9cfe1 100644 --- a/tests/various/countbits.ys +++ b/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 diff --git a/tests/various/param_struct.ys b/tests/various/param_struct.ys index b8de67968..bb26b61d5 100644 --- a/tests/various/param_struct.ys +++ b/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 diff --git a/tests/various/struct_access.ys b/tests/various/struct_access.ys index 2282edd92..43a2ac8b8 100644 --- a/tests/various/struct_access.ys +++ b/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 diff --git a/tests/verilog/asgn_expr.ys b/tests/verilog/asgn_expr.ys index 18180c785..78c005228 100644 --- a/tests/verilog/asgn_expr.ys +++ b/tests/verilog/asgn_expr.ys @@ -1,3 +1,4 @@ read_verilog -sv asgn_expr.sv proc +async2sync sat -verify -prove-asserts -show-all diff --git a/tests/verilog/atom_type_signedness.ys b/tests/verilog/atom_type_signedness.ys index 22bbe6efc..c8a82f993 100644 --- a/tests/verilog/atom_type_signedness.ys +++ b/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 diff --git a/tests/verilog/bug2042-sv.ys b/tests/verilog/bug2042-sv.ys index 91989f412..c3b904eb4 100644 --- a/tests/verilog/bug2042-sv.ys +++ b/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 diff --git a/tests/verilog/func_tern_hint.ys b/tests/verilog/func_tern_hint.ys index ab8a1e032..dfbd13bdf 100644 --- a/tests/verilog/func_tern_hint.ys +++ b/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 diff --git a/tests/verilog/func_upto.ys b/tests/verilog/func_upto.ys index 7a8c53506..df986a0ba 100644 --- a/tests/verilog/func_upto.ys +++ b/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 diff --git a/tests/verilog/int_types.ys b/tests/verilog/int_types.ys index c17c44b4c..344f3ee09 100644 --- a/tests/verilog/int_types.ys +++ b/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 diff --git a/tests/verilog/mem_bounds.ys b/tests/verilog/mem_bounds.ys index 42623ad09..146a6f433 100644 --- a/tests/verilog/mem_bounds.ys +++ b/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 diff --git a/tests/verilog/net_types.ys b/tests/verilog/net_types.ys index 9f75812ea..b3a0b2b38 100644 --- a/tests/verilog/net_types.ys +++ b/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 diff --git a/tests/verilog/package_task_func.ys b/tests/verilog/package_task_func.ys index c94cc2acb..0066946ae 100644 --- a/tests/verilog/package_task_func.ys +++ b/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 diff --git a/tests/verilog/param_no_default.ys b/tests/verilog/param_no_default.ys index 7f161a909..cc34c6a53 100644 --- a/tests/verilog/param_no_default.ys +++ b/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 diff --git a/tests/verilog/parameters_across_files.ys b/tests/verilog/parameters_across_files.ys index c53e40179..94565eb67 100644 --- a/tests/verilog/parameters_across_files.ys +++ b/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 diff --git a/tests/verilog/past_signedness.ys b/tests/verilog/past_signedness.ys index 91f32328b..65b9f69e4 100644 --- a/tests/verilog/past_signedness.ys +++ b/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 diff --git a/tests/verilog/prefix.ys b/tests/verilog/prefix.ys index ed3b3a111..399a985ae 100644 --- a/tests/verilog/prefix.ys +++ b/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 diff --git a/tests/verilog/sign_array_query.ys b/tests/verilog/sign_array_query.ys index f955450b7..b545b4015 100644 --- a/tests/verilog/sign_array_query.ys +++ b/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 diff --git a/tests/verilog/size_cast.ys b/tests/verilog/size_cast.ys index 6890cd2d5..e3fb4b0c7 100644 --- a/tests/verilog/size_cast.ys +++ b/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 diff --git a/tests/verilog/struct_access.ys b/tests/verilog/struct_access.ys index 29d569c01..c115f4ede 100644 --- a/tests/verilog/struct_access.ys +++ b/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 diff --git a/tests/verilog/typedef_across_files.ys b/tests/verilog/typedef_across_files.ys index ca9bba736..baa4b7919 100644 --- a/tests/verilog/typedef_across_files.ys +++ b/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 diff --git a/tests/verilog/typedef_legacy_conflict.ys b/tests/verilog/typedef_legacy_conflict.ys index 8dff4ec5f..dd1503a85 100644 --- a/tests/verilog/typedef_legacy_conflict.ys +++ b/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 diff --git a/tests/verilog/unbased_unsized.ys b/tests/verilog/unbased_unsized.ys index e1bc99c64..75d1bf5e4 100644 --- a/tests/verilog/unbased_unsized.ys +++ b/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 diff --git a/tests/verilog/unbased_unsized_shift.ys b/tests/verilog/unbased_unsized_shift.ys index c36049600..2b5b9d8d0 100644 --- a/tests/verilog/unbased_unsized_shift.ys +++ b/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 diff --git a/tests/verilog/unreachable_case_sign.ys b/tests/verilog/unreachable_case_sign.ys index 25bc0c6f0..569c8a313 100644 --- a/tests/verilog/unreachable_case_sign.ys +++ b/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