Support variable-length intersect in SVA sequences (#7835)
This commit is contained in:
Yilou Wang
GitHub
parent
0ebae43713
commit
000afcf52d
|
|
@ -384,6 +384,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
|
||||
|
|
@ -1028,6 +1096,188 @@ 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.
|
||||
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.
|
||||
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;
|
||||
}
|
||||
|
||||
// Empty common-length intersection -- unequal fixed lengths, or disjoint
|
||||
// ranged lengths. IEEE 1800-2023 16.9.6 requires both operands to match
|
||||
// over a window of the same length, so with no common length the intersect
|
||||
// simply never matches. This is legal (matching nothing), not an error, so
|
||||
// lower to a constant false rather than rejecting legal code.
|
||||
BuildResult buildNeverMatchIntersect(AstNodeExpr* nodep, SvaStateVertex* entryVtxp,
|
||||
bool isTopLevelStep) {
|
||||
AstNodeExpr* const falsep = new AstConst{nodep->fileline(), AstConst::BitFalse{}};
|
||||
return buildFromLoweringTree(falsep, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
|
||||
// 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) {
|
||||
// Disjoint length ranges share no common length -> never matches.
|
||||
return buildNeverMatchIntersect(nodep, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
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.
|
||||
|
|
@ -1232,18 +1482,26 @@ 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 start and end (equal length). Lower to a single sequence
|
||||
// that conjoins both operands' per-cycle checks -- correct under
|
||||
// concurrent attempts, where the done-latch combiner conflates the
|
||||
// two operands' start times and over-accepts. The combiner remains
|
||||
// only as a fallback for operands that do not flatten.
|
||||
const int lhsLen = fixedLength(intp->lhsp());
|
||||
const int rhsLen = fixedLength(intp->rhsp());
|
||||
if (lhsLen < 0 || rhsLen < 0) return BuildResult::fail();
|
||||
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)");
|
||||
return BuildResult::failWithError();
|
||||
if (lhsLen >= 0 && rhsLen >= 0) {
|
||||
if (lhsLen != rhsLen) {
|
||||
// Unequal fixed lengths share no common length -> never matches.
|
||||
return buildNeverMatchIntersect(intp, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
if (AstNodeExpr* const conjp
|
||||
= conjoinFixedSeqs(intp->lhsp(), intp->rhsp(), intp->fileline())) {
|
||||
return buildFromLoweringTree(conjp, entryVtxp, isTopLevelStep);
|
||||
}
|
||||
return buildAndCombiner(intp->lhsp(), intp->rhsp(), entryVtxp, intp->fileline());
|
||||
}
|
||||
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);
|
||||
|
|
|
|||
|
|
@ -79,6 +79,10 @@ module t (
|
|||
assert property (@(posedge clk)
|
||||
(1'b1 ##1 1'b1) intersect (1'b1 ##1 1'b1));
|
||||
|
||||
// Leading-delay operands (no offset-0 check): conjoin first offset > 0.
|
||||
assert property (@(posedge clk)
|
||||
(##2 1'b1) intersect (##2 1'b1));
|
||||
|
||||
// Intersect with `throughout` on one side: exercises fixedLength's
|
||||
// SThroughout branch (recurses into rhs to compute the length).
|
||||
cover property (@(posedge clk)
|
||||
|
|
|
|||
|
|
@ -1,10 +0,0 @@
|
|||
%Error: t/t_sequence_intersect_len_warn.v:16:17: Intersect sequence length mismatch: left 1 cycles, right 3 cycles (IEEE 1800-2023 16.9.6)
|
||||
: ... note: In instance 't'
|
||||
16 | (a ##1 b) intersect (c ##3 d));
|
||||
| ^~~~~~~~~
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
%Error: t/t_sequence_intersect_len_warn.v:20:17: Intersect sequence length mismatch: left 3 cycles, right 1 cycles (IEEE 1800-2023 16.9.6)
|
||||
: ... note: In instance 't'
|
||||
20 | (a ##3 b) intersect (c ##1 d));
|
||||
| ^~~~~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
@ -1,22 +0,0 @@
|
|||
// 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
|
||||
// verilog_lint: off
|
||||
// verilog_format: on
|
||||
|
||||
module t (input clk);
|
||||
logic a, b, c, d;
|
||||
|
||||
// LHS length 2, RHS length 4 -- WIDTHTRUNC (left < right)
|
||||
assert property (@(posedge clk)
|
||||
(a ##1 b) intersect (c ##3 d));
|
||||
|
||||
// LHS length 4, RHS length 2 -- WIDTHEXPAND (left > right)
|
||||
assert property (@(posedge clk)
|
||||
(a ##3 b) intersect (c ##1 d));
|
||||
|
||||
endmodule
|
||||
|
|
@ -9,10 +9,10 @@
|
|||
|
||||
import vltest_bootstrap
|
||||
|
||||
test.scenarios('vlt_all')
|
||||
test.scenarios('simulator')
|
||||
|
||||
test.compile(verilator_flags2=['--assert', '--timing', '--lint-only'],
|
||||
fails=True,
|
||||
expect_filename=test.golden_filename)
|
||||
test.compile(verilator_flags2=['--assert --timing'])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,57 @@
|
|||
// 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];
|
||||
|
||||
int f_fix = 0;
|
||||
int f_dis = 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
|
||||
|
||||
// An intersect whose operands share no common length compiles and never
|
||||
// matches (IEEE 1800-2023 16.9.6 requires a window of equal length). Each
|
||||
// form is the antecedent of `|-> 1'b0`: it stays vacuous while it never
|
||||
// matches, so the else fires once per match -- pinned to 0. A spurious match
|
||||
// would both fail the assertion and bump the counter.
|
||||
|
||||
// Unequal fixed lengths: {2} vs {3}.
|
||||
ap_fix :
|
||||
assert property (disable iff (cyc < 2) ((a ##2 b) intersect (c ##3 d)) |-> 1'b0)
|
||||
else f_fix <= f_fix + 1;
|
||||
|
||||
// Disjoint ranges: {1,2} vs {4,5}.
|
||||
ap_dis :
|
||||
assert property (disable iff (cyc < 2) ((a ##[1:2] b) intersect (c ##[4:5] d)) |-> 1'b0)
|
||||
else f_dis <= f_dis + 1;
|
||||
|
||||
final begin
|
||||
`checkd(f_fix, 0); // Questa: 0
|
||||
`checkd(f_dis, 0); // Questa: 0
|
||||
end
|
||||
endmodule
|
||||
|
|
@ -1,14 +1,18 @@
|
|||
%Error: t/t_sequence_intersect_range_unsup.v:12:10: Usage of cycle delays requires default clocking (IEEE 1800-2023 14.11)
|
||||
: ... 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)
|
||||
: ... 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()
|
||||
: ... 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.
|
||||
%Error-UNSUPPORTED: t/t_sequence_intersect_range_unsup.v:16:44: Unsupported: intersect with this variable-length operand
|
||||
: ... note: In instance 't'
|
||||
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'
|
||||
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'
|
||||
22 | assert property ((a ##[1:3] (b ##1 c)) intersect (d ##[2:4] e));
|
||||
| ^~~~~~~~~
|
||||
%Error-UNSUPPORTED: t/t_sequence_intersect_range_unsup.v:25:42: Unsupported: intersect of two sequences that each vary in length over a range with internal structure
|
||||
: ... note: In instance 't'
|
||||
25 | assert property ((a ##2 (b ##[1:3] c)) intersect (d ##[3:5] e));
|
||||
| ^~~~~~~~~
|
||||
%Error: Exiting due to
|
||||
|
|
|
|||
|
|
@ -4,11 +4,24 @@
|
|||
// 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));
|
||||
|
||||
// Operand top-level delay fixed but length varies via a nested range
|
||||
assert property ((a ##2 (b ##[1:3] c)) intersect (d ##[3:5] e));
|
||||
|
||||
endmodule
|
||||
|
|
|
|||
|
|
@ -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'])
|
||||
|
||||
test.execute()
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,71 @@
|
|||
// 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;
|
||||
int f_over = 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;
|
||||
|
||||
// Equal fixed length, one operand carrying an internal check: lowered through
|
||||
// the per-cycle conjoin, not the done-latch combiner (which conflates
|
||||
// concurrent attempts and over-accepts).
|
||||
ap_over :
|
||||
assert property (disable iff (cyc < 2) (a ##4 b) intersect (c ##2 d ##2 e))
|
||||
else f_over <= f_over + 1;
|
||||
|
||||
final begin
|
||||
`checkd(f_var, 7); // Questa: 7
|
||||
`checkd(f_ieee, 41); // Questa: 41
|
||||
`checkd(f_collapse, 0); // Questa: 0
|
||||
`checkd(f_over, 84); // Questa: 84
|
||||
end
|
||||
endmodule
|
||||
Loading…
Reference in New Issue