From 8fbb5b62400edf82f6719eda90a75730d467db83 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 20 Jun 2013 12:49:10 +0200 Subject: [PATCH] Added timout functionality to SAT solver --- libs/ezsat/ezminisat.cc | 38 +++++++++++++++++++- libs/ezsat/ezminisat.h | 5 +++ libs/ezsat/ezsat.cc | 3 ++ libs/ezsat/ezsat.h | 11 ++++++ passes/sat/sat.cc | 67 +++++++++++++++++++++++++++++++++--- tests/xsthammer/run-check.sh | 4 +-- 6 files changed, 120 insertions(+), 8 deletions(-) diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index c34ad7480..56f04fefd 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -23,6 +23,7 @@ #include #include +#include #include #include "minisat/core/Solver.h" @@ -50,8 +51,22 @@ void ezMiniSAT::clear() ezSAT::clear(); } +ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL; +clock_t ezMiniSAT::alarmHandlerTimeout = 0; + +void ezMiniSAT::alarmHandler(int) +{ + if (clock() > alarmHandlerTimeout) { + alarmHandlerThis->minisatSolver->interrupt(); + alarmHandlerTimeout = 0; + } else + alarm(1); +} + bool ezMiniSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { + solverTimoutStatus = false; + if (0) { contradiction: delete minisatSolver; @@ -104,7 +119,28 @@ contradiction: else assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true)); - if (!minisatSolver->solve(assumps)) + sighandler_t old_alarm_sighandler; + int old_alarm_timeout; + + if (solverTimeout > 0) { + alarmHandlerThis = this; + alarmHandlerTimeout = clock() + solverTimeout*CLOCKS_PER_SEC; + old_alarm_timeout = alarm(0); + old_alarm_sighandler = signal(SIGALRM, alarmHandler); + alarm(1); + } + + bool foundSolution = minisatSolver->solve(assumps); + + if (solverTimeout > 0) { + if (alarmHandlerTimeout == 0) + solverTimoutStatus = true; + alarm(0); + signal(SIGALRM, old_alarm_sighandler); + alarm(old_alarm_timeout); + } + + if (!foundSolution) return false; modelValues.clear(); diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h index 4171985b6..2919aa2e3 100644 --- a/libs/ezsat/ezminisat.h +++ b/libs/ezsat/ezminisat.h @@ -21,6 +21,7 @@ #define EZMINISAT_H #include "ezsat.h" +#include // minisat is using limit macros and format macros in their headers that // can be the source of some troubles when used from c++11. thefore we @@ -36,6 +37,10 @@ private: std::vector minisatVars; bool foundContradiction; + static ezMiniSAT *alarmHandlerThis; + static clock_t alarmHandlerTimeout; + static void alarmHandler(int); + public: ezMiniSAT(); virtual ~ezMiniSAT(); diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index e37031314..00918f62f 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -38,6 +38,9 @@ ezSAT::ezSAT() cnfConsumed = false; cnfVariableCount = 0; cnfClausesCount = 0; + + solverTimeout = 0; + solverTimoutStatus = false; } ezSAT::~ezSAT() diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 2674d83df..2d0307d51 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -69,6 +69,9 @@ private: int bind_cnf_or(const std::vector &args); public: + int solverTimeout; + bool solverTimoutStatus; + ezSAT(); virtual ~ezSAT(); @@ -130,6 +133,14 @@ public: return solver(modelExpressions, modelValues, assumptions); } + void setSolverTimeout(int newTimeoutSeconds) { + solverTimeout = newTimeoutSeconds; + } + + bool getSolverTimoutStatus() { + return solverTimoutStatus; + } + // manage CNF (usually only accessed by SAT solvers) virtual void clear(); diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 3000c54a0..769d94a07 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -52,12 +52,15 @@ struct SatHelper std::vector shows; SigPool show_signal_pool; SigSet 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 &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"); log(" Set a maximum length for the induction.\n"); log("\n"); + log(" -timeout \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 args, RTLIL::Design *design) { @@ -452,8 +482,8 @@ struct SatPass : public Pass { std::map>> sets_at; std::map> unsets_at; std::vector 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; diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh index 994f4d923..3dd63b599 100644 --- a/tests/xsthammer/run-check.sh +++ b/tests/xsthammer/run-check.sh @@ -51,8 +51,8 @@ done { echo "read_ilang ${job}_top_nomap.il" echo "read_ilang ${job}_top_techmap.il" - echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_nomap" - echo "sat -verify -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_techmap" + echo "sat -timeout 60 -verify-no-timeout -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_nomap" + echo "sat -timeout 60 -verify-no-timeout -show a,b,y_rtl,y_xst -prove y_rtl y_xst ${job}_top_techmap" if [[ $job != expression_* ]]; then echo "eval -brute_force_equiv_checker ${job}_rtl_nomap ${job}_xst_nomap" echo "eval -brute_force_equiv_checker ${job}_rtl_techmap ${job}_xst_techmap" -- 2.30.2