Merge 01cbc51b73 into 742c0b134c
This commit is contained in:
commit
ff588f336f
|
|
@ -371,25 +371,50 @@ bool VlRandomizer::next(VlRNG& rngr) {
|
|||
std::iostream& os = getSolver();
|
||||
if (!os) return false;
|
||||
|
||||
os << "(set-option :produce-models true)\n";
|
||||
os << "(set-logic 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";
|
||||
for (const auto& var : m_vars) {
|
||||
if (var.second->dimension() > 0) {
|
||||
auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
|
||||
var.second->setArrayInfo(arrVarsp);
|
||||
// Helper lambda to emit common setup (options, logic, functions, vars)
|
||||
auto emitSetup = [&]() {
|
||||
os << "(set-option :produce-models true)\n";
|
||||
os << "(set-logic 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";
|
||||
for (const auto& var : m_vars) {
|
||||
if (var.second->dimension() > 0) {
|
||||
auto arrVarsp = std::make_shared<const ArrayInfoMap>(m_arr_vars);
|
||||
var.second->setArrayInfo(arrVarsp);
|
||||
}
|
||||
os << "(declare-fun " << var.first << " () ";
|
||||
var.second->emitType(os);
|
||||
os << ")\n";
|
||||
}
|
||||
os << "(declare-fun " << var.first << " () ";
|
||||
var.second->emitType(os);
|
||||
os << ")\n";
|
||||
}
|
||||
for (const std::string& constraint : m_constraints) {
|
||||
};
|
||||
|
||||
// Helper lambda to emit hard constraints
|
||||
auto emitHardConstraints = [&]() {
|
||||
for (const std::string& constraint : m_constraints) {
|
||||
os << "(assert (= #b1 " << constraint << "))\n";
|
||||
}
|
||||
};
|
||||
|
||||
emitSetup();
|
||||
emitHardConstraints();
|
||||
|
||||
// Also add soft constraints in the first pass
|
||||
for (const std::string& constraint : m_softConstraints) {
|
||||
os << "(assert (= #b1 " << constraint << "))\n";
|
||||
}
|
||||
os << "(check-sat)\n";
|
||||
|
||||
bool sat = parseSolution(os);
|
||||
|
||||
// If unsatisfiable and we have soft constraints, retry with only hard constraints
|
||||
if (!sat && !m_softConstraints.empty()) {
|
||||
os << "(reset)\n";
|
||||
emitSetup();
|
||||
emitHardConstraints();
|
||||
os << "(check-sat)\n";
|
||||
sat = parseSolution(os);
|
||||
}
|
||||
|
||||
if (!sat) {
|
||||
os << "(reset)\n";
|
||||
return false;
|
||||
|
|
@ -505,13 +530,19 @@ void VlRandomizer::hard(std::string&& constraint) {
|
|||
m_constraints.emplace_back(std::move(constraint));
|
||||
}
|
||||
|
||||
void VlRandomizer::soft(std::string&& constraint) {
|
||||
m_softConstraints.emplace_back(std::move(constraint));
|
||||
}
|
||||
|
||||
void VlRandomizer::clearConstraints() {
|
||||
m_constraints.clear();
|
||||
m_softConstraints.clear();
|
||||
// Keep m_vars for class member randomization
|
||||
}
|
||||
|
||||
void VlRandomizer::clearAll() {
|
||||
m_constraints.clear();
|
||||
m_softConstraints.clear();
|
||||
m_vars.clear();
|
||||
}
|
||||
|
||||
|
|
@ -520,6 +551,7 @@ void VlRandomizer::dump() const {
|
|||
for (const auto& var : m_vars) {
|
||||
VL_PRINTF("Variable (%d): %s\n", var.second->width(), var.second->name().c_str());
|
||||
}
|
||||
for (const std::string& c : m_constraints) VL_PRINTF("Constraint: %s\n", c.c_str());
|
||||
for (const std::string& c : m_constraints) VL_PRINTF("Hard constraint: %s\n", c.c_str());
|
||||
for (const std::string& c : m_softConstraints) VL_PRINTF("Soft constraint: %s\n", c.c_str());
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -199,7 +199,8 @@ public:
|
|||
// Object holding constraints and variable references.
|
||||
class VlRandomizer VL_NOT_FINAL {
|
||||
// MEMBERS
|
||||
std::vector<std::string> m_constraints; // Solver-dependent constraints
|
||||
std::vector<std::string> m_constraints; // Hard constraints (must be satisfied)
|
||||
std::vector<std::string> m_softConstraints; // Soft constraints (optional, best-effort)
|
||||
std::map<std::string, std::shared_ptr<const VlRandomVar>> m_vars; // Solver-dependent
|
||||
// variables
|
||||
ArrayInfoMap m_arr_vars; // Tracks each element in array structures for iteration
|
||||
|
|
@ -570,6 +571,7 @@ public:
|
|||
}
|
||||
|
||||
void hard(std::string&& constraint);
|
||||
void soft(std::string&& constraint);
|
||||
void clearConstraints();
|
||||
void clearAll(); // Clear both constraints and variables
|
||||
void set_randmode(const VlQueue<CData>& randmode) { m_randmodep = &randmode; }
|
||||
|
|
|
|||
|
|
@ -787,6 +787,7 @@ public:
|
|||
RANDOMIZER_CLEARCONSTRAINTS,
|
||||
RANDOMIZER_CLEARALL,
|
||||
RANDOMIZER_HARD,
|
||||
RANDOMIZER_SOFT,
|
||||
RANDOMIZER_WRITE_VAR,
|
||||
RNG_GET_RANDSTATE,
|
||||
RNG_SET_RANDSTATE,
|
||||
|
|
@ -916,6 +917,7 @@ inline std::ostream& operator<<(std::ostream& os, const VCMethod& rhs) {
|
|||
{RANDOMIZER_CLEARCONSTRAINTS, "clearConstraints", false}, \
|
||||
{RANDOMIZER_CLEARALL, "clearAll", false}, \
|
||||
{RANDOMIZER_HARD, "hard", false}, \
|
||||
{RANDOMIZER_SOFT, "soft", false}, \
|
||||
{RANDOMIZER_WRITE_VAR, "write_var", false}, \
|
||||
{RNG_GET_RANDSTATE, "__Vm_rng.get_randstate", true}, \
|
||||
{RNG_SET_RANDSTATE, "__Vm_rng.set_randstate", false}, \
|
||||
|
|
|
|||
|
|
@ -1330,12 +1330,14 @@ class ConstraintExprVisitor final : public VNVisitor {
|
|||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||
return;
|
||||
}
|
||||
// Only hard constraints are currently supported
|
||||
// Use RANDOMIZER_SOFT for soft constraints, RANDOMIZER_HARD for hard constraints
|
||||
const VCMethod method
|
||||
= nodep->isSoft() ? VCMethod::RANDOMIZER_SOFT : VCMethod::RANDOMIZER_HARD;
|
||||
AstCMethodHard* const callp = new AstCMethodHard{
|
||||
nodep->fileline(),
|
||||
new AstVarRef{nodep->fileline(), VN_AS(m_genp->user2p(), NodeModule), m_genp,
|
||||
VAccess::READWRITE},
|
||||
VCMethod::RANDOMIZER_HARD, nodep->exprp()->unlinkFrBack()};
|
||||
method, nodep->exprp()->unlinkFrBack()};
|
||||
callp->dtypeSetVoid();
|
||||
nodep->replaceWith(callp->makeStmt());
|
||||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||
|
|
|
|||
|
|
@ -0,0 +1,21 @@
|
|||
#!/usr/bin/env python3
|
||||
# DESCRIPTION: Verilator: Verilog Test driver/expect definition
|
||||
#
|
||||
# Copyright 2025 by Wilson Snyder. 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-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,113 @@
|
|||
// DESCRIPTION: Verilator: Verilog Test module
|
||||
//
|
||||
// This file ONLY is placed under the Creative Commons Public Domain, for
|
||||
// any use, without warranty, 2025 by Wilson Snyder.
|
||||
// SPDX-License-Identifier: CC0-1.0
|
||||
|
||||
// Test soft constraint support.
|
||||
// Soft constraints should be satisfied when possible, but dropped when
|
||||
// they conflict with hard constraints.
|
||||
|
||||
class soft_constraint_basic;
|
||||
rand bit [7:0] value;
|
||||
|
||||
// Soft constraint: prefer value in range [10:20]
|
||||
constraint c_soft { soft value inside {[10:20]}; }
|
||||
|
||||
function new();
|
||||
value = 0;
|
||||
endfunction
|
||||
endclass
|
||||
|
||||
class soft_constraint_conflict;
|
||||
rand bit [7:0] value;
|
||||
|
||||
// Hard constraint: value must be > 100
|
||||
constraint c_hard { value > 100; }
|
||||
|
||||
// Soft constraint: prefer value < 50 (conflicts with hard!)
|
||||
constraint c_soft { soft value < 50; }
|
||||
|
||||
function new();
|
||||
value = 0;
|
||||
endfunction
|
||||
|
||||
function void check();
|
||||
// Hard constraint must always be satisfied
|
||||
if (!(value > 100)) begin
|
||||
$display("ERROR: Hard constraint violated! value=%0d should be > 100", value);
|
||||
$stop;
|
||||
end
|
||||
endfunction
|
||||
endclass
|
||||
|
||||
class soft_constraint_multiple;
|
||||
rand bit [7:0] a;
|
||||
rand bit [7:0] b;
|
||||
|
||||
// Hard constraint
|
||||
constraint c_hard { a + b == 100; }
|
||||
|
||||
// Soft constraints that can be satisfied together with hard
|
||||
constraint c_soft1 { soft a > 30; }
|
||||
constraint c_soft2 { soft b > 30; }
|
||||
|
||||
function new();
|
||||
a = 0;
|
||||
b = 0;
|
||||
endfunction
|
||||
|
||||
function void check();
|
||||
// Hard constraint must always be satisfied
|
||||
if (a + b != 100) begin
|
||||
$display("ERROR: Hard constraint violated! a=%0d + b=%0d != 100", a, b);
|
||||
$stop;
|
||||
end
|
||||
endfunction
|
||||
endclass
|
||||
|
||||
module t;
|
||||
soft_constraint_basic obj_basic;
|
||||
soft_constraint_conflict obj_conflict;
|
||||
soft_constraint_multiple obj_multiple;
|
||||
|
||||
initial begin
|
||||
// Test basic soft constraint
|
||||
obj_basic = new();
|
||||
repeat(5) begin
|
||||
if (obj_basic.randomize() != 1) begin
|
||||
$display("ERROR: randomize() failed for basic");
|
||||
$stop;
|
||||
end
|
||||
// Soft constraint suggests [10:20], but any value is acceptable
|
||||
$display("Basic: value=%0d", obj_basic.value);
|
||||
end
|
||||
|
||||
// Test soft constraint that conflicts with hard constraint
|
||||
// Randomization should succeed by dropping soft constraint
|
||||
obj_conflict = new();
|
||||
repeat(5) begin
|
||||
if (obj_conflict.randomize() != 1) begin
|
||||
$display("ERROR: randomize() failed for conflict case");
|
||||
$stop;
|
||||
end
|
||||
obj_conflict.check();
|
||||
$display("Conflict: value=%0d (must be > 100)", obj_conflict.value);
|
||||
end
|
||||
|
||||
// Test multiple soft constraints
|
||||
obj_multiple = new();
|
||||
repeat(5) begin
|
||||
if (obj_multiple.randomize() != 1) begin
|
||||
$display("ERROR: randomize() failed for multiple");
|
||||
$stop;
|
||||
end
|
||||
obj_multiple.check();
|
||||
$display("Multiple: a=%0d, b=%0d (sum=%0d)", obj_multiple.a, obj_multiple.b,
|
||||
obj_multiple.a + obj_multiple.b);
|
||||
end
|
||||
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
endmodule
|
||||
Loading…
Reference in New Issue