3 files changed, 106 insertions, 0 deletions

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);
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index a078b0b1c..590a7eb1d 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -20,6 +20,7 @@
 #include "kernel/register.h"
 #include "kernel/celltypes.h"
 #include "kernel/sigtools.h"
+#include "kernel/mem.h"
 #include "kernel/rtlil.h"
 #include "kernel/log.h"
 
@@ -478,6 +479,29 @@ struct SetundefPass : public Pass {
 				log_assert(ffbits.empty());
 			}
 
+			if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
+			{
+				// Do not add anyseq / anyconst to unused memory port clocks
+				std::vector<Mem> memories = Mem::get_selected_memories(module);
+				for (auto &mem : memories) {
+					bool changed = false;
+					for (auto &rd_port : mem.rd_ports) {
+						if (!rd_port.clk_enable && rd_port.clk.is_fully_undef()) {
+							changed = true;
+							rd_port.clk = State::S0;
+						}
+					}
+					for (auto &wr_port : mem.rd_ports) {
+						if (!wr_port.clk_enable && wr_port.clk.is_fully_undef()) {
+							changed = true;
+							wr_port.clk = State::S0;
+						}
+					}
+					if (changed)
+						mem.emit();
+				}
+			}
+
 			module->rewrite_sigspecs(worker);
 
 			if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index 43deba47b..4d5605932 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -574,6 +574,7 @@ struct ShowWorker
 	{
 		ct.setup_internals();
 		ct.setup_internals_mem();
+		ct.setup_internals_anyinit();
 		ct.setup_stdcells();
 		ct.setup_stdcells_mem();
 		ct.setup_design(design);