From 443678d8c425f31b3c84b9d3e5ef25944b214d63 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Sun, 22 Feb 2026 15:23:02 +0100 Subject: [PATCH] Support array reduction methods without 'with' clause in constraints for dynamic arrays (#7104) (#7108) --- src/V3Randomize.cpp | 93 ++++++++++++++++ .../t/t_constraint_dyn_array_reduction.py | 21 ++++ .../t/t_constraint_dyn_array_reduction.v | 104 ++++++++++++++++++ 3 files changed, 218 insertions(+) create mode 100755 test_regress/t/t_constraint_dyn_array_reduction.py create mode 100644 test_regress/t/t_constraint_dyn_array_reduction.v diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 6d886da5d..d0eb41e53 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -1933,6 +1933,99 @@ 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)) { + + 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(); + + // Get element width + AstNodeDType* elemDtp = arrVarp->dtypep()->skipRefp()->subDTypep(); + const int elemWidth = elemDtp->width(); + + // 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()}; + AstSelLoopVars* const arrayp + = new AstSelLoopVars{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, arrayp, 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"); + } + + 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}); + 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_dyn_array_reduction.py b/test_regress/t/t_constraint_dyn_array_reduction.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_constraint_dyn_array_reduction.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_dyn_array_reduction.v b/test_regress/t/t_constraint_dyn_array_reduction.v new file mode 100644 index 000000000..0fa6123dd --- /dev/null +++ b/test_regress/t/t_constraint_dyn_array_reduction.v @@ -0,0 +1,104 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`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); +`define checkh(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +// Test dynamic array reduction methods (xor, sum, and, or, product) +// without 'with' clause in constraints. +// Each method is tested in a separate class to avoid conflicting constraints. + +module t; + + class XorTest; + rand bit [7:0] data []; + rand bit [7:0] result; + function new(); data = new[4]; endfunction + constraint c_size { data.size() == 4; } + constraint c_xor { result == data.xor(); } + endclass + + class SumTest; + rand bit [7:0] data []; + rand bit [7:0] result; + function new(); data = new[4]; endfunction + constraint c_size { data.size() == 4; } + constraint c_sum { result == data.sum(); } + endclass + + class AndTest; + rand bit [7:0] data []; + rand bit [7:0] result; + function new(); data = new[4]; endfunction + constraint c_size { data.size() == 4; } + constraint c_and { result == data.and(); } + endclass + + class OrTest; + rand bit [7:0] data []; + rand bit [7:0] result; + function new(); data = new[4]; endfunction + constraint c_size { data.size() == 4; } + constraint c_or { result == data.or(); } + endclass + + class ProductTest; + rand bit [7:0] data []; + rand bit [7:0] result; + function new(); data = new[4]; endfunction + constraint c_size { data.size() == 4; } + constraint c_prod { result == data.product(); } + endclass + + initial begin + static XorTest t_xor = new(); + static SumTest t_sum = new(); + static AndTest t_and = new(); + static OrTest t_or = new(); + static ProductTest t_prod = new(); + + repeat (10) begin + bit [7:0] exp; + int i; + + // Test xor + `checkd(t_xor.randomize(), 1) + exp = 0; + foreach (t_xor.data[i]) exp ^= t_xor.data[i]; + `checkh(t_xor.result, exp) + + // Test sum + `checkd(t_sum.randomize(), 1) + exp = 0; + foreach (t_sum.data[i]) exp += t_sum.data[i]; + `checkh(t_sum.result, exp) + + // Test and + `checkd(t_and.randomize(), 1) + exp = 8'hff; + foreach (t_and.data[i]) exp &= t_and.data[i]; + `checkh(t_and.result, exp) + + // Test or + `checkd(t_or.randomize(), 1) + exp = 0; + foreach (t_or.data[i]) exp |= t_or.data[i]; + `checkh(t_or.result, exp) + + // Test product + `checkd(t_prod.randomize(), 1) + exp = 8'd1; + foreach (t_prod.data[i]) exp *= t_prod.data[i]; + `checkh(t_prod.result, exp) + end + $write("*-* All Finished *-*\n"); + $finish; + end + +endmodule