From bc541b47ea0ceb2556b54bd5310d11c1d77a5d3d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Jan 2014 13:10:51 +0100
Subject: [PATCH] Improved performance of freduce input cone reduction

---
 passes/sat/freduce.cc | 101 ++++++++++++++++++++++++++++++++----------
 1 file changed, 78 insertions(+), 23 deletions(-)

diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 9ccce167a..81250b000 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -75,12 +75,59 @@ struct FindReducedInputs
 	std::set<RTLIL::Cell*> ez_cells;
 	SatGen satgen;
 
+	std::map<RTLIL::SigBit, int> sat_pi;
+	std::vector<int> sat_pi_uniq_bitvec;
+
 	FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
 			sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
 	{
 		satgen.model_undef = true;
 	}
 
+	int get_bits(int val)
+	{
+		int bits = 0;
+		for (int i = 8*sizeof(int); val; i = i >> 1)
+			if (val >> (i-1)) {
+				bits += i;
+				val = val >> i;
+			}
+		return bits;
+	}
+
+	void register_pi_bit(RTLIL::SigBit bit)
+	{
+		if (sat_pi.count(bit) != 0)
+			return;
+
+		satgen.setContext(&sigmap, "A");
+		int sat_a = satgen.importSigSpec(bit).front();
+		ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+
+		satgen.setContext(&sigmap, "B");
+		int sat_b = satgen.importSigSpec(bit).front();
+		ez.assume(ez.NOT(satgen.importUndefSigSpec(bit).front()));
+
+		int idx = sat_pi.size();
+		size_t idx_bits = get_bits(idx);
+
+		if (sat_pi_uniq_bitvec.size() != idx_bits) {
+			sat_pi_uniq_bitvec.push_back(ez.literal(stringf("uniq_%d", int(idx_bits)-1)));
+			for (auto &it : sat_pi)
+				ez.assume(ez.OR(ez.NOT(it.second), ez.NOT(sat_pi_uniq_bitvec.back())));
+		}
+		log_assert(sat_pi_uniq_bitvec.size() == idx_bits);
+
+		sat_pi[bit] = ez.literal(stringf("pi_%s", log_signal(bit)));
+		ez.assume(ez.IFF(ez.XOR(sat_a, sat_b), sat_pi[bit]));
+
+		for (size_t i = 0; i < idx_bits; i++)
+			if ((idx & (1 << i)) == 0)
+				ez.assume(ez.OR(ez.NOT(sat_pi[bit]), ez.NOT(sat_pi_uniq_bitvec[i])));
+			else
+				ez.assume(ez.OR(ez.NOT(sat_pi[bit]), sat_pi_uniq_bitvec[i]));
+	}
+
 	void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
 	{
 		if (out.wire == NULL)
@@ -102,8 +149,10 @@ struct FindReducedInputs
 			}
 			for (auto &bit : drv.second)
 				register_cone_worker(pi, sigdone, bit);
-		} else
+		} else {
+			register_pi_bit(out);
 			pi.insert(out);
+		}
 	}
 
 	void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out)
@@ -128,39 +177,45 @@ struct FindReducedInputs
 		satgen.setContext(&sigmap, "A");
 		int output_a = satgen.importSigSpec(output).front();
 		int output_undef_a = satgen.importUndefSigSpec(output).front();
-		ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
 
 		satgen.setContext(&sigmap, "B");
 		int output_b = satgen.importSigSpec(output).front();
 		int output_undef_b = satgen.importUndefSigSpec(output).front();
-		ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+		std::set<int> unused_pi_idx;
 
 		for (size_t i = 0; i < pi.size(); i++)
-		{
-			RTLIL::SigSpec test_sig(pi[i]);
-			RTLIL::SigSpec rest_sig(pi);
-			rest_sig.remove(i, 1);
+			unused_pi_idx.insert(i);
 
-			int test_sig_a, test_sig_b;
-			std::vector<int> rest_sig_a, rest_sig_b;
+		while (1)
+		{
+			std::vector<int> model_pi_idx;
+			std::vector<int> model_expr;
+			std::vector<bool> model;
+
+			for (size_t i = 0; i < pi.size(); i++)
+				if (unused_pi_idx.count(i) != 0) {
+					model_pi_idx.push_back(i);
+					model_expr.push_back(sat_pi.at(pi[i]));
+				}
 
-			satgen.setContext(&sigmap, "A");
-			test_sig_a = satgen.importSigSpec(test_sig).front();
-			rest_sig_a = satgen.importSigSpec(rest_sig);
+			if (!ez.solve(model_expr, model, ez.expression(ezSAT::OpOr, model_expr), ez.XOR(output_a, output_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b)))
+				break;
 
-			satgen.setContext(&sigmap, "B");
-			test_sig_b = satgen.importSigSpec(test_sig).front();
-			rest_sig_b = satgen.importSigSpec(rest_sig);
+			int found_count = 0;
+			for (size_t i = 0; i < model_pi_idx.size(); i++)
+				if (model[i]) {
+					if (verbose_level >= 2)
+						log("         Found relevant input: %s\n", log_signal(pi[model_pi_idx[i]]));
+					unused_pi_idx.erase(model_pi_idx[i]);
+					found_count++;
+				}
+			log_assert(found_count == 1);
+		}
 
-			if (ez.solve(ez.vec_eq(rest_sig_a, rest_sig_b), ez.XOR(output_a, output_b), ez.XOR(test_sig_a, test_sig_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) {
-				if (verbose_level >= 2)
-					log("         Result for input %s: pass\n", log_signal(test_sig));
+		for (size_t i = 0; i < pi.size(); i++)
+			if (unused_pi_idx.count(i) == 0)
 				reduced_inputs.push_back(pi[i]);
-			} else {
-				if (verbose_level >= 2)
-					log("         Result for input %s: strip\n", log_signal(test_sig));
-			}
-		}
 
 		if (verbose_level >= 1)
 			log("         Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
-- 
2.30.2