mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 11:42:30 +00:00 
			
		
		
		
	formal
This commit is contained in:
		
							parent
							
								
									aa4c5e9ee5
								
							
						
					
					
						commit
						21f026cb05
					
				
					 1 changed files with 69 additions and 53 deletions
				
			
		|  | @ -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; | ||||
|  |  | |||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue