From 944735fc05ac0f7eaa5494895a4e839433ee590e Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Wed, 17 Jun 2026 10:56:03 +0200 Subject: [PATCH] Support variable-length intersect in SVA sequences --- src/V3AssertNfa.cpp | 265 +++++++++++++++++- .../t/t_sequence_intersect_disjoint_bad.out | 6 + .../t/t_sequence_intersect_disjoint_bad.py | 18 ++ .../t/t_sequence_intersect_disjoint_bad.v | 18 ++ .../t/t_sequence_intersect_range_unsup.out | 28 +- .../t/t_sequence_intersect_range_unsup.v | 20 +- test_regress/t/t_sequence_intersect_varlen.py | 18 ++ test_regress/t/t_sequence_intersect_varlen.v | 62 ++++ 8 files changed, 407 insertions(+), 28 deletions(-) create mode 100644 test_regress/t/t_sequence_intersect_disjoint_bad.out create mode 100755 test_regress/t/t_sequence_intersect_disjoint_bad.py create mode 100644 test_regress/t/t_sequence_intersect_disjoint_bad.v create mode 100755 test_regress/t/t_sequence_intersect_varlen.py create mode 100644 test_regress/t/t_sequence_intersect_varlen.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 8db3e7761..6761b7608 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -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 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 @@ -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>& 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> 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. (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 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) { + 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(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. @@ -1010,18 +1254,21 @@ 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 != 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) { + 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 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_disjoint_bad.out b/test_regress/t/t_sequence_intersect_disjoint_bad.out new file mode 100644 index 000000000..c5a131724 --- /dev/null +++ b/test_regress/t/t_sequence_intersect_disjoint_bad.out @@ -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 diff --git a/test_regress/t/t_sequence_intersect_disjoint_bad.py b/test_regress/t/t_sequence_intersect_disjoint_bad.py new file mode 100755 index 000000000..f83bbb887 --- /dev/null +++ b/test_regress/t/t_sequence_intersect_disjoint_bad.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('linter') + +test.compile(verilator_flags2=['--assert --timing'], + fails=True, + expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_sequence_intersect_disjoint_bad.v b/test_regress/t/t_sequence_intersect_disjoint_bad.v new file mode 100644 index 000000000..321a592d5 --- /dev/null +++ b/test_regress/t/t_sequence_intersect_disjoint_bad.v @@ -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 diff --git a/test_regress/t/t_sequence_intersect_range_unsup.out b/test_regress/t/t_sequence_intersect_range_unsup.out index 3d71a9f29..d88521588 100644 --- a/test_regress/t/t_sequence_intersect_range_unsup.out +++ b/test_regress/t/t_sequence_intersect_range_unsup.out @@ -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) - : ... 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: 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..8d1445aa2 100644 --- a/test_regress/t/t_sequence_intersect_range_unsup.v +++ b/test_regress/t/t_sequence_intersect_range_unsup.v @@ -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 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..02f5fb0b6 --- /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 --debug-check']) + +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..5a091eccc --- /dev/null +++ b/test_regress/t/t_sequence_intersect_varlen.v @@ -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