Merge e331b5b8d7 into f232449252

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

@@ -215,6 +215,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

@@ -1829,6 +1829,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);
     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

@@ -355,6 +355,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
@@ -643,6 +644,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

@@ -2048,95 +2048,214 @@ class ConstraintExprVisitor final : public VNVisitor {
             return;
         }
 
-        // Array reduction without 'with' clause (sum, product, and, or, xor)
-        // For dynamic arrays, V3Width keeps these as AstCMethodHard.
-        // Register each element as individual scalar solver variable at constraint
-        // setup time, then build SMT reduction expression over those variables.
-        if (nodep->fromp()->user1()
-            && (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)) {
+        // Array reduction methods (sum, product, and, or, xor)
+        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) {
 
-            AstVarRef* const arrRefp = VN_CAST(nodep->fromp(), VarRef);
-            UASSERT_OBJ(arrRefp, nodep, "Array reduction in constraint has non-VarRef source");
-            AstVar* const arrVarp = arrRefp->varp();
-            const std::string smtArrayName = arrVarp->name();
+            AstWith* const withp = nodep->withp();
 
-            // Get element width
-            AstNodeDType* elemDtp = arrVarp->dtypep()->skipRefp()->subDTypep();
-            const int elemWidth = elemDtp->width();
+            // For 'with' clause: check array size limit and item.index support
+            if (withp) {
+                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;
+                    }
+                }
 
-            // Compute correctly-sized identity value for empty array case
-            const int hexDigits = (elemWidth + 3) / 4;
-            std::string zeroIdentity = "#x" + std::string(hexDigits, '0');
-            std::string oneIdentity = "#x" + std::string(hexDigits - 1, '0') + "1";
-            std::string allOnesIdentity = "#x" + std::string(hexDigits, 'f');
-
-            // Class module for generating VarRefs
-            AstNodeModule* const classModulep = m_classp ? static_cast<AstNodeModule*>(m_classp)
-                                                         : VN_AS(m_genp->user2p(), NodeModule);
-
-            // Mark array as handled so BasicRand skips it. Solver controls
-            // element values via per-element write_var calls in the foreach below.
-            // Don't generate constructor write_var with dimension>0: dynamic arrays
-            // are empty at construction, so record_arr_table finds no elements.
-            arrVarp->user3(true);
-
-            AstVar* const newVarp
-                = new AstVar{fl, VVarType::BLOCKTEMP, "__Vreduce", nodep->findSigned32DType()};
-            AstForeachHeader* const headerp
-                = new AstForeachHeader{fl, nodep->fromp()->cloneTreePure(false), newVarp};
-
-            // Foreach body: register element as scalar solver var + append name
-            AstCStmt* const cstmtp = new AstCStmt{fl};
-            // char __Vn[128]; VL_SNPRINTF(__Vn, ..., "arrayname_%x", idx);
-            cstmtp->add("{\nchar __Vn[128];\nVL_SNPRINTF(__Vn, sizeof(__Vn), \"" + smtArrayName
-                        + "_%x\", (unsigned)");
-            cstmtp->add(new AstVarRef{fl, newVarp, VAccess::READ});
-            cstmtp->add(");\n");
-            // constraint.write_var(array.atWrite(idx), width, __Vn, 0);
-            cstmtp->add(new AstVarRef{fl, classModulep, m_genp, VAccess::READWRITE});
-            cstmtp->add(".write_var(");
-            cstmtp->add(new AstVarRef{fl, classModulep, arrVarp, VAccess::READWRITE});
-            cstmtp->add(".atWrite(");
-            cstmtp->add(new AstVarRef{fl, newVarp, VAccess::READ});
-            cstmtp->add("), " + std::to_string(elemWidth) + "ULL, __Vn, 0ULL);\n");
-            // ret += " "; ret += __Vn;
-            cstmtp->add("ret += \" \";\nret += __Vn;\n}\n");
-
-            AstCExpr* const cexprp = new AstCExpr{fl};
-            cexprp->dtypeSetString();
-            cexprp->add("([&]{\nstd::string ret;\n");
-            cexprp->add(new AstBegin{fl, "", new AstForeach{fl, headerp, cstmtp}, true});
-
-            const char* smtOp = nullptr;
-            std::string identity;
-            if (nodep->method() == VCMethod::ARRAY_R_SUM) {
-                smtOp = "bvadd";
-                identity = zeroIdentity;
-            } else if (nodep->method() == VCMethod::ARRAY_R_PRODUCT) {
-                smtOp = "bvmul";
-                identity = oneIdentity;
-            } else if (nodep->method() == VCMethod::ARRAY_R_AND) {
-                smtOp = "bvand";
-                identity = allOnesIdentity;
-            } else if (nodep->method() == VCMethod::ARRAY_R_OR) {
-                smtOp = "bvor";
-                identity = zeroIdentity;
-            } else if (nodep->method() == VCMethod::ARRAY_R_XOR) {
-                smtOp = "bvxor";
-                identity = zeroIdentity;
-            } else {
-                nodep->v3fatalSrc("Unhandled reduction method");
+                bool hasItemIndex = false;
+                withp->exprp()->foreach([&](AstLambdaArgRef* refp) {
+                    if (refp->index()) hasItemIndex = true;
+                });
+                if (hasItemIndex) {
+                    nodep->v3warn(CONSTRAINTIGN,
+                                  "Unsupported: item.index in array reduction constraint 'with' "
+                                  "clause; treating as state");
+                    nodep->user1(false);
+                    if (editFormat(nodep)) return;
+                    nodep->v3fatalSrc("Method not handled in constraints? " << nodep);
+                    return;
+                }
             }
 
-            cexprp->add(std::string("return ret.empty() ? \"") + identity + "\" : \"(" + smtOp
-                        + "\" + ret + \")\";\n})()");
-            // Unlink fromp before replacing (newSel already unlinked it in v1,
-            // but here we used cloneTreePure, so fromp is still linked)
-            nodep->replaceWith(new AstSFormatF{fl, "%@", false, cexprp});
+            // For without 'with' clause: need random array for variable registration
+            const bool hasRandomArray = nodep->fromp()->user1();
+            if (!withp && !hasRandomArray) {
+                // No 'with' clause and not a random array - can't handle
+                nodep->v3warn(CONSTRAINTIGN,
+                              "Unsupported: randomizing this expression, treating as state");
+                nodep->user1(false);
+                if (editFormat(nodep)) return;
+                nodep->v3fatalSrc("Method not handled in constraints? " << nodep);
+                return;
+            }
+
+            // Create loop variable and header
+            AstVar* const loopVarp
+                = new AstVar{fl, VVarType::BLOCKTEMP, "__Vreduce", nodep->findSigned32DType()};
+            AstForeachHeader* const headerp
+                = new AstForeachHeader{fl, nodep->fromp()->cloneTreePure(false), loopVarp};
+
+            // Determine SMT operation and compute identity elements
+            const char* smtOp = nullptr;
+            std::string identity;
+            if (withp) {
+                // For 'with' clause: use binary format, compute from result width
+                const int width = nodep->dtypep()->width();
+                if (nodep->method() == VCMethod::ARRAY_R_SUM) {
+                    smtOp = "bvadd";
+                    identity = "#b" + std::string(width, '0');
+                } else if (nodep->method() == VCMethod::ARRAY_R_PRODUCT) {
+                    smtOp = "bvmul";
+                    identity = (width > 0) ? "#b" + std::string(width - 1, '0') + "1" : "#b0";
+                } else if (nodep->method() == VCMethod::ARRAY_R_AND) {
+                    smtOp = "bvand";
+                    identity = "#b" + std::string(width, '1');
+                } else if (nodep->method() == VCMethod::ARRAY_R_OR) {
+                    smtOp = "bvor";
+                    identity = "#b" + std::string(width, '0');
+                } else {  // ARRAY_R_XOR
+                    smtOp = "bvxor";
+                    identity = "#b" + std::string(width, '0');
+                }
+            } else {
+                // For without 'with' clause: use hex format, compute from element width
+                AstVarRef* const arrRefp = VN_CAST(nodep->fromp(), VarRef);
+                UASSERT_OBJ(arrRefp, nodep, "Array reduction in constraint has non-VarRef source");
+                AstVar* const arrVarp = arrRefp->varp();
+                AstNodeDType* elemDtp = arrVarp->dtypep()->skipRefp()->subDTypep();
+                const int elemWidth = elemDtp->width();
+                const int hexDigits = (elemWidth + 3) / 4;
+
+                std::string zeroIdentity = "#x" + std::string(hexDigits, '0');
+                std::string oneIdentity = "#x" + std::string(hexDigits - 1, '0') + "1";
+                std::string allOnesIdentity = "#x" + std::string(hexDigits, 'f');
+
+                if (nodep->method() == VCMethod::ARRAY_R_SUM) {
+                    smtOp = "bvadd";
+                    identity = zeroIdentity;
+                } else if (nodep->method() == VCMethod::ARRAY_R_PRODUCT) {
+                    smtOp = "bvmul";
+                    identity = oneIdentity;
+                } else if (nodep->method() == VCMethod::ARRAY_R_AND) {
+                    smtOp = "bvand";
+                    identity = allOnesIdentity;
+                } else if (nodep->method() == VCMethod::ARRAY_R_OR) {
+                    smtOp = "bvor";
+                    identity = zeroIdentity;
+                } else {  // ARRAY_R_XOR
+                    smtOp = "bvxor";
+                    identity = zeroIdentity;
+                }
+            }
+
+            // Build loop body based on whether we have a 'with' clause
+            AstCStmt* const cstmtp = new AstCStmt{fl};
+            if (withp) {
+                // With 'with' clause: evaluate expression for each element
+                const bool randArr = nodep->fromp()->user1();
+                AstNodeExpr* const idxRefp = new AstVarRef{fl, loopVarp, VAccess::READ};
+                AstNodeExpr* const elemSelp = newSel(fl, nodep->fromp(), idxRefp);
+                elemSelp->user1(randArr);
+
+                AstNode* perElemExprp = withp->exprp()->cloneTreePure(false);
+                if (AstLambdaArgRef* const rootRefp = VN_CAST(perElemExprp, LambdaArgRef)) {
+                    perElemExprp = elemSelp->cloneTreePure(false);
+                    VL_DO_DANGLING(rootRefp->deleteTree(), rootRefp);
+                } else {
+                    perElemExprp->foreach([&](AstLambdaArgRef* refp) {
+                        refp->replaceWith(elemSelp->cloneTreePure(false));
+                        VL_DO_DANGLING(pushDeletep(refp), refp);
+                    });
+                }
+                VL_DO_DANGLING(elemSelp->deleteTree(), elemSelp);
+
+                perElemExprp->foreach([](AstNode* nodep) {
+                    if (!VN_IS(nodep, Const)) nodep->user1(true);
+                });
+
+                cstmtp->add("ret = \"(" + std::string(smtOp) + " \" + ret + \" \";\n");
+                cstmtp->add("ret += ");
+                cstmtp->add(iterateSubtreeReturnEdits(perElemExprp));
+                cstmtp->add(";\n");
+                cstmtp->add("ret += \")\";\n");
+            } else {
+                // Without 'with' clause: register each element as solver variable
+                AstVarRef* const arrRefp = VN_CAST(nodep->fromp(), VarRef);
+                AstVar* const arrVarp = arrRefp->varp();
+                const std::string smtArrayName = arrVarp->name();
+                AstNodeDType* elemDtp = arrVarp->dtypep()->skipRefp()->subDTypep();
+                const int elemWidth = elemDtp->width();
+                AstNodeModule* const classModulep = m_classp
+                                                        ? static_cast<AstNodeModule*>(m_classp)
+                                                        : VN_AS(m_genp->user2p(), NodeModule);
+                arrVarp->user3(true);
+
+                // Create variable name using AstSFormatF
+                AstSFormatF* const varNamep = new AstSFormatF{
+                    fl, smtArrayName + "_%x", false, new AstVarRef{fl, loopVarp, VAccess::READ}};
+
+                // Create array element reference: array.atWrite(index)
+                AstCMethodHard* const atWritep = new AstCMethodHard{
+                    fl, new AstVarRef{fl, classModulep, arrVarp, VAccess::READWRITE},
+                    VCMethod::ARRAY_AT_WRITE, new AstVarRef{fl, loopVarp, VAccess::READ}};
+                atWritep->dtypeFrom(elemDtp);
+
+                // Convert std::string to const char* for write_var
+                AstCExpr* const varNameCStrp = new AstCExpr{fl, AstCExpr::Pure{}};
+                varNameCStrp->dtypeSetString();
+                varNameCStrp->add("(");
+                varNameCStrp->add(varNamep->cloneTree(false));
+                varNameCStrp->add(").c_str()");
+
+                // Create write_var method call: gen.write_var(arrElement, width, name, 0)
+                AstCMethodHard* const writeVarp = new AstCMethodHard{
+                    fl, new AstVarRef{fl, classModulep, m_genp, VAccess::READWRITE},
+                    VCMethod::RANDOMIZER_WRITE_VAR, atWritep};
+                writeVarp->addPinsp(new AstConst{fl, AstConst::WidthedValue{}, 64,
+                                                 static_cast<uint32_t>(elemWidth)});
+                writeVarp->addPinsp(varNameCStrp);
+                writeVarp->addPinsp(new AstConst{fl, AstConst::WidthedValue{}, 64, 0});
+                writeVarp->dtypeSetVoid();
+
+                cstmtp->add(writeVarp->makeStmt());
+                cstmtp->add("ret += \" \";\n");
+                cstmtp->add("ret += ");
+                cstmtp->add(varNamep);
+                cstmtp->add(";\n");
+            }
+
+            // Build final expression
+            if (withp) {
+                // For 'with' clause: use lambda expression with AstCExpr
+                AstCExpr* const cexprp = new AstCExpr{fl};
+                cexprp->dtypeSetString();
+                cexprp->add("([&]{\nstd::string ret = \"" + identity + "\";\n");
+                cexprp->add(new AstBegin{fl, "", new AstForeach{fl, headerp, cstmtp}, true});
+                cexprp->add("return ret;\n})()");
+                nodep->replaceWith(new AstSFormatF{fl, "%@", false, cexprp});
+            } else {
+                // For without 'with' clause: use AstCExpr with conditional
+                AstCExpr* const cexprp = new AstCExpr{fl};
+                cexprp->dtypeSetString();
+                cexprp->add("([&]{\nstd::string ret;\n");
+                cexprp->add(new AstBegin{fl, "", new AstForeach{fl, headerp, cstmtp}, true});
+                cexprp->add("return ret.empty() ? \"" + identity + "\" : \"(" + smtOp
+                            + "\" + ret + \")\";\n})()");
+                nodep->replaceWith(new AstSFormatF{fl, "%@", false, cexprp});
+            }
             VL_DO_DANGLING(nodep->deleteTree(), nodep);
             return;
         }

test_regress/t/t_constraint_array_index_unsup.out

@@ -0,0 +1,6 @@
+%Warning-CONSTRAINTIGN: t/t_constraint_array_index_unsup.v:13:11: Unsupported: item.index in array reduction constraint 'with' clause; treating as state
+   13 |      data.sum() with (item.index) <= 10;
+      |           ^~~
+                        ... 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_index_unsup.py

@@ -0,0 +1,19 @@
+#!/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: 2024 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(fails=True, expect_filename=test.golden_filename)
+
+test.passes()

test_regress/t/t_constraint_array_index_unsup.v

@@ -0,0 +1,29 @@
+// DESCRIPTION: Verilator: Verilog Test module
+//
+// This file ONLY is placed under the Creative Commons Public Domain.
+// SPDX-FileCopyrightText: 2024 Wilson Snyder
+// SPDX-License-Identifier: CC0-1.0
+
+// Test that item.index in array reduction constraints is not yet supported
+class Packet;
+  rand bit [3:0] data[5];
+
+  constraint c {
+     // This should trigger unsupported warning
+     data.sum() with (item.index) <= 10;
+  }
+endclass
+
+module t;
+  initial begin
+     Packet p;
+     int i;
+
+     p = new;
+
+     i = p.randomize();
+
+     $write("*-* All Finished *-*\n");
+     $finish;
+  end
+endmodule

test_regress/t/t_constraint_array_limit.out

@@ -0,0 +1,6 @@
+%Warning-CONSTRAINTIGN: t/t_constraint_array_limit.v:15:10: 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/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: 2024 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(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.
+// SPDX-FileCopyrightText: 2024 Wilson Snyder
+// 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