Optimize consecutive repetiton and goto repetition using ring-buffer (#8096)

src/V3AssertNfa.cpp

@@ -73,10 +73,15 @@ public:
     std::vector<AstNodeExpr*> m_throughoutConds;
     // Nonzero for a bitset ring-buffer vertex for ## delays.
     bool m_isFixedDelayRing = false;
-    unsigned m_delayRingSize = 0;  // Fixed delay cycles. Range: max-min+1.
+    unsigned m_delayRingSize = 0;  // Number of ring slots. Range: max-min+1.
     AstNodeExpr* m_delayRingClearCondp = nullptr;  // local RHS for pure-boolean range
-    // OWNED; enclosing-abort fire condition clearing in-flight ring bits
+    AstNodeExpr* m_delayRingAdvanceCondp = nullptr;  // Advance only when this condition holds
+    SvaStateVertex* m_matchCountRingp = nullptr;  // Ring supplying this checked match's count
+    bool m_replayAbortReject = false;  // Compressed repetition needs per-thread abort replay
+    // OWNED; enclosing-abort fire condition clearing state or suppressing guard rejection
     AstNodeExpr* m_abortClearp = nullptr;
+    // OWNED; reject-abort fire condition rejecting all represented live threads
+    AstNodeExpr* m_abortRejectp = nullptr;
     // Liveness terminal (IEEE weak semantics): reject must not fire from this source
     bool m_isUnbounded = false;
     // Temporal sequence AND combiner; IEEE 1800-2023 16.9.5
@@ -101,7 +106,10 @@ public:
         for (AstNodeExpr* cp : m_throughoutConds) VL_DO_DANGLING(cp->deleteTree(), cp);
         if (m_delayRingClearCondp)
             VL_DO_DANGLING(m_delayRingClearCondp->deleteTree(), m_delayRingClearCondp);
+        if (m_delayRingAdvanceCondp)
+            VL_DO_DANGLING(m_delayRingAdvanceCondp->deleteTree(), m_delayRingAdvanceCondp);
         if (m_abortClearp) VL_DO_DANGLING(m_abortClearp->deleteTree(), m_abortClearp);
+        if (m_abortRejectp) VL_DO_DANGLING(m_abortRejectp->deleteTree(), m_abortRejectp);
         if (m_andLhsCondp) VL_DO_DANGLING(m_andLhsCondp->deleteTree(), m_andLhsCondp);
         if (m_andRhsCondp) VL_DO_DANGLING(m_andRhsCondp->deleteTree(), m_andRhsCondp);
     }
@@ -516,17 +524,6 @@ class SvaNfaBuilder final {
         return sampled(exprp->cloneTreePure(false));
     }
 
-    // Reject concurrent assertions whose unrolled vertex count would exceed
-    // --assert-unroll-limit, so a pathological count cannot blow up compile time.
-    static bool exceedsAssertUnrollLimit(AstNode* nodep, unsigned requested) {
-        const int limit = v3Global.opt.assertUnrollLimit();
-        if (limit >= 0 && requested <= static_cast<unsigned>(limit)) return false;
-        nodep->v3error("Concurrent assertion repetition count "
-                       << requested << " exceeds --assert-unroll-limit (" << limit
-                       << "); raise '--assert-unroll-limit' to compile");
-        return true;
-    }
-
     // Create vertex and inherit temporal guards from the current scope.
     SvaStateVertex* scopedCreateVertex() {
         SvaStateVertex* const vtxp = m_graph.createStateVertex();
@@ -555,10 +552,11 @@ class SvaNfaBuilder final {
     }
 
     SvaStateVertex* addDelayChain(SvaStateVertex* startp, unsigned size, FileLine* flp,
-                                  bool isFixed = true, AstNodeExpr* clearCondp = nullptr) {
+                                  bool isFixed = true, AstNodeExpr* clearCondp = nullptr,
+                                  AstNodeExpr* advanceCondp = nullptr) {
         if (isFixed && size == 0) return startp;
         UASSERT_OBJ(size > 0, startp, "Delay chain needs at least one slot");
-        if (isFixed && size == 1) {
+        if (isFixed && size == 1 && !advanceCondp) {
             SvaStateVertex* const nextp = scopedCreateVertex();
             guardedEdge(startp, nextp, flp);
             return nextp;
@@ -570,6 +568,7 @@ class SvaNfaBuilder final {
             UASSERT_OBJ(!isFixed, startp, "Fixed delay cannot have a clear condition");
             ringVtxp->m_delayRingClearCondp = clearCondp->cloneTreePure(false);
         }
+        ringVtxp->m_delayRingAdvanceCondp = advanceCondp;
         if (isFixed) {
             guardedEdge(startp, ringVtxp, flp);
         } else {
@@ -765,7 +764,6 @@ class SvaNfaBuilder final {
         } else if (repp->maxCountp()) {
             totalSites += getConstUInt(repp->maxCountp()) - minN;
         }
-        if (exceedsAssertUnrollLimit(repp, totalSites)) return BuildResult::failWithError();
         AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites);
 
         // Cover-sequence (IEEE 1800-2023 16.14.3): collect each end-of-match
@@ -774,16 +772,25 @@ class SvaNfaBuilder final {
 
         SvaStateVertex* currentp = entryVtxp;
         for (unsigned i = 0; i < minN; ++i) {
-            if (i > 0) {
-                SvaStateVertex* const nextp = scopedCreateVertex();
-                guardedEdge(currentp, nextp, flp);
-                currentp = nextp;
+            // Keep the first repetition explicit, collapse all remaining checks into the ring.
+            if (i == 1) {
+                currentp = addDelayChain(currentp, minN - 1, flp);
+                currentp->m_delayRingClearCondp
+                    = new AstLogNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)};
+                currentp->m_replayAbortReject = true;
+                if (isTopLevelStep) {
+                    currentp->m_throughoutConds.push_back(
+                        sampledRefOrClone(hoistVarp, exprp, flp));
+                }
+                i = minN - 1;
             }
             // Every repetition in the minimum prefix is required.
             SvaStateVertex* const condVtxp = scopedCreateVertex();
             SvaTransEdge* const linkp
                 = guardedLink(currentp, condVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
-            if (isTopLevelStep) linkp->m_rejectOnFail = true;
+            // Only an outermost required step rejects the property. Its first check is explicit,
+            // later required checks reject through the ring's throughout guard.
+            if (isTopLevelStep && i == 0) linkp->m_rejectOnFail = true;
             currentp = condVtxp;
         }
         // After minN: currentp is the first valid end-of-match position for [*m:n].
@@ -815,13 +822,31 @@ class SvaNfaBuilder final {
             const unsigned maxN = getConstUInt(repp->maxCountp());
             SvaStateVertex* const mergeVtxp = scopedCreateVertex();
             guardedLink(currentp, mergeVtxp, flp);
-            for (unsigned i = minN; i < maxN; ++i) {
+            unsigned tailMinN = minN;
+            SvaStateVertex* tailStartp = currentp;
+            if (minN == 0) {
+                // Build the first optional iteration explicitly. Feeding the empty endpoint
+                // directly into a range ring would incorrectly keep that match alive.
                 SvaStateVertex* const nextVtxp = scopedCreateVertex();
                 guardedEdge(currentp, nextVtxp, flp);
                 SvaStateVertex* const checkVtxp = scopedCreateVertex();
                 guardedLink(nextVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
                 guardedLink(checkVtxp, mergeVtxp, flp);
-                currentp = checkVtxp;
+                if (m_isCoverSeq) consMidSources.push_back(checkVtxp);
+                tailStartp = checkVtxp;
+                tailMinN = 1;
+            }
+            if (maxN > tailMinN) {
+                // Add tail-ring only if the tail is non-empty.
+                SvaStateVertex* const nextVtxp
+                    = addDelayChain(tailStartp, maxN - tailMinN + 1, flp, false);
+                nextVtxp->m_delayRingClearCondp
+                    = new AstLogNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)};
+                nextVtxp->m_replayAbortReject = true;
+                SvaStateVertex* const checkVtxp = scopedCreateVertex();
+                guardedLink(nextVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
+                checkVtxp->m_matchCountRingp = nextVtxp;
+                guardedLink(checkVtxp, mergeVtxp, flp);
                 if (m_isCoverSeq) consMidSources.push_back(checkVtxp);
             }
             currentp = mergeVtxp;
@@ -892,55 +917,50 @@ class SvaNfaBuilder final {
         if (minN == 0) return BuildResult::fail();
         const bool hasMax = repp->maxCountp() != nullptr;
         const unsigned maxN = hasMax ? getConstUInt(repp->maxCountp()) : minN;
-        if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError();
-
         if (m_isCoverSeq) {
-            // Several matches may wait across false cycles, but the NFA stores only one bit for
+            // Several matches may wait across false cycles, but the ring stores only one bit for
             // them, so a cover sequence action block could run too few times.
             warnEndpointUnsupported(flp, "a goto repetition");
             return BuildResult::failWithError();
         }
 
-        // Wait + match per iter -> 2 sites per iteration; range form needs
-        // sites for every iteration in [0..maxN). NOT($sampled(x)) matches
-        // $sampled(NOT(x)) at the value level (IEEE 1800-2023 16.9.9);
-        // purity is enforced uniformly via cloneTreePure inside sampledRefOrClone.
-        AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2U * maxN);
-        SvaStateVertex* currentp = entryVtxp;
-        // Build minN match-wait chains to reach the first accept point.
-        for (unsigned i = 0; i < minN; ++i) {
-            SvaStateVertex* const waitVtxp = scopedCreateVertex();
-            // Edge (not Link) for all iterations: IEEE expansion ##1 before each
-            // match. A Link at i==0 was wrong -- it allowed same-cycle matching
-            // and was discarded by Phase 2 (waitNode has a self-loop Edge).
-            guardedEdge(currentp, waitVtxp, flp);
-            AstNodeExpr* const waitCondp
-                = new AstLogNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)};
-            guardedEdge(waitVtxp, waitVtxp, waitCondp, flp);
-            SvaStateVertex* const matchVtxp = scopedCreateVertex();
-            guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
-            currentp = matchVtxp;
+        AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2);
+
+        // The first guardedEdge is the ##1 before waiting for a match. In the wait state, false
+        // takes the clocked self-loop, while true takes the zero-delay guardedLink on that tick.
+        SvaStateVertex* const waitVtxp = scopedCreateVertex();
+        guardedEdge(entryVtxp, waitVtxp, flp);
+        guardedEdge(waitVtxp, waitVtxp,
+                    new AstLogNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)}, flp);
+        SvaStateVertex* currentp = scopedCreateVertex();
+        guardedLink(waitVtxp, currentp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
+
+        if (minN > 1) {
+            SvaStateVertex* const ringVtxp = addDelayChain(
+                currentp, minN - 1, flp, true, nullptr, sampledRefOrClone(hoistVarp, exprp, flp));
+            ringVtxp->m_replayAbortReject = true;
+            SvaStateVertex* const checkVtxp = scopedCreateVertex();
+            guardedLink(ringVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
+            currentp = checkVtxp;
         }
         if (!hasMax) {
             currentp->m_isUnbounded = true;  // [->N] waits unboundedly
             m_inUnboundedScope = true;
             return {currentp, nullptr, {}};
         }
-        // [->M:N]: every match in [M..N] feeds a shared merge vertex so the
-        // property can accept at any count in that range. Mirrors
-        // buildConsRep's range fan-out.
+
+        // [->M:N]: the range ring holds matches from M through N and advances
+        // only on expr, preserving arbitrarily long gaps between occurrences.
         SvaStateVertex* const mergeVtxp = scopedCreateVertex();
         guardedLink(currentp, mergeVtxp, flp);  // accept at match_M
-        for (unsigned i = minN; i < maxN; ++i) {
-            SvaStateVertex* const waitVtxp = scopedCreateVertex();
-            guardedEdge(currentp, waitVtxp, flp);
-            AstNodeExpr* const waitCondp
-                = new AstLogNot{flp, sampledRefOrClone(hoistVarp, exprp, flp)};
-            guardedEdge(waitVtxp, waitVtxp, waitCondp, flp);
-            SvaStateVertex* const matchVtxp = scopedCreateVertex();
-            guardedLink(waitVtxp, matchVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
-            guardedLink(matchVtxp, mergeVtxp, flp);  // accept at match_(i+1)
-            currentp = matchVtxp;
+        if (maxN > minN) {
+            SvaStateVertex* const ringVtxp
+                = addDelayChain(currentp, maxN - minN + 1, flp, false, nullptr,
+                                sampledRefOrClone(hoistVarp, exprp, flp));
+            ringVtxp->m_replayAbortReject = true;
+            SvaStateVertex* const checkVtxp = scopedCreateVertex();
+            guardedLink(ringVtxp, checkVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
+            guardedLink(checkVtxp, mergeVtxp, flp);
         }
         mergeVtxp->m_isUnbounded = true;  // [->M:N] still has unbounded waits between matches
         m_inUnboundedScope = true;
@@ -1428,10 +1448,18 @@ class SvaNfaBuilder final {
         return resultp;
     }
 
-    // True when a same-tick Link chain already accounts the attempt: a
-    // required-step Link covers both outcomes; followed-by pairs both edges.
+    // True when unguarded ring-wide rejection or a same-tick Link chain already accounts the
+    // attempt: a required-step Link covers both outcomes; followed-by pairs both edges.
     static bool chainAccountsSource(const SvaStateVertex* srcp,
                                     const std::unordered_set<const V3GraphEdge*>& preEdges) {
+        if (srcp->m_delayRingSize && srcp->m_throughoutConds.empty()) return true;
+        for (const V3GraphEdge& edger : srcp->inEdges()) {
+            if (preEdges.count(&edger)) continue;
+            const SvaTransEdge& tedger = static_cast<const SvaTransEdge&>(edger);
+            if (tedger.m_consumesCycle) continue;
+            const auto* const fromp = static_cast<const SvaStateVertex*>(tedger.fromVtxp());
+            if (fromp->m_abortRejectp) return true;
+        }
         bool plainNonSink = false;
         bool markedSink = false;
         for (const V3GraphEdge& edger : srcp->outEdges()) {
@@ -1443,6 +1471,7 @@ class SvaNfaBuilder final {
                 if (!sink) return true;
                 markedSink = true;
             } else if (!sink) {
+                if (srcp->m_abortRejectp) return true;
                 plainNonSink = true;
             }
         }
@@ -1504,11 +1533,18 @@ class SvaNfaBuilder final {
         for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) {
             if (preExisting.count(&vtxr)) continue;
             auto* const sp = static_cast<SvaStateVertex*>(&vtxr);
-            if (sp->m_delayRingSize) {
+            if (sp->m_delayRingSize || !sp->m_throughoutConds.empty()) {
                 AstNodeExpr* const firep = abortFireExpr(condp, flp);
                 sp->m_abortClearp
                     = sp->m_abortClearp ? new AstLogOr{flp, sp->m_abortClearp, firep} : firep;
             }
+            if (!kind.isAccept()
+                && ((sp->m_delayRingSize && sp->m_throughoutConds.empty())
+                    || sp->m_replayAbortReject)) {
+                AstNodeExpr* const firep = abortFireExpr(condp, flp);
+                sp->m_abortRejectp
+                    = sp->m_abortRejectp ? new AstLogOr{flp, sp->m_abortRejectp, firep} : firep;
+            }
             if (sp->m_isRejectSink) continue;
             abortSources.push_back(sp);
         }
@@ -1772,7 +1808,8 @@ class SvaNfaLowering final {
         const auto u32Const = [flp](uint32_t value) {
             return new AstConst{flp, AstConst::WidthedValue{}, 32, value};
         };
-        UASSERT(size > 1, "Delay ring index needs at least two slots");
+        UASSERT_OBJ(size > 0, idxp, "Ring size must be positive");
+        if (size == 1) return u32Const(0);
         // idx == size - 1 ? 0 : idx + 1
         AstAdd* const addp = new AstAdd{flp, new AstVarRef{flp, idxp, VAccess::READ}, u32Const(1)};
         addp->dtypeFrom(idxp);
@@ -1816,6 +1853,7 @@ class SvaNfaLowering final {
     // Phase 3 output signals
     struct SignalSet final {
         AstNodeExpr* terminalActivep = nullptr;  // OR of all successful terminal matches
+        AstNodeExpr* matchCountp = nullptr;  // NFA paths completing the sequence this tick
         AstNodeExpr* rejectBasep = nullptr;  // Reject when a terminal match fails
         AstNodeExpr* requiredStepRejectp = nullptr;  // Per-source reject from rejectOnFail Links
         AstNodeExpr* throughoutRejectp = nullptr;  // Reject when a throughout guard drops
@@ -1933,6 +1971,11 @@ class SvaNfaLowering final {
             updateBodyp->addNext(new AstAssignDly{c.flp,
                                                   new AstVarRef{c.flp, idxp, VAccess::WRITE},
                                                   nextRingIndex(c.flp, idxp, size)});
+            if (vtxp->m_delayRingAdvanceCondp) {
+                updateBodyp = new AstIf{
+                    c.flp, sampled(vtxp->m_delayRingAdvanceCondp->cloneTreePure(false)),
+                    updateBodyp};
+            }
 
             AstNodeExpr* clearCondp = killActive(c);
             if (vtxp->m_delayRingClearCondp) {
@@ -2040,11 +2083,10 @@ class SvaNfaLowering final {
     // throughout-drop reject; clean up intermediate state signals.
     // Phase 3: terminalActive and rejectBase from Links to matchVertex.
     // Builder only adds Links (non-clocked) to matchVertex via addLink in
-    // wireMatchAndMidSources. When outPerMidSrcsp is non-null, also collect
-    // the per-edge match signal (IEEE 1800-2023 16.14.3 cover sequence: each
-    // end-of-match fires the action independently, no OR-fold).
+    // wireMatchAndMidSources. For cover sequence, also count each end-of-match
+    // so the action can be replayed without unrolling endpoints.
     void computeTerminalMatchAndReject(LowerCtx& c, AstNodeExpr* snapshotOkp, SignalSet& sigs,
-                                       std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
+                                       const bool needMatchCount) {
         for (const SvaTransEdge* const tedgep : c.edges) {
             if (tedgep->toVtxp() != c.graph.m_matchVertexp) continue;
             const int fi = tedgep->fromVtxp()->color();
@@ -2056,17 +2098,20 @@ class SvaNfaLowering final {
             if (snapshotOkp) {
                 srcSigp = new AstLogAnd{c.flp, srcSigp, snapshotOkp->cloneTreePure(false)};
             }
-            if (outPerMidSrcsp) {
-                // Per-mid signal must also AND in matchCondp (the final boolean
-                // check, e.g. sampled(b) for `a ##[1:3] b`). assembleResult does
-                // this for the OR-collapsed terminalActivep; we replicate it
-                // per-edge here so each end-of-match is gated identically.
-                AstNodeExpr* perMidp = srcSigp->cloneTreePure(false);
-                if (c.matchCondp) {
-                    perMidp = new AstLogAnd{c.flp, perMidp,
-                                            sampled(c.matchCondp->cloneTreePure(false))};
+            if (needMatchCount) {
+                AstNodeExpr* contributionp = nullptr;
+                SvaStateVertex* const countRingp = tedgep->fromVtxp()->m_matchCountRingp;
+                if (countRingp) {
+                    AstVar* const liveCountVarp
+                        = c.vtx[countRingp->color()]->datap()->delayRingLiveCountVarp;
+                    contributionp = new AstCond{c.flp, srcSigp->cloneTreePure(false),
+                                                new AstVarRef{c.flp, liveCountVarp, VAccess::READ},
+                                                newTypedConstp(c.flp, liveCountVarp->dtypep(), 0)};
+                } else {
+                    contributionp = new AstExtend{c.flp, srcSigp->cloneTreePure(false),
+                                                  m_u32DTypep->width()};
                 }
-                outPerMidSrcsp->push_back(perMidp);
+                sigs.matchCountp = addThreadFailCountp(c.flp, sigs.matchCountp, contributionp);
             }
 
             if (tedgep->fromVtxp()->m_delayRingSize && !tedgep->fromVtxp()->m_isFixedDelayRing) {
@@ -2097,21 +2142,20 @@ class SvaNfaLowering final {
 
     AstNodeExpr* newThroughoutThreadFailCountp(LowerCtx& c, AstVar* const delayRingLiveCountVarp,
                                                AstNodeExpr* const stateExprp,
-                                               AstNodeExpr* const notGuardp) {
+                                               AstNodeExpr* const enablep) {
         AstNodeExpr* const activeThreadCountp
             = delayRingLiveCountVarp
                   ? static_cast<AstNodeExpr*>(
                         new AstVarRef{c.flp, delayRingLiveCountVarp, VAccess::READ})
                   : new AstExtend{c.flp, stateExprp->cloneTreePure(false), m_u32DTypep->width()};
-        return addThreadFailCountp(c.flp, nullptr, activeThreadCountp,
-                                   notGuardp->cloneTreePure(false));
+        return addThreadFailCountp(c.flp, nullptr, activeThreadCountp, enablep);
     }
 
-    // Phase 3b: Throughout-drop rejection (IEEE 16.9.9).
+    // Phase 3b: Throughout-drop and ring-wide abort rejection.
     void computeThroughoutReject(LowerCtx& c, SignalSet& sigs, const bool needThreadFailCount) {
         for (int i = 0; i < c.N; ++i) {
             const auto& conds = c.vtx[i]->m_throughoutConds;
-            if (conds.empty()) continue;
+            if (conds.empty() && !c.vtx[i]->m_abortRejectp) continue;
             if (c.vtx[i]->m_isAndCombiner) continue;
             AstNodeExpr* stateExprp = nullptr;
             if (c.vtx[i]->datap()->stateVarp) {
@@ -2129,21 +2173,52 @@ class SvaNfaLowering final {
                 AstNodeExpr* const sp = sampled(cp->cloneTreePure(false));
                 guardp = guardp ? static_cast<AstNodeExpr*>(new AstLogAnd{c.flp, guardp, sp}) : sp;
             }
-            AstNodeExpr* const notGuardp = new AstLogNot{c.flp, guardp};
+            if (c.vtx[i]->m_abortRejectp) {
+                AstNodeExpr* const notAbortp = new AstLogNot{
+                    c.flp, sampled(c.vtx[i]->m_abortRejectp->cloneTreePure(false))};
+                guardp = guardp
+                             ? static_cast<AstNodeExpr*>(new AstLogAnd{c.flp, guardp, notAbortp})
+                             : notAbortp;
+            }
+            AstNodeExpr* rejectCondp = new AstLogNot{c.flp, guardp};
+            if (c.vtx[i]->m_abortClearp) {
+                // Any abort clears the ring. Accept aborts suppress a simultaneous guard failure;
+                // reject aborts are restored below so they still force rejection.
+                AstNodeExpr* const notAbortClearp
+                    = new AstLogNot{c.flp, sampled(c.vtx[i]->m_abortClearp->cloneTreePure(false))};
+                rejectCondp = new AstLogAnd{c.flp, rejectCondp, notAbortClearp};
+                if (c.vtx[i]->m_abortRejectp) {
+                    rejectCondp
+                        = new AstLogOr{c.flp, rejectCondp,
+                                       sampled(c.vtx[i]->m_abortRejectp->cloneTreePure(false))};
+                }
+            }
             if (needThreadFailCount) {
-                AstNodeExpr* const contributionp = newThroughoutThreadFailCountp(
-                    c, c.vtx[i]->datap()->delayRingLiveCountVarp, stateExprp, notGuardp);
+                AstNodeExpr* const contributionp
+                    = newThroughoutThreadFailCountp(c, c.vtx[i]->datap()->delayRingLiveCountVarp,
+                                                    stateExprp, rejectCondp->cloneTreePure(false));
                 sigs.threadFailCountp
                     = addThreadFailCountp(c.flp, sigs.threadFailCountp, contributionp);
+                if (c.vtx[i]->m_abortRejectp && c.vtx[i]->m_delayRingAdvanceCondp) {
+                    // An advancing ring thread also occupies its same-tick match vertex in the
+                    // unrolled NFA, so abort rejection must replay both fail actions.
+                    AstNodeExpr* const abortAndAdvancep = new AstLogAnd{
+                        c.flp, sampled(c.vtx[i]->m_abortRejectp->cloneTreePure(false)),
+                        sampled(c.vtx[i]->m_delayRingAdvanceCondp->cloneTreePure(false))};
+                    AstNodeExpr* const matchContributionp = newThroughoutThreadFailCountp(
+                        c, c.vtx[i]->datap()->delayRingLiveCountVarp, stateExprp,
+                        abortAndAdvancep);
+                    sigs.threadFailCountp
+                        = addThreadFailCountp(c.flp, sigs.threadFailCountp, matchContributionp);
+                }
             }
             sigs.throughoutRejectp = orExprs(c.flp, sigs.throughoutRejectp,
-                                             new AstLogAnd{c.flp, stateExprp, notGuardp});
+                                             new AstLogAnd{c.flp, stateExprp, rejectCondp});
         }
     }
 
     SignalSet computeSignals(LowerCtx& c, const bool needThreadFailCount,
-                             const bool needThroughoutThreadFailCount,
-                             std::vector<AstNodeExpr*>* outPerMidSrcsp = nullptr) {
+                             const bool needThroughoutThreadFailCount, const bool needMatchCount) {
         SignalSet sigs;
 
         // Snapshot comparison expression for disable-iff counter.
@@ -2155,7 +2230,7 @@ class SvaNfaLowering final {
                                     new AstVarRef{c.flp, c.disableCntVarp, VAccess::READ}};
         }
 
-        computeTerminalMatchAndReject(c, snapshotOkp, sigs, outPerMidSrcsp);
+        computeTerminalMatchAndReject(c, snapshotOkp, sigs, needMatchCount);
 
         // Phase 3a: required-step rejection.
         // Builder only sets m_rejectOnFail on non-clocked Links with m_condp
@@ -2196,6 +2271,14 @@ class SvaNfaLowering final {
             sigs.threadFailCountp
                 = addThreadFailCountp(c.flp, nullptr, sigs.threadFailCountp, notKillActive(c));
         }
+        if (sigs.matchCountp) {
+            if (c.matchCondp) {
+                sigs.matchCountp = addThreadFailCountp(
+                    c.flp, nullptr, sigs.matchCountp, sampled(c.matchCondp->cloneTreePure(false)));
+            }
+            sigs.matchCountp
+                = addThreadFailCountp(c.flp, nullptr, sigs.matchCountp, notKillActive(c));
+        }
         sigs.terminalActivep = gateNotKill(c, sigs.terminalActivep);
         sigs.rejectBasep = gateNotKill(c, sigs.rejectBasep);
         sigs.throughoutRejectp = gateNotKill(c, sigs.throughoutRejectp);
@@ -2229,6 +2312,11 @@ class SvaNfaLowering final {
                     = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
                 sigs.requiredStepRejectp = new AstLogAnd{c.flp, sigs.requiredStepRejectp, notDisp};
             }
+            if (sigs.matchCountp) {
+                sigs.matchCountp = addThreadFailCountp(
+                    c.flp, nullptr, sigs.matchCountp,
+                    new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)});
+            }
         }
 
         if (snapshotOkp) {
@@ -2257,16 +2345,13 @@ 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.
+        // Fixed-point propagation along zero-delay (Link) edges. Rebuild each
+        // derived signal from its incoming edges on every pass; appending the same
+        // contributions repeatedly makes merge expressions grow exponentially.
         for (int pass = 0; pass < 2 * c.N + 2; ++pass) {
-            bool changed = false;
-            // Seed SAnd combiners (sub-NFA termVertices may only be available
-            // after a propagation pass).
+            // Rebuild SAnd combiners once both sub-NFA terminals are available.
             for (int i = 0; i < c.N; ++i) {
                 if (!c.vtx[i]->m_isAndCombiner) continue;
-                if (c.vtx[i]->datap()->stateSigp) continue;
                 // AndCombiner vertices always have both terminal pointers set.
                 UASSERT_OBJ(c.vtx[i]->m_andLhsTermp && c.vtx[i]->m_andRhsTermp, c.vtx[i],
                             "AndCombiner vertex missing LHS/RHS terminal");
@@ -2286,33 +2371,34 @@ class SvaNfaLowering final {
                 AstNodeExpr* const bothp = new AstLogAnd{c.flp, doneLOrp, doneROrp};
                 AstNodeExpr* const oneNowp = new AstLogOr{c.flp, matchLp->cloneTreePure(false),
                                                           matchRp->cloneTreePure(false)};
-                c.vtx[i]->datap()->stateSigp = new AstLogAnd{c.flp, bothp, oneNowp};
-                changed = true;
-            }
-            // Propagate Link edges
-            for (int fi = 0; fi < c.N; ++fi) {
-                if (!c.vtx[fi]->datap()->stateSigp) continue;
-                for (const V3GraphEdge& edger : c.vtx[fi]->outEdges()) {
-                    const SvaTransEdge& tedger = static_cast<const SvaTransEdge&>(edger);
-                    if (tedger.m_consumesCycle) continue;
-                    const int ti = tedger.toVtxp()->color();
-                    if (tedger.toVtxp()->m_isMatch || tedger.toVtxp()->m_isRejectSink) continue;
-                    AstNodeExpr* const contributionp
-                        = andCond(c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false),
-                                  tedger.m_condp);
-                    if (!c.vtx[ti]->datap()->stateSigp) {
-                        c.vtx[ti]->datap()->stateSigp = contributionp;
-                        changed = true;
-                    } else if (!c.vtx[ti]->datap()->needsReg) {
-                        c.vtx[ti]->datap()->stateSigp
-                            = orExprs(c.flp, c.vtx[ti]->datap()->stateSigp, contributionp);
-                        changed = true;
-                    } else {
-                        VL_DO_DANGLING(contributionp->deleteTree(), contributionp);
-                    }
+                if (c.vtx[i]->datap()->stateSigp) {
+                    VL_DO_DANGLING(c.vtx[i]->datap()->stateSigp->deleteTree(),
+                                   c.vtx[i]->datap()->stateSigp);
                 }
+                c.vtx[i]->datap()->stateSigp = new AstLogAnd{c.flp, bothp, oneNowp};
+            }
+
+            for (int ti = 0; ti < c.N; ++ti) {
+                if (ti == c.startIdx || c.vtx[ti]->datap()->stateVarp
+                    || c.vtx[ti]->datap()->delayRingVarp || c.vtx[ti]->m_isAndCombiner
+                    || c.vtx[ti]->m_isMatch || c.vtx[ti]->m_isRejectSink) {
+                    continue;
+                }
+                AstNodeExpr* nextStatep = nullptr;
+                for (const V3GraphEdge& er : c.vtx[ti]->inEdges()) {
+                    const SvaTransEdge& te = static_cast<const SvaTransEdge&>(er);
+                    const int fi = te.fromVtxp()->color();
+                    if (!c.vtx[fi]->datap()->stateSigp) continue;
+                    AstNodeExpr* const contributionp = andCond(
+                        c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false), te.m_condp);
+                    nextStatep = orExprs(c.flp, nextStatep, contributionp);
+                }
+                if (c.vtx[ti]->datap()->stateSigp) {
+                    VL_DO_DANGLING(c.vtx[ti]->datap()->stateSigp->deleteTree(),
+                                   c.vtx[ti]->datap()->stateSigp);
+                }
+                c.vtx[ti]->datap()->stateSigp = nextStatep;
             }
-            if (!changed) break;
         }
     }
 
@@ -2424,8 +2510,7 @@ public:
                     AstSenTree* const senTreep, AstNodeExpr* const matchCondp,
                     AstNodeExpr* const disableExprp, AstVar* const disableCntVarp,
                     AstVar* const snapshotVarp, const bool needThreadFailCount,
-                    const bool needThroughoutThreadFailCount,
-                    std::vector<AstNodeExpr*>* const outPerMidSrcsp) {
+                    const bool needThroughoutThreadFailCount) {
         FileLine* const flp = assertp->fileline();
         AstCover* const coverp = VN_CAST(assertp, Cover);
         const bool isSeqEvent = coverp && coverp->isSeqEvent();
@@ -2543,8 +2628,8 @@ public:
         emitKillAckNba(c);
 
         // Phase 3/3a/3b: Compute terminal match/reject signals (cleans up stateSig).
-        const SignalSet sigs = computeSignals(c, needThreadFailCount,
-                                              needThroughoutThreadFailCount, outPerMidSrcsp);
+        const SignalSet sigs = computeSignals(
+            c, needThreadFailCount, needThroughoutThreadFailCount, coverp && coverp->isCoverSeq());
 
         // Strong s_always[m:n] end-of-simulation liveness: if any in-window state
         // is still set at $finish, the universal-quantifier window never completed
@@ -3259,19 +3344,19 @@ class AssertNfaVisitor final : public VNVisitor {
 
         const bool needsThreadFailReplay
             = assertAssertp && assertAssertp->failsp() && !parts.hasImplication;
-        // For `cover sequence` (IEEE 1800-2023 16.14.3) collect per-edge match
-        // signals so each end-of-match fires the action independently, rather
-        // than getting OR-folded into a single per-cycle terminalActive.
-        // coverp / isCoverSeq are computed earlier (passed to SvaNfaBuilder).
-        std::vector<AstNodeExpr*> perMidSrcs;
-
         const auto signals = m_loweringp->lower(
             assertp, graph, senTreep, result.finalCondp, disableExprp, disableCntVarp,
-            snapshotVarp, needsThreadFailReplay, needsThreadFailReplay && !negated,
-            isCoverSeq ? &perMidSrcs : nullptr);
+            snapshotVarp, needsThreadFailReplay, needsThreadFailReplay && !negated);
         AstNodeExpr* matchExprp = nullptr;
-        AstNodeExpr* const outputExprp = m_loweringp->assembleResult(
+        AstNodeExpr* outputExprp = m_loweringp->assembleResult(
             assertp, negated, result.finalCondp, signals, needMatch ? &matchExprp : nullptr);
+        if (isCoverSeq) {
+            UASSERT_OBJ(signals.matchCountp, coverp, "Cover sequence missing match count");
+            VL_DO_DANGLING(outputExprp->deleteTree(), outputExprp);
+            propp->matchCountp(signals.matchCountp);
+            outputExprp = new AstNeq{flp, signals.matchCountp->cloneTreePure(false),
+                                     newTypedConstp(flp, signals.matchCountp->dtypep(), 0)};
+        }
 
         AstSenTree* const threadFailReplaySenTreep
             = signals.threadFailCountp ? senTreep->cloneTree(false) : nullptr;
@@ -3287,38 +3372,9 @@ class AssertNfaVisitor final : public VNVisitor {
                                  signals.threadFailCountp);
         }
 
-        if (isCoverSeq && perMidSrcs.size() > 1) {
-            // Clone AstCover (N-1) times, each gated by its own per-mid signal.
-            // V3Assert sees N independent covers and emits N `if (cond_i) {coverinc;
-            // userAction}` bodies; the shared AstCoverDecl bucket is incremented
-            // per fire, matching IEEE "executed each time the sequence matches."
-            // Clones reuse AstCover->propp's original SVA tree, but we overwrite
-            // each clone's inner propp with the corresponding per-mid signal
-            // BEFORE the next iterator step, so hasMultiCycleExpr() returns false
-            // and processAssertion skips them on revisit.
-            std::vector<AstCover*> coverList;
-            coverList.push_back(coverp);
-            for (size_t i = 1; i < perMidSrcs.size(); ++i) {
-                AstCover* const clonep = coverp->cloneTree(false);
-                coverp->addNextHere(clonep);
-                coverList.push_back(clonep);
-            }
-            for (size_t i = 0; i < perMidSrcs.size(); ++i) {
-                AstPropSpec* const clonePropSpecp = VN_CAST(coverList[i]->propp(), PropSpec);
-                AstNode* const innerp = clonePropSpecp->propp();
-                innerp->replaceWith(perMidSrcs[i]);
-                VL_DO_DANGLING(pushDeletep(innerp), innerp);
-            }
-            // Discard the OR-collapsed fallback signal -- cover_sequence path
-            // does not use it.
-            VL_DO_DANGLING(outputExprp->deleteTree(), outputExprp);
-        } else {
-            AstNode* const innerPropp = propp->propp();
-            innerPropp->replaceWith(outputExprp);
-            VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
-            // If we collected per-mid (N==1) but didn't clone, drop the spare.
-            for (AstNodeExpr* const sp : perMidSrcs) pushDeletep(sp);
-        }
+        AstNode* const innerPropp = propp->propp();
+        innerPropp->replaceWith(outputExprp);
+        VL_DO_DANGLING(pushDeletep(innerPropp), innerPropp);
 
         UINFO(4, "NFA converted assertion at " << flp << endl);