From 00c9e58006321cce847dba656058ec2c333e67ac Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Mon, 18 May 2026 09:54:10 +0800 Subject: [PATCH] Fix internal error on consecutive repetition with N > 256 (#7552) (#7603) --- bin/verilator | 1 + docs/guide/exe_verilator.rst | 9 ++++ src/V3AssertNfa.cpp | 23 +++++---- src/V3Options.cpp | 1 + src/V3Options.h | 2 + test_regress/t/t_assert_consec_rep_large.py | 18 +++++++ test_regress/t/t_assert_consec_rep_large.v | 48 +++++++++++++++++++ .../t_assert_consec_rep_unroll_limit_bad.out | 6 +++ .../t/t_assert_consec_rep_unroll_limit_bad.py | 18 +++++++ .../t/t_assert_consec_rep_unroll_limit_bad.v | 14 ++++++ 10 files changed, 131 insertions(+), 9 deletions(-) create mode 100755 test_regress/t/t_assert_consec_rep_large.py create mode 100644 test_regress/t/t_assert_consec_rep_large.v create mode 100644 test_regress/t/t_assert_consec_rep_unroll_limit_bad.out create mode 100755 test_regress/t/t_assert_consec_rep_unroll_limit_bad.py create mode 100644 test_regress/t/t_assert_consec_rep_unroll_limit_bad.v diff --git a/bin/verilator b/bin/verilator index c0a603bba..eeb7e8489 100755 --- a/bin/verilator +++ b/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 Max SVA assertion repetition before erroring --autoflush Flush streams after all $displays --bbox-sys Blackbox unknown $system calls --bbox-unsup Blackbox unsupported language features diff --git a/docs/guide/exe_verilator.rst b/docs/guide/exe_verilator.rst index 42964d2d1..cedc524bc 100644 --- a/docs/guide/exe_verilator.rst +++ b/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 + + 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 diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 98876d257..22bb39d75 100644 --- a/src/V3AssertNfa.cpp +++ b/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 diff --git a/src/V3Options.cpp b/src/V3Options.cpp index 4570e6db4..b6edabe24 100644 --- a/src/V3Options.cpp +++ b/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); diff --git a/src/V3Options.h b/src/V3Options.h index 127142f66..9b429d211 100644 --- a/src/V3Options.h +++ b/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; } diff --git a/test_regress/t/t_assert_consec_rep_large.py b/test_regress/t/t_assert_consec_rep_large.py new file mode 100755 index 000000000..23f04b54c --- /dev/null +++ b/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() diff --git a/test_regress/t/t_assert_consec_rep_large.v b/test_regress/t/t_assert_consec_rep_large.v new file mode 100644 index 000000000..4a0e332fc --- /dev/null +++ b/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 diff --git a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.out b/test_regress/t/t_assert_consec_rep_unroll_limit_bad.out new file mode 100644 index 000000000..3ac575c90 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.py b/test_regress/t/t_assert_consec_rep_unroll_limit_bad.py new file mode 100755 index 000000000..ba6d29aaf --- /dev/null +++ b/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() diff --git a/test_regress/t/t_assert_consec_rep_unroll_limit_bad.v b/test_regress/t/t_assert_consec_rep_unroll_limit_bad.v new file mode 100644 index 000000000..061e8b1ce --- /dev/null +++ b/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