Added timout functionality to SAT solver

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index c34ad7480e087bf5e85aeed588605940b98df8e3..56f04fefda7b24eec9de9067862ac30ef9881005 100644 (file)
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -23,6 +23,7 @@
 
 #include <limits.h>
 #include <stdint.h>
+#include <signal.h>
 #include <cinttypes>
 
 #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<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &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 4171985b6dfcda4cbb18a32cbcf057ecf593fe2e..2919aa2e3b45c8d8f31e6c0009b294594881fada 100644 (file)
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -21,6 +21,7 @@
 #define EZMINISAT_H
 
 #include "ezsat.h"
+#include <time.h>
 
 // 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<int> 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 e37031314d5bedba0c16b417ba2f07930741995b..00918f62f7a022f7f1f0701f6aa589e1ac3532b6 100644 (file)
--- 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 2674d83df723adae8c5a3ac62d2be7872747a106..2d0307d5124e7964e0ae15bb0e9849b88fc35021 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -69,6 +69,9 @@ private:
        int bind_cnf_or(const std::vector<int> &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 3000c54a025a4d5017b6313d780572ed856e1415..769d94a073e333e8e4843be14806b7c071ec927f 100644 (file)
--- 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;
  

diff --git a/tests/xsthammer/run-check.sh b/tests/xsthammer/run-check.sh
index 994f4d923e045f3ec32e495958be095008a93866..3dd63b59978054e845ed086724c149a083ba5d07 100644 (file)
--- 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"