From c7ad617b10b12d920883aba02b5f1a76551379ec Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Sun, 5 Apr 2026 00:42:11 +0200 Subject: [PATCH] extend consecutive repetition support [*N:M]/[+]/[*] in sequence expressions --- src/V3AssertPre.cpp | 6 +- src/V3AssertProp.cpp | 241 ++++++++++++++++++ src/V3AstNodeExpr.h | 35 ++- src/V3AstNodes.cpp | 8 + src/V3Width.cpp | 25 +- src/verilog.y | 27 +- .../t/t_assert_prop_consec_rep_bad.out | 30 ++- test_regress/t/t_assert_prop_consec_rep_bad.v | 17 +- .../t_assert_prop_consec_rep_delay_unsup.out | 6 + .../t/t_assert_prop_consec_rep_delay_unsup.py | 16 ++ .../t/t_assert_prop_consec_rep_delay_unsup.v | 13 + .../t/t_assert_prop_consec_rep_range_bad.out | 6 + .../t/t_assert_prop_consec_rep_range_bad.py | 16 ++ .../t/t_assert_prop_consec_rep_range_bad.v | 13 + .../t_assert_prop_consec_rep_trail_unsup.out | 6 + .../t/t_assert_prop_consec_rep_trail_unsup.py | 16 ++ .../t/t_assert_prop_consec_rep_trail_unsup.v | 13 + 17 files changed, 459 insertions(+), 35 deletions(-) create mode 100644 test_regress/t/t_assert_prop_consec_rep_delay_unsup.out create mode 100755 test_regress/t/t_assert_prop_consec_rep_delay_unsup.py create mode 100644 test_regress/t/t_assert_prop_consec_rep_delay_unsup.v create mode 100644 test_regress/t/t_assert_prop_consec_rep_range_bad.out create mode 100755 test_regress/t/t_assert_prop_consec_rep_range_bad.py create mode 100644 test_regress/t/t_assert_prop_consec_rep_range_bad.v create mode 100644 test_regress/t/t_assert_prop_consec_rep_trail_unsup.out create mode 100755 test_regress/t/t_assert_prop_consec_rep_trail_unsup.py create mode 100644 test_regress/t/t_assert_prop_consec_rep_trail_unsup.v diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 1417a8460..a1f4583e5 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -657,9 +657,10 @@ private: nodep->sentreep(newSenTree(nodep)); } void visit(AstConsRep* nodep) override { - // IEEE 1800-2023 16.9.2 -- Lower consecutive repetition [*N] - // Saturating counter tracks consecutive true cycles; avoids O(N) $past tree. + // IEEE 1800-2023 16.9.2 -- Lower standalone exact [*N] (N >= 2) via saturating counter. + // Range/unbounded forms and SExpr-contained forms are lowered by V3AssertProp. iterateChildren(nodep); + if (nodep->unbounded() || nodep->maxCountp()) return; // Handled by V3AssertProp const AstConst* const constp = VN_CAST(nodep->countp(), Const); if (VL_UNLIKELY(!constp || constp->toSInt() < 1)) { nodep->v3fatalSrc("Consecutive repetition count must be a positive constant" @@ -695,7 +696,6 @@ private: AstSenTree* const senTreep = newSenTree(nodep); AstAlways* const alwaysp = new AstAlways{flp, VAlwaysKwd::ALWAYS, senTreep, ifp}; cntVarp->addNextHere(alwaysp); - // Match when N-1 previous cycles were true and current cycle is true AstNodeExpr* const cntCheckp = new AstGte{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, new AstConst{flp, static_cast(n - 1)}}; cntCheckp->dtypeSetBit(); diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index 6888284c4..125db7c85 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -44,6 +44,245 @@ VL_DEFINE_DEBUG_FUNCTIONS; +//###################################################################### +// Lower consecutive repetition forms not handled by V3AssertPre: +// SExpr leading -- all forms via PExpr forward-looking loop (IEEE 1800-2023 16.9.2) +// Standalone -- [*1]/[+]/[*] to expr/1'b1; range/unbounded unsupported +// SExpr trailing -- range/unbounded unsupported + +class AssertPropConsRepVisitor final : public VNVisitor { + V3UniqueNames m_names{"__VconsRep"}; + + struct RepRange final { + int minN; + int maxN; // valid only when !unbounded && maxCountp != nullptr + bool unbounded; + }; + + RepRange getCounts(const AstConsRep* repp) { + const AstConst* const minp = VN_CAST(repp->countp(), Const); + UASSERT_OBJ(minp, repp, "ConsRep min count must be constant after V3Width"); + RepRange r; + r.minN = minp->toSInt(); + r.unbounded = repp->unbounded(); + r.maxN = r.minN; + if (repp->maxCountp()) { + const AstConst* const maxp = VN_CAST(repp->maxCountp(), Const); + UASSERT_OBJ(maxp, repp, "ConsRep max count must be constant after V3Width"); + r.maxN = maxp->toSInt(); + } + return r; + } + + // VISITORS + + void visit(AstSExpr* nodep) override { + // Intercept before iterating children: lowerInSExpr deletes nodep, so + // calling iterateChildren after would be a use-after-free. + if (AstConsRep* const repp = VN_CAST(nodep->preExprp(), ConsRep)) { + lowerInSExpr(nodep, repp); + return; + } + iterateChildren(nodep); + } + + void visit(AstConsRep* nodep) override { + // Leading SExpr case is handled by visit(AstSExpr). + // Here: trailing position ("b ##1 a[+]") and standalone. + if (AstSExpr* const sexprp = VN_CAST(nodep->backp(), SExpr)) { + // Trailing range/unbounded: needs forward-looking NFA -- not yet supported. + if (nodep == sexprp->exprp() && (nodep->unbounded() || nodep->maxCountp())) { + nodep->v3warn(E_UNSUPPORTED, + "Unsupported: trailing consecutive repetition range" + " in sequence expression (e.g. a ##1 b[+])"); + AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack(); + nodep->replaceWith(exprp); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + } + return; + } + lowerStandalone(nodep); + } + + void visit(AstNode* nodep) override { iterateChildren(nodep); } + + void lowerStandalone(AstConsRep* nodep) { + const RepRange r = getCounts(nodep); + if (!nodep->maxCountp() && !r.unbounded && r.minN >= 2) return; // V3AssertPre handles + + FileLine* const flp = nodep->fileline(); + AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack(); + + if (r.minN == 0 && r.unbounded) { + // [*]: always matches (zero or more -- no temporal constraint alone) + VL_DO_DANGLING(exprp->deleteTree(), exprp); + nodep->replaceWith(new AstConst{flp, AstConst::BitTrue{}}); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + return; + } + if (r.minN <= 1 && (r.unbounded || !nodep->maxCountp())) { + // [+] or [*1]: just the expression itself + nodep->replaceWith(exprp); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + return; + } + // [*N:M] or [*N:$] range standalone -- requires NFA, not yet supported + nodep->v3warn(E_UNSUPPORTED, "Unsupported: standalone consecutive repetition range"); + nodep->replaceWith(exprp); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + } + + static bool isCycleDelay1(const AstNode* delayp) { + const AstDelay* const dp = VN_CAST(delayp, Delay); + if (!dp || !dp->isCycleDelay() || dp->isRangeDelay()) return false; + const AstConst* const cp = VN_CAST(dp->lhsp(), Const); + return cp && cp->toUInt() == 1; + } + + // Lower "expr[*N:M] ##1 next" to a PExpr loop: + // if ($sampled(expr)) { cnt=1; do { ##1; branch on cnt vs N/M; } while (!done); } + // else if (N==0): ##1; if ($sampled(next)) pass; else fail; + void lowerInSExpr(AstSExpr* sexprp, AstConsRep* repp) { + const RepRange r = getCounts(repp); + FileLine* const flp = sexprp->fileline(); + + // Unlink the three components of the SExpr + AstNodeExpr* const repExprp = repp->exprp()->unlinkFrBack(); + AstNodeStmt* const delayp = sexprp->delayp()->unlinkFrBack(); + AstNodeExpr* const nextExprp = sexprp->exprp()->unlinkFrBack(); + + // Trivial case: [*1] exact in SExpr -- just restore the SExpr for DFA + if (r.minN == 1 && !r.unbounded && !repp->maxCountp()) { + repp->replaceWith(repExprp); + VL_DO_DANGLING(repp->deleteTree(), repp); + sexprp->delayp(delayp); + sexprp->exprp(nextExprp); + return; + } + + // Non-##1 delay combined with multi-cycle repetition would produce incorrect + // inter-repetition timing (IEEE 1800-2023 16.9.2 requires ##1 between matches). + if (!isCycleDelay1(delayp)) { + sexprp->v3warn(E_UNSUPPORTED, + "Unsupported: consecutive repetition with non-##1 cycle delay"); + repp->replaceWith(repExprp); + VL_DO_DANGLING(repp->deleteTree(), repp); + sexprp->delayp(delayp); + sexprp->exprp(nextExprp); + return; + } + + // Build the counter and done-flag variables (AUTOMATIC_EXPLICIT for PExpr scope) + AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, m_names.get(sexprp), + sexprp->findBasicDType(VBasicDTypeKwd::UINT32)}; + cntVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + AstVar* const doneVarp + = new AstVar{flp, VVarType::BLOCKTEMP, m_names.get(sexprp), sexprp->findBitDType()}; + doneVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + + // Convenience constructors + auto cntRef = [&](VAccess acc) { return new AstVarRef{flp, cntVarp, acc}; }; + auto setDone = [&]() { + return new AstAssign{flp, new AstVarRef{flp, doneVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitTrue{}}}; + }; + auto incrCnt = [&]() { + return new AstAssign{flp, cntRef(VAccess::WRITE), + new AstAdd{flp, cntRef(VAccess::READ), new AstConst{flp, 1u}}}; + }; + auto passStmts = [&]() { + AstBegin* const bp = new AstBegin{flp, "", nullptr, true}; + bp->addStmtsp(new AstPExprClause{flp, true}); + bp->addStmtsp(setDone()); + return bp; + }; + auto failStmts = [&]() { + AstBegin* const bp = new AstBegin{flp, "", nullptr, true}; + bp->addStmtsp(new AstPExprClause{flp, false}); + bp->addStmtsp(setDone()); + return bp; + }; + auto sampled = [&](AstNodeExpr* ep) { + AstSampled* const sp = new AstSampled{flp, ep}; + sp->dtypeFrom(ep); + return sp; + }; + + // Loop body: ##1 delay, then branch on count vs min + AstLoop* const loopp = new AstLoop{flp}; + loopp->addStmtsp(delayp); + + // When cnt >= minN: try to match next, or continue accumulating, or fail + AstBegin* const continueBlockp = new AstBegin{flp, "", nullptr, true}; + continueBlockp->addStmtsp(incrCnt()); + if (!r.unbounded) { + // Upper-bound check: if cnt > maxN, the window is exhausted + continueBlockp->addStmtsp( + new AstIf{flp, + new AstGt{flp, cntRef(VAccess::READ), + new AstConst{flp, static_cast(r.maxN)}}, + failStmts()}); + } + AstIf* const tryNextp + = new AstIf{flp, sampled(nextExprp), passStmts(), + new AstIf{flp, sampled(repExprp->cloneTreePure(false)), continueBlockp, + failStmts()}}; + + if (r.minN > 0) { + // When cnt < minN: still accumulating -- must see expr to continue + AstIf* const accumulatep = new AstIf{flp, sampled(repExprp->cloneTreePure(false)), + incrCnt(), failStmts()}; + loopp->addStmtsp( + new AstIf{flp, + new AstGte{flp, cntRef(VAccess::READ), + new AstConst{flp, static_cast(r.minN)}}, + tryNextp, accumulatep}); + } else { + // minN == 0: every iteration is already past the minimum threshold + loopp->addStmtsp(tryNextp); + } + loopp->addStmtsp(new AstLoopTest{ + flp, loopp, new AstNot{flp, new AstVarRef{flp, doneVarp, VAccess::READ}}}); + + // Entry: expr matched at cycle 0 -- initialize counter and start loop + AstBegin* const entryBlockp = new AstBegin{flp, "", nullptr, true}; + entryBlockp->addStmtsp( + new AstAssign{flp, cntRef(VAccess::WRITE), new AstConst{flp, 1u}}); + entryBlockp->addStmtsp(loopp); + + // Else branch: no match at cycle 0 + AstNode* const elsep = [&]() -> AstNode* { + if (r.minN == 0) { + // Zero-repetition path: skip directly to ##1 and check next + AstBegin* const skipBlockp = new AstBegin{flp, "", nullptr, true}; + skipBlockp->addStmtsp(delayp->cloneTree(false)); + skipBlockp->addStmtsp( + new AstIf{flp, sampled(nextExprp->cloneTreePure(false)), passStmts(), + failStmts()}); + return skipBlockp; + } + return new AstPExprClause{flp, false}; + }(); + + AstIf* const topIfp = new AstIf{flp, sampled(repExprp), entryBlockp, elsep}; + + // Wrap everything in a PExpr with cnt and done as locals + AstBegin* const bodyp = new AstBegin{flp, "", cntVarp, true}; + bodyp->addStmtsp(doneVarp); + bodyp->addStmtsp( + new AstAssign{flp, new AstVarRef{flp, doneVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitFalse{}}}); + bodyp->addStmtsp(topIfp); + + sexprp->replaceWith(new AstPExpr{flp, bodyp, sexprp->dtypep()}); + VL_DO_DANGLING(sexprp->deleteTree(), sexprp); + } + +public: + explicit AssertPropConsRepVisitor(AstNetlist* nodep) { iterate(nodep); } + ~AssertPropConsRepVisitor() override = default; +}; + //###################################################################### // Data structures (graph types) @@ -996,6 +1235,8 @@ public: void V3AssertProp::assertPropAll(AstNetlist* nodep) { UINFO(2, __FUNCTION__ << ":"); + // Lower range/unbounded consecutive repetition before DFA graph building + { AssertPropConsRepVisitor{nodep}; } { RangeDelayExpander{nodep}; } { AssertPropLowerVisitor{nodep}; } { diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 4f50c5083..4472155de 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -984,23 +984,52 @@ public: bool rhsIsValue() const { return m_rhsIsValue; } }; class AstConsRep final : public AstNodeExpr { - // Consecutive repetition [*N] (IEEE 1800-2023 16.9.2) - // Lowered by V3AssertPre to: expr && $past(expr,1) && ... && $past(expr,N-1) + // Consecutive repetition [*N], [*N:M], [+], [*] (IEEE 1800-2023 16.9.2) + // op1 := exprp -- the repeated expression + // op2 := countp -- min repetition count (N); always a positive constant after V3Width + // op3 := maxCountp -- max repetition count (M); nullptr when exact or unbounded + // + // Encoding: + // [*N]: countp=N, maxCountp=nullptr, unbounded=false + // [*N:M]: countp=N, maxCountp=M, unbounded=false + // [+]: countp=1, maxCountp=nullptr, unbounded=true (= [*1:$]) + // [*]: countp=0, maxCountp=nullptr, unbounded=true (= [*0:$]) + // + // Lowering: + // Exact [*N] standalone: V3AssertPre saturating counter + // All other forms and all SExpr-contained forms: V3AssertProp PExpr loop // @astgen op1 := exprp : AstNodeExpr // @astgen op2 := countp : AstNodeExpr + // @astgen op3 := maxCountp : Optional[AstNodeExpr] + const bool m_unbounded = false; // True for [+] and [*] (upper bound is $) public: + // Exact [*N] AstConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) : ASTGEN_SUPER_ConsRep(fl) { this->exprp(exprp); this->countp(countp); } + // Range [*N:M] or unbounded [+]/[*] + AstConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp, AstNodeExpr* maxCountp, + bool unbounded) + : ASTGEN_SUPER_ConsRep(fl) + , m_unbounded{unbounded} { + this->exprp(exprp); + this->countp(countp); + this->maxCountp(maxCountp); + } ASTGEN_MEMBERS_AstConsRep; + void dump(std::ostream& str) const override; + void dumpJson(std::ostream& str) const override; string emitVerilog() override { V3ERROR_NA_RETURN(""); } string emitC() override { V3ERROR_NA_RETURN(""); } string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); } bool cleanOut() const override { V3ERROR_NA_RETURN(""); } int instrCount() const override { V3ERROR_NA_RETURN(0); } - bool sameNode(const AstNode* /*samep*/) const override { V3ERROR_NA_RETURN(false); } + bool sameNode(const AstNode* samep) const override { + return m_unbounded == VN_DBG_AS(samep, ConsRep)->m_unbounded; + } + bool unbounded() const { return m_unbounded; } }; class AstConsWildcard final : public AstNodeExpr { // Construct a wildcard assoc array and return object, '{} diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index 9383f542f..ace0ece76 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -448,6 +448,14 @@ void AstConsDynArray::dumpJson(std::ostream& str) const { dumpJsonGen(str); } +void AstConsRep::dump(std::ostream& str) const { + this->AstNodeExpr::dump(str); + if (unbounded()) str << " [unbounded]"; +} +void AstConsRep::dumpJson(std::ostream& str) const { + dumpJsonBoolFuncIf(str, unbounded); + dumpJsonGen(str); +} void AstConsQueue::dump(std::ostream& str) const { this->AstNodeExpr::dump(str); if (lhsIsValue()) str << " [LVAL]"; diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 8e3f54e14..224cd263b 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1506,19 +1506,34 @@ class WidthVisitor final : public VNVisitor { } } void visit(AstConsRep* nodep) override { - // IEEE 1800-2023 16.9.2 -- consecutive repetition [*N] + // IEEE 1800-2023 16.9.2 -- consecutive repetition [*N], [*N:M], [+], [*] assertAtExpr(nodep); if (m_vup->prelim()) { userIterateAndNext(nodep->exprp(), WidthVP{SELF, BOTH}.p()); userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); - V3Const::constifyParamsEdit(nodep->countp()); // countp may change - const AstConst* const constp = VN_CAST(nodep->countp(), Const); - if (!constp) { + V3Const::constifyParamsEdit(nodep->countp()); + const AstConst* const minConstp = VN_CAST(nodep->countp(), Const); + if (!minConstp) { nodep->v3error("Consecutive repetition count must be constant expression" " (IEEE 1800-2023 16.9.2)"); - } else if (constp->toSInt() < 1) { + } else if (!nodep->unbounded() && !nodep->maxCountp() && minConstp->toSInt() < 1) { nodep->v3warn(E_UNSUPPORTED, "Unsupported: [*0] consecutive repetition"); } + if (nodep->maxCountp()) { + userIterateAndNext(nodep->maxCountp(), WidthVP{SELF, BOTH}.p()); + V3Const::constifyParamsEdit(nodep->maxCountp()); + const AstConst* const maxConstp = VN_CAST(nodep->maxCountp(), Const); + if (!maxConstp) { + nodep->v3error("Consecutive repetition max count must be constant" + " expression (IEEE 1800-2023 16.9.2)"); + } else if (minConstp && maxConstp->toSInt() < minConstp->toSInt()) { + nodep->v3error("Consecutive repetition max count must be >= min count" + " (IEEE 1800-2023 16.9.2)"); + } else if (maxConstp->toSInt() < 1) { + nodep->v3warn(E_UNSUPPORTED, "Unsupported: [*N:0] consecutive repetition" + " with zero max count"); + } + } nodep->dtypeSetBit(); } } diff --git a/src/verilog.y b/src/verilog.y index acf14048c..1b1771aaa 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6812,10 +6812,21 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // IEEE: expression_or_dist [ boolean_abbrev ] // // Note expression_or_dist includes "expr"! // // sexpr/*sexpression_or_dist*/ --- Hardcoded below - // // Consecutive repetition [*N] (IEEE 1800-2023 16.9.2) - // // Creates AstConsRep; lowered by V3AssertPre + // // Consecutive repetition (IEEE 1800-2023 16.9.2) + // // [*N] exact count | ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR constExpr ']' { $$ = new AstConsRep{$2, $1, $3}; } + // // [*N:M] range + | ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR constExpr ':' constExpr ']' + { $$ = new AstConsRep{$2, $1, $3, $5, false}; } + // // [+] = [*1:$] + | ~p~sexpr/*sexpression_or_dist*/ yP_BRAPLUSKET + { $$ = new AstConsRep{$2, $1, + new AstConst{$2, 1u}, nullptr, true}; } + // // [*] = [*0:$] + | ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR ']' + { $$ = new AstConsRep{$2, $1, + new AstConst{$2, 0u}, nullptr, true}; } // // IEEE: goto_repetition (single count form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']' { $$ = new AstSExprGotoRep{$2, $1, $3}; } @@ -6907,17 +6918,9 @@ sequence_match_item: // ==IEEE: sequence_match_item boolean_abbrev: // ==IEEE: boolean_abbrev // // IEEE: consecutive_repetition - // // [*N] exact count handled directly in sexpr rule - yP_BRASTAR constExpr ':' constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [*] boolean abbrev expression"); DEL($4); } - | yP_BRASTAR ']' - { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: [*] boolean abbrev expression"); } - | yP_BRAPLUSKET - { $$ = new AstConst{$1, AstConst::BitFalse{}}; - BBUNSUP($1, "Unsupported: [+] boolean abbrev expression"); } + // // [*N], [*N:M], [+], [*] all handled in sexpr rule // // IEEE: nonconsecutive_repetition/non_consecutive_repetition - | yP_BRAEQ constExpr ']' + yP_BRAEQ constExpr ']' { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); } | yP_BRAEQ constExpr ':' constExpr ']' { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); DEL($4); } diff --git a/test_regress/t/t_assert_prop_consec_rep_bad.out b/test_regress/t/t_assert_prop_consec_rep_bad.out index 287ae183a..482819b77 100644 --- a/test_regress/t/t_assert_prop_consec_rep_bad.out +++ b/test_regress/t/t_assert_prop_consec_rep_bad.out @@ -1,15 +1,31 @@ -%Error: t/t_assert_prop_consec_rep_bad.v:14:40: Expecting expression to be constant, but variable isn't const: 'n' +%Error: t/t_assert_prop_consec_rep_bad.v:12:39: Expecting expression to be constant, but variable isn't const: 'n' : ... note: In instance 't' - 14 | assert property (@(posedge clk) a [* n] |-> 1); - | ^ + 12 | assert property (@(posedge clk) a [*n] |-> 1); + | ^ ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: t/t_assert_prop_consec_rep_bad.v:14:37: Consecutive repetition count must be constant expression (IEEE 1800-2023 16.9.2) +%Error: t/t_assert_prop_consec_rep_bad.v:12:37: Consecutive repetition count must be constant expression (IEEE 1800-2023 16.9.2) : ... note: In instance 't' - 14 | assert property (@(posedge clk) a [* n] |-> 1); + 12 | assert property (@(posedge clk) a [*n] |-> 1); | ^~ -%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_bad.v:17:37: Unsupported: [*0] consecutive repetition +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_bad.v:15:37: Unsupported: [*0] consecutive repetition : ... note: In instance 't' - 17 | assert property (@(posedge clk) a [* 0] |-> 1); + 15 | assert property (@(posedge clk) a [*0] |-> 1); | ^~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: t/t_assert_prop_consec_rep_bad.v:18:37: Consecutive repetition max count must be >= min count (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 18 | assert property (@(posedge clk) a [*3:1] |-> 1); + | ^~ +%Error: t/t_assert_prop_consec_rep_bad.v:21:41: Expecting expression to be constant, but variable isn't const: 'n' + : ... note: In instance 't' + 21 | assert property (@(posedge clk) a [*1:n] |-> 1); + | ^ +%Error: t/t_assert_prop_consec_rep_bad.v:21:37: Consecutive repetition max count must be constant expression (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 21 | assert property (@(posedge clk) a [*1:n] |-> 1); + | ^~ +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_bad.v:24:37: Unsupported: [*N:0] consecutive repetition with zero max count + : ... note: In instance 't' + 24 | assert property (@(posedge clk) a [*0:0] |-> 1); + | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_bad.v b/test_regress/t/t_assert_prop_consec_rep_bad.v index 6c54b908a..df81234e9 100644 --- a/test_regress/t/t_assert_prop_consec_rep_bad.v +++ b/test_regress/t/t_assert_prop_consec_rep_bad.v @@ -4,16 +4,23 @@ // SPDX-FileCopyrightText: 2026 PlanV GmbH // SPDX-License-Identifier: CC0-1.0 -module t ( - input clk -); +module t (input clk); logic a; int n; // Bad: non-constant repetition count - assert property (@(posedge clk) a [* n] |-> 1); + assert property (@(posedge clk) a [*n] |-> 1); // Bad: [*0] consecutive repetition unsupported - assert property (@(posedge clk) a [* 0] |-> 1); + assert property (@(posedge clk) a [*0] |-> 1); + + // Bad: max count < min count + assert property (@(posedge clk) a [*3:1] |-> 1); + + // Bad: non-constant max count + assert property (@(posedge clk) a [*1:n] |-> 1); + + // Bad: zero max count ([*0:0]) + assert property (@(posedge clk) a [*0:0] |-> 1); endmodule diff --git a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.out b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.out new file mode 100644 index 000000000..9b6379796 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_delay_unsup.v:11:41: Unsupported: consecutive repetition with non-##1 cycle delay + : ... note: In instance 't' + 11 | assert property (@(posedge clk) a[*2] ##3 b); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.py b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.py @@ -0,0 +1,16 @@ +#!/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, expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_assert_prop_consec_rep_delay_unsup.v b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.v new file mode 100644 index 000000000..55cecfef6 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_delay_unsup.v @@ -0,0 +1,13 @@ +// 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; + + // Bad: consecutive repetition with non-##1 delay + assert property (@(posedge clk) a[*2] ##3 b); + +endmodule diff --git a/test_regress/t/t_assert_prop_consec_rep_range_bad.out b/test_regress/t/t_assert_prop_consec_rep_range_bad.out new file mode 100644 index 000000000..1e2b2f5bc --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_range_bad.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_range_bad.v:11:37: Unsupported: standalone consecutive repetition range + : ... note: In instance 't' + 11 | assert property (@(posedge clk) a [*2:3] |-> 1); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_range_bad.py b/test_regress/t/t_assert_prop_consec_rep_range_bad.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_range_bad.py @@ -0,0 +1,16 @@ +#!/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, expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_assert_prop_consec_rep_range_bad.v b/test_regress/t/t_assert_prop_consec_rep_range_bad.v new file mode 100644 index 000000000..8014fdfa6 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_range_bad.v @@ -0,0 +1,13 @@ +// 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; + + // Bad: standalone range repetition (no ## delay to anchor the sequence) + assert property (@(posedge clk) a [*2:3] |-> 1); + +endmodule diff --git a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.out b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.out new file mode 100644 index 000000000..474c5bc40 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_trail_unsup.v:11:42: Unsupported: trailing consecutive repetition range in sequence expression (e.g. a ##1 b[+]) + : ... note: In instance 't' + 11 | assert property (@(posedge clk) b ##1 a[+]); + | ^~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.py b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.py @@ -0,0 +1,16 @@ +#!/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, expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_assert_prop_consec_rep_trail_unsup.v b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.v new file mode 100644 index 000000000..9c8404c6f --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_trail_unsup.v @@ -0,0 +1,13 @@ +// 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; + + // Bad: trailing consecutive repetition range in sequence expression + assert property (@(posedge clk) b ##1 a[+]); + +endmodule