Fix V3Width SVA bound limit guard, leave headroom for alignment, respect --max-num-width (#8192)

Signed-off-by: Artur Bieniek <[email protected]>

docs/guide/exe_verilator.rst

@@ -1223,6 +1223,8 @@ Summary:
 .. option:: --max-num-width <value>
 
    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 <directory>

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<unsigned>(std::numeric_limits<int>::max()) - 32U;
+        const unsigned configuredLimit = static_cast<unsigned>(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"

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

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

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

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

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

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

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);
       |                                   ^~

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

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

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

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

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