Implement delay chains in the NFA using bit-vector ring buffers with O(1) operations

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

src/V3AssertNfa.cpp

@@ -48,8 +48,8 @@ class SvaStateVertex;
 // Per-vertex algorithm data, stored via V3GraphVertex::userp() during lowering
 struct SvaVertexData final {
     AstVar* stateVarp = nullptr;  // NBA state register for this vertex
-    AstVar* counterActiveVarp = nullptr;  // Counter FSM active flag
+    AstVar* delayRingVarp = nullptr;  // Bitset ring buffer
-    AstVar* counterCountVarp = nullptr;  // Counter FSM count register
+    AstVar* delayRingIdxVarp = nullptr;  // Next slot written in delayRingVarp
     AstVar* doneLVarp = nullptr;  // SAnd LHS done-latch
     AstVar* doneRVarp = nullptr;  // SAnd RHS done-latch
     AstNodeExpr* stateSigp = nullptr;  // Combinational state signal (owned during lowering)
@@ -64,10 +64,10 @@ public:
     bool m_isMatch = false;
     // Owned throughout-guard condition clones; IEEE 1800-2023 16.9.9
     std::vector<AstNodeExpr*> m_throughoutConds;
-    // Counter FSM vertex for ##[M:N] when N-M > kChainLimit
+    // Nonzero for a bitset ring-buffer vertex for ## delays.
-    bool m_isCounter = false;
+    bool m_isFixedDelayRing = false;
-    int m_counterMax
+    int m_delayRingSize = 0;  // Fixed delay cycles. Range: max-min+1.
-        = 0;  // Counter window maximum (min is always 0; pre-chain handles the M offset)
+    AstNodeExpr* m_delayRingClearCondp = nullptr;  // local RHS for pure-boolean range
     // 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
@@ -88,15 +88,25 @@ public:
         : V3GraphVertex{graphp} {}
     ~SvaStateVertex() override {
         for (AstNodeExpr* cp : m_throughoutConds) VL_DO_DANGLING(cp->deleteTree(), cp);
+        if (m_delayRingClearCondp)
+            VL_DO_DANGLING(m_delayRingClearCondp->deleteTree(), m_delayRingClearCondp);
         if (m_andLhsCondp) VL_DO_DANGLING(m_andLhsCondp->deleteTree(), m_andLhsCondp);
         if (m_andRhsCondp) VL_DO_DANGLING(m_andRhsCondp->deleteTree(), m_andRhsCondp);
     }
     // METHODS
-    string name() const override { return "s" + cvtToStr(color()); }  // LCOV_EXCL_LINE
     // LCOV_EXCL_START -- Graphviz dump only
+    string name() const override {
+        string name = "s" + cvtToStr(color());
+        if (m_delayRingSize) {
+            name += "\\n";
+            name += m_isFixedDelayRing ? "fixed chain " : "range chain ";
+            name += cvtToStr(m_delayRingSize) + " bits";
+        }
+        return name;
+    }
     string dotColor() const override {
         if (m_isMatch) return "red";
-        if (m_isCounter) return "blue";
+        if (m_delayRingSize) return "blue";
         if (m_isAndCombiner) return "purple";
         return "black";
     }
@@ -513,14 +523,28 @@ class SvaNfaBuilder final {
         return m_graph.addClockedEdge(fromp, top, throughoutCond(nullptr, flp));
     }
 
-    SvaStateVertex* addDelayChain(SvaStateVertex* startp, int n, FileLine* flp) {
+    SvaStateVertex* addDelayChain(SvaStateVertex* startp, int size, FileLine* flp,
-        SvaStateVertex* currentp = startp;
+                                  bool isFixed = true, AstNodeExpr* clearCondp = nullptr) {
-        for (int i = 0; i < n; ++i) {
+        if (isFixed && size == 0) return startp;
+        UASSERT_OBJ(size > 0, startp, "Delay chain needs at least one slot");
+        if (isFixed && size == 1) {
             SvaStateVertex* const nextp = scopedCreateVertex();
-            guardedEdge(currentp, nextp, flp);
+            guardedEdge(startp, nextp, flp);
-            currentp = nextp;
+            return nextp;
         }
-        return currentp;
+        SvaStateVertex* const ringVtxp = scopedCreateVertex();
+        ringVtxp->m_isFixedDelayRing = isFixed;
+        ringVtxp->m_delayRingSize = size;
+        if (clearCondp) {
+            UASSERT_OBJ(!isFixed, startp, "Fixed delay cannot have a clear condition");
+            ringVtxp->m_delayRingClearCondp = clearCondp->cloneTreePure(false);
+        }
+        if (isFixed) {
+            guardedEdge(startp, ringVtxp, flp);
+        } else {
+            guardedLink(startp, ringVtxp, flp);
+        }
+        return ringVtxp;
     }
 
     // Build NFA for an SExpr. finalCond = RHS (not yet added as a vertex).
@@ -565,7 +589,7 @@ class SvaNfaBuilder final {
         const int range = maxDelay - minDelay;
         currentp = addDelayChain(currentp, minDelay, flp);
         // kChainLimit bounds per-attempt unrolled vertices. Above this, a
-        // counter FSM (constant-size state) is used instead, so the vertex
+        // ring buffer (constant-size state) is used instead, so the vertex
         // count is O(1) in range regardless of user input; no adversarial N
         // blowup is possible.
         constexpr int kChainLimit = 256;
@@ -580,13 +604,8 @@ class SvaNfaBuilder final {
             return false;
         }
         if (range > kChainLimit) {
-            // Large range: counter FSM. Overlapping triggers during an active
+            currentp = addDelayChain(currentp, range + 1, flp, false,
-            // count are dropped (non-overlapping semantics only).
+                                     rhsExprp->isMultiCycleSva() ? nullptr : rhsExprp);
-            SvaStateVertex* const counterVtxp = scopedCreateVertex();
-            counterVtxp->m_isCounter = true;
-            counterVtxp->m_counterMax = range;
-            guardedEdge(currentp, counterVtxp, flp);
-            currentp = counterVtxp;
         } else if (VN_IS(rhsExprp, SExpr)) {
             // Nested-SExpr RHS: merge all [M,N] positions. Candidate-local misses
             // are not assertion rejects while a later position can still match.
@@ -1640,6 +1659,25 @@ class SvaNfaLowering final {
         if (!exprp) return nullptr;
         return new AstLogAnd{c.flp, exprp, notKillActive(c)};
     }
+    static AstNodeExpr* nextRingIndex(FileLine* flp, AstVar* idxp, uint32_t size) {
+        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");
+        // idx == size - 1 ? 0 : idx + 1
+        AstAdd* const addp = new AstAdd{flp, new AstVarRef{flp, idxp, VAccess::READ}, u32Const(1)};
+        addp->dtypeFrom(idxp);
+        AstCond* const condp = new AstCond{
+            flp, new AstEq{flp, new AstVarRef{flp, idxp, VAccess::READ}, u32Const(size - 1)},
+            u32Const(0), addp};
+        condp->dtypeFrom(idxp);
+        return condp;
+    }
+    static AstNodeExpr* delayRingBit(FileLine* flp, AstVar* ringp, AstNodeExpr* idxExprp,
+                                     VAccess access = VAccess::READ) {
+        // ring[idx]
+        return new AstSel{flp, new AstVarRef{flp, ringp, access}, idxExprp, 1};
+    }
 
     // Phase 3 output signals
     struct SignalSet final {
@@ -1650,12 +1688,14 @@ class SvaNfaLowering final {
     };
 
     // Phase 2/2b/2c: Emit NBA state-update always blocks for registered vertices,
-    // counter FSMs, and SAnd combiner done-latches.
+    // delay rings, and SAnd combiner done-latches.
     // Phase 2: State register NBA always block. Each clocked-edge target
     // latches the OR of its incoming contributions.
     void emitStateRegisterNba(LowerCtx& c) {
         AstNode* bodyp = nullptr;
+        bool hasDelayRing = false;
         for (int i = 0; i < c.N; ++i) {
+            if (c.vtx[i]->datap()->delayRingVarp) hasDelayRing = true;
             if (!c.vtx[i]->datap()->stateVarp) continue;
 
             AstNodeExpr* nextStatep = nullptr;
@@ -1684,100 +1724,104 @@ class SvaNfaLowering final {
             AstAssignDly* const assignp = new AstAssignDly{
                 c.flp, new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::WRITE},
                 nextStatep};
-            if (!bodyp) {
+            bodyp = AstNode::addNextNull(bodyp, assignp);
-                bodyp = assignp;
-            } else {
-                bodyp->addNext(assignp);
-            }
         }
 
-        if (!bodyp) return;
         // Capture disableCnt in Phase-2 NBA before any reactive re-evaluation.
         // snapshotVarp and disableCntVarp are allocated together.
-        if (c.snapshotVarp) {
+        if (c.snapshotVarp && (bodyp || hasDelayRing)) {
             UASSERT_OBJ(c.disableCntVarp, c.senTreep, "snapshotVarp set without disableCntVarp");
-            bodyp->addNext(
+            // disable_snapshot <= disable_count;
-                new AstAssignDly{c.flp, new AstVarRef{c.flp, c.snapshotVarp, VAccess::WRITE},
+            AstAssignDly* const snapshotp
-                                 new AstVarRef{c.flp, c.disableCntVarp, VAccess::READ}});
+                = new AstAssignDly{c.flp, new AstVarRef{c.flp, c.snapshotVarp, VAccess::WRITE},
+                                   new AstVarRef{c.flp, c.disableCntVarp, VAccess::READ}};
+            bodyp = AstNode::addNextNull(bodyp, snapshotp);
         }
+        if (!bodyp) return;
         m_modp->addStmtsp(
             new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), bodyp});
     }
 
-    // Phase 2b: Counter FSM always block.
+    // Phase 2b: Bitset ring-buffer delay always block.
-    // if (active) { if (done) active<=0; else counter<=counter+1; }
+    void emitDelayRingNba(LowerCtx& c) {
-    // else if (incoming) { active<=1; counter<=0; }
+        for (int ri = 0; ri < c.N; ++ri) {
-    void emitCounterFsmNba(LowerCtx& c) {
+            SvaStateVertex* const vtxp = c.vtx[ri];
-        for (int ci = 0; ci < c.N; ++ci) {
+            if (!vtxp->datap()->delayRingVarp) continue;
-            if (!c.vtx[ci]->datap()->counterActiveVarp) continue;
+            AstVar* const ringp = vtxp->datap()->delayRingVarp;
-            AstVar* const activep = c.vtx[ci]->datap()->counterActiveVarp;
+            AstVar* const idxp = vtxp->datap()->delayRingIdxVarp;
-            AstVar* const cntp = c.vtx[ci]->datap()->counterCountVarp;
+            const uint32_t size = static_cast<uint32_t>(vtxp->m_delayRingSize);
-            const uint32_t counterMax = static_cast<uint32_t>(c.vtx[ci]->m_counterMax);
 
-            // Builder only adds clocked edges to counter vertices (guardedEdge
-            // in buildSExpr), so m_consumesCycle is always true here.
             AstNodeExpr* incomingp = nullptr;
             for (const SvaTransEdge* const tep : c.edges) {
-                const int toIdx = tep->toVtxp()->color();
+                if (static_cast<int>(tep->toVtxp()->color()) != ri) continue;
-                if (toIdx != ci) continue;
+                UASSERT_OBJ(tep->m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp,
+                            "Delay-ring incoming edge kind mismatch");
                 const int fi = tep->fromVtxp()->color();
                 UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, c.vtx[fi],
-                            "Clocked edge source missing stateSig");
+                            "Delay-ring incoming source missing stateSig");
                 AstNodeExpr* contribp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false);
                 contribp = andCond(c.flp, contribp, tep->m_condp);
-                if (c.disableExprp) {
+                if (c.disableExprp && !c.snapshotVarp) {
                     AstNodeExpr* const notDisp
                         = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)};
                     contribp = new AstLogAnd{c.flp, contribp, notDisp};
                 }
                 incomingp = orExprs(c.flp, incomingp, contribp);
             }
-            UASSERT_OBJ(incomingp, c.vtx[ci], "Counter vertex has no incoming contribution");
+            UASSERT_OBJ(incomingp, vtxp, "Delay ring has no incoming edge");
-
+            AstNode* updateBodyp = nullptr;
-            // Counter window is always [0, m_counterMax]; M offset is handled by
+            if (vtxp->m_isFixedDelayRing) {
-            // the pre-chain in buildSExpr, so every tick inside an active count
+                // ring[idx] <= incoming;
-            // is in-window.
+                updateBodyp = new AstAssignDly{
-            AstNodeExpr* inWindowp = new AstConst{c.flp, AstConst::BitTrue{}};
+                    c.flp,
-            AstNodeExpr* matchedNowp = nullptr;
+                    delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ},
-            if (c.matchCondp) {
+                                 VAccess::WRITE),
-                matchedNowp
+                    incomingp};
-                    = new AstLogAnd{c.flp, inWindowp, sampled(c.matchCondp->cloneTreePure(false))};
+            } else {
-            } else {  // LCOV_EXCL_LINE -- no counter-FSM caller leaves matchCondp null
+                // ring[next_idx] <= 1'b0; ring[idx] <= incoming;
-                matchedNowp = inWindowp;  // LCOV_EXCL_LINE
+                AstAssignDly* const clearExpirep = new AstAssignDly{
+                    c.flp,
+                    delayRingBit(c.flp, ringp, nextRingIndex(c.flp, idxp, size), VAccess::WRITE),
+                    new AstConst{c.flp, AstConst::BitFalse{}}};
+                AstAssignDly* const writeIncomingp = new AstAssignDly{
+                    c.flp,
+                    delayRingBit(c.flp, ringp, new AstVarRef{c.flp, idxp, VAccess::READ},
+                                 VAccess::WRITE),
+                    incomingp};
+                clearExpirep->addNext(writeIncomingp);
+                updateBodyp = clearExpirep;
             }
 
-            AstNodeExpr* const counterAtEndp
+            AstNodeExpr* clearCondp = nullptr;
-                = new AstEq{c.flp, new AstVarRef{c.flp, cntp, VAccess::READ},
+            if (vtxp->m_delayRingClearCondp) {
-                            new AstConst{c.flp, AstConst::WidthedValue{}, 32, counterMax}};
+                clearCondp = sampled(vtxp->m_delayRingClearCondp->cloneTreePure(false));
+            }
+            if (c.disableExprp && !c.snapshotVarp) {
+                clearCondp = orExprs(c.flp, clearCondp, c.disableExprp->cloneTreePure(false));
+            }
+            AstNodeExpr* guardp = nullptr;
+            for (AstNodeExpr* const cp : vtxp->m_throughoutConds) {
+                AstNodeExpr* const sampledp = sampled(cp->cloneTreePure(false));
+                guardp = guardp ? static_cast<AstNodeExpr*>(new AstLogAnd{c.flp, guardp, sampledp})
+                                : sampledp;
+            }
+            if (guardp) clearCondp = orExprs(c.flp, clearCondp, new AstLogNot{c.flp, guardp});
+            if (clearCondp) {
+                // if (clear) ring <= '0;
+                AstConst* const zerop = new AstConst{c.flp, AstConst::DTyped{}, ringp->dtypep()};
+                zerop->num().setAllBits0();
+                updateBodyp = new AstIf{
+                    c.flp, clearCondp,
+                    new AstAssignDly{c.flp, new AstVarRef{c.flp, ringp, VAccess::WRITE}, zerop},
+                    updateBodyp};
+            }
+            // idx <= next_idx;
+            updateBodyp->addNext(new AstAssignDly{c.flp,
+                                                  new AstVarRef{c.flp, idxp, VAccess::WRITE},
+                                                  nextRingIndex(c.flp, idxp, size)});
 
-            AstNodeExpr* const donep = new AstLogOr{
+            m_modp->addStmtsp(new AstAlways{c.flp, VAlwaysKwd::ALWAYS,
-                c.flp, killActive(c), new AstLogOr{c.flp, matchedNowp, counterAtEndp}};
+                                            c.senTreep->cloneTree(false), updateBodyp});
-
-            AstAssignDly* const clearActivep
-                = new AstAssignDly{c.flp, new AstVarRef{c.flp, activep, VAccess::WRITE},
-                                   new AstConst{c.flp, AstConst::BitFalse{}}};
-            AstAdd* const addExprp
-                = new AstAdd{c.flp, new AstVarRef{c.flp, cntp, VAccess::READ},
-                             new AstConst{c.flp, AstConst::WidthedValue{}, 32, 1u}};
-            addExprp->dtypeFrom(cntp);
-            AstAssignDly* const incCountp
-                = new AstAssignDly{c.flp, new AstVarRef{c.flp, cntp, VAccess::WRITE}, addExprp};
-            AstIf* const doneIfp = new AstIf{c.flp, donep, clearActivep, incCountp};
-
-            AstAssignDly* const setActivep
-                = new AstAssignDly{c.flp, new AstVarRef{c.flp, activep, VAccess::WRITE},
-                                   new AstConst{c.flp, AstConst::BitTrue{}}};
-            AstAssignDly* const resetCountp
-                = new AstAssignDly{c.flp, new AstVarRef{c.flp, cntp, VAccess::WRITE},
-                                   new AstConst{c.flp, AstConst::WidthedValue{}, 32, 0u}};
-            setActivep->addNext(resetCountp);
-            AstIf* const startIfp
-                = new AstIf{c.flp, gateNotKill(c, incomingp), setActivep, nullptr};
-            AstIf* const topIfp = new AstIf{c.flp, new AstVarRef{c.flp, activep, VAccess::READ},
-                                            doneIfp, startIfp};
-
-            m_modp->addStmtsp(
-                new AstAlways{c.flp, VAlwaysKwd::ALWAYS, c.senTreep->cloneTree(false), topIfp});
         }
     }
 
@@ -1880,16 +1924,22 @@ class SvaNfaLowering final {
                 outPerMidSrcsp->push_back(perMidp);
             }
 
-            if (tep->fromVtxp()->m_isCounter) {
+            if (tep->fromVtxp()->m_delayRingSize && !tep->fromVtxp()->m_isFixedDelayRing) {
                 sigs.terminalActivep
                     = orExprs(c.flp, sigs.terminalActivep, srcSigp->cloneTreePure(false));
-                AstNodeExpr* const atEndp = new AstEq{
+                AstVar* const ringp = c.vtx[fi]->datap()->delayRingVarp;
-                    c.flp,
+                AstVar* const idxp = c.vtx[fi]->datap()->delayRingIdxVarp;
-                    new AstVarRef{c.flp, c.vtx[fi]->datap()->counterCountVarp, VAccess::READ},
+                const uint32_t size = static_cast<uint32_t>(c.vtx[fi]->m_delayRingSize);
-                    new AstConst{c.flp, AstConst::WidthedValue{}, 32,
+                // reject |= ring[next_idx] && final_condition;
-                                 static_cast<uint32_t>(tep->fromVtxp()->m_counterMax)}};
+                AstNodeExpr* expireContribp
-                AstNodeExpr* const expireContribp = new AstLogAnd{c.flp, srcSigp, atEndp};
+                    = delayRingBit(c.flp, ringp, nextRingIndex(c.flp, idxp, size));
+                expireContribp = andCond(c.flp, expireContribp, tep->m_condp);
+                if (snapshotOkp) {
+                    expireContribp
+                        = new AstLogAnd{c.flp, expireContribp, snapshotOkp->cloneTreePure(false)};
+                }
                 sigs.rejectBasep = orExprs(c.flp, sigs.rejectBasep, expireContribp);
+                VL_DO_DANGLING(srcSigp->deleteTree(), srcSigp);
             } else if (tep->fromVtxp()->m_isUnbounded || tep->fromVtxp()->m_isAndCombiner) {
                 sigs.terminalActivep = orExprs(c.flp, sigs.terminalActivep, srcSigp);
             } else {
@@ -1913,6 +1963,10 @@ class SvaNfaLowering final {
             AstNodeExpr* stateExprp = nullptr;
             if (c.vtx[i]->datap()->stateVarp) {
                 stateExprp = new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::READ};
+            } else if (c.vtx[i]->datap()->delayRingVarp && c.vtx[i]->m_isFixedDelayRing) {
+                // fixed_chain_active = |ring;
+                stateExprp = new AstRedOr{
+                    c.flp, new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingVarp, VAccess::READ}};
             } else {
                 UASSERT_OBJ(c.vtx[i]->datap()->stateSigp, c.vtx[i],
                             "Throughout-conds vertex missing state representation");
@@ -2027,10 +2081,18 @@ class SvaNfaLowering final {
             if (c.vtx[i]->datap()->stateVarp) {
                 c.vtx[i]->datap()->stateSigp
                     = new AstVarRef{c.flp, c.vtx[i]->datap()->stateVarp, VAccess::READ};
-            } else if (c.vtx[i]->datap()->counterActiveVarp) {
+            } else if (c.vtx[i]->datap()->delayRingVarp) {
-                // Counter window is always [0, m_counterMax]; see buildSExpr.
+                if (c.vtx[i]->m_isFixedDelayRing) {
-                c.vtx[i]->datap()->stateSigp
+                    // state = ring[idx];
-                    = new AstVarRef{c.flp, c.vtx[i]->datap()->counterActiveVarp, VAccess::READ};
+                    c.vtx[i]->datap()->stateSigp = delayRingBit(
+                        c.flp, c.vtx[i]->datap()->delayRingVarp,
+                        new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingIdxVarp, VAccess::READ});
+                } else {
+                    // state = |ring;
+                    c.vtx[i]->datap()->stateSigp = new AstRedOr{
+                        c.flp,
+                        new AstVarRef{c.flp, c.vtx[i]->datap()->delayRingVarp, VAccess::READ}};
+                }
             }
         }
         // Fixed-point propagation along zero-delay (Link) edges.
@@ -2247,18 +2309,22 @@ public:
                 vtx[i]->datap()->doneRVarp = rp;
                 continue;
             }
-            if (vtx[i]->m_isCounter) {
+            if (vtx[i]->m_delayRingSize) {
-                const std::string base = baseName + "__c" + std::to_string(i);
+                const std::string base = baseName + "__d" + std::to_string(i);
-                AstVar* const activep = new AstVar{flp, VVarType::MODULETEMP, base + "_active",
+                // bit [size-1:0] ring;
-                                                   m_modp->findBitDType()};
+                AstNodeDType* const ringDTypep = m_modp->findBitDType(
-                activep->lifetime(VLifetime::STATIC_EXPLICIT);
+                    vtx[i]->m_delayRingSize, vtx[i]->m_delayRingSize, VSigning::UNSIGNED);
-                m_modp->addStmtsp(activep);
+                AstVar* const ringp
-                vtx[i]->datap()->counterActiveVarp = activep;
+                    = new AstVar{flp, VVarType::MODULETEMP, base + "_ring", ringDTypep};
-                AstVar* const cntp
+                ringp->lifetime(VLifetime::STATIC_EXPLICIT);
-                    = new AstVar{flp, VVarType::MODULETEMP, base + "_cnt", u32DTypep};
+                m_modp->addStmtsp(ringp);
-                cntp->lifetime(VLifetime::STATIC_EXPLICIT);
+                vtx[i]->datap()->delayRingVarp = ringp;
-                m_modp->addStmtsp(cntp);
+                // int unsigned idx;
-                vtx[i]->datap()->counterCountVarp = cntp;
+                AstVar* const idxp
+                    = new AstVar{flp, VVarType::MODULETEMP, base + "_idx", u32DTypep};
+                idxp->lifetime(VLifetime::STATIC_EXPLICIT);
+                m_modp->addStmtsp(idxp);
+                vtx[i]->datap()->delayRingIdxVarp = idxp;
                 continue;
             }
             if (!vtx[i]->datap()->needsReg) continue;
@@ -2279,9 +2345,9 @@ public:
         // Phase 1: Resolve combinational Links via fixed-point propagation.
         resolveLinks(c, triggerExprp);
 
-        // Phase 2/2b/2c: Emit NBA state-update, counter FSM, and SAnd done-latch logic.
+        // Phase 2/2b/2c: Emit NBA state-update, delay-ring, and SAnd done-latch logic.
         emitStateRegisterNba(c);
-        emitCounterFsmNba(c);
+        emitDelayRingNba(c);
         emitAndCombinerDoneLatchNba(c);
         emitKillAckNba(c);
 
@@ -2999,6 +3065,8 @@ class AssertNfaVisitor final : public VNVisitor {
         }
 
         UINFO(4, "NFA converted assertion at " << flp << endl);
+
+        if (dumpGraphLevel() >= 6) graph.m_graph.dumpDotFilePrefixed("assert-nfa");
     }
 
     // VISITORS

src/V3Subst.cpp

@@ -183,6 +183,7 @@ class SubstValidVisitor final : public VNVisitorConst {
     }
 
     void visit(AstConst*) override {}  // Accelerate
+    void visit(AstText*) override {}  // CExpr/CStmt literal text has no variable dependencies
 
     void visit(AstNodeExpr* nodep) override {
         if (!m_valid) return;

test_regress/t/t_property_delay_large.py

@@ -0,0 +1,21 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expect definition
+#
+# This program is free software; you can redistribute it and/or modify it
+# under the terms of either the GNU Lesser General Public License Version 3
+# or the Perl Artistic License Version 2.0.
+# SPDX-FileCopyrightText: 2026 Wilson Snyder
+# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('simulator')
+
+test.sim_time = 2700
+
+test.compile(timing_loop=True,
+             verilator_flags2=['--assert', '--timing', '--coverage-user', '--dumpi-graph', '6'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_property_delay_large.v

@@ -0,0 +1,73 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 Antmicro
+// SPDX-License-Identifier: CC0-1.0
+
+// verilog_format: off
+`define stop $stop
+`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)
+`define checkp(gotv,expv_s) do begin string gotv_s; gotv_s = $sformatf("%p", gotv); if ((gotv_s) != (expv_s)) begin $write("%%Error: %s:%0d:  got='%s' exp='%s'\n", `__FILE__,`__LINE__, (gotv_s), (expv_s)); `stop; end end while(0);
+// verilog_format: on
+
+module t (
+    input clk
+);
+  localparam int BIG_DELAY = 1024;
+  localparam int END_CYC = BIG_DELAY + 300;
+
+  int cyc = 0;
+  int fixed_pass_q[$];
+  int fixed_fail_q[$];
+  int range_pass_q[$];
+  int range_fail_q[$];
+
+  // Fixed delay: starts 1..12. Odd starts pass; even starts fail.
+  wire fixed_a = (cyc >= 1 && cyc <= 12);
+  wire fixed_b = (cyc == BIG_DELAY + 1) || (cyc == BIG_DELAY + 3)
+                 || (cyc == BIG_DELAY + 5) || (cyc == BIG_DELAY + 7)
+                 || (cyc == BIG_DELAY + 9) || (cyc == BIG_DELAY + 11);
+
+  // Range delay: single passing starts match 10 cycles later. Two blocks never
+  // match and expire 300 cycles after each start.
+  wire range_pass_a = (cyc == 10) || (cyc == 40) || (cyc == 70) || (cyc == 100)
+                      || (cyc == 130) || (cyc == 600) || (cyc == 640)
+                      || (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;
+  wire range_b = (cyc == 20) || (cyc == 50) || (cyc == 80) || (cyc == 110)
+                 || (cyc == 140) || (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);
+
+  assert property (@(posedge clk) fixed_a |-> ##1024 fixed_b)
+  else fixed_fail_q.push_back($sampled(cyc) + 1);
+
+  cover property (@(posedge clk) range_a ##[5:300] range_b) range_pass_q.push_back($sampled(cyc) + 1);
+
+  assert property (@(posedge clk) range_a |-> ##[5:300] range_b)
+  else range_fail_q.push_back($sampled(cyc) + 1);
+
+  assert property (@(posedge clk)
+      1'b0 |-> (fixed_a throughout (range_a throughout (range_b ##40 fixed_b))));
+
+  assert property (@(posedge clk) 1'b0 |-> ##[5:300] (range_b ##1 fixed_b));
+
+  assert property (@(posedge clk) 1'b0 |-> (fixed_a throughout (range_a ##[5:300] range_b)));
+
+  always_ff @(posedge clk) begin
+    cyc <= cyc + 1;
+    if (cyc == END_CYC) begin
+      `checkp(fixed_pass_q, "'{'h402, 'h404, 'h406, 'h408, 'h40a, 'h40c}");
+      `checkp(fixed_fail_q, "'{'h403, 'h405, 'h407, 'h409, 'h40b, 'h40d}");
+      `checkp(range_pass_q, "'{'h15, 'h33, 'h51, 'h6f, 'h8d, 'h263, 'h28b, 'h2b3, 'h2db}");
+      `checkp(range_fail_q,
+              "'{'h227, 'h228, 'h229, 'h22a, 'h22b, 'h22c, 'h22d, 'h22e, 'h461, 'h462, 'h463, 'h464, 'h465, 'h466, 'h467, 'h468}");
+
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule

test_regress/t/t_property_sexpr_multi.py

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

test_regress/t/t_property_sexpr_range_delay.v

@@ -80,6 +80,9 @@ module t (
   assert property (@(posedge clk) disable iff (cyc < 2)
       a |-> ##[1:10000] (a | b | c | d | e));
 
+  cover property (@(posedge clk) disable iff (cyc < 2)
+      ##[0:10000] 1'b1);
+
   // Range with binary SExpr: nextStep has delay > 0 after range match
   assert property (@(posedge clk) disable iff (cyc < 2)
       a |-> b ##[1:2] (a | b | c | d | e) ##3 (a | b | c | d | e))