diff --git a/bin/verilator b/bin/verilator index a94b7fe56..8bdff0d52 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/CONTRIBUTORS b/docs/CONTRIBUTORS index c652b4f39..1573079b3 100644 --- a/docs/CONTRIBUTORS +++ b/docs/CONTRIBUTORS @@ -211,6 +211,7 @@ Piotr Binkowski Qingyao Sun Quentin Corradi Rafal Kapuscik +Rahul Behl Rasfunk Raynard Qiao Ricardo Barbedo diff --git a/docs/guide/exe_verilator.rst b/docs/guide/exe_verilator.rst index d9900899b..b15e07888 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 86a703515..00f1cfbde 100644 --- a/src/V3Options.cpp +++ b/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 diff --git a/src/V3Options.h b/src/V3Options.h index c761455d5..8c4120c10 100644 --- a/src/V3Options.h +++ b/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; } diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 94e694485..ff14cf1bf 100644 --- a/src/V3Randomize.cpp +++ b/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); 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..7eb325933 --- /dev/null +++ b/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 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..e8b70b0d9 --- /dev/null +++ b/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() 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..e0a00d90b --- /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, 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 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