luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support consecutive repetition [*N:M], [+], and [*] in sequence expressions (#7379)

This commit is contained in:
Yilou Wang 2026-04-08 16:26:03 +02:00 committed by GitHub
parent 7dcf586807
commit e63c4f563e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
14 changed files with 435 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/V3AssertPre.cpp
View File

@ -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"

230
src/V3AssertProp.cpp
View File

@ -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<uint32_t>(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<uint32_t>(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}; }
{

35
src/V3AstNodeExpr.h
View File

@ -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, '{}

8
src/V3AstNodes.cpp
View File

@ -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]";

25
src/V3Width.cpp
View File

@ -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();
}
}

27
src/verilog.y
View File

@ -6812,10 +6812,21 @@ sexpr<nodeExprp>: // ==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{$<fl>2, $1, $3}; }
// // [*N:M] range
| ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR constExpr ':' constExpr ']'
{ $$ = new AstConsRep{$<fl>2, $1, $3, $5, false}; } // LCOV_EXCL_LINE
// // [+] = [*1:$]
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAPLUSKET
{ $$ = new AstConsRep{$<fl>2, $1,
new AstConst{$<fl>2, 1u}, nullptr, true}; }
// // [*] = [*0:$]
| ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR ']'
{ $$ = new AstConsRep{$<fl>2, $1,
new AstConst{$<fl>2, 0u}, nullptr, true}; }
// // IEEE: goto_repetition (single count form)
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']'
{ $$ = new AstSGotoRep{$<fl>2, $1, $3}; }
@ -6907,17 +6918,9 @@ sequence_match_item<nodep>: // ==IEEE: sequence_match_item
boolean_abbrev<nodeExprp>: // ==IEEE: boolean_abbrev
// // IEEE: consecutive_repetition
// // [*N] exact count handled directly in sexpr rule
yP_BRASTAR constExpr ':' constExpr ']'
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); DEL($4); }
| yP_BRASTAR ']'
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
BBUNSUP($<fl>1, "Unsupported: [*] boolean abbrev expression"); }
| yP_BRAPLUSKET
{ $$ = new AstConst{$1, AstConst::BitFalse{}};
BBUNSUP($<fl>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($<fl>1, "Unsupported: [= boolean abbrev expression"); }
| yP_BRAEQ constExpr ':' constExpr ']'
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); DEL($4); }

2
test_regress/t/t_assert_prop_consec_rep.py
View File

@ -11,7 +11,7 @@ import vltest_bootstrap
test.scenarios('simulator')
test.compile()
test.compile(verilator_flags2=['--timing'])
test.execute()

46
test_regress/t/t_assert_prop_consec_rep.v
View File

@ -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

30
test_regress/t/t_assert_prop_consec_rep_bad.out
View File

@ -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

19
test_regress/t/t_assert_prop_consec_rep_bad.v
View File

@ -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

14
test_regress/t/t_assert_prop_consec_rep_unsup.out Normal file
View File

@ -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

16
test_regress/t/t_assert_prop_consec_rep_unsup.py Executable file
View File

@ -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()

19
test_regress/t/t_assert_prop_consec_rep_unsup.v Normal file
View File

@ -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

12
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -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];
| ^~