rename: Add -witness mode

2 files changed, 83 insertions, 0 deletions

diff --git a/CHANGELOG b/CHANGELOG
index a9144facf..6403c5b9a 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -7,6 +7,8 @@ Yosys 0.20 .. Yosys 0.20-dev
  * New commands and options
     - Added "formalff" pass - transforms FFs for formal verification
     - Added option "-formal" to "memory_map" pass
+    - Added option "-witness" to "rename" - give public names to all signals
+      present in yosys witness traces
 
  * Formal Verification
     - Added $anyinit cell to directly represent FFs with an unconstrained
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index b49d5cdc2..45576c91c 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -106,6 +106,60 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, strin
 	return name + suffix;
 }
 
+static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &cache, RTLIL::Module *module)
+{
+	auto cached = cache.find(module);
+	if (cached != cache.end()) {
+		if (cached->second == -1)
+			log_error("Cannot rename witness signals in a design containing recursive instantiations.\n");
+		return cached->second;
+	}
+	cache.emplace(module, -1);
+
+	bool has_witness_signals = false;
+	for (auto cell : module->cells())
+	{
+		RTLIL::Module *impl = design->module(cell->type);
+		if (impl != nullptr) {
+			bool witness_in_cell = rename_witness(design, cache, impl);
+			has_witness_signals |= witness_in_cell;
+			if (witness_in_cell && !cell->name.isPublic()) {
+				std::string name = cell->name.c_str() + 1;
+				for (auto &c : name)
+					if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
+						c = '_';
+				auto new_id = module->uniquify("\\_witness_." + name);
+				cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
+				module->rename(cell, new_id);
+			}
+		}
+
+		if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
+			has_witness_signals = true;
+			auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
+			auto sig_out = cell->getPort(QY);
+
+			for (auto chunk : sig_out.chunks()) {
+				if (chunk.is_wire() && !chunk.wire->name.isPublic()) {
+					std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1);
+					for (auto &c : name)
+						if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
+							c = '_';
+					auto new_id = module->uniquify("\\_witness_." + name);
+					auto new_wire = module->addWire(new_id, GetSize(sig_out));
+					new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
+					module->connect({sig_out, new_wire});
+					cell->setPort(QY, new_wire);
+					break;
+				}
+			}
+		}
+	}
+
+	cache[module] = has_witness_signals;
+	return has_witness_signals;
+}
+
 struct RenamePass : public Pass {
 	RenamePass() : Pass("rename", "rename object in the design") { }
 	void help() override
@@ -147,6 +201,14 @@ struct RenamePass : public Pass {
 		log("pattern is '_%%_'.\n");
 		log("\n");
 		log("\n");
+		log("    rename -witness\n");
+		log("\n");
+		log("Assigns auto-generated names to all $any*/$all* output wires and containing\n");
+		log("cells that do not have a public name. This ensures that, during formal\n");
+		log("verification, a solver-found trace can be fully specified using a public\n");
+		log("hierarchical names.\n");
+		log("\n");
+		log("\n");
 		log("    rename -hide [selection]\n");
 		log("\n");
 		log("Assign private names (the ones with $-prefix) to all selected wires and cells\n");
@@ -172,6 +234,7 @@ struct RenamePass : public Pass {
 		bool flag_src = false;
 		bool flag_wire = false;
 		bool flag_enumerate = false;
+		bool flag_witness = false;
 		bool flag_hide = false;
 		bool flag_top = false;
 		bool flag_output = false;
@@ -203,6 +266,11 @@ struct RenamePass : public Pass {
 				got_mode = true;
 				continue;
 			}
+			if (arg == "-witness" && !got_mode) {
+				flag_witness = true;
+				got_mode = true;
+				continue;
+			}
 			if (arg == "-hide" && !got_mode) {
 				flag_hide = true;
 				got_mode = true;
@@ -309,6 +377,19 @@ struct RenamePass : public Pass {
 			}
 		}
 		else
+		if (flag_witness)
+		{
+			extra_args(args, argidx, design, false);
+
+			RTLIL::Module *module = design->top_module();
+
+			if (module == nullptr)
+				log_cmd_error("No top module found!\n");
+
+			dict<RTLIL::Module *, int> cache;
+			rename_witness(design, cache, module);
+		}
+		else
 		if (flag_hide)
 		{
 			extra_args(args, argidx, design);