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

Support sequence 'throughout' operator (#7378)

This commit is contained in:
Yilou Wang 2026-04-06 23:12:22 +02:00 committed by GitHub
parent 72b2ca5585
commit dfb7b034a5
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
15 changed files with 338 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
src/V3AssertPre.cpp
View File

@ -474,6 +474,9 @@ private:
AstEventControl* const controlp = new AstEventControl{
nodep->fileline(), new AstSenTree{flp, sensesp->cloneTree(false)}, nullptr};
const std::string delayName = m_cycleDlyNames.get(nodep);
AstNodeExpr* throughoutp
= nodep->throughoutp() ? nodep->throughoutp()->unlinkFrBack() : nullptr;
AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, delayName + "__counter",
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
cntVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
@ -481,24 +484,71 @@ private:
AstBegin* const beginp = new AstBegin{flp, delayName + "__block", cntVarp, true};
beginp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, valuep});
// Throughout: create flag tracking whether condition held every tick
AstVar* throughoutOkp = nullptr;
if (throughoutp) {
throughoutOkp = new AstVar{flp, VVarType::BLOCKTEMP, delayName + "__throughoutOk",
nodep->findBasicDType(VBasicDTypeKwd::LOGIC_IMPLICIT)};
throughoutOkp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
beginp->addStmtsp(throughoutOkp);
beginp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, throughoutOkp, VAccess::WRITE},
new AstConst{flp, AstConst::BitTrue{}}});
// Check condition at tick 0 (sequence start, before entering loop)
AstSampled* const initSampledp
= new AstSampled{flp, throughoutp->cloneTreePure(false)};
initSampledp->dtypeSetBit();
beginp->addStmtsp(
new AstIf{flp, new AstLogNot{flp, initSampledp},
new AstAssign{flp, new AstVarRef{flp, throughoutOkp, VAccess::WRITE},
new AstConst{flp, AstConst::BitFalse{}}}});
}
{
AstLoop* const loopp = new AstLoop{flp};
loopp->addStmtsp(new AstLoopTest{
flp, loopp,
new AstGt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, new AstConst{flp, 0}}});
// When throughout is present, exit loop early if condition fails
AstNodeExpr* loopCondp
= new AstGt{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, new AstConst{flp, 0}};
if (throughoutOkp) {
loopCondp = new AstLogAnd{flp, loopCondp,
new AstVarRef{flp, throughoutOkp, VAccess::READ}};
}
loopp->addStmtsp(new AstLoopTest{flp, loopp, loopCondp});
loopp->addStmtsp(controlp);
loopp->addStmtsp(
new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE},
new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
new AstConst{flp, 1}}});
// Check throughout condition at each tick during delay (IEEE 1800-2023 16.9.9)
if (throughoutp) {
AstSampled* const sampledp = new AstSampled{flp, throughoutp};
sampledp->dtypeSetBit();
loopp->addStmtsp(
new AstIf{flp, new AstLogNot{flp, sampledp},
new AstAssign{flp, new AstVarRef{flp, throughoutOkp, VAccess::WRITE},
new AstConst{flp, AstConst::BitFalse{}}}});
}
beginp->addStmtsp(loopp);
}
if (m_disableSeqIfp) {
// Compose wrappers on remaining sequence: throughout gate (inner), disable iff (outer)
AstNode* remainp = nodep->nextp() ? nodep->nextp()->unlinkFrBackWithNext() : nullptr;
if (throughoutOkp) {
// If condition failed during delay, fail assertion
remainp = new AstIf{flp, new AstVarRef{flp, throughoutOkp, VAccess::READ}, remainp,
new AstPExprClause{flp, /*pass=*/false}};
}
if (m_disableSeqIfp && remainp) {
AstIf* const disableSeqIfp = m_disableSeqIfp->cloneTree(false);
AstNode* const continuationsp = nodep->nextp()->unlinkFrBackWithNext();
// Keep continuation statements in a proper statement-list container.
disableSeqIfp->addThensp(new AstBegin{flp, "", continuationsp, true});
nodep->addNextHere(disableSeqIfp);
disableSeqIfp->addThensp(new AstBegin{flp, "", remainp, true});
remainp = disableSeqIfp;
}
if (remainp) {
if (throughoutOkp) {
// throughoutOkp is declared in beginp scope -- check must be inside it
beginp->addStmtsp(remainp);
} else {
nodep->addNextHere(remainp);
}
}
nodep->replaceWith(beginp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
@ -843,7 +893,7 @@ private:
return new AstPExpr{flp, beginp, exprp->findBitDType()};
}
void visit(AstSExprGotoRep* nodep) override {
void visit(AstSGotoRep* nodep) override {
// Standalone goto rep (not inside implication antecedent)
iterateChildren(nodep);
FileLine* const flp = nodep->fileline();
@ -870,8 +920,8 @@ private:
if (nodep->sentreep()) return; // Already processed
// Handle goto repetition as antecedent before iterateChildren,
// so the standalone AstSExprGotoRep visitor doesn't process it
if (AstSExprGotoRep* const gotop = VN_CAST(nodep->lhsp(), SExprGotoRep)) {
// so the standalone AstSGotoRep visitor doesn't process it
if (AstSGotoRep* const gotop = VN_CAST(nodep->lhsp(), SGotoRep)) {
iterateChildren(gotop);
iterateAndNextNull(nodep->rhsp());
FileLine* const flp = nodep->fileline();

73
src/V3AssertProp.cpp
View File

@ -422,6 +422,45 @@ class AssertPropLowerVisitor final : public VNVisitor {
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
}
void visit(AstSThroughout* nodep) override {
// IEEE 1800-2023 16.9.9: expr throughout seq
// Transform by AND-ing cond with every leaf expression in the sequence,
// and attaching cond to every delay for per-tick checking in V3AssertPre.
AstNodeExpr* const condp = nodep->lhsp()->unlinkFrBack();
AstNodeExpr* const seqp = nodep->rhsp()->unlinkFrBack();
if (AstSExpr* const sexprp = VN_CAST(seqp, SExpr)) {
// Walk all SExpr nodes: AND cond with leaf expressions, attach to delays
sexprp->foreach([&](AstSExpr* sp) {
if (sp->exprp() && !VN_IS(sp->exprp(), SExpr)) {
AstNodeExpr* const origp = sp->exprp()->unlinkFrBack();
AstLogAnd* const andp
= new AstLogAnd{origp->fileline(), condp->cloneTreePure(false), origp};
andp->dtypeSetBit();
sp->exprp(andp);
}
if (sp->preExprp() && !VN_IS(sp->preExprp(), SExpr)) {
AstNodeExpr* const origp = sp->preExprp()->unlinkFrBack();
AstLogAnd* const andp
= new AstLogAnd{origp->fileline(), condp->cloneTreePure(false), origp};
andp->dtypeSetBit();
sp->preExprp(andp);
}
if (AstDelay* const dlyp = VN_CAST(sp->delayp(), Delay)) {
dlyp->throughoutp(condp->cloneTreePure(false));
}
});
nodep->replaceWith(sexprp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
VL_DO_DANGLING(condp->deleteTree(), condp);
visit(sexprp);
} else {
// Single expression (no delay): degenerate to cond && seq
AstLogAnd* const andp = new AstLogAnd{nodep->fileline(), condp, seqp};
andp->dtypeSetBit();
nodep->replaceWith(andp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
}
void visit(AstNodeModule* nodep) override {
VL_RESTORER(m_modp);
m_modp = nodep;
@ -1060,6 +1099,40 @@ class RangeDelayExpander final : public VNVisitor {
}
}
void visit(AstSThroughout* nodep) override {
// Reject throughout with range-delay sequences before FSM expansion
// would silently lose per-tick enforcement (IEEE 1800-2023 16.9.9)
if (AstSExpr* const sexprp = VN_CAST(nodep->rhsp(), SExpr)) {
if (containsRangeDelay(sexprp)) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: throughout with range delay sequence");
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
}
// Reject throughout with nested throughout or goto repetition
if (VN_IS(nodep->rhsp(), SThroughout) || VN_IS(nodep->rhsp(), SGotoRep)) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: throughout with complex sequence operator");
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
// Reject throughout with temporal SAnd/SOr (containing SExpr = multi-cycle).
// Pure boolean SAnd/SOr are OK -- AssertPropLowerVisitor lowers them to LogAnd/LogOr.
if (VN_IS(nodep->rhsp(), SAnd) || VN_IS(nodep->rhsp(), SOr)) {
bool hasSExpr = false;
nodep->rhsp()->foreach([&](const AstSExpr*) { hasSExpr = true; });
if (hasSExpr) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: throughout with complex sequence operator");
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
}
iterateChildren(nodep);
}
void visit(AstNode* nodep) override { iterateChildren(nodep); }
public:

54
src/V3AstNodeExpr.h
View File

@ -2168,22 +2168,6 @@ public:
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
int instrCount() const override { return widthInstrs(); }
};
class AstSExprGotoRep final : public AstNodeExpr {
// Goto repetition: expr [-> count]
// IEEE 1800-2023 16.9.2
// @astgen op1 := exprp : AstNodeExpr
// @astgen op2 := countp : AstNodeExpr
public:
explicit AstSExprGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp)
: ASTGEN_SUPER_SExprGotoRep(fl) {
this->exprp(exprp);
this->countp(countp);
}
ASTGEN_MEMBERS_AstSExprGotoRep;
string emitVerilog() override { V3ERROR_NA_RETURN(""); }
string emitC() override { V3ERROR_NA_RETURN(""); }
bool cleanOut() const override { V3ERROR_NA_RETURN(""); }
};
class AstSFormatArg final : public AstNodeExpr {
// Information for formatting each argument to AstSFormat,
// used to pass to (potentially) runtime decoding of format arguments
@ -2286,6 +2270,22 @@ public:
bool cleanOut() const override { V3ERROR_NA_RETURN(true); }
bool isSystemFunc() const override { return true; }
};
class AstSGotoRep final : public AstNodeExpr {
// Goto repetition: expr [-> count]
// IEEE 1800-2023 16.9.2
// @astgen op1 := exprp : AstNodeExpr
// @astgen op2 := countp : AstNodeExpr
public:
explicit AstSGotoRep(FileLine* fl, AstNodeExpr* exprp, AstNodeExpr* countp)
: ASTGEN_SUPER_SGotoRep(fl) {
this->exprp(exprp);
this->countp(countp);
}
ASTGEN_MEMBERS_AstSGotoRep;
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
@ -3692,6 +3692,28 @@ public:
bool sizeMattersRhs() const override { return false; }
int instrCount() const override { return widthInstrs() + INSTR_COUNT_BRANCH; }
};
class AstSThroughout final : public AstNodeBiop {
// expr throughout seq (IEEE 1800-2023 16.9.9)
public:
AstSThroughout(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp)
: ASTGEN_SUPER_SThroughout(fl, lhsp, rhsp) {
dtypeSetBit();
}
ASTGEN_MEMBERS_AstSThroughout;
// LCOV_EXCL_START // Lowered in V3AssertProp before these are called
void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override {
out.opLogAnd(lhs, rhs);
}
string emitVerilog() override { return "%k(%l %fthroughout %r)"; }
string emitC() override { V3ERROR_NA_RETURN(""); }
string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
bool cleanOut() const override { return true; }
bool cleanLhs() const override { return true; }
bool cleanRhs() const override { return true; }
bool sizeMattersLhs() const override { return false; }
bool sizeMattersRhs() const override { return false; }
// LCOV_EXCL_STOP
};
class AstSel final : public AstNodeBiop {
// *Resolved* (tyep checked) multiple bit range extraction. Always const width
// @astgen alias op1 := fromp

1
src/V3AstNodeStmt.h
View File

@ -544,6 +544,7 @@ class AstDelay final : public AstNodeStmt {
// @astgen op1 := lhsp : AstNodeExpr // Delay value (or min for range)
// @astgen op2 := stmtsp : List[AstNode] // Statements under delay
// @astgen op3 := rhsp : Optional[AstNodeExpr] // Max delay value (range delay only)
// @astgen op4 := throughoutp : Optional[AstNodeExpr] // Throughout condition (IEEE 16.9.9)
VTimescale m_timeunit; // Delay's time unit
const bool m_isCycle; // True if it is a cycle delay

7
src/V3Dfg.cpp
View File

@ -781,7 +781,12 @@ void DfgVertex::typeCheck(const DfgGraph& dfg) const {
}
case VDfgType::SAnd:
case VDfgType::SOr: UASSERT_OBJ(false, this, "SAnd/SOr should be removed before DFG"); return;
case VDfgType::SOr:
case VDfgType::SThroughout: {
UASSERT_OBJ(false, this,
"SAnd/SOr/SThroughout should be removed before DFG"); // LCOV_EXCL_LINE
return; // LCOV_EXCL_LINE
}
case VDfgType::LogAnd:
case VDfgType::LogEq:

2
src/V3DfgCse.cpp
View File

@ -127,6 +127,7 @@ class V3DfgCse final {
case VDfgType::StreamR:
case VDfgType::SAnd:
case VDfgType::SOr:
case VDfgType::SThroughout:
case VDfgType::Sub:
case VDfgType::Xor: return V3Hash{};
}
@ -251,6 +252,7 @@ class V3DfgCse final {
case VDfgType::StreamL:
case VDfgType::SAnd:
case VDfgType::SOr:
case VDfgType::SThroughout:
case VDfgType::StreamR:
case VDfgType::Sub:
case VDfgType::Xor: return true;

1
src/V3EmitV.cpp
View File

@ -1067,7 +1067,6 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst {
}
iterateConst(nodep->exprp());
}
// Terminals
void visit(AstVarRef* nodep) override {
if (nodep->varScopep()) {

15
src/V3Width.cpp
View File

@ -1637,7 +1637,7 @@ class WidthVisitor final : public VNVisitor {
if (nodep->seedp()) iterateCheckSigned32(nodep, "seed", nodep->seedp(), BOTH);
}
}
void visit(AstSExprGotoRep* nodep) override {
void visit(AstSGotoRep* nodep) override {
assertAtExpr(nodep);
if (m_vup->prelim()) {
iterateCheckBool(nodep, "exprp", nodep->exprp(), BOTH);
@ -1645,6 +1645,19 @@ class WidthVisitor final : public VNVisitor {
nodep->dtypeSetBit();
}
}
void visit(AstSThroughout* nodep) override {
m_hasSExpr = true;
assertAtExpr(nodep);
if (m_vup->prelim()) {
// lhsp is a boolean expression, not a sequence -- clear m_underSExpr temporarily
VL_RESTORER(m_underSExpr);
m_underSExpr = false;
iterateCheckBool(nodep, "lhsp", nodep->lhsp(), BOTH);
m_underSExpr = true;
iterate(nodep->rhsp());
nodep->dtypeSetBit();
}
}
void visit(AstSExpr* nodep) override {
VL_RESTORER(m_underSExpr);
m_underSExpr = true;

6
src/verilog.y
View File

@ -6818,7 +6818,7 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
{ $$ = new AstConsRep{$<fl>2, $1, $3}; }
// // IEEE: goto_repetition (single count form)
| ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']'
{ $$ = new AstSExprGotoRep{$<fl>2, $1, $3}; }
{ $$ = new AstSGotoRep{$<fl>2, $1, $3}; }
// // 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); }
@ -6856,7 +6856,7 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
| yFIRST_MATCH '(' sexpr ',' sequence_match_itemList ')'
{ $$ = $3; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); DEL($5); }
| ~p~sexpr/*sexpression_or_dist*/ yTHROUGHOUT sexpr
{ $$ = $1; BBUNSUP($2, "Unsupported: throughout (in sequence expression)"); DEL($3); }
{ $$ = new AstSThroughout{$2, $1, $3}; }
// // Below pexpr's are really sequence_expr, but avoid conflict
// // IEEE: sexpr yWITHIN sexpr
| ~p~sexpr yWITHIN sexpr
@ -6922,7 +6922,7 @@ boolean_abbrev<nodeExprp>: // ==IEEE: boolean_abbrev
| yP_BRAEQ constExpr ':' constExpr ']'
{ $$ = $2; BBUNSUP($<fl>1, "Unsupported: [= boolean abbrev expression"); DEL($4); }
// // IEEE: goto_repetition
// // Goto repetition [->N] handled in sexpr rule (AstSExprGotoRep)
// // Goto repetition [->N] handled in sexpr rule (AstSGotoRep)
// // Range form [->M:N] also handled there (unsupported)
;

18
test_regress/t/t_sequence_sexpr_throughout.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(timing_loop=True, verilator_flags2=['--assert', '--timing'])
test.execute()
test.passes()

67
test_regress/t/t_sequence_sexpr_throughout.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='h%x exp='h%x\n", `__FILE__,`__LINE__, (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
// IEEE 1800-2023 16.9.9: expr throughout seq
// CRC-driven random stimulus exercises throughout with varying cond/a/b signals.
module t (
input clk
);
integer cyc = 0;
reg [63:0] crc = '0;
// Derive signals from non-adjacent CRC bits (gap > max delay to avoid LFSR correlation)
wire cond = crc[0];
wire a = crc[4];
wire b = crc[8];
int count_fail1 = 0;
int count_fail2 = 0;
int count_fail3 = 0;
// Test 1: a |-> (cond throughout (1'b1 ##3 1'b1))
// If a fires, cond must hold for 4 consecutive ticks (start + 3 delay ticks).
assert property (@(posedge clk) disable iff (cyc < 10)
a |-> (cond throughout (1'b1 ##3 1'b1)))
else count_fail1 <= count_fail1 + 1;
// Test 2: a |-> (cond throughout (1'b1 ##1 b))
// If a fires, cond must hold for 2 ticks and b must be true at tick +1.
assert property (@(posedge clk) disable iff (cyc < 10)
a |-> (cond throughout (1'b1 ##1 b)))
else count_fail2 <= count_fail2 + 1;
// Test 3: a |-> (cond throughout b)
// No delay: degenerates to a |-> (cond && b).
assert property (@(posedge clk) disable iff (cyc < 10)
a |-> (cond throughout b))
else count_fail3 <= count_fail3 + 1;
always_ff @(posedge clk) begin
`ifdef TEST_VERBOSE
$write("[%0t] cyc==%0d crc=%x cond=%b a=%b b=%b\n",
$time, cyc, crc, cond, a, b);
`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, 36);
`checkd(count_fail2, 37);
`checkd(count_fail3, 31);
$write("*-* All Finished *-*\n");
$finish;
end
end
endmodule

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

@ -0,0 +1,14 @@
%Error-UNSUPPORTED: t/t_sequence_sexpr_throughout_unsup.v:14:16: Unsupported: throughout with range delay sequence
: ... note: In instance 't'
14 | a |-> (a throughout (b ##[1:2] c)));
| ^~~~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_sexpr_throughout_unsup.v:18:16: Unsupported: throughout with complex sequence operator
: ... note: In instance 't'
18 | a |-> (a throughout ((b ##1 c) and (c ##1 b))));
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_throughout_unsup.v:22:16: Unsupported: throughout with complex sequence operator
: ... note: In instance 't'
22 | a |-> (a throughout (b throughout (b ##1 c))));
| ^~~~~~~~~~
%Error: Exiting due to

18
test_regress/t/t_sequence_sexpr_throughout_unsup.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('vlt')
test.lint(expect_filename=test.golden_filename,
verilator_flags2=['--assert --timing --error-limit 1000'],
fails=True)
test.passes()

24
test_regress/t/t_sequence_sexpr_throughout_unsup.v Normal file
View File

@ -0,0 +1,24 @@
// 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, c;
// Unsupported: throughout with range delay on RHS (IEEE 16.9.9)
assert property (@(posedge clk)
a |-> (a throughout (b ##[1:2] c)));
// Unsupported: throughout with temporal 'and' sequence on RHS
assert property (@(posedge clk)
a |-> (a throughout ((b ##1 c) and (c ##1 b))));
// Unsupported: nested throughout
assert property (@(posedge clk)
a |-> (a throughout (b throughout (b ##1 c))));
endmodule

3
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -2,9 +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:46:7: Unsupported: throughout (in sequence expression)
46 | a throughout b;
| ^~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:50:7: Unsupported: intersect (in sequence expression)
50 | a intersect b;
| ^~~~~~~~~