verific: Improve logic generated for SVA value change expressions

The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

	a) provides the expected behavior in a 2-valued logic setting, not
	   depending on any dont-care optimizations, and

	b) properly handles 'x values in yosys simulation

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index d19d837ffcca33316b8271ffb1d664c32ad06f36..145a5acf2dd0c66fd50bc87137d454e5b18bc3d3 100644 (file)
--- 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 cc254049ab4c2973ccb592a49c4f453a76270c88..b1965c97d3a70e06df64f2ead01673b4f273f862 100644 (file)
--- 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 1b217f746e55c2eb9cabd209e35cb232f7a4120b..dcabcf42ba463eb33cadabb11e83b0d3b349b2c6 100644 (file)
--- 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 8ed7f8cbc79999af59dbcbbce50ea8f11cab8775..2ecc9780c5de124d9f9f542f7d02c4f63bbaf474 100644 (file)
--- 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 (file)
index 0000000..8f3a05a
--- /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 (file)
index 0000000..d1c5290
--- /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 (file)
index 0000000..80ff309
--- /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 (file)
index 0000000..e004520
--- /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