diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index b6ec6964f..7949f8563 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -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 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 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 preRange{0, 0}; + if (AstNodeExpr* const prep = sexprp->preExprp()) { + preRange = lengthRange(prep); + if (preRange.first < 0) return {-1, -1}; + } + const std::pair 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(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>& 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> 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(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(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 lhsRange = lengthRange(nodep->lhsp()); + const std::pair 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(lo)}, + /*isCycle=*/true}; + delayp->rhsp(new AstConst{flp, static_cast(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); diff --git a/test_regress/t/t_sequence_intersect.v b/test_regress/t/t_sequence_intersect.v index 1e1b754b5..4e278a177 100644 --- a/test_regress/t/t_sequence_intersect.v +++ b/test_regress/t/t_sequence_intersect.v @@ -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) diff --git a/test_regress/t/t_sequence_intersect_len_warn.out b/test_regress/t/t_sequence_intersect_len_warn.out deleted file mode 100644 index f8239fae1..000000000 --- a/test_regress/t/t_sequence_intersect_len_warn.out +++ /dev/null @@ -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 diff --git a/test_regress/t/t_sequence_intersect_len_warn.v b/test_regress/t/t_sequence_intersect_len_warn.v deleted file mode 100644 index e544c8926..000000000 --- a/test_regress/t/t_sequence_intersect_len_warn.v +++ /dev/null @@ -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 diff --git a/test_regress/t/t_sequence_intersect_len_warn.py b/test_regress/t/t_sequence_intersect_nevermatch.py similarity index 71% rename from test_regress/t/t_sequence_intersect_len_warn.py rename to test_regress/t/t_sequence_intersect_nevermatch.py index 58fc7aeba..ddef50cab 100755 --- a/test_regress/t/t_sequence_intersect_len_warn.py +++ b/test_regress/t/t_sequence_intersect_nevermatch.py @@ -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() diff --git a/test_regress/t/t_sequence_intersect_nevermatch.v b/test_regress/t/t_sequence_intersect_nevermatch.v new file mode 100644 index 000000000..17887e184 --- /dev/null +++ b/test_regress/t/t_sequence_intersect_nevermatch.v @@ -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 diff --git a/test_regress/t/t_sequence_intersect_range_unsup.out b/test_regress/t/t_sequence_intersect_range_unsup.out index 3d71a9f29..8788a6735 100644 --- a/test_regress/t/t_sequence_intersect_range_unsup.out +++ b/test_regress/t/t_sequence_intersect_range_unsup.out @@ -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 diff --git a/test_regress/t/t_sequence_intersect_range_unsup.v b/test_regress/t/t_sequence_intersect_range_unsup.v index 837f9b146..567496a47 100644 --- a/test_regress/t/t_sequence_intersect_range_unsup.v +++ b/test_regress/t/t_sequence_intersect_range_unsup.v @@ -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 diff --git a/test_regress/t/t_sequence_intersect_varlen.py b/test_regress/t/t_sequence_intersect_varlen.py new file mode 100755 index 000000000..ddef50cab --- /dev/null +++ b/test_regress/t/t_sequence_intersect_varlen.py @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0. +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('simulator') + +test.compile(verilator_flags2=['--assert --timing']) + +test.execute() + +test.passes() diff --git a/test_regress/t/t_sequence_intersect_varlen.v b/test_regress/t/t_sequence_intersect_varlen.v new file mode 100644 index 000000000..402560af3 --- /dev/null +++ b/test_regress/t/t_sequence_intersect_varlen.v @@ -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