From 73bcf5e0dbd7721ec63fc707891ffd14dbbc0080 Mon Sep 17 00:00:00 2001 From: Artur Bieniek Date: Wed, 12 Aug 2026 18:28:32 +0200 Subject: [PATCH] Fix NFA range ring outgoing bit selection (#8061 repair) (#8092) Signed-off-by: Artur Bieniek --- src/V3AssertNfa.cpp | 16 ++++------------ test_regress/t/t_property_delay_large.v | 5 +++-- test_regress/t/t_property_nfa_error_limit.out | 6 +++--- test_regress/t/t_property_nfa_error_limit.v | 13 ++++++++++--- 4 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index e015923de..1fac39083 100644 --- a/src/V3AssertNfa.cpp +++ b/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{ - c.flp, delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ}), - liveCountWidth}}; + new AstExtend{c.flp, delayRingBit(c.flp, ringp, outgoingIdxp), liveCountWidth}}; updateBodyp->addNext(new AstAssignDly{ c.flp, new AstVarRef{c.flp, liveCountVarp, VAccess::WRITE}, nextLiveCountp}); diff --git a/test_regress/t/t_property_delay_large.v b/test_regress/t/t_property_delay_large.v index 39caf5af4..7846f5b6c 100644 --- a/test_regress/t/t_property_delay_large.v +++ b/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 == 730); + || (cyc == 140) || (cyc == 559) + || (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); diff --git a/test_regress/t/t_property_nfa_error_limit.out b/test_regress/t/t_property_nfa_error_limit.out index b5a6df2b1..45412db25 100644 --- a/test_regress/t/t_property_nfa_error_limit.out +++ b/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. --Info: t/t_property_nfa_error_limit.v:46: Verilog $stop, ignored due to +verilator+error+limit -[7] %Error: t_property_nfa_error_limit.v:45: 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:48: Verilog $stop, ignored due to +verilator+error+limit +[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. diff --git a/test_regress/t/t_property_nfa_error_limit.v b/test_regress/t/t_property_nfa_error_limit.v index 5031262be..587c56b27 100644 --- a/test_regress/t/t_property_nfa_error_limit.v +++ b/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;