Fix solve-before over array variables failing randomization

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<const ArrayInfoMap>(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;

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()

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