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

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)