From e4b6bac50abc7416c47270cc3d2eeec2049c534e Mon Sep 17 00:00:00 2001
From: Artur Bieniek <abieniek@antmicro.com>
Date: Tue, 4 Aug 2026 18:50:33 +0200
Subject: [PATCH] Fix mid-range consecutive repetition rejects (#8041)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
---
 src/V3AssertNfa.cpp                        |  5 ++---
 test_regress/t/t_assert_consec_rep.v       | 12 ++++++++++++
 test_regress/t/t_assert_consec_rep_large.v |  3 +--
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp
index ccbd6f74d..161643b52 100644
--- a/src/V3AssertNfa.cpp
+++ b/src/V3AssertNfa.cpp
@@ -783,12 +783,11 @@ class SvaNfaBuilder final {
                 guardedEdge(currentp, nextp, flp);
                 currentp = nextp;
             }
-            // Mark first and last boolean Links as rejectOnFail for correct
-            // reject on standalone ConsRep.
+            // Every repetition in the minimum prefix is required.
             SvaStateVertex* const condVtxp = scopedCreateVertex();
             SvaTransEdge* const linkp
                 = guardedLink(currentp, condVtxp, sampledRefOrClone(hoistVarp, exprp, flp), flp);
-            if (isTopLevelStep && (i == 0 || i == minN - 1)) { linkp->m_rejectOnFail = true; }
+            if (isTopLevelStep) linkp->m_rejectOnFail = true;
             currentp = condVtxp;
         }
         // After minN: currentp is the first valid end-of-match position for [*m:n].
diff --git a/test_regress/t/t_assert_consec_rep.v b/test_regress/t/t_assert_consec_rep.v
index 2daee40e8..30dac51d1 100644
--- a/test_regress/t/t_assert_consec_rep.v
+++ b/test_regress/t/t_assert_consec_rep.v
@@ -46,6 +46,8 @@ module t (
   int count_fail19 = 0;
   int count_fail20 = 0;
   int count_fail21 = 0;
+  int count_fail22 = 0;
+  int count_fail23 = 0;
 
   // Test 1: a[*3] |-> b
   assert property (@(posedge clk) a [* 3] |-> b)
@@ -126,6 +128,14 @@ module t (
   assert property (@(posedge clk) c |-> (a ##1 a [+]))
   else count_fail21 <= count_fail21 + 1;
 
+  // Test 22: Fail the middle required check of an exact repetition.
+  assert property (@(posedge clk) cyc == 1 |-> ##1 (cyc != 3) [*3])
+  else count_fail22 <= count_fail22 + 1;
+
+  // Test 23: A bounded range succeeds at its minimum, later repetitions are optional.
+  assert property (@(posedge clk) cyc == 1 |-> ##1 (cyc != 5) [*3:5])
+  else count_fail23 <= count_fail23 + 1;
+
   // Counter FSM with M>0: range > kChainLimit (256) forces counter vertex
   // creation; min>0 exercises the Gte/active gating path in resolveLinks and
   // emitNbaLogic. Cover-only so count_fail values above are undisturbed.
@@ -165,6 +175,8 @@ module t (
       `checkd(count_fail16, count_fail17);
       `checkd(count_fail18, count_fail19);
       `checkd(count_fail20, count_fail21);
+      `checkd(count_fail22, 1);
+      `checkd(count_fail23, 0);
       $write("*-* All Finished *-*\n");
       $finish;
     end
diff --git a/test_regress/t/t_assert_consec_rep_large.v b/test_regress/t/t_assert_consec_rep_large.v
index 4df36f7bc..27dcbd14c 100644
--- a/test_regress/t/t_assert_consec_rep_large.v
+++ b/test_regress/t/t_assert_consec_rep_large.v
@@ -40,8 +40,7 @@ module t (
     else if (cyc == 99) begin
       `checkh(crc, 64'hc77bb9b3784ea091);
       `checkd(count_fail_257, 0);
-      // Mismatch due to pre-existing ~26.5% NFA reject gap on |-> ##1 [*N]
-      `checkd(count_fail_513, 23);  // All other sims: 31
+      `checkd(count_fail_513, 31);
       $write("*-* All Finished *-*\n");
       $finish;
     end