Refactor common parts of SAT-using optimizations into a helper.

This also aligns the functionality:

- in all cases, the onehot attribute is used to create appropriate
  constraints (previously, opt_dff didn't do it at all, and share
  created one-hot constraints based on $pmux presence alone, which
  is unsound)
- in all cases, shift and mul/div/pow cells are now skipped when
  importing the SAT problem (previously only memory_share did this)
  — this avoids creating clauses for hard cells that are unlikely
  to help with proving the UNSATness needed for optimization

2 files changed, 30 insertions, 89 deletions

diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc
index 94d6d5443..ddf08392b 100644
--- a/passes/opt/opt_dff.cc
+++ b/passes/opt/opt_dff.cc
@@ -21,7 +21,8 @@
 #include "kernel/log.h"
 #include "kernel/register.h"
 #include "kernel/rtlil.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
+#include "kernel/modtools.h"
 #include "kernel/sigtools.h"
 #include "kernel/ffinit.h"
 #include "kernel/ff.h"
@@ -51,26 +52,23 @@ struct OptDffWorker
 	FfInitVals initvals;
 	dict<SigBit, int> bitusers;
 	dict<SigBit, cell_int_t> bit2mux;
-	dict<SigBit, RTLIL::Cell*> bit2driver;
 
 	typedef std::map<RTLIL::SigBit, bool> pattern_t;
 	typedef std::set<pattern_t> patterns_t;
 	typedef std::pair<RTLIL::SigBit, bool> ctrl_t;
 	typedef std::set<ctrl_t> ctrls_t;
 
-	ezSatPtr ez;
-	SatGen satgen;
-	pool<Cell*> sat_cells;
+	ModWalker modwalker;
+	QuickConeSat qcsat;
 
 	// Used as a queue.
 	std::vector<Cell *> dff_cells;
 
-	OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), ez(), satgen(ez.get(), &sigmap) {
-		// Gathering three kinds of information here for every sigmapped SigBit:
+	OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), modwalker(module->design, module), qcsat(modwalker) {
+		// Gathering two kinds of information here for every sigmapped SigBit:
 		//
 		// - bitusers: how many users it has (muxes will only be merged into FFs if this is 1, making the FF the only user)
 		// - bit2mux: the mux cell and bit index that drives it, if any
-		// - bit2driver: the cell driving it, if any
 
 		for (auto wire : module->wires())
 		{
@@ -88,10 +86,6 @@ struct OptDffWorker
 
 			for (auto conn : cell->connections()) {
 				bool is_output = cell->output(conn.first);
-				if (is_output) {
-					for (auto bit : sigmap(conn.second))
-						bit2driver[bit] = cell;
-				}
 				if (!is_output || !cell->known()) {
 					for (auto bit : sigmap(conn.second))
 						bitusers[bit]++;
@@ -104,20 +98,6 @@ struct OptDffWorker
 
 	}
 
-	std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
-		if (!sat_cells.insert(c).second)
-			return;
-		if (!satgen.importCell(c))
-			return;
-		for (auto &conn : c->connections()) {
-			if (!c->input(conn.first))
-				continue;
-			for (auto bit : sigmap(conn.second))
-				if (bit2driver.count(bit))
-					sat_import_cell(bit2driver.at(bit));
-		}
-	};
-
 	State combine_const(State a, State b) {
 		if (a == State::Sx && !opt.keepdc)
 			return b;
@@ -594,19 +574,19 @@ struct OptDffWorker
 						if (!opt.sat)
 							continue;
 						// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
-						if (!bit2driver.count(ff.sig_d[i]))
+						if (!modwalker.has_drivers(ff.sig_d.extract(i)))
 							continue;
 						if (val != State::S0 && val != State::S1)
 							continue;
 
-						sat_import_cell(bit2driver.at(ff.sig_d[i]));
+						int init_sat_pi = qcsat.importSigBit(val);
+						int q_sat_pi = qcsat.importSigBit(ff.sig_q[i]);
+						int d_sat_pi = qcsat.importSigBit(ff.sig_d[i]);
 
-						int init_sat_pi = satgen.importSigSpec(val).front();
-						int q_sat_pi = satgen.importSigBit(ff.sig_q[i]);
-						int d_sat_pi = satgen.importSigBit(ff.sig_d[i]);
+						qcsat.prepare();
 
 						// Try to find out whether the register bit can change under some circumstances
-						bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
+						bool counter_example_found = qcsat.ez->solve(qcsat.ez->IFF(q_sat_pi, init_sat_pi), qcsat.ez->NOT(qcsat.ez->IFF(d_sat_pi, init_sat_pi)));
 
 						// If the register bit cannot change, we can replace it with a constant
 						if (counter_example_found)
diff --git a/passes/opt/share.cc b/passes/opt/share.cc
index 88c4dee8b..ee1acfb7f 100644
--- a/passes/opt/share.cc
+++ b/passes/opt/share.cc
@@ -18,7 +18,7 @@
  */
 
 #include "kernel/yosys.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
 #include "kernel/sigtools.h"
 #include "kernel/modtools.h"
 #include "kernel/utils.h"
@@ -58,8 +58,6 @@ struct ShareWorker
 	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;
 
-	std::vector<std::pair<RTLIL::SigBit, RTLIL::SigBit>> exclusive_ctrls;
-
 
 	// ------------------------------------------------------------------------------
 	// Find terminal bits -- i.e. bits that do not (exclusively) feed into a mux tree
@@ -1156,7 +1154,6 @@ struct ShareWorker
 		recursion_state.clear();
 		topo_cell_drivers.clear();
 		topo_bit_drivers.clear();
-		exclusive_ctrls.clear();
 		terminal_bits.clear();
 		shareable_cells.clear();
 		forbidden_controls_cache.clear();
@@ -1171,13 +1168,6 @@ struct ShareWorker
 		log("Found %d cells in module %s that may be considered for resource sharing.\n",
 				GetSize(shareable_cells), log_id(module));
 
-		for (auto cell : module->cells())
-			if (cell->type == ID($pmux))
-				for (auto bit : cell->getPort(ID::S))
-				for (auto other_bit : cell->getPort(ID::S))
-					if (bit < other_bit)
-						exclusive_ctrls.push_back(std::pair<RTLIL::SigBit, RTLIL::SigBit>(bit, other_bit));
-
 		while (!shareable_cells.empty() && config.limit != 0)
 		{
 			RTLIL::Cell *cell = *shareable_cells.begin();
@@ -1256,8 +1246,11 @@ struct ShareWorker
 				optimize_activation_patterns(filtered_cell_activation_patterns);
 				optimize_activation_patterns(filtered_other_cell_activation_patterns);
 
-				ezSatPtr ez;
-				SatGen satgen(ez.get(), &modwalker.sigmap);
+				QuickConeSat qcsat(modwalker);
+				if (config.opt_fast) {
+					qcsat.max_cell_outs = 3;
+					qcsat.max_cell_count = 100;
+				}
 
 				pool<RTLIL::Cell*> sat_cells;
 				std::set<RTLIL::SigBit> bits_queue;
@@ -1267,77 +1260,45 @@ struct ShareWorker
 
 				for (auto &p : filtered_cell_activation_patterns) {
 					log("      Activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second));
-					cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
+					cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
 					all_ctrl_signals.append(p.first);
 				}
 
 				for (auto &p : filtered_other_cell_activation_patterns) {
 					log("      Activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second));
-					other_cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
+					other_cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
 					all_ctrl_signals.append(p.first);
 				}
 
-				for (auto &bit : cell_activation_signals.to_sigbit_vector())
-					bits_queue.insert(bit);
-
-				for (auto &bit : other_cell_activation_signals.to_sigbit_vector())
-					bits_queue.insert(bit);
-
-				while (!bits_queue.empty())
-				{
-					pool<ModWalker::PortBit> portbits;
-					modwalker.get_drivers(portbits, bits_queue);
-					bits_queue.clear();
-
-					for (auto &pbit : portbits)
-						if (sat_cells.count(pbit.cell) == 0 && cone_ct.cell_known(pbit.cell->type)) {
-							if (config.opt_fast && modwalker.cell_outputs[pbit.cell].size() >= 4)
-								continue;
-							// log("      Adding cell %s (%s) to SAT problem.\n", log_id(pbit.cell), log_id(pbit.cell->type));
-							bits_queue.insert(modwalker.cell_inputs[pbit.cell].begin(), modwalker.cell_inputs[pbit.cell].end());
-							satgen.importCell(pbit.cell);
-							sat_cells.insert(pbit.cell);
-						}
-
-					if (config.opt_fast && sat_cells.size() > 100)
-						break;
-				}
-
-				for (auto it : exclusive_ctrls)
-					if (satgen.importedSigBit(it.first) && satgen.importedSigBit(it.second)) {
-						log("      Adding exclusive control bits: %s vs. %s\n", log_signal(it.first), log_signal(it.second));
-						int sub1 = satgen.importSigBit(it.first);
-						int sub2 = satgen.importSigBit(it.second);
-						ez->assume(ez->NOT(ez->AND(sub1, sub2)));
-					}
+				qcsat.prepare();
 
-				if (!ez->solve(ez->expression(ez->OpOr, cell_active))) {
+				int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active);
+				if (!qcsat.ez->solve(sub1)) {
 					log("      According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell));
 					cells_to_remove.insert(cell);
 					break;
 				}
 
-				if (!ez->solve(ez->expression(ez->OpOr, other_cell_active))) {
+				int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active);
+				if (!qcsat.ez->solve(sub2)) {
 					log("      According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell));
 					cells_to_remove.insert(other_cell);
 					shareable_cells.erase(other_cell);
 					continue;
 				}
 
-				ez->non_incremental();
+				qcsat.ez->non_incremental();
 
 				all_ctrl_signals.sort_and_unify();
-				std::vector<int> sat_model = satgen.importSigSpec(all_ctrl_signals);
+				std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
 				std::vector<bool> sat_model_values;
 
-				int sub1 = ez->expression(ez->OpOr, cell_active);
-				int sub2 = ez->expression(ez->OpOr, other_cell_active);
-				ez->assume(ez->AND(sub1, sub2));
+				qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
 
 				log("      Size of SAT problem: %d cells, %d variables, %d clauses\n",
-						GetSize(sat_cells), ez->numCnfVariables(), ez->numCnfClauses());
+						GetSize(sat_cells), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
 
-				if (ez->solve(sat_model, sat_model_values)) {
+				if (qcsat.ez->solve(sat_model, sat_model_values)) {
 					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--)