mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-06-06 22:23:23 +00:00
Code Activity

Added sat -ignore_div_by_zero switch

Browse source
This commit is contained in:
Clifford Wolf 2013-08-15 11:40:01 +02:00
parent d0e93e04d1
commit 2f3da54f26
2 changed files with 17 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
kernel/satgen.h
View file

@ -39,9 +39,10 @@ struct SatGen
SigMap *sigmap; SigMap *sigmap;
std::string prefix; std::string prefix;
SigPool initial_state; SigPool initial_state;
bool ignore_div_by_zero;
SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) : 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 else
ez->assume(ez->vec_eq(y, chain_buf)); ez->assume(ez->vec_eq(y, chain_buf));
} }
if (ignore_div_by_zero)
ez->assume(ez->expression(ezSAT::OpOr, b));
return true; return true;
} }

12
passes/sat/sat.cc
View file

@ -444,6 +444,9 @@ struct SatPass : public Pass {
log(" show the model for the specified signal. if no -show option is\n"); 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(" passed then a set of signals to be shown is automatically selected.\n");
log("\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("The following options can be used to set up a sequential problem:\n");
log("\n"); log("\n");
log(" -seq <N>\n"); log(" -seq <N>\n");
@ -483,7 +486,7 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::string>> unsets_at; std::map<int, std::vector<std::string>> unsets_at;
std::vector<std::string> shows; std::vector<std::string> shows;
int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0; 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"); 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()); maxsteps = atoi(args[++argidx].c_str());
continue; 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()) { if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx].c_str(); std::string lhs = args[++argidx].c_str();
std::string rhs = 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.unsets_at = unsets_at;
basecase.shows = shows; basecase.shows = shows;
basecase.timeout = timeout; basecase.timeout = timeout;
basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
for (int timestep = 1; timestep <= seq_len; timestep++) for (int timestep = 1; timestep <= seq_len; timestep++)
basecase.setup(timestep); basecase.setup(timestep);
@ -587,6 +595,7 @@ struct SatPass : public Pass {
inductstep.prove = prove; inductstep.prove = prove;
inductstep.shows = shows; inductstep.shows = shows;
inductstep.timeout = timeout; inductstep.timeout = timeout;
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
inductstep.setup(1); inductstep.setup(1);
inductstep.ez.assume(inductstep.setup_proof(1)); inductstep.ez.assume(inductstep.setup_proof(1));
@ -669,6 +678,7 @@ struct SatPass : public Pass {
sathelper.unsets_at = unsets_at; sathelper.unsets_at = unsets_at;
sathelper.shows = shows; sathelper.shows = shows;
sathelper.timeout = timeout; sathelper.timeout = timeout;
sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
if (seq_len == 0) { if (seq_len == 0) {
sathelper.setup(); sathelper.setup();