From cd029c0638d21ceed96c762acb02907b6892f48a Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 17 Aug 2026 12:19:07 +0200 Subject: [PATCH 1/3] Add solve without model. --- kernel/qcsat.cc | 8 ++++++++ kernel/qcsat.h | 3 +++ 2 files changed, 11 insertions(+) diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc index f996a963a..a5ecd5cb0 100644 --- a/kernel/qcsat.cc +++ b/kernel/qcsat.cc @@ -108,9 +108,17 @@ void SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t &cells_charged) cells_charged = GetSize(qcsat.imported_cells); } +SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector &assumptions) +{ + std::vector modelVals; + return solve(qcsat, cap, {}, modelVals, assumptions); +} + SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector &modelExprs, std::vector &modelVals, const std::vector &assumptions) { + if (spent()) + return Result::LimitReached; if (enabled()) cap = (cap > 0) ? std::min(cap, remaining) : remaining; qcsat.ez->setSolverPropLimit(cap); diff --git a/kernel/qcsat.h b/kernel/qcsat.h index d0b717c8f..09d072f7c 100644 --- a/kernel/qcsat.h +++ b/kernel/qcsat.h @@ -102,6 +102,9 @@ struct SatEffortBudget { Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector &modelExprs, std::vector &modelVals, const std::vector &assumptions); + + // Assumptions-only query without a model + Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector &assumptions); }; YOSYS_NAMESPACE_END From ce0785a01bb2513481683bae8fcd51a3fb7d8ff2 Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 17 Aug 2026 12:20:43 +0200 Subject: [PATCH 2/3] Limit SAT effort. --- passes/opt/share.cc | 64 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 58 insertions(+), 6 deletions(-) diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 119243d48..2b6dbb796 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -36,6 +36,7 @@ struct ShareWorkerConfig { int limit; size_t pattern_limit; + int sat_effort; bool opt_aggressive; bool opt_fast; StaticCellTypes::Categories::Category generic_uni_ops, generic_bin_ops, generic_cbin_ops, generic_other_ops; @@ -55,6 +56,9 @@ struct ShareWorker pool cells_to_remove; pool recursion_state; + SatEffortBudget sat_budget; + bool sat_warned = false; + SigMap topo_sigmap; std::map, cell_ptr_cmp> topo_cell_drivers; std::map> topo_bit_drivers; @@ -1197,6 +1201,18 @@ struct ShareWorker // Setup and run // ------------- + bool warn_if_budget_spent() + { + if (!sat_budget.spent()) + return false; + if (!sat_warned) + log_warning("share: solver effort budget for module %s is exhausted, leaving the " + "remaining cells un-shared. Raise or clear the limit with the scratchpad " + "option 'share.sat_effort' (0 disables it).\n", log_id(module)); + sat_warned = true; + return true; + } + void remove_cell(Cell *cell) { shareable_cells.erase(cell); @@ -1222,6 +1238,8 @@ struct ShareWorker #endif limit = config.limit; + sat_budget = SatEffortBudget(config.sat_effort); + sat_warned = false; modwalker.setup(module); cells_to_remove.clear(); @@ -1242,7 +1260,7 @@ struct ShareWorker log("Found %d cells in module %s that may be considered for resource sharing.\n", GetSize(shareable_cells), module); - while (!shareable_cells.empty() && config.limit != 0) + while (!shareable_cells.empty() && config.limit != 0 && !warn_if_budget_spent()) { RTLIL::Cell *cell = *shareable_cells.begin(); shareable_cells.erase(cell); @@ -1280,6 +1298,9 @@ struct ShareWorker for (auto other_cell : candidates) { + if (warn_if_budget_spent()) + break; + log(" Analyzing resource sharing with %s (%s):\n", other_cell, other_cell->type.unescape()); const pool &other_cell_activation_patterns = find_cell_activation_patterns(other_cell, " "); @@ -1325,6 +1346,7 @@ struct ShareWorker qcsat.max_cell_outs = 3; qcsat.max_cell_count = 100; } + int64_t cells_charged = 0; std::set bits_queue; @@ -1345,16 +1367,39 @@ struct ShareWorker int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active); int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active); - bool pattern_only_solve = qcsat.ez->solve(qcsat.ez->AND(sub1, sub2)); - qcsat.prepare(); + auto pattern_res = sat_budget.solve(qcsat, 0, {qcsat.ez->AND(sub1, sub2)}); + if (pattern_res == SatEffortBudget::Result::LimitReached) { + warn_if_budget_spent(); + break; + } + bool pattern_only_solve = pattern_res == SatEffortBudget::Result::Sat; - if (!qcsat.ez->solve(sub1)) { + // Don't import more of the cone than the budget can still pay for + if (sat_budget.enabled()) { + int import_cap = max(int(sat_budget.remaining / SatEffortBudget::import_cell_cost), 1); + if (!qcsat.max_cell_count || import_cap < qcsat.max_cell_count) + qcsat.max_cell_count = import_cap; + } + qcsat.prepare(); + sat_budget.charge_import(qcsat, cells_charged); + + auto act_res = sat_budget.solve(qcsat, 0, {sub1}); + if (act_res == SatEffortBudget::Result::LimitReached) { + warn_if_budget_spent(); + break; + } + if (act_res == SatEffortBudget::Result::Unsat) { log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", cell); cells_to_remove.insert(cell); break; } - if (!qcsat.ez->solve(sub2)) { + act_res = sat_budget.solve(qcsat, 0, {sub2}); + if (act_res == SatEffortBudget::Result::LimitReached) { + warn_if_budget_spent(); + break; + } + if (act_res == SatEffortBudget::Result::Unsat) { log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", other_cell); cells_to_remove.insert(other_cell); shareable_cells.erase(other_cell); @@ -1376,7 +1421,13 @@ struct ShareWorker log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n", qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses()); - if (qcsat.ez->solve(sat_model, sat_model_values)) { + auto res = sat_budget.solve(qcsat, 0, sat_model, sat_model_values, {}); + if (res == SatEffortBudget::Result::LimitReached) { + warn_if_budget_spent(); + break; + } + + if (res == SatEffortBudget::Result::Sat) { log(" According to the SAT solver this pair of cells can not be shared.\n"); log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values)); for (int i = GetSize(sat_model_values)-1; i >= 0; i--) @@ -1529,6 +1580,7 @@ struct SharePass : public Pass { config.limit = -1; config.pattern_limit = design->scratchpad_get_int("share.pattern_limit", 1000); + config.sat_effort = design->scratchpad_get_int("share.sat_effort", 1000000000); config.opt_aggressive = false; config.opt_fast = false; From bbcbdcec09bd85ef3f2a59a23c9b6b28a3fed26a Mon Sep 17 00:00:00 2001 From: nella Date: Mon, 17 Aug 2026 12:20:51 +0200 Subject: [PATCH 3/3] Add test. --- tests/opt/share_sat_effort.ys | 53 +++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) create mode 100644 tests/opt/share_sat_effort.ys diff --git a/tests/opt/share_sat_effort.ys b/tests/opt/share_sat_effort.ys new file mode 100644 index 000000000..eeaf4ce49 --- /dev/null +++ b/tests/opt/share_sat_effort.ys @@ -0,0 +1,53 @@ +design -reset +read_verilog < 4'd10; + assign y = s1 ? a*b : 8'd0; + assign z = s2 ? a*c : 8'd0; +endmodule +EOT + +hierarchy -top test_case +prep +design -save gold + +share +opt_clean -purge +select -assert-count 1 t:$mul +design -save gate_full + +# low budget skips all merges +design -load gold +scratchpad -set share.sat_effort 1 +logger -expect warning "solver effort budget for module test_case is exhausted" 1 +share +logger -check-expected +opt_clean -purge +select -assert-count 2 t:$mul +design -save gate_low + +# 0 disables the limit +design -load gold +scratchpad -set share.sat_effort 0 +share +opt_clean -purge +select -assert-count 1 t:$mul + +# eq +design -load gold +design -copy-from gate_full -as gate test_case +miter -equiv -flatten -make_outputs test_case gate miter +sat -verify -prove trigger 0 miter + +design -load gold +design -copy-from gate_low -as gate test_case +miter -equiv -flatten -make_outputs test_case gate miter +sat -verify -prove trigger 0 miter