mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

Added sat -tempinduc and sat -prove-asserts

Browse source
This commit is contained in:
Clifford Wolf 2014-01-19 15:38:23 +01:00
parent c36bac0e10
commit 03a876c7e8
1 changed files with 41 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

51
passes/sat/sat.cc
View file

@ -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");