1 files changed, 45 insertions, 10 deletions

diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
index c2a1b5c44..5dee72e1b 100644
--- a/passes/cmds/xprop.cc
+++ b/passes/cmds/xprop.cc
@@ -33,6 +33,7 @@ struct XpropOptions
 {
 	bool split_inputs = false;
 	bool split_outputs = false;
+	bool split_public = false;
 	bool assume_encoding = false;
 	bool assert_encoding = false;
 	bool assume_def_inputs = false;
@@ -966,7 +967,7 @@ struct XpropWorker
 		if (!options.split_inputs && !options.split_outputs)
 			return;
 
-		vector<IdString> new_ports;
+		int port_id = 1;
 
 		for (auto port : module->ports) {
 			auto wire = module->wire(port);
@@ -982,16 +983,21 @@ struct XpropWorker
 
 					wire_d->port_input = wire->port_input;
 					wire_d->port_output = wire->port_output;
-					wire_d->port_id = GetSize(new_ports) + 1;
+					wire_d->port_id = port_id++;
 
 					wire_x->port_input = wire->port_input;
 					wire_x->port_output = wire->port_output;
-					wire_x->port_id = GetSize(new_ports) + 2;
+					wire_x->port_id = port_id++;
 
 					if (wire->port_output) {
 						auto enc = encoded(wire);
 						module->connect(wire_d, enc.is_1);
 						module->connect(wire_x, enc.is_x);
+
+						if (options.split_public) {
+							// Need to hide the original wire so split_public doesn't try to split it again
+							module->rename(wire, NEW_ID_SUFFIX(wire->name.c_str()));
+						}
 					} else {
 						auto enc = encoded(wire, true);
 
@@ -1003,21 +1009,37 @@ struct XpropWorker
 					wire->port_input = wire->port_output = false;
 					wire->port_id = 0;
 
-					new_ports.push_back(port_d);
-					new_ports.push_back(port_x);
-
 					continue;
 				}
 			}
-			wire->port_id = GetSize(new_ports) + 1;
-			new_ports.push_back(port);
+			wire->port_id = port_id++;
 		}
 
-		module->ports = new_ports;
-
 		module->fixup_ports();
 	}
 
+	void split_public()
+	{
+		if (!options.split_public)
+			return;
+
+		for (auto wire : module->selected_wires()) {
+			if (wire->port_input || wire->port_output || !wire->name.isPublic())
+				continue;
+			auto name_d = module->uniquify(stringf("%s_d", wire->name.c_str()));
+			auto name_x = module->uniquify(stringf("%s_x", wire->name.c_str()));
+
+			auto wire_d = module->addWire(name_d, GetSize(wire));
+			auto wire_x = module->addWire(name_x, GetSize(wire));
+
+			auto enc = encoded(wire);
+			module->connect(wire_d, enc.is_1);
+			module->connect(wire_x, enc.is_x);
+
+			module->rename(wire, NEW_ID_SUFFIX(wire->name.c_str()));
+		}
+	}
+
 	void encode_remaining()
 	{
 		pool<Wire *> enc_undriven_wires;
@@ -1083,6 +1105,13 @@ struct XpropPass : public Pass {
 		log("        the corresponding bit in <portname>_d is ignored for inputs and\n");
 		log("        guaranteed to be 0 for outputs.\n");
 		log("\n");
+		log("    -split-public\n");
+		log("        Replace each public non-port wire with two new wires, one carrying the\n");
+		log("        defined values (named <wirename>_d) and one carrying the mask of which\n");
+		log("        bits are x (named <wirename>_x). When a bit in the <portname>_x is set\n");
+		log("        the corresponding bit in <wirename>_d is guaranteed to be 0 for\n");
+		log("        outputs.\n");
+		log("\n");
 		log("    -assume-encoding\n");
 		log("        Add encoding invariants as assumptions. This can speed up formal\n");
 		log("        verification tasks.\n");
@@ -1129,6 +1158,10 @@ struct XpropPass : public Pass {
 				options.split_outputs = true;
 				continue;
 			}
+			if (args[argidx] == "-split-public") {
+				options.split_public = true;
+				continue;
+			}
 			if (args[argidx] == "-assume-encoding") {
 				options.assume_encoding = true;
 				continue;
@@ -1188,6 +1221,8 @@ struct XpropPass : public Pass {
 			worker.process_cells();
 			log_debug("Splitting ports.\n");
 			worker.split_ports();
+			log_debug("Splitting public signals.\n");
+			worker.split_public();
 			log_debug("Encode remaining signals.\n");
 			worker.encode_remaining();