diff options
| -rw-r--r-- | kernel/satgen.h | 7 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 12 |
2 files changed, 17 insertions, 2 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index b2f8b15b..5b4abfc2 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 c7520423..31808503 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(); |