diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 79769bd07..2a722f264 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -707,9 +707,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" diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index a36cc8004..757b65a13 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -44,6 +44,234 @@ 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 + + AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack(); + + if (r.minN <= 1 && (r.unbounded || !nodep->maxCountp())) { + // [+], [*], or [*1]: reduce to the expression itself. + // [*] (zero-or-more) uses the shortest non-vacuous match (length 1 when expr=true), + // matching simulator behavior; zero-length matches do not trigger |-> implications. + 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) @@ -1223,6 +1451,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 3a4ebf035..08c6dbed1 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 { // LCOV_EXCL_LINE + return m_unbounded == VN_DBG_AS(samep, ConsRep)->m_unbounded; // LCOV_EXCL_LINE + } + 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 5465f876a..a77aad311 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 { // LCOV_EXCL_START + this->AstNodeExpr::dump(str); + if (unbounded()) str << " [unbounded]"; +} +void AstConsRep::dumpJson(std::ostream& str) const { + dumpJsonBoolFuncIf(str, unbounded); + dumpJsonGen(str); +} // LCOV_EXCL_STOP 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 35f2e2b6c..b507ff84d 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1512,19 +1512,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 6b6a453e6..dc5a80c88 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}; } // LCOV_EXCL_LINE + // // [+] = [*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 AstSGotoRep{$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.py b/test_regress/t/t_assert_prop_consec_rep.py index 8a938befd..f090e5249 100755 --- a/test_regress/t/t_assert_prop_consec_rep.py +++ b/test_regress/t/t_assert_prop_consec_rep.py @@ -11,7 +11,7 @@ import vltest_bootstrap test.scenarios('simulator') -test.compile() +test.compile(verilator_flags2=['--timing']) test.execute() diff --git a/test_regress/t/t_assert_prop_consec_rep.v b/test_regress/t/t_assert_prop_consec_rep.v index a6f4421e6..58a08cfd1 100644 --- a/test_regress/t/t_assert_prop_consec_rep.v +++ b/test_regress/t/t_assert_prop_consec_rep.v @@ -28,27 +28,57 @@ module t ( int count_fail3 = 0; int count_fail4 = 0; int count_fail5 = 0; + int count_fail6 = 0; + int count_fail7 = 0; + int count_fail8 = 0; + int count_fail9 = 0; + int count_fail10 = 0; + int count_fail11 = 0; - // Test 1: a[*3] |-> b (3 consecutive, overlapping implication) + // Test 1: a[*3] |-> b assert property (@(posedge clk) a [* 3] |-> b) else count_fail1 <= count_fail1 + 1; - // Test 2: a[*1] |-> c (trivial [*1], overlapping) + // Test 2: a[*1] |-> c assert property (@(posedge clk) a [* 1] |-> c) else count_fail2 <= count_fail2 + 1; - // Test 3: a[*2] |=> d (2 consecutive, non-overlapping implication) + // Test 3: a[*2] |=> d assert property (@(posedge clk) a [* 2] |=> d) else count_fail3 <= count_fail3 + 1; - // Test 4: standalone consecutive rep (no implication) + // Test 4: b[*2] standalone assert property (@(posedge clk) b [* 2]) else count_fail4 <= count_fail4 + 1; - // Test 5: [*10000] large count -- verifies counter-based lowering compiles + // Test 5: a[*10000] large count assert property (@(posedge clk) a [* 10000] |-> b) else count_fail5 <= count_fail5 + 1; + // Test 6: a[*1:3] ##1 b -- bounded range in SExpr + assert property (@(posedge clk) a [* 1:3] ##1 b) + else count_fail6 <= count_fail6 + 1; + + // Test 7: a[+] ##1 b -- one-or-more in SExpr + assert property (@(posedge clk) a [+] ##1 b) + else count_fail7 <= count_fail7 + 1; + + // Test 8: a[+] |-> b -- standalone [+] (same as a |-> b) + assert property (@(posedge clk) a [+] |-> b) + else count_fail8 <= count_fail8 + 1; + + // Test 9: a[*] |-> b -- standalone [*] (shortest non-vacuous match = a) + assert property (@(posedge clk) a [*] |-> b) + else count_fail9 <= count_fail9 + 1; + + // Test 10: a[*1] ##1 b -- trivial [*1] in SExpr (restored to plain SExpr) + assert property (@(posedge clk) a [* 1] ##1 b) + else count_fail10 <= count_fail10 + 1; + + // Test 11: a[*] ##1 b -- zero-or-more in SExpr (minN==0 path) + assert property (@(posedge clk) a [*] ##1 b) + else count_fail11 <= count_fail11 + 1; + always @(posedge clk) begin `ifdef TEST_VERBOSE $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n", $time, cyc, crc, a, b, c, d); @@ -65,6 +95,12 @@ module t ( `checkd(count_fail3, 9); `checkd(count_fail4, 74); `checkd(count_fail5, 0); + `checkd(count_fail6, 65); + `checkd(count_fail7, 65); + `checkd(count_fail8, 20); + `checkd(count_fail9, 20); + `checkd(count_fail10, 73); + `checkd(count_fail11, 40); $write("*-* All Finished *-*\n"); $finish; end 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..7c9a10d3a 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); + // Bad: [*0] unsupported exact zero repetition + 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: [*N:0] zero max count + assert property (@(posedge clk) a [*0:0] |-> 1); endmodule diff --git a/test_regress/t/t_assert_prop_consec_rep_unsup.out b/test_regress/t/t_assert_prop_consec_rep_unsup.out new file mode 100644 index 000000000..610a15565 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_unsup.out @@ -0,0 +1,14 @@ +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_unsup.v:11:42: 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-UNSUPPORTED: t/t_assert_prop_consec_rep_unsup.v:14:37: Unsupported: standalone consecutive repetition range + : ... note: In instance 't' + 14 | assert property (@(posedge clk) a [*2:3] |-> 1); + | ^~ +%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_unsup.v:17:42: Unsupported: trailing consecutive repetition range in sequence expression (e.g. a ##1 b[+]) + : ... note: In instance 't' + 17 | assert property (@(posedge clk) b ##1 a[+]); + | ^~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_unsup.py b/test_regress/t/t_assert_prop_consec_rep_unsup.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_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_unsup.v b/test_regress/t/t_assert_prop_consec_rep_unsup.v new file mode 100644 index 000000000..b1f77504c --- /dev/null +++ b/test_regress/t/t_assert_prop_consec_rep_unsup.v @@ -0,0 +1,19 @@ +// 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; + + // Unsupported: non-##1 inter-repetition delay + assert property (@(posedge clk) a [*2] ##3 b); + + // Unsupported: standalone range repetition (no ## anchor) + assert property (@(posedge clk) a [*2:3] |-> 1); + + // Unsupported: trailing consecutive repetition in sequence + assert property (@(posedge clk) b ##1 a[+]); + +endmodule diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 8c43cda59..df6947bb9 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -2,18 +2,6 @@ 34 | a within(b); | ^~~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: [*] boolean abbrev expression - 89 | a [*]; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: boolean abbrev (in sequence expression) - 89 | a [*]; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:92:7: Unsupported: [+] boolean abbrev expression - 92 | a [+]; - | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:92:7: Unsupported: boolean abbrev (in sequence expression) - 92 | a [+]; - | ^~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:95:7: Unsupported: [= boolean abbrev expression 95 | a [= 1]; | ^~