aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/sat.cc
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat/sat.cc')
-rw-r--r--passes/sat/sat.cc239
1 files changed, 182 insertions, 57 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e330dfa6d..fef99dfc0 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -44,14 +44,14 @@ struct SatHelper
SatGen satgen;
// additional constraints
- std::vector<std::pair<std::string, std::string>> sets, prove, sets_init;
+ 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;
// undef constraints
bool enable_undef, set_init_undef;
- std::vector<std::string> sets_def, sets_undef, sets_all_undef;
- std::map<int, std::vector<std::string>> sets_def_at, sets_undef_at, sets_all_undef_at;
+ std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
// model variables
std::vector<std::string> shows;
@@ -61,7 +61,7 @@ struct SatHelper
bool gotTimeout;
SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
- design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
+ design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
@@ -202,6 +202,71 @@ struct SatHelper
check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ // 0 = sets_def
+ // 1 = sets_any_undef
+ // 2 = sets_all_undef
+ std::set<RTLIL::SigSpec> sets_def_undef[3];
+
+ for (auto &s : sets_def) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ }
+
+ for (auto &s : sets_any_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[1].insert(sig);
+ }
+
+ for (auto &s : sets_all_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (auto &s : sets_def_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_any_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].insert(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_all_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (int t = 0; t < 3; t++)
+ for (auto &sig : sets_def_undef[t]) {
+ log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+ std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
+ if (t == 0)
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+ if (t == 1)
+ ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+ if (t == 2)
+ ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+ }
+
int import_cell_counter = 0;
for (auto &c : module->cells)
if (design->selected(module, c.second)) {
@@ -219,34 +284,75 @@ struct SatHelper
int setup_proof(int timestep = -1)
{
- assert(prove.size() > 0);
+ assert(prove.size() + prove_x.size() > 0);
RTLIL::SigSpec big_lhs, big_rhs;
+ std::vector<int> prove_bits;
- for (auto &s : prove)
+ if (prove.size() > 0)
{
- RTLIL::SigSpec lhs, rhs;
+ for (auto &s : prove)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.width != rhs.width)
+ log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+ log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
- log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
- if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
- log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
- show_signal_pool.add(sigmap(lhs));
- show_signal_pool.add(sigmap(rhs));
+ log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+ check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+ prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ }
- if (lhs.width != rhs.width)
- log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
- s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+ if (prove_x.size() > 0)
+ {
+ for (auto &s : prove_x)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.width != rhs.width)
+ log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+ log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
- log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
- big_lhs.remove2(lhs, &big_rhs);
- big_lhs.append(lhs);
- big_rhs.append(rhs);
+ log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+
+ std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
+ std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
+
+ std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
+ std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
+
+ for (size_t i = 0; i < value_lhs.size(); i++)
+ 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))))));
}
- log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
- check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
- return satgen.signals_eq(big_lhs, big_rhs, timestep);
+ return ez.expression(ezSAT::OpAnd, prove_bits);
}
void force_unique_state(int timestep_from, int timestep_to)
@@ -567,17 +673,18 @@ struct SatPass : public Pass {
log(" -set <signal> <value>\n");
log(" set the specified signal to the specified value.\n");
log("\n");
- #if 0
log(" -set-def <signal>\n");
log(" add a constraint that all bits of the given signal must be defined\n");
log("\n");
- log(" -set-undef <signal>\n");
+ log(" -set-any-undef <signal>\n");
log(" add a constraint that at least one bit of the given signal is undefined\n");
log("\n");
log(" -set-all-undef <signal>\n");
log(" add a constraint that all bits of the given signal are undefined\n");
log("\n");
- #endif
+ log(" -set-def-inputs\n");
+ log(" add -set-def constraints for all module inputs\n");
+ log("\n");
log(" -show <signal>\n");
log(" show the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
@@ -596,13 +703,11 @@ struct SatPass : public Pass {
log(" set or unset the specified signal to the specified value in the\n");
log(" given timestep. this has priority over a -set for the same signal.\n");
log("\n");
- #if 0
- log(" -set-def <N> <signal>\n");
- log(" -set-undef <N> <signal>\n");
- log(" -set-all-undef <N> <signal>\n");
+ log(" -set-def-at <N> <signal>\n");
+ log(" -set-any-undef-at <N> <signal>\n");
+ log(" -set-all-undef-at <N> <signal>\n");
log(" add undef contraints in the given timestep.\n");
log("\n");
- #endif
log(" -set-init <signal> <value>\n");
log(" set the initial value for the register driving the signal to the value\n");
log("\n");
@@ -617,6 +722,10 @@ struct SatPass : public Pass {
log(" induction proof it is proven that the condition holds forever after\n");
log(" the number of time steps passed using -seq.\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(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
@@ -632,13 +741,13 @@ struct SatPass : public Pass {
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
- std::vector<std::pair<std::string, std::string>> sets, sets_init, prove;
+ std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
- std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at;
- std::vector<std::string> shows, sets_def, sets_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
+ std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
- bool verify = false, fail_on_timeout = false, enable_undef = false;
- bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true;
+ 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;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -682,23 +791,28 @@ struct SatPass : public Pass {
max_undef = true;
continue;
}
+ if (args[argidx] == "-set-def-inputs") {
+ enable_undef = true;
+ set_def_inputs = true;
+ continue;
+ }
if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
continue;
}
- if (args[argidx] == "-set-def" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
sets_def.push_back(args[++argidx]);
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-undef" && argidx+2 < args.size()) {
- sets_undef.push_back(args[++argidx]);
+ if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
+ sets_any_undef.push_back(args[++argidx]);
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-all-undef" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
sets_all_undef.push_back(args[++argidx]);
enable_undef = true;
continue;
@@ -709,6 +823,13 @@ struct SatPass : public Pass {
prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
continue;
}
+ if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ enable_undef = true;
+ continue;
+ }
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
seq_len = atoi(args[++argidx].c_str());
continue;
@@ -731,9 +852,9 @@ struct SatPass : public Pass {
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-undef-at" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
int timestep = atoi(args[++argidx].c_str());
- sets_undef_at[timestep].push_back(args[++argidx]);
+ sets_any_undef_at[timestep].push_back(args[++argidx]);
enable_undef = true;
continue;
}
@@ -773,10 +894,16 @@ struct SatPass : public Pass {
if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n");
- if (prove.size() == 0 && verify)
+ if (prove.size() + prove_x.size() == 0 && verify)
log_cmd_error("Got -verify but nothing to prove!\n");
- if (prove.size() > 0 && seq_len > 0)
+ 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 (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -786,15 +913,16 @@ struct SatPass : public Pass {
basecase.sets = sets;
basecase.prove = prove;
+ basecase.prove_x = prove_x;
basecase.sets_at = sets_at;
basecase.unsets_at = unsets_at;
basecase.shows = shows;
basecase.timeout = timeout;
basecase.sets_def = sets_def;
- basecase.sets_undef = sets_undef;
+ basecase.sets_any_undef = sets_any_undef;
basecase.sets_all_undef = sets_all_undef;
basecase.sets_def_at = sets_def_at;
- basecase.sets_undef_at = sets_undef_at;
+ basecase.sets_any_undef_at = sets_any_undef_at;
basecase.sets_all_undef_at = sets_all_undef_at;
basecase.sets_init = sets_init;
basecase.set_init_undef = set_init_undef;
@@ -806,16 +934,12 @@ struct SatPass : public Pass {
inductstep.sets = sets;
inductstep.prove = prove;
+ inductstep.prove_x = prove_x;
inductstep.shows = shows;
inductstep.timeout = timeout;
inductstep.sets_def = sets_def;
- inductstep.sets_undef = sets_undef;
+ inductstep.sets_any_undef = sets_any_undef;
inductstep.sets_all_undef = sets_all_undef;
- inductstep.sets_def_at = sets_def_at;
- inductstep.sets_undef_at = sets_undef_at;
- inductstep.sets_all_undef_at = sets_all_undef_at;
- inductstep.sets_init = sets_init;
- inductstep.set_init_undef = set_init_undef;
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
inductstep.setup(1);
@@ -896,15 +1020,16 @@ struct SatPass : public Pass {
sathelper.sets = sets;
sathelper.prove = prove;
+ sathelper.prove_x = prove_x;
sathelper.sets_at = sets_at;
sathelper.unsets_at = unsets_at;
sathelper.shows = shows;
sathelper.timeout = timeout;
sathelper.sets_def = sets_def;
- sathelper.sets_undef = sets_undef;
+ sathelper.sets_any_undef = sets_any_undef;
sathelper.sets_all_undef = sets_all_undef;
sathelper.sets_def_at = sets_def_at;
- sathelper.sets_undef_at = sets_undef_at;
+ sathelper.sets_any_undef_at = sets_any_undef_at;
sathelper.sets_all_undef_at = sets_all_undef_at;
sathelper.sets_init = sets_init;
sathelper.set_init_undef = set_init_undef;
@@ -912,7 +1037,7 @@ struct SatPass : public Pass {
if (seq_len == 0) {
sathelper.setup();
- if (sathelper.prove.size() > 0)
+ if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
} else {
for (int timestep = 1; timestep <= seq_len; timestep++)
@@ -939,7 +1064,7 @@ struct SatPass : public Pass {
sathelper.maximize_undefs();
}
- if (prove.size() == 0) {
+ if (prove.size() + prove_x.size() == 0) {
log("SAT solving finished - model found:\n");
} else {
log("SAT proof finished - model found: FAIL!\n");
@@ -965,7 +1090,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() == 0)
+ else if (prove.size() + prove_x.size() == 0)
log("SAT solving finished - no model found.\n");
else {
log("SAT proof finished - no model found: SUCCESS!\n");
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-06 05:41:54 +0000