Merge 88da4a644b into 4821ed17b4

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<int> &modelExprs,
+		std::vector<bool> &modelVals, const std::vector<int> &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;
+}

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<int> &modelExprs,
+			std::vector<bool> &modelVals, const std::vector<int> &assumptions);
+};
+
 YOSYS_NAMESPACE_END
 
 #endif

libs/ezsat/ezminisat.cc

@@ -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
 

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");

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();

passes/opt/opt_dff.cc

@@ -143,6 +143,25 @@ struct OptDffWorker
 
 	std::vector<Cell *> dff_cells;
 
+	// 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;
+
+	SatEffortBudget sat_budget;
+	bool sat_warned = false;
+
+	bool warn_if_budget_spent()
+	{
+		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 {
 		return sig == (pol ? State::S1 : State::S0);
 	}
@@ -197,6 +216,8 @@ struct OptDffWorker
 	OptDffWorker(const OptDffOptions &opt, Module *mod)
 		: opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod)
 	{
+		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)
 		// - bit2mux: the mux cell and bit index that drives it, if any
@@ -885,25 +906,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 +921,242 @@ 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;
+	}
+
+	// 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<int> &modelExprs, const std::vector<ConstObligation *> &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<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;
+		// 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
 		ModWalker modwalker(module->design, module);
-		QuickConeSat qcsat(modwalker);
 
-		std::vector<RTLIL::Cell*> cells_to_remove;
+		dict<Cell *, pool<int>> const_bits;
-		std::vector<FfData> ffs_to_emit;
 		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
+				// Fold all const inputs first, so the SAT targets are checked against the final const
-				if (ff.has_clk || ff.has_gclk) {
+				if ((ff.has_clk || ff.has_gclk) && !ff.sig_d[i].wire) {
-					if (!ff.sig_d[i].wire) {
+					val = combine_const(val, ff.sig_d[i].data);
-						// D is already a constant
+					if (val == State::Sm) continue;
-						val = combine_const(val, ff.sig_d[i].data);
+				}
-						if (val == State::Sm) continue;
+				if (ff.has_aload && !ff.sig_ad[i].wire) {
-					} else if (opt.sat) {
+					val = combine_const(val, ff.sig_ad[i].data);
-						// Try SAT proof for non-constant D wires
+					if (val == State::Sm) continue;
-						if (!prove_const_with_sat(qcsat, modwalker, ff.sig_q[i], ff.sig_d[i], val))
-							continue;
-					} else {
-						continue;
-					}
 				}
 
-				// Check Async Load input AD
+				ConstObligation ob;
-				if (ff.has_aload) {
+				ob.cell = cell;
-					if (!ff.sig_ad[i].wire) {
+				ob.idx = i;
-						val = combine_const(val, ff.sig_ad[i].data);
+				ob.val = val;
-						if (val == State::Sm) continue;
+				ob.q = ff.sig_q[i];
-					} else if (opt.sat) {
+
-						if (!prove_const_with_sat(qcsat, modwalker, ff.sig_q[i], ff.sig_ad[i], val))
+				bool feasible = true;
-							continue;
+				if ((ff.has_clk || ff.has_gclk) && ff.sig_d[i].wire)
-					} else {
+					feasible = add_const_target(modwalker, ob, ff.sig_d[i]);
-						continue;
+				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",
+		int64_t screen_cap = 0;
-						val ? 1 : 0, i, cell, cell->type.unescape(), module);
+		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_budget.total / (4 * num_queries)));
+		}
 
-				// Replace the Q output with the constant value
+		// Each obligation is proven independently, so processing obligations in
-				initvals.remove_init(ff.sig_q[i]);
+		// batches and stopping early on an exhausted budget is safe
-				module->connect(ff.sig_q[i], val);
+		for (int batch_begin = 0; batch_begin < GetSize(obligations) && !warn_if_budget_spent(); ) {
-				removed_sigbits.insert(i);
+			QuickConeSat qcsat(modwalker);
+			int64_t cells_charged = 0;
+			int batch_end = batch_begin;
+
+			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];
+				ob.q_lit = qcsat.importSigBit(ob.q);
+				for (auto &t : ob.targets)
+					t.lit = qcsat.importSigBit(t.sig);
+				qcsat.prepare();
+				sat_budget.charge_import(qcsat, cells_charged);
+				batch_end++;
 			}
 
-			// Reconstruct FF with constant bits removed
+			// Sweep the batch under a cheap screening cap, then re-sweep  the still-undecided targets
-			if (!removed_sigbits.empty()) {
+			int64_t cap = screen_cap;
-				std::vector<int> keep_bits;
+			bool out_of_budget = false;
-				for (int i = 0; i < ff.width; i++)
-					if (!removed_sigbits.count(i))
-						keep_bits.push_back(i);
 
-				if (keep_bits.empty()) {
+			while (!out_of_budget) {
-					cells_to_remove.push_back(cell);
+				bool all_resolved = true;
-				} else {
+
-					ff = ff.slice(keep_bits);
+				// Counter ex.: every pending target in the batch. Entries that get proven or dropped later
-					ff.cell = cell;
+				// in the sweep are harmless (a proven bit is constant in every model)
-					ffs_to_emit.push_back(ff);
+				std::vector<int> modelExprs;
+				std::vector<ConstObligation *> 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 (warn_if_budget_spent()) {
+							out_of_budget = true;
+							break;
+						}
+						if (!resolve_const_target(qcsat, cap, ob, t, modelExprs, model_obs))
+							all_resolved = false;
+					}
+				}
+
+				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 +1357,13 @@ struct OptDffWorker
 		return refined_classes;
 	}
 
+	std::vector<std::vector<int>> drop_all_classes()
+	{
+		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 {};
+	}
+
 	std::vector<std::vector<int>> filter_classes_sat(
 		std::vector<std::vector<int>> classes,
 		const std::vector<EqBit> &bits,
@@ -1208,10 +1376,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 (warn_if_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 +1414,10 @@ struct OptDffWorker
 
 				n_lit[idx] = n;
 			}
+			qcsat.prepare();
+			sat_budget.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 +1454,9 @@ struct OptDffWorker
 				if (n_lit[rep] == n_lit[cls[i]])
 					continue;
 
+				if (warn_if_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 +1468,14 @@ struct OptDffWorker
 				std::vector<bool> modelVals;
 				assumptions.push_back(query);
 
-				if (qcsat.ez->solve(modelExprs, modelVals, assumptions)) {
+				auto res = sat_budget.solve(qcsat, 0, modelExprs, modelVals, assumptions);
+
+				if (res == SatEffortBudget::Result::LimitReached) {
+					warn_if_budget_spent();
+					return drop_all_classes();
+				}
+
+				if (res == SatEffortBudget::Result::Sat) {
 					// SAT -> partition entire class
 					std::vector<int> sub0;
 					std::vector<int> sub1;
@@ -1427,6 +1608,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");

tests/opt/opt_dff_sat_effort.ys

@@ -0,0 +1,67 @@
+design -reset
+read_verilog -sv <<EOT
+module test_case (
+	input wire clk,
+	input wire [3:0] a,
+	input wire [3:0] b,
+	output reg y0,
+	output reg y1,
+	output reg y2,
+	output reg y3
+);
+	initial begin
+		y0 = 1'b0;
+		y1 = 1'b0;
+		y2 = 1'b0;
+		y3 = 1'b0;
+	end
+	always @(posedge clk) begin
+		y0 <= (a > 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 "solver effort budget for module test_case is exhausted" 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