luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Support variable-length intersect in SVA sequences

This commit is contained in:
Yilou Wang 2026-06-17 10:56:03 +02:00
parent 969a775ae5
commit 944735fc05
8 changed files with 407 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

259
src/V3AssertNfa.cpp
View File

@ -290,6 +290,74 @@ class SvaNfaBuilder final {
return 0;
}
// Contiguous match-length range [lo,hi] for an operand whose length varies
// from AT MOST ONE ranged cycle delay; {-1,-1} otherwise. Drives the
// variable-length `intersect` lowering (IEEE 1800-2023 16.9.6): more than
// one ranged delay would make the per-length realization ambiguous, so it
// is reported unsupported rather than mis-paired.
static std::pair<int, int> lengthRange(AstNodeExpr* nodep) {
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay()) return {-1, -1};
std::pair<int, int> delayRange;
if (delayp->isRangeDelay()) {
if (delayp->isUnbounded()) return {-1, -1};
const int minD = getConstInt(delayp->lhsp());
const int maxD = getConstInt(delayp->rhsp());
if (minD < 0 || maxD < 0 || maxD < minD) return {-1, -1};
delayRange = {minD, maxD};
} else {
const int d = getConstInt(delayp->lhsp());
if (d < 0) return {-1, -1};
delayRange = {d, d};
}
std::pair<int, int> preRange{0, 0};
if (AstNodeExpr* const prep = sexprp->preExprp()) {
preRange = lengthRange(prep);
if (preRange.first < 0) return {-1, -1};
}
const std::pair<int, int> bodyRange = lengthRange(sexprp->exprp());
if (bodyRange.first < 0) return {-1, -1};
const int variableParts = (preRange.first != preRange.second)
+ (delayRange.first != delayRange.second)
+ (bodyRange.first != bodyRange.second);
if (variableParts > 1) return {-1, -1};
return {preRange.first + delayRange.first + bodyRange.first,
preRange.second + delayRange.second + bodyRange.second};
}
if (AstSThroughout* const throughp = VN_CAST(nodep, SThroughout)) {
return lengthRange(throughp->rhsp());
}
if (nodep->isMultiCycleSva()) return {-1, -1};
return {0, 0}; // plain boolean -- 0 cycles
}
// Clone `operand` with its sole variable ranged cycle delay pinned so the
// total match length is exactly `len`. `lo` is the operand's minimum length
// (lengthRange().first). A fixed operand has no such delay and is returned
// as a plain clone (callers only request its single achievable length).
static AstNodeExpr* realizeAtLength(AstNodeExpr* operand, int len, int lo) {
AstNodeExpr* const clonep = operand->cloneTreePure(false);
AstDelay* rangeDelayp = nullptr;
clonep->foreach([&](AstDelay* dp) {
if (!rangeDelayp && dp->isRangeDelay() && !dp->isUnbounded()
&& getConstInt(dp->lhsp()) != getConstInt(dp->rhsp())) {
rangeDelayp = dp;
}
});
if (rangeDelayp) {
FileLine* const flp = rangeDelayp->fileline();
const int pinned = getConstInt(rangeDelayp->lhsp()) + (len - lo);
AstNodeExpr* const oldMinp = rangeDelayp->lhsp();
oldMinp->replaceWith(new AstConst{flp, static_cast<uint32_t>(pinned)});
VL_DO_DANGLING(oldMinp->deleteTree(), oldMinp);
// Drop the max bound so it lowers as a fixed `##d`, not `##[d:d]`.
AstNode* const oldMaxp = rangeDelayp->rhsp()->unlinkFrBack();
VL_DO_DANGLING(oldMaxp->deleteTree(), oldMaxp);
}
return clonep;
}
// Cuts AST size from O(N * sizeof(exprp)) to O(N) + O(sizeof(exprp)) by
// sharing a single `VarRef` across N check edges. Hoist also matches the
// IEEE 1800-2023 16.9.9 "single preponed-region snapshot" semantic for
@ -808,6 +876,182 @@ class SvaNfaBuilder final {
return result;
}
// Collect the boolean leaf checks of a fixed-length sequence keyed by their
// clock offset from the start. Returns false for anything other than nested
// AstSExpr with fixed cycle delays over boolean leaves (e.g. throughout).
static bool flattenFixedSeq(AstNodeExpr* nodep, int baseOffset,
std::map<int, std::vector<AstNodeExpr*>>& out) {
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay() || delayp->isUnbounded()) return false;
const int delayCycles = getConstInt(delayp->lhsp());
if (delayCycles < 0) return false;
if (delayp->isRangeDelay() && getConstInt(delayp->rhsp()) != delayCycles) return false;
int preLen = 0;
if (AstNodeExpr* const prep = sexprp->preExprp()) {
if (!flattenFixedSeq(prep, baseOffset, out)) return false;
preLen = fixedLength(prep);
if (preLen < 0) return false;
}
return flattenFixedSeq(sexprp->exprp(), baseOffset + preLen + delayCycles, out);
}
if (nodep->isMultiCycleSva()) return false;
out[baseOffset].push_back(nodep);
return true;
}
// Conjoin two equal-length fixed sequences into one: at each clock offset
// AND the boolean checks of both operands (IEEE 1800-2023 16.9.6 -- both
// operands match the same window). Returns null if either operand is not a
// plain fixed sequence of boolean leaves. Caller owns the returned tree.
static AstNodeExpr* conjoinFixedSeqs(AstNodeExpr* lhsp, AstNodeExpr* rhsp, FileLine* flp) {
std::map<int, std::vector<AstNodeExpr*>> checks;
if (!flattenFixedSeq(lhsp, 0, checks) || !flattenFixedSeq(rhsp, 0, checks)) return nullptr;
if (checks.empty()) return nullptr;
AstNodeExpr* resultp = nullptr;
int prevOffset = 0;
for (const auto& offsetChecks : checks) {
const int offset = offsetChecks.first;
AstNodeExpr* condp = nullptr;
for (AstNodeExpr* const leafp : offsetChecks.second) {
AstNodeExpr* const clonep = leafp->cloneTreePure(false);
if (!condp) {
condp = clonep;
} else {
condp = new AstLogAnd{flp, condp, clonep};
condp->dtypeSetBit();
}
}
if (!resultp) {
if (offset > 0) {
AstDelay* const delayp = new AstDelay{
flp, new AstConst{flp, static_cast<uint32_t>(offset)}, /*isCycle=*/true};
resultp
= new AstSExpr{flp, new AstConst{flp, AstConst::BitTrue{}}, delayp, condp};
resultp->dtypeSetBit();
} else {
resultp = condp;
}
} else {
AstDelay* const delayp = new AstDelay{
flp, new AstConst{flp, static_cast<uint32_t>(offset - prevOffset)},
/*isCycle=*/true};
resultp = new AstSExpr{flp, resultp, delayp, condp};
resultp->dtypeSetBit();
}
prevOffset = offset;
}
return resultp;
}
// `seq` is a simple ranged sequence `start ##[m:n] end` (start/end boolean,
// start may be absent). Used to collapse a both-variable intersect to one
// ranged delay.
struct SimpleRanged final {
bool ok = false;
AstNodeExpr* startp = nullptr; // may be null (absent start)
AstNodeExpr* endp = nullptr;
};
static SimpleRanged asSimpleRanged(AstNodeExpr* nodep) {
AstSExpr* const sexprp = VN_CAST(nodep, SExpr);
if (!sexprp) return {};
AstDelay* const delayp = VN_CAST(sexprp->delayp(), Delay);
if (!delayp || !delayp->isCycleDelay() || !delayp->isRangeDelay() || delayp->isUnbounded())
return {};
if (getConstInt(delayp->lhsp()) == getConstInt(delayp->rhsp())) return {};
AstNodeExpr* const prep = sexprp->preExprp();
if (prep && fixedLength(prep) != 0) return {};
if (fixedLength(sexprp->exprp()) != 0) return {};
return {true, prep, sexprp->exprp()};
}
// Build the NFA for a synthesized intersect lowering tree, then free it.
// buildExpr returns the terminal condition (finalCondp) by reference into the
// tree; detach a clone so the tree can be freed here. The graph already holds
// clones/hoists of every edge condition, so nothing else dangles. (A shared
// tree freed later would double-free at the parent-less-finalCondp sites.)
BuildResult buildFromLoweringTree(AstNodeExpr* treep, SvaStateVertex* entryVtxp,
bool isTopLevelStep) {
BuildResult result = buildExpr(treep, entryVtxp, isTopLevelStep);
if (result.valid() && result.finalCondp) {
result.finalCondp = result.finalCondp->cloneTreePure(false);
}
VL_DO_DANGLING(treep->deleteTree(), treep);
return result;
}
// Lower `seq1 intersect seq2` when an operand's match length varies
// (IEEE 1800-2023 16.9.6: both match over one window, equal start and end).
// The common length range is [lo,hi] = intersection of the two operands'
// achievable lengths. The equal-length combiner is avoided -- it mis-handles
// operands with an internal boolean check -- by lowering to plain sequences:
// - lo == hi (one shared length, e.g. one fixed + one ranged operand):
// pin each operand to that length and conjoin them cycle-by-cycle into a
// single fixed sequence.
// - lo < hi with simple `bool ##[m:n] bool` operands: collapse to one
// ranged delay `(start1 & start2) ##[lo:hi] (end1 & end2)`. (An OR of
// per-length branches cannot reject correctly -- a single missed length
// would fail the whole intersect, cf. Lesson 48.)
// - otherwise unsupported (clean error, not the legacy fall-through crash).
BuildResult buildVarLenIntersect(AstSIntersect* nodep, SvaStateVertex* entryVtxp,
bool isTopLevelStep) {
const std::pair<int, int> lhsRange = lengthRange(nodep->lhsp());
const std::pair<int, int> rhsRange = lengthRange(nodep->rhsp());
if (lhsRange.first < 0 || rhsRange.first < 0) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: intersect with this variable-length operand");
return BuildResult::failWithError();
}
const int lo = std::max(lhsRange.first, rhsRange.first);
const int hi = std::min(lhsRange.second, rhsRange.second);
if (lo > hi) {
nodep->v3error("Intersect sequence lengths share no common value: left "
+ std::to_string(lhsRange.first) + ".."
+ std::to_string(lhsRange.second) + " cycles, right "
+ std::to_string(rhsRange.first) + ".."
+ std::to_string(rhsRange.second) + " cycles (IEEE 1800-2023 16.9.6)");
return BuildResult::failWithError();
}
FileLine* const flp = nodep->fileline();
if (lo == hi) {
AstNodeExpr* const lp = realizeAtLength(nodep->lhsp(), lo, lhsRange.first);
AstNodeExpr* const rp = realizeAtLength(nodep->rhsp(), lo, rhsRange.first);
AstNodeExpr* const conjp = conjoinFixedSeqs(lp, rp, flp);
VL_DO_DANGLING(lp->deleteTree(), lp);
VL_DO_DANGLING(rp->deleteTree(), rp);
if (!conjp) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: intersect operand is not a plain boolean sequence");
return BuildResult::failWithError();
}
return buildFromLoweringTree(conjp, entryVtxp, isTopLevelStep);
}
const SimpleRanged sl = asSimpleRanged(nodep->lhsp());
const SimpleRanged sr = asSimpleRanged(nodep->rhsp());
if (!sl.ok || !sr.ok) {
nodep->v3warn(E_UNSUPPORTED,
"Unsupported: intersect of two sequences that each vary in length over a"
" range with internal structure");
return BuildResult::failWithError();
}
const auto andBool = [&](AstNodeExpr* ap, AstNodeExpr* bp) -> AstNodeExpr* {
AstNodeExpr* const aClonep
= ap ? ap->cloneTreePure(false) : new AstConst{flp, AstConst::BitTrue{}};
AstNodeExpr* const bClonep
= bp ? bp->cloneTreePure(false) : new AstConst{flp, AstConst::BitTrue{}};
AstLogAnd* const andp = new AstLogAnd{flp, aClonep, bClonep};
andp->dtypeSetBit();
return andp;
};
AstDelay* const delayp = new AstDelay{flp, new AstConst{flp, static_cast<uint32_t>(lo)},
/*isCycle=*/true};
delayp->rhsp(new AstConst{flp, static_cast<uint32_t>(hi)});
AstSExpr* const reducedp
= new AstSExpr{flp, andBool(sl.startp, sr.startp), delayp, andBool(sl.endp, sr.endp)};
reducedp->dtypeSetBit();
return buildFromLoweringTree(reducedp, entryVtxp, isTopLevelStep);
}
BuildResult buildThroughout(AstSThroughout* nodep, SvaStateVertex* entryVtxp,
bool isTopLevelStep = false) {
// Mark entryVtxp so "cond false at tick 0" is detected as throughout-drop.
@ -1010,19 +1254,22 @@ public:
return buildAndCombiner(andp->lhsp(), andp->rhsp(), entryVtxp, andp->fileline());
}
if (AstSIntersect* const intp = VN_CAST(nodep, SIntersect)) {
// IEEE 1800-2023 16.9.6: SAnd with equal-length constraint.
// Variable-length intersect deferred to follow-up.
// IEEE 1800-2023 16.9.6: both operands match over one window with
// equal length. Equal fixed length is a single AND-combiner; a
// varying length (ranged cycle delay) pairs each common length.
const int lhsLen = fixedLength(intp->lhsp());
const int rhsLen = fixedLength(intp->rhsp());
if (lhsLen < 0 || rhsLen < 0) return BuildResult::fail();
if (lhsLen >= 0 && rhsLen >= 0) {
if (lhsLen != rhsLen) {
intp->v3error("Intersect sequence length mismatch: left " + std::to_string(lhsLen)
+ " cycles, right " + std::to_string(rhsLen)
+ " cycles (IEEE 1800-2023 16.9.6)");
intp->v3error("Intersect sequence length mismatch: left "
+ std::to_string(lhsLen) + " cycles, right "
+ std::to_string(rhsLen) + " cycles (IEEE 1800-2023 16.9.6)");
return BuildResult::failWithError();
}
return buildAndCombiner(intp->lhsp(), intp->rhsp(), entryVtxp, intp->fileline());
}
return buildVarLenIntersect(intp, entryVtxp, isTopLevelStep);
}
if (AstSWithin* const withinp = VN_CAST(nodep, SWithin)) {
return buildSWithin(withinp, entryVtxp, isTopLevelStep);
}

6
test_regress/t/t_sequence_intersect_disjoint_bad.out Normal file
View File

@ -0,0 +1,6 @@
%Error: t/t_sequence_intersect_disjoint_bad.v:16:34: Intersect sequence lengths share no common value: left 1..2 cycles, right 4..5 cycles (IEEE 1800-2023 16.9.6)
: ... note: In instance 't'
16 | assert property ((a ##[1:2] b) intersect (c ##[4:5] d));
| ^~~~~~~~~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: Exiting due to

18
test_regress/t/t_sequence_intersect_disjoint_bad.py Executable file
View File

@ -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('linter')
test.compile(verilator_flags2=['--assert --timing'],
fails=True,
expect_filename=test.golden_filename)
test.passes()

18
test_regress/t/t_sequence_intersect_disjoint_bad.v Normal file
View File

@ -0,0 +1,18 @@
// DESCRIPTION: Verilator: Verilog Test module
//
// This file ONLY is placed under the Creative Commons Public Domain.
// SPDX-FileCopyrightText: 2026 PlanV GmbH
// SPDX-License-Identifier: CC0-1.0
module t (
input clk
);
logic a, b, c, d;
default clocking @(posedge clk);
endclocking
// LHS length in [1,2], RHS in [4,5]: no common length, can never match
assert property ((a ##[1:2] b) intersect (c ##[4:5] d));
endmodule

22
test_regress/t/t_sequence_intersect_range_unsup.out
View File

@ -1,14 +1,14 @@
%Error: t/t_sequence_intersect_range_unsup.v:12:10: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11)
%Error-UNSUPPORTED: t/t_sequence_intersect_range_unsup.v:16:44: Unsupported: intersect with this variable-length operand
: ... note: In instance 't'
12 | (a ##[1:5] b) intersect (c ##2 d));
| ^~
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
%Error: t/t_sequence_intersect_range_unsup.v:12:34: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11)
16 | assert property ((a ##[1:3] b ##[1:2] c) intersect (d ##2 e));
| ^~~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_intersect_range_unsup.v:19:45: Unsupported: intersect operand is not a plain boolean sequence
: ... note: In instance 't'
12 | (a ##[1:5] b) intersect (c ##2 d));
| ^~
%Error: Internal Error: t/t_sequence_intersect_range_unsup.v:12:10: ../V3Ast.cpp:#: AstSExpr must have non-nullptr delayp()
19 | assert property ((a throughout (b ##1 c)) intersect (d ##[0:2] e));
| ^~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_intersect_range_unsup.v:22:42: Unsupported: intersect of two sequences that each vary in length over a range with internal structure
: ... note: In instance 't'
12 | (a ##[1:5] b) intersect (c ##2 d));
| ^~
... This fatal error may be caused by the earlier error(s); resolve those first.
22 | assert property ((a ##[1:3] (b ##1 c)) intersect (d ##[2:4] e));
| ^~~~~~~~~
%Error: Exiting due to

20
test_regress/t/t_sequence_intersect_range_unsup.v
View File

@ -4,11 +4,21 @@
// SPDX-FileCopyrightText: 2026 PlanV GmbH
// SPDX-License-Identifier: CC0-1.0
module t (input clk);
logic a, b, c, d;
module t (
input clk
);
logic a, b, c, d, e;
// Range delay in intersect operand is unsupported
assert property (@(posedge clk)
(a ##[1:5] b) intersect (c ##2 d));
default clocking @(posedge clk);
endclocking
// Two ranged cycle delays in one intersect operand is unsupported
assert property ((a ##[1:3] b ##[1:2] c) intersect (d ##2 e));
// Single common length, but an operand is not a plain boolean sequence
assert property ((a throughout (b ##1 c)) intersect (d ##[0:2] e));
// Both operands vary over a range and carry internal structure
assert property ((a ##[1:3] (b ##1 c)) intersect (d ##[2:4] e));
endmodule

18
test_regress/t/t_sequence_intersect_varlen.py Executable file
View File

@ -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(verilator_flags2=['--assert --timing --debug-check'])
test.execute()
test.passes()

62
test_regress/t/t_sequence_intersect_varlen.v Normal file
View File

@ -0,0 +1,62 @@
// 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 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
);
integer cyc = 0;
reg [63:0] crc = 64'h5aef0c8d_d70a4497;
wire a = crc[0];
wire b = crc[1];
wire c = crc[2];
wire d = crc[3];
wire e = crc[4];
int f_var = 0;
int f_ieee = 0;
int f_collapse = 0;
always_ff @(posedge clk) begin
cyc <= cyc + 1;
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
if (cyc == 99) begin
$write("*-* All Finished *-*\n");
$finish;
end
end
default clocking @(posedge clk);
endclocking
// Both operands vary in length: lhs in [1,3], rhs in [2,5], common [2,3].
// Variable-length intersect (IEEE 1800-2023 16.9.6): both match the same
// window with equal start and end, length chosen from each operand's range.
ap_var :
assert property (disable iff (cyc < 2) (a & c) |-> ((a ##[1:3] b) intersect (c ##[2:5] d)))
else f_var <= f_var + 1;
// IEEE 16.9.6 canonical: one variable + one fixed operand, common length {4}.
ap_ieee :
assert property (disable iff (cyc < 2) a |-> ((a ##[1:5] b) intersect (c ##2 d ##2 e)))
else f_ieee <= f_ieee + 1;
// Common length collapses to {0}: (a ##[0:3] b) intersect c == a & b & c,
// so this implication never fails (exercises the bare-boolean lowering path).
ap_collapse :
assert property (disable iff (cyc < 2) (a & b & c) |-> ((a ##[0:3] b) intersect c))
else f_collapse <= f_collapse + 1;
final begin
`checkd(f_var, 7); // Questa: 7
`checkd(f_ieee, 41); // Questa: 41
`checkd(f_collapse, 0); // Questa: 0
end
endmodule