aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-08-15 11:40:01 +0200
committerClifford Wolf <clifford@clifford.at>2013-08-15 11:40:01 +0200
commit2f3da54f269fac5dab4b03eec80182c534f8c28f (patch)
treeb2da83064fd40f50b46aa958a55e7415b893214e /passes/sat
parentd0e93e04d1cc196264b0bbcf1aafcfba0adb2ea0 (diff)
downloadyosys-2f3da54f269fac5dab4b03eec80182c534f8c28f.tar.gz
yosys-2f3da54f269fac5dab4b03eec80182c534f8c28f.tar.bz2
yosys-2f3da54f269fac5dab4b03eec80182c534f8c28f.zip
Added sat -ignore_div_by_zero switch
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/sat.cc12
1 files changed, 11 insertions, 1 deletions
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();