From 2baa578d949b449a05c91e4f3d0c4b96a92f4be7 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 22 Jan 2024 18:16:52 +0100 Subject: [PATCH 1/6] Remove too fragile smtlib2_module test This compares the write_smt2 output pretty much verbatim, which contains auto generated private names and fixes an arbitrary ordering. The tested functionality is also covered by SBY tests which actually interpret the write_smt2 output using an SMT solver and thus are much more robust, so we can safely remove this test. --- tests/various/smtlib2_module-expected.smt2 | 96 ---------------------- tests/various/smtlib2_module.sh | 5 -- tests/various/smtlib2_module.v | 33 -------- 3 files changed, 134 deletions(-) delete mode 100644 tests/various/smtlib2_module-expected.smt2 delete mode 100755 tests/various/smtlib2_module.sh delete mode 100644 tests/various/smtlib2_module.v diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2 deleted file mode 100644 index 494e7cda095..00000000000 --- a/tests/various/smtlib2_module-expected.smt2 +++ /dev/null @@ -1,96 +0,0 @@ -; SMT-LIBv2 description generated by Yosys $VERSION -; yosys-smt2-module smtlib2 -(declare-sort |smtlib2_s| 0) -(declare-fun |smtlib2_is| (|smtlib2_s|) Bool) -(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a -; yosys-smt2-input a 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8} -(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state)) -(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b -; yosys-smt2-input b 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8} -(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state)) -; yosys-smt2-output add 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8} -(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( -(|a| (|smtlib2_n a| state)) -(|b| (|smtlib2_n b| state)) -) -(bvadd a b) -)) -; yosys-smt2-output eq 1 -; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1} -(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let ( -(|a| (|smtlib2_n a| state)) -(|b| (|smtlib2_n b| state)) -) -(= a b) -)) -; yosys-smt2-output sub 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8} -(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let ( -(|a| (|smtlib2_n a| state)) -(|b| (|smtlib2_n b| state)) -) -(bvadd a (bvneg b)) -)) -(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true) -(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true) -(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true) -(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true) -(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2 -; yosys-smt2-module uut -(declare-sort |uut_s| 0) -(declare-fun |uut_is| (|uut_s|) Bool) -; yosys-smt2-cell smtlib2 s -; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"} -(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add -(declare-fun |uut#1| (|uut_s|) Bool) ; \eq -(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub -(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|) -; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26 -; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8} -(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a -; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41 -; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8} -(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b -(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2 -(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9 -; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22 -(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19 -(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2 -(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11 -; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22 -(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20 -(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y -(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13 -; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25 -(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21 -(define-fun |uut_a| ((state |uut_s|)) Bool (and - (|uut_a 0| state) - (|uut_a 1| state) - (|uut_a 2| state) - (|smtlib2_a| (|uut_h s| state)) -)) -(define-fun |uut_u| ((state |uut_s|)) Bool - (|smtlib2_u| (|uut_h s| state)) -) -(define-fun |uut_i| ((state |uut_s|)) Bool - (|smtlib2_i| (|uut_h s| state)) -) -(define-fun |uut_h| ((state |uut_s|)) Bool (and - (= (|uut_is| state) (|smtlib2_is| (|uut_h s| state))) - (= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a - (= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add - (= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b - (= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq - (= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub - (|smtlib2_h| (|uut_h s| state)) -)) -(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and - (= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b - (= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a - (|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state)) -)) ; end of module uut -; yosys-smt2-topmod uut -; end of yosys output diff --git a/tests/various/smtlib2_module.sh b/tests/various/smtlib2_module.sh deleted file mode 100755 index a2206eea73d..00000000000 --- a/tests/various/smtlib2_module.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/usr/bin/env bash -set -ex -../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2' -sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/ *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2 -diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2 diff --git a/tests/various/smtlib2_module.v b/tests/various/smtlib2_module.v deleted file mode 100644 index 4aad8690527..00000000000 --- a/tests/various/smtlib2_module.v +++ /dev/null @@ -1,33 +0,0 @@ -(* smtlib2_module *) -module smtlib2(a, b, add, sub, eq); - input [7:0] a, b; - (* smtlib2_comb_expr = "(bvadd a b)" *) - output [7:0] add; - (* smtlib2_comb_expr = "(bvadd a (bvneg b))" *) - output [7:0] sub; - (* smtlib2_comb_expr = "(= a b)" *) - output eq; -endmodule - -(* top *) -module uut; - wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2; - wire eq; - - assign add2 = a + b; - assign sub2 = a - b; - - smtlib2 s ( - .a(a), - .b(b), - .add(add), - .sub(sub), - .eq(eq) - ); - - always @* begin - assert(add == add2); - assert(sub == sub2); - assert(eq == (a == b)); - end -endmodule From 331ac5285fa61deaa288ed1496da77e40c495640 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 22 Jan 2024 17:44:05 +0100 Subject: [PATCH 2/6] 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 | 3 ++- tests/arch/quicklogic/qlf_k6n10f/mem_gen.py | 17 +++++++++-------- tests/arch/quicklogic/qlf_k6n10f/meminit.ys | 1 + tests/arch/xilinx/dsp_abc9.ys | 1 + tests/gen-tests-makefile.sh | 2 +- tests/sat/asserts.ys | 2 +- tests/sat/asserts_seq.ys | 2 +- tests/sat/initval.ys | 2 +- tests/sat/sizebits.ys | 2 +- tests/svtypes/enum_simple.ys | 2 +- tests/svtypes/struct_dynamic_range.ys | 1 + tests/svtypes/typedef_initial_and_assign.ys | 4 ++-- tests/svtypes/typedef_struct_port.ys | 2 +- tests/various/chformal_coverenable.ys | 2 ++ tests/various/chparam.sh | 3 +++ tests/various/const_arg_loop.ys | 1 + tests/various/const_func.ys | 1 + tests/various/countbits.ys | 1 + tests/various/param_struct.ys | 1 + tests/various/struct_access.ys | 1 + tests/verilog/asgn_expr.ys | 1 + tests/verilog/atom_type_signedness.ys | 2 +- tests/verilog/bug2042-sv.ys | 2 ++ tests/verilog/func_tern_hint.ys | 1 + tests/verilog/func_upto.ys | 1 + tests/verilog/int_types.ys | 1 + tests/verilog/mem_bounds.ys | 1 + tests/verilog/net_types.ys | 1 + tests/verilog/package_task_func.ys | 1 + tests/verilog/param_no_default.ys | 1 + tests/verilog/parameters_across_files.ys | 1 + tests/verilog/past_signedness.ys | 2 ++ tests/verilog/prefix.ys | 1 + tests/verilog/sign_array_query.ys | 3 +++ tests/verilog/size_cast.ys | 1 + tests/verilog/struct_access.ys | 1 + tests/verilog/typedef_across_files.ys | 1 + tests/verilog/typedef_legacy_conflict.ys | 1 + tests/verilog/unbased_unsized.ys | 1 + tests/verilog/unbased_unsized_shift.ys | 1 + tests/verilog/unreachable_case_sign.ys | 2 ++ 41 files changed, 59 insertions(+), 19 deletions(-) diff --git a/tests/arch/quicklogic/qlf_k6n10f/dsp.ys b/tests/arch/quicklogic/qlf_k6n10f/dsp.ys index 023ff0d89f6..1e652855bbd 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 226d6a1a0d7..b608e66eba9 100644 --- a/tests/arch/quicklogic/qlf_k6n10f/mem_gen.py +++ b/tests/arch/quicklogic/qlf_k6n10f/mem_gen.py @@ -36,7 +36,7 @@ ([("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 @@ 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 @@ class 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 @@ class 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 @@ class 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 @@ class TestClass: 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 2949e1590d9..8e9849c3b46 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 ae4839d7f1f..1d74cfa89b2 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 3df36a963b1..6bf91b4dc34 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 d8f9949257f..7df8dade38c 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 e97686644c6..db94f94ea69 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 1436724b0d3..6fa94d52bc8 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 689227a4177..61e1d6f7097 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 79981657b6f..36922f5e09f 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 9606e73840c..c090b6e7c9b 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 de456bb82bd..e778a49bb01 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 5b75c310551..dd0775b9ff9 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 52b3ee6bf60..c052f6dbafe 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 d7712b80734..0c237112e09 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 392532213b4..01bea704499 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 2f60acfe670..d982c3a43fa 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 a556f7c5d83..f2db9cfe1f6 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 b8de67968d5..bb26b61d586 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 2282edd9246..43a2ac8b827 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 18180c7854f..78c005228f4 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 22bbe6efc2f..c8a82f993c5 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 91989f412c5..c3b904eb4ac 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 ab8a1e032ed..dfbd13bdf39 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 7a8c5350649..df986a0ba26 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 c17c44b4ce0..344f3ee09aa 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 42623ad097b..146a6f43302 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 9f75812ea4a..b3a0b2b38f3 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 c94cc2acb26..0066946aed8 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 7f161a909b7..cc34c6a53e3 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 c53e4017930..94565eb6703 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 91f32328b43..65b9f69e478 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 ed3b3a111a6..399a985aef0 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 f955450b793..b545b401516 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 6890cd2d5b5..e3fb4b0c7ca 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 29d569c010a..c115f4ede96 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 ca9bba7361c..baa4b7919dd 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 8dff4ec5f4e..dd1503a852c 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 e1bc99c64a7..75d1bf5e4b5 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 c36049600fd..2b5b9d8d082 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 25bc0c6f040..569c8a313c8 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 From 6c4902313bc76bae367444fe6e363bb340cf084e Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 22 Jan 2024 18:30:24 +0100 Subject: [PATCH 3/6] chformal: Support $check cells and add chformal -lower This adds support for `$check` cells in chformal and adds a `-lower` mode which converts `$check` cells into `$assert` etc. cells with a `$print` cell to output the `$check` message. --- passes/cmds/chformal.cc | 183 ++++++++++++++++++++++++++++++++++------ 1 file changed, 158 insertions(+), 25 deletions(-) diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index da97ff71d69..e027103bb03 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -23,6 +23,52 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +static RTLIL::IdString formal_flavor(RTLIL::Cell *cell) +{ + if (cell->type != ID($check)) + return cell->type; + + std::string flavor_param = cell->getParam(ID(FLAVOR)).decode_string(); + if (flavor_param == "assert") + return ID($assert); + else if (flavor_param == "assume") + return ID($assume); + else if (flavor_param == "cover") + return ID($cover); + else if (flavor_param == "live") + return ID($live); + else if (flavor_param == "fair") + return ID($fair); + else + log_abort(); +} + +static void set_formal_flavor(RTLIL::Cell *cell, RTLIL::IdString flavor) +{ + if (cell->type != ID($check)) { + cell->type = flavor; + return; + } + + if (flavor == ID($assert)) + cell->setParam(ID(FLAVOR), std::string("assert")); + else if (flavor == ID($assume)) + cell->setParam(ID(FLAVOR), std::string("assume")); + else if (flavor == ID($cover)) + cell->setParam(ID(FLAVOR), std::string("cover")); + else if (flavor == ID($live)) + cell->setParam(ID(FLAVOR), std::string("live")); + else if (flavor == ID($fair)) + cell->setParam(ID(FLAVOR), std::string("fair")); + else + log_abort(); +} + +static bool is_triggered_check_cell(RTLIL::Cell * cell) +{ + return cell->type == ID($check) && cell->getParam(ID(TRG_ENABLE)).as_bool(); +} + struct ChformalPass : public Pass { ChformalPass() : Pass("chformal", "change formal constraints of the design") { } void help() override @@ -41,13 +87,18 @@ struct ChformalPass : public Pass { log(" -fair $fair cells, representing assume(s_eventually ...)\n"); log(" -cover $cover cells, representing cover() statements\n"); log("\n"); + log(" Additionally chformal will operate on $check cells corresponding to the\n"); + log(" selected constraint types.\n"); + log("\n"); log("Exactly one of the following modes must be specified:\n"); log("\n"); log(" -remove\n"); log(" remove the cells and thus constraints from the design\n"); log("\n"); log(" -early\n"); - log(" bypass FFs that only delay the activation of a constraint\n"); + log(" bypass FFs that only delay the activation of a constraint. When inputs\n"); + log(" of the bypassed FFs do not remain stable between clock edges, this may\n"); + log(" result in unexpected behavior.\n"); log("\n"); log(" -delay \n"); log(" delay activation of the constraint by clock cycles\n"); @@ -69,6 +120,11 @@ struct ChformalPass : public Pass { log(" -fair2live\n"); log(" change the roles of cells as indicated. these options can be combined\n"); log("\n"); + log(" -lower\n"); + log(" convert each $check cell into an $assert, $assume, $live, $fair or\n"); + log(" $cover cell. If the $check cell contains a message, also produce a\n"); + log(" $print cell.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -146,6 +202,10 @@ struct ChformalPass : public Pass { mode = 'c'; continue; } + if (mode == 0 && args[argidx] == "-lower") { + mode = 'l'; + continue; + } break; } extra_args(args, argidx, design); @@ -166,7 +226,7 @@ struct ChformalPass : public Pass { vector constr_cells; for (auto cell : module->selected_cells()) - if (constr_types.count(cell->type)) + if (constr_types.count(formal_flavor(cell))) constr_cells.push_back(cell); if (mode == 'r') @@ -216,6 +276,18 @@ struct ChformalPass : public Pass { } for (auto cell : constr_cells) + { + if (is_triggered_check_cell(cell)) { + if (cell->getParam(ID::TRG_WIDTH).as_int() != 1) + continue; + cell->setPort(ID::TRG, SigSpec()); + cell->setParam(ID::TRG_ENABLE, false); + cell->setParam(ID::TRG_WIDTH, 0); + cell->setParam(ID::TRG_POLARITY, false); + } + + IdString flavor = formal_flavor(cell); + while (true) { SigSpec A = sigmap(cell->getPort(ID::A)); @@ -225,8 +297,8 @@ struct ChformalPass : public Pass { break; if (!init_zero.count(EN)) { - if (cell->type == ID($cover)) break; - if (cell->type.in(ID($assert), ID($assume)) && !init_one.count(A)) break; + if (flavor == ID($cover)) break; + if (flavor.in(ID($assert), ID($assume)) && !init_one.count(A)) break; } const auto &A_map = ffmap.at(A); @@ -238,25 +310,31 @@ struct ChformalPass : public Pass { cell->setPort(ID::A, A_map.first); cell->setPort(ID::EN, EN_map.first); } + } } else if (mode == 'd') { for (auto cell : constr_cells) - for (int i = 0; i < mode_arg; i++) { - SigSpec orig_a = cell->getPort(ID::A); - SigSpec orig_en = cell->getPort(ID::EN); + if (is_triggered_check_cell(cell)) + log_error("Cannot delay edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell)); - Wire *new_a = module->addWire(NEW_ID); - Wire *new_en = module->addWire(NEW_ID); - new_en->attributes[ID::init] = State::S0; + for (int i = 0; i < mode_arg; i++) + { + SigSpec orig_a = cell->getPort(ID::A); + SigSpec orig_en = cell->getPort(ID::EN); + + Wire *new_a = module->addWire(NEW_ID); + Wire *new_en = module->addWire(NEW_ID); + new_en->attributes[ID::init] = State::S0; - module->addFf(NEW_ID, orig_a, new_a); - module->addFf(NEW_ID, orig_en, new_en); + module->addFf(NEW_ID, orig_a, new_a); + module->addFf(NEW_ID, orig_en, new_en); - cell->setPort(ID::A, new_a); - cell->setPort(ID::EN, new_en); + cell->setPort(ID::A, new_a); + cell->setPort(ID::EN, new_en); + } } } else @@ -278,21 +356,76 @@ struct ChformalPass : public Pass { if (mode =='p') { for (auto cell : constr_cells) - module->addCover(NEW_ID_SUFFIX("coverenable"), - cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); + { + if (cell->type == ID($check)) { + Cell *cover = module->addCell(NEW_ID_SUFFIX("coverenable"), ID($check)); + cover->attributes = cell->attributes; + cover->parameters = cell->parameters; + cover->setParam(ID(FLAVOR), Const("cover")); + + for (auto const &conn : cell->connections()) + if (!conn.first.in(ID::A, ID::EN)) + cover->setPort(conn.first, conn.second); + cover->setPort(ID::A, cell->getPort(ID::EN)); + cover->setPort(ID::EN, State::S1); + } else { + module->addCover(NEW_ID_SUFFIX("coverenable"), + cell->getPort(ID::EN), State::S1, cell->get_src_attribute()); + } + } } else if (mode == 'c') { - for (auto cell : constr_cells) - if (assert2assume && cell->type == ID($assert)) - cell->type = ID($assume); - else if (assume2assert && cell->type == ID($assume)) - cell->type = ID($assert); - else if (live2fair && cell->type == ID($live)) - cell->type = ID($fair); - else if (fair2live && cell->type == ID($fair)) - cell->type = ID($live); + for (auto cell : constr_cells) { + IdString flavor = formal_flavor(cell); + if (assert2assume && flavor == ID($assert)) + set_formal_flavor(cell, ID($assume)); + else if (assume2assert && flavor == ID($assume)) + set_formal_flavor(cell, ID($assert)); + else if (live2fair && flavor == ID($live)) + set_formal_flavor(cell, ID($fair)); + else if (fair2live && flavor == ID($fair)) + set_formal_flavor(cell, ID($live)); + } + } + else + if (mode == 'l') + { + for (auto cell : constr_cells) { + if (cell->type != ID($check)) + continue; + + if (is_triggered_check_cell(cell)) + log_error("Cannot lower edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell)); + + + Cell *plain_cell = module->addCell(NEW_ID, formal_flavor(cell)); + + plain_cell->attributes = cell->attributes; + + SigBit sig_a = cell->getPort(ID::A); + SigBit sig_en = cell->getPort(ID::EN); + + plain_cell->setPort(ID::A, sig_a); + plain_cell->setPort(ID::EN, sig_en); + + if (plain_cell->type.in(ID($assert), ID($assume))) + sig_a = module->Not(NEW_ID, sig_a); + + SigBit combined_en = module->And(NEW_ID, sig_a, sig_en); + + module->swap_names(cell, plain_cell); + + if (cell->getPort(ID::ARGS).empty()) { + module->remove(cell); + } else { + cell->type = ID($print); + cell->setPort(ID::EN, combined_en); + cell->unsetPort(ID::A); + cell->unsetParam(ID(FLAVOR)); + } + } } } } From e1a59ba80b123bf28f2185c91b051895903493ce Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 22 Jan 2024 18:32:23 +0100 Subject: [PATCH 4/6] async2sync, clk2fflogic: Add support for $check and $print cells --- passes/sat/async2sync.cc | 73 +++++++++- passes/sat/clk2fflogic.cc | 185 +++++++++++++++++--------- tests/various/chformal_coverenable.ys | 2 + 3 files changed, 194 insertions(+), 66 deletions(-) diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index 6fdf470b12b..93c7e96c809 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -41,31 +41,88 @@ struct Async2syncPass : public Pass { log("reset value in the next cycle regardless of the data-in value at the time of\n"); log("the clock edge.\n"); log("\n"); + log(" -nolower\n"); + log(" Do not automatically run 'chformal -lower' to lower $check cells.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { - // bool flag_noinit = false; + bool flag_nolower = false; log_header(design, "Executing ASYNC2SYNC pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - // if (args[argidx] == "-noinit") { - // flag_noinit = true; - // continue; - // } + if (args[argidx] == "-nolower") { + flag_nolower = true; + continue; + } break; } extra_args(args, argidx, design); + bool have_check_cells = false; + for (auto module : design->selected_modules()) { SigMap sigmap(module); FfInitVals initvals(&sigmap, module); + SigBit initstate; + for (auto cell : vector(module->selected_cells())) { + if (cell->type.in(ID($print), ID($check))) + { + if (cell->type == ID($check)) + have_check_cells = true; + + bool trg_enable = cell->getParam(ID(TRG_ENABLE)).as_bool(); + if (!trg_enable) + continue; + + int trg_width = cell->getParam(ID(TRG_WIDTH)).as_int(); + + if (trg_width > 1) + log_error("$check cell %s with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic.\n", log_id(cell)); + + if (trg_width == 0) { + if (initstate == State::S0) + initstate = module->Initstate(NEW_ID); + + SigBit sig_en = cell->getPort(ID::EN); + cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate)); + } else { + SigBit sig_en = cell->getPort(ID::EN); + SigSpec sig_args = cell->getPort(ID::ARGS); + bool trg_polarity = cell->getParam(ID(TRG_POLARITY)).as_bool(); + SigBit sig_trg = cell->getPort(ID::TRG); + Wire *sig_en_q = module->addWire(NEW_ID); + Wire *sig_args_q = module->addWire(NEW_ID, GetSize(sig_args)); + sig_en_q->attributes.emplace(ID::init, State::S0); + module->addDff(NEW_ID, sig_trg, sig_en, sig_en_q, trg_polarity, cell->get_src_attribute()); + module->addDff(NEW_ID, sig_trg, sig_args, sig_args_q, trg_polarity, cell->get_src_attribute()); + cell->setPort(ID::EN, sig_en_q); + cell->setPort(ID::ARGS, sig_args_q); + if (cell->type == ID($check)) { + SigBit sig_a = cell->getPort(ID::A); + Wire *sig_a_q = module->addWire(NEW_ID); + sig_a_q->attributes.emplace(ID::init, State::S1); + module->addDff(NEW_ID, sig_trg, sig_a, sig_a_q, trg_polarity, cell->get_src_attribute()); + cell->setPort(ID::A, sig_a_q); + } + } + + cell->setPort(ID::TRG, SigSpec()); + + cell->setParam(ID::TRG_ENABLE, false); + cell->setParam(ID::TRG_WIDTH, 0); + cell->setParam(ID::TRG_POLARITY, false); + cell->set_bool_attribute(ID(trg_on_gclk)); + continue; + } + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) continue; @@ -273,6 +330,12 @@ struct Async2syncPass : public Pass { ff.emit(); } } + + if (have_check_cells && !flag_nolower) { + log_push(); + Pass::call(design, "chformal -lower"); + log_pop(); + } } } Async2syncPass; diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 3dc96ecce2a..2c0e13f852e 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -48,6 +48,9 @@ struct Clk2fflogicPass : public Pass { log("reset value in the next cycle regardless of the data-in value at the time of\n"); log("the clock edge.\n"); log("\n"); + log(" -nolower\n"); + log(" Do not automatically run 'chformal -lower' to lower $check cells.\n"); + log("\n"); } // Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted. SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) { @@ -117,21 +120,23 @@ struct Clk2fflogicPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { - // bool flag_noinit = false; + bool flag_nolower = false; log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - // if (args[argidx] == "-noinit") { - // flag_noinit = true; - // continue; - // } + if (args[argidx] == "-nolower") { + flag_nolower = true; + continue; + } break; } extra_args(args, argidx, design); + bool have_check_cells = false; + for (auto module : design->selected_modules()) { SigMap sigmap(module); @@ -194,79 +199,137 @@ struct Clk2fflogicPass : public Pass { mem.emit(); } + SigBit initstate; + for (auto cell : vector(module->selected_cells())) { - SigSpec qval; - if (RTLIL::builtin_ff_cell_types().count(cell->type)) { - FfData ff(&initvals, cell); + if (cell->type.in(ID($print), ID($check))) + { + if (cell->type == ID($check)) + have_check_cells = true; - if (ff.has_gclk) { - // Already a $ff or $_FF_ cell. + bool trg_enable = cell->getParam(ID(TRG_ENABLE)).as_bool(); + if (!trg_enable) continue; - } - if (ff.has_clk) { - log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q)); - } else if (ff.has_aload) { - log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q)); + int trg_width = cell->getParam(ID(TRG_WIDTH)).as_int(); + + if (trg_width == 0) { + if (initstate == State::S0) + initstate = module->Initstate(NEW_ID); + + SigBit sig_en = cell->getPort(ID::EN); + cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate)); } else { - // $sr. - log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n", - log_id(module), log_id(cell), log_id(cell->type), - log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q)); + SigBit sig_en = cell->getPort(ID::EN); + SigSpec sig_args = cell->getPort(ID::ARGS); + Const trg_polarity = cell->getParam(ID(TRG_POLARITY)); + SigSpec sig_trg = cell->getPort(ID::TRG); + + SigSpec sig_trg_sampled; + + for (auto const &bit : sig_trg) + sig_trg_sampled.append(sample_control_edge(module, bit, trg_polarity[GetSize(sig_trg_sampled)] == State::S1, false)); + SigSpec sig_args_sampled = sample_data(module, sig_args, Const(State::S0, GetSize(sig_args)), false, false).sampled; + SigBit sig_en_sampled = sample_data(module, sig_en, State::S0, false, false).sampled; + + SigBit sig_trg_combined = module->ReduceOr(NEW_ID, sig_trg_sampled); + + cell->setPort(ID::EN, module->And(NEW_ID, sig_en_sampled, sig_trg_combined)); + cell->setPort(ID::ARGS, sig_args_sampled); + if (cell->type == ID($check)) { + SigBit sig_a_sampled = sample_data(module, sig_en, State::S1, false, false).sampled; + cell->setPort(ID::A, sig_a_sampled); + } } - ff.remove(); + cell->setPort(ID::TRG, SigSpec()); - if (ff.has_clk) - ff.unmap_ce_srst(); + cell->setParam(ID::TRG_ENABLE, false); + cell->setParam(ID::TRG_WIDTH, 0); + cell->setParam(ID::TRG_POLARITY, false); + cell->set_bool_attribute(ID(trg_on_gclk)); - auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled; + continue; + } - if (ff.has_clk) { - // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs - auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine); - auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine); - next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine); - } + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + continue; - SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst; - // The check for a constant sig_aload is also done by opt_dff, but when using verific and running - // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids - // generating a lot of extra logic. - bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1); - if (has_nonconst_aload) { - sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine); - // The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs - sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine); - } - if (ff.has_sr) { - sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine); - sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine); - } - if (ff.has_arst) - sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine); - - // First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous - // implementation, this approach correctly handles all the cases of multiple signals changing simultaneously. - for (int current = 0; current < 2; current++) { - if (has_nonconst_aload) - next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine); - if (ff.has_sr) - next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine); - if (ff.has_arst) - next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine); - } + FfData ff(&initvals, cell); - module->connect(ff.sig_q, next_q); + if (ff.has_gclk) { + // Already a $ff or $_FF_ cell. + continue; } + + if (ff.has_clk) { + log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q)); + } else if (ff.has_aload) { + log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q)); + } else { + // $sr. + log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n", + log_id(module), log_id(cell), log_id(cell->type), + log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q)); + } + + ff.remove(); + + if (ff.has_clk) + ff.unmap_ce_srst(); + + auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled; + + if (ff.has_clk) { + // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs + auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine); + auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine); + next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine); + } + + SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst; + // The check for a constant sig_aload is also done by opt_dff, but when using verific and running + // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids + // generating a lot of extra logic. + bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1); + if (has_nonconst_aload) { + sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine); + // The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs + sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine); + } + if (ff.has_sr) { + sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine); + sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine); + } + if (ff.has_arst) + sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine); + + // First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous + // implementation, this approach correctly handles all the cases of multiple signals changing simultaneously. + for (int current = 0; current < 2; current++) { + if (has_nonconst_aload) + next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine); + if (ff.has_sr) + next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine); + if (ff.has_arst) + next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine); + } + + module->connect(ff.sig_q, next_q); + } } + if (have_check_cells && !flag_nolower) { + log_push(); + Pass::call(design, "chformal -lower"); + log_pop(); + } } } Clk2fflogicPass; diff --git a/tests/various/chformal_coverenable.ys b/tests/various/chformal_coverenable.ys index c052f6dbafe..efb197773b8 100644 --- a/tests/various/chformal_coverenable.ys +++ b/tests/various/chformal_coverenable.ys @@ -13,6 +13,8 @@ EOT prep -top top +design -save prep + async2sync select -assert-count 1 t:$cover From c7bf0e3b8f05f898974c00f05ce8e23aac296cac Mon Sep 17 00:00:00 2001 From: Catherine Date: Thu, 11 Jan 2024 09:39:28 +0000 Subject: [PATCH 5/6] Add new `$check` cell to represent assertions with a message. --- backends/cxxrtl/cxxrtl_backend.cc | 363 +++++++++++++++--------- backends/cxxrtl/runtime/cxxrtl/cxxrtl.h | 27 +- backends/verilog/verilog_backend.cc | 88 +++++- docs/source/CHAPTER_CellLib.rst | 6 +- frontends/ast/genrtlil.cc | 189 ++++++++---- frontends/ast/simplify.cc | 95 +------ kernel/celltypes.h | 1 + kernel/constids.inc | 1 + kernel/rtlil.cc | 22 ++ passes/hierarchy/hierarchy.cc | 2 +- passes/opt/opt_clean.cc | 2 +- techlibs/common/simlib.v | 24 +- 12 files changed, 515 insertions(+), 305 deletions(-) diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index d2bca306504..c60b43d3faa 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -218,7 +218,7 @@ bool is_internal_cell(RTLIL::IdString type) bool is_effectful_cell(RTLIL::IdString type) { - return type.isPublic() || type == ID($print); + return type.in(ID($print), ID($check)); } bool is_cxxrtl_blackbox_cell(const RTLIL::Cell *cell) @@ -282,7 +282,7 @@ struct FlowGraph { CONNECT, CELL_SYNC, CELL_EVAL, - PRINT_SYNC, + EFFECT_SYNC, PROCESS_SYNC, PROCESS_CASE, MEM_RDPORT, @@ -292,7 +292,7 @@ struct FlowGraph { Type type; RTLIL::SigSig connect = {}; const RTLIL::Cell *cell = nullptr; - std::vector print_sync_cells; + std::vector cells; const RTLIL::Process *process = nullptr; const Mem *mem = nullptr; int portidx; @@ -480,11 +480,11 @@ struct FlowGraph { return node; } - Node *add_print_sync_node(std::vector cells) + Node *add_effect_sync_node(std::vector cells) { Node *node = new Node; - node->type = Node::Type::PRINT_SYNC; - node->print_sync_cells = cells; + node->type = Node::Type::EFFECT_SYNC; + node->cells = cells; nodes.push_back(node); return node; } @@ -1063,99 +1063,6 @@ struct CxxrtlWorker { f << ".val()"; } - void dump_print(const RTLIL::Cell *cell) - { - Fmt fmt = {}; - fmt.parse_rtlil(cell); - - f << indent << "if ("; - dump_sigspec_rhs(cell->getPort(ID::EN)); - f << " == value<1>{1u}) {\n"; - inc_indent(); - dict fmt_args; - f << indent << "struct : public lazy_fmt {\n"; - inc_indent(); - f << indent << "std::string operator() () const override {\n"; - inc_indent(); - fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) { - if (sig.size() == 0) - f << "value<0>()"; - else { - std::string arg_name = "arg" + std::to_string(fmt_args.size()); - fmt_args[arg_name] = sig; - f << arg_name; - } - }, "performer"); - dec_indent(); - f << indent << "}\n"; - f << indent << "struct performer *performer;\n"; - for (auto arg : fmt_args) - f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n"; - dec_indent(); - f << indent << "} formatter;\n"; - f << indent << "formatter.performer = performer;\n"; - for (auto arg : fmt_args) { - f << indent << "formatter." << arg.first << " = "; - dump_sigspec_rhs(arg.second); - f << ";\n"; - } - f << indent << "if (performer) {\n"; - inc_indent(); - f << indent << "static const metadata_map attributes = "; - dump_metadata_map(cell->attributes); - f << ";\n"; - f << indent << "performer->on_print(formatter, attributes);\n"; - dec_indent(); - f << indent << "} else {\n"; - inc_indent(); - f << indent << print_output << " << formatter();\n"; - dec_indent(); - f << indent << "}\n"; - dec_indent(); - f << indent << "}\n"; - } - - void dump_sync_print(std::vector &cells) - { - log_assert(!cells.empty()); - const auto &trg = cells[0]->getPort(ID::TRG); - const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY); - - f << indent << "if ("; - for (int i = 0; i < trg.size(); i++) { - RTLIL::SigBit trg_bit = trg[i]; - trg_bit = sigmaps[trg_bit.wire->module](trg_bit); - log_assert(trg_bit.wire); - - if (i != 0) - f << " || "; - - if (trg_polarity[i] == State::S1) - f << "posedge_"; - else - f << "negedge_"; - f << mangle(trg_bit); - } - f << ") {\n"; - inc_indent(); - std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) { - return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int(); - }); - for (auto cell : cells) { - log_assert(cell->getParam(ID::TRG_ENABLE).as_bool()); - log_assert(cell->getPort(ID::TRG) == trg); - log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity); - - std::vector inlined_cells; - collect_cell_eval(cell, /*for_debug=*/false, inlined_cells); - dump_inlined_cells(inlined_cells); - dump_print(cell); - } - dec_indent(); - - f << indent << "}\n"; - } - void dump_inlined_cells(const std::vector &cells) { if (cells.empty()) { @@ -1309,6 +1216,144 @@ struct CxxrtlWorker { } } + void dump_print(const RTLIL::Cell *cell) + { + Fmt fmt; + fmt.parse_rtlil(cell); + + f << indent << "if ("; + dump_sigspec_rhs(cell->getPort(ID::EN)); + f << " == value<1>{1u}) {\n"; + inc_indent(); + dict fmt_args; + f << indent << "struct : public lazy_fmt {\n"; + inc_indent(); + f << indent << "std::string operator() () const override {\n"; + inc_indent(); + fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) { + if (sig.size() == 0) + f << "value<0>()"; + else { + std::string arg_name = "arg" + std::to_string(fmt_args.size()); + fmt_args[arg_name] = sig; + f << arg_name; + } + }, "performer"); + dec_indent(); + f << indent << "}\n"; + f << indent << "struct performer *performer;\n"; + for (auto arg : fmt_args) + f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n"; + dec_indent(); + f << indent << "} formatter;\n"; + f << indent << "formatter.performer = performer;\n"; + for (auto arg : fmt_args) { + f << indent << "formatter." << arg.first << " = "; + dump_sigspec_rhs(arg.second); + f << ";\n"; + } + f << indent << "if (performer) {\n"; + inc_indent(); + f << indent << "static const metadata_map attributes = "; + dump_metadata_map(cell->attributes); + f << ";\n"; + f << indent << "performer->on_print(formatter, attributes);\n"; + dec_indent(); + f << indent << "} else {\n"; + inc_indent(); + f << indent << print_output << " << formatter();\n"; + dec_indent(); + f << indent << "}\n"; + dec_indent(); + f << indent << "}\n"; + } + + void dump_effect(const RTLIL::Cell *cell) + { + Fmt fmt; + fmt.parse_rtlil(cell); + + f << indent << "if ("; + dump_sigspec_rhs(cell->getPort(ID::EN)); + f << ") {\n"; + inc_indent(); + dict fmt_args; + f << indent << "struct : public lazy_fmt {\n"; + inc_indent(); + f << indent << "std::string operator() () const override {\n"; + inc_indent(); + fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) { + if (sig.size() == 0) + f << "value<0>()"; + else { + std::string arg_name = "arg" + std::to_string(fmt_args.size()); + fmt_args[arg_name] = sig; + f << arg_name; + } + }, "performer"); + dec_indent(); + f << indent << "}\n"; + f << indent << "struct performer *performer;\n"; + for (auto arg : fmt_args) + f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n"; + dec_indent(); + f << indent << "} formatter;\n"; + f << indent << "formatter.performer = performer;\n"; + for (auto arg : fmt_args) { + f << indent << "formatter." << arg.first << " = "; + dump_sigspec_rhs(arg.second); + f << ";\n"; + } + if (cell->hasPort(ID::A)) { + f << indent << "bool condition = (bool)"; + dump_sigspec_rhs(cell->getPort(ID::A)); + f << ";\n"; + } + f << indent << "if (performer) {\n"; + inc_indent(); + f << indent << "static const metadata_map attributes = "; + dump_metadata_map(cell->attributes); + f << ";\n"; + if (cell->type == ID($print)) { + f << indent << "performer->on_print(formatter, attributes);\n"; + } else if (cell->type == ID($check)) { + std::string flavor = cell->getParam(ID::FLAVOR).decode_string(); + f << indent << "performer->on_check("; + if (flavor == "assert") + f << "flavor::ASSERT"; + else if (flavor == "assume") + f << "flavor::ASSUME"; + else if (flavor == "live") + f << "flavor::ASSERT_EVENTUALLY"; + else if (flavor == "fair") + f << "flavor::ASSUME_EVENTUALLY"; + else if (flavor == "cover") + f << "flavor::COVER"; + else log_assert(false); + f << ", condition, formatter, attributes);\n"; + } else log_assert(false); + dec_indent(); + f << indent << "} else {\n"; + inc_indent(); + if (cell->type == ID($print)) { + f << indent << print_output << " << formatter();\n"; + } else if (cell->type == ID($check)) { + std::string flavor = cell->getParam(ID::FLAVOR).decode_string(); + if (flavor == "assert" || flavor == "assume") { + f << indent << "if (!condition) {\n"; + inc_indent(); + f << indent << "std::cerr << formatter();\n"; + dec_indent(); + f << indent << "}\n"; + f << indent << "CXXRTL_ASSERT(condition && \"Check failed\");\n"; + } + } else log_assert(false); + dec_indent(); + f << indent << "}\n"; + dec_indent(); + f << indent << "}\n"; + } + void dump_cell_eval(const RTLIL::Cell *cell, bool for_debug = false) { std::vector inlined_cells; @@ -1322,30 +1367,34 @@ struct CxxrtlWorker { f << " = "; dump_cell_expr(cell, for_debug); f << ";\n"; - // $print cell - } else if (cell->type == ID($print)) { + // Effectful cells + } else if (is_effectful_cell(cell->type)) { log_assert(!for_debug); - // Sync $print cells are grouped into PRINT_SYNC nodes in the FlowGraph. + // Sync effectful cells are grouped into EFFECT_SYNC nodes in the FlowGraph. log_assert(!cell->getParam(ID::TRG_ENABLE).as_bool() || (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)); - if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async $print cell - f << indent << "auto " << mangle(cell) << "_curr = "; + if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async effectful cell + f << indent << "auto " << mangle(cell) << "_next = "; dump_sigspec_rhs(cell->getPort(ID::EN)); f << ".concat("; - dump_sigspec_rhs(cell->getPort(ID::ARGS)); + if (cell->type == ID($print)) + dump_sigspec_rhs(cell->getPort(ID::ARGS)); + else if (cell->type == ID($check)) + dump_sigspec_rhs(cell->getPort(ID::A)); + else log_assert(false); f << ").val();\n"; - f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_curr) {\n"; + f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_next) {\n"; inc_indent(); - dump_print(cell); - f << indent << mangle(cell) << " = " << mangle(cell) << "_curr;\n"; + dump_effect(cell); + f << indent << mangle(cell) << " = " << mangle(cell) << "_next;\n"; dec_indent(); f << indent << "}\n"; - } else { // initial $print cell + } else { // initial effectful cell f << indent << "if (!" << mangle(cell) << ") {\n"; inc_indent(); - dump_print(cell); + dump_effect(cell); f << indent << mangle(cell) << " = value<1>{1u};\n"; dec_indent(); f << indent << "}\n"; @@ -1728,6 +1777,47 @@ struct CxxrtlWorker { } } + void dump_cell_effect_sync(std::vector &cells) + { + log_assert(!cells.empty()); + const auto &trg = cells[0]->getPort(ID::TRG); + const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY); + + f << indent << "if ("; + for (int i = 0; i < trg.size(); i++) { + RTLIL::SigBit trg_bit = trg[i]; + trg_bit = sigmaps[trg_bit.wire->module](trg_bit); + log_assert(trg_bit.wire); + + if (i != 0) + f << " || "; + + if (trg_polarity[i] == State::S1) + f << "posedge_"; + else + f << "negedge_"; + f << mangle(trg_bit); + } + f << ") {\n"; + inc_indent(); + std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) { + return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int(); + }); + for (auto cell : cells) { + log_assert(cell->getParam(ID::TRG_ENABLE).as_bool()); + log_assert(cell->getPort(ID::TRG) == trg); + log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity); + + std::vector inlined_cells; + collect_cell_eval(cell, /*for_debug=*/false, inlined_cells); + dump_inlined_cells(inlined_cells); + dump_effect(cell); + } + dec_indent(); + + f << indent << "}\n"; + } + void dump_mem_rdport(const Mem *mem, int portidx, bool for_debug = false) { auto &port = mem->rd_ports[portidx]; @@ -2047,11 +2137,10 @@ struct CxxrtlWorker { } } for (auto cell : module->cells()) { - // Certain $print cells have additional state, which must be reset as well. - if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool()) - f << indent << mangle(cell) << " = value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << ">();\n"; - if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0) - f << indent << mangle(cell) << " = value<1>();\n"; + // Async and initial effectful cells have additional state, which must be reset as well. + if (is_effectful_cell(cell->type)) + if (!cell->getParam(ID::TRG_ENABLE).as_bool() || cell->getParam(ID::TRG_WIDTH).as_int() == 0) + f << indent << mangle(cell) << " = {};\n"; if (is_internal_cell(cell->type)) continue; f << indent << mangle(cell); @@ -2099,8 +2188,8 @@ struct CxxrtlWorker { case FlowGraph::Node::Type::CELL_EVAL: dump_cell_eval(node.cell); break; - case FlowGraph::Node::Type::PRINT_SYNC: - dump_sync_print(node.print_sync_cells); + case FlowGraph::Node::Type::EFFECT_SYNC: + dump_cell_effect_sync(node.cells); break; case FlowGraph::Node::Type::PROCESS_CASE: dump_process_case(node.process); @@ -2481,11 +2570,15 @@ struct CxxrtlWorker { f << "\n"; bool has_cells = false; for (auto cell : module->cells()) { - // Certain $print cells have additional state, which requires storage. - if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool()) - f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n"; - if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0) - f << indent << "value<1> " << mangle(cell) << ";\n"; + // Async and initial effectful cells have additional state, which requires storage. + if (is_effectful_cell(cell->type)) { + if (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0) + f << indent << "value<1> " << mangle(cell) << ";\n"; // async initial cell + if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($print)) + f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n"; // {EN, ARGS} + if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($check)) + f << indent << "value<2> " << mangle(cell) << ";\n"; // {EN, A} + } if (is_internal_cell(cell->type)) continue; dump_attrs(cell); @@ -2803,8 +2896,8 @@ struct CxxrtlWorker { cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn); } - // $print cells may be triggered on posedge/negedge events. - if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) { + // Effectful cells may be triggered on posedge/negedge events. + if (is_effectful_cell(cell->type) && cell->getParam(ID::TRG_ENABLE).as_bool()) { for (size_t i = 0; i < (size_t)cell->getParam(ID::TRG_WIDTH).as_int(); i++) { RTLIL::SigBit trg = cell->getPort(ID::TRG).extract(i, 1); if (is_valid_clock(trg)) @@ -2945,10 +3038,12 @@ struct CxxrtlWorker { // Discover nodes reachable from primary outputs (i.e. members) and collect reachable wire users. pool worklist; for (auto node : flow.nodes) { - if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type)) - worklist.insert(node); // node has effects - else if (node->type == FlowGraph::Node::Type::PRINT_SYNC) - worklist.insert(node); // node is sync $print + if (node->type == FlowGraph::Node::Type::CELL_EVAL && !is_internal_cell(node->cell->type)) + worklist.insert(node); // node evaluates a submodule + else if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type)) + worklist.insert(node); // node has async effects + else if (node->type == FlowGraph::Node::Type::EFFECT_SYNC) + worklist.insert(node); // node has sync effects else if (node->type == FlowGraph::Node::Type::MEM_WRPORTS) worklist.insert(node); // node is memory write else if (node->type == FlowGraph::Node::Type::PROCESS_SYNC && is_memwr_process(node->process)) @@ -3005,21 +3100,21 @@ struct CxxrtlWorker { } // Emit reachable nodes in eval(). - // Accumulate sync $print cells per trigger condition. - dict, std::vector> sync_print_cells; + // Accumulate sync effectful cells per trigger condition. + dict, std::vector> effect_sync_cells; for (auto node : node_order) if (live_nodes[node]) { if (node->type == FlowGraph::Node::Type::CELL_EVAL && - node->cell->type == ID($print) && + is_effectful_cell(node->cell->type) && node->cell->getParam(ID::TRG_ENABLE).as_bool() && node->cell->getParam(ID::TRG_WIDTH).as_int() != 0) - sync_print_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell); + effect_sync_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell); else schedule[module].push_back(*node); } - for (auto &it : sync_print_cells) { - auto node = flow.add_print_sync_node(it.second); + for (auto &it : effect_sync_cells) { + auto node = flow.add_effect_sync_node(it.second); schedule[module].push_back(*node); } diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h index 55057149721..ee55011e86d 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h @@ -952,7 +952,23 @@ struct lazy_fmt { virtual std::string operator() () const = 0; }; -// An object that can be passed to a `eval()` method in order to act on side effects. +// Flavor of a `$check` cell. +enum class flavor { + // Corresponds to a `$assert` cell in other flows, and a Verilog `assert ()` statement. + ASSERT, + // Corresponds to a `$assume` cell in other flows, and a Verilog `assume ()` statement. + ASSUME, + // Corresponds to a `$live` cell in other flows, and a Verilog `assert (eventually)` statement. + ASSERT_EVENTUALLY, + // Corresponds to a `$fair` cell in other flows, and a Verilog `assume (eventually)` statement. + ASSUME_EVENTUALLY, + // Corresponds to a `$cover` cell in other flows, and a Verilog `cover ()` statement. + COVER, +}; + +// An object that can be passed to a `eval()` method in order to act on side effects. The default behavior implemented +// below is the same as the behavior of `eval(nullptr)`, except that `-print-output` option of `write_cxxrtl` is not +// taken into account. struct performer { // Called by generated formatting code to evaluate a Verilog `$time` expression. virtual int64_t vlog_time() const { return 0; } @@ -964,6 +980,15 @@ struct performer { virtual void on_print(const lazy_fmt &formatter, const metadata_map &attributes) { std::cout << formatter(); } + + // Called when a `$check` cell is triggered. + virtual void on_check(flavor type, bool condition, const lazy_fmt &formatter, const metadata_map &attributes) { + if (type == flavor::ASSERT || type == flavor::ASSUME) { + if (!condition) + std::cerr << formatter(); + CXXRTL_ASSERT(condition && "Check failed"); + } + } }; // An object that can be passed to a `commit()` method in order to produce a replay log of every state change in diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 41e51f3289b..988eef6588f 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -1008,7 +1008,7 @@ void dump_cell_expr_binop(std::ostream &f, std::string indent, RTLIL::Cell *cell void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell *cell) { - Fmt fmt = {}; + Fmt fmt; fmt.parse_rtlil(cell); std::vector args = fmt.emit_verilog(); @@ -1041,6 +1041,23 @@ void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell f << stringf(");\n"); } +void dump_cell_expr_check(std::ostream &f, std::string indent, const RTLIL::Cell *cell) +{ + std::string flavor = cell->getParam(ID(FLAVOR)).decode_string(); + if (flavor == "assert") + f << stringf("%s" "assert (", indent.c_str()); + else if (flavor == "assume") + f << stringf("%s" "assume (", indent.c_str()); + else if (flavor == "live") + f << stringf("%s" "assert (eventually ", indent.c_str()); + else if (flavor == "fair") + f << stringf("%s" "assume (eventually ", indent.c_str()); + else if (flavor == "cover") + f << stringf("%s" "cover (", indent.c_str()); + dump_sigspec(f, cell->getPort(ID::A)); + f << stringf(");\n"); +} + bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) { if (cell->type == ID($_NOT_)) { @@ -1814,6 +1831,39 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } + if (cell->type == ID($check)) + { + // Sync $check cells are accumulated and handled in dump_module. + if (cell->getParam(ID::TRG_ENABLE).as_bool()) + return true; + + f << stringf("%s" "always @*\n", indent.c_str()); + + f << stringf("%s" " if (", indent.c_str()); + dump_sigspec(f, cell->getPort(ID::EN)); + f << stringf(") begin\n"); + + std::string flavor = cell->getParam(ID::FLAVOR).decode_string(); + if (flavor == "assert" || flavor == "assume") { + Fmt fmt; + fmt.parse_rtlil(cell); + if (!fmt.parts.empty()) { + f << stringf("%s" " if (!", indent.c_str()); + dump_sigspec(f, cell->getPort(ID::A)); + f << stringf(")\n"); + dump_cell_expr_print(f, indent + " ", cell); + } + } else { + f << stringf("%s" " /* message omitted */\n", indent.c_str()); + } + + dump_cell_expr_check(f, indent + " ", cell); + + f << stringf("%s" " end\n", indent.c_str()); + + return true; + } + // FIXME: $fsm return false; @@ -1903,7 +1953,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell) } } -void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec &trg, const RTLIL::Const &polarity, std::vector &cells) +void dump_sync_effect(std::ostream &f, std::string indent, const RTLIL::SigSpec &trg, const RTLIL::Const &polarity, std::vector &cells) { if (trg.size() == 0) { f << stringf("%s" "initial begin\n", indent.c_str()); @@ -1927,9 +1977,29 @@ void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec & for (auto cell : cells) { f << stringf("%s" " if (", indent.c_str()); dump_sigspec(f, cell->getPort(ID::EN)); - f << stringf(")\n"); + f << stringf(") begin\n"); + + if (cell->type == ID($print)) { + dump_cell_expr_print(f, indent + " ", cell); + } else if (cell->type == ID($check)) { + std::string flavor = cell->getParam(ID::FLAVOR).decode_string(); + if (flavor == "assert" || flavor == "assume") { + Fmt fmt; + fmt.parse_rtlil(cell); + if (!fmt.parts.empty()) { + f << stringf("%s" " if (!", indent.c_str()); + dump_sigspec(f, cell->getPort(ID::A)); + f << stringf(")\n"); + dump_cell_expr_print(f, indent + " ", cell); + } + } else { + f << stringf("%s" " /* message omitted */\n", indent.c_str()); + } - dump_cell_expr_print(f, indent + " ", cell); + dump_cell_expr_check(f, indent + " ", cell); + } + + f << stringf("%s" " end\n", indent.c_str()); } f << stringf("%s" "end\n", indent.c_str()); @@ -2182,7 +2252,7 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) { - std::map, std::vector> sync_print_cells; + std::map, std::vector> sync_effect_cells; reg_wires.clear(); reset_auto_counter(module); @@ -2214,8 +2284,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) std::set> reg_bits; for (auto cell : module->cells()) { - if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) { - sync_print_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell); + if (cell->type.in(ID($print), ID($check)) && cell->getParam(ID::TRG_ENABLE).as_bool()) { + sync_effect_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell); continue; } @@ -2274,8 +2344,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) for (auto cell : module->cells()) dump_cell(f, indent + " ", cell); - for (auto &it : sync_print_cells) - dump_sync_print(f, indent + " ", it.first.first, it.first.second, it.second); + for (auto &it : sync_effect_cells) + dump_sync_effect(f, indent + " ", it.first.first, it.first.second, it.second); for (auto it = module->processes.begin(); it != module->processes.end(); ++it) dump_process(f, indent + " ", it->second); diff --git a/docs/source/CHAPTER_CellLib.rst b/docs/source/CHAPTER_CellLib.rst index 0f0d791235c..3b6f1b4d387 100644 --- a/docs/source/CHAPTER_CellLib.rst +++ b/docs/source/CHAPTER_CellLib.rst @@ -621,7 +621,7 @@ Add information about ``$specify2``, ``$specify3``, and ``$specrule`` cells. Formal verification cells ~~~~~~~~~~~~~~~~~~~~~~~~~ -Add information about ``$assert``, ``$assume``, ``$live``, ``$fair``, +Add information about ``$check``, ``$assert``, ``$assume``, ``$live``, ``$fair``, ``$cover``, ``$equiv``, ``$initstate``, ``$anyconst``, ``$anyseq``, ``$anyinit``, ``$allconst``, ``$allseq`` cells. @@ -654,8 +654,8 @@ If ``\TRG_ENABLE`` is true, the following parameters also apply: negative-edge triggered. ``\PRIORITY`` - When multiple ``$print`` cells fire on the same trigger, they execute in - descending priority order. + When multiple ``$print`` or ``$$check`` cells fire on the same trigger, they\ + execute in descending priority order. Ports: diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 0a502162e8d..03697ebf314 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -163,6 +163,28 @@ static RTLIL::SigSpec mux2rtlil(AstNode *that, const RTLIL::SigSpec &cond, const return wire; } +static void check_unique_id(RTLIL::Module *module, RTLIL::IdString id, + const AstNode *node, const char *to_add_kind) +{ + auto already_exists = [&](const RTLIL::AttrObject *existing, const char *existing_kind) { + std::string src = existing->get_string_attribute(ID::src); + std::string location_str = "earlier"; + if (!src.empty()) + location_str = "at " + src; + node->input_error("Cannot add %s `%s' because a %s with the same name was already created %s!\n", + to_add_kind, id.c_str(), existing_kind, location_str.c_str()); + }; + + if (const RTLIL::Wire *wire = module->wire(id)) + already_exists(wire, "signal"); + if (const RTLIL::Cell *cell = module->cell(id)) + already_exists(cell, "cell"); + if (module->processes.count(id)) + already_exists(module->processes.at(id), "process"); + if (module->memories.count(id)) + already_exists(module->memories.at(id), "memory"); +} + // helper class for rewriting simple lookahead references in AST always blocks struct AST_INTERNAL::LookaheadRewriter { @@ -316,10 +338,10 @@ struct AST_INTERNAL::ProcessGenerator // Buffer for generating the init action RTLIL::SigSpec init_lvalue, init_rvalue; - // The most recently assigned $print cell \PRIORITY. - int last_print_priority; + // The most recently assigned $print or $check cell \PRIORITY. + int last_effect_priority; - ProcessGenerator(AstNode *always, RTLIL::SigSpec initSyncSignalsArg = RTLIL::SigSpec()) : always(always), initSyncSignals(initSyncSignalsArg), last_print_priority(0) + ProcessGenerator(AstNode *always, RTLIL::SigSpec initSyncSignalsArg = RTLIL::SigSpec()) : always(always), initSyncSignals(initSyncSignalsArg), last_effect_priority(0) { // rewrite lookahead references LookaheadRewriter la_rewriter(always); @@ -703,8 +725,10 @@ struct AST_INTERNAL::ProcessGenerator std::stringstream sstr; sstr << ast->str << "$" << ast->filename << ":" << ast->location.first_line << "$" << (autoidx++); - RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print)); - set_src_attr(cell, ast); + Wire *en = current_module->addWire(sstr.str() + "_EN", 1); + set_src_attr(en, ast); + proc->root_case.actions.push_back(SigSig(en, false)); + current_case->actions.push_back(SigSig(en, true)); RTLIL::SigSpec triggers; RTLIL::Const polarity; @@ -717,18 +741,15 @@ struct AST_INTERNAL::ProcessGenerator polarity.bits.push_back(RTLIL::S0); } } - cell->parameters[ID::TRG_WIDTH] = triggers.size(); - cell->parameters[ID::TRG_ENABLE] = (always->type == AST_INITIAL) || !triggers.empty(); - cell->parameters[ID::TRG_POLARITY] = polarity; - cell->parameters[ID::PRIORITY] = --last_print_priority; - cell->setPort(ID::TRG, triggers); - - Wire *wire = current_module->addWire(sstr.str() + "_EN", 1); - set_src_attr(wire, ast); - cell->setPort(ID::EN, wire); - proc->root_case.actions.push_back(SigSig(wire, false)); - current_case->actions.push_back(SigSig(wire, true)); + RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print)); + set_src_attr(cell, ast); + cell->setParam(ID::TRG_WIDTH, triggers.size()); + cell->setParam(ID::TRG_ENABLE, (always->type == AST_INITIAL) || !triggers.empty()); + cell->setParam(ID::TRG_POLARITY, polarity); + cell->setParam(ID::PRIORITY, --last_effect_priority); + cell->setPort(ID::TRG, triggers); + cell->setPort(ID::EN, en); int default_base = 10; if (ast->str.back() == 'b') @@ -766,7 +787,7 @@ struct AST_INTERNAL::ProcessGenerator args.push_back(arg); } - Fmt fmt = {}; + Fmt fmt; fmt.parse_verilog(args, /*sformat_like=*/false, default_base, /*task_name=*/ast->str, current_module->name); if (ast->str.substr(0, 8) == "$display") fmt.append_string("\n"); @@ -776,6 +797,70 @@ struct AST_INTERNAL::ProcessGenerator } break; + // generate $check cells + case AST_ASSERT: + case AST_ASSUME: + case AST_LIVE: + case AST_FAIR: + case AST_COVER: + { + std::string flavor, desc; + if (ast->type == AST_ASSERT) { flavor = "assert"; desc = "assert ()"; } + if (ast->type == AST_ASSUME) { flavor = "assume"; desc = "assume ()"; } + if (ast->type == AST_LIVE) { flavor = "live"; desc = "assert (eventually)"; } + if (ast->type == AST_FAIR) { flavor = "fair"; desc = "assume (eventually)"; } + if (ast->type == AST_COVER) { flavor = "cover"; desc = "cover ()"; } + + IdString cellname; + if (ast->str.empty()) + cellname = stringf("$%s$%s:%d$%d", flavor.c_str(), RTLIL::encode_filename(ast->filename).c_str(), ast->location.first_line, autoidx++); + else + cellname = ast->str; + check_unique_id(current_module, cellname, ast, "procedural assertion"); + + RTLIL::SigSpec check = ast->children[0]->genWidthRTLIL(-1, false, &subst_rvalue_map.stdmap()); + if (GetSize(check) != 1) + check = current_module->ReduceBool(NEW_ID, check); + + Wire *en = current_module->addWire(cellname.str() + "_EN", 1); + set_src_attr(en, ast); + proc->root_case.actions.push_back(SigSig(en, false)); + current_case->actions.push_back(SigSig(en, true)); + + RTLIL::SigSpec triggers; + RTLIL::Const polarity; + for (auto sync : proc->syncs) { + if (sync->type == RTLIL::STp) { + triggers.append(sync->signal); + polarity.bits.push_back(RTLIL::S1); + } else if (sync->type == RTLIL::STn) { + triggers.append(sync->signal); + polarity.bits.push_back(RTLIL::S0); + } + } + + RTLIL::Cell *cell = current_module->addCell(cellname, ID($check)); + set_src_attr(cell, ast); + for (auto &attr : ast->attributes) { + if (attr.second->type != AST_CONSTANT) + log_file_error(ast->filename, ast->location.first_line, "Attribute `%s' with non-constant value!\n", attr.first.c_str()); + cell->attributes[attr.first] = attr.second->asAttrConst(); + } + cell->setParam(ID::FLAVOR, flavor); + cell->setParam(ID::TRG_WIDTH, triggers.size()); + cell->setParam(ID::TRG_ENABLE, (always->type == AST_INITIAL) || !triggers.empty()); + cell->setParam(ID::TRG_POLARITY, polarity); + cell->setParam(ID::PRIORITY, --last_effect_priority); + cell->setPort(ID::TRG, triggers); + cell->setPort(ID::EN, en); + cell->setPort(ID::A, check); + + // No message is emitted to ensure Verilog code roundtrips correctly. + Fmt fmt; + fmt.emit_rtlil(cell); + break; + } + case AST_NONE: case AST_FOR: break; @@ -1242,28 +1327,6 @@ void AstNode::detectSignWidth(int &width_hint, bool &sign_hint, bool *found_real width_hint, kWidthLimit); } -static void check_unique_id(RTLIL::Module *module, RTLIL::IdString id, - const AstNode *node, const char *to_add_kind) -{ - auto already_exists = [&](const RTLIL::AttrObject *existing, const char *existing_kind) { - std::string src = existing->get_string_attribute(ID::src); - std::string location_str = "earlier"; - if (!src.empty()) - location_str = "at " + src; - node->input_error("Cannot add %s `%s' because a %s with the same name was already created %s!\n", - to_add_kind, id.c_str(), existing_kind, location_str.c_str()); - }; - - if (const RTLIL::Wire *wire = module->wire(id)) - already_exists(wire, "signal"); - if (const RTLIL::Cell *cell = module->cell(id)) - already_exists(cell, "cell"); - if (module->processes.count(id)) - already_exists(module->processes.at(id), "process"); - if (module->memories.count(id)) - already_exists(module->memories.at(id), "memory"); -} - // create RTLIL from an AST node // all generated cells, wires and processes are added to the module pointed to by 'current_module' // when the AST node is an expression (AST_ADD, AST_BIT_XOR, etc.), the result signal is returned. @@ -1945,48 +2008,50 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) } break; - // generate $assert cells + // generate $check cells case AST_ASSERT: case AST_ASSUME: case AST_LIVE: case AST_FAIR: case AST_COVER: { - IdString celltype; - if (type == AST_ASSERT) celltype = ID($assert); - if (type == AST_ASSUME) celltype = ID($assume); - if (type == AST_LIVE) celltype = ID($live); - if (type == AST_FAIR) celltype = ID($fair); - if (type == AST_COVER) celltype = ID($cover); - - log_assert(children.size() == 2); - - RTLIL::SigSpec check = children[0]->genRTLIL(); - if (GetSize(check) != 1) - check = current_module->ReduceBool(NEW_ID, check); - - RTLIL::SigSpec en = children[1]->genRTLIL(); - if (GetSize(en) != 1) - en = current_module->ReduceBool(NEW_ID, en); + std::string flavor, desc; + if (type == AST_ASSERT) { flavor = "assert"; desc = "assert property ()"; } + if (type == AST_ASSUME) { flavor = "assume"; desc = "assume property ()"; } + if (type == AST_LIVE) { flavor = "live"; desc = "assert property (eventually)"; } + if (type == AST_FAIR) { flavor = "fair"; desc = "assume property (eventually)"; } + if (type == AST_COVER) { flavor = "cover"; desc = "cover property ()"; } IdString cellname; if (str.empty()) - cellname = stringf("%s$%s:%d$%d", celltype.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line, autoidx++); + cellname = stringf("$%s$%s:%d$%d", flavor.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line, autoidx++); else cellname = str; - check_unique_id(current_module, cellname, this, "procedural assertion"); - RTLIL::Cell *cell = current_module->addCell(cellname, celltype); - set_src_attr(cell, this); + RTLIL::SigSpec check = children[0]->genRTLIL(); + if (GetSize(check) != 1) + check = current_module->ReduceBool(NEW_ID, check); + + RTLIL::Cell *cell = current_module->addCell(cellname, ID($check)); + set_src_attr(cell, this); for (auto &attr : attributes) { if (attr.second->type != AST_CONSTANT) input_error("Attribute `%s' with non-constant value!\n", attr.first.c_str()); cell->attributes[attr.first] = attr.second->asAttrConst(); } - + cell->setParam(ID(FLAVOR), flavor); + cell->parameters[ID::TRG_WIDTH] = 0; + cell->parameters[ID::TRG_ENABLE] = 0; + cell->parameters[ID::TRG_POLARITY] = 0; + cell->parameters[ID::PRIORITY] = 0; + cell->setPort(ID::TRG, RTLIL::SigSpec()); + cell->setPort(ID::EN, RTLIL::S1); cell->setPort(ID::A, check); - cell->setPort(ID::EN, en); + + // No message is emitted to ensure Verilog code roundtrips correctly. + Fmt fmt; + fmt.emit_rtlil(cell); } break; diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index fa079f3e365..8e0de299470 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -178,7 +178,7 @@ Fmt AstNode::processFormat(int stage, bool sformat_like, int default_base, size_ args.push_back(arg); } - Fmt fmt = {}; + Fmt fmt; fmt.parse_verilog(args, sformat_like, default_base, /*task_name=*/str, current_module->name); return fmt; } @@ -784,7 +784,7 @@ AstNode *AstNode::clone_at_zero() pointee->type != AST_MEMORY) break; - YS_FALLTHROUGH; + YS_FALLTHROUGH case AST_MEMRD: detectSignWidth(width_hint, sign_hint); return mkconst_int(0, sign_hint, width_hint); @@ -3039,97 +3039,6 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin } skip_dynamic_range_lvalue_expansion:; - if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_LIVE || type == AST_FAIR || type == AST_COVER) && current_block != NULL) - { - std::stringstream sstr; - sstr << "$formal$" << RTLIL::encode_filename(filename) << ":" << location.first_line << "$" << (autoidx++); - std::string id_check = sstr.str() + "_CHECK", id_en = sstr.str() + "_EN"; - - AstNode *wire_check = new AstNode(AST_WIRE); - wire_check->str = id_check; - wire_check->was_checked = true; - current_ast_mod->children.push_back(wire_check); - current_scope[wire_check->str] = wire_check; - while (wire_check->simplify(true, 1, -1, false)) { } - - AstNode *wire_en = new AstNode(AST_WIRE); - wire_en->str = id_en; - wire_en->was_checked = true; - current_ast_mod->children.push_back(wire_en); - if (current_always_clocked) { - current_ast_mod->children.push_back(new AstNode(AST_INITIAL, new AstNode(AST_BLOCK, new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), AstNode::mkconst_int(0, false, 1))))); - current_ast_mod->children.back()->children[0]->children[0]->children[0]->str = id_en; - current_ast_mod->children.back()->children[0]->children[0]->children[0]->was_checked = true; - } - current_scope[wire_en->str] = wire_en; - while (wire_en->simplify(true, 1, -1, false)) { } - - AstNode *check_defval; - if (type == AST_LIVE || type == AST_FAIR) { - check_defval = new AstNode(AST_REDUCE_BOOL, children[0]->clone()); - } else { - std::vector x_bit; - x_bit.push_back(RTLIL::State::Sx); - check_defval = mkconst_bits(x_bit, false); - } - - AstNode *assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), check_defval); - assign_check->children[0]->str = id_check; - assign_check->children[0]->was_checked = true; - - AstNode *assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(0, false, 1)); - assign_en->children[0]->str = id_en; - assign_en->children[0]->was_checked = true; - - AstNode *default_signals = new AstNode(AST_BLOCK); - default_signals->children.push_back(assign_check); - default_signals->children.push_back(assign_en); - current_top_block->children.insert(current_top_block->children.begin(), default_signals); - - if (type == AST_LIVE || type == AST_FAIR) { - assign_check = nullptr; - } else { - assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_REDUCE_BOOL, children[0]->clone())); - assign_check->children[0]->str = id_check; - assign_check->children[0]->was_checked = true; - assign_check->fixup_hierarchy_flags(); - } - - if (current_always == nullptr || current_always->type != AST_INITIAL) { - assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1)); - } else { - assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_FCALL)); - assign_en->children[1]->str = "\\$initstate"; - } - assign_en->children[0]->str = id_en; - assign_en->children[0]->was_checked = true; - assign_en->fixup_hierarchy_flags(); - - newNode = new AstNode(AST_BLOCK); - if (assign_check != nullptr) - newNode->children.push_back(assign_check); - newNode->children.push_back(assign_en); - - AstNode *assertnode = new AstNode(type); - assertnode->location = location; - assertnode->str = str; - assertnode->children.push_back(new AstNode(AST_IDENTIFIER)); - assertnode->children.push_back(new AstNode(AST_IDENTIFIER)); - assertnode->children[0]->str = id_check; - assertnode->children[1]->str = id_en; - assertnode->attributes.swap(attributes); - current_ast_mod->children.push_back(assertnode); - - goto apply_newNode; - } - - if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_LIVE || type == AST_FAIR || type == AST_COVER) && children.size() == 1) - { - children.push_back(mkconst_int(1, false, 1)); - fixup_hierarchy_flags(); - did_something = true; - } - // found right-hand side identifier for memory -> replace with memory read port if (stage > 1 && type == AST_IDENTIFIER && id2ast != NULL && id2ast->type == AST_MEMORY && !in_lvalue && children.size() == 1 && children[0]->type == AST_RANGE && children[0]->children.size() == 1) { diff --git a/kernel/celltypes.h b/kernel/celltypes.h index cad505d9afd..77cb3e324c2 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -102,6 +102,7 @@ struct CellTypes setup_type(ID($specify3), {ID::EN, ID::SRC, ID::DST, ID::DAT}, pool(), true); setup_type(ID($specrule), {ID::EN_SRC, ID::EN_DST, ID::SRC, ID::DST}, pool(), true); setup_type(ID($print), {ID::EN, ID::ARGS, ID::TRG}, pool()); + setup_type(ID($check), {ID::A, ID::EN, ID::ARGS, ID::TRG}, pool()); setup_type(ID($set_tag), {ID::A, ID::SET, ID::CLR}, {ID::Y}); setup_type(ID($get_tag), {ID::A}, {ID::Y}); setup_type(ID($overwrite_tag), {ID::A, ID::SET, ID::CLR}, pool()); diff --git a/kernel/constids.inc b/kernel/constids.inc index 480e2afc6fa..7db21debb0e 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -88,6 +88,7 @@ X(equiv_merged) X(equiv_region) X(extract_order) X(F) +X(FLAVOR) X(FORMAT) X(force_downto) X(force_upto) diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index f19da69e284..125730f2924 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1068,6 +1068,12 @@ namespace { error(__LINE__); } + std::string param_string(const RTLIL::IdString &name) + { + param(name); + return cell->parameters.at(name).decode_string(); + } + void port(const RTLIL::IdString& name, int width) { auto it = cell->connections_.find(name); @@ -1747,6 +1753,22 @@ namespace { return; } + if (cell->type == ID($check)) { + std::string flavor = param_string(ID(FLAVOR)); + if (!(flavor == "assert" || flavor == "assume" || flavor == "live" || flavor == "fair" || flavor == "cover")) + error(__LINE__); + param(ID(FORMAT)); + param_bool(ID::TRG_ENABLE); + param(ID::TRG_POLARITY); + param(ID::PRIORITY); + port(ID::A, 1); + port(ID::EN, 1); + port(ID::TRG, param(ID::TRG_WIDTH)); + port(ID::ARGS, param(ID::ARGS_WIDTH)); + check_expected(); + return; + } + if (cell->type == ID($_BUF_)) { port(ID::A,1); port(ID::Y,1); check_expected(); return; } if (cell->type == ID($_NOT_)) { port(ID::A,1); port(ID::Y,1); check_expected(); return; } if (cell->type == ID($_AND_)) { port(ID::A,1); port(ID::B,1); port(ID::Y,1); check_expected(); return; } diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index 69cc6fb914d..90f890e8075 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -671,7 +671,7 @@ bool set_keep_assert(std::map &cache, RTLIL::Module *mod) if (cache.count(mod) == 0) for (auto c : mod->cells()) { RTLIL::Module *m = mod->design->module(c->type); - if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) + if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) return cache[mod] = true; } return cache[mod]; diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index a219e470813..ffb3052db64 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -82,7 +82,7 @@ struct keep_cache_t if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule))) return true; - if (cell->type == ID($print)) + if (cell->type == ID($print) || cell->type == ID($check)) return true; if (cell->has_keep_attr()) diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index fd804786fd8..930d2000b4d 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1803,14 +1803,36 @@ endmodule module \$print (EN, TRG, ARGS); +parameter PRIORITY = 0; + parameter FORMAT = ""; parameter ARGS_WIDTH = 0; -parameter PRIORITY = 0; + parameter TRG_ENABLE = 1; +parameter TRG_WIDTH = 0; +parameter TRG_POLARITY = 0; +input EN; +input [TRG_WIDTH-1:0] TRG; +input [ARGS_WIDTH-1:0] ARGS; + +endmodule + +// -------------------------------------------------------- + +module \$check (A, EN, TRG, ARGS); + +parameter FLAVOR = ""; +parameter PRIORITY = 0; + +parameter FORMAT = ""; +parameter ARGS_WIDTH = 0; + +parameter TRG_ENABLE = 1; parameter TRG_WIDTH = 0; parameter TRG_POLARITY = 0; +input A; input EN; input [TRG_WIDTH-1:0] TRG; input [ARGS_WIDTH-1:0] ARGS; From ffb82df33cb47d005241b5e28d7f69ccb8bc4f93 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 1 Feb 2024 20:08:55 +0100 Subject: [PATCH 6/6] Additional tests for FV $check compatibility --- tests/various/chformal_check.ys | 68 ++++++++++++++++++++++ tests/various/chformal_coverenable.ys | 41 ++++++++++++-- tests/various/clk2fflogic_effects.sh | 27 +++++++++ tests/various/clk2fflogic_effects.sv | 82 +++++++++++++++++++++++++++ 4 files changed, 214 insertions(+), 4 deletions(-) create mode 100644 tests/various/chformal_check.ys create mode 100755 tests/various/clk2fflogic_effects.sh create mode 100644 tests/various/clk2fflogic_effects.sv diff --git a/tests/various/chformal_check.ys b/tests/various/chformal_check.ys new file mode 100644 index 00000000000..951543fa5e5 --- /dev/null +++ b/tests/various/chformal_check.ys @@ -0,0 +1,68 @@ +read_verilog -formal < clk2fflogic_effects.iv.log + +sort clk2fflogic_effects.iv.log > clk2fflogic_effects.iv.sorted.log +tail +3 clk2fflogic_effects.sim.log | sort > clk2fflogic_effects.sim.sorted.log +tail +3 clk2fflogic_effects.clk2fflogic.log | sort > clk2fflogic_effects.clk2fflogic.sorted.log + +cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.sim.sorted.log +cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.clk2fflogic.sorted.log diff --git a/tests/various/clk2fflogic_effects.sv b/tests/various/clk2fflogic_effects.sv new file mode 100644 index 00000000000..b571cf3fe7d --- /dev/null +++ b/tests/various/clk2fflogic_effects.sv @@ -0,0 +1,82 @@ +module top; + +(* gclk *) +reg gclk; + +reg clk = 0; +always @(posedge gclk) + clk <= !clk; + +reg [4:0] counter = 0; + +reg eff_0_trg = '0; +reg eff_0_en = '0; + +reg eff_1_trgA = '0; +reg eff_1_trgB = '0; +reg eff_1_en = '0; + +reg eff_2_trgA = '0; +reg eff_2_trgB = '0; +reg eff_2_en = '0; + +`ifdef FAST +always @(posedge gclk) begin +`else +always @(posedge clk) begin +`endif + counter <= counter + 1; + + eff_0_trg = 32'b00000000000000110011001100101010 >> counter; + eff_0_en <= 32'b00000000000001100000110110110110 >> counter; + + eff_1_trgA = 32'b00000000000000000011110000011110 >> counter; + eff_1_trgB = 32'b00000000000000001111000001111000 >> counter; + eff_1_en <= 32'b00000000000000001010101010101010 >> counter; + + eff_2_trgA = counter[0]; + eff_2_trgB = !counter[0]; + eff_2_en <= 32'b00000000000000000000001111111100 >> counter; +end + +always @(posedge eff_0_trg) + if (eff_0_en) + $display("%02d: eff0 +", counter); + +always @(negedge eff_0_trg) + if (eff_0_en) + $display("%02d: eff0 -", counter); + +always @(posedge eff_0_trg, negedge eff_0_trg) + if (eff_0_en) + $display("%02d: eff0 *", counter); + +always @(posedge eff_1_trgA, posedge eff_1_trgB) + if (eff_1_en) + $display("%02d: eff1 ++", counter); + +always @(posedge eff_1_trgA, negedge eff_1_trgB) + if (eff_1_en) + $display("%02d: eff1 +-", counter); + +always @(negedge eff_1_trgA, posedge eff_1_trgB) + if (eff_1_en) + $display("%02d: eff1 -+", counter); + +always @(negedge eff_1_trgA, negedge eff_1_trgB) + if (eff_1_en) + $display("%02d: eff1 --", counter); + +always @(posedge eff_2_trgA, posedge eff_2_trgB) + if (eff_2_en) + $display("repeated"); + +`ifdef __ICARUS__ +initial gclk = 0; +always @(gclk) gclk <= #5 !gclk; +always @(posedge gclk) + if (counter == 31) + $finish(0); +`endif + +endmodule