From 893589f4443e7788447bada5a5c744187fdbfd79 Mon Sep 17 00:00:00 2001 From: Rahul Behl Date: Mon, 2 Feb 2026 11:55:55 +0530 Subject: [PATCH 1/2] Support array reduction methods with 'with' clause in constraints Fixes #6455 This commit adds support for array reduction methods (sum, product, and, or, xor) with 'with' clauses in randomization constraints. Previously, expressions like 'array.sum() with (int'(item == value))' were not supported in constraints. Implementation details: - Added handler in ConstraintExprVisitor::visit(AstCMethodHard*) for ARRAY_R_SUM, ARRAY_R_PRODUCT, ARRAY_R_AND, ARRAY_R_OR, ARRAY_R_XOR - Substitutes lambda argument references (item/index) in the with expression - Generates appropriate SMT operations (bvadd, bvmul, bvand, bvor, bvxor) - Uses correct identity elements for each reduction operation - Marks non-constant nodes with user1() flag to ensure proper SMT code generation The implementation follows the same pattern as the existing ARRAY_INSIDE handler, generating SMT expressions at Verilator compile time that are evaluated by the constraint solver at runtime. --- bin/verilator | 1 + docs/guide/exe_verilator.rst | 11 + src/V3Options.cpp | 1 + src/V3Options.h | 2 + src/V3Randomize.cpp | 287 +++++++++++++----- .../t/t_constraint_array_index_unsup.out | 6 + .../t/t_constraint_array_index_unsup.py | 19 ++ .../t/t_constraint_array_index_unsup.v | 29 ++ test_regress/t/t_constraint_array_limit.out | 6 + test_regress/t/t_constraint_array_limit.py | 21 ++ test_regress/t/t_constraint_array_limit.v | 38 +++ test_regress/t/t_constraint_array_sum_with.py | 21 ++ test_regress/t/t_constraint_array_sum_with.v | 217 +++++++++++++ 13 files changed, 575 insertions(+), 84 deletions(-) create mode 100644 test_regress/t/t_constraint_array_index_unsup.out create mode 100755 test_regress/t/t_constraint_array_index_unsup.py create mode 100644 test_regress/t/t_constraint_array_index_unsup.v create mode 100644 test_regress/t/t_constraint_array_limit.out create mode 100755 test_regress/t/t_constraint_array_limit.py create mode 100644 test_regress/t/t_constraint_array_limit.v create mode 100755 test_regress/t/t_constraint_array_sum_with.py create mode 100644 test_regress/t/t_constraint_array_sum_with.v diff --git a/bin/verilator b/bin/verilator index ab07e6201..c1fd70398 100755 --- a/bin/verilator +++ b/bin/verilator @@ -345,6 +345,7 @@ detailed descriptions of these arguments. -CFLAGS C++ compiler arguments for makefile --compiler Tune for specified C++ compiler --compiler-include Include additional header in the precompiled one + --constraint-array-limit Maximum array size for constraint array reduction --converge-limit Tune convergence settle time --coverage Enable all coverage --coverage-expr Enable expression coverage diff --git a/docs/guide/exe_verilator.rst b/docs/guide/exe_verilator.rst index 791d9417f..21f301be8 100644 --- a/docs/guide/exe_verilator.rst +++ b/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 `. +.. option:: --constraint-array-limit + + 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 Rarely needed. Specifies the maximum number of runtime iterations before diff --git a/src/V3Options.cpp b/src/V3Options.cpp index 7018bc296..65e4d34e0 100644 --- a/src/V3Options.cpp +++ b/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 diff --git a/src/V3Options.h b/src/V3Options.h index 138c597b3..83ffe1886 100644 --- a/src/V3Options.h +++ b/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; } diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 4e5e25eff..3637d74de 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -1985,95 +1985,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(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(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(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; } diff --git a/test_regress/t/t_constraint_array_index_unsup.out b/test_regress/t/t_constraint_array_index_unsup.out new file mode 100644 index 000000000..1d9c596e4 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_constraint_array_index_unsup.py b/test_regress/t/t_constraint_array_index_unsup.py new file mode 100755 index 000000000..d85bfeb37 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_constraint_array_index_unsup.v b/test_regress/t/t_constraint_array_index_unsup.v new file mode 100644 index 000000000..c22469a75 --- /dev/null +++ b/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 diff --git a/test_regress/t/t_constraint_array_limit.out b/test_regress/t/t_constraint_array_limit.out new file mode 100644 index 000000000..2394ae08a --- /dev/null +++ b/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 diff --git a/test_regress/t/t_constraint_array_limit.py b/test_regress/t/t_constraint_array_limit.py new file mode 100755 index 000000000..fac064bd4 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_constraint_array_limit.v b/test_regress/t/t_constraint_array_limit.v new file mode 100644 index 000000000..6683227cf --- /dev/null +++ b/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 diff --git a/test_regress/t/t_constraint_array_sum_with.py b/test_regress/t/t_constraint_array_sum_with.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_constraint_array_sum_with.v b/test_regress/t/t_constraint_array_sum_with.v new file mode 100644 index 000000000..01e7dfa71 --- /dev/null +++ b/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 From e331b5b8d7c4343f0758d6815f39d2b049386a9d Mon Sep 17 00:00:00 2001 From: Rahul Behl Date: Thu, 5 Feb 2026 12:08:08 +0530 Subject: [PATCH 2/2] Updating contributors --- docs/CONTRIBUTORS | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/CONTRIBUTORS b/docs/CONTRIBUTORS index 5ac1958e1..dfaa40281 100644 --- a/docs/CONTRIBUTORS +++ b/docs/CONTRIBUTORS @@ -214,6 +214,7 @@ Piotr Binkowski Qingyao Sun Quentin Corradi Rafal Kapuscik +Rahul Behl Rasfunk Raynard Qiao Ricardo Barbedo