From d8cdc213a64de682952af6f5dc9a12bb2d3f54a4 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 27 Feb 2024 19:56:47 +0100
Subject: [PATCH] rename -witness: Bug fix and rename formal cells

Rename formal cells in addition to witness signals. This is required to
reliably track individual property states for the non-smtbmc flows.

Also removes a misplced `break` which resulted in only partial witness
renaming.
---
 backends/smt2/smt2.cc | 13 ++++++++++++-
 passes/cmds/rename.cc | 15 ++++++++++++++-
 2 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 5e63e6237..c702d5e7e 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1117,7 +1117,18 @@ struct Smt2Worker
 
 				string name_a = get_bool(cell->getPort(ID::A));
 				string name_en = get_bool(cell->getPort(ID::EN));
-				if (cell->name[0] == '$' && cell->attributes.count(ID::src))
+				bool private_name = cell->name[0] == '$';
+
+				if (!private_name && cell->has_attribute(ID::hdlname)) {
+					for (auto const &part : cell->get_hdlname_attribute()) {
+						if (part == "_witness_") {
+							private_name = true;
+							break;
+						}
+					}
+				}
+
+				if (private_name && cell->attributes.count(ID::src))
 					decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str()));
 				else
 					decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell)));
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index da4ba2f17..3f8d807b3 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -134,7 +134,6 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
 				cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
 				renames.emplace_back(cell, new_id);
 			}
-			break;
 		}
 
 		if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
@@ -165,6 +164,20 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
 				}
 			}
 		}
+
+
+		if (cell->type.in(ID($assert), ID($assume), ID($cover), ID($live), ID($fair), ID($check))) {
+			has_witness_signals = true;
+			if (cell->name.isPublic())
+				continue;
+			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);
+			renames.emplace_back(cell, new_id);
+			cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
+		}
 	}
 	for (auto rename : renames) {
 		module->rename(rename.first, rename.second);