Added sat -show-regs, -show-public, -show-all

diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index c832869241c607651f425135e56702531ee3e083..e72eddf339475644291e70ce8ad10610a81add3d 100644 (file)
--- 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)