mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-14 19:25:40 +00:00
Code Activity

Merge 3f8433b52d into dddf137888

Browse source
This commit is contained in:
nella 2026-07-13 15:05:50 +02:00 • committed by GitHub
commit 95bdc88938
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 313 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

19
libs/ezsat/ezminisat.cc
View file

@ -104,6 +104,8 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
preSolverCallback();
solverTimeoutStatus = false;
solverPropLimitStatus = false;
solverProps = 0;
if (0) {
contradiction:
@ -201,7 +203,21 @@ contradiction:
}
#endif
bool foundSolution = minisatSolver->solve(assumps);
uint64_t solverPropsBefore = minisatSolver->propagations;
bool foundSolution;
if (solverPropLimit > 0) {
minisatSolver->setPropBudget(solverPropLimit);
Minisat::lbool res = minisatSolver->solveLimited(assumps);
minisatSolver->budgetOff();
if (Minisat::toInt(res) == 2) // l_Undef: propagation budget exhausted
solverPropLimitStatus = true;
foundSolution = (Minisat::toInt(res) == 0); // l_True
} else {
foundSolution = minisatSolver->solve(assumps);
}
solverProps = minisatSolver->propagations - solverPropsBefore;
#if defined(HAS_ALARM)
if (solverTimeout > 0) {
@ -210,6 +226,7 @@ contradiction:
alarm(0);
sigaction(SIGALRM, &old_sig_action, NULL);
alarm(old_alarm_timeout);
minisatSolver->clearInterrupt();
}
#endif

3
libs/ezsat/ezsat.cc
View file

@ -55,6 +55,9 @@ ezSAT::ezSAT()
solverTimeout = 0;
solverTimeoutStatus = false;
solverPropLimit = 0;
solverPropLimitStatus = false;
solverProps = 0;
literal("CONST_TRUE");
literal("CONST_FALSE");

16
libs/ezsat/ezsat.h
View file

@ -79,6 +79,9 @@ protected:
public:
int solverTimeout;
bool solverTimeoutStatus;
int64_t solverPropLimit;
bool solverPropLimitStatus;
int64_t solverProps;
ezSAT();
virtual ~ezSAT();
@ -157,6 +160,19 @@ public:
return solverTimeoutStatus;
}
void setSolverPropLimit(int64_t newPropLimit) {
solverPropLimit = newPropLimit;
}
bool getSolverPropLimitStatus() {
return solverPropLimitStatus;
}
// propagations spent by the most recent solve() call
int64_t getSolverProps() {
return solverProps;
}
// manage CNF (usually only accessed by SAT solvers)
virtual void clear();

344
passes/opt/opt_dff.cc
View file

@ -143,6 +143,56 @@ struct OptDffWorker
std::vector<Cell *> dff_cells;
// Solver effort budget shared by run_constbits and run_eqbits, per module
static constexpr int64_t sat_import_cell_cost = 100;
static constexpr int sat_batch_cells = 10000;
int64_t sat_effort = 0;
int64_t sat_effort_left = 0;
bool sat_budget_out = false;
void sat_budget_exceeded()
{
if (!sat_budget_out)
log_warning("opt_dff -sat: effort limit exceeded in module %s, skipping remaining "
"sat proofs (scratchpad option 'opt_dff.sat_effort').\n", log_id(module));
sat_budget_out = true;
}
bool sat_budget_spent()
{
if (sat_budget_out)
return true;
if (sat_effort > 0 && sat_effort_left <= 0) {
sat_budget_exceeded();
return true;
}
return false;
}
int solve_budgeted(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
std::vector<bool> &modelVals, const std::vector<int> &assumptions)
{
// SAT = 1
// UNSAT = 0
// effort limit reached = -1 (can't be treated as UNSAT)
if (sat_effort > 0)
cap = (cap > 0) ? min(cap, sat_effort_left) : sat_effort_left;
qcsat.ez->setSolverPropLimit(cap);
bool sat_res = qcsat.ez->solve(modelExprs, modelVals, assumptions);
if (sat_effort > 0)
sat_effort_left -= qcsat.ez->getSolverProps();
if (!sat_res && qcsat.ez->getSolverPropLimitStatus())
return -1;
return sat_res ? 1 : 0;
}
void charge_import(QuickConeSat &qcsat, int64_t &cells_charged)
{
if (sat_effort > 0)
sat_effort_left -= (GetSize(qcsat.imported_cells) - cells_charged) * sat_import_cell_cost;
cells_charged = GetSize(qcsat.imported_cells);
}
bool is_active(SigBit sig, bool pol) const {
return sig == (pol ? State::S1 : State::S0);
}
@ -197,6 +247,9 @@ struct OptDffWorker
OptDffWorker(const OptDffOptions &opt, Module *mod)
: opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod)
{
sat_effort = module->design->scratchpad_get_int("opt_dff.sat_effort", 1000000000);
sat_effort_left = sat_effort;
// Gathering two kinds of information here for every sigmapped SigBit:
// - bitusers: how many users it has (muxes will only be merged into FFs if the FF is the only user)
// - bit2mux: the mux cell and bit index that drives it, if any
@ -885,25 +938,6 @@ struct OptDffWorker
return did_something;
}
bool prove_const_with_sat(QuickConeSat &qcsat, ModWalker &modwalker, SigBit q, SigBit d, State val)
{
// Trivial non-const cases
if (!modwalker.has_drivers(d))
return false;
if (val != State::S0 && val != State::S1)
return false;
int init_sat_pi = qcsat.importSigBit(val);
int q_sat_pi = qcsat.importSigBit(q);
int d_sat_pi = qcsat.importSigBit(d);
qcsat.prepare();
// If no counterexample exists, FF is constant
return !qcsat.ez->solve(
qcsat.ez->IFF(q_sat_pi, init_sat_pi),
qcsat.ez->NOT(qcsat.ez->IFF(d_sat_pi, init_sat_pi)));
}
State check_constbit(FfData &ff, int i)
{
State val = ff.val_init[i];
@ -919,83 +953,234 @@ struct OptDffWorker
return val;
}
// One FF bit whose constness needs SAT proofs; each target is a non-const input (D and/or AD)
// that must be shown eq to val
struct ConstTarget {
SigBit sig;
int lit = -1;
bool proven = false;
};
struct ConstObligation {
Cell *cell;
int idx;
State val;
SigBit q;
int q_lit = -1;
bool dropped = false;
std::vector<ConstTarget> targets;
};
void commit_const(dict<Cell *, pool<int>> &const_bits, Cell *cell, int i, SigBit q, State val)
{
log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n",
val == State::S1 ? 1 : 0, i, cell, cell->type.unescape(), module);
initvals.remove_init(q);
module->connect(q, val);
const_bits[cell].insert(i);
}
bool add_const_target(ModWalker &modwalker, ConstObligation &ob, SigBit sig)
{
if (!opt.sat || (ob.val != State::S0 && ob.val != State::S1) || !modwalker.has_drivers(sig))
return false;
ob.targets.push_back(ConstTarget{sig});
return true;
}
bool run_constbits()
{
// Find FFs that are provably constant
ModWalker modwalker(module->design, module);
QuickConeSat qcsat(modwalker);
std::vector<RTLIL::Cell*> cells_to_remove;
std::vector<FfData> ffs_to_emit;
dict<Cell *, pool<int>> const_bits;
bool did_something = false;
// Fold constant D/AD inputs into the tested value directly bits whose remaining inputs are
// wires become SAT proof obligations
std::vector<ConstObligation> obligations;
for (auto cell : module->selected_cells()) {
if (!cell->is_builtin_ff())
continue;
FfData ff(&initvals, cell);
pool<int> removed_sigbits;
for (int i = 0; i < ff.width; i++) {
State val = check_constbit(ff, i);
if (val == State::Sm)
continue;
// Check Synchronous input D
if (ff.has_clk || ff.has_gclk) {
if (!ff.sig_d[i].wire) {
// D is already a constant
val = combine_const(val, ff.sig_d[i].data);
if (val == State::Sm) continue;
} else if (opt.sat) {
// Try SAT proof for non-constant D wires
if (!prove_const_with_sat(qcsat, modwalker, ff.sig_q[i], ff.sig_d[i], val))
continue;
} else {
continue;
}
// Fold all const inputs first, so the SAT targets are checked against the final const
if ((ff.has_clk || ff.has_gclk) && !ff.sig_d[i].wire) {
val = combine_const(val, ff.sig_d[i].data);
if (val == State::Sm) continue;
}
if (ff.has_aload && !ff.sig_ad[i].wire) {
val = combine_const(val, ff.sig_ad[i].data);
if (val == State::Sm) continue;
}
// Check Async Load input AD
if (ff.has_aload) {
if (!ff.sig_ad[i].wire) {
val = combine_const(val, ff.sig_ad[i].data);
if (val == State::Sm) continue;
} else if (opt.sat) {
if (!prove_const_with_sat(qcsat, modwalker, ff.sig_q[i], ff.sig_ad[i], val))
continue;
} else {
continue;
}
ConstObligation ob;
ob.cell = cell;
ob.idx = i;
ob.val = val;
ob.q = ff.sig_q[i];
bool feasible = true;
if ((ff.has_clk || ff.has_gclk) && ff.sig_d[i].wire)
feasible = add_const_target(modwalker, ob, ff.sig_d[i]);
if (feasible && ff.has_aload && ff.sig_ad[i].wire)
feasible = add_const_target(modwalker, ob, ff.sig_ad[i]);
if (!feasible)
continue;
if (ob.targets.empty()) {
commit_const(const_bits, cell, i, ff.sig_q[i], val);
did_something = true;
continue;
}
obligations.push_back(ob);
}
}
log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n",
val ? 1 : 0, i, cell, cell->type.unescape(), module);
int64_t screen_cap = 0;
if (sat_effort > 0 && !obligations.empty()) {
// Screening cap, scaled down when the budget cannot afford a full-price screening round
int64_t num_queries = 0;
for (auto &ob : obligations)
num_queries += GetSize(ob.targets);
screen_cap = max((int64_t)20000, min((int64_t)200000, sat_effort / (4 * num_queries)));
}
// Replace the Q output with the constant value
initvals.remove_init(ff.sig_q[i]);
module->connect(ff.sig_q[i], val);
removed_sigbits.insert(i);
for (int batch_begin = 0; batch_begin < GetSize(obligations) && !sat_budget_spent(); ) {
QuickConeSat qcsat(modwalker);
int64_t cells_charged = 0;
int batch_end = batch_begin;
while (batch_end < GetSize(obligations) && !sat_budget_spent()) {
if (batch_end > batch_begin && GetSize(qcsat.imported_cells) >= sat_batch_cells)
break;
auto &ob = obligations[batch_end];
ob.q_lit = qcsat.importSigBit(ob.q);
for (auto &t : ob.targets)
t.lit = qcsat.importSigBit(t.sig);
qcsat.prepare();
charge_import(qcsat, cells_charged);
batch_end++;
}
// Reconstruct FF with constant bits removed
if (!removed_sigbits.empty()) {
std::vector<int> keep_bits;
for (int i = 0; i < ff.width; i++)
if (!removed_sigbits.count(i))
keep_bits.push_back(i);
int64_t cap = screen_cap;
bool out_of_budget = false;
if (keep_bits.empty()) {
cells_to_remove.push_back(cell);
} else {
ff = ff.slice(keep_bits);
ff.cell = cell;
ffs_to_emit.push_back(ff);
while (!out_of_budget) {
bool all_resolved = true;
for (int obi = batch_begin; obi < batch_end; obi++) {
auto &ob = obligations[obi];
if (ob.dropped)
continue;
for (auto &t : ob.targets) {
if (t.proven || ob.dropped)
continue;
if (sat_budget_spent()) {
out_of_budget = true;
break;
}
std::vector<int> modelExprs;
std::vector<ConstObligation *> model_obs;
for (int obi2 = batch_begin; obi2 < batch_end; obi2++) {
auto &ob2 = obligations[obi2];
if (ob2.dropped)
continue;
for (auto &t2 : ob2.targets)
if (!t2.proven) {
modelExprs.push_back(t2.lit);
modelExprs.push_back(ob2.q_lit);
model_obs.push_back(&ob2);
}
}
// Prove that the next value equals the constant in every state where Q already holds it
int vlit = qcsat.ez->value(ob.val == State::S1);
std::vector<int> assumptions;
assumptions.push_back(qcsat.ez->IFF(ob.q_lit, vlit));
assumptions.push_back(qcsat.ez->NOT(qcsat.ez->IFF(t.lit, vlit)));
std::vector<bool> modelVals;
int res = solve_budgeted(qcsat, cap, modelExprs, modelVals, assumptions);
if (res < 0) {
all_resolved = false;
continue;
}
if (res == 0) {
t.proven = true;
continue;
}
// Counterexample: this bit is not constant
// Any other pending bit whose Q holds its constant while its next value differs is
// disproven by the same state
for (int k = 0; k < GetSize(model_obs); k++) {
ConstObligation *ob2 = model_obs[k];
if (ob2->dropped)
continue;
bool want = (ob2->val == State::S1);
bool t_val = modelVals[2*k];
bool q_val = modelVals[2*k + 1];
if (q_val == want && t_val != want)
ob2->dropped = true;
}
ob.dropped = true;
}
if (out_of_budget)
break;
}
if (out_of_budget || all_resolved)
break;
cap = 0;
}
batch_begin = batch_end;
}
for (auto &ob : obligations) {
if (ob.dropped)
continue;
bool all_proven = true;
for (auto &t : ob.targets)
all_proven &= t.proven;
if (all_proven) {
commit_const(const_bits, ob.cell, ob.idx, ob.q, ob.val);
did_something = true;
}
}
// Reconstruct FF with constant bits removed
std::vector<RTLIL::Cell*> cells_to_remove;
std::vector<FfData> ffs_to_emit;
for (auto &kv : const_bits) {
Cell *cell = kv.first;
FfData ff(&initvals, cell);
std::vector<int> keep_bits;
for (int i = 0; i < ff.width; i++)
if (!kv.second.count(i))
keep_bits.push_back(i);
if (keep_bits.empty()) {
cells_to_remove.push_back(cell);
} else {
ff = ff.slice(keep_bits);
ff.cell = cell;
ffs_to_emit.push_back(ff);
}
}
for (auto* cell : cells_to_remove)
module->remove(cell);
@ -1196,6 +1381,13 @@ struct OptDffWorker
return refined_classes;
}
std::vector<std::vector<int>> drop_all_classes()
{
// Verified merges can depend on the equality of classes that are still unproven, so an incomplete run cannot keep any of them
log("Dropping all equivalent-FF merge candidates in module %s (sat effort budget exceeded before all classes were proven).\n", log_id(module));
return {};
}
std::vector<std::vector<int>> filter_classes_sat(
std::vector<std::vector<int>> classes,
const std::vector<EqBit> &bits,
@ -1208,10 +1400,13 @@ struct OptDffWorker
// Build the next-state function n_lit[idx] of every candidate bit by
// folding the FF's control logic on top of the D input (-> next value)
int64_t cells_charged = 0;
// Two bits are equivalent if their next states always agree whenever their
// current states (and those of every other candidate pair) agree
for (auto &cls : classes) {
if (sat_budget_spent())
return drop_all_classes();
for (int idx : cls) {
const EqBit &eb = bits[idx];
const FfData &ff = ff_for_cell.at(eb.cell);
@ -1243,10 +1438,10 @@ struct OptDffWorker
n_lit[idx] = n;
}
qcsat.prepare();
charge_import(qcsat, cells_charged);
}
qcsat.prepare();
// Assume the induction hypo (that every current class is internally equal in the present cycle), and try
// to prove that the members of each class therefore also agree in the next cycle
@ -1283,6 +1478,9 @@ struct OptDffWorker
if (n_lit[rep] == n_lit[cls[i]])
continue;
if (sat_budget_spent())
return drop_all_classes();
// Can the next state of the rep and this member ever differ?
int query = qcsat.ez->XOR(n_lit[rep], n_lit[cls[i]]);
// Capture every member's next-state value in that model so one counterexample
@ -1294,7 +1492,14 @@ struct OptDffWorker
std::vector<bool> modelVals;
assumptions.push_back(query);
if (qcsat.ez->solve(modelExprs, modelVals, assumptions)) {
int res = solve_budgeted(qcsat, 0, modelExprs, modelVals, assumptions);
if (res < 0) {
sat_budget_exceeded();
return drop_all_classes();
}
if (res > 0) {
// SAT -> partition entire class
std::vector<int> sub0;
std::vector<int> sub1;
@ -1427,6 +1632,9 @@ struct OptDffPass : public Pass {
log(" non-constant inputs) that can also be replaced with a constant driver,\n");
log(" or merged with equivalent flip-flops. this reasons in 2-valued logic\n");
log(" and may resolve don't-care bits, so it is incompatible with -keepdc.\n");
log(" the scratchpad option 'opt_dff.sat_effort' (solver propagation steps,\n");
log(" default 1000000000, 0 = unlimited) deterministically bounds the total\n");
log(" sat effort spent per module, remaining proofs are skipped once exceeded.\n");
log("\n");
log(" -keepdc\n");
log(" some optimizations change the behavior of the circuit with respect to\n");