luke/verilator
1
0
Fork 0
mirror of https://github.com/verilator/verilator.git synced 2026-10-06 01:54:01 +02:00
Code Issues Packages Projects Releases Wiki Activity

Fix NFA rings for bounded SVA delays (#8371)

Browse Source 
Signed-off-by: Artur Bieniek <[email protected]>
This commit is contained in:
Artur Bieniek
2026-09-16 17:52:28 -04:00
committed by GitHub
parent 08cadc034d
commit e2caf971de
13 changed files with 433 additions and 94 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/V3AssertNfa.cpp
+51 -72
View File
@@ -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<SvaStateVertex*>& midSources, FileLine* flp,
bool& outErrorEmitted, RangeDelayRejectInfo* rangeRejectInfop = nullptr) {
// failure, emits a diagnostic and returns false.
bool applyRangeDelay(AstSExpr* sexprp, SvaStateVertex*& currentp,
std::vector<SvaStateVertex*>& 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<const AstVar*, AstNodeExpr*>& matchItems,
bool& errorEmitted) {
// delays or composite sequence operators and returns -1 on failure.
int
walkSubstituteMatchItems(AstNodeExpr* nodep, unsigned K,
const std::unordered_map<const AstVar*, AstNodeExpr*>& 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<AstVarRef*> 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);
test_regress/t/t_cover_sequence_range.py
Executable
+23
View File
@@ -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()
test_regress/t/t_cover_sequence_range.v
+154
View File
@@ -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
test_regress/t/t_cover_sequence_unsup.out
+20 -5
View File
@@ -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
test_regress/t/t_cover_sequence_unsup.v
+9 -2
View File
@@ -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
test_regress/t/t_property_delay_large.py
+2 -2
View File
@@ -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()
test_regress/t/t_property_local_var_range_unsup.v
+6 -6
View File
@@ -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,
test_regress/t/t_property_nfa_counts.py
+1 -1
View File
@@ -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'])
test_regress/t/t_property_nfa_msgs_unsup.out
+17 -2
View File
@@ -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
test_regress/t/t_property_nfa_msgs_unsup.v
+8
View File
@@ -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
test_regress/t/t_property_range_ring.py
Executable
+17
View File
@@ -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()
test_regress/t/t_property_range_ring.v
+125
View File
@@ -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
test_regress/t/t_property_sexpr_range_delay.v
-4
View File
@@ -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));