diff options
author | Clifford Wolf <clifford@clifford.at> | 2015-08-18 17:14:30 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2015-08-18 17:14:30 +0200 |
commit | f40d1b78b629dfebff7598e04b8470e6942f8f58 (patch) | |
tree | 29dc6f9c3d72566753e16f14dd000b6455dcc6a7 /passes/sat | |
parent | 246e362717f23bb8cfbd22c33728d6517b7d3d8f (diff) | |
download | yosys-f40d1b78b629dfebff7598e04b8470e6942f8f58.tar.gz yosys-f40d1b78b629dfebff7598e04b8470e6942f8f58.tar.bz2 yosys-f40d1b78b629dfebff7598e04b8470e6942f8f58.zip |
Added sat -show-regs, -show-public, -show-all
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/sat.cc | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index c83286924..e72eddf33 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -936,6 +936,9 @@ struct SatPass : public Pass { log(" -show-inputs, -show-outputs, -show-ports\n"); log(" add all module (input/output) ports to the list of shown signals\n"); log("\n"); + log(" -show-regs, -show-public, -show-all\n"); + log(" show all registers, show signals with 'public' names, show all signals\n"); + log("\n"); log(" -ignore_div_by_zero\n"); log(" ignore all solutions that involve a division by zero\n"); log("\n"); @@ -1064,6 +1067,7 @@ struct SatPass : public Pass { bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false; bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false; bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false; + bool show_regs = false, show_public = false, show_all = false; bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false; bool tempinduct_baseonly = false, tempinduct_inductonly = false, set_assumes = false; int tempinduct_skip = 0, stepsize = 1; @@ -1272,6 +1276,18 @@ struct SatPass : public Pass { show_outputs = true; continue; } + if (args[argidx] == "-show-regs") { + show_regs = true; + continue; + } + if (args[argidx] == "-show-public") { + show_public = true; + continue; + } + if (args[argidx] == "-show-all") { + show_all = true; + continue; + } if (args[argidx] == "-ignore_unknown_cells") { ignore_unknown_cells = true; continue; @@ -1331,6 +1347,29 @@ struct SatPass : public Pass { shows.push_back(it.second->name.str()); } + if (show_regs) { + pool<Wire*> reg_wires; + for (auto cell : module->cells()) { + if (cell->type == "$dff" || cell->type.substr(0, 6) == "$_DFF_") + for (auto bit : cell->getPort("\\Q")) + if (bit.wire) + reg_wires.insert(bit.wire); + } + for (auto wire : reg_wires) + shows.push_back(wire->name.str()); + } + + if (show_public) { + for (auto wire : module->wires()) + if (wire->name[0] == '\\') + shows.push_back(wire->name.str()); + } + + if (show_all) { + for (auto wire : module->wires()) + shows.push_back(wire->name.str()); + } + if (tempinduct) { if (loopcount > 0 || max_undef) |