verific: Use new value change logic also for $stable of wide signals.

I missed this in the previous PR.

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index fd8bbc3f12bfa30638a9ac632378cb65b1e8e65a..b130edbdc1dab8b971c1b140ef84eaedf139de2a 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1527,23 +1527,45 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 
                        log_assert(inst->Input1Size() == inst->OutputSize());
 
-                       SigSpec sig_d, sig_q, sig_o;
-                       sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
+                       unsigned width = inst->Input1Size();
 
-                       for (int i = int(inst->Input1Size())-1; i >= 0; i--){
+                       SigSpec sig_d, sig_dx, sig_qx, sig_o, sig_ox;
+                       sig_dx = module->addWire(new_verific_id(inst), width * 2);
+                       sig_qx = module->addWire(new_verific_id(inst), width * 2);
+                       sig_ox = module->addWire(new_verific_id(inst), width * 2);
+
+                       for (int i = int(width)-1; i >= 0; i--){
                                sig_d.append(net_map_at(inst->GetInput1Bit(i)));
                                sig_o.append(net_map_at(inst->GetOutputBit(i)));
                        }
 
                        if (verific_verbose) {
+                               for (unsigned i = 0; i < width; i++) {
+                                       log("    NEX with A=%s, B=0, Y=%s.\n",
+                                                       log_signal(sig_d[i]), log_signal(sig_dx[i]));
+                                       log("    EQX with A=%s, B=1, Y=%s.\n",
+                                                       log_signal(sig_d[i]), log_signal(sig_dx[i + width]));
+                               }
                                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_dx), log_signal(sig_qx), 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(sig_ox));
+                               log("    AND with A=%s, B=%s, Y=%s.\n",
+                                               log_signal(sig_ox.extract(0, width)), log_signal(sig_ox.extract(width, width)), 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);
+                       for (unsigned i = 0; i < width; i++) {
+                               module->addNex(new_verific_id(inst), sig_d[i], State::S0, sig_dx[i]);
+                               module->addEqx(new_verific_id(inst), sig_d[i], State::S1, sig_dx[i + width]);
+                       }
+
+                       Const qx_init = Const(State::S1, width);
+                       qx_init.bits.resize(2 * width, State::S0);
+
+                       clocking.addDff(new_verific_id(inst), sig_dx, sig_qx, qx_init);
+                       module->addXnor(new_verific_id(inst), sig_dx, sig_qx, sig_ox);
+
+                       module->addAnd(new_verific_id(inst), sig_ox.extract(0, width), sig_ox.extract(width, width), sig_o);
 
                        if (!mode_keep)
                                continue;

diff --git a/tests/sva/sva_value_change_changed_wide.sv b/tests/sva/sva_value_change_changed_wide.sv
new file mode 100644 (file)
index 0000000..c9147c4
--- /dev/null
+++ b/tests/sva/sva_value_change_changed_wide.sv
@@ -0,0 +1,22 @@
+module top (
+       input clk,
+       input [2:0] a,
+       input [2:0] b
+);
+       default clocking @(posedge clk); endclocking
+
+       assert property (
+               $changed(a)
+       );
+
+    assert property (
+        $changed(b) == ($changed(b[0]) || $changed(b[1]) || $changed(b[2]))
+    );
+
+`ifndef FAIL
+       assume property (
+               a !== 'x ##1 $changed(a)
+       );
+`endif
+
+endmodule

diff --git a/tests/sva/sva_value_change_sim.sv b/tests/sva/sva_value_change_sim.sv
index 80ff309cd5e0c8f59689dddf5840f233ece38ca0..92fe30b239a383d8cae5101b01f09b1679d7463a 100644 (file)
--- a/tests/sva/sva_value_change_sim.sv
+++ b/tests/sva/sva_value_change_sim.sv
@@ -7,6 +7,8 @@ reg [7:0] counter = 0;
 reg a = 0;
 reg b = 1;
 reg c;
+reg [2:0] wide_a = 3'b10x;
+reg [2:0] wide_b = 'x;
 
 wire a_fell; assign a_fell = $fell(a, @(posedge clk));
 wire a_rose; assign a_rose = $rose(a, @(posedge clk));
@@ -20,6 +22,9 @@ 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));
 
+wire wide_a_stable; assign wide_a_stable = $stable(wide_a, @(posedge clk));
+wire wide_b_stable; assign wide_b_stable = $stable(wide_b, @(posedge clk));
+
 always @(posedge clk) begin
        counter <= counter + 1;
 
@@ -28,13 +33,20 @@ always @(posedge clk) 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));
+            assert property (!$stable(wide_a));
+            assert property ($stable(wide_b));
             a <= 1; b <= 1; c <= 1;
         end
-               1: begin a <= 0; b <= 1; c <= 'x; end
+               1: begin
+            a <= 0; b <= 1; c <= 'x;
+            wide_a <= 3'b101; wide_b <= 3'bxx0;
+        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));
+            assert property (!$stable(wide_a));
+            assert property (!$stable(wide_b));
             a <= 0; b <= 0; c <= 0;
         end
                3: begin a <= 0; b <= 1; c <= 'x; end
@@ -42,9 +54,16 @@ always @(posedge clk) 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));
+            assert property ($stable(wide_a));
+            assert property ($stable(wide_b));
             a <= 'x; b <= 'x; c <= 'x;
+            wide_a <= 'x; wide_b <= 'x;
+        end
+               5: begin
+            a <= 0; b <= 1; c <= 'x;
+            wide_a <= 3'b10x; wide_b <= 'x;
+            counter <= 0;
         end
-               5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end
        endcase;
 end