summaryrefslogtreecommitdiff
path: root/passes/sat/sat.cc
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat/sat.cc')
-rw-r--r--passes/sat/sat.cc67
1 files changed, 62 insertions, 5 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 3000c54a..769d94a0 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -52,12 +52,15 @@ struct SatHelper
std::vector<std::string> shows;
SigPool show_signal_pool;
SigSet<RTLIL::Cell*> show_drivers;
- int max_timestep;
+ int max_timestep, timeout;
+ bool gotTimeout;
SatHelper(RTLIL::Design *design, RTLIL::Module *module) :
design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
{
max_timestep = -1;
+ timeout = 0;
+ gotTimeout = false;
}
void setup(int timestep = -1)
@@ -190,12 +193,22 @@ struct SatHelper
bool solve(const std::vector<int> &assumptions)
{
- return ez.solve(modelExpressions, modelValues, assumptions);
+ log_assert(gotTimeout == false);
+ ez.setSolverTimeout(timeout);
+ bool success = ez.solve(modelExpressions, modelValues, assumptions);
+ if (ez.getSolverTimoutStatus())
+ gotTimeout = true;
+ return success;
}
bool solve(int a = 0, int b = 0, int c = 0, int d = 0, int e = 0, int f = 0)
{
- return ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
+ log_assert(gotTimeout == false);
+ ez.setSolverTimeout(timeout);
+ bool success = ez.solve(modelExpressions, modelValues, a, b, c, d, e, f);
+ if (ez.getSolverTimoutStatus())
+ gotTimeout = true;
+ return success;
}
struct ModelBlockInfo {
@@ -380,6 +393,17 @@ static void print_proof_failed()
log("\n");
}
+static void print_timeout()
+{
+ log("\n");
+ log(" _____ _ _ _____ ____ _ _____\n");
+ log(" /__ __\\/ \\/ \\__/|/ __// _ \\/ \\ /\\/__ __\\\n");
+ log(" / \\ | || |\\/||| \\ | / \\|| | || / \\\n");
+ log(" | | | || | ||| /_ | \\_/|| \\_/| | |\n");
+ log(" \\_/ \\_/\\_/ \\|\\____\\\\____/\\____/ \\_/\n");
+ log("\n");
+}
+
static void print_qed()
{
log("\n");
@@ -442,9 +466,15 @@ struct SatPass : public Pass {
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
+ log(" -timeout <N>\n");
+ log(" Maximum number of seconds a single SAT instance may take.\n");
+ log("\n");
log(" -verify\n");
log(" Return an error and stop the synthesis script if the proof fails.\n");
log("\n");
+ log(" -verify-no-timeout\n");
+ log(" Like -verify but do not return an error for timeouts.\n");
+ log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
@@ -452,8 +482,8 @@ struct SatPass : public Pass {
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at;
std::vector<std::string> shows;
- int loopcount = 0, seq_len = 0, maxsteps = 0;
- bool verify = false;
+ int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
+ bool verify = false, fail_on_timeout = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -464,9 +494,18 @@ struct SatPass : public Pass {
continue;
}
if (args[argidx] == "-verify") {
+ fail_on_timeout = true;
verify = true;
continue;
}
+ if (args[argidx] == "-verify-no-timeout") {
+ verify = true;
+ continue;
+ }
+ if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
+ timeout = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-max" && argidx+1 < args.size()) {
loopcount = atoi(args[++argidx].c_str());
continue;
@@ -539,6 +578,7 @@ struct SatPass : public Pass {
basecase.sets_at = sets_at;
basecase.unsets_at = unsets_at;
basecase.shows = shows;
+ basecase.timeout = timeout;
for (int timestep = 1; timestep <= seq_len; timestep++)
basecase.setup(timestep);
@@ -546,6 +586,7 @@ struct SatPass : public Pass {
inductstep.sets = sets;
inductstep.prove = prove;
inductstep.shows = shows;
+ inductstep.timeout = timeout;
inductstep.setup(1);
inductstep.ez.assume(inductstep.setup_proof(1));
@@ -573,6 +614,9 @@ struct SatPass : public Pass {
goto tip_failed;
}
+ if (basecase.gotTimeout)
+ goto timeout;
+
log("Base case for induction length %d proven.\n", inductlen);
basecase.ez.assume(property);
@@ -589,6 +633,8 @@ struct SatPass : public Pass {
inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
if (!inductstep.solve(inductstep.ez.NOT(property))) {
+ if (inductstep.gotTimeout)
+ goto timeout;
log("Induction step proven: SUCCESS!\n");
print_qed();
goto tip_success;
@@ -622,6 +668,7 @@ struct SatPass : public Pass {
sathelper.sets_at = sets_at;
sathelper.unsets_at = unsets_at;
sathelper.shows = shows;
+ sathelper.timeout = timeout;
if (seq_len == 0) {
sathelper.setup();
@@ -668,6 +715,8 @@ struct SatPass : public Pass {
}
else
{
+ if (sathelper.gotTimeout)
+ goto timeout;
if (did_rerun)
log("SAT solving finished - no more models found.\n");
else if (prove.size() == 0)
@@ -678,6 +727,14 @@ struct SatPass : public Pass {
}
}
}
+
+ if (0) {
+ timeout:
+ log("Interrupted SAT solver: TIMEOUT!\n");
+ print_timeout();
+ if (fail_on_timeout)
+ log_error("Called with -verify and proof did time out!\n");
+ }
}
} SatPass;