aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--libs/ezsat/ezminisat.cc38
-rw-r--r--libs/ezsat/ezminisat.h5
-rw-r--r--libs/ezsat/ezsat.cc3
-rw-r--r--libs/ezsat/ezsat.h11
-rw-r--r--passes/sat/sat.cc67
-rw-r--r--tests/xsthammer/run-check.sh4
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 <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 4171985b6..2919aa2e3 100644
--- 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 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<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 3000c54a0..769d94a07 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;
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"
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 05:15:16 +0000