From 06ee8b7261de568e8e3eefbb277cdae0f77de4cc Mon Sep 17 00:00:00 2001 From: Artur Bieniek Date: Wed, 19 Aug 2026 08:05:05 +0200 Subject: [PATCH] Use unsigned in NFA, guard against overflow using V3Width. (#8152) Signed-off-by: Artur Bieniek --- src/V3AssertNfa.cpp | 135 +++++++----------- src/V3Width.cpp | 55 ++++++- test_regress/t/t_assert_rep_bad_count.out | 32 +++-- test_regress/t/t_assert_rep_bad_count.v | 6 + test_regress/t/t_property_sexpr2_bad.out | 5 + test_regress/t/t_property_sexpr2_bad.v | 2 + .../t/t_property_sexpr_range_delay_bad.out | 9 ++ .../t/t_property_sexpr_range_delay_bad.v | 3 + 8 files changed, 150 insertions(+), 97 deletions(-) diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6e12bba61..f235e56b8 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -72,7 +72,7 @@ public: 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. + unsigned 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; @@ -324,7 +324,7 @@ class SvaNfaBuilder final { struct RangeDelayRejectInfo final { SvaStateVertex* startp = nullptr; - int range = 0; + unsigned range = 0; int rhsLen = 0; }; @@ -354,10 +354,10 @@ class SvaNfaBuilder final { return guardp; } - static int getConstInt(AstNodeExpr* exprp) { + static unsigned getConstUInt(AstNodeExpr* exprp) { AstNodeExpr* const constp = V3Const::constifyEdit(exprp->cloneTreePure(false)); const AstConst* const cp = VN_CAST(constp, Const); - const int val = cp ? cp->toSInt() : -1; + const unsigned val = cp ? cp->toUInt() : 0; VL_DO_DANGLING(constp->deleteTree(), constp); return val; } @@ -379,16 +379,15 @@ class SvaNfaBuilder final { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay); if (!delayp || !delayp->isCycleDelay()) return -1; - int delayCycles = -1; + unsigned delayCycles; if (delayp->isRangeDelay()) { if (delayp->isUnbounded()) return -1; // LCOV_EXCL_LINE - const int minD = getConstInt(delayp->lhsp()); - const int maxD = getConstInt(delayp->rhsp()); - if (minD < 0 || maxD < 0 || minD != maxD) return -1; + const unsigned minD = getConstUInt(delayp->lhsp()); + const unsigned maxD = getConstUInt(delayp->rhsp()); + if (minD != maxD) return -1; delayCycles = minD; } else { - delayCycles = getConstInt(delayp->lhsp()); - if (delayCycles < 0) return -1; // LCOV_EXCL_LINE + delayCycles = getConstUInt(delayp->lhsp()); } int preLen = 0; if (AstNodeExpr* const prep = sexprp->preExprp()) { @@ -439,13 +438,11 @@ class SvaNfaBuilder final { std::pair delayRange; if (delayp->isRangeDelay()) { if (delayp->isUnbounded()) return {-1, -1}; - const int minD = getConstInt(delayp->lhsp()); - const int maxD = getConstInt(delayp->rhsp()); - if (minD < 0 || maxD < 0 || maxD < minD) return {-1, -1}; + const unsigned minD = getConstUInt(delayp->lhsp()); + const unsigned maxD = getConstUInt(delayp->rhsp()); delayRange = {minD, maxD}; } else { - const int d = getConstInt(delayp->lhsp()); - if (d < 0) return {-1, -1}; + const unsigned d = getConstUInt(delayp->lhsp()); delayRange = {d, d}; } std::pair preRange{0, 0}; @@ -478,15 +475,15 @@ class SvaNfaBuilder final { AstDelay* rangeDelayp = nullptr; clonep->foreach([&](AstDelay* dp) { if (!rangeDelayp && dp->isRangeDelay() && !dp->isUnbounded() - && getConstInt(dp->lhsp()) != getConstInt(dp->rhsp())) { + && getConstUInt(dp->lhsp()) != getConstUInt(dp->rhsp())) { rangeDelayp = dp; } }); if (rangeDelayp) { FileLine* const flp = rangeDelayp->fileline(); - const int pinned = getConstInt(rangeDelayp->lhsp()) + (len - lo); + const unsigned pinned = getConstUInt(rangeDelayp->lhsp()) + (len - lo); AstNodeExpr* const oldMinp = rangeDelayp->lhsp(); - oldMinp->replaceWith(new AstConst{flp, static_cast(pinned)}); + oldMinp->replaceWith(new AstConst{flp, pinned}); VL_DO_DANGLING(oldMinp->deleteTree(), oldMinp); // Drop the max bound so it lowers as a fixed `##d`, not `##[d:d]`. AstNode* const oldMaxp = rangeDelayp->rhsp()->unlinkFrBack(); @@ -501,8 +498,8 @@ class SvaNfaBuilder final { // any exprp -- even an impure one would now evaluate exactly once per // clock instead of N times. Orphan temps from failed builds are unused // MODULETEMPs and are removed by V3Dead. - AstVar* tryHoistSampled(AstNodeExpr* exprp, FileLine* flp, int cloneCount) { - constexpr int kHoistThreshold = 2; + AstVar* tryHoistSampled(AstNodeExpr* exprp, FileLine* flp, unsigned cloneCount) { + constexpr unsigned kHoistThreshold = 2; if (cloneCount < kHoistThreshold) return nullptr; AstVar* const tempVarp = new AstVar{flp, VVarType::MODULETEMP, m_propTempNames.get(exprp), exprp->dtypep()}; @@ -520,9 +517,9 @@ class SvaNfaBuilder final { // 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, int requested) { + static bool exceedsAssertUnrollLimit(AstNode* nodep, unsigned requested) { const int limit = v3Global.opt.assertUnrollLimit(); - if (requested <= limit) return false; + 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"); @@ -556,7 +553,7 @@ class SvaNfaBuilder final { return m_graph.addClockedEdge(fromp, top, throughoutCond(nullptr, flp)); } - SvaStateVertex* addDelayChain(SvaStateVertex* startp, int size, FileLine* flp, + SvaStateVertex* addDelayChain(SvaStateVertex* startp, unsigned size, FileLine* flp, bool isFixed = true, AstNodeExpr* clearCondp = nullptr) { if (isFixed && size == 0) return startp; UASSERT_OBJ(size > 0, startp, "Delay chain needs at least one slot"); @@ -587,13 +584,7 @@ class SvaNfaBuilder final { bool applyRangeDelay(AstDelay* delayp, AstNodeExpr* rhsExprp, SvaStateVertex*& currentp, std::vector& midSources, FileLine* flp, bool& outErrorEmitted, RangeDelayRejectInfo* rangeRejectInfop = nullptr) { - const int minDelay = getConstInt(delayp->lhsp()); - if (minDelay < 0) { - delayp->v3error("Range delay minimum is not a non-negative elaboration-time constant" - " (IEEE 1800-2023 16.7)"); - outErrorEmitted = true; - return false; - } + const unsigned minDelay = getConstUInt(delayp->lhsp()); if (delayp->isUnbounded()) { // `##[M:$]`: wait M cycles, then self-loop waiting for the match // condition. Unbounded = liveness, so no reject. @@ -603,29 +594,18 @@ class SvaNfaBuilder final { m_inUnboundedScope = true; return true; } - const int maxDelay = getConstInt(delayp->rhsp()); - if (maxDelay < 0) { - delayp->v3error("Range delay maximum is not a non-negative elaboration-time constant" - " (IEEE 1800-2023 16.7)"); - outErrorEmitted = true; - return false; - } - if (maxDelay < minDelay) { - delayp->v3error("Range delay maximum must be >= minimum (IEEE 1800-2023 16.7)"); - outErrorEmitted = true; - return false; - } + const unsigned maxDelay = getConstUInt(delayp->rhsp()); if (minDelay == maxDelay) { currentp = addDelayChain(currentp, minDelay, flp); return true; } - const int range = maxDelay - minDelay; + const unsigned range = maxDelay - minDelay; currentp = addDelayChain(currentp, minDelay, flp); // kChainLimit bounds per-attempt unrolled vertices. Above this, a // ring buffer (constant-size state) is used instead, so the vertex // count is O(1) in range regardless of user input; no adversarial N // blowup is possible. - constexpr int kChainLimit = 256; + constexpr unsigned kChainLimit = 256; // IEEE 1800-2023 16.14.3: only a small bounded range before a plain // boolean enumerates every end-of-match below. The counter FSM drops // overlapping ends and the nested-sequence merge collapses them, so @@ -636,7 +616,7 @@ class SvaNfaBuilder final { return false; } if (range > kChainLimit) { - currentp = addDelayChain(currentp, range + 1, flp, false, + currentp = addDelayChain(currentp, range + 1U, flp, false, rhsExprp->isMultiCycleSva() ? nullptr : rhsExprp); } else if (VN_IS(rhsExprp, SExpr)) { // Nested-SExpr RHS: merge all [M,N] positions. Candidate-local misses @@ -648,7 +628,7 @@ class SvaNfaBuilder final { SvaStateVertex* const mergeVtxp = scopedCreateVertex(); mergeVtxp->m_isUnbounded = true; guardedLink(currentp, mergeVtxp, flp); - for (int i = 0; i < range; ++i) { + for (unsigned i = 0; i < range; ++i) { SvaStateVertex* const nextVtxp = scopedCreateVertex(); guardedEdge(currentp, nextVtxp, flp); guardedLink(nextVtxp, mergeVtxp, flp); @@ -665,7 +645,7 @@ class SvaNfaBuilder final { AstVar* const hoistVarp = m_isCoverSeq ? nullptr : tryHoistSampled(rhsExprp, flp, range); midSources.push_back(currentp); - for (int i = 0; i < range; ++i) { + for (unsigned i = 0; i < range; ++i) { SvaStateVertex* const nextVtxp = scopedCreateVertex(); if (m_isCoverSeq) { guardedEdge(currentp, nextVtxp, flp); @@ -697,7 +677,7 @@ class SvaNfaBuilder final { guardedLink(srcp, successNowp, condp, flp); SvaStateVertex* stagep = successNowp; guardedLink(stagep, expiryMatchp, flp); - for (int i = 0; i < info.range; ++i) { + for (unsigned i = 0; i < info.range; ++i) { SvaStateVertex* const nextp = scopedCreateVertex(); guardedEdge(stagep, nextp, flp); stagep = nextp; @@ -751,13 +731,7 @@ class SvaNfaBuilder final { return BuildResult::fail(errorEmitted); } } else { - const int delayCycles = getConstInt(delayp->lhsp()); - if (delayCycles < 0) { - delayp->v3error("Delay value is not a non-negative" - " elaboration-time constant" - " (IEEE 1800-2023 16.7)"); - return BuildResult::failWithError(); - } + const unsigned delayCycles = getConstUInt(delayp->lhsp()); currentp = addDelayChain(currentp, delayCycles, flp); } @@ -780,16 +754,15 @@ class SvaNfaBuilder final { " consecutive repetition (IEEE 1800-2023 16.9.2)"); return BuildResult::failWithError(); } - const int minN = getConstInt(repp->countp()); - UASSERT_OBJ(minN >= 0, repp, "ConsRep count must be non-negative (V3Width invariant)"); + const unsigned minN = getConstUInt(repp->countp()); // Sum sites across prefix + unbounded/range tail so one hoist covers // every check edge of this repetition. - int totalSites = minN; + unsigned totalSites = minN; if (repp->unbounded()) { totalSites += 1; } else if (repp->maxCountp()) { - totalSites += getConstInt(repp->maxCountp()) - minN; + totalSites += getConstUInt(repp->maxCountp()) - minN; } if (exceedsAssertUnrollLimit(repp, totalSites)) return BuildResult::failWithError(); AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites); @@ -799,7 +772,7 @@ class SvaNfaBuilder final { std::vector consMidSources; SvaStateVertex* currentp = entryVtxp; - for (int i = 0; i < minN; ++i) { + for (unsigned i = 0; i < minN; ++i) { if (i > 0) { SvaStateVertex* const nextp = scopedCreateVertex(); guardedEdge(currentp, nextp, flp); @@ -838,11 +811,10 @@ class SvaNfaBuilder final { currentp->m_isUnbounded = true; m_inUnboundedScope = true; } else if (repp->maxCountp()) { - const int maxN = getConstInt(repp->maxCountp()); - UASSERT_OBJ(maxN >= minN, repp, "ConsRep range max < min (V3Width invariant)"); + const unsigned maxN = getConstUInt(repp->maxCountp()); SvaStateVertex* const mergeVtxp = scopedCreateVertex(); guardedLink(currentp, mergeVtxp, flp); - for (int i = minN; i < maxN; ++i) { + for (unsigned i = minN; i < maxN; ++i) { SvaStateVertex* const nextVtxp = scopedCreateVertex(); guardedEdge(currentp, nextVtxp, flp); SvaStateVertex* const checkVtxp = scopedCreateVertex(); @@ -869,7 +841,7 @@ class SvaNfaBuilder final { bool isTopLevelStep = false) { FileLine* const flp = nodep->fileline(); AstNodeExpr* const propp = nodep->propp(); - const int lo = getConstInt(nodep->loBoundp()); + const unsigned lo = getConstUInt(nodep->loBoundp()); if (VN_IS(nodep->hiBoundp(), Unbounded)) { // Weak always [lo:$]: unbounded upper bound (IEEE 1800-2023 16.12.11). // p must hold at every clock tick at least lo cycles after the attempt @@ -877,8 +849,7 @@ class SvaNfaBuilder final { // end-of-trace obligation (weak). The self-loop keeps the attempt live // every cycle; each observed cycle is a safety obligation, so a false p // rejects immediately. - UASSERT_OBJ(!nodep->isStrong() && lo >= 0, nodep, - "Unbounded always must be weak with non-negative lo (V3Width)"); + UASSERT_OBJ(!nodep->isStrong(), nodep, "Unbounded always must be weak (V3Width)"); SvaStateVertex* const livep = addDelayChain(entryVtxp, lo, flp); livep->m_isUnbounded = true; guardedEdge(livep, livep, flp); // stay active every subsequent cycle @@ -889,8 +860,7 @@ class SvaNfaBuilder final { if (isTopLevelStep) rejEdgep->m_rejectOnFail = true; return {livep, nullptr, {}}; } - const int hi = getConstInt(nodep->hiBoundp()); - UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)"); + const unsigned hi = getConstUInt(nodep->hiBoundp()); // Strong s_always[m:n]: mark every in-window registered vertex so an // attempt still mid-window at end-of-simulation is reported as a liveness // failure (IEEE strong: the n+1 ticks must exist). An attempt that has @@ -917,11 +887,10 @@ class SvaNfaBuilder final { BuildResult buildGotoRep(AstSGotoRep* repp, SvaStateVertex* entryVtxp) { FileLine* const flp = repp->fileline(); AstNodeExpr* const exprp = repp->exprp(); - const int minN = getConstInt(repp->countp()); - if (minN <= 0) return BuildResult::fail(); + const unsigned minN = getConstUInt(repp->countp()); + if (minN == 0) return BuildResult::fail(); const bool hasMax = repp->maxCountp() != nullptr; - const int maxN = hasMax ? getConstInt(repp->maxCountp()) : minN; - UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)"); + const unsigned maxN = hasMax ? getConstUInt(repp->maxCountp()) : minN; if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError(); if (m_isCoverSeq) { @@ -935,10 +904,10 @@ class SvaNfaBuilder final { // 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, 2 * maxN); + AstVar* const hoistVarp = tryHoistSampled(exprp, flp, 2U * maxN); SvaStateVertex* currentp = entryVtxp; // Build minN match-wait chains to reach the first accept point. - for (int i = 0; i < minN; ++i) { + 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 @@ -961,7 +930,7 @@ class SvaNfaBuilder final { // buildConsRep's range fan-out. SvaStateVertex* const mergeVtxp = scopedCreateVertex(); guardedLink(currentp, mergeVtxp, flp); // accept at match_M - for (int i = minN; i < maxN; ++i) { + for (unsigned i = minN; i < maxN; ++i) { SvaStateVertex* const waitVtxp = scopedCreateVertex(); guardedEdge(currentp, waitVtxp, flp); AstNodeExpr* const waitCondp @@ -1172,9 +1141,9 @@ class SvaNfaBuilder final { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay); if (!delayp || !delayp->isCycleDelay() || delayp->isUnbounded()) return false; - const int delayCycles = getConstInt(delayp->lhsp()); - if (delayCycles < 0) return false; - if (delayp->isRangeDelay() && getConstInt(delayp->rhsp()) != delayCycles) return false; + const unsigned delayCycles = getConstUInt(delayp->lhsp()); + if (delayp->isRangeDelay() && getConstUInt(delayp->rhsp()) != delayCycles) + return false; int preLen = 0; if (AstNodeExpr* const prep = sexprp->preExprp()) { if (!flattenFixedSeq(prep, baseOffset, out)) return false; @@ -1246,7 +1215,7 @@ class SvaNfaBuilder final { AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay); if (!delayp || !delayp->isCycleDelay() || !delayp->isRangeDelay() || delayp->isUnbounded()) return {}; - if (getConstInt(delayp->lhsp()) == getConstInt(delayp->rhsp())) return {}; + if (getConstUInt(delayp->lhsp()) == getConstUInt(delayp->rhsp())) return {}; AstNodeExpr* const prep = sexprp->preExprp(); if (prep && fixedLength(prep) != 0) return {}; if (fixedLength(sexprp->exprp()) != 0) return {}; @@ -3036,7 +3005,7 @@ class AssertNfaVisitor final : public VNVisitor { // Replace one VarRef to a captured local var with $past(rhs, K) // (or rhs inline when K == 0). No-op if refp is not in matchMap. - void substituteMatchItemRef(AstVarRef* refp, int K, + void substituteMatchItemRef(AstVarRef* refp, unsigned K, const std::unordered_map& matchMap) { const auto it = matchMap.find(refp->varp()); if (it == matchMap.end()) return; @@ -3057,7 +3026,7 @@ class AssertNfaVisitor final : public VNVisitor { // substitutes each VarRef to a captured local var with $past(rhs, K) // (or rhs inline when K == 0). Reports E_UNSUPPORTED on non-constant // delays or composite sequence operators. - int walkSubstituteMatchItems(AstNodeExpr* nodep, int K, + int walkSubstituteMatchItems(AstNodeExpr* nodep, unsigned K, const std::unordered_map& matchItems, bool& errorEmitted) { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { @@ -3075,7 +3044,7 @@ class AssertNfaVisitor final : public VNVisitor { errorEmitted = true; return -1; } - const int delayCycles = VN_AS(delayp->lhsp(), Const)->toSInt(); + const unsigned delayCycles = VN_AS(delayp->lhsp(), Const)->toUInt(); int preLen = 0; if (AstNodeExpr* const prep = sexprp->preExprp()) { preLen = walkSubstituteMatchItems(prep, K, matchItems, errorEmitted); @@ -3121,7 +3090,7 @@ class AssertNfaVisitor final : public VNVisitor { AstVarRef* const lhsRefp = VN_AS(assignp->lhsp(), VarRef); matchItems[lhsRefp->varp()] = assignp->rhsp(); } - const int startK = parts.isOverlapped ? 0 : 1; + const unsigned startK = parts.isOverlapped ? 0 : 1; bool errorEmitted = false; walkSubstituteMatchItems(seqBodyp, startK, matchItems, errorEmitted); // Match-item substitution / strip mutates ancestor purity. Release diff --git a/src/V3Width.cpp b/src/V3Width.cpp index f87dc9ddb..f5e6a7d06 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -744,15 +744,39 @@ class WidthVisitor final : public VNVisitor { // it's like an if() condition. iterateCheckBool(nodep, "default disable iff condition", nodep->condp(), BOTH); } + static const AstConst* widthCheckSvaDelayBound(AstDelay* nodep, AstNodeExpr* boundp, + const char* what) { + const AstConst* const constp = VN_CAST(boundp, Const); + if (!constp || (constp->dtypep()->isSigned() && constp->num().isNegative())) { + nodep->v3error(what << " is not a non-negative elaboration-time constant" + " (IEEE 1800-2023 16.7)"); + return nullptr; + } + if (constp->num().mostSetBitP1() > 31) { + nodep->v3warn( + E_UNSUPPORTED, + "Unsupported: SVA cycle delay exceeds implementation limit of 2147483647"); + return nullptr; + } + return constp; + } void visit(AstDelay* nodep) override { if (nodep->isCycleDelay() && m_underSExpr) { // Fold parameterized SVA cycle-delay bounds userIterateAndNext(nodep->lhsp(), WidthVP{SELF, BOTH}.p()); V3Const::constifyParamsNoWarnEdit(nodep->lhsp()); + const AstConst* const minConstp = widthCheckSvaDelayBound( + nodep, nodep->lhsp(), + nodep->isRangeDelay() ? "Range delay minimum" : "Delay value"); if (nodep->rhsp() && !nodep->isUnbounded()) { // Fold parametrized SVA cycle-delay max bound userIterateAndNext(nodep->rhsp(), WidthVP{SELF, BOTH}.p()); V3Const::constifyParamsNoWarnEdit(nodep->rhsp()); + const AstConst* const maxConstp + = widthCheckSvaDelayBound(nodep, nodep->rhsp(), "Range delay maximum"); + if (minConstp && maxConstp && maxConstp->toUInt() < minConstp->toUInt()) { + nodep->v3error("Range delay maximum must be >= minimum (IEEE 1800-2023 16.7)"); + } } return; } @@ -1832,7 +1856,11 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); - if (nodep->maxCountp()) widthCheckGotoRepRange(nodep, "Goto"); + if (nodep->maxCountp()) { + widthCheckGotoRepRange(nodep, "Goto"); + } else { + widthCheckRepCount(nodep); + } nodep->dtypeSetBit(); } } @@ -1841,10 +1869,33 @@ class WidthVisitor final : public VNVisitor { if (m_vup->prelim()) { iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); - if (nodep->maxCountp()) widthCheckGotoRepRange(nodep, "Nonconsecutive"); + if (nodep->maxCountp()) { + widthCheckGotoRepRange(nodep, "Nonconsecutive"); + } else { + widthCheckRepCount(nodep); + } nodep->dtypeSetBit(); } } + template + void widthCheckRepCount(T_Rep* nodep) { + V3Const::constifyParamsNoWarnEdit(nodep->countp()); + const AstConst* const constp = VN_CAST(nodep->countp(), Const); + if (!constp) { + nodep->v3error("Repetition count is not an elaboration-time constant" + " (IEEE 1800-2023 16.9.2)"); + } else if (constp->dtypep()->isSigned() && constp->num().isNegative()) { + nodep->v3error("Repetition count must be non-negative" + " (IEEE 1800-2023 16.9.2)"); + } else if (constp->num().mostSetBitP1() > 31) { + nodep->v3warn( + E_UNSUPPORTED, + "Unsupported: SVA repetition count exceeds implementation limit of 2147483647"); + } else if (constp->isZero()) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: zero repetition count" + " (IEEE 1800-2023 16.9.2)"); + } + } // IEEE 1800-2023 16.9.2 range-form bound validation for goto/nonconsec. // Parent accessors are re-fetched after constifyParamsEdit because that // call can replace the node in-tree (Lesson: AstSConsRep visitor pattern). diff --git a/test_regress/t/t_assert_rep_bad_count.out b/test_regress/t/t_assert_rep_bad_count.out index 787e79d93..fb6c5c7e6 100644 --- a/test_regress/t/t_assert_rep_bad_count.out +++ b/test_regress/t/t_assert_rep_bad_count.out @@ -1,27 +1,35 @@ -%Error: t/t_assert_rep_bad_count.v:14:42: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) +%Error: t/t_assert_rep_bad_count.v:14:36: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) : ... note: In instance 't' 14 | assert property (@(posedge clk) a[->n] |-> b) - | ^~~ + | ^~~ ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:18:42: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2) +%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:18:36: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2) : ... note: In instance 't' 18 | assert property (@(posedge clk) a[->0] |-> b) - | ^~~ + | ^~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error: t/t_assert_rep_bad_count.v:22:43: Repetition count must be non-negative (IEEE 1800-2023 16.9.2) +%Error: t/t_assert_rep_bad_count.v:22:36: Repetition count must be non-negative (IEEE 1800-2023 16.9.2) : ... note: In instance 't' 22 | assert property (@(posedge clk) a[->-1] |-> b) - | ^~~ -%Error: t/t_assert_rep_bad_count.v:28:41: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) + | ^~~ +%Error: t/t_assert_rep_bad_count.v:28:36: Repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) : ... note: In instance 't' 28 | assert property (@(posedge clk) a[=n] |-> b) - | ^~~ -%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:32:41: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2) + | ^~ +%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:32:36: Unsupported: zero repetition count (IEEE 1800-2023 16.9.2) : ... note: In instance 't' 32 | assert property (@(posedge clk) a[=0] |-> b) - | ^~~ -%Error: t/t_assert_rep_bad_count.v:36:42: Repetition count must be non-negative (IEEE 1800-2023 16.9.2) + | ^~ +%Error: t/t_assert_rep_bad_count.v:36:36: Repetition count must be non-negative (IEEE 1800-2023 16.9.2) : ... note: In instance 't' 36 | assert property (@(posedge clk) a[=-1] |-> b) - | ^~~ + | ^~ +%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:39:36: Unsupported: SVA repetition count exceeds implementation limit of 2147483647 + : ... note: In instance 't' + 39 | assert property (@(posedge clk) a[->32'h80000000] |-> b) + | ^~~ +%Error-UNSUPPORTED: t/t_assert_rep_bad_count.v:42:36: Unsupported: SVA repetition count exceeds implementation limit of 2147483647 + : ... note: In instance 't' + 42 | assert property (@(posedge clk) a[=32'h80000000] |-> b) + | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_assert_rep_bad_count.v b/test_regress/t/t_assert_rep_bad_count.v index 79e38c77d..94618ea5c 100644 --- a/test_regress/t/t_assert_rep_bad_count.v +++ b/test_regress/t/t_assert_rep_bad_count.v @@ -36,4 +36,10 @@ module t (input clk); assert property (@(posedge clk) a[=-1] |-> b) else $error("FAIL"); + assert property (@(posedge clk) a[->32'h80000000] |-> b) + else $error("FAIL"); + + assert property (@(posedge clk) a[=32'h80000000] |-> b) + else $error("FAIL"); + endmodule diff --git a/test_regress/t/t_property_sexpr2_bad.out b/test_regress/t/t_property_sexpr2_bad.out index 533f7550b..2990fa446 100644 --- a/test_regress/t/t_property_sexpr2_bad.out +++ b/test_regress/t/t_property_sexpr2_bad.out @@ -7,4 +7,9 @@ : ... note: In instance 't' 21 | assert property (@(posedge clk) ##(1+clk) val); | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr2_bad.v:23:35: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647 + : ... note: In instance 't' + 23 | assert property (@(posedge clk) ##32'h80000000 val); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr2_bad.v b/test_regress/t/t_property_sexpr2_bad.v index c927cc466..f94db4da1 100644 --- a/test_regress/t/t_property_sexpr2_bad.v +++ b/test_regress/t/t_property_sexpr2_bad.v @@ -19,4 +19,6 @@ module t ( /*AUTOARG*/ assert property (@(posedge clk) ##clk val); assert property (@(posedge clk) ##(1+clk) val); + + assert property (@(posedge clk) ##32'h80000000 val); endmodule diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.out b/test_regress/t/t_property_sexpr_range_delay_bad.out index 257fd0109..afc85c949 100644 --- a/test_regress/t/t_property_sexpr_range_delay_bad.out +++ b/test_regress/t/t_property_sexpr_range_delay_bad.out @@ -19,4 +19,13 @@ : ... note: In instance 't' 34 | a6: assert property (@(posedge clk) a |-> ##[NEG:$] b); | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:36:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647 + : ... note: In instance 't' + 36 | a7: assert property (@(posedge clk) a |-> ##[1:32'h80000000] b); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:37:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647 + : ... note: In instance 't' + 37 | a8: assert property (@(posedge clk) a |-> ##[32'h80000000:$] b); + | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.v b/test_regress/t/t_property_sexpr_range_delay_bad.v index 91ae69e9a..0188ca685 100644 --- a/test_regress/t/t_property_sexpr_range_delay_bad.v +++ b/test_regress/t/t_property_sexpr_range_delay_bad.v @@ -33,4 +33,7 @@ module t; localparam int NEG = -1; a6: assert property (@(posedge clk) a |-> ##[NEG:$] b); + a7: assert property (@(posedge clk) a |-> ##[1:32'h80000000] b); + a8: assert property (@(posedge clk) a |-> ##[32'h80000000:$] b); + endmodule