From 172a8e79f0b818a3d7f6634f3149439b34c28b4e Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 8 Dec 2022 20:00:01 +0100
Subject: xprop: Add -split-public option

---
 passes/cmds/xprop.cc | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

(limited to 'passes')

diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
index c2a1b5c44..fa1976b34 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;
@@ -1018,6 +1019,31 @@ struct XpropWorker
 		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->wires_.erase(wire->name);
+			wire->attributes.erase(ID::fsm_encoding);
+			wire->name = NEW_ID_SUFFIX(wire->name.c_str());
+			module->wires_[wire->name] = wire;
+		}
+	}
+
 	void encode_remaining()
 	{
 		pool<Wire *> enc_undriven_wires;
@@ -1083,6 +1109,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 +1162,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 +1225,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();
 
-- 
cgit v1.2.3