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

Support nonconsecutive repetition [=N] in sequence expressions (#7397)

This commit is contained in:
Yilou Wang 2026-04-10 00:28:28 +02:00 committed by GitHub
parent ecf6d9b674
commit 854e80c3c2
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
25 changed files with 447 additions and 207 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

139
src/V3AssertPre.cpp
View File

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

13
src/V3AssertProp.cpp
View File

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

112
src/V3AstNodeExpr.h
View File

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

4
src/V3AstNodes.cpp
View File

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

10
src/V3Width.cpp
View File

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

36
src/verilog.y
View File

@ -6815,17 +6815,17 @@ sexpr<nodeExprp>: // ==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{$<fl>2, $1, $3}; }
{ $$ = new AstSConsRep{$<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
{ $$ = new AstSConsRep{$<fl>2, $1, $3, $5, false}; } // LCOV_EXCL_LINE
// // [+] = [*1:$]
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAPLUSKET
{ $$ = new AstConsRep{$<fl>2, $1,
{ $$ = new AstSConsRep{$<fl>2, $1,
new AstConst{$<fl>2, 1u}, nullptr, true}; }
// // [*] = [*0:$]
| ~p~sexpr/*sexpression_or_dist*/ yP_BRASTAR ']'
{ $$ = new AstConsRep{$<fl>2, $1,
{ $$ = new AstSConsRep{$<fl>2, $1,
new AstConst{$<fl>2, 0u}, nullptr, true}; }
// // IEEE: goto_repetition (single count form)
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']'
@ -6833,8 +6833,16 @@ sexpr<nodeExprp>: // ==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($<fl>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{$<fl>2, $1, $3}; }
// // IEEE: nonconsecutive_repetition (range form -- unsupported)
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAEQ constExpr ':' constExpr ']'
{ $$ = $1; BBUNSUP($<fl>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<nodep>: // ==IEEE: sequence_match_item
for_step_assignment { $$ = $1; }
;
boolean_abbrev<nodeExprp>: // ==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($<fl>1, "Unsupported: [= boolean abbrev expression"); }
| yP_BRAEQ constExpr ':' constExpr ']'
{ $$ = $2; BBUNSUP($<fl>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

0
test_regress/t/t_assert_prop_consec_rep.py → test_regress/t/t_assert_consec_rep.py
View File

0
test_regress/t/t_assert_prop_consec_rep.v → test_regress/t/t_assert_consec_rep.v
View File

31
test_regress/t/t_assert_consec_rep_bad.out Executable file
View File

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

0
test_regress/t/t_assert_goto_rep_bad_count.py → test_regress/t/t_assert_consec_rep_bad.py
View File

0
test_regress/t/t_assert_prop_consec_rep_bad.v → test_regress/t/t_assert_consec_rep_bad.v
View File

10
test_regress/t/t_assert_goto_rep_bad_count.out
View File

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

30
test_regress/t/t_assert_goto_rep_bad_count.v
View File

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

18
test_regress/t/t_assert_nonconsec_rep.py Executable file
View File

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

67
test_regress/t/t_assert_nonconsec_rep.v Normal file
View File

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

31
test_regress/t/t_assert_prop_consec_rep_bad.out
View File

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

14
test_regress/t/t_assert_prop_consec_rep_unsup.out
View File

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

27
test_regress/t/t_assert_rep_bad_count.out Normal file
View File

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

0
test_regress/t/t_assert_prop_consec_rep_bad.py → test_regress/t/t_assert_rep_bad_count.py
View File

39
test_regress/t/t_assert_rep_bad_count.v Normal file
View File

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

18
test_regress/t/t_assert_rep_unsup.out Normal file
View File

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

0
test_regress/t/t_assert_prop_consec_rep_unsup.py → test_regress/t/t_assert_rep_unsup.py
View File

8
test_regress/t/t_assert_prop_consec_rep_unsup.v → test_regress/t/t_assert_rep_unsup.v
View File

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

42
test_regress/t/t_sequence_sexpr_unsup.out
View File

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

5
test_regress/t/t_sequence_sexpr_unsup.v
View File

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