summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-12-27 13:27:21 +0100
committerClifford Wolf <clifford@clifford.at>2013-12-27 13:27:21 +0100
commit11ffa7867794ee5bda2742830bda64976ad4f549 (patch)
tree8bc62fe0895586d1ffa665d90eb32c158262c4e8 /passes
parentfb31d10236635bf098210aa42327fbe2c8f3d08d (diff)
Added sat -set-def/-set-*-undef support
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc71
1 files changed, 66 insertions, 5 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e3b941f5..0a8006eb 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -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)) {
@@ -567,7 +632,6 @@ 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");
@@ -577,7 +641,6 @@ struct SatPass : public Pass {
log(" -set-all-undef <signal>\n");
log(" add a constraint that all bits of the given signal are undefined\n");
log("\n");
- #endif
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 +659,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-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");
@@ -638,7 +699,7 @@ struct SatPass : public Pass {
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 ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");