Fix NFA range ring outgoing bit selection (#8061 repair) (#8092)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>

src/V3AssertNfa.cpp

@@ -1811,26 +1811,18 @@ class SvaNfaLowering final {
                              VAccess::WRITE),
                 incomingp};
             AstNode* updateBodyp = writeIncomingp;
-            if (!vtxp->m_isFixedDelayRing) {
-                // ring[next_idx] <= 1'b0;
-                AstAssignDly* const clearExpirep = new AstAssignDly{
-                    c.flp,
-                    delayRingBit(c.flp, ringp, nextRingIndex(c.flp, idxp, size), VAccess::WRITE),
-                    new AstConst{c.flp, AstConst::BitFalse{}}};
-                clearExpirep->addNext(writeIncomingp);
-                updateBodyp = clearExpirep;
-            }
             // live_count <= live_count + incoming_bit - outgoing_bit;
             const int liveCountWidth = liveCountVarp->dtypep()->width();
             AstNodeExpr* const incomingIncrementp
                 = new AstExtend{c.flp, incomingp->cloneTreePure(false), liveCountWidth};
+            AstNodeExpr* const outgoingIdxp = vtxp->m_isFixedDelayRing
+                                                  ? new AstVarRef{c.flp, idxp, VAccess::READ}
+                                                  : nextRingIndex(c.flp, idxp, size);
             AstSub* const nextLiveCountp = new AstSub{
                 c.flp,
                 new AstAdd{c.flp, new AstVarRef{c.flp, liveCountVarp, VAccess::READ},
                            incomingIncrementp},
-                new AstExtend{
+                new AstExtend{c.flp, delayRingBit(c.flp, ringp, outgoingIdxp), liveCountWidth}};
-                    c.flp, delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ}),
-                    liveCountWidth}};
             updateBodyp->addNext(new AstAssignDly{
                 c.flp, new AstVarRef{c.flp, liveCountVarp, VAccess::WRITE}, nextLiveCountp});
 

test_regress/t/t_property_delay_large.v

@@ -35,9 +35,10 @@ module t (
                       || (cyc == 680) || (cyc == 720);
   wire range_fail_a = (cyc >= 250 && cyc <= 257) || (cyc >= 820 && cyc <= 827);
   wire range_a = range_pass_a || range_fail_a;
+  // The pulse at 559 must not match after all preceding attempts have expired.
   wire range_b = (cyc == 20) || (cyc == 50) || (cyc == 80) || (cyc == 110)
-                 || (cyc == 140) || (cyc == 610) || (cyc == 650) || (cyc == 690)
+                 || (cyc == 140) || (cyc == 559)
-                 || (cyc == 730);
+                 || (cyc == 610) || (cyc == 650) || (cyc == 690) || (cyc == 730);
 
   // Questa action blocks observe the cycle after the sampled property cycle.
   cover property (@(posedge clk) fixed_a ##1024 fixed_b) fixed_pass_q.push_back($sampled(cyc) + 1);

test_regress/t/t_property_nfa_error_limit.out

@@ -1,6 +1,6 @@
-[7] %Error: t_property_nfa_error_limit.v:46: Assertion failed in top.t: 'assert' failed.
+[5] %Error: t_property_nfa_error_limit.v:48: Assertion failed in top.t: 'assert' failed.
--Info: t/t_property_nfa_error_limit.v:46: Verilog $stop, ignored due to +verilator+error+limit
+-Info: t/t_property_nfa_error_limit.v:48: Verilog $stop, ignored due to +verilator+error+limit
-[7] %Error: t_property_nfa_error_limit.v:45: Assertion failed in top.t: 'assert' failed.
+[7] %Error: t_property_nfa_error_limit.v:49: Assertion failed in top.t: 'assert' failed.
 [9] %Error: t_property_nfa_error_limit.v:32: Assertion failed in top.t: 'assert' failed.
 [11] %Error: t_property_nfa_error_limit.v:35: Assertion failed in top.t: 'assert' failed.
 [13] %Error: t_property_nfa_error_limit.v:37: Assertion failed in top.t: 'assert' failed.

test_regress/t/t_property_nfa_error_limit.v

@@ -38,14 +38,17 @@ module t (
 
   // Simultaneous negated-consequent failures behind a temporal antecedent
   bit ant = 0;
+  bit early_b = 0;
   bit b = 0;
   int temporal_small_fail = 0, temporal_ring_fail = 0, boolean_ant_fail = 0;
   int impossible_pass = 0, impossible_fail = 0;
 
-  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:2] b));
+  // Separate consequent pulses keep diagnostic order independent of
+  // multithreaded mtask numbering.
+  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:2] early_b));
   assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:300] b));
 
-  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:2] b))
+  assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:2] early_b))
   else temporal_small_fail++;
   assert property (@(posedge clk) (1'b1 ##1 ant) |-> not (1'b1 ##[1:300] b))
   else temporal_ring_fail++;
@@ -65,9 +68,13 @@ module t (
 
   initial begin
     @(negedge clk) ant = 1;
-    @(negedge clk) ant = 1;
+    @(negedge clk) begin
+      ant = 1;
+      early_b = 1;
+    end
     @(negedge clk) begin
       ant = 0;
+      early_b = 0;
       b = 1;
     end
     @(negedge clk) b = 0;