From 4b34bfffcb88c232af45d1f5c0071ff06bb0b320 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Wed, 18 Mar 2026 10:15:50 +0100 Subject: [PATCH] Fix soft constraint relaxation dropping compatible constraints (#7271) * Fix soft constraint relaxation dropping compatible constraints * patch changes the soft handle ordering so update the out files --- include/verilated_random.cpp | 44 ++++++++++++++---- include/verilated_random.h | 1 + test_regress/t/t_constraint_unsat.out | 2 - .../t/t_constraint_unsat_protect_ids.out | 2 - test_regress/t/t_randomize_soft_relaxation.py | 21 +++++++++ test_regress/t/t_randomize_soft_relaxation.v | 45 +++++++++++++++++++ 6 files changed, 102 insertions(+), 13 deletions(-) create mode 100755 test_regress/t/t_randomize_soft_relaxation.py create mode 100644 test_regress/t/t_randomize_soft_relaxation.v diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index d7f4225b2..afc5e3eb1 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -468,16 +468,36 @@ bool VlRandomizer::next(VlRNG& rngr) { const size_t nSoft = m_softConstraints.size(); bool sat = false; - for (size_t phase = 0; phase <= nSoft && !sat; ++phase) { - const bool hasSoft = (phase < nSoft); - if (hasSoft) { - os << "(push 1)\n"; - for (size_t i = phase; i < nSoft; ++i) - os << "(assert (= #b1 " << m_softConstraints[i] << "))\n"; - } + 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, /*log=*/phase == nSoft); - if (!sat && hasSoft) os << "(pop 1)\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); } if (!sat) { @@ -530,6 +550,12 @@ bool VlRandomizer::next(VlRNG& rngr) { return false; // Should not reach here } +bool VlRandomizer::checkSat(std::iostream& os) { + std::string result; + do { std::getline(os, result); } while (result.empty()); + return result == "sat"; +} + bool VlRandomizer::parseSolution(std::iostream& os, bool log) { std::string sat; do { std::getline(os, sat); } while (sat == ""); diff --git a/include/verilated_random.h b/include/verilated_random.h index 8fba88e2f..f45e7c8de 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -230,6 +230,7 @@ class VlRandomizer VL_NOT_FINAL { // PRIVATE METHODS void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); bool parseSolution(std::iostream& file, bool log = false); + bool checkSat(std::iostream& os); void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints void recordRandcValues(); // Record solved randc values for future exclusion size_t hashConstraints() const; diff --git a/test_regress/t/t_constraint_unsat.out b/test_regress/t/t_constraint_unsat.out index 3cc41487e..57dda34eb 100644 --- a/test_regress/t/t_constraint_unsat.out +++ b/test_regress/t/t_constraint_unsat.out @@ -2,8 +2,6 @@ === Test 1: Valid constraints === === Test 2: addr out of range === -%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin' -%Warning-UNSATCONSTR: t/t_constraint_unsat.v:12: Unsatisfied constraint: 'constraint data_range { data > 10 && data < 200; }' %Warning-UNSATCONSTR: t/t_constraint_unsat.v:11: Unsatisfied constraint: 'constraint addr_range { addr < 127; }' %Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin' Randomization failed. diff --git a/test_regress/t/t_constraint_unsat_protect_ids.out b/test_regress/t/t_constraint_unsat_protect_ids.out index 8677a573f..0b458dbfd 100644 --- a/test_regress/t/t_constraint_unsat_protect_ids.out +++ b/test_regress/t/t_constraint_unsat_protect_ids.out @@ -2,8 +2,6 @@ === Test 1: Valid constraints === === Test 2: addr out of range === -%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint -%Warning-UNSATCONSTR: PSTByA:12: Unsatisfied constraint %Warning-UNSATCONSTR: PSTByA:11: Unsatisfied constraint %Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint Randomization failed. diff --git a/test_regress/t/t_randomize_soft_relaxation.py b/test_regress/t/t_randomize_soft_relaxation.py new file mode 100755 index 000000000..db1adb3f9 --- /dev/null +++ b/test_regress/t/t_randomize_soft_relaxation.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_relaxation.v b/test_regress/t/t_randomize_soft_relaxation.v new file mode 100644 index 000000000..5ea1bff17 --- /dev/null +++ b/test_regress/t/t_randomize_soft_relaxation.v @@ -0,0 +1,45 @@ +// 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); +`define check_range(gotv,minv,maxv) do if ((gotv) < (minv) || (gotv) > (maxv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d-%0d\n", `__FILE__,`__LINE__, (gotv), (minv), (maxv)); `stop; end while(0); +// verilog_format: on + +// Soft constraint relaxation must preserve the maximum compatible set. +// When soft[1] conflicts with soft[2], a correct algorithm should still +// keep soft[0] if it is compatible with soft[2]. +// +// soft[0]: b > 100 (low priority, COMPATIBLE with soft[2]) +// soft[1]: a == 30 (mid priority, CONFLICTS with soft[2]) +// soft[2]: a == 80 (high priority, should win over soft[1]) +// +// Correct result: a == 80, b > 100 (soft[0] and soft[2] both kept) +// Bug result: a == 80, b unconstrained (soft[0] wrongly dropped) + +class SoftRelax; + rand bit [7:0] a; + rand bit [7:0] b; + constraint c_hard { a < 8'd200; b < 8'd200; } + constraint c_soft0 { soft b > 8'd100; } + constraint c_soft1 { soft a == 8'd30; } + constraint c_soft2 { soft a == 8'd80; } +endclass + +module t; + initial begin + SoftRelax obj; + obj = new; + repeat (20) begin + `checkd(obj.randomize(), 1) + `checkd(obj.a, 8'd80) + `check_range(obj.b, 8'd101, 8'd199) + end + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule