From 33ad9d530edfc69154dfeaefcf2de69210951b7d Mon Sep 17 00:00:00 2001 From: Artur Bieniek Date: Mon, 24 Aug 2026 14:57:18 +0200 Subject: [PATCH] Fix V3Width SVA bound limit guard, leave headroom for alignment, respect --max-num-width (#8192) Signed-off-by: Artur Bieniek --- docs/guide/exe_verilator.rst | 2 + src/V3Width.cpp | 30 +++++++++--- test_regress/t/t_past_bad.out | 13 +++++ test_regress/t/t_past_bad.py | 4 +- test_regress/t/t_past_bad.v | 3 ++ test_regress/t/t_prop_always_bad.out | 13 +++++ test_regress/t/t_prop_always_bad.py | 4 +- test_regress/t/t_prop_always_bad.v | 7 +++ test_regress/t/t_property_sexpr2_bad.out | 2 +- .../t/t_property_sexpr_range_delay_bad.out | 28 ++++++++++- .../t/t_property_sexpr_range_delay_bad.py | 7 +-- .../t/t_property_sexpr_range_delay_bad.v | 9 ++++ test_regress/t/t_sva_max_bound.py | 16 +++++++ test_regress/t/t_sva_max_bound.v | 47 +++++++++++++++++++ 14 files changed, 170 insertions(+), 15 deletions(-) create mode 100755 test_regress/t/t_sva_max_bound.py create mode 100644 test_regress/t/t_sva_max_bound.v diff --git a/docs/guide/exe_verilator.rst b/docs/guide/exe_verilator.rst index 94c7d1a17..4c1fa91b9 100644 --- a/docs/guide/exe_verilator.rst +++ b/docs/guide/exe_verilator.rst @@ -1223,6 +1223,8 @@ Summary: .. option:: --max-num-width Set the maximum number literal width (e.g., in 1024'd22 the 1024). + This also limits SVA cycle delay and temporal bound values. + Defaults to 64K. .. option:: --Mdir diff --git a/src/V3Width.cpp b/src/V3Width.cpp index ee9a48ef4..cdafc6d61 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -744,6 +744,22 @@ class WidthVisitor final : public VNVisitor { // it's like an if() condition. iterateCheckBool(nodep, "default disable iff condition", nodep->condp(), BOTH); } + static bool widthCheckSvaValueLimit(AstNode* nodep, const AstConst* constp, const char* what) { + // Temporal values can materialize as O(N) AST or state in later passes. + // Leave headroom for a range ring's extra slot and V3Number's signed + // `(bits + 31) / 32` word count. + static constexpr unsigned SVA_VALUE_HARD_LIMIT + = static_cast(std::numeric_limits::max()) - 32U; + const unsigned configuredLimit = static_cast(v3Global.opt.maxNumWidth()); + const unsigned limit = std::min(configuredLimit, SVA_VALUE_HARD_LIMIT); + if (constp->num().fitsInUInt() && constp->toUInt() <= limit) return true; + nodep->v3warn(E_UNSUPPORTED, "Unsupported: " << what << " exceeds implementation limit of " + << limit + << (configuredLimit <= SVA_VALUE_HARD_LIMIT + ? " (--max-num-width)" + : " (host arithmetic limit)")); + return false; + } static const AstConst* widthCheckSvaDelayBound(AstDelay* nodep, AstNodeExpr* boundp, const char* what) { const AstConst* const constp = VN_CAST(boundp, Const); @@ -752,12 +768,7 @@ class WidthVisitor final : public VNVisitor { " (IEEE 1800-2023 16.7)"); return nullptr; } - if (constp->num().mostSetBitP1() > 31) { - nodep->v3warn( - E_UNSUPPORTED, - "Unsupported: SVA cycle delay exceeds implementation limit of 2147483647"); - return nullptr; - } + if (!widthCheckSvaValueLimit(nodep, constp, "SVA cycle delay")) return nullptr; return constp; } void visit(AstDelay* nodep) override { @@ -1577,7 +1588,7 @@ class WidthVisitor final : public VNVisitor { } else if (constp->toSInt() < 1) { constp->v3error("$past tick value must be >= 1 (IEEE 1800-2023 16.9.3)"); nodep->ticksp()->unlinkFrBack()->deleteTree(); - } else { + } else if (widthCheckSvaValueLimit(nodep, constp, "$past tick value")) { if (constp->toSInt() > 10) { constp->v3warn(TICKCOUNT, "$past tick value of " << constp->toSInt() @@ -1668,6 +1679,11 @@ class WidthVisitor final : public VNVisitor { if (loConstp && loConstp->toSInt() < 0) { nodep->loBoundp()->v3error("always range low bound must be non-negative" " (IEEE 1800-2023 16.12.11)"); + } else if (loConstp) { + widthCheckSvaValueLimit(nodep->loBoundp(), loConstp, "always range bound"); + } + if (!hiUnbounded && hiConstp) { + widthCheckSvaValueLimit(nodep->hiBoundp(), hiConstp, "always range bound"); } if (!hiUnbounded && loConstp && hiConstp && hiConstp->toSInt() < loConstp->toSInt()) { nodep->hiBoundp()->v3error("always range high bound must be >= low bound" diff --git a/test_regress/t/t_past_bad.out b/test_regress/t/t_past_bad.out index 9fe6ddcaa..712b4125c 100644 --- a/test_regress/t/t_past_bad.out +++ b/test_regress/t/t_past_bad.out @@ -17,4 +17,17 @@ | ^~~~~ ... For warning description see https://verilator.org/warn/TICKCOUNT?v=latest ... Use "/* verilator lint_off TICKCOUNT */" and lint_on around source to disable this message. +%Error-UNSUPPORTED: t/t_past_bad.v:19:9: Unsupported: $past tick value exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 19 | if ($past(d, 32'h7fffffff)) $stop; + | ^~~~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_past_bad.v:20:9: Unsupported: $past tick value exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 20 | if ($past(d, 32'h7ffffffe)) $stop; + | ^~~~~ +%Error-UNSUPPORTED: t/t_past_bad.v:21:9: Unsupported: $past tick value exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 21 | if ($past(d, 32'h7ffffffc)) $stop; + | ^~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_past_bad.py b/test_regress/t/t_past_bad.py index 3160d0589..a9c31e2da 100755 --- a/test_regress/t/t_past_bad.py +++ b/test_regress/t/t_past_bad.py @@ -11,6 +11,8 @@ import vltest_bootstrap test.scenarios('vlt') -test.lint(fails=True, expect_filename=test.golden_filename) +test.lint(fails=True, + expect_filename=test.golden_filename, + verilator_flags2=['--max-num-width 2147483647']) test.passes() diff --git a/test_regress/t/t_past_bad.v b/test_regress/t/t_past_bad.v index 20fd3eda8..88f904e1e 100644 --- a/test_regress/t/t_past_bad.v +++ b/test_regress/t/t_past_bad.v @@ -16,5 +16,8 @@ module t (/*AUTOARG*/ if ($past(d, num)) $stop; // IEEE 16.9.3 must be const if ($past(d, 0)) $stop; // IEEE 16.9.3 must be >= 0 if ($past(d, 10000)) $stop; // TICKCOUNT + if ($past(d, 32'h7fffffff)) $stop; + if ($past(d, 32'h7ffffffe)) $stop; + if ($past(d, 32'h7ffffffc)) $stop; end endmodule diff --git a/test_regress/t/t_prop_always_bad.out b/test_regress/t/t_prop_always_bad.out index 62d3d66a8..c6ff20c6f 100644 --- a/test_regress/t/t_prop_always_bad.out +++ b/test_regress/t/t_prop_always_bad.out @@ -31,4 +31,17 @@ : ... note: In instance 't' 18 | assert property (s_always [1:$] a); | ^ +%Error-UNSUPPORTED: t/t_prop_always_bad.v:23:30: Unsupported: always range bound exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 23 | assert property (always [0:MAX] a); + | ^~~ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error-UNSUPPORTED: t/t_prop_always_bad.v:24:28: Unsupported: always range bound exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 24 | assert property (always [MAX_M1:$] a); + | ^~~~~~ +%Error-UNSUPPORTED: t/t_prop_always_bad.v:25:32: Unsupported: always range bound exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 25 | assert property (s_always [0:MAX_M3] a); + | ^~~~~~ %Error: Exiting due to diff --git a/test_regress/t/t_prop_always_bad.py b/test_regress/t/t_prop_always_bad.py index 77a0ac64b..ca53a68fc 100755 --- a/test_regress/t/t_prop_always_bad.py +++ b/test_regress/t/t_prop_always_bad.py @@ -11,6 +11,8 @@ import vltest_bootstrap test.scenarios('vlt') -test.lint(expect_filename=test.golden_filename, fails=True) +test.lint(expect_filename=test.golden_filename, + verilator_flags2=['--max-num-width 2147483647'], + fails=True) test.passes() diff --git a/test_regress/t/t_prop_always_bad.v b/test_regress/t/t_prop_always_bad.v index 8fa30b3eb..7112d75fc 100644 --- a/test_regress/t/t_prop_always_bad.v +++ b/test_regress/t/t_prop_always_bad.v @@ -17,4 +17,11 @@ module t (input clk); assert property (s_always a); assert property (s_always [1:$] a); + localparam int unsigned MAX = 32'h7fffffff; + localparam int unsigned MAX_M1 = 32'h7ffffffe; + localparam int unsigned MAX_M3 = 32'h7ffffffc; + assert property (always [0:MAX] a); + assert property (always [MAX_M1:$] a); + assert property (s_always [0:MAX_M3] a); + endmodule diff --git a/test_regress/t/t_property_sexpr2_bad.out b/test_regress/t/t_property_sexpr2_bad.out index 2990fa446..3051fbb83 100644 --- a/test_regress/t/t_property_sexpr2_bad.out +++ b/test_regress/t/t_property_sexpr2_bad.out @@ -7,7 +7,7 @@ : ... note: In instance 't' 21 | assert property (@(posedge clk) ##(1+clk) val); | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr2_bad.v:23:35: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647 +%Error-UNSUPPORTED: t/t_property_sexpr2_bad.v:23:35: Unsupported: SVA cycle delay exceeds implementation limit of 65536 (--max-num-width) : ... note: In instance 't' 23 | assert property (@(posedge clk) ##32'h80000000 val); | ^~ diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.out b/test_regress/t/t_property_sexpr_range_delay_bad.out index afc85c949..c363325e7 100644 --- a/test_regress/t/t_property_sexpr_range_delay_bad.out +++ b/test_regress/t/t_property_sexpr_range_delay_bad.out @@ -19,13 +19,37 @@ : ... note: In instance 't' 34 | a6: assert property (@(posedge clk) a |-> ##[NEG:$] b); | ^~ -%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:36:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647 +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:36:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) : ... note: In instance 't' 36 | a7: assert property (@(posedge clk) a |-> ##[1:32'h80000000] b); | ^~ ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest -%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:37:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483647 +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:37:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) : ... note: In instance 't' 37 | a8: assert property (@(posedge clk) a |-> ##[32'h80000000:$] b); | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:42:45: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 42 | a9: assert property (@(posedge clk) a |-> ##MAX b); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:43:46: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 43 | a10: assert property (@(posedge clk) a |-> ##[0:MAX_M1] b); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:44:46: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 44 | a11: assert property (@(posedge clk) a |-> ##[MAX_M3:$] b); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:45:43: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 45 | a12: assert property (@(posedge clk) (a ##MAX_M3 b ##4 a) intersect (a ##MAX_M3 b ##4 a)); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:45:74: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 45 | a12: assert property (@(posedge clk) (a ##MAX_M3 b ##4 a) intersect (a ##MAX_M3 b ##4 a)); + | ^~ +%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:46:52: Unsupported: SVA cycle delay exceeds implementation limit of 2147483615 (host arithmetic limit) + : ... note: In instance 't' + 46 | a13: assert property (@(posedge clk) a within (a ##MAX_M3 b)); + | ^~ %Error: Exiting due to diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.py b/test_regress/t/t_property_sexpr_range_delay_bad.py index 504773395..198a3f9a0 100755 --- a/test_regress/t/t_property_sexpr_range_delay_bad.py +++ b/test_regress/t/t_property_sexpr_range_delay_bad.py @@ -11,8 +11,9 @@ import vltest_bootstrap test.scenarios('vlt') -test.lint(expect_filename=test.golden_filename, - verilator_flags2=['--assert', '--timing', '--error-limit 1000'], - fails=True) +test.lint( + expect_filename=test.golden_filename, + verilator_flags2=['--assert', '--timing', '--error-limit 1000', '--max-num-width 2147483647'], + fails=True) test.passes() diff --git a/test_regress/t/t_property_sexpr_range_delay_bad.v b/test_regress/t/t_property_sexpr_range_delay_bad.v index 0188ca685..1ab8aaef3 100644 --- a/test_regress/t/t_property_sexpr_range_delay_bad.v +++ b/test_regress/t/t_property_sexpr_range_delay_bad.v @@ -36,4 +36,13 @@ module t; a7: assert property (@(posedge clk) a |-> ##[1:32'h80000000] b); a8: assert property (@(posedge clk) a |-> ##[32'h80000000:$] b); + localparam int unsigned MAX = 32'h7fffffff; + localparam int unsigned MAX_M1 = 32'h7ffffffe; + localparam int unsigned MAX_M3 = 32'h7ffffffc; + a9: assert property (@(posedge clk) a |-> ##MAX b); + a10: assert property (@(posedge clk) a |-> ##[0:MAX_M1] b); + a11: assert property (@(posedge clk) a |-> ##[MAX_M3:$] b); + a12: assert property (@(posedge clk) (a ##MAX_M3 b ##4 a) intersect (a ##MAX_M3 b ##4 a)); + a13: assert property (@(posedge clk) a within (a ##MAX_M3 b)); + endmodule diff --git a/test_regress/t/t_sva_max_bound.py b/test_regress/t/t_sva_max_bound.py new file mode 100755 index 000000000..a5a67761f --- /dev/null +++ b/test_regress/t/t_sva_max_bound.py @@ -0,0 +1,16 @@ +#!/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.lint(verilator_flags2=['--assert', '--max-num-width 2147483647', '-Wno-TICKCOUNT']) + +test.passes() diff --git a/test_regress/t/t_sva_max_bound.v b/test_regress/t/t_sva_max_bound.v new file mode 100644 index 000000000..b89bcd19c --- /dev/null +++ b/test_regress/t/t_sva_max_bound.v @@ -0,0 +1,47 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 Antmicro +// SPDX-License-Identifier: CC0-1.0 + +module t ( + input clk, + input a, + input b +); + localparam int unsigned MAX_SUPPORTED = 32'h7fffffdf; // INT_MAX - 32 + + default clocking cb @(posedge clk); + endclocking + + sequence s_fixed; a ##MAX_SUPPORTED b; endsequence + + sequence s_range_hi; a ##[0:MAX_SUPPORTED] b; endsequence + + sequence s_range_lo; a ##[MAX_SUPPORTED:$] b; endsequence + + sequence s_intersect; + (a ##MAX_SUPPORTED b ##4 a) intersect (a ##MAX_SUPPORTED b ##4 a); + endsequence + + sequence s_within; a within (a ##MAX_SUPPORTED b); endsequence + + sequence s_past; + $past( + a, MAX_SUPPORTED + ); + endsequence + + property p_always_hi; + always[0: MAX_SUPPORTED] a; + endproperty + + property p_always_lo; + always[MAX_SUPPORTED: $] a; + endproperty + + property p_s_always_hi; + s_always[0: MAX_SUPPORTED] a; + endproperty + +endmodule