Merge pull request #6125 from YosysHQ/nella/share-sat-effort

share: limit SAT effort [sc-750]

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<int> &assumptions)
+{
+	std::vector<bool> modelVals;
+	return solve(qcsat, cap, {}, modelVals, assumptions);
+}
+
 SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
 		std::vector<bool> &modelVals, const std::vector<int> &assumptions)
 {
+	if (spent())
+		return Result::LimitReached;
 	if (enabled())
 		cap = (cap > 0) ? std::min(cap, remaining) : remaining;
 	qcsat.ez->setSolverPropLimit(cap);

kernel/qcsat.h

@@ -102,6 +102,9 @@ struct SatEffortBudget {
 
 	Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
 			std::vector<bool> &modelVals, const std::vector<int> &assumptions);
+
+	// Assumptions-only query without a model
+	Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &assumptions);
 };
 
 YOSYS_NAMESPACE_END

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<RTLIL::Cell*> cells_to_remove;
 	pool<RTLIL::Cell*> recursion_state;
 
+	SatEffortBudget sat_budget;
+	bool sat_warned = false;
+
 	SigMap topo_sigmap;
 	std::map<RTLIL::Cell*, std::set<RTLIL::Cell*, cell_ptr_cmp>, cell_ptr_cmp> topo_cell_drivers;
 	std::map<RTLIL::SigBit, std::set<RTLIL::Cell*, cell_ptr_cmp>> 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<ssc_pair_t> &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<RTLIL::SigBit> 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;
 

tests/opt/share_sat_effort.ys

@@ -0,0 +1,53 @@
+design -reset
+read_verilog <<EOT
+module test_case (
+	input wire [3:0] a,
+	input wire [3:0] b,
+	input wire [3:0] c,
+	input wire [3:0] d,
+	output wire [7:0] y,
+	output wire [7:0] z
+);
+	wire s1 = d < 4'd5;
+	wire s2 = d > 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