From 854e80c3c251f15fb8d7195018bcb9f8334b2565 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Fri, 10 Apr 2026 00:28:28 +0200 Subject: [PATCH] Support nonconsecutive repetition [=N] in sequence expressions (#7397) --- src/V3AssertPre.cpp | 139 +++++++++++++++--- src/V3AssertProp.cpp | 13 +- src/V3AstNodeExpr.h | 112 ++++++++------ src/V3AstNodes.cpp | 4 +- src/V3Width.cpp | 10 +- src/verilog.y | 36 ++--- ...p_consec_rep.py => t_assert_consec_rep.py} | 0 ...rop_consec_rep.v => t_assert_consec_rep.v} | 0 test_regress/t/t_assert_consec_rep_bad.out | 31 ++++ ...ad_count.py => t_assert_consec_rep_bad.py} | 0 ...ec_rep_bad.v => t_assert_consec_rep_bad.v} | 0 .../t/t_assert_goto_rep_bad_count.out | 10 -- test_regress/t/t_assert_goto_rep_bad_count.v | 30 ---- test_regress/t/t_assert_nonconsec_rep.py | 18 +++ test_regress/t/t_assert_nonconsec_rep.v | 67 +++++++++ .../t/t_assert_prop_consec_rep_bad.out | 31 ---- .../t/t_assert_prop_consec_rep_unsup.out | 14 -- test_regress/t/t_assert_rep_bad_count.out | 27 ++++ ...c_rep_bad.py => t_assert_rep_bad_count.py} | 0 test_regress/t/t_assert_rep_bad_count.v | 39 +++++ test_regress/t/t_assert_rep_unsup.out | 18 +++ ...sec_rep_unsup.py => t_assert_rep_unsup.py} | 0 ...onsec_rep_unsup.v => t_assert_rep_unsup.v} | 8 + test_regress/t/t_sequence_sexpr_unsup.out | 42 +++--- test_regress/t/t_sequence_sexpr_unsup.v | 5 +- 25 files changed, 447 insertions(+), 207 deletions(-) rename test_regress/t/{t_assert_prop_consec_rep.py => t_assert_consec_rep.py} (100%) rename test_regress/t/{t_assert_prop_consec_rep.v => t_assert_consec_rep.v} (100%) create mode 100755 test_regress/t/t_assert_consec_rep_bad.out rename test_regress/t/{t_assert_goto_rep_bad_count.py => t_assert_consec_rep_bad.py} (100%) rename test_regress/t/{t_assert_prop_consec_rep_bad.v => t_assert_consec_rep_bad.v} (100%) delete mode 100644 test_regress/t/t_assert_goto_rep_bad_count.out delete mode 100644 test_regress/t/t_assert_goto_rep_bad_count.v create mode 100755 test_regress/t/t_assert_nonconsec_rep.py create mode 100644 test_regress/t/t_assert_nonconsec_rep.v delete mode 100644 test_regress/t/t_assert_prop_consec_rep_bad.out delete mode 100644 test_regress/t/t_assert_prop_consec_rep_unsup.out create mode 100644 test_regress/t/t_assert_rep_bad_count.out rename test_regress/t/{t_assert_prop_consec_rep_bad.py => t_assert_rep_bad_count.py} (100%) create mode 100644 test_regress/t/t_assert_rep_bad_count.v create mode 100644 test_regress/t/t_assert_rep_unsup.out rename test_regress/t/{t_assert_prop_consec_rep_unsup.py => t_assert_rep_unsup.py} (100%) rename test_regress/t/{t_assert_prop_consec_rep_unsup.v => t_assert_rep_unsup.v} (68%) diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 9c946b31e..fe1b58a79 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -62,6 +62,7 @@ private: V3UniqueNames m_cycleDlyNames{"__VcycleDly"}; // Cycle delay counter name generator V3UniqueNames m_consRepNames{"__VconsRep"}; // Consecutive repetition counter name generator V3UniqueNames m_gotoRepNames{"__VgotoRep"}; // Goto repetition counter name generator + V3UniqueNames m_nonConsRepNames{"__VnonConsRep"}; // Nonconsecutive rep name generator V3UniqueNames m_disableCntNames{"__VdisableCnt"}; // Disable condition counter name generator V3UniqueNames m_propVarNames{"__Vpropvar"}; // Property-local variable name generator bool m_inAssign = false; // True if in an AssignNode @@ -700,7 +701,7 @@ private: iterateChildren(nodep); nodep->sentreep(newSenTree(nodep)); } - void visit(AstConsRep* nodep) override { + void visit(AstSConsRep* nodep) override { // 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); @@ -806,13 +807,22 @@ private: VL_DO_DANGLING(pushDeletep(nodep), nodep); } - // Validate goto repetition count: must be a positive elaboration-time constant. + // Validate repetition count: must be a non-negative elaboration-time constant. + // Shared by goto [->N] and nonconsecutive [=N] repetition. // On error, replaces nodep with BitFalse placeholder and returns nullptr. - const AstConst* validateGotoRepCount(AstNode* nodep, AstNodeExpr*& countp) { + const AstConst* validateRepCount(AstNode* nodep, AstNodeExpr*& countp) { countp = V3Const::constifyEdit(countp); const AstConst* const constp = VN_CAST(countp, Const); if (!constp) { - nodep->v3error("Goto repetition count is not an elaboration-time constant" + nodep->v3error("Repetition count is not an elaboration-time constant" + " (IEEE 1800-2023 16.9.2)"); + VL_DO_DANGLING(pushDeletep(countp), countp); + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return nullptr; + } + if (constp->toSInt() < 0) { + nodep->v3error("Repetition count must be non-negative" " (IEEE 1800-2023 16.9.2)"); VL_DO_DANGLING(pushDeletep(countp), countp); nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); @@ -820,8 +830,8 @@ private: return nullptr; } if (constp->isZero()) { - nodep->v3error("Goto repetition count must be greater than zero" - " (IEEE 1800-2023 16.9.2)"); + nodep->v3warn(E_UNSUPPORTED, "Unsupported: zero repetition count" + " (IEEE 1800-2023 16.9.2)"); VL_DO_DANGLING(pushDeletep(countp), countp); nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); VL_DO_DANGLING(pushDeletep(nodep), nodep); @@ -830,19 +840,31 @@ private: return constp; } - // Lower goto repetition expr[->N] to a counter-based PExpr loop. - // Generated structure: + // Lower goto/nonconsecutive repetition to a counter-based PExpr loop. + // IEEE 1800-2023 16.9.2: + // Goto [->N]: count N occurrences, then check consequent + // Nonconsec [=N] = [->N] ##1 !b[*0:$]: count N, then scan trailing !b window + // Generated structure for goto [->N]: // begin // automatic uint32 cnt = 0; // loop { test(cnt < N); if (sampled(expr)) cnt++; if (cnt < N) @(clk); } - // // consequent check (if rhsp) or pass clause + // // consequent check or pass clause // end - AstPExpr* createGotoRepPExpr(FileLine* flp, AstNodeExpr* exprp, AstNodeExpr* countp, - AstNodeExpr* rhsp, bool isOverlapped) { + // Generated structure for nonconsec [=N] with implication: + // begin + // automatic uint32 cnt = 0; + // loop { test(cnt < N); if (sampled(expr)) cnt++; if (cnt < N) @(clk); } + // @(clk); // ##1 + // if (!isOverlapped) @(clk); // |=> delay + // loop { if (sampled(expr)) fail; if (sampled(rhs)) pass; @(clk); } + // end + AstPExpr* createRepPExpr(FileLine* flp, AstNodeExpr* exprp, AstNodeExpr* countp, + AstNodeExpr* rhsp, bool isOverlapped, bool isNonConsec) { AstSenItem* const sensesp = m_senip; - UASSERT_OBJ(sensesp, exprp, "Goto repetition requires a clock"); + UASSERT_OBJ(sensesp, exprp, "Repetition requires a clock"); - const std::string name = m_gotoRepNames.get(exprp); + const std::string name + = isNonConsec ? m_nonConsRepNames.get(exprp) : m_gotoRepNames.get(exprp); AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, name + "__counter", exprp->findBasicDType(VBasicDTypeKwd::UINT32)}; cntVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); @@ -851,26 +873,69 @@ private: beginp->addStmtsp( new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, new AstConst{flp, 0}}); + // Counting loop: find N occurrences of expr (shared by goto and nonconsec) AstLoop* const loopp = new AstLoop{flp}; - // Loop test: continue while cnt < N loopp->addStmtsp(new AstLoopTest{flp, loopp, new AstLt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, countp->cloneTreePure(false)}}); - // if ($sampled(expr)) cnt++ - // sampled is applied to whole property expr + // if (expr) cnt++ -- sampled is applied to whole property expr by V3Assert loopp->addStmtsp( new AstIf{flp, exprp, new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, new AstAdd{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, new AstConst{flp, 1}}}}); - // if (cnt < N) @(clk) -- only wait if not yet matched loopp->addStmtsp(new AstIf{ flp, new AstLt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, countp}, new AstEventControl{flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}}); beginp->addStmtsp(loopp); - if (rhsp) { + if (isNonConsec && rhsp) { + // IEEE 16.9.2: b[=N] = b[->N] ##1 !b[*0:$] + // Trailing window: ##1 advance, then scan !expr cycles checking rhs. + // Window closes when expr becomes true again (fail if rhs was never true). + beginp->addStmtsp(new AstEventControl{ + flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}); // ##1 + if (!isOverlapped) { + beginp->addStmtsp(new AstEventControl{ + flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}); // |=> + } + // Window loop: check rhs at each !expr cycle (done variable for termination) + AstVar* const doneVarp + = new AstVar{flp, VVarType::BLOCKTEMP, name + "__done", exprp->findBitDType()}; + doneVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT); + beginp->addStmtsp(doneVarp); + beginp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, doneVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitFalse{}}}); + auto setDone = [&]() { + return new AstAssign{flp, new AstVarRef{flp, doneVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitTrue{}}}; + }; + AstLoop* const windowp = new AstLoop{flp}; + // LoopTest: continue while !done + windowp->addStmtsp(new AstLoopTest{ + flp, windowp, new AstNot{flp, new AstVarRef{flp, doneVarp, VAccess::READ}}}); + // if (expr) { fail; done = 1; } -- window closed, expr true again + AstBegin* const failBlockp = new AstBegin{flp, "", nullptr, true}; + failBlockp->addStmtsp(new AstPExprClause{flp, false}); + failBlockp->addStmtsp(setDone()); + windowp->addStmtsp(new AstIf{flp, exprp->cloneTreePure(false), failBlockp}); + // if (rhs) { pass; done = 1; } -- consequent true at this !expr endpoint + AstBegin* const passBlockp = new AstBegin{flp, "", nullptr, true}; + passBlockp->addStmtsp(new AstPExprClause{flp, true}); + passBlockp->addStmtsp(setDone()); + windowp->addStmtsp(new AstIf{flp, rhsp, passBlockp}); + // @(clk) -- advance to next cycle in window + windowp->addStmtsp( + new AstEventControl{flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}); + beginp->addStmtsp(windowp); + } else if (isNonConsec) { + // Standalone nonconsec: ##1 into window, then pass + beginp->addStmtsp( + new AstEventControl{flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}); + beginp->addStmtsp(new AstPExprClause{flp, true}); + } else if (rhsp) { + // Goto rep: check consequent once at match endpoint if (!isOverlapped) { beginp->addStmtsp(new AstEventControl{ flp, new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr}); @@ -878,6 +943,7 @@ private: beginp->addStmtsp(new AstIf{flp, rhsp, new AstPExprClause{flp, true}, new AstPExprClause{flp, false}}); } else { + // Standalone goto: pass after counting beginp->addStmtsp(new AstPExprClause{flp, true}); } @@ -889,9 +955,21 @@ private: iterateChildren(nodep); FileLine* const flp = nodep->fileline(); AstNodeExpr* countp = nodep->countp()->unlinkFrBack(); - if (!validateGotoRepCount(nodep, countp)) return; + if (!validateRepCount(nodep, countp)) return; AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack(); - AstPExpr* const pexprp = createGotoRepPExpr(flp, exprp, countp, nullptr, true); + AstPExpr* const pexprp = createRepPExpr(flp, exprp, countp, nullptr, true, false); + nodep->replaceWith(pexprp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + } + + void visit(AstSNonConsRep* nodep) override { + // Standalone nonconsecutive rep (not inside implication antecedent) + iterateChildren(nodep); + FileLine* const flp = nodep->fileline(); + AstNodeExpr* countp = nodep->countp()->unlinkFrBack(); + if (!validateRepCount(nodep, countp)) return; + AstNodeExpr* const exprp = nodep->exprp()->unlinkFrBack(); + AstPExpr* const pexprp = createRepPExpr(flp, exprp, countp, nullptr, true, true); nodep->replaceWith(pexprp); VL_DO_DANGLING(pushDeletep(nodep), nodep); } @@ -917,11 +995,28 @@ private: iterateAndNextNull(nodep->rhsp()); FileLine* const flp = nodep->fileline(); AstNodeExpr* countp = gotop->countp()->unlinkFrBack(); - if (!validateGotoRepCount(nodep, countp)) return; + if (!validateRepCount(nodep, countp)) return; AstNodeExpr* const exprp = gotop->exprp()->unlinkFrBack(); AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); AstPExpr* const pexprp - = createGotoRepPExpr(flp, exprp, countp, rhsp, nodep->isOverlapped()); + = createRepPExpr(flp, exprp, countp, rhsp, nodep->isOverlapped(), false); + nodep->replaceWith(pexprp); + VL_DO_DANGLING(pushDeletep(nodep), nodep); + return; + } + + // Handle nonconsecutive repetition as antecedent before iterateChildren, + // so the standalone AstSNonConsRep visitor doesn't process it + if (AstSNonConsRep* const ncrp = VN_CAST(nodep->lhsp(), SNonConsRep)) { + iterateChildren(ncrp); + iterateAndNextNull(nodep->rhsp()); + FileLine* const flp = nodep->fileline(); + AstNodeExpr* countp = ncrp->countp()->unlinkFrBack(); + if (!validateRepCount(nodep, countp)) return; + AstNodeExpr* const exprp = ncrp->exprp()->unlinkFrBack(); + AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack(); + AstPExpr* const pexprp + = createRepPExpr(flp, exprp, countp, rhsp, nodep->isOverlapped(), true); nodep->replaceWith(pexprp); VL_DO_DANGLING(pushDeletep(nodep), nodep); return; diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index 716e78231..1477a8265 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -59,7 +59,7 @@ class AssertPropConsRepVisitor final : public VNVisitor { bool unbounded; }; - RepRange getCounts(const AstConsRep* repp) { + RepRange getCounts(const AstSConsRep* repp) { const AstConst* const minp = VN_CAST(repp->countp(), Const); UASSERT_OBJ(minp, repp, "ConsRep min count must be constant after V3Width"); RepRange r; @@ -79,14 +79,14 @@ class AssertPropConsRepVisitor final : public VNVisitor { 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)) { + if (AstSConsRep* const repp = VN_CAST(nodep->preExprp(), SConsRep)) { lowerInSExpr(nodep, repp); return; } iterateChildren(nodep); } - void visit(AstConsRep* nodep) override { + void visit(AstSConsRep* 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)) { @@ -105,7 +105,7 @@ class AssertPropConsRepVisitor final : public VNVisitor { void visit(AstNode* nodep) override { iterateChildren(nodep); } - void lowerStandalone(AstConsRep* nodep) { + void lowerStandalone(AstSConsRep* nodep) { const RepRange r = getCounts(nodep); if (!nodep->maxCountp() && !r.unbounded && r.minN >= 2) return; // V3AssertPre handles @@ -135,7 +135,7 @@ class AssertPropConsRepVisitor final : public VNVisitor { // 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) { + void lowerInSExpr(AstSExpr* sexprp, AstSConsRep* repp) { const RepRange r = getCounts(repp); FileLine* const flp = sexprp->fileline(); @@ -1396,7 +1396,8 @@ class RangeDelayExpander final : public VNVisitor { } } // Reject throughout with nested throughout or goto repetition - if (VN_IS(nodep->rhsp(), SThroughout) || VN_IS(nodep->rhsp(), SGotoRep)) { + if (VN_IS(nodep->rhsp(), SThroughout) || VN_IS(nodep->rhsp(), SGotoRep) + || VN_IS(nodep->rhsp(), SNonConsRep)) { nodep->v3warn(E_UNSUPPORTED, "Unsupported: throughout with complex sequence operator"); nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); VL_DO_DANGLING(nodep->deleteTree(), nodep); diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 08c6dbed1..058291d74 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -983,54 +983,6 @@ public: bool lhsIsValue() const { return m_lhsIsValue; } bool rhsIsValue() const { return m_rhsIsValue; } }; -class AstConsRep final : public AstNodeExpr { - // 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 { // 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, '{} // @astgen op1 := defaultp : Optional[AstNodeExpr] @@ -2173,6 +2125,54 @@ public: bool sameNode(const AstNode* /*samep*/) const override { return true; } bool isSystemFunc() const override { return true; } }; +class AstSConsRep final : public AstNodeExpr { + // 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] + AstSConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) + : ASTGEN_SUPER_SConsRep(fl) { + this->exprp(exprp); + this->countp(countp); + } + // Range [*N:M] or unbounded [+]/[*] + AstSConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp, AstNodeExpr* maxCountp, + bool unbounded) + : ASTGEN_SUPER_SConsRep(fl) + , m_unbounded{unbounded} { + this->exprp(exprp); + this->countp(countp); + this->maxCountp(maxCountp); + } + ASTGEN_MEMBERS_AstSConsRep; + 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 { // LCOV_EXCL_LINE + return m_unbounded == VN_DBG_AS(samep, SConsRep)->m_unbounded; // LCOV_EXCL_LINE + } + bool unbounded() const { return m_unbounded; } +}; class AstSExpr final : public AstNodeExpr { // Sequence expression // @astgen op1 := preExprp: Optional[AstNodeExpr] @@ -2315,6 +2315,22 @@ public: string emitC() override { V3ERROR_NA_RETURN(""); } bool cleanOut() const override { V3ERROR_NA_RETURN(""); } }; +class AstSNonConsRep final : public AstNodeExpr { + // Nonconsecutive repetition: expr [= count] + // IEEE 1800-2023 16.9.2 + // @astgen op1 := exprp : AstNodeExpr + // @astgen op2 := countp : AstNodeExpr +public: + explicit AstSNonConsRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp) + : ASTGEN_SUPER_SNonConsRep(fl) { + this->exprp(exprp); + this->countp(countp); + } + ASTGEN_MEMBERS_AstSNonConsRep; + string emitVerilog() override { V3ERROR_NA_RETURN(""); } + string emitC() override { V3ERROR_NA_RETURN(""); } + bool cleanOut() const override { V3ERROR_NA_RETURN(""); } +}; class AstSScanF final : public AstNodeExpr { // @astgen op1 := exprsp : List[AstNodeExpr] // VarRefs for results // @astgen op2 := fromp : AstNodeExpr diff --git a/src/V3AstNodes.cpp b/src/V3AstNodes.cpp index a77aad311..6b3c9bfcd 100644 --- a/src/V3AstNodes.cpp +++ b/src/V3AstNodes.cpp @@ -448,11 +448,11 @@ void AstConsDynArray::dumpJson(std::ostream& str) const { dumpJsonGen(str); } -void AstConsRep::dump(std::ostream& str) const { // LCOV_EXCL_START +void AstSConsRep::dump(std::ostream& str) const { // LCOV_EXCL_START this->AstNodeExpr::dump(str); if (unbounded()) str << " [unbounded]"; } -void AstConsRep::dumpJson(std::ostream& str) const { +void AstSConsRep::dumpJson(std::ostream& str) const { dumpJsonBoolFuncIf(str, unbounded); dumpJsonGen(str); } // LCOV_EXCL_STOP diff --git a/src/V3Width.cpp b/src/V3Width.cpp index b507ff84d..234df1d28 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -1511,7 +1511,7 @@ class WidthVisitor final : public VNVisitor { userIterate(nodep->sentreep(), nullptr); } } - void visit(AstConsRep* nodep) override { + void visit(AstSConsRep* nodep) override { // IEEE 1800-2023 16.9.2 -- consecutive repetition [*N], [*N:M], [+], [*] assertAtExpr(nodep); if (m_vup->prelim()) { @@ -1666,6 +1666,14 @@ class WidthVisitor final : public VNVisitor { nodep->dtypeSetBit(); } } + void visit(AstSNonConsRep* nodep) override { + assertAtExpr(nodep); + if (m_vup->prelim()) { + iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH); + userIterateAndNext(nodep->countp(), WidthVP{SELF, BOTH}.p()); + nodep->dtypeSetBit(); + } + } void visit(AstSThroughout* nodep) override { m_hasSExpr = true; assertAtExpr(nodep); diff --git a/src/verilog.y b/src/verilog.y index 5d5cb252a..ab951ebd5 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6815,17 +6815,17 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // Consecutive repetition (IEEE 1800-2023 16.9.2) // // [*N] exact count | ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR constExpr ']' - { $$ = new AstConsRep{$2, $1, $3}; } + { $$ = new AstSConsRep{$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 + { $$ = new AstSConsRep{$2, $1, $3, $5, false}; } // LCOV_EXCL_LINE // // [+] = [*1:$] | ~p~sexpr/*sexpression_or_dist*/ yP_BRAPLUSKET - { $$ = new AstConsRep{$2, $1, + { $$ = new AstSConsRep{$2, $1, new AstConst{$2, 1u}, nullptr, true}; } // // [*] = [*0:$] | ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR ']' - { $$ = new AstConsRep{$2, $1, + { $$ = new AstSConsRep{$2, $1, new AstConst{$2, 0u}, nullptr, true}; } // // IEEE: goto_repetition (single count form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']' @@ -6833,8 +6833,16 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg // // IEEE: goto_repetition (range form -- unsupported) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ':' constExpr ']' { $$ = $1; BBUNSUP($2, "Unsupported: [-> range goto repetition"); DEL($3); DEL($5); } - | ~p~sexpr/*sexpression_or_dist*/ boolean_abbrev - { $$ = $1; BBUNSUP($2->fileline(), "Unsupported: boolean abbrev (in sequence expression)"); DEL($2); } + // // IEEE: nonconsecutive_repetition (single count form) + | ~p~sexpr/*sexpression_or_dist*/ yP_BRAEQ constExpr ']' + { $$ = new AstSNonConsRep{$2, $1, $3}; } + // // IEEE: nonconsecutive_repetition (range form -- unsupported) + | ~p~sexpr/*sexpression_or_dist*/ yP_BRAEQ constExpr ':' constExpr ']' + { $$ = $1; BBUNSUP($2, "Unsupported: [= range nonconsecutive repetition"); DEL($3); DEL($5); } + // // All boolean_abbrev forms are now handled above: + // // [*N], [*N:M], [+], [*] via AstSConsRep + // // [->N], [->M:N] via AstSGotoRep + // // [=N], [=M:N] via AstSNonConsRep // // // IEEE: "sequence_instance [ sequence_abbrev ]" // // version without sequence_abbrev looks just like normal function call @@ -6916,18 +6924,10 @@ sequence_match_item: // ==IEEE: sequence_match_item for_step_assignment { $$ = $1; } ; -boolean_abbrev: // ==IEEE: boolean_abbrev - // // IEEE: consecutive_repetition - // // [*N], [*N:M], [+], [*] all handled in sexpr rule - // // IEEE: nonconsecutive_repetition/non_consecutive_repetition - yP_BRAEQ constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); } - | yP_BRAEQ constExpr ':' constExpr ']' - { $$ = $2; BBUNSUP($1, "Unsupported: [= boolean abbrev expression"); DEL($4); } - // // IEEE: goto_repetition - // // Goto repetition [->N] handled in sexpr rule (AstSGotoRep) - // // Range form [->M:N] also handled there (unsupported) - ; +// boolean_abbrev -- all forms now handled directly in sexpr rule: +// // IEEE: consecutive_repetition -- [*N], [*N:M], [+], [*] via AstSConsRep +// // IEEE: goto_repetition -- [->N] via AstSGotoRep, [->M:N] unsupported +// // IEEE: nonconsecutive_repetition -- [=N] via AstSNonConsRep, [=M:N] unsupported //************************************************ // Covergroup diff --git a/test_regress/t/t_assert_prop_consec_rep.py b/test_regress/t/t_assert_consec_rep.py similarity index 100% rename from test_regress/t/t_assert_prop_consec_rep.py rename to test_regress/t/t_assert_consec_rep.py diff --git a/test_regress/t/t_assert_prop_consec_rep.v b/test_regress/t/t_assert_consec_rep.v similarity index 100% rename from test_regress/t/t_assert_prop_consec_rep.v rename to test_regress/t/t_assert_consec_rep.v diff --git a/test_regress/t/t_assert_consec_rep_bad.out b/test_regress/t/t_assert_consec_rep_bad.out new file mode 100755 index 000000000..f7da5ab6a --- /dev/null +++ b/test_regress/t/t_assert_consec_rep_bad.out @@ -0,0 +1,31 @@ +%Error: t/t_assert_consec_rep_bad.v:12:39: Expecting expression to be constant, but variable isn't const: 'n' + : ... note: In instance 't' + 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_consec_rep_bad.v:12:37: Consecutive repetition count must be constant expression (IEEE 1800-2023 16.9.2) + : ... note: In instance 't' + 12 | assert property (@(posedge clk) a [*n] |-> 1); + | ^~ +%Error-UNSUPPORTED: t/t_assert_consec_rep_bad.v:15:37: Unsupported: [*0] consecutive repetition + : ... note: In instance 't' + 15 | assert property (@(posedge clk) a [*0] |-> 1); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: t/t_assert_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_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_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_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_goto_rep_bad_count.py b/test_regress/t/t_assert_consec_rep_bad.py similarity index 100% rename from test_regress/t/t_assert_goto_rep_bad_count.py rename to test_regress/t/t_assert_consec_rep_bad.py diff --git a/test_regress/t/t_assert_prop_consec_rep_bad.v b/test_regress/t/t_assert_consec_rep_bad.v similarity index 100% rename from test_regress/t/t_assert_prop_consec_rep_bad.v rename to test_regress/t/t_assert_consec_rep_bad.v diff --git a/test_regress/t/t_assert_goto_rep_bad_count.out b/test_regress/t/t_assert_goto_rep_bad_count.out deleted file mode 100644 index 994370fed..000000000 --- a/test_regress/t/t_assert_goto_rep_bad_count.out +++ /dev/null @@ -1,10 +0,0 @@ -%Error: t/t_assert_goto_rep_bad_count.v:16:42: Goto repetition count is not an elaboration-time constant (IEEE 1800-2023 16.9.2) - : ... note: In instance 't' - 16 | assert property (@(posedge clk) a[->n] |-> b) - | ^~~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: t/t_assert_goto_rep_bad_count.v:20:42: Goto repetition count must be greater than zero (IEEE 1800-2023 16.9.2) - : ... note: In instance 't' - 20 | assert property (@(posedge clk) a[->0] |-> b) - | ^~~ -%Error: Exiting due to diff --git a/test_regress/t/t_assert_goto_rep_bad_count.v b/test_regress/t/t_assert_goto_rep_bad_count.v deleted file mode 100644 index 46383a027..000000000 --- a/test_regress/t/t_assert_goto_rep_bad_count.v +++ /dev/null @@ -1,30 +0,0 @@ -// DESCRIPTION: Verilator: Verilog Test module -// -// This file ONLY is placed under the Creative Commons Public Domain. -// SPDX-FileCopyrightText: 2026 PlanV GmbH -// SPDX-License-Identifier: CC0-1.0 - -module t; - logic clk = 0; - always #5 clk = ~clk; - - int cyc = 0; - logic a, b; - int n; - - // Error: non-constant count - assert property (@(posedge clk) a[->n] |-> b) - else $error("FAIL"); - - // Error: zero count - assert property (@(posedge clk) a[->0] |-> b) - else $error("FAIL"); - - always @(posedge clk) begin - cyc <= cyc + 1; - if (cyc == 5) begin - $write("*-* All Finished *-*\n"); - $finish; - end - end -endmodule diff --git a/test_regress/t/t_assert_nonconsec_rep.py b/test_regress/t/t_assert_nonconsec_rep.py new file mode 100755 index 000000000..b92324a60 --- /dev/null +++ b/test_regress/t/t_assert_nonconsec_rep.py @@ -0,0 +1,18 @@ +#!/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.compile(verilator_flags2=['--timing', '--assert']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_assert_nonconsec_rep.v b/test_regress/t/t_assert_nonconsec_rep.v new file mode 100644 index 000000000..115044bfc --- /dev/null +++ b/test_regress/t/t_assert_nonconsec_rep.v @@ -0,0 +1,67 @@ +// 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 checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0); +`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 ( + input clk +); + + int cyc; + reg [63:0] crc; + + // Derive signals from non-adjacent CRC bits (lesson 17: avoid shift correlation) + wire a = crc[0]; + wire b = crc[4]; + wire c = crc[8]; + wire d = crc[12]; + + int count_fail1 = 0; + int count_fail2 = 0; + int count_fail3 = 0; + int count_fail4 = 0; + + // Test 1: a[=2] |-> b (overlapping implication, 2 non-consecutive occurrences) + assert property (@(posedge clk) a[=2] |-> b) + else count_fail1 <= count_fail1 + 1; + + // Test 2: a[=1] |-> c (single occurrence, overlapping) + assert property (@(posedge clk) a[=1] |-> c) + else count_fail2 <= count_fail2 + 1; + + // Test 3: a[=3] |=> d (3 occurrences, non-overlapping implication) + assert property (@(posedge clk) a[=3] |=> d) + else count_fail3 <= count_fail3 + 1; + + // Test 4: standalone nonconsec rep (no implication) + assert property (@(posedge clk) b[=2]) + else count_fail4 <= count_fail4 + 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); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + end + else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + `checkd(count_fail1, 34); + `checkd(count_fail2, 27); + `checkd(count_fail3, 25); + `checkd(count_fail4, 0); + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_assert_prop_consec_rep_bad.out b/test_regress/t/t_assert_prop_consec_rep_bad.out deleted file mode 100644 index 482819b77..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_bad.out +++ /dev/null @@ -1,31 +0,0 @@ -%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' - 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:12:37: Consecutive repetition count must be constant expression (IEEE 1800-2023 16.9.2) - : ... note: In instance 't' - 12 | assert property (@(posedge clk) a [*n] |-> 1); - | ^~ -%Error-UNSUPPORTED: t/t_assert_prop_consec_rep_bad.v:15:37: Unsupported: [*0] consecutive repetition - : ... note: In instance 't' - 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_unsup.out b/test_regress/t/t_assert_prop_consec_rep_unsup.out deleted file mode 100644 index 610a15565..000000000 --- a/test_regress/t/t_assert_prop_consec_rep_unsup.out +++ /dev/null @@ -1,14 +0,0 @@ -%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_rep_bad_count.out b/test_regress/t/t_assert_rep_bad_count.out new file mode 100644 index 000000000..787e79d93 --- /dev/null +++ b/test_regress/t/t_assert_rep_bad_count.out @@ -0,0 +1,27 @@ +%Error: t/t_assert_rep_bad_count.v:14:42: 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) + : ... 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) + : ... 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) + : ... 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) + : ... 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) + : ... note: In instance 't' + 36 | assert property (@(posedge clk) a[=-1] |-> b) + | ^~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_bad.py b/test_regress/t/t_assert_rep_bad_count.py similarity index 100% rename from test_regress/t/t_assert_prop_consec_rep_bad.py rename to test_regress/t/t_assert_rep_bad_count.py diff --git a/test_regress/t/t_assert_rep_bad_count.v b/test_regress/t/t_assert_rep_bad_count.v new file mode 100644 index 000000000..79e38c77d --- /dev/null +++ b/test_regress/t/t_assert_rep_bad_count.v @@ -0,0 +1,39 @@ +// 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; + int n; + + // === Goto repetition [->N] error paths === + + // Error: non-constant count + assert property (@(posedge clk) a[->n] |-> b) + else $error("FAIL"); + + // Unsupported: zero count + assert property (@(posedge clk) a[->0] |-> b) + else $error("FAIL"); + + // Error: negative count + assert property (@(posedge clk) a[->-1] |-> b) + else $error("FAIL"); + + // === Nonconsecutive repetition [=N] error paths === + + // Error: non-constant count + assert property (@(posedge clk) a[=n] |-> b) + else $error("FAIL"); + + // Unsupported: zero count + assert property (@(posedge clk) a[=0] |-> b) + else $error("FAIL"); + + // Error: negative count + assert property (@(posedge clk) a[=-1] |-> b) + else $error("FAIL"); + +endmodule diff --git a/test_regress/t/t_assert_rep_unsup.out b/test_regress/t/t_assert_rep_unsup.out new file mode 100644 index 000000000..8da37c2fb --- /dev/null +++ b/test_regress/t/t_assert_rep_unsup.out @@ -0,0 +1,18 @@ +%Error-UNSUPPORTED: t/t_assert_rep_unsup.v:13:42: Unsupported: consecutive repetition with non-##1 cycle delay + : ... note: In instance 't' + 13 | assert property (@(posedge clk) a [*2] ##3 b); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_assert_rep_unsup.v:16:37: Unsupported: standalone consecutive repetition range + : ... note: In instance 't' + 16 | assert property (@(posedge clk) a [*2:3] |-> 1); + | ^~ +%Error-UNSUPPORTED: t/t_assert_rep_unsup.v:19:42: Unsupported: trailing consecutive repetition range in sequence expression (e.g. a ##1 b[+]) + : ... note: In instance 't' + 19 | assert property (@(posedge clk) b ##1 a[+]); + | ^~~ +%Error-UNSUPPORTED: t/t_assert_rep_unsup.v:24:37: Unsupported: throughout with complex sequence operator + : ... note: In instance 't' + 24 | assert property (@(posedge clk) a throughout (b[=2])) + | ^~~~~~~~~~ +%Error: Exiting due to diff --git a/test_regress/t/t_assert_prop_consec_rep_unsup.py b/test_regress/t/t_assert_rep_unsup.py similarity index 100% rename from test_regress/t/t_assert_prop_consec_rep_unsup.py rename to test_regress/t/t_assert_rep_unsup.py diff --git a/test_regress/t/t_assert_prop_consec_rep_unsup.v b/test_regress/t/t_assert_rep_unsup.v similarity index 68% rename from test_regress/t/t_assert_prop_consec_rep_unsup.v rename to test_regress/t/t_assert_rep_unsup.v index b1f77504c..5fddac7d0 100644 --- a/test_regress/t/t_assert_prop_consec_rep_unsup.v +++ b/test_regress/t/t_assert_rep_unsup.v @@ -7,6 +7,8 @@ module t (input clk); logic a, b; + // === Consecutive repetition [*N] unsupported forms === + // Unsupported: non-##1 inter-repetition delay assert property (@(posedge clk) a [*2] ##3 b); @@ -16,4 +18,10 @@ module t (input clk); // Unsupported: trailing consecutive repetition in sequence assert property (@(posedge clk) b ##1 a[+]); + // === Nonconsecutive repetition [=N] unsupported forms === + + // Unsupported: nonconsecutive rep inside throughout + assert property (@(posedge clk) a throughout (b[=2])) + else $error("FAIL"); + endmodule diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 8ff412c30..0ef65b78c 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -2,39 +2,33 @@ 34 | a within(b); | ^~~~~~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:95:7: Unsupported: [= boolean abbrev expression - 95 | a [= 1]; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:95:10: Unsupported: boolean abbrev (in sequence expression) - 95 | a [= 1]; - | ^ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:98:7: Unsupported: [= boolean abbrev expression +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:98:7: Unsupported: [= range nonconsecutive repetition 98 | a [= 1:2]; | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:98:10: Unsupported: boolean abbrev (in sequence expression) - 98 | a [= 1:2]; - | ^ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:104:7: Unsupported: [-> range goto repetition - 104 | a [-> 1:2]; +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:101:7: Unsupported: [= range nonconsecutive repetition + 101 | a [= 1:$]; + | ^~ +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:7: Unsupported: [-> range goto repetition + 107 | a [-> 1:2]; | ^~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:107:26: Unsupported: sequence argument data type - 107 | sequence p_arg_seqence(sequence inseq); +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:110:26: Unsupported: sequence argument data type + 110 | sequence p_arg_seqence(sequence inseq); | ^~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:115:5: Unsupported: first_match with sequence_match_items - 115 | first_match (a, res0 = 1); - | ^~~~~~~~~~~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:118:5: Unsupported: first_match with sequence_match_items - 118 | first_match (a, res0 = 1, res1 = 2); + 118 | first_match (a, res0 = 1); | ^~~~~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:121:9: Ignoring unsupported: cover sequence - 121 | cover sequence (s_a) $display(""); +%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:121:5: Unsupported: first_match with sequence_match_items + 121 | first_match (a, res0 = 1, res1 = 2); + | ^~~~~~~~~~~ +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:124:9: Ignoring unsupported: cover sequence + 124 | cover sequence (s_a) $display(""); | ^~~~~~~~ ... 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. -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:122:9: Ignoring unsupported: cover sequence - 122 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:125:9: Ignoring unsupported: cover sequence + 125 | cover sequence (@(posedge a) disable iff (b) s_a) $display(""); | ^~~~~~~~ -%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:123:9: Ignoring unsupported: cover sequence - 123 | cover sequence (disable iff (b) s_a) $display(""); +%Warning-COVERIGN: t/t_sequence_sexpr_unsup.v:126:9: Ignoring unsupported: cover sequence + 126 | cover sequence (disable iff (b) s_a) $display(""); | ^~~~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_sequence_sexpr_unsup.v b/test_regress/t/t_sequence_sexpr_unsup.v index eac565574..cdd0e935a 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.v +++ b/test_regress/t/t_sequence_sexpr_unsup.v @@ -92,11 +92,14 @@ module t ( a [+]; endsequence sequence s_booleanabbrev_eq; - a [= 1]; + a [= 1]; // Now supported (AstSNonConsRep) endsequence sequence s_booleanabbrev_eq_range; a [= 1:2]; endsequence + sequence s_booleanabbrev_eq_unbounded; + a [= 1:$]; + endsequence sequence s_booleanabbrev_minusgt; a [-> 1]; endsequence