From 143975bd66885a65fa7c9d09cfc487f0154b92fa Mon Sep 17 00:00:00 2001 From: nella Date: Sat, 11 Jul 2026 12:23:03 +0200 Subject: [PATCH 1/8] ezsat add propagation budget api. --- libs/ezsat/ezminisat.cc | 19 ++++++++++++++++++- libs/ezsat/ezsat.cc | 3 +++ libs/ezsat/ezsat.h | 16 ++++++++++++++++ 3 files changed, 37 insertions(+), 1 deletion(-) diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index 1f4b8855f..a820405ac 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -104,6 +104,8 @@ bool ezMiniSAT::solver(const std::vector &modelExpressions, std::vectorsolve(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 diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 8e3114705..e5cdf84c1 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -55,6 +55,9 @@ ezSAT::ezSAT() solverTimeout = 0; solverTimeoutStatus = false; + solverPropLimit = 0; + solverPropLimitStatus = false; + solverProps = 0; literal("CONST_TRUE"); literal("CONST_FALSE"); diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 445c8edba..77496b89f 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -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(); From 0a6ff36e305bbc621f1255831a7a6b0f614f0bb7 Mon Sep 17 00:00:00 2001 From: nella Date: Sat, 11 Jul 2026 12:32:06 +0200 Subject: [PATCH 2/8] Test solve_budgeted. --- passes/opt/opt_dff.cc | 63 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 49275bc7c..1130e911e 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -143,6 +143,57 @@ struct OptDffWorker std::vector 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: solver effort budget of %lld exceeded in module %s, " + "skipping remaining sat proofs (scratchpad option 'opt_dff.sat_effort').\n", + (long long)(sat_effort / 1000), 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 &modelExprs, + std::vector &modelVals, const std::vector &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); } @@ -1283,6 +1334,9 @@ struct OptDffWorker if (n_lit[rep] == n_lit[cls[i]]) continue; + if (sat_budget_spent()) + return drop_all(); + // 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 +1348,14 @@ struct OptDffWorker std::vector 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(); + } + + if (res > 0) { // SAT -> partition entire class std::vector sub0; std::vector sub1; From 0bf4afc023e97cb9f143a63a4891e38a575505ec Mon Sep 17 00:00:00 2001 From: nella Date: Sat, 11 Jul 2026 12:34:37 +0200 Subject: [PATCH 3/8] eqbits drop_all. --- passes/opt/opt_dff.cc | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 1130e911e..240734796 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -1260,9 +1260,18 @@ 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) + // Verified merges can depend on the equality of classes that are still unproven, so an incomplete run cannot keep any of them + auto drop_all = [&]() -> std::vector> { + log("Dropping all equivalent-FF merge candidates in module %s (sat effort budget exceeded before all classes were proven).\n", log_id(module)); + return {}; + }; + 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(); for (int idx : cls) { const EqBit &eb = bits[idx]; const FfData &ff = ff_for_cell.at(eb.cell); @@ -1294,6 +1303,8 @@ struct OptDffWorker n_lit[idx] = n; } + qcsat.prepare(); + charge_import(qcsat, cells_charged); } qcsat.prepare(); From 7bdcc97aeda459a72a828534584db70a38da28ce Mon Sep 17 00:00:00 2001 From: nella Date: Sat, 11 Jul 2026 12:41:27 +0200 Subject: [PATCH 4/8] Implement constbit gather. --- passes/opt/opt_dff.cc | 244 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 200 insertions(+), 44 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 240734796..b8016df20 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -248,6 +248,9 @@ struct OptDffWorker OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod) { + sat_effort = (int64_t)module->design->scratchpad_get_int("opt_dff.sat_effort", 1000000) * 1000; + 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 @@ -970,16 +973,46 @@ 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 targets; + }; + bool run_constbits() { // Find FFs that are provably constant ModWalker modwalker(module->design, module); QuickConeSat qcsat(modwalker); - std::vector cells_to_remove; - std::vector ffs_to_emit; + dict> const_bits; bool did_something = false; + auto commit_const = [&](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); + did_something = true; + }; + + // Fold constant D/AD inputs into the tested value directly bits whose remaining inputs are + // wires become SAT proof obligations + std::vector obligations; + for (auto cell : module->selected_cells()) { if (!cell->is_builtin_ff()) continue; @@ -992,58 +1025,181 @@ struct OptDffWorker 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; + auto add_target = [&](SigBit sig) { + if (!opt.sat || (val != State::S0 && val != State::S1) || + !modwalker.has_drivers(sig)) { + feasible = false; + return; } + ConstTarget t; + t.sig = sig; + ob.targets.push_back(t); + }; + + if ((ff.has_clk || ff.has_gclk) && ff.sig_d[i].wire) + add_target(ff.sig_d[i]); + if (feasible && ff.has_aload && ff.sig_ad[i].wire) + add_target(ff.sig_ad[i]); + if (!feasible) + continue; + + if (ob.targets.empty()) { + commit_const(cell, i, ff.sig_q[i], val); + 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 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 modelExprs; + std::vector 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 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 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; } - did_something = true; + + 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(ob.cell, ob.idx, ob.q, ob.val); + } + + // Reconstruct FF with constant bits removed + std::vector cells_to_remove; + std::vector ffs_to_emit; + + for (auto &kv : const_bits) { + Cell *cell = kv.first; + FfData ff(&initvals, cell); + std::vector 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); } } From a2b76556f3dff6b3caa132958f18953a58f839aa Mon Sep 17 00:00:00 2001 From: nella Date: Sat, 11 Jul 2026 13:06:42 +0200 Subject: [PATCH 5/8] Add help message + cleanup. --- passes/opt/opt_dff.cc | 102 +++++++++++++++++------------------------- 1 file changed, 41 insertions(+), 61 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index b8016df20..5a700d835 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -153,9 +153,8 @@ struct OptDffWorker void sat_budget_exceeded() { if (!sat_budget_out) - log_warning("opt_dff -sat: solver effort budget of %lld exceeded in module %s, " - "skipping remaining sat proofs (scratchpad option 'opt_dff.sat_effort').\n", - (long long)(sat_effort / 1000), log_id(module)); + 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; } @@ -248,7 +247,7 @@ struct OptDffWorker OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod) { - sat_effort = (int64_t)module->design->scratchpad_get_int("opt_dff.sat_effort", 1000000) * 1000; + 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: @@ -939,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]; @@ -991,24 +971,31 @@ struct OptDffWorker std::vector targets; }; + void commit_const(dict> &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); dict> const_bits; bool did_something = false; - auto commit_const = [&](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); - did_something = true; - }; - // Fold constant D/AD inputs into the tested value directly bits whose remaining inputs are // wires become SAT proof obligations std::vector obligations; @@ -1018,7 +1005,6 @@ struct OptDffWorker continue; FfData ff(&initvals, cell); - pool removed_sigbits; for (int i = 0; i < ff.width; i++) { State val = check_constbit(ff, i); @@ -1042,26 +1028,16 @@ struct OptDffWorker ob.q = ff.sig_q[i]; bool feasible = true; - auto add_target = [&](SigBit sig) { - if (!opt.sat || (val != State::S0 && val != State::S1) || - !modwalker.has_drivers(sig)) { - feasible = false; - return; - } - ConstTarget t; - t.sig = sig; - ob.targets.push_back(t); - }; - if ((ff.has_clk || ff.has_gclk) && ff.sig_d[i].wire) - add_target(ff.sig_d[i]); + feasible = add_const_target(modwalker, ob, ff.sig_d[i]); if (feasible && ff.has_aload && ff.sig_ad[i].wire) - add_target(ff.sig_ad[i]); + feasible = add_const_target(modwalker, ob, ff.sig_ad[i]); if (!feasible) continue; if (ob.targets.empty()) { - commit_const(cell, i, ff.sig_q[i], val); + commit_const(const_bits, cell, i, ff.sig_q[i], val); + did_something = true; continue; } obligations.push_back(ob); @@ -1178,8 +1154,10 @@ struct OptDffWorker bool all_proven = true; for (auto &t : ob.targets) all_proven &= t.proven; - if (all_proven) - commit_const(ob.cell, ob.idx, ob.q, ob.val); + if (all_proven) { + commit_const(const_bits, ob.cell, ob.idx, ob.q, ob.val); + did_something = true; + } } // Reconstruct FF with constant bits removed @@ -1403,6 +1381,13 @@ struct OptDffWorker return refined_classes; } + std::vector> 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> filter_classes_sat( std::vector> classes, const std::vector &bits, @@ -1415,19 +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) - - // Verified merges can depend on the equality of classes that are still unproven, so an incomplete run cannot keep any of them - auto drop_all = [&]() -> std::vector> { - log("Dropping all equivalent-FF merge candidates in module %s (sat effort budget exceeded before all classes were proven).\n", log_id(module)); - return {}; - }; 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(); + return drop_all_classes(); for (int idx : cls) { const EqBit &eb = bits[idx]; const FfData &ff = ff_for_cell.at(eb.cell); @@ -1463,8 +1442,6 @@ struct OptDffWorker 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 @@ -1502,7 +1479,7 @@ struct OptDffWorker continue; if (sat_budget_spent()) - return drop_all(); + 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]]); @@ -1519,7 +1496,7 @@ struct OptDffWorker if (res < 0) { sat_budget_exceeded(); - return drop_all(); + return drop_all_classes(); } if (res > 0) { @@ -1655,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"); From 5489a9added4db85b2a2a17e5ebf6243c1639aaf Mon Sep 17 00:00:00 2001 From: nella Date: Fri, 24 Jul 2026 13:30:43 +0200 Subject: [PATCH 6/8] Add SAT effort test. --- tests/opt/opt_dff_sat_effort.ys | 67 +++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 tests/opt/opt_dff_sat_effort.ys diff --git a/tests/opt/opt_dff_sat_effort.ys b/tests/opt/opt_dff_sat_effort.ys new file mode 100644 index 000000000..70c90a2ce --- /dev/null +++ b/tests/opt/opt_dff_sat_effort.ys @@ -0,0 +1,67 @@ +design -reset +read_verilog -sv < 4'd10) & (a < 4'd3); + y1 <= (b > 4'd12) & (b < 4'd5); + y2 <= (a > 4'd9) & (a < 4'd2); + y3 <= (b > 4'd11) & (b < 4'd4); + end +endmodule +EOT + +hierarchy -top test_case +prep +design -save gold + +# default budget proves everything +opt_dff -sat +opt_clean -purge +select -assert-count 0 t:$dff +design -save gate_full + +# low budget skips all +design -load gold +scratchpad -set opt_dff.sat_effort 1 +logger -expect warning "effort limit exceeded" 1 +opt_dff -sat +logger -check-expected +opt_clean -purge +select -assert-count 4 t:$dff +design -save gate_low + +# only the selected cone is folded +design -load gold +scratchpad -set opt_dff.sat_effort 0 +select o:y0 %ci* +opt_dff -sat +select -clear +opt_clean -purge +select -assert-count 3 t:$dff + +# eq +design -load gold +design -copy-from gate_full -as gate_full test_case +equiv_make test_case gate_full equiv_full +equiv_induct equiv_full +equiv_status -assert + +design -load gold +design -copy-from gate_low -as gate_low test_case +equiv_make test_case gate_low equiv_low +equiv_induct equiv_low +equiv_status -assert From 3ac8daafd11c4710b35394cba8d184b0273c0a90 Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 27 Jul 2026 10:00:16 +0200 Subject: [PATCH 7/8] Add reusable SatEffortBudget helper to qcsat. --- kernel/qcsat.cc | 21 +++++++++++++++++++++ kernel/qcsat.h | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 54 insertions(+) diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc index c9d00efa1..f996a963a 100644 --- a/kernel/qcsat.cc +++ b/kernel/qcsat.cc @@ -100,3 +100,24 @@ int QuickConeSat::cell_complexity(RTLIL::Cell *cell) // Unknown cell. return 5; } + +void SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t &cells_charged) +{ + if (enabled()) + remaining -= (GetSize(qcsat.imported_cells) - cells_charged) * import_cell_cost; + cells_charged = GetSize(qcsat.imported_cells); +} + +SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector &modelExprs, + std::vector &modelVals, const std::vector &assumptions) +{ + if (enabled()) + cap = (cap > 0) ? std::min(cap, remaining) : remaining; + qcsat.ez->setSolverPropLimit(cap); + bool sat = qcsat.ez->solve(modelExprs, modelVals, assumptions); + if (enabled()) + remaining -= qcsat.ez->getSolverProps(); + if (!sat && qcsat.ez->getSolverPropLimitStatus()) + return Result::LimitReached; + return sat ? Result::Sat : Result::Unsat; +} diff --git a/kernel/qcsat.h b/kernel/qcsat.h index e4d3c3c5d..d0b717c8f 100644 --- a/kernel/qcsat.h +++ b/kernel/qcsat.h @@ -71,6 +71,39 @@ struct QuickConeSat { static int cell_complexity(RTLIL::Cell *cell); }; +// A deterministic effort budget for SAT-based optimizations, measured in solver +// propagation steps (see ezSAT::getSolverProps). The budget is held once per unit +// of work (typically a module) and reused across many QuickConeSat instances: a +// pass that rebuilds the solver in batches keeps a single SatEffortBudget and +// spends from it in every batch, rather than resetting the budget per solver. +// Spending the budget only skips optimizations, and it never affects correctness, +// because a skipped proof just leaves a candidate un-optimized. +struct SatEffortBudget { + enum class Result { Sat, Unsat, LimitReached }; + + // Effort charged per imported cell + static constexpr int64_t import_cell_cost = 100; + + // starting budget (0 = unlimited) + int64_t total = 0; + int64_t remaining = 0; + + SatEffortBudget() {} + explicit SatEffortBudget(int64_t total) : total(total), remaining(total) {} + + bool enabled() const { return total > 0; } + + // True once the budget is used up + bool spent() const { return enabled() && remaining <= 0; } + + // Charge for the cells imported into qcsat since the previous call (pricing the cells pulled in) + // cells_charged records how many of qcsat's imported cells are already paid for + void charge_import(QuickConeSat &qcsat, int64_t &cells_charged); + + Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector &modelExprs, + std::vector &modelVals, const std::vector &assumptions); +}; + YOSYS_NAMESPACE_END #endif From 88da4a644b1002ae7fa1777a2418c9b9de2926ac Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 27 Jul 2026 10:01:24 +0200 Subject: [PATCH 8/8] Budget SAT effort via shared SatEffortBudget. --- passes/opt/opt_dff.cc | 196 ++++++++++++++------------------ tests/opt/opt_dff_sat_effort.ys | 2 +- 2 files changed, 87 insertions(+), 111 deletions(-) diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 5a700d835..58661c38f 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -143,54 +143,23 @@ struct OptDffWorker std::vector dff_cells; - // Solver effort budget shared by run_constbits and run_eqbits, per module - static constexpr int64_t sat_import_cell_cost = 100; + // opt_dff -sat rebuilds the solver in batches of at most this many imported + // cells, so one pathological module can't grow a single giant solver 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; - } + SatEffortBudget sat_budget; + bool sat_warned = false; - bool sat_budget_spent() + bool warn_if_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 &modelExprs, - std::vector &modelVals, const std::vector &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); + if (!sat_budget.spent()) + return false; + if (!sat_warned) + log_warning("opt_dff -sat: solver effort budget for module %s is exhausted, leaving the " + "remaining FFs un-optimized. Raise or clear the limit with the scratchpad " + "option 'opt_dff.sat_effort' (0 disables it).\n", log_id(module)); + sat_warned = true; + return true; } bool is_active(SigBit sig, bool pol) const { @@ -247,8 +216,7 @@ 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; + sat_budget = SatEffortBudget(module->design->scratchpad_get_int("opt_dff.sat_effort", 1000000000)); // 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) @@ -988,6 +956,43 @@ struct OptDffWorker return true; } + // Try to decide whether target t of obligation ob is constant, under the given per-query cap. + bool resolve_const_target(QuickConeSat &qcsat, int64_t cap, ConstObligation &ob, ConstTarget &t, + const std::vector &modelExprs, const std::vector &model_obs) + { + // 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 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 modelVals; + // One counterexample can prune many targets + auto res = sat_budget.solve(qcsat, cap, modelExprs, modelVals, assumptions); + + if (res == SatEffortBudget::Result::LimitReached) + return false; // Nothing changed + if (res == SatEffortBudget::Result::Unsat) { + t.proven = true; // t is proven to be const + return true; + } + + // 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; + return true; + } + bool run_constbits() { // Find FFs that are provably constant @@ -1045,20 +1050,22 @@ struct OptDffWorker } int64_t screen_cap = 0; - if (sat_effort > 0 && !obligations.empty()) { + if (sat_budget.enabled() && !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))); + screen_cap = max((int64_t)20000, min((int64_t)200000, sat_budget.total / (4 * num_queries))); } - for (int batch_begin = 0; batch_begin < GetSize(obligations) && !sat_budget_spent(); ) { + // Each obligation is proven independently, so processing obligations in + // batches and stopping early on an exhausted budget is safe + for (int batch_begin = 0; batch_begin < GetSize(obligations) && !warn_if_budget_spent(); ) { QuickConeSat qcsat(modwalker); int64_t cells_charged = 0; int batch_end = batch_begin; - while (batch_end < GetSize(obligations) && !sat_budget_spent()) { + while (batch_end < GetSize(obligations) && !warn_if_budget_spent()) { if (batch_end > batch_begin && GetSize(qcsat.imported_cells) >= sat_batch_cells) break; auto &ob = obligations[batch_end]; @@ -1066,78 +1073,47 @@ struct OptDffWorker for (auto &t : ob.targets) t.lit = qcsat.importSigBit(t.sig); qcsat.prepare(); - charge_import(qcsat, cells_charged); + sat_budget.charge_import(qcsat, cells_charged); batch_end++; } + // Sweep the batch under a cheap screening cap, then re-sweep the still-undecided targets int64_t cap = screen_cap; bool out_of_budget = false; while (!out_of_budget) { bool all_resolved = true; + // Counter ex.: every pending target in the batch. Entries that get proven or dropped later + // in the sweep are harmless (a proven bit is constant in every model) + std::vector modelExprs; + std::vector model_obs; 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) { + modelExprs.push_back(t.lit); + modelExprs.push_back(ob.q_lit); + model_obs.push_back(&ob); + } + } + + for (int obi = batch_begin; obi < batch_end && !out_of_budget; obi++) { auto &ob = obligations[obi]; if (ob.dropped) continue; for (auto &t : ob.targets) { if (t.proven || ob.dropped) continue; - if (sat_budget_spent()) { + if (warn_if_budget_spent()) { out_of_budget = true; break; } - - std::vector modelExprs; - std::vector 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 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 modelVals; - int res = solve_budgeted(qcsat, cap, modelExprs, modelVals, assumptions); - - if (res < 0) { + if (!resolve_const_target(qcsat, cap, ob, t, modelExprs, model_obs)) 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) @@ -1383,8 +1359,8 @@ struct OptDffWorker std::vector> 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)); + log("opt_dff -sat: skipping all equivalent-flip-flop merges in module %s (solver effort budget " + "exhausted before the equivalences could be proven).\n", log_id(module)); return {}; } @@ -1405,7 +1381,7 @@ struct OptDffWorker // 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()) + if (warn_if_budget_spent()) return drop_all_classes(); for (int idx : cls) { const EqBit &eb = bits[idx]; @@ -1439,7 +1415,7 @@ struct OptDffWorker n_lit[idx] = n; } qcsat.prepare(); - charge_import(qcsat, cells_charged); + sat_budget.charge_import(qcsat, cells_charged); } // Assume the induction hypo (that every current class is internally equal in the present cycle), and try @@ -1478,7 +1454,7 @@ struct OptDffWorker if (n_lit[rep] == n_lit[cls[i]]) continue; - if (sat_budget_spent()) + if (warn_if_budget_spent()) return drop_all_classes(); // Can the next state of the rep and this member ever differ? @@ -1492,14 +1468,14 @@ struct OptDffWorker std::vector modelVals; assumptions.push_back(query); - int res = solve_budgeted(qcsat, 0, modelExprs, modelVals, assumptions); + auto res = sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions); - if (res < 0) { - sat_budget_exceeded(); + if (res == SatEffortBudget::Result::LimitReached) { + warn_if_budget_spent(); return drop_all_classes(); } - if (res > 0) { + if (res == SatEffortBudget::Result::Sat) { // SAT -> partition entire class std::vector sub0; std::vector sub1; diff --git a/tests/opt/opt_dff_sat_effort.ys b/tests/opt/opt_dff_sat_effort.ys index 70c90a2ce..4ab868f17 100644 --- a/tests/opt/opt_dff_sat_effort.ys +++ b/tests/opt/opt_dff_sat_effort.ys @@ -37,7 +37,7 @@ design -save gate_full # low budget skips all design -load gold scratchpad -set opt_dff.sat_effort 1 -logger -expect warning "effort limit exceeded" 1 +logger -expect warning "solver effort budget for module test_case is exhausted" 1 opt_dff -sat logger -check-expected opt_clean -purge