Fix internal error on consecutive repetition with N > 256 (#7552) (#7603)

bin/verilator

@@ -357,6 +357,7 @@ detailed descriptions of these arguments.
     --no-aslr                   Disable address space layout randomization
     --no-assert                 Disable all assertions
     --no-assert-case            Disable unique/unique0/priority-case assertions
+    --assert-unroll-limit <iter> Max SVA assertion repetition before erroring
     --autoflush                 Flush streams after all $displays
     --bbox-sys                  Blackbox unknown $system calls
     --bbox-unsup                Blackbox unsupported language features

docs/guide/exe_verilator.rst

@@ -113,6 +113,15 @@ Summary:
    In versions before 5.038, these were disabled by default, and `--assert`
    or `--assert-case` was required to enable case assertions.
 
+.. option:: --assert-unroll-limit <iterations>
+
+   Rarely needed. Specifies the maximum repetition or range count Verilator
+   will unroll inside an SVA concurrent assertion (e.g. ``[*N]``, ``[->M:N]``,
+   ``always[lo:hi]``). Beyond this, the assertion is rejected with an error
+   so that pathological counts do not blow up compile time or memory.
+
+   Defaults to 1024. Increase if a design needs larger repetition counts.
+
 .. option:: --autoflush
 
    After every $display or $fdisplay, flush the output stream. This ensures

src/V3AssertNfa.cpp

@@ -313,6 +313,17 @@ class SvaNfaBuilder final {
         return sampled(exprp->cloneTreePure(false));
     }
 
+    // Reject concurrent assertions whose unrolled vertex count would exceed
+    // --assert-unroll-limit, so a pathological count cannot blow up compile time.
+    static bool exceedsAssertUnrollLimit(AstNode* nodep, int requested) {
+        const int limit = v3Global.opt.assertUnrollLimit();
+        if (requested <= limit) return false;
+        nodep->v3error("Concurrent assertion repetition count "
+                       << requested << " exceeds --assert-unroll-limit (" << limit
+                       << "); raise '--assert-unroll-limit' to compile");
+        return true;
+    }
+
     // Create vertex and inherit throughout guards from current scope (IEEE 16.9.9).
     SvaStateVertex* scopedCreateVertex() {
         SvaStateVertex* const vtxp = m_graph.createStateVertex();
@@ -494,15 +505,6 @@ class SvaNfaBuilder final {
         }
         const int minN = getConstInt(repp->countp());
         UASSERT_OBJ(minN >= 0, repp, "ConsRep count must be non-negative (V3Width invariant)");
-        // Exact-repetition ConsRep is currently unrolled into minN vertices, so
-        // we cap minN to keep compile size bounded. An unbounded or ranged rep
-        // has already been rewritten to a counter-FSM path elsewhere.
-        constexpr int kConsRepLimit = 256;
-        // LCOV_EXCL_START -- compile-size guard; exercised only with >256-rep inputs
-        if (minN > kConsRepLimit && !repp->unbounded() && !repp->maxCountp()) {
-            return BuildResult::fail();
-        }
-        // LCOV_EXCL_STOP
 
         // Sum sites across prefix + unbounded/range tail so one hoist covers
         // every check edge of this repetition.
@@ -512,6 +514,7 @@ class SvaNfaBuilder final {
         } else if (repp->maxCountp()) {
             totalSites += getConstInt(repp->maxCountp()) - minN;
         }
+        if (exceedsAssertUnrollLimit(repp, totalSites)) return BuildResult::failWithError();
         AstVar* const hoistVarp = tryHoistSampled(exprp, flp, totalSites);
 
         SvaStateVertex* currentp = entryVtxp;
@@ -577,6 +580,7 @@ class SvaNfaBuilder final {
         const int lo = getConstInt(nodep->loBoundp());
         const int hi = getConstInt(nodep->hiBoundp());
         UASSERT_OBJ(lo >= 0 && hi >= lo, nodep, "PropAlways bounds invariant (V3Width)");
+        if (exceedsAssertUnrollLimit(nodep, hi - lo + 1)) return BuildResult::failWithError();
         AstVar* const hoistVarp = tryHoistSampled(propp, flp, hi - lo + 1);
         SvaStateVertex* currentp = addDelayChain(entryVtxp, lo, flp);
         for (int k = 0; k <= hi - lo; ++k) {
@@ -602,6 +606,7 @@ class SvaNfaBuilder final {
         const bool hasMax = repp->maxCountp() != nullptr;
         const int maxN = hasMax ? getConstInt(repp->maxCountp()) : minN;
         UASSERT_OBJ(maxN >= minN, repp, "GotoRep range max < min (V3Width invariant)");
+        if (exceedsAssertUnrollLimit(repp, maxN)) return BuildResult::failWithError();
 
         // Wait + match per iter -> 2 sites per iteration; range form needs
         // sites for every iteration in [0..maxN). NOT($sampled(x)) matches

src/V3Options.cpp

@@ -1290,6 +1290,7 @@ void V3Options::parseOptsList(FileLine* fl, const string& optdir, int argc,
         m_assertCase = flag;
     });
     DECL_OPTION("-assert-case", OnOff, &m_assertCase);
+    DECL_OPTION("-assert-unroll-limit", Set, &m_assertUnrollLimit);
     DECL_OPTION("-autoflush", OnOff, &m_autoflush);
 
     DECL_OPTION("-bbox-sys", OnOff, &m_bboxSys);

src/V3Options.h

@@ -311,6 +311,7 @@ private:
     bool m_waiverMultiline = false;  // main switch: --waiver-multiline
     bool m_xInitialEdge = false;    // main switch: --x-initial-edge
 
+    int         m_assertUnrollLimit = 1024;  // main switch: --assert-unroll-limit
     int         m_buildJobs = -1;    // main switch: --build-jobs, -j
     int         m_coverageExprMax = 32;    // main switch: --coverage-expr-max
     int         m_convergeLimit = 10000;  // main switch: --converge-limit
@@ -606,6 +607,7 @@ public:
     bool serializeOnly() const { return m_jsonOnly; }
     bool topIfacesSupported() const { return lintOnly() && !hierarchical(); }
 
+    int assertUnrollLimit() const { return m_assertUnrollLimit; }
     int buildJobs() const VL_MT_SAFE { return m_buildJobs; }
     int convergeLimit() const { return m_convergeLimit; }
     int coverageExprMax() const { return m_coverageExprMax; }

test_regress/t/t_assert_consec_rep_large.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('vlt')
+
+test.compile(verilator_flags2=['--assert', '--timing'])
+
+test.execute()
+
+test.passes()

test_regress/t/t_assert_consec_rep_large.v

@@ -0,0 +1,48 @@
+// 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 stop $stop
+`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d:  got=%0x exp=%0x (%s !== %s)\n", `__FILE__,`__LINE__, (gotv), (expv), `"gotv`", `"expv`"); `stop; end while(0);
+`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
+);
+
+  int cyc;
+  reg [63:0] crc;
+
+  wire a = crc[0];
+  wire b = crc[4];
+  wire c = crc[8];
+
+  int count_fail_257 = 0;
+  int count_fail_513 = 0;
+
+  // All N > prior kConsRepLimit=256 (pre-fix: V3AssertNfa crash at codegen).
+  assert property (@(posedge clk) a [* 257] |-> b)
+  else count_fail_257 <= count_fail_257 + 1;
+
+  assert property (@(posedge clk) c |-> ##1 a [* 513])
+  else count_fail_513 <= count_fail_513 + 1;
+
+  always @(posedge clk) begin
+    cyc <= cyc + 1;
+    crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
+    if (cyc == 0) begin
+      crc <= 64'h5aef0c8d_d70a4497;
+    end else if (cyc == 99) begin
+      `checkh(crc, 64'hc77bb9b3784ea091);
+      `checkd(count_fail_257, 0);
+      // Questa: 31 -- pre-existing ~26.5% NFA reject gap on |-> ##1 [*N]
+      `checkd(count_fail_513, 23);
+      $write("*-* All Finished *-*\n");
+      $finish;
+    end
+  end
+endmodule

test_regress/t/t_assert_consec_rep_unroll_limit_bad.out

@@ -0,0 +1,6 @@
+%Error: t/t_assert_consec_rep_unroll_limit_bad.v:12:37: Concurrent assertion repetition count 25700000 exceeds --assert-unroll-limit (1024); raise '--assert-unroll-limit' to compile
+                                                      : ... note: In instance 't'
+   12 |   assert property (@(posedge clk) a [* 25700000] |-> b);
+      |                                     ^~
+        ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
+%Error: Exiting due to

test_regress/t/t_assert_consec_rep_unroll_limit_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.lint(fails=True,
+          verilator_flags2=['--assert-unroll-limit 1024'],
+          expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_assert_consec_rep_unroll_limit_bad.v

@@ -0,0 +1,14 @@
+// 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;
+
+  // Repetition count exceeds --assert-unroll-limit; pre-fix this hung the
+  // compiler, now an error names the limit so the user can raise it.
+  assert property (@(posedge clk) a [* 25700000] |-> b);
+
+endmodule