Merge c9d7713389 into a0b89dde8e

bin/verilator

@@ -345,6 +345,7 @@ detailed descriptions of these arguments.
      -CFLAGS <flags>            C++ compiler arguments for makefile
     --compiler <compiler-name>  Tune for specified C++ compiler
     --compiler-include          Include additional header in the precompiled one
+    --constraint-array-limit <size>   Maximum array size for constraint array reduction
     --converge-limit <loops>    Tune convergence settle time
     --coverage                  Enable all coverage
     --coverage-expr             Enable expression coverage

docs/CONTRIBUTORS

@@ -211,6 +211,7 @@ Piotr Binkowski
 Qingyao Sun
 Quentin Corradi
 Rafal Kapuscik
+Rahul Behl
 Rasfunk
 Raynard Qiao
 Ricardo Barbedo

docs/guide/exe_verilator.rst

@@ -262,6 +262,17 @@ Summary:
    limitation that allow only one precompiled header per compilation.
    Use this instead of ::vlopt:`-CFLAGS` with `-include <header-path>`.
 
+.. option:: --constraint-array-limit <size>
+
+   Specifies the maximum array size for which array reduction methods
+   (sum, product, and, or, xor) in constraint expressions will be
+   expanded. Arrays larger than this limit will have their reduction
+   constraints ignored with a `CONSTRAINTIGN` warning. This prevents
+   excessive code generation for very large arrays.
+
+   Defaults to 64. Setting to 0 disables all array reduction constraint
+   expansion.
+
 .. option:: --converge-limit <loops>
 
    Rarely needed. Specifies the maximum number of runtime iterations before

src/V3Options.cpp

@@ -1826,6 +1826,7 @@ void V3Options::parseOptsList(FileLine* fl, const string& optdir, int argc,
     DECL_OPTION("-U", CbPartialMatch, &V3PreShell::undef);
     DECL_OPTION("-underline-zero", OnOff, &m_underlineZero).undocumented();  // Deprecated
     DECL_OPTION("-no-unlimited-stack", CbCall, []() {});  // Processed only in bin/verilator shell
+    DECL_OPTION("-constraint-array-limit", Set, &m_constraintArrayLimit).undocumented();
     DECL_OPTION("-unroll-count", Set, &m_unrollCount).undocumented();  // Optimization tweak
     DECL_OPTION("-unroll-limit", Set, &m_unrollLimit);
     DECL_OPTION("-unroll-stmts", Set, &m_unrollStmts).undocumented();  // Optimization tweak

src/V3Options.h

@@ -352,6 +352,7 @@ private:
     int         m_unrollCount = 64;  // main switch: --unroll-count
     int         m_unrollLimit = 16384;  // main switch: --unroll-limit
     int         m_unrollStmts = 30000;  // main switch: --unroll-stmts
+    int         m_constraintArrayLimit = 64;  // main switch: --constraint-array-limit
     int         m_verilateJobs = -1;  // main switch: --verilate-jobs
 
     int         m_compLimitBlocks = 0;  // compiler selection; number of nested blocks
@@ -636,6 +637,7 @@ public:
     int unrollCount() const { return m_unrollCount; }
     int unrollLimit() const { return m_unrollLimit; }
     int unrollStmts() const { return m_unrollStmts; }
+    int constraintArrayLimit() const { return m_constraintArrayLimit; }
     int verilateJobs() const { return m_verilateJobs; }
 
     int compLimitBlocks() const { return m_compLimitBlocks; }

src/V3Randomize.cpp

@@ -1830,6 +1830,135 @@ class ConstraintExprVisitor final : public VNVisitor {
             return;
         }
 
+        // Handle array reduction methods with 'with' clause
+        if (nodep->method() == VCMethod::ARRAY_R_SUM
+            || nodep->method() == VCMethod::ARRAY_R_PRODUCT
+            || nodep->method() == VCMethod::ARRAY_R_AND || nodep->method() == VCMethod::ARRAY_R_OR
+            || nodep->method() == VCMethod::ARRAY_R_XOR) {
+            // Handle array reduction methods with 'with' clause
+            AstWith* const withp = VN_CAST(nodep->pinsp(), With);
+            UASSERT_OBJ(withp, nodep, "Array reduction in constraint should have 'with' clause");
+
+            // Check array size against limit to avoid code explosion
+            if (AstUnpackArrayDType* const adtypep
+                = VN_CAST(nodep->fromp()->dtypep()->skipRefp(), UnpackArrayDType)) {
+                const int arraySize = adtypep->elementsConst();
+                if (arraySize > v3Global.opt.constraintArrayLimit()) {
+                    nodep->v3warn(CONSTRAINTIGN,
+                                  "Constraint array reduction ignored (array size "
+                                      + cvtToStr(arraySize)
+                                      + " exceeds --constraint-array-limit of "
+                                      + cvtToStr(v3Global.opt.constraintArrayLimit())
+                                      + "), treating as state");
+                    nodep->user1(false);
+                    if (editFormat(nodep)) return;
+                    nodep->v3fatalSrc("Method not handled in constraints? " << nodep);
+                    return;
+                }
+            }
+
+            const bool randArr = nodep->fromp()->user1();
+
+            // Create loop variable
+            AstVar* const loopVarp
+                = new AstVar{fl, VVarType::BLOCKTEMP, "__Vreduce", nodep->findSigned32DType()};
+            AstNodeExpr* const idxRefp = new AstVarRef{fl, loopVarp, VAccess::READ};
+
+            // Create array iteration structure
+            AstSelLoopVars* const arrayLoopVars
+                = new AstSelLoopVars{fl, nodep->fromp()->cloneTreePure(false), loopVarp};
+
+            // Get array element selector
+            AstNodeExpr* const elemSelp = newSel(fl, nodep->fromp(), idxRefp);
+            elemSelp->user1(randArr);
+
+            // Clone the 'with' expression and substitute lambda args
+            AstNode* perElemExprp = withp->exprp()->cloneTreePure(false);
+
+            // Substitute lambda argument references with actual array element/index
+            // Handle case where perElemExprp itself is a LambdaArgRef
+            if (AstLambdaArgRef* const rootRefp = VN_CAST(perElemExprp, LambdaArgRef)) {
+                if (rootRefp->index()) {
+                    perElemExprp = idxRefp->cloneTreePure(false);
+                } else {
+                    perElemExprp = elemSelp->cloneTreePure(false);
+                }
+                VL_DO_DANGLING(rootRefp->deleteTree(), rootRefp);
+            } else {
+                perElemExprp->foreach([&](AstLambdaArgRef* refp) {
+                    if (refp->index()) {
+                        refp->replaceWith(idxRefp->cloneTreePure(false));
+                    } else {
+                        refp->replaceWith(elemSelp->cloneTreePure(false));
+                    }
+                    VL_DO_DANGLING(pushDeletep(refp), refp);
+                });
+            }
+            // Clean up the original template nodes (elemSelp contains idxRefp)
+            VL_DO_DANGLING(elemSelp->deleteTree(), elemSelp);
+
+            // Mark all non-constant nodes in the expression as depending on random variables
+            // Constants remain unmarked so they'll be formatted as SMT constants
+            perElemExprp->foreach([](AstNode* nodep) {
+                if (!VN_IS(nodep, Const)) nodep->user1(true);
+            });
+
+            // Determine SMT operation and identity element
+            std::string smtOp;
+            std::string identityVal;
+            if (nodep->method() == VCMethod::ARRAY_R_SUM) {
+                smtOp = "bvadd";
+                identityVal = "#b" + std::string(nodep->dtypep()->width(), '0');
+            } else if (nodep->method() == VCMethod::ARRAY_R_PRODUCT) {
+                smtOp = "bvmul";
+                // Identity = 1 in binary (guard against zero width to avoid out-of-bounds)
+                const size_t w = nodep->dtypep()->width();
+                identityVal = (w > 0) ? "#b" + std::string(w - 1, '0') + "1" : "#b0";
+            } else if (nodep->method() == VCMethod::ARRAY_R_AND) {
+                smtOp = "bvand";
+                // Identity = all 1s
+                identityVal = "#b" + std::string(nodep->dtypep()->width(), '1');
+            } else if (nodep->method() == VCMethod::ARRAY_R_OR) {
+                smtOp = "bvor";
+                identityVal = "#b" + std::string(nodep->dtypep()->width(), '0');
+            } else {  // ARRAY_R_XOR
+                smtOp = "bvxor";
+                identityVal = "#b" + std::string(nodep->dtypep()->width(), '0');
+            }
+
+            // Build the loop body that accumulates results
+            AstCStmt* const cstmtp = new AstCStmt{fl};
+            cstmtp->add("ret = \"(" + smtOp + " \" + ret + \" \";\n");
+            cstmtp->add("ret += ");
+            cstmtp->add(iterateSubtreeReturnEdits(perElemExprp));
+            cstmtp->add(";\n");
+            cstmtp->add("ret += \")\";\n");
+
+            // Initialize return value variable
+            AstCStmt* const initStmtp = new AstCStmt{fl};
+            initStmtp->add("std::string ret = \"" + identityVal + "\";\n");
+
+            // Create loop statement
+            AstNode* const loopStmtp
+                = new AstBegin{fl, "", new AstForeach{fl, arrayLoopVars, cstmtp}, true};
+
+            // Create return expression
+            AstCExpr* const retExprp = new AstCExpr{fl, AstCExpr::Pure{}, "ret"};
+            retExprp->dtypeSetString();
+
+            // Build lambda as AstExprStmt with CReturn
+            AstNode* const lambdaStmtsp = initStmtp;
+            lambdaStmtsp->addNext(loopStmtp);
+            lambdaStmtsp->addNext(new AstCReturn{fl, retExprp});
+            AstExprStmt* const lambdap
+                = new AstExprStmt{fl, lambdaStmtsp, retExprp->cloneTree(false)};
+            lambdap->hasResult(false);  // Result comes from CReturn, not resultp
+
+            nodep->replaceWith(new AstSFormatF{fl, "%@", false, lambdap});
+            VL_DO_DANGLING(nodep->deleteTree(), nodep);
+            return;
+        }
+
         nodep->v3warn(CONSTRAINTIGN,
                       "Unsupported: randomizing this expression, treating as state");
         nodep->user1(false);

test_regress/t/t_constraint_array_limit.out

@@ -0,0 +1,6 @@
+%Warning-CONSTRAINTIGN: t/t_constraint_array_limit.v:15:12: Constraint array reduction ignored (array size 32 exceeds --constraint-array-limit of 16), treating as state
+   15 |       data.sum() with (item) < 1000;
+      |            ^~~
+                        ... For warning description see https://verilator.org/warn/CONSTRAINTIGN?v=latest
+                        ... Use "/* verilator lint_off CONSTRAINTIGN */" and lint_on around source to disable this message.
+%Error: Exiting due to

test_regress/t/t_constraint_array_limit.py

@@ -0,0 +1,21 @@
+#!/usr/bin/env python3
+# DESCRIPTION: Verilator: Verilog Test driver/expectations definition
+#
+# Copyright 2024 by Wilson Snyder. 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0
+
+import vltest_bootstrap
+
+test.scenarios('simulator')
+
+if not test.have_solver:
+    test.skip("No constraint solver installed")
+
+test.compile(fails=True,
+             verilator_flags2=["--constraint-array-limit", "16"],
+             expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_constraint_array_limit.v

@@ -0,0 +1,38 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain, for
+// any use, without warranty, 2024 by Ravi Behl.
+// SPDX-License-Identifier: CC0-1.0
+
+// Test that array reduction constraints are ignored when array size exceeds --constraint-array-limit
+`define stop $stop
+`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);
+
+class Packet;
+   rand int data[32];
+
+   constraint c {
+      data.sum() with (item) < 1000;
+   }
+
+   function void verify();
+      int i;
+      i = randomize();
+      `checkd(i, 1);
+   endfunction
+endclass
+
+module t;
+   initial begin
+      Packet p;
+      int success_count;
+
+      p = new;
+
+      // Try randomization -- should fail with a warning
+      p.verify();
+
+      $write("*-* All Finished *-*\n");
+      $finish;
+   end
+endmodule

test_regress/t/t_constraint_array_sum_with.py

@@ -0,0 +1,21 @@
+#!/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('simulator')
+
+if not test.have_solver:
+    test.skip("No constraint solver installed")
+
+test.compile()
+
+test.execute()
+
+test.passes()

test_regress/t/t_constraint_array_sum_with.v

@@ -0,0 +1,217 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2026 by Wilson Snyder and Contributors
+// SPDX-License-Identifier: CC0-1.0
+
+// Test case for array reduction methods with 'with' clause in constraints (issue #6455)
+`define stop $stop
+`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);
+
+class test_sum;
+  rand byte array[5];
+  rand byte repeated_value;
+
+  constraint c {
+    // Ensure exactly 3 occurrences of repeated_value using sum
+    array.sum() with (int'(item==repeated_value)) == 3;
+
+    // All other values should appear exactly once
+    foreach(array[i]) {
+      array[i] != repeated_value -> array.sum() with (int'(item==array[i])) == 1;
+    }
+  }
+
+  function void verify();
+    int count_map[byte];
+    int repeated_count = 0;
+    int i;
+
+    i = randomize();
+    `checkd(i, 1);
+
+    // Count occurrences
+    foreach (array[idx]) begin
+      if (!count_map.exists(array[idx])) count_map[array[idx]] = 0;
+      count_map[array[idx]]++;
+    end
+
+    // Check repeated_value appears exactly 3 times
+    if (count_map.exists(repeated_value)) begin
+      repeated_count = count_map[repeated_value];
+      if (repeated_count != 3) begin
+        $display("%%Error: sum test - repeated_value=%0d appears %0d times, expected 3",
+                 repeated_value, repeated_count);
+        $stop;
+      end
+    end else begin
+      $display("%%Error: sum test - repeated_value=%0d doesn't appear in array", repeated_value);
+      $stop;
+    end
+
+    // Check all other values appear exactly once
+    foreach (count_map[val]) begin
+      if (val != repeated_value && count_map[val] != 1) begin
+        $display("%%Error: sum test - value=%0d appears %0d times, expected 1", val, count_map[val]);
+        $stop;
+      end
+    end
+  endfunction
+endclass
+
+class test_product;
+  rand bit [3:0] array[4];
+
+  constraint c {
+    // Product of non-zero elements should be <= 100
+    array.product() with (item != 0 ? int'(item) : 1) <= 100;
+    // At least 2 non-zero elements
+    array.sum() with (int'(item != 0)) >= 2;
+  }
+
+  function void verify();
+    int prod = 1;
+    int nonzero_count = 0;
+    int i;
+
+    i = randomize();
+    `checkd(i, 1);
+
+    foreach (array[idx]) begin
+      if (array[idx] != 0) begin
+        prod *= array[idx];
+        nonzero_count++;
+      end
+    end
+
+    if (prod > 100) begin
+      $display("%%Error: product test - product %0d > 100", prod);
+      $stop;
+    end
+
+    if (nonzero_count < 2) begin
+      $display("%%Error: product test - only %0d non-zero elements", nonzero_count);
+      $stop;
+    end
+  endfunction
+endclass
+
+class test_and;
+  rand bit [7:0] array[3];
+
+  constraint c {
+    // AND of all elements with a mask should equal specific value
+    array.and() with (item & 8'hF0) == 8'h50;
+  }
+
+  function void verify();
+    bit [7:0] result = 8'hFF;
+    int i;
+
+    i = randomize();
+    `checkd(i, 1);
+
+    foreach (array[idx]) begin
+      result &= (array[idx] & 8'hF0);
+    end
+
+    if (result != 8'h50) begin
+      $display("%%Error: and test - result 0x%0h != 0x50", result);
+      $stop;
+    end
+  endfunction
+endclass
+
+class test_or;
+  rand bit [7:0] array[3];
+
+  constraint c {
+    // OR of specific bits should set bit 3
+    (array.or() with (item & 8'h08)) == 8'h08;
+    // At least one element has bit 3 set
+    array.sum() with (int'((item & 8'h08) != 0)) >= 1;
+  }
+
+  function void verify();
+    bit [7:0] result = 8'h00;
+    int i;
+
+    i = randomize();
+    `checkd(i, 1);
+
+    foreach (array[idx]) begin
+      result |= (array[idx] & 8'h08);
+    end
+
+    if (result != 8'h08) begin
+      $display("%%Error: or test - result 0x%0h != 0x08", result);
+      $stop;
+    end
+  endfunction
+endclass
+
+class test_xor;
+  rand bit [7:0] array[4];
+
+  constraint c {
+    // XOR of all elements should be non-zero (parity check)
+    array.xor() with (item) != 0;
+    // Ensure some variation
+    array.sum() with (int'(item != 0)) >= 2;
+  }
+
+  function void verify();
+    bit [7:0] result = 8'h00;
+    int i;
+
+    i = randomize();
+    `checkd(i, 1);
+
+    foreach (array[idx]) begin
+      result ^= array[idx];
+    end
+
+    if (result == 0) begin
+      $display("%%Error: xor test - result is 0");
+      $stop;
+    end
+  endfunction
+endclass
+
+module t;
+  test_sum sum_inst;
+  test_product product_inst;
+  test_and and_inst;
+  test_or or_inst;
+  test_xor xor_inst;
+
+  initial begin
+    // Test sum
+    sum_inst = new();
+    repeat (20) sum_inst.verify();
+    $display("sum test PASSED");
+
+    // Test product
+    product_inst = new();
+    repeat (20) product_inst.verify();
+    $display("product test PASSED");
+
+    // Test and
+    and_inst = new();
+    repeat (20) and_inst.verify();
+    $display("and test PASSED");
+
+    // Test or
+    or_inst = new();
+    repeat (20) or_inst.verify();
+    $display("or test PASSED");
+
+    // Test xor
+    xor_inst = new();
+    repeat (20) xor_inst.verify();
+    $display("xor test PASSED");
+
+    $write("*-* All Finished *-*\n");
+    $finish;
+  end
+endmodule