diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index fa6d6c6a5..e94288fcf 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -998,15 +998,15 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { // Step 3: Solve phase by phase std::map solvedValues; // varName -> SMT value literal - bool hasNonEnumArray = false; + bool needsAllLogic = false; for (const auto& var : m_vars) { if (var.second->dimension() == 0) continue; - if (var.second->countMatchingElements(m_arr_vars, var.second->name()) == 0) { - hasNonEnumArray = true; + if (!var.second->hasMatchingElements(m_arr_vars, var.second->name())) { + needsAllLogic = true; break; } } - const char* const logicp = hasNonEnumArray ? "ALL" : "QF_ABV"; + const char* const logicp = needsAllLogic ? "ALL" : "QF_ABV"; for (size_t phase = 0; phase < layers.size(); phase++) { const bool isFinalPhase = (phase == layers.size() - 1); @@ -1085,8 +1085,7 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { auto arrVarsp = std::make_shared(m_arr_vars); it->second->setArrayInfo(arrVarsp); // Enumerable arrays: query each element for a QF_ABV-safe pin. - if (it->second->countMatchingElements(m_arr_vars, it->second->name()) - > 0) { + if (it->second->hasMatchingElements(m_arr_vars, it->second->name())) { it->second->emitGetValue(os); continue; } diff --git a/include/verilated_random.h b/include/verilated_random.h index 648ea560e..c09b41663 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -104,6 +104,9 @@ public: count_cache[base_name] = count; return count; } + bool hasMatchingElements(const ArrayInfoMap& arr_vars, const std::string& base_name) const { + return arr_vars.find(base_name + "0") != arr_vars.end(); + } }; template class VlRandomArrayVarTemplate final : public VlRandomVar { diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 2786ea305..6390c6906 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -2162,6 +2162,16 @@ class ConstraintExprVisitor final : public VNVisitor { // Generate solveBefore() calls for each (lhs, rhs) variable pair. // Do NOT iterate children -- these are variable references, not constraint expressions. FileLine* const fl = nodep->fileline(); + for (AstNodeExpr* const listp : {nodep->lhssp(), nodep->rhssp()}) { + for (AstNodeExpr* ep = listp; ep; ep = VN_CAST(ep->nextp(), NodeExpr)) { + if (VN_IS(ep->dtypep()->skipRefp(), AssocArrayDType)) { + ep->v3warn(E_UNSUPPORTED, + "Unsupported: 'solve ... before' with associative array"); + VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); + return; + } + } + } AstNodeModule* const genModp = VN_AS(m_genp->user2p(), NodeModule); for (AstNodeExpr* lhsp = nodep->lhssp(); lhsp; lhsp = VN_CAST(lhsp->nextp(), NodeExpr)) { diff --git a/test_regress/t/t_constraint_solve_before_array.v b/test_regress/t/t_constraint_solve_before_array.v index 535b8f462..60db27107 100644 --- a/test_regress/t/t_constraint_solve_before_array.v +++ b/test_regress/t/t_constraint_solve_before_array.v @@ -72,6 +72,17 @@ class ScFirst; // scalar solved before an array } endclass +class DynArr; // dynamic array solved before a scalar + rand int unsigned d[]; + rand int unsigned s; + constraint c { + d.size() == 3; + solve d before s; + foreach (d[i]) d[i] inside {[1:10]}; + s == d[0] + d[1] + d[2]; + } +endclass + module t; OneD o1; TwoD o2; @@ -79,6 +90,7 @@ module t; Chain oc; Que oq; ScFirst osf; + DynArr odn; int ok; initial begin o1 = new; @@ -87,6 +99,7 @@ module t; oc = new; oq = new; osf = new; + odn = new; for (int i = 0; i < 10; ++i) begin ok = o1.randomize(); `checkd(ok, 1); @@ -115,6 +128,11 @@ module t; `checkd(ok, 1); `checkd(osf.a[0], osf.xw); `checkd(osf.a[1], osf.xw + 1); + + ok = odn.randomize(); + `checkd(ok, 1); + `checkd(odn.d.size(), 3); + `checkd(odn.s, odn.d[0] + odn.d[1] + odn.d[2]); end $write("*-* All Finished *-*\n"); $finish; diff --git a/test_regress/t/t_constraint_solve_before_assoc_unsup.out b/test_regress/t/t_constraint_solve_before_assoc_unsup.out new file mode 100644 index 000000000..e737b4c63 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_assoc_unsup.out @@ -0,0 +1,6 @@ +%Error-UNSUPPORTED: t/t_constraint_solve_before_assoc_unsup.v:11:11: Unsupported: 'solve ... before' with associative array + : ... note: In instance 't' + 11 | solve m before s; + | ^ + ... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest +%Error: Exiting due to diff --git a/test_regress/t/t_constraint_solve_before_assoc_unsup.py b/test_regress/t/t_constraint_solve_before_assoc_unsup.py new file mode 100755 index 000000000..38cf36b43 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_assoc_unsup.py @@ -0,0 +1,16 @@ +#!/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('linter') + +test.lint(fails=True, expect_filename=test.golden_filename) + +test.passes() diff --git a/test_regress/t/t_constraint_solve_before_assoc_unsup.v b/test_regress/t/t_constraint_solve_before_assoc_unsup.v new file mode 100644 index 000000000..fb6c852d2 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_assoc_unsup.v @@ -0,0 +1,24 @@ +// 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 + +class Assoc; + rand int unsigned m[int]; + rand int unsigned s; + constraint c { + solve m before s; + m.size() == 2; + } +endclass + +module t; + Assoc o; + initial begin + o = new; + void'(o.randomize()); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule