Randomize disable iff tests with reference models, dedup Link OR propagation, extract shift-chain helpers

src/V3AssertNfa.cpp

@@ -33,6 +33,7 @@
 #include "V3UniqueNames.h"
 
 #include <set>
+#include <unordered_map>
 #include <unordered_set>
 #include <vector>
 
@@ -1652,98 +1653,93 @@ class SvaNfaLowering final {
         AstNodeExpr* throughoutRejectp = nullptr;  // Reject when a throughout guard drops
     };
 
-    // Pack ##N delay and uniform b[*N] repetition sub-chains -- maximal simple
+    static const SvaTransEdge* singleClockedInEdge(SvaStateVertex* vtxp) {
-    // paths of registered vertices, each holding the previous vertex's state
+        const SvaTransEdge* inp = nullptr;
-    // delayed one cycle -- into single vectors shifted once per clock
+        for (const V3GraphEdge& er : vtxp->inEdges()) {
-    // (verilator/verilator#7792). Sets shiftVecp/shiftBit/shiftStepCondp.
+            const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
+            if (!te.m_consumesCycle) return nullptr;  // an incoming Link disqualifies
+            if (inp) return nullptr;  // more than one clocked source -> OR-merge
+            inp = &te;
+        }
+        return inp;
+    }
+    static bool shiftable(const std::vector<SvaStateVertex*>& vtx, int i, int startIdx) {
+        SvaStateVertex* const v = vtx[i];
+        if (!v->datap()->needsReg) return false;
+        if (i == startIdx || v->m_isMatch) return false;
+        if (v->m_isCounter || v->m_isAndCombiner || v->m_isRejectSink) return false;
+        if (v->m_isUnbounded) return false;  // self-loop accumulator, not a pure shift
+        if (v->m_strongPending) return false;  // final-block liveness reads its own reg
+        if (!v->m_throughoutConds.empty()) return false;
+        return singleClockedInEdge(v) != nullptr;
+    }
+    // Chain predecessor of a registered vertex and the per-step condition into it
+    // (null = unconditional ##N delay; else the b[*N] Link boolean).
+    static int chainPred(const std::vector<SvaStateVertex*>& vtx, int ci, int startIdx,
+                         AstNodeExpr*& condpr) {
+        condpr = nullptr;
+        const SvaTransEdge* const e = singleClockedInEdge(vtx[ci]);
+        if (!e || e->m_rejectOnFail || e->m_condVtxp) return -1;
+        const int mi = e->fromVtxp()->color();
+        if (shiftable(vtx, mi, startIdx)) {  // direct clocked step
+            condpr = e->m_condp;
+            return mi;
+        }
+        if (e->m_condp) return -1;  // pass-through requires an unconditional ##1 edge
+        SvaStateVertex* const m = vtx[mi];
+        const SvaTransEdge* linkp = nullptr;
+        for (const V3GraphEdge& er : m->inEdges()) {
+            if (linkp) return -1;  // more than one input -> not a clean pass-through
+            linkp = static_cast<const SvaTransEdge*>(&er);
+        }
+        if (!linkp || linkp->m_consumesCycle || linkp->m_rejectOnFail || linkp->m_condVtxp)
+            return -1;
+        const int pi = linkp->fromVtxp()->color();
+        if (!shiftable(vtx, pi, startIdx)) return -1;
+        condpr = linkp->m_condp;
+        return pi;
+    }
+    static bool sameCond(const AstNodeExpr* a, const AstNodeExpr* b) {
+        if (!a && !b) return true;
+        if (!a || !b) return false;
+        return a->sameTree(b);
+    }
+
+    // Pack ##N delay and uniform b[*N] repetition chains of registered vertices
+    // into single vectors shifted once per clock. Sets shiftVecp/shiftBit/etc.
     void detectShiftChains(const std::vector<SvaStateVertex*>& vtx, int N, int startIdx,
                            const std::string& baseName, FileLine* flp) {
-        const auto singleClockedInEdge = [](SvaStateVertex* v) -> const SvaTransEdge* {
+        // Link each shiftable vertex to its unique chain predecessor and successor.
-            const SvaTransEdge* inp = nullptr;
-            for (const V3GraphEdge& er : v->inEdges()) {
-                const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
-                if (!te.m_consumesCycle) return nullptr;  // an incoming Link disqualifies
-                if (inp) return nullptr;  // more than one clocked source -> OR-merge
-                inp = &te;
-            }
-            return inp;
-        };
-        const auto shiftable = [&](int i) -> bool {
-            SvaStateVertex* const v = vtx[i];
-            if (!v->datap()->needsReg) return false;
-            if (i == startIdx || v->m_isMatch) return false;
-            if (v->m_isCounter || v->m_isAndCombiner || v->m_isRejectSink) return false;
-            if (v->m_isUnbounded) return false;  // self-loop accumulator, not a pure shift
-            if (v->m_strongPending) return false;  // final-block liveness reads its own reg
-            if (!v->m_throughoutConds.empty()) return false;
-            return singleClockedInEdge(v) != nullptr;
-        };
-        // Chain predecessor of a registered vertex, plus the per-step condition
-        // into it (null = unconditional). A shift step is a direct clocked edge
-        // (##N delay) or a clocked edge fed through one pass-through condition
-        // Link vertex (`b[*N]` repetition; the Link boolean is the condition).
-        const auto chainPred = [&](int ci, AstNodeExpr*& condpr) -> int {
-            condpr = nullptr;
-            const SvaTransEdge* const e = singleClockedInEdge(vtx[ci]);
-            if (!e || e->m_rejectOnFail || e->m_condVtxp) return -1;
-            const int mi = e->fromVtxp()->color();
-            if (shiftable(mi)) {  // direct clocked step
-                condpr = e->m_condp;
-                return mi;
-            }
-            if (e->m_condp) return -1;  // pass-through requires an unconditional ##1 edge
-            SvaStateVertex* const m = vtx[mi];
-            const SvaTransEdge* linkp = nullptr;
-            for (const V3GraphEdge& er : m->inEdges()) {
-                if (linkp) return -1;  // more than one input -> not a clean pass-through
-                linkp = static_cast<const SvaTransEdge*>(&er);
-            }
-            if (!linkp || linkp->m_consumesCycle || linkp->m_rejectOnFail || linkp->m_condVtxp)
-                return -1;
-            const int pi = linkp->fromVtxp()->color();
-            if (!shiftable(pi)) return -1;
-            condpr = linkp->m_condp;
-            return pi;
-        };
-        const auto sameCond = [](const AstNodeExpr* a, const AstNodeExpr* b) -> bool {
-            if (!a && !b) return true;
-            if (!a || !b) return false;
-            return a->sameTree(b);
-        };
-        // Bond each vertex to its chain predecessor; a predecessor feeding more
-        // than one chain vertex branches and cannot shift unambiguously.
         struct Bond final {
             int pred = -1;
+            int next = -1;
+            int childCount = 0;
+            bool hasPrev = false;
             AstNodeExpr* stepCondp = nullptr;  // borrowed step condition into this vertex
         };
         std::vector<Bond> bond(N);
-        std::vector<int> childCount(N, 0);
         for (int i = 0; i < N; ++i) {
-            if (!shiftable(i)) continue;
+            if (!shiftable(vtx, i, startIdx)) continue;
             AstNodeExpr* cp = nullptr;
-            const int p = chainPred(i, cp);
+            const int p = chainPred(vtx, i, startIdx, cp);
             if (p < 0) continue;
-            bond[i] = {p, cp};
+            bond[i].pred = p;
-            ++childCount[p];
+            bond[i].stepCondp = cp;
+            ++bond[p].childCount;
         }
-        std::vector<int> nextInChain(N, -1);
-        std::vector<bool> hasPrevInChain(N, false);
         for (int i = 0; i < N; ++i) {
             const int p = bond[i].pred;
-            if (p < 0 || childCount[p] != 1) continue;
+            if (p < 0 || bond[p].childCount != 1) continue;
-            nextInChain[p] = i;
+            bond[p].next = i;
-            hasPrevInChain[i] = true;
+            bond[i].hasPrev = true;
         }
-        // Walk each chain head, splitting into maximal segments whose interior
+        // Split each chain into maximal segments sharing one step condition,
-        // steps share one condition; each segment of >= 2 vertices packs into
+        // each packed into one vector. Cap at 64 bits (wider VlWide breaks V3Subst).
-        // one vector. Segments cap at 64 bits: a wider (VlWide) shift emitted
-        // after V3Width is not word-split and breaks V3Subst. A capped chain
-        // carries into the next vector through the shared clocked predecessor.
         constexpr int kMaxShiftVec = 64;
         for (int h = 0; h < N; ++h) {
-            if (hasPrevInChain[h] || nextInChain[h] == -1) continue;
+            if (bond[h].hasPrev || bond[h].next == -1) continue;
             std::vector<int> chain;
-            for (int j = h; j != -1; j = nextInChain[j]) chain.push_back(j);
+            for (int j = h; j != -1; j = bond[j].next) chain.push_back(j);
             int a = 0;
             while (a + 1 < static_cast<int>(chain.size())) {
                 AstNodeExpr* const segCondp = bond[chain[a + 1]].stepCondp;
@@ -1787,8 +1783,7 @@ class SvaNfaLowering final {
                 AstNodeExpr* srcSigp = c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false);
                 srcSigp = andCond(c.flp, srcSigp, te.m_condp);
 
-                // Zero in-flight state while the disable is active; the edge
+                // Zero in-flight state while the disable is active.
-                // counter misses a held or mid-window disable (IEEE 1800-2023 16.12)
                 if (c.disableExprp) {
                     AstNodeExpr* const notDisp
                         = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
@@ -1811,10 +1806,8 @@ class SvaNfaLowering final {
             }
         }
 
-        // Delay / uniform-repetition chains: one masked shift per vector.
+        // One masked shift per vector; bit 0 injects the head's feeder:
         //   vec <= (((vec << 1) & {W{step}}) | inject) & {W{!disable & !kill}}
-        // bit 0 injects the head's feeder; `step` is the shared per-step
-        // condition (absent for a pure ##N delay), on the shifted bits only.
         for (int i = 0; i < c.N; ++i) {
             if (!c.vtx[i]->datap()->shiftVecp || c.vtx[i]->datap()->shiftBit != 0) continue;
             AstVar* const vecp = c.vtx[i]->datap()->shiftVecp;
@@ -1919,8 +1912,7 @@ class SvaNfaLowering final {
 
             AstNodeExpr* donep = new AstLogOr{c.flp, killActive(c),
                                               new AstLogOr{c.flp, matchedNowp, counterAtEndp}};
-            // A mid-window disable aborts the in-flight count (IEEE 1800-2023
+            // A mid-window disable aborts the in-flight count.
-            // 16.12); the expiry reject is separately disable-gated
             if (c.disableExprp)
                 donep = new AstLogOr{c.flp, donep, c.disableExprp->cloneTreePure(false)};
 
@@ -2004,8 +1996,7 @@ class SvaNfaLowering final {
 
             AstNodeExpr* clearCondp = new AstLogOr{
                 c.flp, killActive(c), c.vtx[ai]->datap()->stateSigp->cloneTreePure(false)};
-            // A mid-window disable clears a half-latched side so a disabled
+            // A mid-window disable clears a half-latched side.
-            // attempt cannot pair with a later attempt (IEEE 1800-2023 16.12)
             if (c.disableExprp)
                 clearCondp = new AstLogOr{c.flp, clearCondp, c.disableExprp->cloneTreePure(false)};
             AstIf* const topp = new AstIf{c.flp, clearCondp, clearLp, setLIfp};
@@ -2215,6 +2206,7 @@ class SvaNfaLowering final {
         // Fixed-point propagation along zero-delay (Link) edges.
         // Worst case: longest chain is N hops; SAnd seeding adds one extra round;
         // factor-of-2 covers reverse-order dependencies.
+        std::unordered_map<const SvaTransEdge*, const AstNodeExpr*> consumedSrcp;
         for (int pass = 0; pass < 2 * c.N + 2; ++pass) {
             bool changed = false;
             // Seed SAnd combiners (sub-NFA termVertices may only be available
@@ -2246,14 +2238,18 @@ class SvaNfaLowering final {
             }
             // Propagate Link edges
             for (int fi = 0; fi < c.N; ++fi) {
-                if (!c.vtx[fi]->datap()->stateSigp) continue;
+                AstNodeExpr* const srcp = c.vtx[fi]->datap()->stateSigp;
+                if (!srcp) continue;
                 for (const V3GraphEdge& er : c.vtx[fi]->outEdges()) {
                     const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
                     if (te.m_consumesCycle) continue;
                     const int ti = te.toVtxp()->color();
                     if (te.toVtxp()->m_isMatch || te.toVtxp()->m_isRejectSink) continue;
-                    AstNodeExpr* const contributionp = andCond(
+                    // Consume each Link edge once per distinct source value
-                        c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false), te.m_condp);
+                    if (consumedSrcp[&te] == srcp) continue;
+                    consumedSrcp[&te] = srcp;
+                    AstNodeExpr* const contributionp
+                        = andCond(c.flp, srcp->cloneTreePure(false), te.m_condp);
                     if (!c.vtx[ti]->datap()->stateSigp) {
                         c.vtx[ti]->datap()->stateSigp = contributionp;
                         changed = true;

test_regress/t/t_prop_always.v

@@ -88,9 +88,6 @@ module t (
       `checkd(rand_bounded_pass_q.size(), 0);
       `checkd(rand_bounded_fail_q.size(), 20);  // Other sims: 19, 11
       `checkd(disable_bounded_pass_q.size(), 0);
-      // A disable true anywhere in the [0:3] window suppresses the attempt;
-      // the residual vs other sims is a disable arriving only after an
-      // in-window failure already fired, which a streaming NFA cannot un-fire.
       `checkd(disable_bounded_fail_q.size(), 8);  // Other sims: 5, 6
       $write("*-* All Finished *-*\n");
       $finish;

test_regress/t/t_property_disable_iff_counter.py

@@ -11,6 +11,8 @@ import vltest_bootstrap
 
 test.scenarios('simulator')
 
+test.sim_time = 16000
+
 test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
 
 test.execute()

test_regress/t/t_property_disable_iff_counter.v

@@ -9,38 +9,59 @@
 `define checkd(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
 // verilog_format: on
 
-// IEEE 1800-2023 16.12: a disable iff true at ANY point of a multi-cycle
+// disable iff mid-window on the counter-FSM path (##[1:N], N > 256 unroll limit).
-// attempt window disables it. A range delay ##[1:N] with N over the 256 unroll
-// limit lowers to a counter-FSM backend (not a state-register chain), which had
-// the same mid-window-disable hole as the register path
-// (verilator/verilator#7792 follow-up). value never matches, so a live attempt
-// fails at window end; skip pulses once mid-window and must abort the in-flight
-// counter so the disabled assert does not fire.
 
 module t (
     input clk
 );
+  localparam int N = 257;  // > 256 unroll limit -> counter FSM path
+  localparam int PERIOD = 260;  // > N -> attempts never overlap
+  localparam int NATT = 30;
+
   int cyc = 0;
-  wire trig = (cyc == 5);
+  reg [63:0] crc = 64'h5aef0c8d_d70a4497;
-  wire value = 1'b0;  // never matches -> attempt would fail at window end
+
-  wire skip = (cyc == 50);  // single mid-window pulse
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
+  wire value = 1'b0;
+
+  reg do_dis = 0;
+  int dis_at = 0;
+  wire dis = in_run && do_dis && (phase == dis_at);
 
   int n_dis_fire = 0;
   int n_ctrl_fire = 0;
+  int exp_dis_fire = 0;
 
-  // Range > 256 -> counter FSM. The cyc-5 attempt is hit by the skip pulse.
+  assert property (@(posedge clk) disable iff (dis) trig |-> ##[1:N] value)
-  assert property (@(posedge clk) disable iff (skip) trig |-> ##[1:300] value)
   else n_dis_fire <= n_dis_fire + 1;
 
-  // Control: same property never disabled -> the cyc-5 attempt fails once.
+  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##[1:N] value)
-  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##[1:300] value)
   else n_ctrl_fire <= n_ctrl_fire + 1;
 
   always @(posedge clk) begin
     cyc <= cyc + 1;
-    if (cyc == 320) begin
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
-      `checkd(n_dis_fire, 0);
+    if (phase == PERIOD - 1) begin
-      `checkd(n_ctrl_fire, 1);
+      phase <= 0;
+      idx <= idx + 1;
+    end else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      do_dis <= crc[3];
+      dis_at <= 1 + (int'(crc[20:12]) % (N - 1));
+    end
+    if (in_run && phase == N && !do_dis) exp_dis_fire <= exp_dis_fire + 1;
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("n_dis_fire=%0d exp=%0d n_ctrl_fire=%0d\n", n_dis_fire, exp_dis_fire, n_ctrl_fire);
+`endif
+      `checkd(n_dis_fire, exp_dis_fire);
+      `checkd(n_ctrl_fire, NATT);
+      if (n_dis_fire == 0 || n_dis_fire == NATT) $stop;  // guard a degenerate seed
       $write("*-* All Finished *-*\n");
       $finish;
     end

test_regress/t/t_property_disable_iff_held.v

@@ -9,47 +9,65 @@
 `define checkd(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
 // verilog_format: on
 
-// IEEE 1800-2023 16.12: a disable iff condition held continuously true must
+// A disable iff held true for the whole attempt window disables it.
-// disable every attempt of a multi-cycle property (verilator/verilator#7792).
-// en_held is a plain non-$sampled, non-constant signal held 1, so it exercises
-// the NFA disable-counter path. The held assert/cover must never fire; the
-// `disable iff (1'b0)` controls prove the same assert/cover do fire when enabled.
 
 module t (
     input clk
 );
+  localparam int N = 5;
+  localparam int PERIOD = 9;
+  localparam int NATT = 40;
+
   int cyc = 0;
   reg [63:0] crc = 64'h5aef0c8d_d70a4497;
-  wire a = crc[0];
-  wire b = crc[4];
 
-  bit en_held = 1'b1;
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
 
-  int n_held_assert = 0;
+  reg hold = 0;
-  int n_held_cover = 0;
+  reg fail_now = 0;
-  int n_ctrl_assert = 0;
+  wire value = !(in_run && (phase == N) && fail_now);
-  int n_ctrl_cover = 0;
+  wire dis = in_run && hold && (phase >= 1);
 
-  // Held-true disable: assert + cover must be fully suppressed.
+  int n_held_fire = 0;
-  assert property (@(posedge clk) disable iff (en_held) (a ##1 b))
+  int n_ctrl_fire = 0;
-    else n_held_assert <= n_held_assert + 1;
+  int exp_held_fire = 0;
-  cover property (@(posedge clk) disable iff (en_held) (a ##1 b))
+  int exp_ctrl_fire = 0;
-    n_held_cover <= n_held_cover + 1;
 
-  // Enabled control (disable iff 1'b0): same assert + cover must fire.
+  assert property (@(posedge clk) disable iff (dis) trig |-> ##N value)
-  assert property (@(posedge clk) disable iff (1'b0) (a ##1 b))
+  else n_held_fire <= n_held_fire + 1;
-    else n_ctrl_assert <= n_ctrl_assert + 1;
+
-  cover property (@(posedge clk) disable iff (1'b0) (a ##1 b))
+  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##N value)
-    n_ctrl_cover <= n_ctrl_cover + 1;
+  else n_ctrl_fire <= n_ctrl_fire + 1;
 
   always @(posedge clk) begin
     cyc <= cyc + 1;
     crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
-    if (cyc == 99) begin
+    if (phase == PERIOD - 1) begin
-      `checkd(n_held_assert, 0);
+      phase <= 0;
-      `checkd(n_held_cover, 0);
+      idx <= idx + 1;
-      `checkd(n_ctrl_assert, 58);
+    end
-      `checkd(n_ctrl_cover, 26);  // Others: 26, One other: 0
+    else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      hold <= crc[3];
+      fail_now <= crc[7];
+    end
+    if (in_run && phase == N) begin
+      exp_ctrl_fire <= exp_ctrl_fire + (fail_now ? 1 : 0);
+      if (!hold) exp_held_fire <= exp_held_fire + (fail_now ? 1 : 0);
+    end
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("n_held_fire=%0d exp=%0d n_ctrl_fire=%0d exp_ctrl=%0d\n", n_held_fire, exp_held_fire,
+             n_ctrl_fire, exp_ctrl_fire);
+`endif
+      `checkd(n_held_fire, exp_held_fire);
+      `checkd(n_ctrl_fire, exp_ctrl_fire);
+      if (n_held_fire == 0 || n_held_fire == NATT) $stop;
       $write("*-* All Finished *-*\n");
       $finish;
     end

test_regress/t/t_property_disable_iff_midpulse.v

@@ -9,39 +9,67 @@
 `define checkd(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
 // verilog_format: on
 
-// IEEE 1800-2023 16.12: a disable iff condition true at ANY point of a
+// Mid-window disable pulse on the packed ##N delay path (N < unroll limit).
-// multi-cycle attempt window disables that attempt, not only when held
-// continuously (verilator/verilator#7792 follow-up to #7841). skip is a plain
-// non-$sampled, non-constant signal pulsed true for a single cycle in the
-// MIDDLE of the ##10 window. value is low only at the attempt's match cycle, so
-// exactly one attempt would fail; the mid-window skip pulse must disable it.
-// Pre-fix the in-flight NFA states were not zeroed on a mid-window pulse, so the
-// disabled assert fired; the control proves the same attempt fails when enabled.
 
 module t (
     input clk
 );
+  localparam int N = 8;
+  localparam int PERIOD = 12;
+  localparam int NATT = 40;
+
   int cyc = 0;
-  wire value = (cyc != 10);  // low only at the cyc-0 attempt's match cycle
+  reg [63:0] crc = 64'h5aef0c8d_d70a4497;
-  wire skip = (cyc == 5);  // single-cycle pulse, mid-window of [0..10]
+
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
+
+  reg do_dis = 0;
+  int dis_at = 0;
+  reg fail_now = 0;
+  wire value = !(in_run && (phase == N) && fail_now);
+  wire dis = in_run && do_dis && (phase == dis_at);
 
   int n_dis_fire = 0;
   int n_ctrl_fire = 0;
+  int exp_dis_fire = 0;
+  int exp_ctrl_fire = 0;
 
-  // Mid-window-pulse disable: the cyc-0 attempt (matches at cyc 10, where value
+  assert property (@(posedge clk) disable iff (dis) trig |-> ##N value)
-  // is low -> would fail) must be disabled by the skip pulse at cyc 5.
-  assert property (@(posedge clk) disable iff (skip) (##10 value))
   else n_dis_fire <= n_dis_fire + 1;
 
-  // Control: same property always enabled -> the cyc-0 attempt fails once.
+  assert property (@(posedge clk) disable iff (1'b0) trig |-> ##N value)
-  assert property (@(posedge clk) disable iff (1'b0) (##10 value))
   else n_ctrl_fire <= n_ctrl_fire + 1;
 
   always @(posedge clk) begin
     cyc <= cyc + 1;
-    if (cyc == 20) begin
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
-      `checkd(n_dis_fire, 0);
+    if (phase == PERIOD - 1) begin
-      `checkd(n_ctrl_fire, 1);
+      phase <= 0;
+      idx <= idx + 1;
+    end
+    else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      do_dis <= crc[3];
+      dis_at <= 1 + (int'(crc[20:12]) % (N - 1));
+      fail_now <= crc[7];
+    end
+    if (in_run && phase == N) begin
+      exp_ctrl_fire <= exp_ctrl_fire + (fail_now ? 1 : 0);
+      if (!do_dis) exp_dis_fire <= exp_dis_fire + (fail_now ? 1 : 0);
+    end
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("n_dis_fire=%0d exp=%0d n_ctrl_fire=%0d exp_ctrl=%0d\n", n_dis_fire, exp_dis_fire,
+             n_ctrl_fire, exp_ctrl_fire);
+`endif
+      `checkd(n_dis_fire, exp_dis_fire);
+      `checkd(n_ctrl_fire, exp_ctrl_fire);
+      if (n_dis_fire == 0 || n_dis_fire == NATT) $stop;
       $write("*-* All Finished *-*\n");
       $finish;
     end

test_regress/t/t_property_shift_chunk.py

@@ -11,6 +11,8 @@ import vltest_bootstrap
 
 test.scenarios('simulator')
 
+test.sim_time = 4000
+
 test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing'])
 
 test.execute()

test_regress/t/t_property_shift_chunk.v

@@ -9,29 +9,77 @@
 `define checkd(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
 // verilog_format: on
 
-// A ##130 delay is a 129-vertex shift chain packed across three <=64-bit
+// ##N delay and held[*N] repetition pack shift chains across 64-bit chunks;
-// vectors (verilator/verilator#7792 optimization). This exercises the
+// the completion must land on exactly cycle N (off-by-one brackets fail).
-// cross-chunk carry: each next vector's bit 0 injects the previous vector's top
-// bit through the shared clocked predecessor. res is high only exactly 130
-// cycles after the single antecedent match, so an off-by-one or dropped carry
-// makes the consequent miss and the assert fire.
 
 module t (
     input clk
 );
+  localparam int LEN = 130;
+  localparam int PERIOD = 140;
+  localparam int NATT = 12;
+
   int cyc = 0;
-  wire trig = (cyc == 5);
+  reg [63:0] crc = 64'h5aef0c8d_d70a4497;
-  wire res = (cyc == 5 + 130);
 
-  int n_fire = 0;
+  int phase = 0;
+  int idx = 0;
+  wire in_run = (idx < NATT);
+  wire trig = in_run && (phase == 0);
 
-  assert property (@(posedge clk) trig |-> ##130 res)
+  reg res_fail = 0;
-  else n_fire <= n_fire + 1;
+  reg rep_fail = 0;
+  wire res = in_run && (phase == LEN) && !res_fail;
+  wire rep_res = in_run && (phase == LEN) && !rep_fail;
+  wire held = in_run && (phase <= LEN - 1);
+
+  int n_d129 = 0;
+  int n_d130 = 0;
+  int n_d131 = 0;
+  int n_rok = 0;
+  int n_rbad = 0;
+  int exp_d130 = 0;
+  int exp_rok = 0;
+
+  assert property (@(posedge clk) trig |-> ##(LEN-1) res)
+  else n_d129 <= n_d129 + 1;
+  assert property (@(posedge clk) trig |-> ##LEN res)
+  else n_d130 <= n_d130 + 1;
+  assert property (@(posedge clk) trig |-> ##(LEN+1) res)
+  else n_d131 <= n_d131 + 1;
+
+  assert property (@(posedge clk) trig |-> held[*LEN] ##1 rep_res)
+  else n_rok <= n_rok + 1;
+  assert property (@(posedge clk) trig |-> held[*(LEN + 1)] ##1 rep_res)
+  else n_rbad <= n_rbad + 1;
 
   always @(posedge clk) begin
     cyc <= cyc + 1;
-    if (cyc == 160) begin
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
-      `checkd(n_fire, 0);
+    if (phase == PERIOD - 1) begin
+      phase <= 0;
+      idx <= idx + 1;
+    end
+    else begin
+      phase <= phase + 1;
+    end
+    if (phase == 0) begin
+      res_fail <= crc[2];
+      rep_fail <= crc[9];
+    end
+    if (in_run && phase == LEN) exp_d130 <= exp_d130 + (res_fail ? 1 : 0);
+    if (in_run && phase == LEN) exp_rok <= exp_rok + (rep_fail ? 1 : 0);
+    if (idx == NATT && phase == 4) begin
+`ifdef TEST_VERBOSE
+      $write("d129=%0d d130=%0d exp=%0d d131=%0d rok=%0d exp=%0d rbad=%0d\n", n_d129, n_d130,
+             exp_d130, n_d131, n_rok, exp_rok, n_rbad);
+`endif
+      `checkd(n_d129, NATT);
+      `checkd(n_d130, exp_d130);
+      `checkd(n_d131, NATT);
+      `checkd(n_rok, exp_rok);
+      `checkd(n_rbad, NATT);
+      if (exp_d130 == 0 || exp_d130 == NATT) $stop;
       $write("*-* All Finished *-*\n");
       $finish;
     end