From f6d56c6440dd42fa4b33ec2367d34dc9eaa5cc0c Mon Sep 17 00:00:00 2001 From: Artur Bieniek Date: Tue, 25 Aug 2026 14:26:46 +0200 Subject: [PATCH] Optimize consecutive repetiton and goto repetition using ring-buffer (#8096) --- Changes | 1 + docs/guide/exe_verilator.rst | 4 + src/V3Assert.cpp | 24 ++ src/V3AssertNfa.cpp | 386 ++++++++++-------- src/V3AstNodeOther.h | 1 + src/V3Options.cpp | 4 +- src/V3Options.h | 2 - test_regress/t/t_assert_consec_rep.v | 6 + test_regress/t/t_assert_consec_rep_large.py | 3 +- test_regress/t/t_assert_consec_rep_large.v | 42 +- .../t_assert_consec_rep_unroll_limit_bad.out | 10 - .../t/t_assert_consec_rep_unroll_limit_bad.py | 18 - .../t/t_assert_consec_rep_unroll_limit_bad.v | 19 - test_regress/t/t_assert_goto_rep.v | 6 + test_regress/t/t_cover_sequence.v | 10 + test_regress/t/t_flag_deprecated_bad.out | 1 + test_regress/t/t_flag_deprecated_bad.py | 2 +- test_regress/t/t_property_abort_implication.v | 76 +++- 18 files changed, 391 insertions(+), 224 deletions(-) delete mode 100644 test_regress/t/t_assert_consec_rep_unroll_limit_bad.out delete mode 100755 test_regress/t/t_assert_consec_rep_unroll_limit_bad.py delete mode 100644 test_regress/t/t_assert_consec_rep_unroll_limit_bad.v diff --git a/Changes b/Changes index b77113f5c..d75403307 100644 --- a/Changes +++ b/Changes @@ -51,6 +51,7 @@ Verilator 5.051 devel * Optimize temporary insertion for single bit replicates in DFG (#8110). [Geza Lore, Testorrent USA, Inc.] * Optimize mtask coarsening in multi-threaded scheduling (#8120). [Geza Lore, Testorrent USA, Inc.] * Optimize NFA delay-ring edge traversal, drop complexity to linear (#8145). [Artur Bieniek, Antmicro Ltd.] +* Optimize consecutive and goto repetitions using ring buffers, deprecate --assert-unroll-limit. [Artur Bieniek, Antmicro Ltd.] * Fix $finish continuing event loop (#7267) (#7950). [Artur Bieniek, Antmicro Ltd.] * Fix $display accepting streaming concat arguments (#7663) (#7890). [Jaeuk Lee] * Fix typedef clocking input sampling (#7688 partial) (#8204). [Marco Bartoli] diff --git a/docs/guide/exe_verilator.rst b/docs/guide/exe_verilator.rst index 4c1fa91b9..ccdf5800e 100644 --- a/docs/guide/exe_verilator.rst +++ b/docs/guide/exe_verilator.rst @@ -116,6 +116,10 @@ Summary: .. option:: --assert-unroll-limit + Deprecated and has no effect (ignored). + + In versions before 5.052: + Rarely needed. Specifies the maximum repetition or range count Verilator will unroll inside an SVA concurrent assertion (e.g. ``[*N]``, ``[->M:N]``, ``always[lo:hi]``). Beyond this, the assertion is rejected with an error diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index d441a8f28..ef132afa9 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -671,9 +671,11 @@ class AssertVisitor final : public VNVisitor { AstNode* propExprp; AstNodeExpr* disablep = nullptr; + AstNodeExpr* matchCountp = nullptr; if (AstPropSpec* const specp = VN_CAST(nodep->propp(), PropSpec)) { propExprp = specp->propp()->unlinkFrBack(); if (specp->disablep()) disablep = specp->disablep()->unlinkFrBack(); + matchCountp = specp->matchCountp(); } else { propExprp = nodep->propp()->unlinkFrBack(); } @@ -688,6 +690,28 @@ class AssertVisitor final : public VNVisitor { if (failsp && !VN_IS(propExprp, PExpr)) { failsp = newIfAssertFailOn(failsp, nodep->directive(), nodep->userType()); } + if (coverp && matchCountp && passsp) { + // Convert the match count into a loop that decrements a temporary variable until it + // reaches zero. + matchCountp->unlinkFrBack(); + AstVar* const remainingp = new AstVar{ + flp, VVarType::BLOCKTEMP, "__VnfaRemainingMatchCount", matchCountp->dtypep()}; + remainingp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + AstBegin* const replayp = new AstBegin{flp, "", remainingp, true}; + replayp->addStmtsp( + new AstAssign{flp, new AstVarRef{flp, remainingp, VAccess::WRITE}, matchCountp}); + AstLoop* const loopp = new AstLoop{flp}; + loopp->addStmtsp( + new AstLoopTest{flp, loopp, new AstVarRef{flp, remainingp, VAccess::READ}}); + loopp->addStmtsp(passsp); + loopp->addStmtsp( + new AstAssign{flp, new AstVarRef{flp, remainingp, VAccess::WRITE}, + new AstSub{flp, new AstVarRef{flp, remainingp, VAccess::READ}, + new AstConst{flp, AstConst::WidthedValue{}, + remainingp->dtypep()->width(), 1}}}); + replayp->addStmtsp(loopp); + passsp = replayp; + } AstNode* bodysp = assertBody(nodep, propExprp, passsp, failsp); if (disablep) bodysp = new AstIf{flp, new AstLogNot{flp, disablep}, bodysp}; // Add assertOn check last, for better combining diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 58f6d65c0..834074ed4 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -73,10 +73,15 @@ public: std::vector 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(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& 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(edger); + if (tedger.m_consumesCycle) continue; + const auto* const fromp = static_cast(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(&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* 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( 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(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(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* 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(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(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* 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 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 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); diff --git a/src/V3AstNodeOther.h b/src/V3AstNodeOther.h index 589311f61..83f71c9f7 100644 --- a/src/V3AstNodeOther.h +++ b/src/V3AstNodeOther.h @@ -1673,6 +1673,7 @@ class AstPropSpec final : public AstNode { // @astgen op1 := sensesp : Optional[AstSenItem] // @astgen op2 := disablep : Optional[AstNodeExpr] // @astgen op3 := propp : AstNode + // @astgen op4 := matchCountp : Optional[AstNodeExpr] // Cover sequence matches this tick VPropStrength m_propStrength = VPropStrength::DEFAULT; public: diff --git a/src/V3Options.cpp b/src/V3Options.cpp index 7f424127f..5f2b3cdf2 100644 --- a/src/V3Options.cpp +++ b/src/V3Options.cpp @@ -1303,7 +1303,9 @@ void V3Options::parseOptsList(FileLine* fl, const string& optdir, int argc, m_assertCase = flag; }); DECL_OPTION("-assert-case", OnOff, &m_assertCase); - DECL_OPTION("-assert-unroll-limit", Set, &m_assertUnrollLimit); + DECL_OPTION("-assert-unroll-limit", CbVal, [fl](const char*) { + fl->v3warn(DEPRECATED, "Option '--assert-unroll-limit' is deprecated and has no effect."); + }).notForRerun(); DECL_OPTION("-autoflush", OnOff, &m_autoflush); DECL_OPTION("-bbox-sys", OnOff, &m_bboxSys); diff --git a/src/V3Options.h b/src/V3Options.h index 3a182ebc6..35d6410dc 100644 --- a/src/V3Options.h +++ b/src/V3Options.h @@ -312,7 +312,6 @@ private: bool m_waiverMultiline = false; // main switch: --waiver-multiline bool m_xInitialEdge = false; // main switch: --x-initial-edge - int m_assertUnrollLimit = 1024; // main switch: --assert-unroll-limit int m_buildJobs = -1; // main switch: --build-jobs, -j int m_coverageExprMax = 32; // main switch: --coverage-expr-max int m_convergeLimit = 10000; // main switch: --converge-limit @@ -617,7 +616,6 @@ public: bool serializeOnly() const { return m_jsonOnly; } bool topIfacesSupported() const { return lintOnly() && !hierarchical(); } - int assertUnrollLimit() const { return m_assertUnrollLimit; } int buildJobs() const VL_MT_SAFE { return m_buildJobs; } int convergeLimit() const { return m_convergeLimit; } int coverageExprMax() const { return m_coverageExprMax; } diff --git a/test_regress/t/t_assert_consec_rep.v b/test_regress/t/t_assert_consec_rep.v index 30dac51d1..c21096cab 100644 --- a/test_regress/t/t_assert_consec_rep.v +++ b/test_regress/t/t_assert_consec_rep.v @@ -48,6 +48,7 @@ module t ( int count_fail21 = 0; int count_fail22 = 0; int count_fail23 = 0; + int count_fail24 = 0; // Test 1: a[*3] |-> b assert property (@(posedge clk) a [* 3] |-> b) @@ -136,6 +137,10 @@ module t ( assert property (@(posedge clk) cyc == 1 |-> ##1 (cyc != 5) [*3:5]) else count_fail23 <= count_fail23 + 1; + // Test 24: The empty endpoint of [*0:1] must not remain live for a later match. + assert property (@(posedge clk) cyc == 1 |-> (cyc == 2) [*0:1] ##1 (cyc == 2)) + else count_fail24 <= count_fail24 + 1; + // Counter FSM with M>0: range > kChainLimit (256) forces counter vertex // creation; min>0 exercises the Gte/active gating path in resolveLinks and // emitNbaLogic. Cover-only so count_fail values above are undisturbed. @@ -177,6 +182,7 @@ module t ( `checkd(count_fail20, count_fail21); `checkd(count_fail22, 1); `checkd(count_fail23, 0); + `checkd(count_fail24, 1); $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_assert_consec_rep_large.py b/test_regress/t/t_assert_consec_rep_large.py index 23f04b54c..bbb665be6 100755 --- a/test_regress/t/t_assert_consec_rep_large.py +++ b/test_regress/t/t_assert_consec_rep_large.py @@ -10,8 +10,9 @@ import vltest_bootstrap test.scenarios('vlt') +test.sim_time = 21000 -test.compile(verilator_flags2=['--assert', '--timing']) +test.compile(verilator_flags2=['--assert', '--timing', '--coverage-user']) test.execute() diff --git a/test_regress/t/t_assert_consec_rep_large.v b/test_regress/t/t_assert_consec_rep_large.v index 27dcbd14c..dbf6b7c63 100644 --- a/test_regress/t/t_assert_consec_rep_large.v +++ b/test_regress/t/t_assert_consec_rep_large.v @@ -20,16 +20,41 @@ module t ( wire a = crc[0]; wire b = crc[4]; wire c = crc[8]; + wire cons_a = cyc < 1100; + wire goto_a = cyc[1:0] != 0; int count_fail_257 = 0; - int count_fail_513 = 0; + int count_fail_cycles_513 = 0; + int count_fail_threads_513 = 0; + int count_fail_consrep_1025 = 0; + int count_fail_consrep_range_1025 = 0; + int count_fail_goto_1025 = 0; + int count_fail_goto_range_1025 = 0; + int count_cover_1025 = 0; // All N > prior kConsRepLimit=256 (pre-fix: V3AssertNfa crash at codegen). assert property (@(posedge clk) a [* 257] |-> b) else count_fail_257 <= count_fail_257 + 1; assert property (@(posedge clk) c |-> ##1 a [* 513]) - else count_fail_513 <= count_fail_513 + 1; + else count_fail_cycles_513 <= count_fail_cycles_513 + 1; + + // A blocking action counts all live threads rejected when the long run ends. + assert property (@(posedge clk) cons_a [* 513]) + else if (cyc == 1100) count_fail_threads_513++; + + // One triggered attempt makes an off-by-one ring exit observable. Consecutive + // repetition sees a long run; goto repetition advances across regular gaps. + assert property (@(posedge clk) (cyc == 0) ##0 cons_a [* 1025: $] |-> cyc == 2047) + else count_fail_consrep_1025++; + assert property (@(posedge clk) (cyc == 0) ##0 cons_a [* 1: 1025] |-> cyc == 2047) + else count_fail_consrep_range_1025++; + cover sequence (@(posedge clk) a [* 1: 1025]) count_cover_1025++; + + assert property (@(posedge clk) (cyc == 0) ##0 goto_a [-> 1025] |-> cyc != 1366) + else count_fail_goto_1025++; + assert property (@(posedge clk) (cyc == 0) ##0 goto_a [-> 1: 1025] |-> cyc == 2047) + else count_fail_goto_range_1025++; always @(posedge clk) begin cyc <= cyc + 1; @@ -37,12 +62,19 @@ module t ( if (cyc == 0) begin crc <= 64'h5aef0c8d_d70a4497; end - else if (cyc == 99) begin - `checkh(crc, 64'hc77bb9b3784ea091); + else if (cyc == 2047) begin + `checkh(crc, 64'h91bd2213af2ba46e); `checkd(count_fail_257, 0); - `checkd(count_fail_513, 31); + `checkd(count_fail_cycles_513, 666); + `checkd(count_fail_threads_513, 513); + `checkd(count_fail_consrep_1025, 76); + `checkd(count_fail_consrep_range_1025, 1025); + `checkd(count_fail_goto_1025, 1); + `checkd(count_fail_goto_range_1025, 1025); + `checkd(count_cover_1025, 2049); $write("*-* All Finished *-*\n"); $finish; end end + endmodule diff --git a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.out b/test_regress/t/t_assert_consec_rep_unroll_limit_bad.out deleted file mode 100644 index 349f425cb..000000000 --- a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.out +++ /dev/null @@ -1,10 +0,0 @@ -%Error: t/t_assert_consec_rep_unroll_limit_bad.v:14:37: Concurrent assertion repetition count 25700000 exceeds --assert-unroll-limit (1024); raise '--assert-unroll-limit' to compile - : ... note: In instance 't' - 14 | assert property (@(posedge clk) a [* 25700000] |-> b); - | ^~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: t/t_assert_consec_rep_unroll_limit_bad.v:17:37: Concurrent assertion repetition count 25700001 exceeds --assert-unroll-limit (1024); raise '--assert-unroll-limit' to compile - : ... note: In instance 't' - 17 | assert property (@(posedge clk) a [* 25700000:$] |-> b); - | ^~ -%Error: Exiting due to diff --git a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.py b/test_regress/t/t_assert_consec_rep_unroll_limit_bad.py deleted file mode 100755 index ba6d29aaf..000000000 --- a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.py +++ /dev/null @@ -1,18 +0,0 @@ -#!/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('linter') - -test.lint(fails=True, - verilator_flags2=['--assert-unroll-limit 1024'], - expect_filename=test.golden_filename) - -test.passes() diff --git a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.v b/test_regress/t/t_assert_consec_rep_unroll_limit_bad.v deleted file mode 100644 index 98f2761c1..000000000 --- a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.v +++ /dev/null @@ -1,19 +0,0 @@ -// DESCRIPTION: Verilator: Verilog Test module -// -// This file ONLY is placed under the Creative Commons Public Domain. -// SPDX-FileCopyrightText: 2026 PlanV GmbH -// SPDX-License-Identifier: CC0-1.0 - -module t ( - input clk -); - logic a, b; - - // Repetition count exceeds --assert-unroll-limit; pre-fix this hung the - // compiler, now an error names the limit so the user can raise it. - assert property (@(posedge clk) a [* 25700000] |-> b); - - // The mandatory prefix of an unbounded repetition is subject to the same limit. - assert property (@(posedge clk) a [* 25700000:$] |-> b); - -endmodule diff --git a/test_regress/t/t_assert_goto_rep.v b/test_regress/t/t_assert_goto_rep.v index 1a209444b..96601500b 100644 --- a/test_regress/t/t_assert_goto_rep.v +++ b/test_regress/t/t_assert_goto_rep.v @@ -31,6 +31,7 @@ module t ( int count_fail6 = 0; int count_fail7 = 0; int count_fail8 = 0; + int count_fail9 = 0; // Test 1: a[->2] |-> b (overlapping implication, 2 non-consecutive occurrences) assert property (@(posedge clk) a [-> 2] |-> b) @@ -64,6 +65,10 @@ module t ( assert property (@(posedge clk) a [-> 1: 4] |-> b) else count_fail8 <= count_fail8 + 1; + // Test 9: a[->2:2] is equivalent to a[->2]. + assert property (@(posedge clk) a [-> 2: 2] |-> b) + else count_fail9 <= count_fail9 + 1; + always @(posedge clk) begin `ifdef TEST_VERBOSE $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", $time, cyc, crc, a, b, c, d); @@ -83,6 +88,7 @@ module t ( `checkd(count_fail6, 25); `checkd(count_fail7, 20); `checkd(count_fail8, 20); + `checkd(count_fail9, count_fail1); $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_cover_sequence.v b/test_regress/t/t_cover_sequence.v index ac3311efe..553029982 100644 --- a/test_regress/t/t_cover_sequence.v +++ b/test_regress/t/t_cover_sequence.v @@ -25,6 +25,9 @@ module t ( int hit_clocked = 0; int hit_clocked_disable = 0; int hit_default_disable = 0; + int hit_consrep_1 = 0; + int hit_consrep_equal_range = 0; + int hit_consrep_range_0 = 0; int hit_consrep_range = 0; int hit_consrep_2 = 0; int hit_consrep_3 = 0; @@ -60,6 +63,9 @@ module t ( cover sequence (disable iff (!rst_n) a ##1 c) hit_default_disable++; // Form 5: consecutive repetition, counted per end-of-match + cover sequence (a [* 1]) hit_consrep_1++; + cover sequence (a [* 1: 1]) hit_consrep_equal_range++; + cover sequence (a [* 0: 1]) hit_consrep_range_0++; cover sequence (a [* 2: 3]) hit_consrep_range++; cover sequence (a [* 2]) hit_consrep_2++; cover sequence (a [* 3]) hit_consrep_3++; @@ -100,6 +106,10 @@ module t ( `checkd(hit_clocked, 149); `checkd(hit_clocked_disable, 27); `checkd(hit_default_disable, 30); + // a[*1:1] == a[*1] (IEEE 1800-2023 16.9.2) + `checkd(hit_consrep_1, 55); + `checkd(hit_consrep_equal_range, hit_consrep_1); + `checkd(hit_consrep_range_0, 154); // Counts both empty and nonempty matches `checkd(hit_consrep_2, 30); // Other sims: 29 `checkd(hit_consrep_3, 14); // Other sims: 13 // a[*2:3] == a[*2] or a[*3] (IEEE 1800-2023 16.9.2) diff --git a/test_regress/t/t_flag_deprecated_bad.out b/test_regress/t/t_flag_deprecated_bad.out index 41e38aebe..c973d5d01 100644 --- a/test_regress/t/t_flag_deprecated_bad.out +++ b/test_regress/t/t_flag_deprecated_bad.out @@ -9,4 +9,5 @@ %Warning-DEPRECATED: Option '-fno-dfg-post-inline' is deprecated and has no effect %Warning-DEPRECATED: Option '-fno-dfg-scoped' is deprecated, use '-fno-dfg' instead. %Warning-DEPRECATED: Option '-fno-dfg-break-cycles' is deprecated and has no effect +%Warning-DEPRECATED: Option '--assert-unroll-limit' is deprecated and has no effect. %Error: Exiting due to diff --git a/test_regress/t/t_flag_deprecated_bad.py b/test_regress/t/t_flag_deprecated_bad.py index 233ce25f8..d8a4baec2 100755 --- a/test_regress/t/t_flag_deprecated_bad.py +++ b/test_regress/t/t_flag_deprecated_bad.py @@ -12,7 +12,7 @@ import vltest_bootstrap test.scenarios('vlt') test.lint(verilator_flags2=[ - "--trace-fst-thread --trace-threads 2 --order-clock-delay --clk foo --no-clk bar -fno-dfg-pre-inline -fno-dfg-post-inline -fno-dfg-scoped -fno-dfg-break-cycles" + "--trace-fst-thread --trace-threads 2 --order-clock-delay --clk foo --no-clk bar -fno-dfg-pre-inline -fno-dfg-post-inline -fno-dfg-scoped -fno-dfg-break-cycles --assert-unroll-limit 1024", ], fails=True, expect_filename=test.golden_filename) diff --git a/test_regress/t/t_property_abort_implication.v b/test_regress/t/t_property_abort_implication.v index 0e2d04fc2..9a8157bf9 100644 --- a/test_regress/t/t_property_abort_implication.v +++ b/test_regress/t/t_property_abort_implication.v @@ -13,7 +13,7 @@ module t; bit clk = 0; int cyc = 0; - bit a = 0, b = 0, c = 0, abrt = 0; + bit a = 0, b = 0, c = 0, abrt = 0, abrt2 = 0; int fail_bool = 0; int fail_seq = 0; int pass_always = 0; @@ -23,11 +23,26 @@ module t; int pass_rej = 0; int fail_rej = 0; int fail_nested = 0; + int fail_nested_rej = 0; + int fail_nested_rej_ref = 0; + int fail_nested_rep_rej = 0; int fail_range = 0; int fail_ring2 = 0; int fail_rep_a = 0; + int fail_rep_accept_priority = 0; int fail_rep_r = 0; + int fail_rep_ring = 0; + int fail_rep_ref = 0; + int fail_rep_ring_true = 0; + int fail_rep_ref_true = 0; + int fail_goto = 0; + int fail_goto2 = 0; + int fail_goto_range = 0; + int fail_goto_range2 = 0; int fail_delay = 0; + int fail_delay2 = 0; + int fail_delay4 = 0; + int fail_delay_range = 0; int fail_fby = 0; int fail_and = 0; int fail_unb = 0; @@ -38,6 +53,7 @@ module t; b <= cyc[1]; c <= cyc[2]; abrt <= (cyc == 7); + abrt2 <= (cyc == 9); end assert property (@(posedge clk) sync_accept_on (abrt) (b |-> c)) @@ -61,6 +77,16 @@ module t; sync_accept_on (abrt) (1'b1 |-> sync_reject_on (1'b0) (1'b1 ##1 c))) else fail_nested++; + assert property (@(posedge clk) + sync_reject_on (abrt) + sync_reject_on (a) (1'b1 throughout (1'b1 ##2 1'b1))) + else fail_nested_rej++; + assert property (@(posedge clk) + sync_reject_on (abrt || a) (1'b1 throughout (1'b1 ##2 1'b1))) + else fail_nested_rej_ref++; + assert property (@(posedge clk) sync_reject_on (abrt) sync_reject_on (a) (b [* 5])) + else fail_nested_rep_rej++; + assert property (@(posedge clk) sync_accept_on (abrt) (1'b1 ##[1:2] (a ##1 b))) else fail_range++; @@ -70,12 +96,42 @@ module t; assert property (@(posedge clk) sync_accept_on (abrt) (a [* 2])) else fail_rep_a++; + assert property (@(posedge clk) + sync_accept_on (cyc == 2) ((cyc == 1) |-> (cyc == 1) [* 2])) + else fail_rep_accept_priority++; + assert property (@(posedge clk) sync_reject_on (abrt) (b [* 2])) else fail_rep_r++; + assert property (@(posedge clk) sync_reject_on (abrt) (b [* 5])) + else fail_rep_ring++; + assert property (@(posedge clk) sync_reject_on (abrt) (b ##1 b ##1 b ##1 b ##1 b)) + else fail_rep_ref++; + assert property (@(posedge clk) sync_reject_on (abrt) (1'b1 [* 5])) + else fail_rep_ring_true++; + assert property (@(posedge clk) + sync_reject_on (abrt) (1'b1 ##1 1'b1 ##1 1'b1 ##1 1'b1 ##1 1'b1)) + else fail_rep_ref_true++; + + assert property (@(posedge clk) sync_reject_on (abrt) (b [-> 5])) + else fail_goto++; + assert property (@(posedge clk) sync_reject_on (abrt2) (c [-> 5])) + else fail_goto2++; + assert property (@(posedge clk) sync_reject_on (abrt) (b [-> 3:5])) + else fail_goto_range++; + assert property (@(posedge clk) sync_reject_on (abrt2) (c [-> 3:5])) + else fail_goto_range2++; + assert property (@(posedge clk) sync_reject_on (abrt) (##1 c)) else fail_delay++; + assert property (@(posedge clk) sync_reject_on (abrt) (a ##2 c)) + else fail_delay2++; + assert property (@(posedge clk) sync_reject_on (abrt) (a ##4 c)) + else fail_delay4++; + assert property (@(posedge clk) sync_reject_on (abrt) (a ##[2:4] c)) + else fail_delay_range++; + cover property (@(posedge clk) (a ##1 b) or(sync_reject_on (abrt) (b ##1 c))); assert property (@(posedge clk) sync_reject_on (1'b0) (a #-# b)) @@ -91,7 +147,11 @@ module t; initial begin - repeat (40) #5 clk = ~clk; + repeat (24) #5 clk = ~clk; + `checkd(fail_delay2, 10); + `checkd(fail_delay4, 10); + `checkd(fail_delay_range, 9); + repeat (16) #5 clk = ~clk; `checkd(fail_bool, 5); `checkd(fail_seq, 3); `checkd(pass_always, 20); @@ -101,10 +161,22 @@ module t; `checkd(pass_rej, 17); `checkd(fail_rej, 2); `checkd(fail_nested, 10); + `checkd(fail_nested_rej_ref, 10); + `checkd(fail_nested_rej, 10); + `checkd(fail_nested_rep_rej, 19); `checkd(fail_range, 6); `checkd(fail_ring2, 1); `checkd(fail_rep_a, 19); + `checkd(fail_rep_accept_priority, 0); `checkd(fail_rep_r, 16); + `checkd(fail_rep_ref, 19); + `checkd(fail_rep_ring, fail_rep_ref); + `checkd(fail_rep_ref_true, 5); + `checkd(fail_rep_ring_true, fail_rep_ref_true); + `checkd(fail_goto, 9); + `checkd(fail_goto2, 6); + `checkd(fail_goto_range, 10); + `checkd(fail_goto_range2, 6); `checkd(fail_delay, 12); `checkd(fail_fby, 16); `checkd(fail_and, 16);