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
This commit is contained in:
parent
612d1611b6
commit
4b34bfffcb
|
|
@ -468,16 +468,36 @@ bool VlRandomizer::next(VlRNG& rngr) {
|
||||||
|
|
||||||
const size_t nSoft = m_softConstraints.size();
|
const size_t nSoft = m_softConstraints.size();
|
||||||
bool sat = false;
|
bool sat = false;
|
||||||
for (size_t phase = 0; phase <= nSoft && !sat; ++phase) {
|
if (nSoft > 0) {
|
||||||
const bool hasSoft = (phase < nSoft);
|
// Fast path: try all soft constraints at once
|
||||||
if (hasSoft) {
|
os << "(push 1)\n";
|
||||||
os << "(push 1)\n";
|
for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n";
|
||||||
for (size_t i = phase; i < nSoft; ++i)
|
|
||||||
os << "(assert (= #b1 " << m_softConstraints[i] << "))\n";
|
|
||||||
}
|
|
||||||
os << "(check-sat)\n";
|
os << "(check-sat)\n";
|
||||||
sat = parseSolution(os, /*log=*/phase == nSoft);
|
sat = parseSolution(os, false);
|
||||||
if (!sat && hasSoft) os << "(pop 1)\n";
|
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);
|
||||||
}
|
}
|
||||||
|
|
||||||
if (!sat) {
|
if (!sat) {
|
||||||
|
|
@ -530,6 +550,12 @@ bool VlRandomizer::next(VlRNG& rngr) {
|
||||||
return false; // Should not reach here
|
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) {
|
bool VlRandomizer::parseSolution(std::iostream& os, bool log) {
|
||||||
std::string sat;
|
std::string sat;
|
||||||
do { std::getline(os, sat); } while (sat == "");
|
do { std::getline(os, sat); } while (sat == "");
|
||||||
|
|
|
||||||
|
|
@ -230,6 +230,7 @@ class VlRandomizer VL_NOT_FINAL {
|
||||||
// PRIVATE METHODS
|
// PRIVATE METHODS
|
||||||
void randomConstraint(std::ostream& os, VlRNG& rngr, int bits);
|
void randomConstraint(std::ostream& os, VlRNG& rngr, int bits);
|
||||||
bool parseSolution(std::iostream& file, bool log = false);
|
bool parseSolution(std::iostream& file, bool log = false);
|
||||||
|
bool checkSat(std::iostream& os);
|
||||||
void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints
|
void emitRandcExclusions(std::ostream& os) const; // Emit randc exclusion constraints
|
||||||
void recordRandcValues(); // Record solved randc values for future exclusion
|
void recordRandcValues(); // Record solved randc values for future exclusion
|
||||||
size_t hashConstraints() const;
|
size_t hashConstraints() const;
|
||||||
|
|
|
||||||
|
|
@ -2,8 +2,6 @@
|
||||||
=== Test 1: Valid constraints ===
|
=== Test 1: Valid constraints ===
|
||||||
|
|
||||||
=== Test 2: addr out of range ===
|
=== 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: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'
|
%Warning-UNSATCONSTR: t/t_constraint_unsat.v:16: Unsatisfied constraint: 'if (!randomize() with { addr == a; data == d; }) begin'
|
||||||
Randomization failed.
|
Randomization failed.
|
||||||
|
|
|
||||||
|
|
@ -2,8 +2,6 @@
|
||||||
=== Test 1: Valid constraints ===
|
=== Test 1: Valid constraints ===
|
||||||
|
|
||||||
=== Test 2: addr out of range ===
|
=== 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:11: Unsatisfied constraint
|
||||||
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
|
%Warning-UNSATCONSTR: PSTByA:16: Unsatisfied constraint
|
||||||
Randomization failed.
|
Randomization failed.
|
||||||
|
|
|
||||||
|
|
@ -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()
|
||||||
|
|
@ -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
|
||||||
Loading…
Reference in New Issue