From f22676eea90590c4104d9b70316cdf398a59ecc8 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Mon, 20 Jul 2026 20:55:49 +0200 Subject: [PATCH] Fix solve-before dropping all soft constraints in randomize() (#7963) --- include/verilated_random.cpp | 59 ++++++++----------- include/verilated_random.h | 2 + .../t/t_randomize_soft_solve_before.py | 21 +++++++ .../t/t_randomize_soft_solve_before.v | 56 ++++++++++++++++++ 4 files changed, 102 insertions(+), 36 deletions(-) create mode 100755 test_regress/t/t_randomize_soft_solve_before.py create mode 100644 test_regress/t/t_randomize_soft_solve_before.v diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 6440067be..e94f64518 100644 --- a/include/verilated_random.cpp +++ b/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(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 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"; diff --git a/include/verilated_random.h b/include/verilated_random.h index 2451adc0d..31135bd97 100644 --- a/include/verilated_random.h +++ b/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" literals named by (get-unsat-assumptions). std::vector readUnsatAssumptions(std::iostream& os); void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints diff --git a/test_regress/t/t_randomize_soft_solve_before.py b/test_regress/t/t_randomize_soft_solve_before.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/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() diff --git a/test_regress/t/t_randomize_soft_solve_before.v b/test_regress/t/t_randomize_soft_solve_before.v new file mode 100644 index 000000000..7802179cc --- /dev/null +++ b/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