address review and fix combiner over-acceptance

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<int, std::vector<AstNodeExpr*>> 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);

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)

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()
 

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

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

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()
 

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