Added sat -ignore_div_by_zero switch

diff --git a/kernel/satgen.h b/kernel/satgen.h
index b2f8b15b72a411ff5f923ebb51fae0a5d8a90f73..5b4abfc215023696ab65fd5d7f4a54f45a76d0db 100644 (file)
--- 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 c75204230ceb83ddf692f3ffa379d26727908d3b..31808503efe484b5a511b62d935e14f14ba52d66 100644 (file)
--- 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();