From 3cc75be0a602a5b78f24e952956a5c349c6b6288 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Sat, 4 Apr 2026 23:32:17 +0200 Subject: [PATCH] Support ##[*], ##[+], ##[M:$] unbounded cycle delays in SVA properties --- src/V3AssertProp.cpp | 320 +++++++++++------- src/V3AstNodeStmt.h | 1 + src/verilog.y | 8 +- test_regress/t/t_prop_unbounded_delay.py | 18 + test_regress/t/t_prop_unbounded_delay.v | 115 +++++++ .../t/t_property_sexpr_range_delay_bad.out | 6 +- .../t/t_property_sexpr_range_delay_bad.v | 3 + test_regress/t/t_sequence_sexpr_unsup.out | 12 - 8 files changed, 346 insertions(+), 137 deletions(-) create mode 100755 test_regress/t/t_prop_unbounded_delay.py create mode 100644 test_regress/t/t_prop_unbounded_delay.v diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index 6888284c4..89a517e64 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -602,44 +602,68 @@ class RangeDelayExpander final : public VNVisitor { 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 + bool isUnbounded; // Whether the range is unbounded (rhs is AstUnbounded) int rangeMin; - int rangeMax; + int rangeMax; // -1 for unbounded }; // Extract delay bounds from AstDelay. Clones and constifies (does not modify original AST). - bool extractDelayBounds(AstDelay* dlyp, bool& isRange, int& minVal, int& maxVal) { + // For unbounded ranges (rhs is AstUnbounded), maxVal is set to -1; rhsp is not constified. + bool extractDelayBounds(AstDelay* dlyp, bool& isRange, bool& isUnbounded, int& minVal, + int& maxVal) { isRange = dlyp->isRangeDelay(); + isUnbounded = dlyp->isUnbounded(); 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)"); + if (isUnbounded) { + // ##[M:$], ##[*], ##[+]: only min bound; max is open-ended + if (!minConstp) { + dlyp->v3error("Range delay minimum must be an elaboration-time constant" + " (IEEE 1800-2023 16.7)"); + VL_DO_DANGLING(minExprp->deleteTree(), minExprp); + return false; + } + minVal = minConstp->toSInt(); + maxVal = -1; + VL_DO_DANGLING(minExprp->deleteTree(), minExprp); + if (minVal < 0) { + dlyp->v3error("Range delay bounds must be non-negative" + " (IEEE 1800-2023 16.7)"); + return false; + } + } else { + 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); - 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; + 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 bounded range delays"); + return false; + } } } else { + isUnbounded = false; minVal = maxVal = minConstp ? minConstp->toSInt() : 0; VL_DO_DANGLING(minExprp->deleteTree(), minExprp); } @@ -663,127 +687,165 @@ class RangeDelayExpander final : public VNVisitor { AstDelay* const dlyp = VN_CAST(curp->delayp(), Delay); UASSERT_OBJ(dlyp, curp, "Expected AstDelay"); bool isRange = false; + bool isUnbounded = false; int minVal = 0; int maxVal = 0; - if (!extractDelayBounds(dlyp, isRange, minVal, maxVal)) return false; + if (!extractDelayBounds(dlyp, isRange, isUnbounded, 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}); + steps.push_back({curp->preExprp(), minVal, isRange, isUnbounded, minVal, maxVal}); } else { - steps.push_back({nullptr, minVal, isRange, minVal, maxVal}); + steps.push_back({nullptr, minVal, isRange, isUnbounded, 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}); + steps.push_back({curp->exprp(), 0, false, 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) { + // Pre-assigned state numbers for one SeqStep. + // Range steps consume their successor (check target); successor entry is unused. + struct StepBounds { + int waitState; // WAIT_MIN state, or -1 if not needed + int checkState; // CHECK or TAIL state; -1 for fixed-delay steps + }; + // Assign state numbers to all steps before building FSM bodies. + // + // State layout for a ##[M:N] b ##1 c (bounded, M>0): + // State 0: IDLE -- detect trigger, launch FSM + // State 1: WAIT_MIN -- count down M-1 cycles + // State 2: CHECK -- sample b; fail after N-M retries + // State 3: WAIT_FIX -- count down 1 cycle for ##1 + // State 4: TAIL -- sample c, report pass/fail + // + // For ##[M:$] b ... (unbounded, M>1): same as bounded but CHECK has no timeout. + // For ##[+] b (unbounded, M=1): WAIT_MIN skipped; CHECK is state 1. + // For ##[*] b (unbounded, M=0): handled in IDLE directly (no WAIT_MIN). + // + // LIMITATION: single-evaluation FSM -- overlapping triggers are ignored + // while the FSM is active. For ##[M:$], if the consequent never becomes + // true the FSM remains in CHECK indefinitely, blocking new evaluations. + std::vector preAssignStates(const std::vector& steps) { + std::vector bounds(steps.size(), {-1, -1}); + int s = 1; + for (size_t i = 0; i < steps.size(); ++i) { + const SeqStep& step = steps[i]; + if (step.isRange) { + // Unbounded with min<=1: no WAIT_MIN (counter starts at 0 in CHECK). + const bool needsWait = !step.isUnbounded || step.rangeMin > 1; + if (needsWait) bounds[i].waitState = s++; + bounds[i].checkState = s++; + ++i; // step[i+1] is the check target, not a separate FSM state + } else if (step.delay > 0) { + bounds[i].waitState = s++; + } else { + bounds[i].checkState = s++; // tail check + } + } + return bounds; + } + + // Build the match action for a range CHECK state. + // isTail=true: return to IDLE; isTail=false: advance to afterMatchState. + AstNode* makeOnMatchAction(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, bool isTail, + int afterMatchState, int nextDelay) { + if (isTail) { + return new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, + new AstConst{flp, 0}}; + } + return makeStateTransition(flp, stateVarp, cntVarp, afterMatchState, + nextDelay > 0 ? nextDelay - 1 : 0); + } + + // Build the body of a range CHECK state. + // Bounded: fail on timeout, decrement counter otherwise. + // Unbounded: stay until match (no timeout). + AstNode* makeRangeCheckBody(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, + AstVar* failVarp, AstNodeExpr* exprp, AstNode* matchActionp, + bool isUnbounded) { + if (isUnbounded) { + return new AstIf{flp, new AstSampled{flp, exprp->cloneTree(false)}, matchActionp, + nullptr}; + } + AstBegin* const timeoutp = new AstBegin{flp, "", nullptr, true}; + timeoutp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, failVarp, VAccess::WRITE}, + new AstConst{flp, AstConst::BitTrue{}}}); + timeoutp->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}; + return new AstIf{flp, new AstSampled{flp, exprp->cloneTree(false)}, matchActionp, + failOrRetryp}; + } + + AstNode* buildFsmBody(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, AstVar* failVarp, + const std::vector& steps, AstNodeExpr* antExprp) { + + const std::vector bounds = preAssignStates(steps); 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 = bounds[i].checkState + 1; + const bool isTail = (i + 2 >= steps.size() && nextStep.delay == 0); - const int afterMatchState = nextState; - - // WAIT_MIN: count down rangeMin cycles - { - AstNode* const bodyp = new AstIf{ + // WAIT_MIN state: count down rangeMin-1 cycles before entering CHECK + if (bounds[i].waitState >= 0) { + const int initCnt + = step.isUnbounded ? 0 : (step.rangeMax - step.rangeMin); + AstNode* const waitBodyp = new AstIf{ flp, new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ}, new AstConst{flp, 0}}, - makeStateTransition(flp, stateVarp, cntVarp, checkState, rangeWidth), + makeStateTransition(flp, stateVarp, cntVarp, bounds[i].checkState, + initCnt), 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); + fsmChainp + = chainState(flp, fsmChainp, stateVarp, bounds[i].waitState, waitBodyp); } - // 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}}}; + // CHECK state: sample consequent each cycle + AstNode* const matchActionp = makeOnMatchAction(flp, stateVarp, cntVarp, isTail, + afterMatchState, nextStep.delay); + AstNode* const checkBodyp + = makeRangeCheckBody(flp, stateVarp, cntVarp, failVarp, nextStep.exprp, + matchActionp, step.isUnbounded); + fsmChainp + = chainState(flp, fsmChainp, stateVarp, bounds[i].checkState, checkBodyp); - 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; + ++i; // step[i+1] consumed as the CHECK target continue; } else if (step.delay > 0) { - // Fixed delay: count down then advance - const int waitState = nextState++; + // Fixed delay: count down then advance to next state + const int nextStateNum = bounds[i].waitState + 1; 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 AstConst{flp, static_cast(nextStateNum)}}, 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); + fsmChainp = chainState(flp, fsmChainp, stateVarp, bounds[i].waitState, bodyp); } else if (i == steps.size() - 1 && step.exprp) { - // Tail: check final expression, pass or fail - const int checkState = nextState++; + // Tail: sample final expression, report pass/fail AstNode* const passp = new AstAssign{ flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, new AstConst{flp, 0}}; AstBegin* const failp = new AstBegin{flp, "", nullptr, true}; @@ -791,27 +853,17 @@ class RangeDelayExpander final : public VNVisitor { 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); + fsmChainp = chainState(flp, fsmChainp, stateVarp, bounds[i].checkState, bodyp); } } - // Build IDLE state (state 0): check trigger and start + // Build IDLE state (state 0) 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 + // Trigger = antecedent AND/OR first step expression AstNodeExpr* triggerp = nullptr; if (antExprp && firstStep.exprp) { triggerp = new AstAnd{flp, new AstSampled{flp, antExprp->cloneTree(false)}, @@ -822,12 +874,37 @@ class RangeDelayExpander final : public VNVisitor { triggerp = new AstSampled{flp, firstStep.exprp->cloneTree(false)}; } - if (triggerp) { - triggerp->dtypeSetBit(); - idleBodyp = new AstIf{flp, triggerp, startActionp, nullptr}; + if (firstStep.isUnbounded && firstStep.rangeMin == 0 && steps.size() > 1) { + // ##[*] / ##[0:$]: check consequent immediately in IDLE. + // On ##0 match: perform match action without entering CHECK. + // On no match: enter CHECK (state bounds[0].checkState) to wait. + const SeqStep& nextStep = steps[1]; + const int checkState = bounds[0].checkState; + const int afterMatch = checkState + 1; + const bool isTail = (steps.size() == 2 && nextStep.delay == 0); + AstNodeExpr* const immCheckp = new AstSampled{flp, nextStep.exprp->cloneTree(false)}; + immCheckp->dtypeSetBit(); + AstNode* const immMatchp + = makeOnMatchAction(flp, stateVarp, cntVarp, isTail, afterMatch, nextStep.delay); + AstNode* const toCheckp = makeStateTransition(flp, stateVarp, cntVarp, checkState, 0); + AstIf* const starBodyp = new AstIf{flp, immCheckp, immMatchp, toCheckp}; + if (triggerp) { + triggerp->dtypeSetBit(); + idleBodyp = new AstIf{flp, triggerp, starBodyp, nullptr}; + } else { + idleBodyp = starBodyp; + } } else { - // Unary form with no antecedent: start unconditionally each cycle - idleBodyp = startActionp; + // Standard start: transition to state 1 with appropriate counter + int initCnt = firstStep.isRange ? firstStep.rangeMin - 1 : firstStep.delay - 1; + AstNode* const startActionp + = makeStateTransition(flp, stateVarp, cntVarp, 1, initCnt < 0 ? 0 : initCnt); + if (triggerp) { + triggerp->dtypeSetBit(); + idleBodyp = new AstIf{flp, triggerp, startActionp, nullptr}; + } else { + idleBodyp = startActionp; + } } // Chain: if (state == 0) idle else if (state == 1) ... else ... @@ -940,16 +1017,19 @@ class RangeDelayExpander final : public VNVisitor { AstVar* const stateVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__state", nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; stateVarp->lifetime(VLifetime::STATIC_EXPLICIT); + stateVarp->noSample(true); AstVar* const cntVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__cnt", nodep->findBasicDType(VBasicDTypeKwd::UINT32)}; cntVarp->lifetime(VLifetime::STATIC_EXPLICIT); + cntVarp->noSample(true); AstVar* const failVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__fail", nodep->findBasicDType(VBasicDTypeKwd::BIT)}; failVarp->lifetime(VLifetime::STATIC_EXPLICIT); + failVarp->noSample(true); // Build FSM body AstNode* const fsmBodyp - = buildFsmBody(flp, stateVarp, cntVarp, failVarp, steps, sensesp, antExprp); + = buildFsmBody(flp, stateVarp, cntVarp, failVarp, steps, antExprp); // Create Always block for the FSM (same scheduling as assertion always blocks) AstAlways* const alwaysp = new AstAlways{ diff --git a/src/V3AstNodeStmt.h b/src/V3AstNodeStmt.h index 5a332599c..591afcb6c 100644 --- a/src/V3AstNodeStmt.h +++ b/src/V3AstNodeStmt.h @@ -562,6 +562,7 @@ public: VTimescale timeunit() const { return m_timeunit; } bool isCycleDelay() const { return m_isCycle; } bool isRangeDelay() const { return rhsp() != nullptr; } + bool isUnbounded() const { return rhsp() && VN_IS(rhsp(), Unbounded); } }; 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 acf14048c..30f842d9e 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6885,11 +6885,11 @@ cycle_delay_range: // IEEE: ==cycle_delay_range { $$ = 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"); } + { $$ = new AstDelay{$1, new AstConst{$1, 0}, true}; + $$->rhsp(new AstUnbounded{$1}); } | yP_POUNDPOUND yP_BRAPLUSKET - { $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true}; - BBUNSUP($1, "Unsupported: ## [+] cycle delay range expression"); } + { $$ = new AstDelay{$1, new AstConst{$1, 1}, true}; + $$->rhsp(new AstUnbounded{$1}); } ; sequence_match_itemList: // IEEE: [sequence_match_item] part of sequence_expr diff --git a/test_regress/t/t_prop_unbounded_delay.py b/test_regress/t/t_prop_unbounded_delay.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_prop_unbounded_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_prop_unbounded_delay.v b/test_regress/t/t_prop_unbounded_delay.v new file mode 100644 index 000000000..5b33dc8db --- /dev/null +++ b/test_regress/t/t_prop_unbounded_delay.v @@ -0,0 +1,115 @@ +// 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 + + // ##[+] with always-true consequent (wait >= 1 cycle, then check 1'b1) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[+] 1'b1); + + // ##[*] with always-true consequent (wait >= 0 cycles, then check 1'b1) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[*] 1'b1); + + // ##[2:$] unbounded with min > 1 + assert property (@(posedge clk) disable iff (cyc < 2) + b |-> ##[2:$] 1'b1); + + // ##[1:$] explicit unbounded (equivalent to ##[+]) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[1:$] 1'b1); + + // Unary ##[+] without antecedent + assert property (@(posedge clk) disable iff (cyc < 2) + ##[+] 1'b1); + + // Unary ##[*] without antecedent + assert property (@(posedge clk) disable iff (cyc < 2) + ##[*] 1'b1); + + // Multi-step: ##[+] then ##1 (tests afterMatchState jump) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[+] 1'b1 ##1 1'b1); + + // Multi-step: ##[*] then ##1 (tests ##[*] immediate match + continuation) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[*] 1'b1 ##1 1'b1); + + // Multi-step: ##[3:$] then ##2 (larger min + continuation) + assert property (@(posedge clk) disable iff (cyc < 2) + b |-> ##[3:$] 1'b1 ##2 1'b1); + + // Binary form without implication: a ##[+] b (no antecedent path) + assert property (@(posedge clk) disable iff (cyc < 2) + a ##[+] 1'b1); + + // Binary form without implication: a ##[*] b (no antecedent path) + assert property (@(posedge clk) disable iff (cyc < 2) + a ##[*] 1'b1); + + // Large min: ##[5:$] (multi-cycle WAIT_MIN countdown) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[5:$] 1'b1); + + // --- Non-trivial consequents: exercise CHECK "stay" path --- + + // ##[+] with CRC signal: wait 1+ cycles for b (exercises match-or-stay) + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[+] b); + + // ##[*] with CRC signal: immediate or deferred match of c + assert property (@(posedge clk) disable iff (cyc < 2) + a |-> ##[*] c); + + // ##[2:$] with CRC signal: min wait then check b (WAIT_MIN + CHECK unbounded) + assert property (@(posedge clk) disable iff (cyc < 2) + b |-> ##[2:$] a); + + // Binary form with CRC signal: a ##[+] b (no implication) + assert property (@(posedge clk) disable iff (cyc < 2) + a ##[+] b); + +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 index d83ac4143..a8b4d4584 100644 --- a/test_regress/t/t_property_sexpr_range_delay_bad.out +++ b/test_regress/t/t_property_sexpr_range_delay_bad.out @@ -11,9 +11,13 @@ : ... 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 +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:27:45: Unsupported: ##0 in bounded 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: t/t_property_sexpr_range_delay_bad.v:30:45: Range delay minimum must be an elaboration-time constant (IEEE 1800-2023 16.7) + : ... note: In instance 't' + 30 | a5: assert property (@(posedge clk) a |-> ##[cyc:$] b); + | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.v b/test_regress/t/t_property_sexpr_range_delay_bad.v index 19441f50d..bfefb738e 100644 --- a/test_regress/t/t_property_sexpr_range_delay_bad.v +++ b/test_regress/t/t_property_sexpr_range_delay_bad.v @@ -26,4 +26,7 @@ module t; // ##0 in range a4: assert property (@(posedge clk) a |-> ##[0:3] b); + // Non-constant minimum in unbounded range + a5: assert property (@(posedge clk) a |-> ##[cyc:$] b); + endmodule diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index e97f8e521..a7e52a13a 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -8,18 +8,6 @@ %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: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:79:7: Unsupported: ## [*] cycle delay range expression - 79 | a ## [*] b; - | ^~ -%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:82:7: Unsupported: ## [+] cycle delay range expression - 82 | a ## [+] b; - | ^~ %Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: [*] boolean abbrev expression 89 | a [*]; | ^~