From 7d790febb040ae153a4db9be725f4d9709a49843 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 10 Jun 2013 16:09:29 +0200
Subject: [PATCH] Improvements and fixes in SAT code

---
 kernel/satgen.h   | 27 ++++++++++++++++++++++-----
 passes/sat/sat.cc | 18 ++++++++++++++----
 2 files changed, 36 insertions(+), 9 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index b7bd87dd4..5b3a4d041 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -74,22 +74,22 @@ struct SatGen
 		return vec;
 	}
 
-	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell)
+	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0)
 	{
 		bool is_signed_a = false, is_signed_b = false;
 		if (cell->parameters.count("\\A_SIGNED") > 0)
 			is_signed_a = cell->parameters["\\A_SIGNED"].as_bool();
 		if (cell->parameters.count("\\B_SIGNED") > 0)
 			is_signed_b = cell->parameters["\\B_SIGNED"].as_bool();
-		while (vec_a.size() < vec_b.size())
+		while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
 			vec_a.push_back(is_signed_a && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
-		while (vec_b.size() < vec_a.size())
+		while (vec_b.size() < vec_a.size() || vec_b.size() < y_width)
 			vec_b.push_back(is_signed_b && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
 	}
 
 	void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell)
 	{
-		extendSignalWidth(vec_a, vec_b, cell);
+		extendSignalWidth(vec_a, vec_b, cell, vec_y.size());
 		while (vec_y.size() < vec_a.size())
 			vec_y.push_back(ez->literal());
 	}
@@ -239,6 +239,23 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$mul") {
+			std::vector<int> a = importSigSpec(cell->connections.at("\\A"), timestep);
+			std::vector<int> b = importSigSpec(cell->connections.at("\\B"), timestep);
+			std::vector<int> y = importSigSpec(cell->connections.at("\\Y"), timestep);
+			extendSignalWidth(a, b, y, cell);
+			std::vector<int> tmp(a.size(), ez->FALSE);
+			for (int i = 0; i < int(a.size()); i++)
+			{
+				std::vector<int> shifted_a(a.size(), ez->FALSE);
+				for (int j = i; j < int(a.size()); j++)
+					shifted_a.at(j) = a.at(j-i);
+				tmp = ez->vec_ite(b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+			}
+			ez->assume(ez->vec_eq(tmp, y));
+			return true;
+		}
+
 		if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) {
 			if (timestep == 1) {
 				initial_state.add((*sigmap)(cell->connections.at("\\Q")));
@@ -250,7 +267,7 @@ struct SatGen
 			return true;
 		}
 
-		// Unsupported internal cell types: $mul $div $mod $pow
+		// Unsupported internal cell types: $div $mod $pow
 		// .. and all sequential cells except $dff and $_DFF_[NP]_
 		return false;
 	}
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index a13f83183..e5f678820 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -41,6 +41,11 @@ static void split(std::vector<std::string> &tokens, const std::string &text, cha
 	tokens.push_back(text.substr(start));
 }
 
+static int get_dummy_line_num()
+{
+	return 0;
+}
+
 static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string str)
 {
 	std::vector<std::string> tokens;
@@ -56,6 +61,7 @@ static bool parse_sigstr(RTLIL::SigSpec &sig, RTLIL::Module *module, std::string
 			continue;
 
 		if ('0' <= netname[0] && netname[0] <= '9') {
+			AST::get_line_num = get_dummy_line_num;
 			AST::AstNode *ast = VERILOG_FRONTEND::const2ast(netname);
 			if (ast == NULL)
 				return false;
@@ -320,7 +326,7 @@ struct SatHelper
 							continue;
 						if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
 							continue;
-						queued_signals.add(handled_signals.remove(p.second));
+						queued_signals.add(handled_signals.remove(sigmap(p.second)));
 					}
 				}
 			}
@@ -712,6 +718,8 @@ struct SatPass : public Pass {
 			sathelper.ez.printDIMACS(stdout, true);
 #endif
 
+			bool did_rerun = false;
+
 		rerun_solver:
 			log("\nSolving problem with %d variables and %d clauses..\n",
 					sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());
@@ -733,16 +741,18 @@ struct SatPass : public Pass {
 				}
 
 				if (loopcount != 0) {
-					loopcount--;
+					loopcount--, did_rerun = true;
 					sathelper.invalidate_model();
 					goto rerun_solver;
 				}
 			}
 			else
 			{
-				if (prove.size() == 0) {
+				if (did_rerun)
+					log("SAT solving finished - no more models found.\n");
+				else if (prove.size() == 0)
 					log("SAT solving finished - no model found.\n");
-				} else {
+				else {
 					log("SAT proof finished - no model found: SUCCESS!\n");
 					print_qed();
 				}
-- 
2.30.2