diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 249326f07..5d99415e5 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -335,6 +335,7 @@ class SvaNfaBuilder final { bool m_isCoverSeq = false; // Unsupported endpoint topology must reject, not ignore, or the wait hangs bool m_isSeqEvent = false; + bool m_inSequencePrefix = false; // Prefix composition does not preserve every endpoint struct RangeDelayRejectInfo final { SvaStateVertex* startp = nullptr; @@ -585,10 +586,13 @@ class SvaNfaBuilder final { // Build NFA for an SExpr. finalCond = RHS (not yet added as a vertex). // isTopLevelStep: marks outermost required boolean check as rejectOnFail. // Apply a range delay `##[M:N]` to currentp. Returns true on success. On - // failure, sets outErrorEmitted per semantic-error policy and returns false. - bool applyRangeDelay(AstDelay* delayp, AstNodeExpr* rhsExprp, SvaStateVertex*& currentp, - std::vector& midSources, FileLine* flp, - bool& outErrorEmitted, RangeDelayRejectInfo* rangeRejectInfop = nullptr) { + // failure, emits a diagnostic and returns false. + bool applyRangeDelay(AstSExpr* sexprp, SvaStateVertex*& currentp, + std::vector& midSources, + RangeDelayRejectInfo* rangeRejectInfop = nullptr) { + FileLine* const flp = sexprp->fileline(); + AstDelay* const delayp = VN_AS(sexprp->delayp(), Delay); + AstNodeExpr* const rhsExprp = sexprp->exprp(); const unsigned minDelay = getConstUInt(delayp->lhsp()); if (delayp->isUnbounded()) { // `##[M:$]`: wait M cycles, then retain every matured attempt in a @@ -613,62 +617,42 @@ class SvaNfaBuilder final { } const unsigned range = maxDelay - minDelay; currentp = addDelayChain(currentp, minDelay, flp); - // kChainLimit bounds per-attempt unrolled vertices. Above this, a - // ring buffer (constant-size state) is used instead, so the vertex - // count is O(1) in range regardless of user input; no adversarial N - // blowup is possible. - constexpr unsigned kChainLimit = 256; - // IEEE 1800-2023 16.14.3: only a small bounded range before a plain - // boolean enumerates every end-of-match below. The large-range ring uses - // first-match clearing and the nested-sequence merge collapses ends, so - // reject those for a cover sequence rather than under-count. - if (m_isCoverSeq && (range > kChainLimit || VN_IS(rhsExprp, SExpr))) { + const bool multiCycleRhs = rhsExprp->isMultiCycleSva(); + const AstNodeExpr* const preExprp = sexprp->preExprp(); + // Prefix and nested-sequence composition can lose endpoints or their multiplicity + // required by cover sequence (IEEE 1800-2023 16.14.3), regardless of the range width. + if (m_isCoverSeq + && (multiCycleRhs || m_inSequencePrefix + || (preExprp && preExprp->isMultiCycleSva()))) { warnEndpointUnsupported(flp, "this ranged cycle delay"); - outErrorEmitted = true; return false; } - if (range > kChainLimit) { - currentp = addDelayChain(currentp, range + 1U, flp, false, - rhsExprp->isMultiCycleSva() ? nullptr : rhsExprp); - } else if (VN_IS(rhsExprp, SExpr)) { - // Nested-SExpr RHS: merge all [M,N] positions. Candidate-local misses - // are not assertion rejects while a later position can still match. + if (m_inSequencePrefix) { + flp->v3warn(E_UNSUPPORTED, + "Unsupported: Bounded ranged cycle delay in a sequence prefix"); + return false; + } + if (multiCycleRhs) { + // Launch a candidate at every eligible tick. Candidate-local misses are not + // assertion rejects while a later position can still match. if (rangeRejectInfop) { const int rhsLen = fixedLength(rhsExprp); if (rhsLen >= 0) *rangeRejectInfop = {currentp, range, rhsLen}; } + SvaStateVertex* const tailp = addDelayChain(currentp, range + 1U, flp, false); SvaStateVertex* const mergeVtxp = scopedCreateVertex(); mergeVtxp->m_isUnbounded = true; guardedLink(currentp, mergeVtxp, flp); - for (unsigned i = 0; i < range; ++i) { - SvaStateVertex* const nextVtxp = scopedCreateVertex(); - guardedEdge(currentp, nextVtxp, flp); - guardedLink(nextVtxp, mergeVtxp, flp); - currentp = nextVtxp; - } + guardedLink(tailp, mergeVtxp, flp); currentp = mergeVtxp; m_inUnboundedScope = true; } else { - // Pure boolean RHS: register chain. Each mid-position links to - // match (match-only); last position is the reject source. - // For cover_sequence (IEEE 1800-2023 16.14.3) the advance edge is - // unconditional so every (start, end) pair fires independently -- - // dropping NOT(b) turns "first-match-wins" into "every end fires". - AstVar* const hoistVarp - = m_isCoverSeq ? nullptr : tryHoistSampled(rhsExprp, flp, range); + // The first eligible tick is explicit. The ring retains attempts for the + // remaining ticks and exposes the final tick for rejection. Only properties + // clear on success, since cover sequence counts every endpoint. midSources.push_back(currentp); - for (unsigned i = 0; i < range; ++i) { - SvaStateVertex* const nextVtxp = scopedCreateVertex(); - if (m_isCoverSeq) { - guardedEdge(currentp, nextVtxp, flp); - } else { - AstNodeExpr* const notExprp - = new AstLogNot{flp, sampledRefOrClone(hoistVarp, rhsExprp, flp)}; - guardedEdge(currentp, nextVtxp, notExprp, flp); - } - if (i < range - 1) midSources.push_back(nextVtxp); - currentp = nextVtxp; - } + currentp = addDelayChain(currentp, range + 1U, flp, false, + m_isCoverSeq ? nullptr : rhsExprp); } return true; } @@ -687,14 +671,11 @@ class SvaNfaBuilder final { = result.finalCondp ? sampled(result.finalCondp->cloneTreePure(false)) : nullptr; SvaStateVertex* const successNowp = scopedCreateVertex(); guardedLink(srcp, successNowp, condp, flp); - SvaStateVertex* stagep = successNowp; - guardedLink(stagep, expiryMatchp, flp); - for (unsigned i = 0; i < info.range; ++i) { - SvaStateVertex* const nextp = scopedCreateVertex(); - guardedEdge(stagep, nextp, flp); - stagep = nextp; - guardedLink(stagep, expiryMatchp, flp); - } + // Retain a success through the latest deadline it can satisfy. + SvaStateVertex* const historyp + = addDelayChain(successNowp, info.range + 1U, flp, false); + guardedLink(successNowp, expiryMatchp, flp); + guardedLink(historyp, expiryMatchp, flp); } SvaStateVertex* const sinkVtxp = m_graph.createStateVertex(); @@ -715,6 +696,8 @@ class SvaNfaBuilder final { // Handle LHS (preExpr) SvaStateVertex* currentp = entryVtxp; if (AstNodeExpr* const preExprp = sexprp->preExprp()) { + VL_RESTORER(m_inSequencePrefix); + m_inSequencePrefix = true; const BuildResult pre = buildExpr(preExprp, currentp, isTopLevelStep); if (!pre.valid()) return BuildResult::fail(pre.errorEmitted); // LCOV_EXCL_LINE if (pre.finalCondp) { @@ -737,10 +720,9 @@ class SvaNfaBuilder final { RangeDelayRejectInfo rangeRejectInfo; const bool addRangeReject = isTopLevelStep && !m_inUnboundedScope; if (delayp->isRangeDelay()) { - bool errorEmitted = false; - if (!applyRangeDelay(delayp, sexprp->exprp(), currentp, rangeMidSources, flp, - errorEmitted, addRangeReject ? &rangeRejectInfo : nullptr)) { - return BuildResult::fail(errorEmitted); + if (!applyRangeDelay(sexprp, currentp, rangeMidSources, + addRangeReject ? &rangeRejectInfo : nullptr)) { + return BuildResult::failWithError(); } } else { const unsigned delayCycles = getConstUInt(delayp->lhsp()); @@ -3343,10 +3325,10 @@ class AssertNfaVisitor final : public VNVisitor { // Recursively walk a consequent. Returns cycle length consumed and // substitutes each VarRef to a captured local var with $past(rhs, K) // (or rhs inline when K == 0). Reports E_UNSUPPORTED on non-constant - // delays or composite sequence operators. - int walkSubstituteMatchItems(AstNodeExpr* nodep, unsigned K, - const std::unordered_map& matchItems, - bool& errorEmitted) { + // delays or composite sequence operators and returns -1 on failure. + int + walkSubstituteMatchItems(AstNodeExpr* nodep, unsigned K, + const std::unordered_map& matchItems) { if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) { // IEEE 1800-2023 16.9.2: cycle_delay's lhsp is a constant_expression // and the delay form in a sequence is always `##N`, folded by @@ -3359,25 +3341,23 @@ class AssertNfaVisitor final : public VNVisitor { sexprp->v3warn(E_UNSUPPORTED, "Unsupported: property local variable used across " "non-constant cycle delay in consequent" " (IEEE 1800-2023 16.10)"); - errorEmitted = true; return -1; } const unsigned delayCycles = VN_AS(delayp->lhsp(), Const)->toUInt(); int preLen = 0; if (AstNodeExpr* const prep = sexprp->preExprp()) { - preLen = walkSubstituteMatchItems(prep, K, matchItems, errorEmitted); - if (errorEmitted) return -1; + preLen = walkSubstituteMatchItems(prep, K, matchItems); + if (preLen < 0) return -1; } - const int bodyLen = walkSubstituteMatchItems(sexprp->exprp(), K + preLen + delayCycles, - matchItems, errorEmitted); - if (errorEmitted) return -1; + const int bodyLen + = walkSubstituteMatchItems(sexprp->exprp(), K + preLen + delayCycles, matchItems); + if (bodyLen < 0) return -1; return preLen + delayCycles + bodyLen; } if (nodep->isMultiCycleSva()) { nodep->v3warn(E_UNSUPPORTED, "Unsupported: property local variable used across " "composite sequence operator in consequent" " (IEEE 1800-2023 16.10)"); - errorEmitted = true; return -1; } std::vector refs; @@ -3409,12 +3389,11 @@ class AssertNfaVisitor final : public VNVisitor { matchItems[lhsRefp->varp()] = assignp->rhsp(); } const unsigned startK = parts.isOverlapped ? 0 : 1; - bool errorEmitted = false; - walkSubstituteMatchItems(seqBodyp, startK, matchItems, errorEmitted); + const int length = walkSubstituteMatchItems(seqBodyp, startK, matchItems); // Match-item substitution / strip mutates ancestor purity. Release // builds don't auto-clear caches on edits, so refresh here. VIsCached::clearCacheTree(); - if (errorEmitted) return true; + if (length < 0) return true; AstNodeExpr* const antBoolp = exprStmtp->resultp()->unlinkFrBack(); exprStmtp->replaceWith(antBoolp); VL_DO_DANGLING(pushDeletep(exprStmtp), exprStmtp); diff --git a/test_regress/t/t_cover_sequence_range.py b/test_regress/t/t_cover_sequence_range.py new file mode 100755 index 000000000..c85ecd230 --- /dev/null +++ b/test_regress/t/t_cover_sequence_range.py @@ -0,0 +1,23 @@ +#!/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.sim_time = 2500 +test.compile(timing_loop=True, + verilator_flags2=['--assert', '--coverage-user', '--timing', '--stats']) +test.execute() + +if test.vlt_all: + test.file_grep(test.stats, r'Assertions, NFA delay ring edge visits\s+(\d+)', 19) + test.inline_checks() + +test.passes() diff --git a/test_regress/t/t_cover_sequence_range.v b/test_regress/t/t_cover_sequence_range.v new file mode 100644 index 000000000..e7859a3f9 --- /dev/null +++ b/test_regress/t/t_cover_sequence_range.v @@ -0,0 +1,154 @@ +// DESCRIPTION: Verilator: Bounded cover sequence delay rings +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + int cyc = 0; + int hits_implicit = 0; + bit a = 0; + bit b = 0; + bit rst = 1; + bit [31:0] crc = 32'h5aef0c8d; + + cover sequence (@(posedge clk) ##[1:3] (cyc == 3)) hits_implicit++; + // CHECK_COVER(-1,"top.t","cover",3) + final `checkd(hits_implicit, 3); + + range_check #( + .LO(0), + .HI(257) + ) zero_min ( + .* + ); + range_check #( + .LO(1), + .HI(258) + ) one_min ( + .* + ); + range_check #( + .LO(3), + .HI(260) + ) fixed_prefix ( + .* + ); + range_check #( + .LO(1), + .HI(300) + ) reported ( + .* + ); + range_check #( + .LO(1), + .HI(3) + ) small_range ( + .* + ); + range_check #( + .LO(0), + .HI(1) + ) adjacent ( + .* + ); + range_check #( + .LO(3), + .HI(259) + ) boundary ( + .* + ); + + always @(negedge clk) begin + if (cyc == 1000) begin + $write("*-* All Finished *-*\n"); + $finish; + end + rst = (cyc == 500 || cyc == 501); + crc = {crc[30:0], crc[31] ^ crc[21] ^ crc[1] ^ crc[0]}; + // Isolated starts, full windows across wraps, draining, then varied traffic. + if (cyc < 330) begin + a = (cyc == 0 || cyc == 2); + b = 1; + end + else if (cyc < 650) begin + a = 1; + b = 1; + end + else if (cyc >= 730) begin + a = 0; + b = 1; + end + else begin + a = crc[0]; + b = crc[9]; + end + cyc++; + end +endmodule + +module range_check #( + parameter int LO = 1, + parameter int HI = 300 +) ( + input clk, + input a, + input b, + input rst +); + bit [HI:0] history = '0; + bit [HI:0] history_disabled = '0; + int hits = 0; + int hits_disabled = 0; + int expected = 0; + int expected_disabled = 0; + + cover sequence (@(posedge clk) a ##[LO:HI] b) hits++; + // CHECK_COVER(-1,"top.t.zero_min","cover",81961) + // CHECK_COVER(-2,"top.t.one_min","cover",81942) + // CHECK_COVER(-3,"top.t.fixed_prefix","cover",81892) + // CHECK_COVER(-4,"top.t.reported","cover",94982) + // CHECK_COVER(-5,"top.t.small_range","cover",1017) + // CHECK_COVER(-6,"top.t.adjacent","cover",673) + // CHECK_COVER(-7,"top.t.boundary","cover",81578) + cover sequence (@(posedge clk) disable iff (rst) a ##[LO:HI] b) hits_disabled++; + // CHECK_COVER(-1,"top.t.zero_min","cover",55021) + // CHECK_COVER(-2,"top.t.one_min","cover",54876) + // CHECK_COVER(-3,"top.t.fixed_prefix","cover",54577) + // CHECK_COVER(-4,"top.t.reported","cover",62540) + // CHECK_COVER(-5,"top.t.small_range","cover",1005) + // CHECK_COVER(-6,"top.t.adjacent","cover",668) + // CHECK_COVER(-7,"top.t.boundary","cover",54391) + + // Each bit represents a distinct start, including the current tick at bit zero. + always @(posedge clk) begin + history = {history[HI-1:0], a}; + if (b) expected += $countones(history[HI:LO]); + end + always @(posedge clk or posedge rst) begin + if (rst) history_disabled = '0; + else begin + history_disabled = {history_disabled[HI-1:0], a}; + if (b) expected_disabled += $countones(history_disabled[HI:LO]); + end + end + + // The action blocks have completed before the falling edge. + always @(negedge clk) begin + `checkd(hits, expected); + `checkd(hits_disabled, expected_disabled); + end + final begin + `checkd(hits, expected); + `checkd(hits_disabled, expected_disabled); + `checkd(hits > 0, 1'b1); + `checkd(hits_disabled > 0, 1'b1); + end +endmodule diff --git a/test_regress/t/t_cover_sequence_unsup.out b/test_regress/t/t_cover_sequence_unsup.out index 7850b7d99..5d038476e 100644 --- a/test_regress/t/t_cover_sequence_unsup.out +++ b/test_regress/t/t_cover_sequence_unsup.out @@ -10,12 +10,27 @@ 27 | cover sequence (a ##[1:2] (b ##1 c)); | ^~ %Warning-COVERIGN: t/t_cover_sequence_unsup.v:30:21: Ignoring unsupported: cover sequence with this ranged cycle delay - 30 | cover sequence (a ##[1:300] b); + 30 | cover sequence (a ##[1:300] (b ##1 c)); | ^~ -%Warning-COVERIGN: t/t_cover_sequence_unsup.v:33:21: Ignoring unsupported: cover sequence with a goto repetition - 33 | cover sequence (a [-> 2]); +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:31:22: Ignoring unsupported: cover sequence with this ranged cycle delay + 31 | cover sequence ((a ##[1:300] b) ##1 c); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:32:22: Ignoring unsupported: cover sequence with this ranged cycle delay + 32 | cover sequence ((a ##[1:2] b) ##1 c); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:33:21: Ignoring unsupported: cover sequence with this ranged cycle delay + 33 | cover sequence (a ##[1:2] b [*2]); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:36:21: Ignoring unsupported: cover sequence with a goto repetition + 36 | cover sequence (a [-> 2]); | ^~~ -%Warning-COVERIGN: t/t_cover_sequence_unsup.v:34:21: Ignoring unsupported: cover sequence with a goto repetition - 34 | cover sequence (a [-> 2: 3]); +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:37:21: Ignoring unsupported: cover sequence with a goto repetition + 37 | cover sequence (a [-> 2: 3]); | ^~~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:40:30: Ignoring unsupported: cover sequence with this ranged cycle delay + 40 | cover sequence ((a [*1:2]) ##[1:258] b); + | ^~ +%Warning-COVERIGN: t/t_cover_sequence_unsup.v:41:30: Ignoring unsupported: cover sequence with this ranged cycle delay + 41 | cover sequence ((a [*1:2]) ##[1:3] b); + | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_cover_sequence_unsup.v b/test_regress/t/t_cover_sequence_unsup.v index 660d0409b..78b9d8103 100644 --- a/test_regress/t/t_cover_sequence_unsup.v +++ b/test_regress/t/t_cover_sequence_unsup.v @@ -26,11 +26,18 @@ module t ( // Ranged cycle delay before a multi-cycle sequence. cover sequence (a ##[1:2] (b ##1 c)); - // Ranged cycle delay wide enough to use the counter FSM. - cover sequence (a ##[1:300] b); + // All range widths require a Boolean endpoint and cannot feed a sequence suffix. + cover sequence (a ##[1:300] (b ##1 c)); + cover sequence ((a ##[1:300] b) ##1 c); + cover sequence ((a ##[1:2] b) ##1 c); + cover sequence (a ##[1:2] b [*2]); // Goto repetition coalesces multiple live attempts into one NFA state. cover sequence (a [-> 2]); cover sequence (a [-> 2: 3]); + // Simultaneous prefix endpoints are not preserved by concatenation. + cover sequence ((a [*1:2]) ##[1:258] b); + cover sequence ((a [*1:2]) ##[1:3] b); + endmodule diff --git a/test_regress/t/t_property_delay_large.py b/test_regress/t/t_property_delay_large.py index 6e10d98d6..017c107a7 100755 --- a/test_regress/t/t_property_delay_large.py +++ b/test_regress/t/t_property_delay_large.py @@ -22,9 +22,9 @@ if test.vlt_all: test.file_grep(test.stats, r'Optimizations, Expand, expanded wide words\s+(\d+)', 0) test.file_grep(test.stats, r'Optimizations, Expand, expanded wides\s+(\d+)', 0) - # Keep the six wide rings bit-packed to avoid 32x storage. + # Keep the wide rings bit-packed to avoid 32x storage. test.file_grep(test.stats, - r'Optimizations, Expand, pattern assign to sel var wide one bit\s+(\d+)', 6) + r'Optimizations, Expand, pattern assign to sel var wide one bit\s+(\d+)', 8) test.execute() diff --git a/test_regress/t/t_property_local_var_range_unsup.v b/test_regress/t/t_property_local_var_range_unsup.v index 518693cb8..40ecc0fc2 100644 --- a/test_regress/t/t_property_local_var_range_unsup.v +++ b/test_regress/t/t_property_local_var_range_unsup.v @@ -32,9 +32,9 @@ module t ( endproperty assert property (p_composite); - // Nested range delay inside the consequent's preExprp -- the outer - // SExpr's recursion into preExprp errors, then the outer caller's - // `if (errorEmitted) return -1;` after preLen recursion is exercised. + // A nested range delay in the consequent's prefix is unsupported. + // Propagate its diagnostic through the enclosing concatenation + // without continuing substitution after the failure. property p_nested_in_pre; int snap; @(posedge clk) (valid, @@ -43,9 +43,9 @@ module t ( endproperty assert property (p_nested_in_pre); - // Nested range delay inside the consequent's exprp -- the outer - // SExpr's recursion into exprp errors, then the outer caller's - // `if (errorEmitted) return -1;` after bodyLen recursion is exercised. + // A nested range delay in the consequent's body is unsupported. + // Propagate its diagnostic through the enclosing concatenation + // without continuing substitution after the failure. property p_nested_in_body; int snap; @(posedge clk) (valid, diff --git a/test_regress/t/t_property_nfa_counts.py b/test_regress/t/t_property_nfa_counts.py index f2a6ec0fc..dfaf37edb 100755 --- a/test_regress/t/t_property_nfa_counts.py +++ b/test_regress/t/t_property_nfa_counts.py @@ -9,7 +9,7 @@ import vltest_bootstrap -test.scenarios('vlt_all') +test.scenarios('vlt') test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing', '--coverage-user']) diff --git a/test_regress/t/t_property_nfa_msgs_unsup.out b/test_regress/t/t_property_nfa_msgs_unsup.out index 5cdbf6675..9921212b9 100644 --- a/test_regress/t/t_property_nfa_msgs_unsup.out +++ b/test_regress/t/t_property_nfa_msgs_unsup.out @@ -33,11 +33,26 @@ %Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:60:37: Unsupported: ranged cycle delay in an operand of property 'and' 60 | assert property (@(posedge clk) c and (1'b1 ##[1:2] b)); | ^~~ -%Warning-COVERIGN: t/t_property_nfa_msgs_unsup.v:63:45: Ignoring unsupported: cover sequence with a sequence operand of 'or' - 63 | cover sequence (@(posedge clk) ((a and b) or(c ##1 d))); +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:61:54: Unsupported: ranged cycle delay in an operand of property 'and' + 61 | assert property (@(posedge clk) (1'b1 ##[1:300] b) and c); + | ^~~ +%Warning-COVERIGN: t/t_property_nfa_msgs_unsup.v:64:45: Ignoring unsupported: cover sequence with a sequence operand of 'or' + 64 | cover sequence (@(posedge clk) ((a and b) or(c ##1 d))); | ^~ ... For warning description see https://verilator.org/warn/COVERIGN?v=latest ... Use "/* verilator lint_off COVERIGN */" and lint_on around source to disable this message. +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:67:44: Unsupported: Bounded ranged cycle delay in a sequence prefix + 67 | assert property (@(posedge clk) a |-> (1 ##[1:3] b) ##1 c); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:68:42: Unsupported: Bounded ranged cycle delay in a sequence prefix + 68 | assert property (@(posedge clk) a |-> (##[0:1] b) ##1 c); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:69:44: Unsupported: Bounded ranged cycle delay in a sequence prefix + 69 | assert property (@(posedge clk) a |-> (1 ##[1:258] b) ##1 c); + | ^~ +%Error-UNSUPPORTED: t/t_property_nfa_msgs_unsup.v:71:13: Unsupported: Bounded ranged cycle delay in a sequence prefix + 71 | a |-> ##[1:2] (a | b | c | d | e) ##1 (a | b | c | d | e)); + | ^~ %Error: t/t_property_nfa_msgs_unsup.v:56:22: Concurrent assertion has no clock (IEEE 1800-2023 16.16) : ... note: In instance 't' : ... Suggest provide a clocking event, a default clocking, or a clocked procedural context diff --git a/test_regress/t/t_property_nfa_msgs_unsup.v b/test_regress/t/t_property_nfa_msgs_unsup.v index e8d7ad73a..7fd52f888 100644 --- a/test_regress/t/t_property_nfa_msgs_unsup.v +++ b/test_regress/t/t_property_nfa_msgs_unsup.v @@ -58,8 +58,16 @@ module t ( // An 'and' operand carrying mid-window sources defers to later passes assert property (@(posedge clk) (1'b1 ##[1:2] b) and c); assert property (@(posedge clk) c and (1'b1 ##[1:2] b)); + assert property (@(posedge clk) (1'b1 ##[1:300] b) and c); // A boolean 'and' operand of a rejected cover-sequence 'or' is freed cover sequence (@(posedge clk) ((a and b) or(c ##1 d))); + // Bounded range prefixes cannot propagate every candidate through a suffix. + assert property (@(posedge clk) a |-> (1 ##[1:3] b) ##1 c); + assert property (@(posedge clk) a |-> (##[0:1] b) ##1 c); + assert property (@(posedge clk) a |-> (1 ##[1:258] b) ##1 c); + assert property (@(posedge clk) + a |-> ##[1:2] (a | b | c | d | e) ##1 (a | b | c | d | e)); + endmodule diff --git a/test_regress/t/t_property_range_ring.py b/test_regress/t/t_property_range_ring.py new file mode 100755 index 000000000..09b1605d1 --- /dev/null +++ b/test_regress/t/t_property_range_ring.py @@ -0,0 +1,17 @@ +#!/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.sim_time = 1940 +test.compile(timing_loop=True, verilator_flags2=['--assert', '--timing']) +test.execute() +test.passes() diff --git a/test_regress/t/t_property_range_ring.v b/test_regress/t/t_property_range_ring.v new file mode 100644 index 000000000..e6f04f467 --- /dev/null +++ b/test_regress/t/t_property_range_ring.v @@ -0,0 +1,125 @@ +// DESCRIPTION: Verilator: Bounded property delay rings +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + int cyc = 0; + + range_check #( + .LO(0), + .HI(1) + ) adjacent ( + .* + ); + range_check #( + .LO(1), + .HI(3) + ) small_range ( + .* + ); + range_check #( + .LO(3), + .HI(259) + ) boundary ( + .* + ); + range_check #( + .LO(1), + .HI(258) + ) above_boundary ( + .* + ); + range_check #( + .LO(1), + .HI(300) + ) reported ( + .* + ); + + always @(negedge clk) begin + // The last start is sampled at 666, expires at 967, and drains at 968. + if (cyc == 968) begin + $write("*-* All Finished *-*\n"); + $finish; + end + cyc <= cyc + 1; + end +endmodule + +module range_check #( + parameter int LO = 1, + parameter int HI = 300 +) ( + input clk, + input int cyc +); + bit a = 0; + bit b = 0; + bit c = 0; + bit rst = 1; + bit previous_b = 0; + bit [HI:0] pending = '0; + bit [HI+1:0] pending_nested = '0; + int failures = 0; + int failures_nested = 0; + int expected = 0; + int expected_nested = 0; + + assert property (@(posedge clk) disable iff (rst) a |-> ##[LO:HI] b) + else failures++; + assert property (@(posedge clk) disable iff (rst) a |-> ##[LO:HI] (b ##1 c)) + else failures_nested++; + + // Retain each attempt until a match clears it or its last endpoint expires. + always @(posedge clk) begin + if (rst) begin + pending = '0; + pending_nested = '0; + previous_b = 0; + end + else begin + pending = {pending[HI-1:0], a}; + pending_nested = {pending_nested[HI:0], a}; + if (b) pending[HI:LO] = '0; + if (previous_b && c) pending_nested[HI+1:LO+1] = '0; + if (pending[HI]) expected++; + if (pending_nested[HI+1]) expected_nested++; + previous_b = b; + end + end + + always @(negedge clk) begin + `checkd(failures, expected); + `checkd(failures_nested, expected_nested); + rst = (cyc == 615); + // Early and last endpoints precede attempts that must expire without a match. + a = (cyc == 1 || cyc == 3 || cyc == HI + 3 || cyc == HI + 4 || (cyc >= 306 && cyc <= 321)); + b = (cyc == LO + 1 || cyc == HI + 1); + c = (cyc == HI + 2); + // Overlapping attempts and fresh matches exercise repeated ring wraps. + if (cyc >= 616 && cyc <= 665) begin + a = 1; + // Preserve the input pattern while moving the burst fifteen cycles earlier. + b = ((cyc + 15) % 13 == 0); + c = ((cyc + 15) % 7 == 0); + end + end + + final begin + `checkd(pending, '0); + `checkd(pending_nested, '0); + `checkd(failures, expected); + `checkd(failures_nested, expected_nested); + `checkd(failures > 0, 1'b1); + `checkd(failures_nested > 0, 1'b1); + end +endmodule diff --git a/test_regress/t/t_property_sexpr_range_delay.v b/test_regress/t/t_property_sexpr_range_delay.v index 929568fda..71c49e8df 100644 --- a/test_regress/t/t_property_sexpr_range_delay.v +++ b/test_regress/t/t_property_sexpr_range_delay.v @@ -79,10 +79,6 @@ module t ( assert property (@(posedge clk) disable iff (cyc < 2) a |-> ##[2:2] (a | b | c | d | e)); - // Multi-step: ##[1:2] then ##1 - assert property (@(posedge clk) disable iff (cyc < 2) - a |-> ##[1:2] (a | b | c | d | e) ##1 (a | b | c | d | e)); - // Large range ##[1:10000] (scalability, O(1) code size) assert property (@(posedge clk) disable iff (cyc < 2) a |-> ##[1:10000] (a | b | c | d | e));