From 2f3da54f269fac5dab4b03eec80182c534f8c28f Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 15 Aug 2013 11:40:01 +0200
Subject: [PATCH] Added sat -ignore_div_by_zero switch

---
 kernel/satgen.h   |  7 ++++++-
 passes/sat/sat.cc | 12 +++++++++++-
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index b2f8b15b7..5b4abfc21 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -39,9 +39,10 @@ struct SatGen
 	SigMap *sigmap;
 	std::string prefix;
 	SigPool initial_state;
+	bool ignore_div_by_zero;
 
 	SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
-			ez(ez), design(design), sigmap(sigmap), prefix(prefix)
+			ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false)
 	{
 	}
 
@@ -310,6 +311,10 @@ struct SatGen
 				else
 					ez->assume(ez->vec_eq(y, chain_buf));
 			}
+
+			if (ignore_div_by_zero)
+				ez->assume(ez->expression(ezSAT::OpOr, b));
+
 			return true;
 		}
 
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index c75204230..31808503e 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -444,6 +444,9 @@ struct SatPass : public Pass {
 		log("        show the model for the specified signal. if no -show option is\n");
 		log("        passed then a set of signals to be shown is automatically selected.\n");
 		log("\n");
+		log("    -ignore_div_by_zero\n");
+		log("        ignore all solutions that involve a division by zero\n");
+		log("\n");
 		log("The following options can be used to set up a sequential problem:\n");
 		log("\n");
 		log("    -seq <N>\n");
@@ -483,7 +486,7 @@ struct SatPass : public Pass {
 		std::map<int, std::vector<std::string>> unsets_at;
 		std::vector<std::string> shows;
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
-		bool verify = false, fail_on_timeout = false;
+		bool verify = false, fail_on_timeout = false, ignore_div_by_zero = false;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -514,6 +517,10 @@ struct SatPass : public Pass {
 				maxsteps = atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-ignore_div_by_zero" && argidx+1 < args.size()) {
+				ignore_div_by_zero = true;
+				continue;
+			}
 			if (args[argidx] == "-set" && argidx+2 < args.size()) {
 				std::string lhs = args[++argidx].c_str();
 				std::string rhs = args[++argidx].c_str();
@@ -579,6 +586,7 @@ struct SatPass : public Pass {
 			basecase.unsets_at = unsets_at;
 			basecase.shows = shows;
 			basecase.timeout = timeout;
+			basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
 
 			for (int timestep = 1; timestep <= seq_len; timestep++)
 				basecase.setup(timestep);
@@ -587,6 +595,7 @@ struct SatPass : public Pass {
 			inductstep.prove = prove;
 			inductstep.shows = shows;
 			inductstep.timeout = timeout;
+			inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
 
 			inductstep.setup(1);
 			inductstep.ez.assume(inductstep.setup_proof(1));
@@ -669,6 +678,7 @@ struct SatPass : public Pass {
 			sathelper.unsets_at = unsets_at;
 			sathelper.shows = shows;
 			sathelper.timeout = timeout;
+			sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
 
 			if (seq_len == 0) {
 				sathelper.setup();
-- 
2.30.2