From 21f026cb054746a63449452c0919c7c73092f255 Mon Sep 17 00:00:00 2001
From: Alain Dargelas <alain@silimate.com>
Date: Fri, 28 Feb 2025 22:08:19 -0800
Subject: [PATCH] formal

---
 passes/silimate/annotate_cell_fanout.cc | 122 ++++++++++++++----------
 1 file changed, 69 insertions(+), 53 deletions(-)

diff --git a/passes/silimate/annotate_cell_fanout.cc b/passes/silimate/annotate_cell_fanout.cc
index c03a4d084..6aed247cf 100644
--- a/passes/silimate/annotate_cell_fanout.cc
+++ b/passes/silimate/annotate_cell_fanout.cc
@@ -64,20 +64,21 @@ void lhs2rhs_rhs2lhs(RTLIL::Module *module, SigMap &sigmap, dict<RTLIL::SigSpec,
 	}
 }
 
-RTLIL::Wire* getParentWire(const RTLIL::SigSpec& sigspec) {
-    if (sigspec.empty()) {
-        return nullptr; // Empty SigSpec, no parent wire
-    }
+RTLIL::Wire *getParentWire(const RTLIL::SigSpec &sigspec)
+{
+	if (sigspec.empty()) {
+		return nullptr; // Empty SigSpec, no parent wire
+	}
 
-    // Get the first SigBit
-    const RTLIL::SigBit& first_bit = sigspec[0];
+	// Get the first SigBit
+	const RTLIL::SigBit &first_bit = sigspec[0];
 
-    // Return the parent wire
-    return first_bit.wire;
+	// Return the parent wire
+	return first_bit.wire;
 }
 
-void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dict<RTLIL::SigSpec, std::set<Cell *>> &sig2CellsInFanout, RTLIL::Cell *cell, int fanout,
-	       int limit)
+void fixfanout(RTLIL::Design *design, RTLIL::Module *module, SigMap &sigmap, dict<RTLIL::SigSpec, std::set<Cell *>> &sig2CellsInFanout,
+	       RTLIL::Cell *cell, int fanout, int limit)
 {
 	if (fanout <= limit) {
 		std::cout << "Nothing to do for: " << cell->name.c_str() << std::endl;
@@ -109,28 +110,28 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 
 	// Create buffers and new wires
 	std::map<Cell *, int> bufferActualFanout;
-	std::map<RTLIL::SigSpec, std::vector<std::tuple<RTLIL::SigSpec, Cell*>>> buffer_outputs;
+	std::map<RTLIL::SigSpec, std::vector<std::tuple<RTLIL::SigSpec, Cell *>>> buffer_outputs;
 	std::map<SigSpec, int> bufferIndexes;
 	for (SigChunk chunk : cellOutSig.chunks()) {
-		std::vector<std::tuple<RTLIL::SigSpec, Cell*>> buffer_chunk_outputs;
+		std::vector<std::tuple<RTLIL::SigSpec, Cell *>> buffer_chunk_outputs;
 		for (int i = 0; i < num_buffers; ++i) {
 			RTLIL::Cell *buffer = module->addCell(NEW_ID2_SUFFIX("fbuf"), ID($pos));
-			bufferActualFanout[buffer] = 0; 
+			bufferActualFanout[buffer] = 0;
 			RTLIL::SigSpec buffer_output = module->addWire(NEW_ID2_SUFFIX("fbuf"), chunk.size());
 			buffer->setPort(ID(A), chunk);
 			buffer->setPort(ID(Y), sigmap(buffer_output));
 			buffer->fixup_parameters();
 			buffer_chunk_outputs.push_back(std::make_tuple(buffer_output, buffer)); // Old - New
-			bufferIndexes[chunk] = 0; 
+			bufferIndexes[chunk] = 0;
 		}
 		buffer_outputs.emplace(sigmap(SigSpec(chunk)), buffer_chunk_outputs);
 	}
 
 	// Cumulate all cells in the fanout of this cell
 	std::set<Cell *> cells = sig2CellsInFanout[cellOutSig];
-	for (int i = 0 ; i < cellOutSig.size(); i++) {
+	for (int i = 0; i < cellOutSig.size(); i++) {
 		SigSpec bit_sig = cellOutSig.extract(i, 1);
-		for (Cell* c : sig2CellsInFanout[sigmap(bit_sig)]) {
+		for (Cell *c : sig2CellsInFanout[sigmap(bit_sig)]) {
 			cells.insert(c);
 		}
 	}
@@ -144,19 +145,21 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 			if (c->input(portName)) {
 				if (actual.is_chunk()) {
 					if (buffer_outputs.find(actual) != buffer_outputs.end()) {
-						std::cout << "  CHUNK, indexCurrentBuffer: " << bufferIndexes[actual] << " buffer_outputs " << buffer_outputs[actual].size() << std::endl;
-						std::vector<std::tuple<RTLIL::SigSpec, Cell*>>& buf_info_vec = buffer_outputs[actual];
+						std::cout << "  CHUNK, indexCurrentBuffer: " << bufferIndexes[actual] << " buffer_outputs "
+							  << buffer_outputs[actual].size() << std::endl;
+						std::vector<std::tuple<RTLIL::SigSpec, Cell *>> &buf_info_vec = buffer_outputs[actual];
 						int bufferIndex = bufferIndexes[actual];
 						std::cout << "  BUFFER INDEX: " << bufferIndex << std::endl;
 						std::cout << "  VEC SIZE: " << buf_info_vec.size() << std::endl;
-						std::tuple<RTLIL::SigSpec, Cell*>& buf_info = buf_info_vec[bufferIndex];
+						std::tuple<RTLIL::SigSpec, Cell *> &buf_info = buf_info_vec[bufferIndex];
 						SigSpec newSig = std::get<0>(buf_info);
-						Cell* newBuf = std::get<1>(buf_info);
+						Cell *newBuf = std::get<1>(buf_info);
 						std::cout << "  MATCH" << std::endl;
 						c->setPort(portName, newSig);
 						sig2CellsInFanout[newSig].insert(c);
 						bufferActualFanout[newBuf]++;
-						std::cout << "   b: " << newBuf->name.c_str() << " fanout: " << bufferActualFanout[newBuf] << std::endl;
+						std::cout << "   b: " << newBuf->name.c_str() << " fanout: " << bufferActualFanout[newBuf]
+							  << std::endl;
 						if (bufferActualFanout[newBuf] >= max_output_per_buffer) {
 							std::cout << "  REACHED MAX" << std::endl;
 							if (buffer_outputs[actual].size() - 1 > bufferIndex) {
@@ -173,7 +176,7 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 							match = true;
 						} else {
 							for (SigChunk chunk_c : cellOutSig.chunks()) {
-						  	if (sigmap(SigSpec(chunk_a)) == sigmap(SigSpec(chunk_c))) {
+								if (sigmap(SigSpec(chunk_a)) == sigmap(SigSpec(chunk_c))) {
 									match = true;
 									break;
 								}
@@ -183,27 +186,29 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 							break;
 					}
 					if (match) {
-						
+
 						std::cout << "  MATCH" << std::endl;
 						std::vector<RTLIL::SigChunk> newChunks;
 						bool missed = true;
 						for (SigChunk chunk : actual.chunks()) {
 							bool replaced = false;
 							if (buffer_outputs.find(chunk) != buffer_outputs.end()) {
-						    std::cout << "  CHUNK, indexCurrentBuffer: " << bufferIndexes[chunk] << " buffer_outputs " << buffer_outputs[chunk].size() << std::endl;
-						    std::vector<std::tuple<RTLIL::SigSpec, Cell*>>& buf_info_vec = buffer_outputs[chunk];
-						    int bufferIndex = bufferIndexes[chunk];
-						    std::cout << "  BUFFER INDEX: " << bufferIndex << std::endl;
-						    std::cout << "  VEC SIZE: " << buf_info_vec.size() << std::endl;
-						    std::tuple<RTLIL::SigSpec, Cell*>& buf_info = buf_info_vec[bufferIndex];
-						    SigSpec newSig = std::get<0>(buf_info);
-						    Cell* newBuf = std::get<1>(buf_info);
+								std::cout << "  CHUNK, indexCurrentBuffer: " << bufferIndexes[chunk]
+									  << " buffer_outputs " << buffer_outputs[chunk].size() << std::endl;
+								std::vector<std::tuple<RTLIL::SigSpec, Cell *>> &buf_info_vec = buffer_outputs[chunk];
+								int bufferIndex = bufferIndexes[chunk];
+								std::cout << "  BUFFER INDEX: " << bufferIndex << std::endl;
+								std::cout << "  VEC SIZE: " << buf_info_vec.size() << std::endl;
+								std::tuple<RTLIL::SigSpec, Cell *> &buf_info = buf_info_vec[bufferIndex];
+								SigSpec newSig = std::get<0>(buf_info);
+								Cell *newBuf = std::get<1>(buf_info);
 								missed = false;
 								newChunks.push_back(newSig.as_chunk());
 								sig2CellsInFanout[newSig].insert(c);
 								replaced = true;
 								bufferActualFanout[newBuf]++;
-								std::cout << "   b: " << newBuf->name.c_str() << " fanout: " << bufferActualFanout[newBuf] << std::endl;
+								std::cout << "   b: " << newBuf->name.c_str()
+									  << " fanout: " << bufferActualFanout[newBuf] << std::endl;
 								if (bufferActualFanout[newBuf] >= max_output_per_buffer) {
 									std::cout << "  REACHED MAX" << std::endl;
 									if (buffer_outputs[chunk].size() - 1 > bufferIndex) {
@@ -217,11 +222,10 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 							}
 						}
 						if (missed) {
-							exit (1);
+							exit(1);
 						}
 						c->setPort(portName, newChunks);
 						break;
-						
 					}
 				}
 			}
@@ -234,9 +238,9 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 			std::cout << "Buffer with fanout 1: " << itr->first->name.c_str() << std::endl;
 			RTLIL::SigSpec bufferInSig = itr->first->getPort(ID::A);
 			RTLIL::SigSpec bufferOutSig = itr->first->getPort(ID::Y);
-			//std::cout << "bufferOutSig: " << bufferOutSig.as_wire()->name.c_str()
+			// std::cout << "bufferOutSig: " << bufferOutSig.as_wire()->name.c_str()
 			//	  << " bufferInSig: " << bufferInSig.as_wire()->name.c_str() << std::endl;
-			// Remove newly created buffers with a fanout of 1
+			//  Remove newly created buffers with a fanout of 1
 			for (Cell *c : cells) {
 				std::cout << "Cell in its fanout: " << c->name.c_str() << std::endl;
 				for (auto &conn : c->connections()) {
@@ -245,14 +249,16 @@ void fixfanout(RTLIL::Design* design, RTLIL::Module *module, SigMap &sigmap, dic
 					if (c->input(portName)) {
 						if (actual.is_chunk()) {
 							if (bufferOutSig == sigmap(actual)) {
-								std::cout << "Replace1: " << getParentWire(bufferOutSig)->name.c_str() << " by " << getParentWire(bufferInSig)->name.c_str() << std::endl;
+								std::cout << "Replace1: " << getParentWire(bufferOutSig)->name.c_str() << " by "
+									  << getParentWire(bufferInSig)->name.c_str() << std::endl;
 								c->setPort(portName, bufferInSig);
 							}
 						} else {
 							std::vector<RTLIL::SigChunk> newChunks;
 							for (SigChunk chunk : actual.chunks()) {
 								if (sigmap(SigSpec(chunk)) == sigmap(bufferOutSig)) {
-									std::cout << "Replace2: " << getParentWire(bufferOutSig)->name.c_str() << " by " << getParentWire(bufferInSig)->name.c_str() << std::endl;
+									std::cout << "Replace2: " << getParentWire(bufferOutSig)->name.c_str()
+										  << " by " << getParentWire(bufferInSig)->name.c_str() << std::endl;
 									newChunks.push_back(bufferInSig.as_chunk());
 								} else {
 									newChunks.push_back(chunk);
@@ -328,13 +334,14 @@ void calculateFanout(RTLIL::Module *module, SigMap &sigmap, dict<RTLIL::SigSpec,
 	}
 }
 
-std::string substringUntil(const std::string& str, char delimiter) {
-    size_t pos = str.find(delimiter);
-    if (pos != std::string::npos) {
-        return str.substr(0, pos);
-    } else {
-        return str;
-    }
+std::string substringUntil(const std::string &str, char delimiter)
+{
+	size_t pos = str.find(delimiter);
+	if (pos != std::string::npos) {
+		return str.substr(0, pos);
+	} else {
+		return str;
+	}
 }
 
 struct AnnotateCellFanout : public ScriptPass {
@@ -344,6 +351,7 @@ struct AnnotateCellFanout : public ScriptPass {
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		int limit = -1;
+		bool formalFriendly = false;
 		if (design == nullptr) {
 			log_error("No design object\n");
 			return;
@@ -357,6 +365,10 @@ struct AnnotateCellFanout : public ScriptPass {
 				limit = std::atoi(args[++argidx].c_str());
 				continue;
 			}
+			if (args[argidx] == "-formal") {
+				formalFriendly = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -367,13 +379,13 @@ struct AnnotateCellFanout : public ScriptPass {
 		for (auto module : design->selected_modules()) {
 			bool fixedFanout = false;
 			{
-				// Split output nets of cells with high fanout 
+				// Split output nets of cells with high fanout
 				SigMap sigmap(module);
 				dict<Cell *, int> cellFanout;
 				dict<RTLIL::SigSpec, std::set<Cell *>> sig2CellsInFanout;
 				calculateFanout(module, sigmap, sig2CellsInFanout, cellFanout);
 
-				std::vector<Cell*> cellsToFixFanout;
+				std::vector<Cell *> cellsToFixFanout;
 				for (auto itrCell : cellFanout) {
 					Cell *cell = itrCell.first;
 					int fanout = itrCell.second;
@@ -384,7 +396,7 @@ struct AnnotateCellFanout : public ScriptPass {
 				std::set<std::string> netsToSplitS;
 				std::string netsToSplit;
 				std::string portsToSplit;
-				for (Cell* cell : cellsToFixFanout) {
+				for (Cell *cell : cellsToFixFanout) {
 					RTLIL::SigSpec cellOutSig;
 					for (auto &conn : cell->connections()) {
 						IdString portName = conn.first;
@@ -392,24 +404,28 @@ struct AnnotateCellFanout : public ScriptPass {
 						if (cell->output(portName)) {
 							cellOutSig = sigmap(actual);
 							break;
-							}
+						}
 					}
 					std::string parent = getParentWire(cellOutSig)->name.c_str();
 					parent = substringUntil(parent, '[');
 					if (netsToSplitS.find(parent) == netsToSplitS.end()) {
-						netsToSplit += std::string(" w:") + parent; // Wire
+						netsToSplit += std::string(" w:") + parent;  // Wire
 						portsToSplit += std::string(" o:") + parent; // Port
 						netsToSplitS.insert(parent);
 						std::string splitnets = std::string("splitnets ") + netsToSplit;
 						Pass::call(design, splitnets);
 						splitnets = std::string("splitnets -ports_only ") + portsToSplit;
-						Pass::call(design, splitnets);
+						if (!formalFriendly) 
+							// Formal verification does not like ports to be split.
+							// This will prevent some buffering to happen on output ports used also internally in high fanout,
+							// but it will make formal happy.
+						  Pass::call(design, splitnets);
 						netsToSplit = "";
 						portsToSplit = "";
 					}
 				}
 			}
-		
+
 			{
 				// Fix high fanout
 				SigMap sigmap(module);
@@ -431,7 +447,7 @@ struct AnnotateCellFanout : public ScriptPass {
 			}
 
 			if (fixedFanout) {
-				// If Fanout got fixed, recalculate and annotate final fanout 
+				// If Fanout got fixed, recalculate and annotate final fanout
 				SigMap sigmap(module);
 				dict<Cell *, int> cellFanout;
 				dict<RTLIL::SigSpec, std::set<Cell *>> sig2CellsInFanout;