Fix solve-before dropping all soft constraints in randomize() (#7963)

include/verilated_random.cpp

@@ -524,9 +524,6 @@ bool VlRandomizer::next(VlRNG& rngr) {
         std::iostream& os = getSolver();
         if (!os) return false;
 
-        // Soft constraint relaxation (IEEE 1800-2023 18.5.13, last-wins priority):
-        // Try hard + soft[0..N-1], then hard + soft[1..N-1], ..., then hard only.
-        // First SAT phase wins. If hard-only is UNSAT, report via unsat-core.
         os << "(set-option :produce-models true)\n";
         // Lets the scalar pin path learn which free-bit assumptions conflict.
         os << "(set-option :produce-unsat-assumptions true)\n";
@@ -560,39 +557,9 @@ bool VlRandomizer::next(VlRNG& rngr) {
         // trivially UNSAT after the first cycle.
         if (!m_checkOnly) emitRandcExclusions(os);
 
-        const size_t nSoft = m_softConstraints.size();
-        bool sat = false;
-        if (nSoft > 0) {
-            // Fast path: try all soft constraints at once
-            os << "(push 1)\n";
-            for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n";
-            os << "(check-sat)\n";
-            sat = parseSolution(os, false);
-            if (!sat) {
-                // Some soft constraints conflict. Incrementally add from back
-                // (highest priority first), keeping only compatible ones.
-                // This preserves the maximum set of compatible soft constraints.
-                os << "(pop 1)\n";
-                for (int i = static_cast<int>(nSoft) - 1; i >= 0; --i) {
-                    os << "(push 1)\n";
-                    os << "(assert (= #b1 " << m_softConstraints[i] << "))\n";
-                    os << "(check-sat)\n";
-                    if (checkSat(os)) {
-                        // Compatible -- keep this push level
-                    } else {
-                        // Incompatible -- remove this soft constraint
-                        os << "(pop 1)\n";
-                    }
-                }
-                // Read solution with remaining compatible soft constraints
-                os << "(check-sat)\n";
-                sat = parseSolution(os, false);
-            }
-        } else {
-            // No soft constraints -- hard-only
-            os << "(check-sat)\n";
-            sat = parseSolution(os, false);
-        }
+        relaxSoftConstraints(os);
+        os << "(check-sat)\n";
+        bool sat = parseSolution(os, false);
 
         if (!sat) {
             os << "(reset)\n";
@@ -708,6 +675,23 @@ bool VlRandomizer::checkSat(std::iostream& os) {
     return result == "sat";
 }
 
+void VlRandomizer::relaxSoftConstraints(std::iostream& os) {
+    // Re-add softs highest-priority first, dropping incompatible ones.
+    const size_t nSoft = m_softConstraints.size();
+    if (nSoft == 0) return;
+    os << "(push 1)\n";
+    for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n";
+    os << "(check-sat)\n";
+    if (checkSat(os)) return;
+    os << "(pop 1)\n";
+    for (auto it = m_softConstraints.rbegin(); it != m_softConstraints.rend(); ++it) {
+        os << "(push 1)\n";
+        os << "(assert (= #b1 " << *it << "))\n";
+        os << "(check-sat)\n";
+        if (!checkSat(os)) os << "(pop 1)\n";
+    }
+}
+
 std::vector<int> VlRandomizer::readUnsatAssumptions(std::iostream& os) {
     os << "(get-unsat-assumptions)\n";
     std::string line;
@@ -1042,6 +1026,9 @@ bool VlRandomizer::nextPhased(VlRNG& rngr) {
         // Randc: exclude previously used values
         emitRandcExclusions(os);
 
+        // Soft constraints participate in every phase, priority-ordered.
+        relaxSoftConstraints(os);
+
         // Initial check-sat WITHOUT diversity (guaranteed sat if constraints are consistent)
         os << "(check-sat)\n";
 

include/verilated_random.h

@@ -260,6 +260,8 @@ class VlRandomizer VL_NOT_FINAL {
     void randomConstraint(std::ostream& os, VlRNG& rngr, int bits);
     bool parseSolution(std::iostream& os, bool log = false);
     bool checkSat(std::iostream& os);
+    // Assert the maximal compatible soft-constraint set onto the open session.
+    void relaxSoftConstraints(std::iostream& os);
     // Indices of the "a<N>" literals named by (get-unsat-assumptions).
     std::vector<int> readUnsatAssumptions(std::iostream& os);
     void emitRandcExclusions(std::ostream& os) const;  // Emit randc exclusion constraints

test_regress/t/t_randomize_soft_solve_before.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_randomize_soft_solve_before.v

@@ -0,0 +1,56 @@
+// 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
+
+class solve_before_soft_c;
+  rand bit sel;
+  rand int unsigned m;
+  rand int unsigned x;
+  constraint m_soft {soft m == 7;}
+  constraint sb_cons {
+    solve sel before x;
+    if (sel)
+    x == 0;
+    else
+    x inside {[1 : 100]};
+  }
+endclass
+
+class conflicting_soft_c;
+  rand bit sel;
+  rand int unsigned a;
+  rand int unsigned b;
+  constraint a_soft3 {soft a == 3;}
+  constraint a_soft9 {soft a == 9;}
+  constraint sb_cons {
+    solve sel before b;
+    if (sel)
+    b == 0;
+    else
+    b inside {[1 : 100]};
+  }
+endclass
+
+module t;
+  initial begin
+    static solve_before_soft_c o1 = new();
+    static conflicting_soft_c o2 = new();
+    repeat (20) begin
+      `checkd(o1.randomize(), 1)
+      `checkd(o1.m, 32'd7)
+    end
+    repeat (20) begin
+      `checkd(o2.randomize(), 1)
+      `checkd(o2.a, 32'd9)
+    end
+    $write("*-* All Finished *-*\n");
+    $finish;
+  end
+endmodule