diff options
-rw-r--r-- | frontends/verific/verific.cc | 35 | ||||
-rw-r--r-- | tests/sva/.gitignore | 1 | ||||
-rw-r--r-- | tests/sva/Makefile | 1 | ||||
-rw-r--r-- | tests/sva/runtest.sh | 4 | ||||
-rw-r--r-- | tests/sva/sva_value_change_changed.sv | 17 | ||||
-rw-r--r-- | tests/sva/sva_value_change_rose.sv | 20 | ||||
-rw-r--r-- | tests/sva/sva_value_change_sim.sv | 51 | ||||
-rw-r--r-- | tests/sva/sva_value_change_sim.ys | 3 |
8 files changed, 121 insertions, 11 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index d19d837ff..145a5acf2 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1557,17 +1557,25 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma SigSpec sig_d = net_map_at(inst->GetInput1()); SigSpec sig_o = net_map_at(inst->GetOutput()); - SigSpec sig_q = module->addWire(new_verific_id(inst)); + SigSpec sig_dx = module->addWire(new_verific_id(inst), 2); + SigSpec sig_qx = module->addWire(new_verific_id(inst), 2); if (verific_verbose) { + log(" NEX with A=%s, B=0, Y=%s.\n", + log_signal(sig_d), log_signal(sig_dx[0])); + log(" EQX with A=%s, B=1, Y=%s.\n", + log_signal(sig_d), log_signal(sig_dx[1])); log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); - log(" XNOR with A=%s, B=%s, Y=%s.\n", - log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); + log_signal(sig_dx), log_signal(sig_qx), log_signal(clocking.clock_sig)); + log(" EQ with A=%s, B=%s, Y=%s.\n", + log_signal(sig_dx), log_signal(sig_qx), log_signal(sig_o)); } - clocking.addDff(new_verific_id(inst), sig_d, sig_q); - module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o); + module->addNex(new_verific_id(inst), sig_d, State::S0, sig_dx[0]); + module->addEqx(new_verific_id(inst), sig_d, State::S1, sig_dx[1]); + + clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, Const(1, 2)); + module->addEq(new_verific_id(inst), sig_dx, sig_qx, sig_o); if (!mode_keep) continue; @@ -1601,13 +1609,20 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_o = net_map_at(inst->GetOutput()); SigBit sig_q = module->addWire(new_verific_id(inst)); + SigBit sig_d_no_x = module->addWire(new_verific_id(inst)); - if (verific_verbose) + if (verific_verbose) { + log(" EQX with A=%s, B=%d, Y=%s.\n", + log_signal(sig_d), inst->Type() == PRIM_SVA_ROSE, log_signal(sig_d_no_x)); log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", - log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); + log_signal(sig_d_no_x), log_signal(sig_q), log_signal(clocking.clock_sig)); + log(" EQ with A={%s, %s}, B={0, 1}, Y=%s.\n", + log_signal(sig_q), log_signal(sig_d_no_x), log_signal(sig_o)); + } - clocking.addDff(new_verific_id(inst), sig_d, sig_q); - module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o); + module->addEqx(new_verific_id(inst), sig_d, inst->Type() == PRIM_SVA_ROSE ? State::S1 : State::S0, sig_d_no_x); + clocking.addDff(new_verific_id(inst), sig_d_no_x, sig_q, State::S0); + module->addEq(new_verific_id(inst), {sig_q, sig_d_no_x}, Const(1, 2), sig_o); if (!mode_keep) continue; diff --git a/tests/sva/.gitignore b/tests/sva/.gitignore index cc254049a..b1965c97d 100644 --- a/tests/sva/.gitignore +++ b/tests/sva/.gitignore @@ -3,5 +3,6 @@ /*_pass /*_fail /*.ok +/*.fst /vhdlpsl[0-9][0-9] /vhdlpsl[0-9][0-9].sby diff --git a/tests/sva/Makefile b/tests/sva/Makefile index 1b217f746..dcabcf42b 100644 --- a/tests/sva/Makefile +++ b/tests/sva/Makefile @@ -10,4 +10,5 @@ clean: rm -rf $(addsuffix .ok,$(TESTS)) $(addsuffix .sby,$(TESTS)) $(TESTS) rm -rf $(addsuffix _pass.sby,$(TESTS)) $(addsuffix _pass,$(TESTS)) rm -rf $(addsuffix _fail.sby,$(TESTS)) $(addsuffix _fail,$(TESTS)) + rm -rf $(addsuffix .fst,$(TESTS)) diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 8ed7f8cbc..2ecc9780c 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -57,7 +57,9 @@ generate_sby() { fi } -if [ -f $prefix.sv ]; then +if [ -f $prefix.ys ]; then + $PWD/../../yosys -q -e "Assert .* failed." -s $prefix.ys +elif [ -f $prefix.sv ]; then generate_sby pass > ${prefix}_pass.sby generate_sby fail > ${prefix}_fail.sby sby --yosys $PWD/../../yosys -f ${prefix}_pass.sby diff --git a/tests/sva/sva_value_change_changed.sv b/tests/sva/sva_value_change_changed.sv new file mode 100644 index 000000000..8f3a05a2f --- /dev/null +++ b/tests/sva/sva_value_change_changed.sv @@ -0,0 +1,17 @@ +module top ( + input clk, + input a, b +); + default clocking @(posedge clk); endclocking + + assert property ( + $changed(b) + ); + +`ifndef FAIL + assume property ( + b !== 'x ##1 $changed(b) + ); +`endif + +endmodule diff --git a/tests/sva/sva_value_change_rose.sv b/tests/sva/sva_value_change_rose.sv new file mode 100644 index 000000000..d1c5290f1 --- /dev/null +++ b/tests/sva/sva_value_change_rose.sv @@ -0,0 +1,20 @@ +module top ( + input clk, + input a, b +); + default clocking @(posedge clk); endclocking + + wire a_copy; + assign a_copy = a; + + assert property ( + $rose(a) |-> b + ); + +`ifndef FAIL + assume property ( + $rose(a_copy) |-> b + ); +`endif + +endmodule diff --git a/tests/sva/sva_value_change_sim.sv b/tests/sva/sva_value_change_sim.sv new file mode 100644 index 000000000..80ff309cd --- /dev/null +++ b/tests/sva/sva_value_change_sim.sv @@ -0,0 +1,51 @@ +module top ( + input clk +); + +reg [7:0] counter = 0; + +reg a = 0; +reg b = 1; +reg c; + +wire a_fell; assign a_fell = $fell(a, @(posedge clk)); +wire a_rose; assign a_rose = $rose(a, @(posedge clk)); +wire a_stable; assign a_stable = $stable(a, @(posedge clk)); + +wire b_fell; assign b_fell = $fell(b, @(posedge clk)); +wire b_rose; assign b_rose = $rose(b, @(posedge clk)); +wire b_stable; assign b_stable = $stable(b, @(posedge clk)); + +wire c_fell; assign c_fell = $fell(c, @(posedge clk)); +wire c_rose; assign c_rose = $rose(c, @(posedge clk)); +wire c_stable; assign c_stable = $stable(c, @(posedge clk)); + +always @(posedge clk) begin + counter <= counter + 1; + + case (counter) + 0: begin + assert property ( $fell(a) && !$rose(a) && !$stable(a)); + assert property (!$fell(b) && $rose(b) && !$stable(b)); + assert property (!$fell(c) && !$rose(c) && $stable(c)); + a <= 1; b <= 1; c <= 1; + end + 1: begin a <= 0; b <= 1; c <= 'x; end + 2: begin + assert property ( $fell(a) && !$rose(a) && !$stable(a)); + assert property (!$fell(b) && !$rose(b) && $stable(b)); + assert property (!$fell(c) && !$rose(c) && !$stable(c)); + a <= 0; b <= 0; c <= 0; + end + 3: begin a <= 0; b <= 1; c <= 'x; end + 4: begin + assert property (!$fell(a) && !$rose(a) && $stable(a)); + assert property (!$fell(b) && $rose(b) && !$stable(b)); + assert property (!$fell(c) && !$rose(c) && !$stable(c)); + a <= 'x; b <= 'x; c <= 'x; + end + 5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end + endcase; +end + +endmodule diff --git a/tests/sva/sva_value_change_sim.ys b/tests/sva/sva_value_change_sim.ys new file mode 100644 index 000000000..e004520ce --- /dev/null +++ b/tests/sva/sva_value_change_sim.ys @@ -0,0 +1,3 @@ +read -sv sva_value_change_sim.sv +hierarchy -top top +sim -clock clk -fst sva_value_change_sim.fst |