diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6fd12eee0..4a4ccf5bc 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -903,7 +903,7 @@ class SvaNfaBuilder final { // 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. + // 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; @@ -968,8 +968,7 @@ class SvaNfaBuilder final { // 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.) + // clones/hoists of every edge condition, so nothing else dangles. BuildResult buildFromLoweringTree(AstNodeExpr* treep, SvaStateVertex* entryVtxp, bool isTopLevelStep) { BuildResult result = buildExpr(treep, entryVtxp, isTopLevelStep); @@ -984,9 +983,7 @@ class SvaNfaBuilder final { // 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. Mirrors - // commercial simulators: compiles clean, the assertion never matches and a - // cover yields zero hits. + // 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{}}; @@ -1264,8 +1261,11 @@ public: } if (AstSIntersect* const intp = VN_CAST(nodep, SIntersect)) { // 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. + // 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) { @@ -1273,6 +1273,10 @@ public: // 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 buildVarLenIntersect(intp, 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_nevermatch.py b/test_regress/t/t_sequence_intersect_nevermatch.py index 02f5fb0b6..ddef50cab 100755 --- a/test_regress/t/t_sequence_intersect_nevermatch.py +++ b/test_regress/t/t_sequence_intersect_nevermatch.py @@ -11,7 +11,7 @@ import vltest_bootstrap test.scenarios('simulator') -test.compile(verilator_flags2=['--assert --timing --debug-check']) +test.compile(verilator_flags2=['--assert --timing']) test.execute() diff --git a/test_regress/t/t_sequence_intersect_range_unsup.out b/test_regress/t/t_sequence_intersect_range_unsup.out index d88521588..8788a6735 100644 --- a/test_regress/t/t_sequence_intersect_range_unsup.out +++ b/test_regress/t/t_sequence_intersect_range_unsup.out @@ -11,4 +11,8 @@ : ... 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 8d1445aa2..567496a47 100644 --- a/test_regress/t/t_sequence_intersect_range_unsup.v +++ b/test_regress/t/t_sequence_intersect_range_unsup.v @@ -21,4 +21,7 @@ module t ( // 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 index 02f5fb0b6..ddef50cab 100755 --- a/test_regress/t/t_sequence_intersect_varlen.py +++ b/test_regress/t/t_sequence_intersect_varlen.py @@ -11,7 +11,7 @@ import vltest_bootstrap test.scenarios('simulator') -test.compile(verilator_flags2=['--assert --timing --debug-check']) +test.compile(verilator_flags2=['--assert --timing']) test.execute() diff --git a/test_regress/t/t_sequence_intersect_varlen.v b/test_regress/t/t_sequence_intersect_varlen.v index 5a091eccc..402560af3 100644 --- a/test_regress/t/t_sequence_intersect_varlen.v +++ b/test_regress/t/t_sequence_intersect_varlen.v @@ -23,6 +23,7 @@ module t ( int f_var = 0; int f_ieee = 0; int f_collapse = 0; + int f_over = 0; always_ff @(posedge clk) begin cyc <= cyc + 1; @@ -54,9 +55,17 @@ module t ( 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