summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-01 22:52:44 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-01 22:52:44 +0100
commit374674aff46c7464596fa18b07a5331e2f03ff8c (patch)
tree02d47264df12b5fb18477c3799ce484b0a727789 /passes/sat
parentcaf540d1adaec4e2a231d16d329aada8791d983c (diff)
Added sat -show-inputs and -show-outputs
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/sat.cc25
1 files changed, 24 insertions, 1 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index cf3cd59f..f5c8f50b 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -693,6 +693,9 @@ struct SatPass : public Pass {
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");
log("\n");
+ log(" -show-inputs, -show-outputs\n");
+ log(" add all module input (output) ports to the list of shown signals\n");
+ log("\n");
log(" -ignore_div_by_zero\n");
log(" ignore all solutions that involve a division by zero\n");
log("\n");
@@ -758,7 +761,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;
+ bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -898,6 +901,14 @@ struct SatPass : public Pass {
shows.push_back(args[++argidx]);
continue;
}
+ if (args[argidx] == "-show-inputs") {
+ show_inputs = true;
+ continue;
+ }
+ if (args[argidx] == "-show-outputs") {
+ show_outputs = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -928,6 +939,18 @@ struct SatPass : public Pass {
sets_def.push_back(it.second->name);
}
+ if (show_inputs) {
+ for (auto &it : module->wires)
+ if (it.second->port_input)
+ shows.push_back(it.second->name);
+ }
+
+ if (show_outputs) {
+ for (auto &it : module->wires)
+ if (it.second->port_output)
+ shows.push_back(it.second->name);
+ }
+
if (tempinduct)
{
if (loopcount > 0 || max_undef)