diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 71f719722..e94288fcf 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -998,15 +998,24 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { // Step 3: Solve phase by phase std::map solvedValues; // varName -> SMT value literal + bool needsAllLogic = false; + for (const auto& var : m_vars) { + if (var.second->dimension() == 0) continue; + if (!var.second->hasMatchingElements(m_arr_vars, var.second->name())) { + needsAllLogic = true; + break; + } + } + const char* const logicp = needsAllLogic ? "ALL" : "QF_ABV"; + for (size_t phase = 0; phase < layers.size(); phase++) { const bool isFinalPhase = (phase == layers.size() - 1); std::iostream& os = getSolver(); if (!os) return false; - // Solver session setup os << "(set-option :produce-models true)\n"; - os << "(set-logic QF_ABV)\n"; + os << "(set-logic " << logicp << ")\n"; os << "(define-fun __Vbv ((b Bool)) (_ BitVec 1) (ite b #b1 #b0))\n"; os << "(define-fun __Vbool ((v (_ BitVec 1))) Bool (= #b1 v))\n"; @@ -1021,7 +1030,6 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { os << ")\n"; } - // Pin all previously solved variables for (const auto& entry : solvedValues) { os << "(assert (= " << entry.first << " " << entry.second << "))\n"; } @@ -1072,51 +1080,58 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { auto getValueCmd = [&]() { os << "(get-value ("; for (const auto& varName : layerVars) { - if (m_vars.count(varName)) os << varName << " "; + const auto it = m_vars.find(varName); + if (it->second->dimension() > 0) { + 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->hasMatchingElements(m_arr_vars, it->second->name())) { + it->second->emitGetValue(os); + continue; + } + } + os << varName << " "; } os << "))\n"; }; - // Helper to parse ((name1 value1) (name2 value2) ...) response auto parseGetValue = [&]() -> bool { + // Parse ((name value) ...): one paren-depth counter drives every match. char c; os >> c; // outer '(' - while (true) { - os >> c; - if (c == ')') break; // outer closing - if (c != '(') return false; - std::string name; - os >> name; - - // Read value handling nested parens for (_ bvN W) format - os >> std::ws; - std::string value; - char firstChar; - os.get(firstChar); - if (firstChar == '(') { - // Compound value like (_ bv5 32) - value = "("; - int depth = 1; - while (depth > 0) { - os.get(c); - value += c; - if (c == '(') - depth++; - else if (c == ')') - depth--; + if (c != '(') return false; + int depth = 1; + std::string tokens[2]; + std::string cur; + int fields = 0; + auto flush = [&]() { + if (cur.empty()) return; + if (fields < 2) tokens[fields] = cur; + ++fields; + cur.clear(); + }; + while (depth > 0 && os.get(c)) { + if (c == '(') { + ++depth; + if (depth >= 3) cur += c; + } else if (c == ')') { + --depth; + if (depth >= 2) { + cur += c; + } else if (depth == 1) { + flush(); + if (fields == 2) solvedValues[tokens[0]] = tokens[1]; + fields = 0; + } + } else if (c == ' ' || c == '\t' || c == '\n' || c == '\r') { + if (depth >= 3) { + cur += c; + } else { + flush(); } - // Read closing ')' of the pair - os >> c; } else { - // Atom value like #x00000005 or #b101 - value += firstChar; - while (os.get(c) && c != ')') { value += c; } - // Trim trailing whitespace - const size_t end = value.find_last_not_of(" \t\n\r"); - if (end != std::string::npos) value = value.substr(0, end + 1); + cur += c; } - - solvedValues[name] = value; } return true; }; diff --git a/include/verilated_random.h b/include/verilated_random.h index 7c92c9aa1..8539b8239 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 c0c9e1707..a55cca0d3 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -2165,6 +2165,12 @@ class ConstraintExprVisitor final : public VNVisitor { AstNodeModule* const genModp = VN_AS(m_genp->user2p(), NodeModule); for (AstNodeExpr* lhsp = nodep->lhssp(); lhsp; lhsp = VN_CAST(lhsp->nextp(), NodeExpr)) { + if (VN_IS(lhsp->dtypep()->skipRefp(), AssocArrayDType)) { + lhsp->v3warn(E_UNSUPPORTED, + "Unsupported: 'solve ... before' with associative array"); + VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); + return; + } AstNodeExpr* const lhsTestp = buildSolveBeforeNameExpr(fl, lhsp); if (!lhsTestp) { lhsp->v3fatalSrc("Unexpected expression type in solve...before lhs"); @@ -2173,6 +2179,12 @@ class ConstraintExprVisitor final : public VNVisitor { VL_DO_DANGLING(lhsTestp->deleteTree(), lhsTestp); for (AstNodeExpr* rhsp = nodep->rhssp(); rhsp; rhsp = VN_CAST(rhsp->nextp(), NodeExpr)) { + if (VN_IS(rhsp->dtypep()->skipRefp(), AssocArrayDType)) { + rhsp->v3warn(E_UNSUPPORTED, + "Unsupported: 'solve ... before' with associative array"); + VL_DO_DANGLING(nodep->unlinkFrBack()->deleteTree(), nodep); + return; + } AstNodeExpr* const rhsNamep = buildSolveBeforeNameExpr(fl, rhsp); if (!rhsNamep) { rhsp->v3fatalSrc("Unexpected expression type in solve...before rhs"); diff --git a/test_regress/t/t_constraint_solve_before_array.py b/test_regress/t/t_constraint_solve_before_array.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_array.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_solve_before_array.v b/test_regress/t/t_constraint_solve_before_array.v new file mode 100644 index 000000000..60db27107 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_array.v @@ -0,0 +1,140 @@ +// 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); +// verilog_format: on + +// solve...before over array rand variables: each solved layer is pinned +// per element so the phased solve round-trips. +class OneD; + rand int unsigned a[2]; + rand int unsigned b[2]; + constraint c { + solve a before b; + foreach (b[i]) b[i] == a[i] + 1; + } +endclass + +class TwoD; + rand int unsigned a[2][2]; + rand int unsigned b[2][2]; + constraint c { + solve a before b; + foreach (b[i, j]) b[i][j] == a[i][j] + 1; + } +endclass + +class Mul; // the rv_timer ticks_c shape: mul across a solved layer + rand int unsigned prescale[2]; + rand int unsigned ticks[2]; + constraint c { + solve prescale before ticks; + foreach (ticks[i]) (ticks[i] * (prescale[i] + 1)) <= 5000; + } +endclass + +class Chain; // three-layer chain + rand int unsigned a[2]; + rand int unsigned b[2]; + rand int unsigned d[2]; + constraint c { + solve a before b; + solve b before d; + foreach (a[i]) a[i] inside {[1:10]}; + foreach (b[i]) b[i] == a[i] * 2; + foreach (d[i]) d[i] == b[i] + a[i]; + } +endclass + +class Que; // dynamic container solved before a scalar + rand int unsigned q[$]; + rand int unsigned s; + constraint c { + q.size() == 3; + solve q before s; + foreach (q[i]) q[i] inside {[1:10]}; + s == q[0] + q[1] + q[2]; + } +endclass + +class ScFirst; // scalar solved before an array + rand int unsigned xw; + rand int unsigned a[2]; + constraint c { + solve xw before a; + xw inside {[1:5]}; + foreach (a[i]) a[i] == xw + i; + } +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; + Mul om; + Chain oc; + Que oq; + ScFirst osf; + DynArr odn; + int ok; + initial begin + o1 = new; + o2 = new; + om = new; + oc = new; + oq = new; + osf = new; + odn = new; + for (int i = 0; i < 10; ++i) begin + ok = o1.randomize(); + `checkd(ok, 1); + `checkd(o1.b[0], o1.a[0] + 1); + `checkd(o1.b[1], o1.a[1] + 1); + + ok = o2.randomize(); + `checkd(ok, 1); + `checkd(o2.b[0][0], o2.a[0][0] + 1); + `checkd(o2.b[1][1], o2.a[1][1] + 1); + + ok = om.randomize(); + `checkd(ok, 1); + if ((om.ticks[0] * (om.prescale[0] + 1)) > 5000) `checkd(0, 1); + + ok = oc.randomize(); + `checkd(ok, 1); + `checkd(oc.b[0], oc.a[0] * 2); + `checkd(oc.d[1], oc.b[1] + oc.a[1]); + + ok = oq.randomize(); + `checkd(ok, 1); + `checkd(oq.s, oq.q[0] + oq.q[1] + oq.q[2]); + + ok = osf.randomize(); + `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; + end +endmodule 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