diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 1417a8460..6bed69be2 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -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(); diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index e3d2f0c00..183afdfc4 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -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: diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index 4f50c5083..7949ebf6e 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -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 diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 591afcb6c..dbf8ed151 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -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 diff --git a/src/V3Dfg.cpp b/src/V3Dfg.cpp index 0107b2ace..36e24baf3 100644 --- a/src/V3Dfg.cpp +++ b/src/V3Dfg.cpp @@ -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: diff --git a/src/V3DfgCse.cpp b/src/V3DfgCse.cpp index bfc0cb5c7..71fef6625 100644 --- a/src/V3DfgCse.cpp +++ b/src/V3DfgCse.cpp @@ -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; diff --git a/src/V3EmitV.cpp b/src/V3EmitV.cpp index 0272c62db..96724db78 100644 --- a/src/V3EmitV.cpp +++ b/src/V3EmitV.cpp @@ -1067,7 +1067,6 @@ class EmitVBaseVisitorConst VL_NOT_FINAL : public VNVisitorConst { } iterateConst(nodep->exprp()); } - // Terminals void visit(AstVarRef* nodep) override { if (nodep->varScopep()) { diff --git a/src/V3Width.cpp b/src/V3Width.cpp index b6c7da9fd..00f7c8269 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -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; diff --git a/src/verilog.y b/src/verilog.y index 30f842d9e..116f0fcad 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6818,7 +6818,7 @@ sexpr: // ==IEEE: sequence_expr (The name sexpr is important as reg { $$ = new AstConsRep{$2, $1, $3}; } // // IEEE: goto_repetition (single count form) | ~p~sexpr/*sexpression_or_dist*/ yP_BRAMINUSGT constExpr ']' - { $$ = new AstSExprGotoRep{$2, $1, $3}; } + { $$ = new AstSGotoRep{$2, $1, $3}; } // // 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); } @@ -6856,7 +6856,7 @@ sexpr: // ==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: // ==IEEE: boolean_abbrev | yP_BRAEQ constExpr ':' constExpr ']' { $$ = $2; BBUNSUP($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) ; diff --git a/test_regress/t/t_sequence_sexpr_throughout.py b/test_regress/t/t_sequence_sexpr_throughout.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_sequence_sexpr_throughout.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(timing_loop=True, verilator_flags2=['--assert', '--timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_sequence_sexpr_throughout.v b/test_regress/t/t_sequence_sexpr_throughout.v new file mode 100644 index 000000000..f47b51685 --- /dev/null +++ b/test_regress/t/t_sequence_sexpr_throughout.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='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 diff --git a/test_regress/t/t_sequence_sexpr_throughout_unsup.out b/test_regress/t/t_sequence_sexpr_throughout_unsup.out new file mode 100644 index 000000000..415250db7 --- /dev/null +++ b/test_regress/t/t_sequence_sexpr_throughout_unsup.out @@ -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 diff --git a/test_regress/t/t_sequence_sexpr_throughout_unsup.py b/test_regress/t/t_sequence_sexpr_throughout_unsup.py new file mode 100755 index 000000000..1c3e73246 --- /dev/null +++ b/test_regress/t/t_sequence_sexpr_throughout_unsup.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('vlt') + +test.lint(expect_filename=test.golden_filename, + verilator_flags2=['--assert --timing --error-limit 1000'], + fails=True) + +test.passes() diff --git a/test_regress/t/t_sequence_sexpr_throughout_unsup.v b/test_regress/t/t_sequence_sexpr_throughout_unsup.v new file mode 100644 index 000000000..2b7cea58d --- /dev/null +++ b/test_regress/t/t_sequence_sexpr_throughout_unsup.v @@ -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 diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index a7e52a13a..351fbc36c 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -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; | ^~~~~~~~~