From 648169b6f48f2db900a24d42dbf25d2ba662c96d Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Sat, 4 Jul 2026 10:47:46 +0200 Subject: [PATCH] Fix solve-before over array variables failing randomization --- include/verilated_random.cpp | 59 +++++++++- .../t/t_constraint_solve_before_array.py | 21 ++++ .../t/t_constraint_solve_before_array.v | 105 ++++++++++++++++++ 3 files changed, 181 insertions(+), 4 deletions(-) create mode 100755 test_regress/t/t_constraint_solve_before_array.py create mode 100644 test_regress/t/t_constraint_solve_before_array.v diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 71f719722..725368681 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -1006,7 +1006,19 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { // Solver session setup os << "(set-option :produce-models true)\n"; - os << "(set-logic QF_ABV)\n"; + // Arrays with recorded elements are pinned per element (plain bit-vector + // literals, below) and round-trip under QF_ABV. Only a container whose + // element table is not enumerable falls back to a whole-array pin, whose + // model text ("(as const ...)") the solver accepts only under ALL. + bool hasNonEnumArray = false; + for (const auto& var : m_vars) { + if (var.second->dimension() > 0 + && var.second->countMatchingElements(m_arr_vars, var.second->name()) == 0) { + hasNonEnumArray = true; + break; + } + } + os << "(set-logic " << (hasNonEnumArray ? "ALL" : "QF_ABV") << ")\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,8 +1033,13 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { os << ")\n"; } - // Pin all previously solved variables + // Pin all previously solved variables. Model text naming solver-internal + // terms ("(_ as-array f)", "(lambda ...)") cannot be re-asserted as + // input; skipping such a pin is safe because ordering never changes the + // solution space (IEEE 1800-2023 18.5.9), it only weakens the bias. for (const auto& entry : solvedValues) { + if (entry.second.find("as-array") != std::string::npos) continue; + if (entry.second.find("(lambda") != std::string::npos) continue; os << "(assert (= " << entry.first << " " << entry.second << "))\n"; } @@ -1072,7 +1089,24 @@ 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 == m_vars.end()) continue; + if (it->second->dimension() > 0) { + auto arrVarsp = std::make_shared(m_arr_vars); + it->second->setArrayInfo(arrVarsp); + // Enumerable (fixed-size) arrays: query each element via a + // (select ...) so the value is a plain bit-vector literal + // that round-trips as a QF_ABV pin, avoiding array model + // text ("(as const ...)" / "(_ as-array ...)"). + if (it->second->countMatchingElements(m_arr_vars, it->second->name()) + > 0) { + it->second->emitGetValue(os); + continue; + } + } + // Scalars, and dynamic containers whose element table is empty, + // query the whole term (pinned via the ALL session above). + os << varName << " "; } os << "))\n"; }; @@ -1085,8 +1119,25 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) { os >> c; if (c == ')') break; // outer closing if (c != '(') return false; + // The queried term is echoed back verbatim as the pair's LHS: + // a bare name for scalars, a balanced "(select arr idx)" for + // array elements. Keep it as the pin target either way. + os >> std::ws; std::string name; - os >> name; + if (os.peek() == '(') { + int ndepth = 0; + char nc; + do { + os.get(nc); + name += nc; + if (nc == '(') + ++ndepth; + else if (nc == ')') + --ndepth; + } while (ndepth > 0 && os); + } else { + os >> name; + } // Read value handling nested parens for (_ bvN W) format os >> std::ws; 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..75657c2b1 --- /dev/null +++ b/test_regress/t/t_constraint_solve_before_array.v @@ -0,0 +1,105 @@ +// 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 + +module t; + OneD o1; + TwoD o2; + Mul om; + Chain oc; + Que oq; + int ok; + initial begin + o1 = new; + o2 = new; + om = new; + oc = new; + oq = 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]); + end + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule