summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-01-19 15:38:23 +0100
committerClifford Wolf <clifford@clifford.at>2014-01-19 16:35:17 +0100
commit03a876c7e877545b4b8aa809f8b4fab9f29a9d54 (patch)
tree7a6a37fb2261ef579a5e82ee852951a1f18036a0
parentc36bac0e109b2a7192247cd3df9319f6f10a3e84 (diff)
Added sat -tempinduc and sat -prove-asserts
-rw-r--r--passes/sat/sat.cc51
1 files changed, 41 insertions, 10 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index fef99dfc..cf3cd59f 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -47,6 +47,7 @@ struct SatHelper
std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at;
+ bool prove_asserts;
// undef constraints
bool enable_undef, set_init_undef;
@@ -284,7 +285,7 @@ struct SatHelper
int setup_proof(int timestep = -1)
{
- assert(prove.size() + prove_x.size() > 0);
+ assert(prove.size() || prove_x.size() || prove_asserts);
RTLIL::SigSpec big_lhs, big_rhs;
std::vector<int> prove_bits;
@@ -352,6 +353,9 @@ struct SatHelper
prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
}
+ if (prove_asserts)
+ prove_bits.push_back(satgen.importAsserts(timestep));
+
return ez.expression(ezSAT::OpAnd, prove_bits);
}
@@ -717,15 +721,21 @@ struct SatPass : public Pass {
log("The following additional options can be used to set up a proof. If also -seq\n");
log("is passed, a temporal induction proof is performed.\n");
log("\n");
+ log(" -tempinduct\n");
+ log(" Perform a temporal induction proof. In a temporalinduction proof it is\n");
+ log(" proven that the condition holds forever after the number of time steps\n");
+ log(" specified using -seq.\n");
+ log("\n");
log(" -prove <signal> <value>\n");
- log(" Attempt to proof that <signal> is always <value>. In a temporal\n");
- log(" induction proof it is proven that the condition holds forever after\n");
- log(" the number of time steps passed using -seq.\n");
+ log(" Attempt to proof that <signal> is always <value>.\n");
log("\n");
log(" -prove-x <signal> <value>\n");
log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
log(" the right hand side. Useful for equivialence checking.\n");
log("\n");
+ log(" -prove-asserts\n");
+ log(" Prove that all asserts in the design hold.\n");
+ log("\n");
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
@@ -748,6 +758,7 @@ struct SatPass : public Pass {
int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
+ bool tempinduct = false, prove_asserts = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -817,6 +828,10 @@ struct SatPass : public Pass {
enable_undef = true;
continue;
}
+ if (args[argidx] == "-tempinduct") {
+ tempinduct = true;
+ continue;
+ }
if (args[argidx] == "-prove" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
@@ -830,6 +845,10 @@ struct SatPass : public Pass {
enable_undef = true;
continue;
}
+ if (args[argidx] == "-prove-asserts") {
+ prove_asserts = true;
+ continue;
+ }
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
seq_len = atoi(args[++argidx].c_str());
continue;
@@ -894,16 +913,22 @@ struct SatPass : public Pass {
if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n");
- if (prove.size() + prove_x.size() == 0 && verify)
+ if (!prove.size() && !prove_x.size() && !prove_asserts && verify)
log_cmd_error("Got -verify but nothing to prove!\n");
+ if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
+ log_cmd_error("Got -tempinduct but nothing to prove!\n");
+
+ if (seq_len == 0 && tempinduct)
+ log_cmd_error("Got -tempinduct but no -seq argument!\n");
+
if (set_def_inputs) {
for (auto &it : module->wires)
if (it.second->port_input)
sets_def.push_back(it.second->name);
}
- if (prove.size() + prove_x.size() > 0 && seq_len > 0)
+ if (tempinduct)
{
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -914,6 +939,7 @@ struct SatPass : public Pass {
basecase.sets = sets;
basecase.prove = prove;
basecase.prove_x = prove_x;
+ basecase.prove_asserts = prove_asserts;
basecase.sets_at = sets_at;
basecase.unsets_at = unsets_at;
basecase.shows = shows;
@@ -935,6 +961,7 @@ struct SatPass : public Pass {
inductstep.sets = sets;
inductstep.prove = prove;
inductstep.prove_x = prove_x;
+ inductstep.prove_asserts = prove_asserts;
inductstep.shows = shows;
inductstep.timeout = timeout;
inductstep.sets_def = sets_def;
@@ -1021,6 +1048,7 @@ struct SatPass : public Pass {
sathelper.sets = sets;
sathelper.prove = prove;
sathelper.prove_x = prove_x;
+ sathelper.prove_asserts = prove_asserts;
sathelper.sets_at = sets_at;
sathelper.unsets_at = unsets_at;
sathelper.shows = shows;
@@ -1037,11 +1065,14 @@ struct SatPass : public Pass {
if (seq_len == 0) {
sathelper.setup();
- if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
+ if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
} else {
- for (int timestep = 1; timestep <= seq_len; timestep++)
+ for (int timestep = 1; timestep <= seq_len; timestep++) {
sathelper.setup(timestep);
+ if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
+ sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof(timestep)));
+ }
sathelper.setup_init();
}
sathelper.generate_model();
@@ -1064,7 +1095,7 @@ struct SatPass : public Pass {
sathelper.maximize_undefs();
}
- if (prove.size() + prove_x.size() == 0) {
+ if (!prove.size() && !prove_x.size() && !prove_asserts) {
log("SAT solving finished - model found:\n");
} else {
log("SAT proof finished - model found: FAIL!\n");
@@ -1090,7 +1121,7 @@ struct SatPass : public Pass {
goto timeout;
if (rerun_counter)
log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
- else if (prove.size() + prove_x.size() == 0)
+ else if (!prove.size() && !prove_x.size() && !prove_asserts)
log("SAT solving finished - no model found.\n");
else {
log("SAT proof finished - no model found: SUCCESS!\n");