diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index 30ca88fb2..f4e561444 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -38,6 +38,7 @@ #include "V3AssertProp.h" +#include "V3Const.h" #include "V3Graph.h" #include "V3UniqueNames.h" @@ -584,11 +585,417 @@ public: } }; +//###################################################################### +// Range delay expansion (runs before DFA builder) +// +// Replaces ##[M:N] range delays with a module-level FSM (always block +// + state/counter vars). No coroutine overhead -- one state advance +// per clock cycle. The SExpr becomes a !fail combinational check. + +class RangeDelayExpander final : public VNVisitor { + // STATE + V3UniqueNames m_names{"__Vrangedly"}; + AstNodeModule* m_modp = nullptr; // Current module + std::vector m_toDelete; // Nodes to delete after traversal + + struct SeqStep final { + AstNodeExpr* exprp; // Expression to check (nullptr if unary leading delay) + int delay; // Fixed delay after this expression (0 for tail) + bool isRange; // Whether this step's delay is a range + int rangeMin; + int rangeMax; + }; + + // Extract delay bounds from AstDelay. Clones and constifies (does not modify original AST). + bool extractDelayBounds(AstDelay* dlyp, bool& isRange, int& minVal, int& maxVal) { + isRange = dlyp->isRangeDelay(); + AstNodeExpr* const minExprp = V3Const::constifyEdit(dlyp->lhsp()->cloneTree(false)); + const AstConst* const minConstp = VN_CAST(minExprp, Const); + if (isRange) { + AstNodeExpr* const maxExprp = V3Const::constifyEdit(dlyp->rhsp()->cloneTree(false)); + const AstConst* const maxConstp = VN_CAST(maxExprp, Const); + if (!minConstp || !maxConstp) { + dlyp->v3error("Range delay bounds must be elaboration-time constants" + " (IEEE 1800-2023 16.7)"); + VL_DO_DANGLING(minExprp->deleteTree(), minExprp); + VL_DO_DANGLING(maxExprp->deleteTree(), maxExprp); + return false; + } + minVal = minConstp->toSInt(); + maxVal = maxConstp->toSInt(); + VL_DO_DANGLING(minExprp->deleteTree(), minExprp); + VL_DO_DANGLING(maxExprp->deleteTree(), maxExprp); + if (minVal < 0 || maxVal < 0) { + dlyp->v3error("Range delay bounds must be non-negative" + " (IEEE 1800-2023 16.7)"); + return false; + } + if (maxVal < minVal) { + dlyp->v3error("Range delay maximum must be >= minimum" + " (IEEE 1800-2023 16.7)"); + return false; + } + if (minVal == 0) { + dlyp->v3warn(E_UNSUPPORTED, "Unsupported: ##0 in range delays"); + return false; + } + } else { + minVal = maxVal = minConstp ? minConstp->toSInt() : 0; + VL_DO_DANGLING(minExprp->deleteTree(), minExprp); + } + return true; + } + + // Flatten a (possibly nested) SExpr tree into a linear vector of SeqSteps. + // SExpr trees are left-recursive: (a ##[1:2] b) ##1 c becomes + // SExpr(pre=SExpr(a, ##[1:2], b), ##1, c) + // Output for that example: [{a, range[1:2]}, {b, delay=1}, {c, delay=0}] + bool linearize(AstSExpr* rootp, std::vector& steps) { + bool hasRange = false; + linearizeImpl(rootp, steps, hasRange /*ref*/); + return hasRange; + } + + bool linearizeImpl(AstSExpr* curp, std::vector& steps, bool& hasRange) { + if (AstSExpr* const prep = VN_CAST(curp->preExprp(), SExpr)) { + if (!linearizeImpl(prep, steps, hasRange)) return false; + } + AstDelay* const dlyp = VN_CAST(curp->delayp(), Delay); + UASSERT_OBJ(dlyp, curp, "Expected AstDelay"); + bool isRange = false; + int minVal = 0, maxVal = 0; + if (!extractDelayBounds(dlyp, isRange, minVal, maxVal)) return false; + if (isRange) hasRange = true; + + if (curp->preExprp() && !VN_IS(curp->preExprp(), SExpr)) { + steps.push_back({curp->preExprp(), minVal, isRange, minVal, maxVal}); + } else { + steps.push_back({nullptr, minVal, isRange, minVal, maxVal}); + } + + if (AstSExpr* const nextp = VN_CAST(curp->exprp(), SExpr)) { + return linearizeImpl(nextp, steps, hasRange); + } + steps.push_back({curp->exprp(), 0, false, 0, 0}); + return true; + } + + // Build FSM body as if/else chain on state variable. + // State 0 = IDLE. Each range delay adds 2 states (wait + check), + // each fixed delay adds 1 (wait), each tail expr adds 1 (check). + // + // Example: a ##[M:N] b ##1 c + // steps: [{a, range[M:N]}, {b, delay=1}, {c, delay=0}] + // State 1: WAIT_MIN (count down M cycles) + // State 2: CHECK_RANGE (check b each cycle, up to N-M retries) + // State 3: WAIT_FIXED (count down 1 cycle for ##1) + // State 4: CHECK_TAIL (check c, report pass/fail) + AstNode* buildFsmBody(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, AstVar* failVarp, + const std::vector& steps, AstSenItem* sensesp, + AstNodeExpr* antExprp) { + + AstNode* fsmChainp = nullptr; + int nextState = 1; + + for (size_t i = 0; i < steps.size(); ++i) { + const SeqStep& step = steps[i]; + + if (step.isRange) { + // Range delay needs two states: WAIT_MIN and CHECK_RANGE + UASSERT(i + 1 < steps.size(), "Range must have next step"); + const int waitState = nextState++; + const int checkState = nextState++; + const int rangeWidth = step.rangeMax - step.rangeMin; + const SeqStep& nextStep = steps[i + 1]; + + const int afterMatchState = nextState; + + // WAIT_MIN: count down rangeMin cycles + { + AstNode* const bodyp = new AstIf{ + flp, + new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 0}}, + makeStateTransition(flp, stateVarp, cntVarp, checkState, rangeWidth), + new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, + new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 1}}}}; + fsmChainp = chainState(flp, fsmChainp, stateVarp, waitState, bodyp); + } + + // CHECK_RANGE: check expr each cycle, fail on timeout + { + AstNode* matchActionp = nullptr; + AstNode* const timeoutp = new AstBegin{flp, "", nullptr, true}; + VN_AS(timeoutp, Begin) + ->addStmtsp(new AstAssign{flp, + new AstVarRef{flp, failVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitTrue{}}}); + VN_AS(timeoutp, Begin) + ->addStmtsp(new AstAssign{flp, + new AstVarRef{flp, stateVarp, VAccess::WRITE}, + new AstConst{flp, 0}}); + AstNode* const decrementp + = new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, + new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 1}}}; + + AstIf* const failOrRetryp + = new AstIf{flp, + new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 0}}, + timeoutp, decrementp}; + + if (nextStep.delay > 0) { + matchActionp = makeStateTransition(flp, stateVarp, cntVarp, + afterMatchState, nextStep.delay - 1); + } else { + matchActionp + = makeStateTransition(flp, stateVarp, cntVarp, afterMatchState, 0); + } + + AstIf* const checkp + = new AstIf{flp, new AstSampled{flp, nextStep.exprp->cloneTree(false)}, + matchActionp, failOrRetryp}; + + fsmChainp = chainState(flp, fsmChainp, stateVarp, checkState, checkp); + } + + // Skip next step (already consumed as the range check target) + ++i; + continue; + + } else if (step.delay > 0) { + // Fixed delay: count down then advance + const int waitState = nextState++; + AstNode* const bodyp = new AstIf{ + flp, + new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 0}}, + new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, + new AstConst{flp, static_cast(nextState)}}, + new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, + new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, + new AstConst{flp, 1}}}}; + + fsmChainp = chainState(flp, fsmChainp, stateVarp, waitState, bodyp); + + } else if (i == steps.size() - 1 && step.exprp) { + // Tail: check final expression, pass or fail + const int checkState = nextState++; + AstNode* const passp = new AstAssign{ + flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, new AstConst{flp, 0}}; + AstBegin* const failp = new AstBegin{flp, "", nullptr, true}; + failp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, failVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitTrue{}}}); + failp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, + new AstConst{flp, 0}}); + + AstIf* const bodyp = new AstIf{ + flp, new AstSampled{flp, step.exprp->cloneTree(false)}, passp, failp}; + + fsmChainp = chainState(flp, fsmChainp, stateVarp, checkState, bodyp); + } + } + + // Build IDLE state (state 0): check trigger and start + AstNode* idleBodyp = nullptr; + const SeqStep& firstStep = steps[0]; + int initCnt = 0; + if (firstStep.isRange) { + initCnt = firstStep.rangeMin - 1; + } else { + initCnt = firstStep.delay - 1; + } + AstNode* const startActionp + = makeStateTransition(flp, stateVarp, cntVarp, 1, initCnt < 0 ? 0 : initCnt); + + // Trigger = antecedent (from implication) AND/OR first step expression + AstNodeExpr* triggerp = nullptr; + if (antExprp && firstStep.exprp) { + triggerp = new AstAnd{flp, new AstSampled{flp, antExprp->cloneTree(false)}, + new AstSampled{flp, firstStep.exprp->cloneTree(false)}}; + } else if (antExprp) { + triggerp = new AstSampled{flp, antExprp->cloneTree(false)}; + } else if (firstStep.exprp) { + triggerp = new AstSampled{flp, firstStep.exprp->cloneTree(false)}; + } + + if (triggerp) { + triggerp->dtypeSetBit(); + idleBodyp = new AstIf{flp, triggerp, startActionp, nullptr}; + } else { + // Unary form with no antecedent: start unconditionally each cycle + idleBodyp = startActionp; + } + + // Chain: if (state == 0) idle else if (state == 1) ... else ... + AstIf* const idleIfp = new AstIf{ + flp, + new AstEq{flp, new AstVarRef{flp, stateVarp, VAccess::READ}, new AstConst{flp, 0}}, + idleBodyp, fsmChainp}; + + // Reset fail flag at top of each cycle + AstNode* const resetFailp + = new AstAssign{flp, new AstVarRef{flp, failVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitFalse{}}}; + resetFailp->addNext(idleIfp); + return resetFailp; + } + + // Helper: generate state = newState; cnt = initCnt; + AstNode* makeStateTransition(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, int newState, + int initCnt) { + AstBegin* const blockp = new AstBegin{flp, "", nullptr, true}; + blockp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, + new AstConst{flp, static_cast(newState)}}); + blockp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE}, + new AstConst{flp, static_cast(initCnt)}}); + return blockp; + } + + // Helper: chain a state check into the if/else chain + // Builds: if (state == stateNum) { body } else { existing chain } + AstNode* chainState(FileLine* flp, AstNode* existingChainp, AstVar* stateVarp, int stateNum, + AstNode* bodyp) { + AstIf* const ifp = new AstIf{flp, + new AstEq{flp, new AstVarRef{flp, stateVarp, VAccess::READ}, + new AstConst{flp, static_cast(stateNum)}}, + bodyp, existingChainp}; + return ifp; + } + + // Recursively check if any delay in the SExpr tree is a range delay + static bool containsRangeDelay(AstSExpr* nodep) { + if (AstDelay* const dlyp = VN_CAST(nodep->delayp(), Delay)) { + if (dlyp->isRangeDelay()) return true; + } + if (AstSExpr* const prep = VN_CAST(nodep->preExprp(), SExpr)) { + if (containsRangeDelay(prep)) return true; + } + if (AstSExpr* const exprp = VN_CAST(nodep->exprp(), SExpr)) { + if (containsRangeDelay(exprp)) return true; + } + return false; + } + + // Find the clock sensitivity for this SExpr by searching up the tree + AstSenItem* findClock(AstNode* nodep) { + for (AstNode* curp = nodep; curp; curp = curp->backp()) { + if (AstPropSpec* const specp = VN_CAST(curp, PropSpec)) { + if (specp->sensesp()) return specp->sensesp(); + } + } + nodep->v3fatalSrc("Range delay SExpr without clocking event"); + return nullptr; + } + + // Find implication antecedent if this SExpr is the RHS of |-> or |=> + // The FSM absorbs the antecedent as its trigger so the implication node + // can be removed -- otherwise fail timing wouldn't align with the trigger. + std::pair findAntecedent(AstNode* nodep) { + for (AstNode* curp = nodep; curp; curp = curp->backp()) { + if (AstImplication* const implp = VN_CAST(curp, Implication)) { + return {implp->lhsp(), implp->isOverlapped()}; + } + } + return {nullptr, false}; + } + + // VISITORS + void visit(AstNodeModule* nodep) override { + VL_RESTORER(m_modp); + m_modp = nodep; + iterateChildren(nodep); + } + + void visit(AstSExpr* nodep) override { + if (!containsRangeDelay(nodep)) { + iterateChildren(nodep); + return; + } + std::vector steps; + if (!linearize(nodep, steps)) { + nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}}); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + return; + } + + FileLine* const flp = nodep->fileline(); + + // Find clock for the FSM (unclocked assertions are caught by V3Assert) + AstSenItem* const sensesp = findClock(nodep); + UASSERT_OBJ(sensesp, nodep, "Range delay SExpr without clocking event"); + + UASSERT_OBJ(m_modp, nodep, "Range delay SExpr not under a module"); + + // Find antecedent (if inside implication) + const std::pair antResult = findAntecedent(nodep); + AstNodeExpr* const antExprp = antResult.first; + // const bool isOverlapped = antResult.second; // Reserved for |=> support + + // Create module-level state variables + const std::string baseName = m_names.get(nodep); + AstVar* const stateVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__state", + nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; + stateVarp->lifetime(VLifetime::STATIC_EXPLICIT); + AstVar* const cntVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__cnt", + nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; + cntVarp->lifetime(VLifetime::STATIC_EXPLICIT); + AstVar* const failVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__fail", + nodep->findBasicDType(VBasicDTypeKwd::BIT)}; + failVarp->lifetime(VLifetime::STATIC_EXPLICIT); + + // Build FSM body + AstNode* const fsmBodyp + = buildFsmBody(flp, stateVarp, cntVarp, failVarp, steps, sensesp, antExprp); + + // Create Always block for the FSM (same scheduling as assertion always blocks) + AstAlways* const alwaysp = new AstAlways{ + flp, VAlwaysKwd::ALWAYS, new AstSenTree{flp, sensesp->cloneTree(false)}, fsmBodyp}; + + // Add state vars and always block to module + m_modp->addStmtsp(stateVarp); + m_modp->addStmtsp(cntVarp); + m_modp->addStmtsp(failVarp); + m_modp->addStmtsp(alwaysp); + + // Replace with !fail expression (combinational check). + // If inside an implication, replace the entire implication since + // the FSM already handles the antecedent. + AstNodeExpr* const checkp = new AstNot{flp, new AstVarRef{flp, failVarp, VAccess::READ}}; + checkp->dtypeSetBit(); + + if (antExprp) { + // Find the implication, replace it with the check, defer deletion + for (AstNode* curp = nodep->backp(); curp; curp = curp->backp()) { + if (AstImplication* const implp = VN_CAST(curp, Implication)) { + implp->replaceWith(checkp); + m_toDelete.push_back(implp); + break; + } + } + } else { + nodep->replaceWith(checkp); + VL_DO_DANGLING(nodep->deleteTree(), nodep); + } + } + + void visit(AstNode* nodep) override { iterateChildren(nodep); } + +public: + explicit RangeDelayExpander(AstNetlist* nodep) { + iterate(nodep); + for (AstNode* const np : m_toDelete) np->deleteTree(); + } +}; + //###################################################################### // Top AssertProp class void V3AssertProp::assertPropAll(AstNetlist* nodep) { UINFO(2, __FUNCTION__ << ":"); + { RangeDelayExpander{nodep}; } { AssertPropLowerVisitor{nodep}; } { V3Graph graph; diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 76f32b64a..5a332599c 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -541,8 +541,9 @@ public: }; class AstDelay final : public AstNodeStmt { // Delay statement - // @astgen op1 := lhsp : AstNodeExpr // Delay value + // @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) VTimescale m_timeunit; // Delay's time unit const bool m_isCycle; // True if it is a cycle delay @@ -560,6 +561,7 @@ public: void timeunit(const VTimescale& flag) { m_timeunit = flag; } VTimescale timeunit() const { return m_timeunit; } bool isCycleDelay() const { return m_isCycle; } + bool isRangeDelay() const { return rhsp() != nullptr; } }; class AstDisable final : public AstNodeStmt { // @astgen op1 := targetRefp : Optional[AstNodeExpr] // Reference to link in V3LinkDot diff --git a/src/verilog.y b/src/verilog.y index bb23f452c..cb94e8531 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6864,10 +6864,9 @@ cycle_delay_range: // IEEE: ==cycle_delay_range // // UNSUP: This causes a big grammar ambiguity // // as ()'s mismatch between primary and the following statement // // the sv-ac committee has been asked to clarify (Mantis 1901) - | yP_POUNDPOUND anyrange - { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true}; - DEL($2); - BBUNSUP($1, "Unsupported: ## range cycle delay range expression"); } + | yP_POUNDPOUND '[' constExpr ':' constExpr ']' + { $$ = new AstDelay{$1, $3, true}; + $$->rhsp($5); } | yP_POUNDPOUND yP_BRASTAR ']' { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true}; BBUNSUP($1, "Unsupported: ## [*] cycle delay range expression"); } diff --git a/test_regress/t/t_property_sexpr_parse_unsup.out b/test_regress/t/t_property_sexpr_parse_unsup.out index 6d775621a..73d3d9bbc 100644 --- a/test_regress/t/t_property_sexpr_parse_unsup.out +++ b/test_regress/t/t_property_sexpr_parse_unsup.out @@ -1,10 +1,7 @@ -%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:29: Unsupported: ## range cycle delay range expression - 65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b]; - | ^~ - ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:51: Unsupported: [-> boolean abbrev expression 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest %Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:54: Unsupported: boolean abbrev (in sequence expression) 82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5; | ^ diff --git a/test_regress/t/t_property_sexpr_range_delay.py b/test_regress/t/t_property_sexpr_range_delay.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_property_sexpr_range_delay.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_property_sexpr_range_delay.v b/test_regress/t/t_property_sexpr_range_delay.v new file mode 100644 index 000000000..69db759c8 --- /dev/null +++ b/test_regress/t/t_property_sexpr_range_delay.v @@ -0,0 +1,88 @@ +// 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); +// verilog_format: on + +module t ( + input clk +); + integer cyc = 0; + reg [63:0] crc = '0; + reg [63:0] sum = '0; + + // Derive test signals from CRC + wire a = crc[0]; + wire b = crc[1]; + wire c = crc[2]; + + wire [63:0] result = {61'h0, c, b, a}; + + always_ff @(posedge clk) begin +`ifdef TEST_VERBOSE + $write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b\n", + $time, cyc, crc, a, b, c); +`endif + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + sum <= result ^ {sum[62:0], sum[63] ^ sum[2] ^ sum[0]}; + + if (cyc == 0) begin + crc <= 64'h5aef0c8d_d70a4497; + sum <= '0; + end else if (cyc < 10) begin + sum <= '0; + end else if (cyc == 99) begin + `checkh(crc, 64'hc77bb9b3784ea091); + `checkh(sum, 64'h38c614665c6b71ad); + $write("*-* All Finished *-*\n"); + $finish; + end + end + + // Basic ##[1:3] range delay (CRC-driven, always-true consequent) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[1:3] 1'b1); + + // ##[2:4] range delay + assert property (@(posedge clk) disable iff (cyc < 2) + b |-> ##[2:4] 1'b1); + + // Degenerate ##[2:2] (equivalent to ##2) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[2:2] 1'b1); + + // Multi-step: ##[1:2] then ##1 (both consequents always true) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[1:2] 1'b1 ##1 1'b1); + + // Large range ##[1:10000] (scalability, O(1) code size) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[1:10000] 1'b1); + + // Range with binary SExpr: nextStep has delay > 0 after range match + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> b ##[1:2] 1'b1 ##3 1'b1); + + // Binary SExpr without implication (covers firstStep.exprp path without antecedent) + assert property (@(posedge clk) disable iff (cyc < 2) + a ##[1:3] 1'b1); + + // Implication with binary SExpr RHS (covers antExprp AND firstStep.exprp) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> b ##[1:2] 1'b1); + + // Fixed delay before range (covers firstStep.delay path in IDLE) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##2 1'b1 ##[1:3] 1'b1); + + // Unary range with no antecedent and no preExpr (covers unconditional start) + assert property (@(posedge clk) disable iff (cyc < 2) + ##[1:3] 1'b1); + +endmodule diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.out b/test_regress/t/t_property_sexpr_range_delay_bad.out new file mode 100644 index 000000000..d83ac4143 --- /dev/null +++ b/test_regress/t/t_property_sexpr_range_delay_bad.out @@ -0,0 +1,19 @@ +%Error: t/t_property_sexpr_range_delay_bad.v:18:45: Range delay bounds must be elaboration-time constants (IEEE 1800-2023 16.7) + : ... note: In instance 't' + 18 | a1: assert property (@(posedge clk) a |-> ##[1:cyc] b); + | ^~ + ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. +%Error: t/t_property_sexpr_range_delay_bad.v:21:45: Range delay bounds must be non-negative (IEEE 1800-2023 16.7) + : ... note: In instance 't' + 21 | a2: assert property (@(posedge clk) a |-> ##[-1:3] b); + | ^~ +%Error: t/t_property_sexpr_range_delay_bad.v:24:45: Range delay maximum must be >= minimum (IEEE 1800-2023 16.7) + : ... note: In instance 't' + 24 | a3: assert property (@(posedge clk) a |-> ##[5:2] b); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:27:45: Unsupported: ##0 in range delays + : ... note: In instance 't' + 27 | a4: assert property (@(posedge clk) a |-> ##[0:3] b); + | ^~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.py b/test_regress/t/t_property_sexpr_range_delay_bad.py new file mode 100755 index 000000000..504773395 --- /dev/null +++ b/test_regress/t/t_property_sexpr_range_delay_bad.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_property_sexpr_range_delay_bad.v b/test_regress/t/t_property_sexpr_range_delay_bad.v new file mode 100644 index 000000000..19441f50d --- /dev/null +++ b/test_regress/t/t_property_sexpr_range_delay_bad.v @@ -0,0 +1,29 @@ +// 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; + + always @(posedge clk) cyc <= cyc + 1; + + // Non-constant bounds + a1: assert property (@(posedge clk) a |-> ##[1:cyc] b); + + // Negative bound + a2: assert property (@(posedge clk) a |-> ##[-1:3] b); + + // Max < min + a3: assert property (@(posedge clk) a |-> ##[5:2] b); + + // ##0 in range + a4: assert property (@(posedge clk) a |-> ##[0:3] b); + +endmodule diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index 33cf25b94..51fcc05ab 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -8,18 +8,12 @@ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:50:7: Unsupported: intersect (in sequence expression) 50 | a intersect b; | ^~~~~~~~~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:60:5: Unsupported: ## range cycle delay range expression - 60 | ## [1:2] b; - | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:63:5: Unsupported: ## [*] cycle delay range expression 63 | ## [*] b; | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:66:5: Unsupported: ## [+] cycle delay range expression 66 | ## [+] b; | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:76:7: Unsupported: ## range cycle delay range expression - 76 | a ## [1:2] b; - | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:79:7: Unsupported: ## [*] cycle delay range expression 79 | a ## [*] b; | ^~