From 8a29360aded98af271128e4f7999948befa6a964 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Tue, 18 Aug 2026 18:30:38 +0200 Subject: [PATCH] Fix NFA assertion crash and mis-counted property if/case (#8074) --- src/V3AssertNfa.cpp | 314 +++++++++++++----- src/V3AstNodeExpr.h | 12 +- src/V3AstNodes.cpp | 8 + src/V3ParseImp.cpp | 4 +- src/verilog.y | 3 +- test_regress/t/t_prop_s_always_eos_count.out | 1 - .../t/t_property_abort_implication.py | 20 ++ test_regress/t/t_property_abort_implication.v | 116 +++++++ test_regress/t/t_property_accept_reject_on.v | 46 ++- test_regress/t/t_property_nfa_msgs_unsup.out | 52 +++ test_regress/t/t_property_nfa_msgs_unsup.py | 33 ++ test_regress/t/t_property_nfa_msgs_unsup.v | 65 ++++ 12 files changed, 562 insertions(+), 112 deletions(-) create mode 100755 test_regress/t/t_property_abort_implication.py create mode 100644 test_regress/t/t_property_abort_implication.v create mode 100644 test_regress/t/t_property_nfa_msgs_unsup.out create mode 100755 test_regress/t/t_property_nfa_msgs_unsup.py create mode 100644 test_regress/t/t_property_nfa_msgs_unsup.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 88103937c..6e12bba61 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -21,6 +21,9 @@ // - Replace converted assertions with combinational match/reject checks // so V3AssertPre sees no multi-cycle SExpr (unsupported ones fall through). // +// Members marked OWNED hold an AST tree this pass allocated and must delete; +// they are not linked into the netlist. +// //************************************************************************* #include "V3PchAstNoMT.h" // VL_MT_DISABLED_CODE_UNIT @@ -55,7 +58,7 @@ struct SvaVertexData final { AstVar* delayRingWrappedVarp = nullptr; // All slots written since the last clear AstVar* doneLVarp = nullptr; // SAnd LHS done-latch AstVar* doneRVarp = nullptr; // SAnd RHS done-latch - AstNodeExpr* stateSigp = nullptr; // Combinational state signal (owned during lowering) + AstNodeExpr* stateSigp = nullptr; // Combinational state signal; OWNED during lowering bool needsReg = false; // True if vertex has incoming clocked edge }; @@ -65,12 +68,14 @@ class SvaStateVertex final : public V3GraphVertex { public: // True if this is the sequence-match terminal vertex bool m_isMatch = false; - // Owned throughout-guard condition clones; IEEE 1800-2023 16.9.9 + // OWNED throughout-guard condition clones; IEEE 1800-2023 16.9.9 std::vector m_throughoutConds; // Nonzero for a bitset ring-buffer vertex for ## delays. bool m_isFixedDelayRing = false; int m_delayRingSize = 0; // Fixed delay cycles. 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_abortClearp = 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 @@ -95,6 +100,7 @@ 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_abortClearp) VL_DO_DANGLING(m_abortClearp->deleteTree(), m_abortClearp); if (m_andLhsCondp) VL_DO_DANGLING(m_andLhsCondp->deleteTree(), m_andLhsCondp); if (m_andRhsCondp) VL_DO_DANGLING(m_andRhsCondp->deleteTree(), m_andRhsCondp); } @@ -183,8 +189,8 @@ public: std::vector allEdges() const { std::vector result; for (const V3GraphVertex& vtxr : m_graph.vertices()) { - for (const V3GraphEdge& er : vtxr.outEdges()) { - result.push_back(static_cast(&er)); + for (const V3GraphEdge& edger : vtxr.outEdges()) { + result.push_back(static_cast(&edger)); } } return result; @@ -208,6 +214,11 @@ struct BuildResult final { static BuildResult failWithError() { return {nullptr, nullptr, {}, true}; } }; +// Parser-marked SAnd of overlapped implications: a property if/else/case. +static bool hasPropertyControlConjunction(const AstNodeExpr* nodep) { + return nodep->exists([](const AstSAnd* andp) { return andp->propertyControl(); }); +} + static AstConst* newTypedConstp(FileLine* const flp, const AstNodeDType* const dtypep, const uint32_t value) { AstConst* const constp = new AstConst{flp, AstConst::DTyped{}, dtypep}; @@ -722,6 +733,7 @@ class SvaNfaBuilder final { // Do not mark liveness sources: first boolean check is deferred. edgep->m_rejectOnFail = true; } + freeUnlinkedCondp(pre.finalCondp); currentp = condVtxp; } else { currentp = pre.termVertexp; @@ -965,12 +977,20 @@ class SvaNfaBuilder final { return {mergeVtxp, nullptr, {}}; } + // Free a dropped sub-result condition that is not linked into the AST + // (abort folds synthesize unparented finalCondp trees). + static void freeUnlinkedCondp(AstNodeExpr* condp) { + if (condp && !condp->backp()) VL_DO_DANGLING(condp->deleteTree(), condp); + } + // Build merge vertex for SOr / LogOr: both branches feed into one vertex. BuildResult buildOrMerge(AstNodeExpr* lhsp, AstNodeExpr* rhsp, SvaStateVertex* entryVtxp, FileLine* flp) { const BuildResult lhs = buildExpr(lhsp, entryVtxp); const BuildResult rhs = buildExpr(rhsp, entryVtxp); if (!lhs.valid() || !rhs.valid()) { // LCOV_EXCL_START -- sub-build fail bail + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); return BuildResult::fail(lhs.errorEmitted || rhs.errorEmitted); } // LCOV_EXCL_STOP // IEEE 1800-2023 16.14.3: a cover sequence counts every end-of-match. A @@ -980,6 +1000,8 @@ class SvaNfaBuilder final { // is handled by the OR-fold. if (m_isCoverSeq && (lhs.termVertexp != entryVtxp || rhs.termVertexp != entryVtxp)) { warnEndpointUnsupported(flp, "a sequence operand of 'or'"); + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); return BuildResult::failWithError(); } SvaStateVertex* const mergeVtxp = scopedCreateVertex(); @@ -995,6 +1017,8 @@ class SvaNfaBuilder final { } else { guardedLink(rhs.termVertexp, mergeVtxp, flp); } + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); return {mergeVtxp, nullptr, {}}; } @@ -1010,6 +1034,8 @@ class SvaNfaBuilder final { const bool rhsScope = m_inUnboundedScope; m_inUnboundedScope = savedScope || lhsScope || rhsScope; if (!lhs.valid() || !rhs.valid()) { // LCOV_EXCL_START -- sub-build fail bail + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); return BuildResult::fail(lhs.errorEmitted || rhs.errorEmitted); } // LCOV_EXCL_STOP @@ -1021,12 +1047,20 @@ class SvaNfaBuilder final { "Single-cycle SAnd operands must have finalCondp"); AstNodeExpr* const condp = new AstLogAnd{flp, lhs.finalCondp->cloneTreePure(false), rhs.finalCondp->cloneTreePure(false)}; + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); return {entryVtxp, condp, {}}; } // Range-delay mid-window sources in either sub-branch would need // to be folded into the latch's match-now signal, which the - // current combiner does not support. Defer (UNSUPPORTED). - if (!lhs.midSources.empty() || !rhs.midSources.empty()) return BuildResult::fail(); + // current combiner does not support. + if (!lhs.midSources.empty() || !rhs.midSources.empty()) { + flp->v3warn(E_UNSUPPORTED, + "Unsupported: ranged cycle delay in an operand of property 'and'"); + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); + return BuildResult::failWithError(); + } SvaStateVertex* const combVtxp = scopedCreateVertex(); combVtxp->m_isAndCombiner = true; combVtxp->m_andLhsTermp = lhs.termVertexp; @@ -1064,6 +1098,8 @@ class SvaNfaBuilder final { } } } + freeUnlinkedCondp(lhs.finalCondp); + freeUnlinkedCondp(rhs.finalCondp); return {combVtxp, nullptr, {}}; } @@ -1421,16 +1457,74 @@ 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. + static bool chainAccountsSource(const SvaStateVertex* srcp, + const std::unordered_set& preEdges) { + bool plainNonSink = false; + bool markedSink = false; + for (const V3GraphEdge& edger : srcp->outEdges()) { + if (preEdges.count(&edger)) continue; + const SvaTransEdge& tedger = static_cast(edger); + if (tedger.m_consumesCycle) continue; + const bool sink = static_cast(tedger.toVtxp())->m_isRejectSink; + if (tedger.m_rejectOnFail) { + if (!sink) return true; + markedSink = true; + } else if (!sink) { + plainNonSink = true; + } + } + return plainNonSink && markedSink; + } + + // Reject edge: fires when the source is live and the abort samples true. + void addAbortRejectEdge(SvaStateVertex* srcp, SvaStateVertex* sinkp, AstNodeExpr* condp, + FileLine* flp) { + AstNodeExpr* const notFirep = new AstLogNot{flp, sampled(abortFireExpr(condp, flp))}; + m_graph.addLink(srcp, sinkp, notFirep)->m_rejectOnFail = true; + return; + } + + // On the fire tick: kill body threads; accept kinds also forgive step misses. + void gateBodyEdgesOnAbort(const std::unordered_set& preEdges, + AstNodeExpr* condp, VAbortKind kind, FileLine* flp) { + for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) { + for (V3GraphEdge& edger : vtxr.outEdges()) { + if (preEdges.count(&edger)) continue; + SvaTransEdge* const tedgep = static_cast(&edger); + if (tedgep->m_rejectOnFail) { + if (!kind.isAccept()) continue; + AstNodeExpr* const firep = sampled(abortFireExpr(condp, flp)); + tedgep->m_condp + = tedgep->m_condp ? new AstLogOr{flp, tedgep->m_condp, firep} : firep; + } else if (tedgep->m_consumesCycle) { + AstNodeExpr* const notFirep + = new AstLogNot{flp, sampled(abortFireExpr(condp, flp))}; + tedgep->m_condp = tedgep->m_condp + ? new AstLogAnd{flp, tedgep->m_condp, notFirep} + : notFirep; + } + } + } + } + BuildResult buildAbortOn(AstNodeExpr* condp, AstNodeExpr* bodyp, SvaStateVertex* entryVtxp, - VAbortKind kind, FileLine* flp) { - // Snapshot pre-body vertices so post-build diff yields the body's sub-NFA. + VAbortKind kind, FileLine* flp, bool isTopLevelStep) { + // Snapshot pre-body vertices/edges so post-build diff yields the body's sub-NFA. std::unordered_set preExisting; - for (const V3GraphVertex& vtxr : m_graph.m_graph.vertices()) preExisting.insert(&vtxr); + std::unordered_set preEdges; + for (V3GraphVertex& vtxr : m_graph.m_graph.vertices()) { + preExisting.insert(&vtxr); + for (V3GraphEdge& edger : vtxr.outEdges()) preEdges.insert(&edger); + } m_outerAbortStack.push_back(condp); - const BuildResult bodyResult = buildExpr(bodyp, entryVtxp, /*isTopLevelStep=*/false); + const BuildResult bodyResult = buildExpr(bodyp, entryVtxp, isTopLevelStep); m_outerAbortStack.pop_back(); - UASSERT_OBJ(bodyResult.valid(), bodyp, "abort body must be a valid SVA expression"); + if (!bodyResult.valid()) return bodyResult; + + gateBodyEdgesOnAbort(preEdges, condp, kind, flp); // Live-thread sources for the abort edge: entry + new body vertices, // minus reject sinks (they carry reject fuel, not live-thread fuel). @@ -1439,6 +1533,11 @@ 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) { + AstNodeExpr* const firep = abortFireExpr(condp, flp); + sp->m_abortClearp + = sp->m_abortClearp ? new AstLogOr{flp, sp->m_abortClearp, firep} : firep; + } if (sp->m_isRejectSink) continue; abortSources.push_back(sp); } @@ -1450,15 +1549,18 @@ class SvaNfaBuilder final { if (kind.isAccept()) { // Match-only sink fed by $sampled(abort-fire) from every live source; - // registered as midSource so it never contributes a reject. The body - // terminal is already in abortSources, so we don't fold abort-fire - // into bodyResult.finalCondp. + // registered as midSource so it never contributes a reject. SvaStateVertex* const acceptSinkp = scopedCreateVertex(); for (SvaStateVertex* const srcp : abortSources) guardedLink(srcp, acceptSinkp, sampledAbortFire(), flp); std::vector midSources = bodyResult.midSources; midSources.push_back(acceptSinkp); - return {bodyResult.termVertexp, bodyResult.finalCondp, std::move(midSources)}; + AstNodeExpr* finalCondp = bodyResult.finalCondp; + if (finalCondp) { + if (finalCondp->backp()) finalCondp = finalCondp->cloneTreePure(false); + finalCondp = new AstLogOr{flp, finalCondp, abortFireExpr(condp, flp)}; + } + return {bodyResult.termVertexp, finalCondp, std::move(midSources)}; } // rejectOnFail treats m_condp as the success condition and fires on @@ -1466,10 +1568,15 @@ class SvaNfaBuilder final { SvaStateVertex* const rejectSinkp = m_graph.createStateVertex(); rejectSinkp->m_isRejectSink = true; for (SvaStateVertex* const srcp : abortSources) - m_graph.addLink(srcp, rejectSinkp, new AstLogNot{flp, sampledAbortFire()}) - ->m_rejectOnFail - = true; - return bodyResult; + if (!chainAccountsSource(srcp, preEdges)) + addAbortRejectEdge(srcp, rejectSinkp, condp, flp); + AstNodeExpr* finalCondp = bodyResult.finalCondp; + if (finalCondp) { + if (finalCondp->backp()) finalCondp = finalCondp->cloneTreePure(false); + finalCondp + = new AstLogAnd{flp, finalCondp, new AstLogNot{flp, abortFireExpr(condp, flp)}}; + } + return {bodyResult.termVertexp, finalCondp, bodyResult.midSources}; } public: @@ -1482,10 +1589,11 @@ public: , m_isSeqEvent{isSeqEvent} {} // Reset scope between antecedent and consequent: liveness must not leak. + // m_outerAbortStack survives: an abort wrapping the implication covers the + // consequent too (IEEE 1800-2023 16.12.14). void resetScope() { m_inUnboundedScope = false; m_temporalGuardStack.clear(); - m_outerAbortStack.clear(); } BuildResult buildExpr(AstNodeExpr* nodep, SvaStateVertex* entryVtxp, @@ -1540,7 +1648,8 @@ public: return buildSWithin(withinp, entryVtxp, isTopLevelStep); } if (AstAbortOn* const ap = VN_CAST(nodep, AbortOn)) { - return buildAbortOn(ap->condp(), ap->propp(), entryVtxp, ap->kind(), ap->fileline()); + return buildAbortOn(ap->condp(), ap->propp(), entryVtxp, ap->kind(), ap->fileline(), + isTopLevelStep); } if (VN_IS(nodep, SNonConsRep)) return BuildResult::fail(); if (AstImplication* const implp = VN_CAST(nodep, Implication)) { @@ -1746,21 +1855,19 @@ class SvaNfaLowering final { // 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; - for (const V3GraphEdge& er : c.vtx[i]->inEdges()) { - const SvaTransEdge& te = static_cast(er); - if (!te.m_consumesCycle) continue; - const int fromIdx = te.fromVtxp()->color(); - UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, te.fromVtxp(), + for (const V3GraphEdge& edger : c.vtx[i]->inEdges()) { + const SvaTransEdge& tedger = static_cast(edger); + if (!tedger.m_consumesCycle) continue; + const int fromIdx = tedger.fromVtxp()->color(); + UASSERT_OBJ(c.vtx[fromIdx]->datap()->stateSigp, tedger.fromVtxp(), "Clocked-edge source missing stateSig"); AstNodeExpr* srcSigp = c.vtx[fromIdx]->datap()->stateSigp->cloneTreePure(false); - srcSigp = andCond(c.flp, srcSigp, te.m_condp); + srcSigp = andCond(c.flp, srcSigp, tedger.m_condp); if (c.disableExprp) { AstNodeExpr* const notDisp @@ -1781,8 +1888,8 @@ class SvaNfaLowering final { } // Capture disableCnt in Phase-2 NBA before any reactive re-evaluation. - // snapshotVarp and disableCntVarp are allocated together. - if (c.snapshotVarp && (bodyp || hasDelayRing)) { + // Emitted even for stateless graphs; snapshotOk gates rejects there too. + if (c.snapshotVarp) { UASSERT_OBJ(c.disableCntVarp, c.senTreep, "snapshotVarp set without disableCntVarp"); // disable_snapshot <= disable_count; AstAssignDly* const snapshotp @@ -1807,15 +1914,15 @@ class SvaNfaLowering final { const uint32_t size = static_cast(vtxp->m_delayRingSize); AstNodeExpr* incomingp = nullptr; - for (const SvaTransEdge* const tep : c.edges) { - if (static_cast(tep->toVtxp()->color()) != ri) continue; - UASSERT_OBJ(tep->m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp, + for (const SvaTransEdge* const tedgep : c.edges) { + if (static_cast(tedgep->toVtxp()->color()) != ri) continue; + UASSERT_OBJ(tedgep->m_consumesCycle == vtxp->m_isFixedDelayRing, vtxp, "Delay-ring incoming edge kind mismatch"); - const int fi = tep->fromVtxp()->color(); + const int fi = tedgep->fromVtxp()->color(); UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, c.vtx[fi], "Delay-ring incoming source missing stateSig"); AstNodeExpr* contribp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false); - contribp = andCond(c.flp, contribp, tep->m_condp); + contribp = andCond(c.flp, contribp, tedgep->m_condp); if (c.disableExprp) { AstNodeExpr* const notDisp = new AstLogNot{c.flp, c.disableExprp->cloneTreePure(false)}; @@ -1858,6 +1965,10 @@ class SvaNfaLowering final { clearCondp = orExprs(c.flp, clearCondp, sampled(vtxp->m_delayRingClearCondp->cloneTreePure(false))); } + if (vtxp->m_abortClearp) { + clearCondp = orExprs(c.flp, clearCondp, + sampled(vtxp->m_abortClearp->cloneTreePure(false))); + } if (c.disableExprp) { clearCondp = orExprs(c.flp, clearCondp, c.disableExprp->cloneTreePure(false)); } @@ -1960,14 +2071,14 @@ class SvaNfaLowering final { // end-of-match fires the action independently, no OR-fold). void computeTerminalMatchAndReject(LowerCtx& c, AstNodeExpr* snapshotOkp, SignalSet& sigs, std::vector* outPerMidSrcsp = nullptr) { - for (const SvaTransEdge* const tep : c.edges) { - if (tep->toVtxp() != c.graph.m_matchVertexp) continue; - const int fi = tep->fromVtxp()->color(); - UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, tep->fromVtxp(), + for (const SvaTransEdge* const tedgep : c.edges) { + if (tedgep->toVtxp() != c.graph.m_matchVertexp) continue; + const int fi = tedgep->fromVtxp()->color(); + UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp, tedgep->fromVtxp(), "Terminal-link source missing stateSig"); AstNodeExpr* srcSigp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false); - srcSigp = andCond(c.flp, srcSigp, tep->m_condp); + srcSigp = andCond(c.flp, srcSigp, tedgep->m_condp); if (snapshotOkp) { srcSigp = new AstLogAnd{c.flp, srcSigp, snapshotOkp->cloneTreePure(false)}; } @@ -1984,19 +2095,19 @@ class SvaNfaLowering final { outPerMidSrcsp->push_back(perMidp); } - if (tep->fromVtxp()->m_delayRingSize && !tep->fromVtxp()->m_isFixedDelayRing) { + if (tedgep->fromVtxp()->m_delayRingSize && !tedgep->fromVtxp()->m_isFixedDelayRing) { sigs.terminalActivep = orExprs(c.flp, sigs.terminalActivep, srcSigp->cloneTreePure(false)); // reject |= ring[next_idx] && final_condition; - AstNodeExpr* expireContribp = delayRingOutput(c.flp, tep->fromVtxp()); - expireContribp = andCond(c.flp, expireContribp, tep->m_condp); + AstNodeExpr* expireContribp = delayRingOutput(c.flp, tedgep->fromVtxp()); + expireContribp = andCond(c.flp, expireContribp, tedgep->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) { + } else if (tedgep->fromVtxp()->m_isUnbounded || tedgep->fromVtxp()->m_isAndCombiner) { sigs.terminalActivep = orExprs(c.flp, sigs.terminalActivep, srcSigp); } else { sigs.terminalActivep @@ -2075,21 +2186,24 @@ class SvaNfaLowering final { // Phase 3a: required-step rejection. // Builder only sets m_rejectOnFail on non-clocked Links with m_condp // or m_condVtxp, and the source always has a resolved stateSig. - for (const SvaTransEdge* const tep : c.edges) { - if (!tep->m_rejectOnFail) continue; - const int fi = tep->fromVtxp()->color(); - UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp && (tep->m_condp || tep->m_condVtxp), - tep->fromVtxp(), + for (const SvaTransEdge* const tedgep : c.edges) { + if (!tedgep->m_rejectOnFail) continue; + const int fi = tedgep->fromVtxp()->color(); + UASSERT_OBJ(c.vtx[fi]->datap()->stateSigp && (tedgep->m_condp || tedgep->m_condVtxp), + tedgep->fromVtxp(), "rejectOnFail Link must have condp/condVtxp and source stateSig"); AstNodeExpr* const srcSigp = c.vtx[fi]->datap()->stateSigp->cloneTreePure(false); AstNodeExpr* condp = nullptr; - if (tep->m_condVtxp) { - const int ci = tep->m_condVtxp->color(); - UASSERT_OBJ(c.vtx[ci]->datap()->stateSigp, tep->m_condVtxp, + if (tedgep->m_condVtxp) { + const int ci = tedgep->m_condVtxp->color(); + UASSERT_OBJ(c.vtx[ci]->datap()->stateSigp, tedgep->m_condVtxp, "rejectOnFail condVtxp missing stateSig"); condp = c.vtx[ci]->datap()->stateSigp->cloneTreePure(false); + if (tedgep->m_condp) { + condp = new AstLogOr{c.flp, condp, tedgep->m_condp->cloneTreePure(false)}; + } } else { - condp = tep->m_condp->cloneTreePure(false); + condp = tedgep->m_condp->cloneTreePure(false); } AstNodeExpr* const notCondp = new AstLogNot{c.flp, condp}; AstNodeExpr* const rawFailp = new AstLogAnd{c.flp, srcSigp, notCondp}; @@ -2204,13 +2318,14 @@ class SvaNfaLowering final { // Propagate Link edges for (int fi = 0; fi < c.N; ++fi) { if (!c.vtx[fi]->datap()->stateSigp) continue; - for (const V3GraphEdge& er : c.vtx[fi]->outEdges()) { - const SvaTransEdge& te = static_cast(er); - if (te.m_consumesCycle) continue; - const int ti = te.toVtxp()->color(); - if (te.toVtxp()->m_isMatch || te.toVtxp()->m_isRejectSink) continue; - AstNodeExpr* const contributionp = andCond( - c.flp, c.vtx[fi]->datap()->stateSigp->cloneTreePure(false), te.m_condp); + 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; @@ -2364,10 +2479,11 @@ public: // Identify registered vertices (targets of clocked edges). for (int i = 0; i < N; ++i) { - for (const V3GraphEdge& er : vtx[i]->outEdges()) { - const SvaTransEdge& te = static_cast(er); - const int toIdx = te.toVtxp()->color(); - if (te.m_consumesCycle && toIdx != matchIdx && !te.toVtxp()->m_isRejectSink) { + for (const V3GraphEdge& edger : vtx[i]->outEdges()) { + const SvaTransEdge& tedger = static_cast(edger); + const int toIdx = tedger.toVtxp()->color(); + if (tedger.m_consumesCycle && toIdx != matchIdx + && !tedger.toVtxp()->m_isRejectSink) { vtx[toIdx]->datap()->needsReg = true; } } @@ -3019,9 +3135,20 @@ class AssertNfaVisitor final : public VNVisitor { return false; } - void processAssertion(AstNodeCoverOrAssert* assertp) { - if (assertp->immediate()) return; + // Outcome counts for a property if/case are wrong in an outcome-multiplying + // context. Returns that context, or nullptr when the shape is supported. + static const char* unsupportedPropertyControl(const AstNodeCoverOrAssert* assertp, + const AstNodeExpr* seqBodyp, bool negated) { + if (!hasPropertyControlConjunction(seqBodyp)) return nullptr; + if (negated) return "negation"; + if (VN_IS(assertp, Cover)) return "cover"; + if (VN_AS(assertp, Assert)->passsp()) return "a pass action"; + return nullptr; + } + // Inline property/sequence refs and reject unsupported shapes. + // Returns the PropSpec to lower, or nullptr when fully handled here. + AstPropSpec* prepareAssertionProp(AstNodeCoverOrAssert* assertp) { if (AstPropSpec* const specp = VN_CAST(assertp->propp(), PropSpec)) { if (AstFuncRef* const funcrefp = VN_CAST(specp->propp(), FuncRef)) { if (const AstProperty* const propyp = VN_CAST(funcrefp->taskp(), Property)) { @@ -3033,20 +3160,36 @@ class AssertNfaVisitor final : public VNVisitor { inlineAllSequenceRefs(assertp->propp()); if (AstPropSpec* const specp = VN_CAST(assertp->propp(), PropSpec)) { - if (hoistClockedSeq(specp)) return; + if (hoistClockedSeq(specp)) return nullptr; } AstPropSpec* const propp = VN_AS(assertp->propp(), PropSpec); - const bool isCover = VN_IS(assertp, Cover); - if (!isCover && effectiveAssertPropStrength(propp) == VPropStrength::STRONG) { + if (!VN_IS(assertp, Cover) + && effectiveAssertPropStrength(propp) == VPropStrength::STRONG) { propp->v3warn(E_UNSUPPORTED, "Unsupported: strong property in " + assertp->verilogKwd() + "."); replaceBodyOnBuildError(assertp->fileline(), propp, /*errorEmitted=*/true); - return; + return nullptr; } - if (!hasMultiCycleExpr(propp)) return; - if (isBareTopLevelUntil(propp)) return; + if (!hasMultiCycleExpr(propp)) return nullptr; + // A nested property instance keeps its body behind the call; lowering would drop it. + if (propp->exists([](const AstFuncRef* refp) { return VN_IS(refp->taskp(), Property); })) { + assertp->v3warn(E_UNSUPPORTED, + "Unsupported: property instance inside a multi-cycle property " + "expression"); + VL_DO_DANGLING(pushDeletep(assertp->unlinkFrBack()), assertp); + return nullptr; + } + if (isBareTopLevelUntil(propp)) return nullptr; + return propp; + } + + void processAssertion(AstNodeCoverOrAssert* assertp) { + if (assertp->immediate()) return; + + AstPropSpec* const propp = prepareAssertionProp(assertp); + if (!propp) return; PropertyParts parts = decomposeProperty(propp); UASSERT_OBJ(parts.seqExprp, propp, "Property body must be an expression"); @@ -3059,6 +3202,9 @@ class AssertNfaVisitor final : public VNVisitor { seqBodyp = notp->lhsp(); } + const char* const propertyControlp + = unsupportedPropertyControl(assertp, seqBodyp, negated); + // Substitute property-local match-item refs in consequent with // $past(rhs, K) before NFA build (IEEE 1800-2023 16.10). if (liftMatchItemSubstitutions(parts, seqBodyp)) { @@ -3068,8 +3214,6 @@ class AssertNfaVisitor final : public VNVisitor { return; } - AstSenTree* senTreep = assertp->sentreep(); - bool senTreeOwned = false; // True if we created senTreep locally AstCover* const coverp = VN_CAST(assertp, Cover); const bool isCoverSeq = coverp && coverp->isCoverSeq(); // A sequence event control is not an assertion directive; no default @@ -3082,12 +3226,10 @@ class AssertNfaVisitor final : public VNVisitor { if (!propp->disablep() && m_defaultDisablep && !isSeqEvent) { propp->disablep(m_defaultDisablep->condp()->cloneTreePure(true)); } - if (!senTreep && propp->sensesp()) { - senTreep = new AstSenTree{propp->fileline(), propp->sensesp()->cloneTree(true)}; - senTreeOwned = true; - } + if (!propp->sensesp()) return; + AstSenTree* senTreep + = new AstSenTree{propp->fileline(), propp->sensesp()->cloneTree(true)}; AstNodeExpr* disableExprp = propp->disablep(); - if (!senTreep) return; // NFA lowering clones repeated operands and may hoist them into an // always_comb block. Resolve implicit sampled-value clocks first, while @@ -3111,7 +3253,15 @@ class AssertNfaVisitor final : public VNVisitor { // from this attempt become orphan MODULETEMPs; V3Dead removes // them along with the dead always_comb driver. replaceBodyOnBuildError(flp, propp, result.errorEmitted); - if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep); + VL_DO_DANGLING(pushDeletep(senTreep), senTreep); + return; + } + // After the build, so a construct the builder rejects reports itself. + if (propertyControlp) { + seqBodyp->v3warn(E_UNSUPPORTED, + "Unsupported: temporal property if/case with " << propertyControlp); + replaceBodyOnBuildError(flp, propp, /*errorEmitted=*/true); + VL_DO_DANGLING(pushDeletep(senTreep), senTreep); return; } @@ -3149,7 +3299,7 @@ class AssertNfaVisitor final : public VNVisitor { AstSenTree* const threadFailReplaySenTreep = signals.threadFailCountp ? senTreep->cloneTree(false) : nullptr; - if (senTreeOwned) VL_DO_DANGLING(pushDeletep(senTreep), senTreep); + VL_DO_DANGLING(pushDeletep(senTreep), senTreep); if (disableExprUnlinked) VL_DO_DANGLING(pushDeletep(disableExprp), disableExprp); if (result.finalCondp && !result.finalCondp->backp()) pushDeletep(result.finalCondp); diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 1428a6cb2..db1e9089d 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -3987,12 +3987,16 @@ public: class AstSAnd final : public AstNodeBiop { // Sequence 'and' (IEEE 1800-2023 16.9.5): both operand sequences must match. // Operates on match sets, not values. For boolean operands, lowered to AstLogAnd. + const bool m_propertyControl; // Parser-generated property if/case branch conjunction public: - AstSAnd(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp) - : ASTGEN_SUPER_SAnd(fl, lhsp, rhsp) { + AstSAnd(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp, bool propertyControl = false) + : ASTGEN_SUPER_SAnd(fl, lhsp, rhsp) + , m_propertyControl{propertyControl} { dtypeSetBit(); } ASTGEN_MEMBERS_AstSAnd; + void dump(std::ostream& str) const override; + void dumpJson(std::ostream& str) const override; void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override { out.opLogAnd(lhs, rhs); } @@ -4006,6 +4010,10 @@ public: bool sizeMattersRhs() const override { return false; } int instrCount() const override { return widthInstrs() + INSTR_COUNT_BRANCH; } bool isMultiCycleSva() const override { return true; } + bool sameNode(const AstNode* samep) const override { // LCOV_EXCL_LINE + return m_propertyControl == VN_DBG_AS(samep, SAnd)->m_propertyControl; // LCOV_EXCL_LINE + } + bool propertyControl() const { return m_propertyControl; } }; class AstSIntersect final : public AstNodeBiop { // Sequence 'intersect' (IEEE 1800-2023 16.9.6): both operands match with equal length. diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index 25d453933..7868d2637 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -483,6 +483,14 @@ void AstSConsRep::dumpJson(std::ostream& str) const { dumpJsonBoolFuncIf(str, unbounded); dumpJsonGen(str); } // LCOV_EXCL_STOP +void AstSAnd::dump(std::ostream& str) const { + this->AstNodeExpr::dump(str); + if (propertyControl()) str << " [PROPERTY_CONTROL]"; +} +void AstSAnd::dumpJson(std::ostream& str) const { + dumpJsonBoolFuncIf(str, propertyControl); + dumpJsonGen(str); +} void AstPropAlways::dump(std::ostream& str) const { this->AstNodeExpr::dump(str); if (isStrong()) str << " [strong]"; diff --git a/src/V3ParseImp.cpp b/src/V3ParseImp.cpp index 549166f6d..62baeea15 100644 --- a/src/V3ParseImp.cpp +++ b/src/V3ParseImp.cpp @@ -137,7 +137,7 @@ AstNodeExpr* V3ParseImp::makePropertyCase(FileLine* flp, AstNodeExpr* exprp, Ast new AstLogNot{itemp->fileline(), matchedp->cloneTreePure(false)}} : itemMatchp->cloneTreePure(false); AstNodeExpr* const branchp = new AstImplication{itemp->fileline(), guardp, propp, true}; - resultp = resultp ? new AstSAnd{flp, resultp, branchp} : branchp; + resultp = resultp ? new AstSAnd{flp, resultp, branchp, /*propertyControl=*/true} : branchp; matchedp = matchedp ? new AstLogOr{itemp->fileline(), matchedp, itemMatchp} : itemMatchp; } itemsp->deleteTree(); @@ -150,7 +150,7 @@ AstNodeExpr* V3ParseImp::makePropertyCase(FileLine* flp, AstNodeExpr* exprp, Ast AstNodeExpr* const noMatchp = static_cast(new AstLogNot{defaultFlp, matchedp->cloneTreePure(false)}); AstNodeExpr* const branchp = new AstImplication{defaultFlp, noMatchp, defaultPropp, true}; - resultp = new AstSAnd{flp, resultp, branchp}; + resultp = new AstSAnd{flp, resultp, branchp, /*propertyControl=*/true}; } matchedp->deleteTree(); exprp->deleteTree(); diff --git a/src/verilog.y b/src/verilog.y index 493c197a2..3b8b66c40 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6719,7 +6719,8 @@ property_exprCaseIf: // IEEE: part of property_expr for if/case | yIF '(' expr/*expression_or_dist*/ ')' pexpr yELSE pexpr { AstNodeExpr* const elseCondp = new AstLogNot{$1, $3->cloneTreePure(false)}; $$ = new AstSAnd{$1, new AstImplication{$1, $3, $5, true}, - new AstImplication{$1, elseCondp, $7, true}}; } + new AstImplication{$1, elseCondp, $7, true}, + /*propertyControl=*/true}; } ; property_case_itemList: // IEEE: {property_case_item} diff --git a/test_regress/t/t_prop_s_always_eos_count.out b/test_regress/t/t_prop_s_always_eos_count.out index ec12d78d1..64edf2348 100644 --- a/test_regress/t/t_prop_s_always_eos_count.out +++ b/test_regress/t/t_prop_s_always_eos_count.out @@ -4,6 +4,5 @@ [115] %Error: t_prop_s_always_eos_count.v:44: Assertion failed in top.t [115] %Error: t_prop_s_always_eos_count.v:48: Assertion failed in top.t [115] %Error: t_prop_s_always_eos_count.v:56: Assertion failed in top.t -[115] %Error: t_prop_s_always_eos_count.v:62: Assertion failed in top.t [115] %Error: t_prop_s_always_eos_count.v:70: Assertion failed in top.t [115] %Error: t_prop_s_always_eos_count.v:73: Assertion failed in top.t diff --git a/test_regress/t/t_property_abort_implication.py b/test_regress/t/t_property_abort_implication.py new file mode 100755 index 000000000..36fbd6160 --- /dev/null +++ b/test_regress/t/t_property_abort_implication.py @@ -0,0 +1,20 @@ +#!/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 = 16000 + +test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_property_abort_implication.v b/test_regress/t/t_property_abort_implication.v new file mode 100644 index 000000000..0e2d04fc2 --- /dev/null +++ b/test_regress/t/t_property_abort_implication.v @@ -0,0 +1,116 @@ +// 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 + +// 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); +// verilog_format: on + +module t; + + bit clk = 0; + int cyc = 0; + bit a = 0, b = 0, c = 0, abrt = 0; + int fail_bool = 0; + int fail_seq = 0; + int pass_always = 0; + int fail_always = 0; + int fail_ring = 0; + int fail_first = 0; + int pass_rej = 0; + int fail_rej = 0; + int fail_nested = 0; + int fail_range = 0; + int fail_ring2 = 0; + int fail_rep_a = 0; + int fail_rep_r = 0; + int fail_delay = 0; + int fail_fby = 0; + int fail_and = 0; + int fail_unb = 0; + + always @(posedge clk) begin + cyc <= cyc + 1; + a <= cyc[0]; + b <= cyc[1]; + c <= cyc[2]; + abrt <= (cyc == 7); + end + + assert property (@(posedge clk) sync_accept_on (abrt) (b |-> c)) + else fail_bool++; + assert property (@(posedge clk) sync_accept_on (abrt) ((a ##1 b) |-> c)) + else fail_seq++; + + assert property (@(posedge clk) sync_accept_on (1'b1) (1'b1 |-> (1'b1 ##1 1'b0))) pass_always++; + else fail_always++; + + assert property (@(posedge clk) sync_accept_on (abrt) (1'b1 ##2 c)) + else fail_ring++; + + assert property (@(posedge clk) sync_accept_on (1'b0) (b ##1 1'b1)) + else fail_first++; + + assert property (@(posedge clk) sync_reject_on (abrt) (1'b1 ##1 1'b1)) pass_rej++; + else fail_rej++; + + assert property (@(posedge clk) + sync_accept_on (abrt) (1'b1 |-> sync_reject_on (1'b0) (1'b1 ##1 c))) + else fail_nested++; + + assert property (@(posedge clk) sync_accept_on (abrt) (1'b1 ##[1:2] (a ##1 b))) + else fail_range++; + + assert property (@(posedge clk) sync_accept_on (abrt) sync_accept_on (b) (1'b1 ##2 c)) + else fail_ring2++; + + assert property (@(posedge clk) sync_accept_on (abrt) (a [* 2])) + else fail_rep_a++; + + assert property (@(posedge clk) sync_reject_on (abrt) (b [* 2])) + else fail_rep_r++; + + assert property (@(posedge clk) sync_reject_on (abrt) (##1 c)) + else fail_delay++; + + 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)) + else fail_fby++; + + assert property (@(posedge clk) (sync_accept_on (abrt) b) and c) + else fail_and++; + + assert property (@(posedge clk) sync_reject_on (abrt) (a and always [1:$] b)) + else fail_unb++; + + cover property (@(posedge clk) (a and b) ##1 c); + + + initial begin + repeat (40) #5 clk = ~clk; + `checkd(fail_bool, 5); + `checkd(fail_seq, 3); + `checkd(pass_always, 20); + `checkd(fail_always, 0); // zero-ok + `checkd(fail_ring, 8); + `checkd(fail_first, 11); + `checkd(pass_rej, 17); + `checkd(fail_rej, 2); + `checkd(fail_nested, 10); + `checkd(fail_range, 6); + `checkd(fail_ring2, 1); + `checkd(fail_rep_a, 19); + `checkd(fail_rep_r, 16); + `checkd(fail_delay, 12); + `checkd(fail_fby, 16); + `checkd(fail_and, 16); + `checkd(fail_unb, 3); // One other sim: 19 + $write("*-* All Finished *-*\n"); + $finish; + end + +endmodule diff --git a/test_regress/t/t_property_accept_reject_on.v b/test_regress/t/t_property_accept_reject_on.v index 080af892c..5dcef2871 100644 --- a/test_regress/t/t_property_accept_reject_on.v +++ b/test_regress/t/t_property_accept_reject_on.v @@ -38,54 +38,52 @@ module t ( // Test 1: accept_on (async) -- property succeeds when cnd_a fires assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) body) - else count_fail1 <= count_fail1 + 1; + else count_fail1 <= count_fail1 + 1; // Test 2: reject_on (async) -- property fails when cnd_r fires assert property (@(posedge clk) disable iff (cyc < 2) reject_on (cnd_r) body) - else count_fail2 <= count_fail2 + 1; + else count_fail2 <= count_fail2 + 1; // Test 3: sync_accept_on -- sampled at matured clocking event assert property (@(posedge clk) disable iff (cyc < 2) sync_accept_on (cnd_a) body) - else count_fail3 <= count_fail3 + 1; + else count_fail3 <= count_fail3 + 1; // Test 4: sync_reject_on assert property (@(posedge clk) disable iff (cyc < 2) sync_reject_on (cnd_r) body) - else count_fail4 <= count_fail4 + 1; + else count_fail4 <= count_fail4 + 1; // Test 5: outer accept_on wraps inner reject_on -- outer wins per 16.12.14 - assert property (@(posedge clk) disable iff (cyc < 2) - accept_on (cnd_a) reject_on (cnd_r) body) - else count_fail5 <= count_fail5 + 1; + assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) reject_on (cnd_r) body) + else count_fail5 <= count_fail5 + 1; // Test 6: outer reject_on wraps inner accept_on - assert property (@(posedge clk) disable iff (cyc < 2) - reject_on (cnd_r) accept_on (cnd_a) body) - else count_fail6 <= count_fail6 + 1; + assert property (@(posedge clk) disable iff (cyc < 2) reject_on (cnd_r) accept_on (cnd_a) body) + else count_fail6 <= count_fail6 + 1; // Test 7: named property form with accept_on inside property p_named; accept_on (cnd_a) body; endproperty assert property (@(posedge clk) disable iff (cyc < 2) p_named) - else count_fail7 <= count_fail7 + 1; + else count_fail7 <= count_fail7 + 1; // Test 8: disable iff over a sync_accept_on with a second disabled window assert property (@(posedge clk) disable iff (cyc < 2 || (cyc >= 50 && cyc < 60)) sync_accept_on (cnd) body) - else count_fail8 <= count_fail8 + 1; + else count_fail8 <= count_fail8 + 1; // Test 9 / 10: async vs sync divergence hook -- identical encoding must // produce identical fail counts under current implementation assert property (@(posedge clk) disable iff (cyc < 2) accept_on (cnd_a) body) - else count_fail9 <= count_fail9 + 1; + else count_fail9 <= count_fail9 + 1; assert property (@(posedge clk) disable iff (cyc < 2) sync_accept_on (cnd_a) body) - else count_fail10 <= count_fail10 + 1; + else count_fail10 <= count_fail10 + 1; always @(posedge clk) begin `ifdef TEST_VERBOSE - $write("[%0t] cyc==%0d crc=%x body=%b cnd_a=%b cnd_r=%b cnd=%b\n", - $time, cyc, crc, body, cnd_a, cnd_r, cnd); + $write("[%0t] cyc==%0d crc=%x body=%b cnd_a=%b cnd_r=%b cnd=%b\n", $time, cyc, crc, body, + cnd_a, cnd_r, cnd); `endif cyc <= cyc + 1; crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; @@ -94,16 +92,16 @@ module t ( end else if (cyc == 99) begin `checkh(crc, 64'hc77bb9b3784ea091); - `checkd(count_fail1, 28); // Other sims: 14, one other: 15 + `checkd(count_fail1, 14); `checkd(count_fail2, 64); // One other sim: 66 - `checkd(count_fail3, 28); // Other sims: 14 + `checkd(count_fail3, 14); `checkd(count_fail4, 64); - `checkd(count_fail5, 45); // Other sims: 31, one other: 32 - `checkd(count_fail6, 64); // Other sims: 59, one other: 60 - `checkd(count_fail7, 28); // Other sims: 14, one other: 15 - `checkd(count_fail8, 13); // Other sims: 10 - `checkd(count_fail9, 28); // Other sims: 14, one other: 15 - `checkd(count_fail10, 28); // Other sims: 14 + `checkd(count_fail5, 31); // One other sim: 32 + `checkd(count_fail6, 59); // One other sim: 60 + `checkd(count_fail7, 14); // One other sim: 15 + `checkd(count_fail8, 10); + `checkd(count_fail9, 14); // One other sim: 15 + `checkd(count_fail10, 14); $write("*-* All Finished *-*\n"); $finish; end diff --git a/test_regress/t/t_property_nfa_msgs_unsup.out b/test_regress/t/t_property_nfa_msgs_unsup.out new file mode 100644 index 000000000..5cdbf6675 --- /dev/null +++ b/test_regress/t/t_property_nfa_msgs_unsup.out @@ -0,0 +1,52 @@ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:26:63: Unsupported: temporal property if/case with a pass action + : ... note: In instance 't' + 26 | assert property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c) $display("pass"); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:27:62: Unsupported: temporal property if/case with cover + : ... note: In instance 't' + 27 | cover property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:28:68: Unsupported: temporal property if/case with negation + : ... note: In instance 't' + 28 | assert property (@(posedge clk) not (if (a) 1'b1 ##1 b else 1'b1 ##2 c)); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:30:35: Unsupported: temporal property if/case with a pass action + : ... note: In instance 't' + 30 | assert property (@(posedge clk) case (a) 1'b0: 1'b1 ##1 b; 1'b1: 1'b1 ##2 c; default: 1'b1 ##1 d; + | ^~~~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:35:65: Unsupported: multi-cycle sequence expression inside consecutive repetition (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 35 | assert property (@(posedge clk) sync_accept_on (a) ((b ##1 c) [* 2])); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:38:52: Unsupported: multi-cycle sequence expression inside consecutive repetition (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 38 | assert property (@(posedge clk) if (a) ((b ##1 c)[*2]) else d) $display("pass"); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:41:3: Unsupported: property instance inside a multi-cycle property expression + : ... note: In instance 't' + 41 | assert property (@(posedge clk) p_nested or e); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:59:52: Unsupported: ranged cycle delay in an operand of property 'and' + 59 | assert property (@(posedge clk) (1'b1 ##[1:2] b) and c); + | ^~~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:60:37: Unsupported: ranged cycle delay in an operand of property 'and' + 60 | assert property (@(posedge clk) c and (1'b1 ##[1:2] b)); + | ^~~ +%Warning-COVERIGN: t/t_property_nfa_msgs_unsup.v:63:45: Ignoring unsupported: cover sequence with a sequence operand of 'or' + 63 | cover sequence (@(posedge clk) ((a and b) or(c ##1 d))); + | ^~ + ... For warning description see https://verilator.org/warn/COVERIGN?v=latest + ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message. +%Error: t/t_property_nfa_msgs_unsup.v:56:22: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context + 56 | assert property (a [* 2]); + | ^~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_property_nfa_msgs_unsup.v:56:3: Concurrent assertion has no clock (IEEE 1800-2023 16.16) + : ... note: In instance 't' + : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context + 56 | assert property (a [* 2]); + | ^~~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_property_nfa_msgs_unsup.py b/test_regress/t/t_property_nfa_msgs_unsup.py new file mode 100755 index 000000000..d043caa09 --- /dev/null +++ b/test_regress/t/t_property_nfa_msgs_unsup.py @@ -0,0 +1,33 @@ +#!/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 glob +import json +import vltest_bootstrap + +test.scenarios('vlt') + +test.lint(expect_filename=test.golden_filename, + verilator_flags2=[ + '--assert', '--timing', '--error-limit', '100', '--dumpi-tree', '3', + '--dumpi-tree-json', '3', '--no-json-edit-nums' + ], + fails=True) + +test.file_grep_any(glob.glob(test.obj_dir + "/V" + test.name + "_*.tree"), + r'SAND.*\[PROPERTY_CONTROL\]') + +jsons = glob.glob(test.obj_dir + "/V" + test.name + "_*.tree.json") +if not jsons: + test.error("No .tree.json dumped") +for fn in jsons: + with open(fn, 'r', encoding="utf8") as fh: + json.load(fh) + +test.passes() diff --git a/test_regress/t/t_property_nfa_msgs_unsup.v b/test_regress/t/t_property_nfa_msgs_unsup.v new file mode 100644 index 000000000..e8d7ad73a --- /dev/null +++ b/test_regress/t/t_property_nfa_msgs_unsup.v @@ -0,0 +1,65 @@ +// 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 + +// Each property exercises one unsupported-diagnostic path of the NFA lowering + +module t ( + input clk +); + + bit a = 0, b = 0, c = 0, d = 0, e = 0; + + property p_nested; + a ##1 b; + endproperty + + sequence s_nested; a ##1 b; endsequence + + function automatic bit fbool(); + return a; + endfunction + + // Property if/else control the fail-only count engine cannot lower + assert property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c) $display("pass"); + cover property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c); + assert property (@(posedge clk) not (if (a) 1'b1 ##1 b else 1'b1 ##2 c)); + + assert property (@(posedge clk) case (a) 1'b0: 1'b1 ##1 b; 1'b1: 1'b1 ##2 c; default: 1'b1 ##1 d; + endcase) + $display("pass"); + + // An unsupported body under an abort reports itself, not an internal error + assert property (@(posedge clk) sync_accept_on (a) ((b ##1 c) [* 2])); + + // A body the builder rejects wins over the property if/case message + assert property (@(posedge clk) if (a) ((b ##1 c)[*2]) else d) $display("pass"); + + // A named property instance nested in a composite is rejected, not dropped + assert property (@(posedge clk) p_nested or e); + + // A named sequence instance is inlined, not rejected + assert property (@(posedge clk) s_nested or e); + + // A function call is not a property instance + assert property (@(posedge clk) fbool() ##1 b); + + // A user-written 'and' of implications is not a property if/case + assert property (@(posedge clk) (a |-> 1'b1 ##1 b) and(c |-> 1'b1 ##2 d)); + + // Property if/else without an action is lowered, not rejected + assert property (@(posedge clk) if (a) 1'b1 ##1 b else 1'b1 ##2 c); + + // A multi-cycle property with no clocking event is left to later passes + assert property (a [* 2]); + + // An 'and' operand carrying mid-window sources defers to later passes + assert property (@(posedge clk) (1'b1 ##[1:2] b) and c); + assert property (@(posedge clk) c and (1'b1 ##[1:2] b)); + + // A boolean 'and' operand of a rejected cover-sequence 'or' is freed + cover sequence (@(posedge clk) ((a and b) or(c ##1 d))); + +endmodule