mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-10-31 03:32:29 +00:00 
			
		
		
		
	
						commit
						74e92d10e8
					
				
					 11 changed files with 2385 additions and 16 deletions
				
			
		
							
								
								
									
										1
									
								
								backends/aiger2/Makefile.inc
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										1
									
								
								backends/aiger2/Makefile.inc
									
										
									
									
									
										Normal file
									
								
							|  | @ -0,0 +1 @@ | ||||||
|  | OBJS += backends/aiger2/aiger.o | ||||||
							
								
								
									
										1471
									
								
								backends/aiger2/aiger.cc
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										1471
									
								
								backends/aiger2/aiger.cc
									
										
									
									
									
										Normal file
									
								
							
										
											
												File diff suppressed because it is too large
												Load diff
											
										
									
								
							
							
								
								
									
										2
									
								
								frontends/aiger2/Makefile.inc
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										2
									
								
								frontends/aiger2/Makefile.inc
									
										
									
									
									
										Normal file
									
								
							|  | @ -0,0 +1,2 @@ | ||||||
|  | 
 | ||||||
|  | OBJS += frontends/aiger2/xaiger.o | ||||||
							
								
								
									
										473
									
								
								frontends/aiger2/xaiger.cc
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										473
									
								
								frontends/aiger2/xaiger.cc
									
										
									
									
									
										Normal file
									
								
							|  | @ -0,0 +1,473 @@ | ||||||
|  | /*
 | ||||||
|  |  *  yosys -- Yosys Open SYnthesis Suite | ||||||
|  |  * | ||||||
|  |  *  Copyright (C)  Martin Povišer <povik@cutebit.org> | ||||||
|  |  * | ||||||
|  |  *  Permission to use, copy, modify, and/or distribute this software for any | ||||||
|  |  *  purpose with or without fee is hereby granted, provided that the above | ||||||
|  |  *  copyright notice and this permission notice appear in all copies. | ||||||
|  |  * | ||||||
|  |  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES | ||||||
|  |  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF | ||||||
|  |  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR | ||||||
|  |  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES | ||||||
|  |  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN | ||||||
|  |  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF | ||||||
|  |  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. | ||||||
|  |  * | ||||||
|  |  */ | ||||||
|  | 
 | ||||||
|  | #include "kernel/register.h" | ||||||
|  | 
 | ||||||
|  | USING_YOSYS_NAMESPACE | ||||||
|  | PRIVATE_NAMESPACE_BEGIN | ||||||
|  | 
 | ||||||
|  | uint32_t read_be32(std::istream &f) { | ||||||
|  | 	return ((uint32_t) f.get() << 24) | | ||||||
|  | 		((uint32_t) f.get() << 16) |  | ||||||
|  | 		((uint32_t) f.get() << 8) | (uint32_t) f.get(); | ||||||
|  | } | ||||||
|  | 
 | ||||||
|  | IdString read_idstring(std::istream &f) | ||||||
|  | { | ||||||
|  | 	std::string str; | ||||||
|  | 	std::getline(f, str, '\0'); | ||||||
|  | 	if (!f.good()) | ||||||
|  | 		log_error("failed to read string\n"); | ||||||
|  | 	return RTLIL::escape_id(str); | ||||||
|  | } | ||||||
|  | 
 | ||||||
|  | struct Xaiger2Frontend : public Frontend { | ||||||
|  | 	Xaiger2Frontend() : Frontend("xaiger2", "(experimental) read XAIGER file") | ||||||
|  | 	{ | ||||||
|  | 		experimental(); | ||||||
|  | 	} | ||||||
|  | 
 | ||||||
|  | 	void help() override | ||||||
|  | 	{ | ||||||
|  | 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    read_xaiger2 -sc_mapping [options] <filename>\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("Read a standard cell mapping from a XAIGER file into an existing module.\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    -module_name <name>\n"); | ||||||
|  | 		log("        name of the target module\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    -map2 <filename>\n"); | ||||||
|  |         log("        read file with symbol information\n"); | ||||||
|  |         log("\n"); | ||||||
|  | 	} | ||||||
|  | 
 | ||||||
|  | 	void read_sc_mapping(std::istream *&f, std::string filename, std::vector<std::string> args, Design *design) | ||||||
|  | 	{ | ||||||
|  | 		IdString module_name; | ||||||
|  | 		std::string map_filename; | ||||||
|  | 
 | ||||||
|  | 		size_t argidx; | ||||||
|  | 		for (argidx = 2; argidx < args.size(); argidx++) { | ||||||
|  | 			std::string arg = args[argidx]; | ||||||
|  | 			if (arg == "-module_name" && argidx + 1 < args.size()) { | ||||||
|  | 				module_name = RTLIL::escape_id(args[++argidx]); | ||||||
|  | 				continue; | ||||||
|  | 			} | ||||||
|  | 			if (arg == "-map2" && argidx + 1 < args.size()) { | ||||||
|  | 				map_filename = args[++argidx]; | ||||||
|  | 				continue; | ||||||
|  | 			} | ||||||
|  | 			break; | ||||||
|  | 		} | ||||||
|  | 		extra_args(f, filename, args, argidx, true); | ||||||
|  | 
 | ||||||
|  | 		if (map_filename.empty()) | ||||||
|  | 			log_error("A '-map2' argument required\n"); | ||||||
|  | 		if (module_name.empty()) | ||||||
|  | 			log_error("A '-module_name' argument required\n"); | ||||||
|  | 
 | ||||||
|  | 		Module *module = design->module(module_name); | ||||||
|  | 		if (!module) | ||||||
|  | 			log_error("Module '%s' not found\n", log_id(module_name)); | ||||||
|  | 
 | ||||||
|  | 		std::ifstream map_file; | ||||||
|  | 		map_file.open(map_filename); | ||||||
|  | 		if (!map_file) | ||||||
|  | 			log_error("Failed to open map file '%s'\n", map_filename.c_str()); | ||||||
|  | 
 | ||||||
|  | 		unsigned int M, I, L, O, A; | ||||||
|  | 		std::string header; | ||||||
|  | 		if (!(*f >> header >> M >> I >> L >> O >> A) || header != "aig") | ||||||
|  | 			log_error("Bad header\n"); | ||||||
|  | 		std::string line; | ||||||
|  | 		std::getline(*f, line); | ||||||
|  | 		log_debug("M=%u I=%u L=%u O=%u A=%u\n", M, I, L, O, A); | ||||||
|  | 
 | ||||||
|  | 		if (L != 0) | ||||||
|  | 			log_error("Latches unsupported\n"); | ||||||
|  | 		if (I + L + A != M) | ||||||
|  | 			log_error("Inconsistent header\n"); | ||||||
|  | 
 | ||||||
|  | 		std::vector<int> outputs; | ||||||
|  | 		for (int i = 0; i < (int) O; i++) { | ||||||
|  | 			int po; | ||||||
|  | 			*f >> po; | ||||||
|  | 			log_assert(f->get() == '\n'); | ||||||
|  | 			outputs.push_back(po); | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		std::vector<std::pair<Cell *, Module *>> boxes; | ||||||
|  | 		std::vector<bool> retained_boxes; | ||||||
|  | 		std::vector<SigBit> bits(2 + 2*M, RTLIL::Sm); | ||||||
|  | 		bits[0] = RTLIL::S0; | ||||||
|  | 		bits[1] = RTLIL::S1; | ||||||
|  | 
 | ||||||
|  | 		std::string type; | ||||||
|  | 		while (map_file >> type) { | ||||||
|  | 			if (type == "pi") { | ||||||
|  | 				int pi_idx; | ||||||
|  | 				int woffset; | ||||||
|  | 				std::string name; | ||||||
|  | 				if (!(map_file >> pi_idx >> woffset >> name)) | ||||||
|  | 					log_error("Bad map file (1)\n"); | ||||||
|  | 				int lit = (2 * pi_idx) + 2; | ||||||
|  | 				if (lit < 0 || lit >= (int) bits.size()) | ||||||
|  | 					log_error("Bad map file (2)\n"); | ||||||
|  | 				Wire *w = module->wire(name); | ||||||
|  | 				if (!w || woffset < 0 || woffset >= w->width) | ||||||
|  | 					log_error("Map file references non-existent signal bit %s[%d]\n", | ||||||
|  | 							  name.c_str(), woffset); | ||||||
|  | 				bits[lit] = SigBit(w, woffset); | ||||||
|  | 			} else if (type == "box") { | ||||||
|  | 				int box_seq; | ||||||
|  | 				std::string name; | ||||||
|  | 				if (!(map_file >> box_seq >> name)) | ||||||
|  | 					log_error("Bad map file (20)\n"); | ||||||
|  | 				if (box_seq < 0) | ||||||
|  | 					log_error("Bad map file (21)\n"); | ||||||
|  | 
 | ||||||
|  | 				Cell *box = module->cell(RTLIL::escape_id(name)); | ||||||
|  | 				if (!box) | ||||||
|  | 					log_error("Map file references non-existent box %s\n", | ||||||
|  | 							  name.c_str()); | ||||||
|  | 
 | ||||||
|  | 				Module *def = design->module(box->type); | ||||||
|  | 				if (def && !box->parameters.empty()) { | ||||||
|  | 					// TODO: This is potentially costly even if a cached derivation exists
 | ||||||
|  | 					def = design->module(def->derive(design, box->parameters)); | ||||||
|  | 					log_assert(def); | ||||||
|  | 				} | ||||||
|  | 
 | ||||||
|  | 				if (!def) | ||||||
|  | 					log_error("Bad map file (22)\n"); | ||||||
|  | 
 | ||||||
|  | 				if (box_seq >= (int) boxes.size()) { | ||||||
|  | 					boxes.resize(box_seq + 1); | ||||||
|  | 					retained_boxes.resize(box_seq + 1); | ||||||
|  | 				} | ||||||
|  | 				boxes[box_seq] = std::make_pair(box, def); | ||||||
|  | 			} else { | ||||||
|  | 				std::string scratch; | ||||||
|  | 				std::getline(map_file, scratch); | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		for (int i = 0; i < (int) A; i++) { | ||||||
|  | 			while (f->get() & 0x80 && !f->eof()); | ||||||
|  | 			while (f->get() & 0x80 && !f->eof()); | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		if (f->get() != 'c') | ||||||
|  | 			log_error("Missing 'c' ahead of extensions\n"); | ||||||
|  | 		if (f->peek() == '\n') | ||||||
|  | 			f->get(); | ||||||
|  | 		auto extensions_start = f->tellg(); | ||||||
|  | 
 | ||||||
|  | 		log_debug("reading 'h' (first pass)\n"); | ||||||
|  | 		for (int c = f->get(); c != EOF; c = f->get()) { | ||||||
|  | 			if (c == 'h') { | ||||||
|  | 				uint32_t len, ci_num, co_num, pi_num, po_num, no_boxes; | ||||||
|  | 				len = read_be32(*f); | ||||||
|  | 				read_be32(*f); | ||||||
|  | 				ci_num = read_be32(*f); | ||||||
|  | 				co_num = read_be32(*f); | ||||||
|  | 				pi_num = read_be32(*f); | ||||||
|  | 				po_num = read_be32(*f); | ||||||
|  | 				no_boxes = read_be32(*f); | ||||||
|  | 
 | ||||||
|  | 				log_debug("len=%u ci_num=%u co_num=%u pi_num=%u po_nun=%u no_boxes=%u\n", | ||||||
|  | 						  len, ci_num, co_num, pi_num, po_num, no_boxes); | ||||||
|  | 
 | ||||||
|  | 				int ci_counter = 0; | ||||||
|  | 				for (uint32_t i = 0; i < no_boxes; i++) { | ||||||
|  | 					uint32_t box_inputs, box_outputs, box_id, box_seq; | ||||||
|  | 					box_inputs = read_be32(*f); | ||||||
|  | 					box_outputs = read_be32(*f); | ||||||
|  | 					box_id = read_be32(*f); | ||||||
|  | 					box_seq = read_be32(*f); | ||||||
|  | 
 | ||||||
|  | 					log("box_seq=%d boxes.size=%d\n", box_seq, (int) boxes.size()); | ||||||
|  | 					log_assert(box_seq < boxes.size()); | ||||||
|  | 
 | ||||||
|  | 					auto [cell, def] = boxes[box_seq]; | ||||||
|  | 					log_assert(cell && def); | ||||||
|  | 					retained_boxes[box_seq] = true; | ||||||
|  | 
 | ||||||
|  | 					int box_ci_idx = 0; | ||||||
|  | 					for (auto port_id : def->ports) { | ||||||
|  | 						Wire *port = def->wire(port_id); | ||||||
|  | 						if (port->port_output) { | ||||||
|  | 							if (!cell->hasPort(port_id) || cell->getPort(port_id).size() != port->width) | ||||||
|  | 								log_error("Malformed design (1)\n"); | ||||||
|  | 
 | ||||||
|  | 							SigSpec &conn = cell->connections_[port_id]; | ||||||
|  | 							for (int j = 0; j < port->width; j++) { | ||||||
|  | 								if (conn[j].wire && conn[j].wire->port_output) | ||||||
|  | 									conn[j] = module->addWire(module->uniquify( | ||||||
|  | 												stringf("$box$%s$%s$%d", | ||||||
|  | 													cell->name.isPublic() ? cell->name.c_str() + 1 : cell->name.c_str(), | ||||||
|  | 													port_id.isPublic() ? port_id.c_str() + 1 : port_id.c_str(), | ||||||
|  | 													j))); | ||||||
|  | 
 | ||||||
|  | 								bits[2*(pi_num + ci_counter + box_ci_idx++) + 2] = conn[j]; | ||||||
|  | 							} | ||||||
|  | 						} | ||||||
|  | 					} | ||||||
|  | 
 | ||||||
|  | 					log_assert(box_ci_idx == (int) box_outputs); | ||||||
|  | 					ci_counter += box_ci_idx; | ||||||
|  | 				} | ||||||
|  | 				log_assert(pi_num + ci_counter == ci_num); | ||||||
|  | 			} else if (c == '\n') { | ||||||
|  | 				break; | ||||||
|  | 			} else if (c == 'c') { | ||||||
|  | 				break; | ||||||
|  | 			} else { | ||||||
|  | 				uint32_t len = read_be32(*f); | ||||||
|  | 				f->ignore(len); | ||||||
|  | 				log_debug("  section '%c' (%d): ignoring %d bytes\n", c, c, len); | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		log_debug("reading 'M' (second pass)\n"); | ||||||
|  | 
 | ||||||
|  | 		f->seekg(extensions_start); | ||||||
|  | 		bool read_mapping = false; | ||||||
|  | 		uint32_t no_cells, no_instances; | ||||||
|  | 		for (int c = f->get(); c != EOF; c = f->get()) { | ||||||
|  | 			if (c == 'M') { | ||||||
|  | 				uint32_t len = read_be32(*f); | ||||||
|  | 				read_mapping = true; | ||||||
|  | 
 | ||||||
|  | 				no_cells = read_be32(*f); | ||||||
|  | 				no_instances = read_be32(*f); | ||||||
|  | 
 | ||||||
|  | 				log_debug("M: len=%u no_cells=%u no_instances=%u\n", len, no_cells, no_instances); | ||||||
|  | 
 | ||||||
|  | 				struct MappingCell { | ||||||
|  | 					RTLIL::IdString type; | ||||||
|  | 					RTLIL::IdString out; | ||||||
|  | 					std::vector<RTLIL::IdString> ins; | ||||||
|  | 				}; | ||||||
|  | 				std::vector<MappingCell> cells; | ||||||
|  | 				cells.resize(no_cells); | ||||||
|  | 
 | ||||||
|  | 				for (unsigned i = 0; i < no_cells; ++i) { | ||||||
|  | 					auto &cell = cells[i]; | ||||||
|  | 					cell.type = read_idstring(*f); | ||||||
|  | 					cell.out = read_idstring(*f); | ||||||
|  | 					uint32_t nins = read_be32(*f); | ||||||
|  | 					for (uint32_t j = 0; j < nins; j++) | ||||||
|  | 						cell.ins.push_back(read_idstring(*f)); | ||||||
|  | 					log_debug("M: Cell %s (out %s, ins", log_id(cell.type), log_id(cell.out)); | ||||||
|  | 					for (auto in : cell.ins) | ||||||
|  | 						log_debug(" %s", log_id(in)); | ||||||
|  | 					log_debug(")\n"); | ||||||
|  | 				} | ||||||
|  | 
 | ||||||
|  | 				for (unsigned i = 0; i < no_instances; ++i) { | ||||||
|  | 					uint32_t cell_id = read_be32(*f); | ||||||
|  | 					uint32_t out_lit = read_be32(*f); | ||||||
|  | 
 | ||||||
|  | 					log_assert(out_lit < bits.size()); | ||||||
|  | 					log_assert(bits[out_lit] == RTLIL::Sm); | ||||||
|  | 					log_assert(cell_id < cells.size()); | ||||||
|  | 					auto &cell = cells[cell_id]; | ||||||
|  | 					Cell *instance = module->addCell(module->uniquify(stringf("$sc%d", out_lit)), cell.type); | ||||||
|  | 					auto out_w = module->addWire(module->uniquify(stringf("$lit%d", out_lit))); | ||||||
|  | 					instance->setPort(cell.out, out_w); | ||||||
|  | 					bits[out_lit] = out_w; | ||||||
|  | 					for (auto in : cell.ins) { | ||||||
|  | 						uint32_t in_lit = read_be32(*f); | ||||||
|  | 						log_assert(out_lit < bits.size()); | ||||||
|  | 						log_assert(bits[in_lit] != RTLIL::Sm); | ||||||
|  | 						instance->setPort(in, bits[in_lit]); | ||||||
|  | 					} | ||||||
|  | 				} | ||||||
|  | 			} else if (c == '\n') { | ||||||
|  | 				break; | ||||||
|  | 			} else if (c == 'c') { | ||||||
|  | 				break; | ||||||
|  | 			} else { | ||||||
|  | 				uint32_t len = read_be32(*f); | ||||||
|  | 				f->ignore(len); | ||||||
|  | 				log_debug("  section '%c' (%d): ignoring %d bytes\n", c, c, len); | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		if (!read_mapping) | ||||||
|  | 			log_error("Missing mapping (no 'M' section)\n"); | ||||||
|  | 
 | ||||||
|  | 		log("Read %d instances with cell library of size %d.\n", | ||||||
|  | 			no_instances, no_cells); | ||||||
|  | 
 | ||||||
|  | 		f->seekg(extensions_start); | ||||||
|  | 		log_debug("reading 'h' (second pass)\n"); | ||||||
|  | 		int co_counter = 0; | ||||||
|  | 		for (int c = f->get(); c != EOF; c = f->get()) { | ||||||
|  | 			if (c == 'h') { | ||||||
|  | 				uint32_t len, ci_num, co_num, pi_num, po_num, no_boxes; | ||||||
|  | 				len = read_be32(*f); | ||||||
|  | 				read_be32(*f); | ||||||
|  | 				ci_num = read_be32(*f); | ||||||
|  | 				co_num = read_be32(*f); | ||||||
|  | 				pi_num = read_be32(*f); | ||||||
|  | 				po_num = read_be32(*f); | ||||||
|  | 				no_boxes = read_be32(*f); | ||||||
|  | 
 | ||||||
|  | 				log_debug("len=%u ci_num=%u co_num=%u pi_num=%u po_nun=%u no_boxes=%u\n", | ||||||
|  | 						  len, ci_num, co_num, pi_num, po_num, no_boxes); | ||||||
|  | 
 | ||||||
|  | 				for (uint32_t i = 0; i < no_boxes; i++) { | ||||||
|  | 					uint32_t box_inputs, box_outputs, box_id, box_seq; | ||||||
|  | 					box_inputs = read_be32(*f); | ||||||
|  | 					box_outputs = read_be32(*f); | ||||||
|  | 					box_id = read_be32(*f); | ||||||
|  | 					box_seq = read_be32(*f); | ||||||
|  | 
 | ||||||
|  | 					log("box_seq=%d boxes.size=%d\n", box_seq, (int) boxes.size()); | ||||||
|  | 					log_assert(box_seq < boxes.size()); | ||||||
|  | 
 | ||||||
|  | 					auto [cell, def] = boxes[box_seq]; | ||||||
|  | 					log_assert(cell && def); | ||||||
|  | 
 | ||||||
|  | 					int box_co_idx = 0; | ||||||
|  | 					for (auto port_id : def->ports) { | ||||||
|  | 						Wire *port = def->wire(port_id); | ||||||
|  | 						SigSpec conn; | ||||||
|  | 						if (port->port_input) { | ||||||
|  | 							if (!cell->hasPort(port_id) || cell->getPort(port_id).size() != port->width) | ||||||
|  | 								log_error("Malformed design (2)\n"); | ||||||
|  | 
 | ||||||
|  | 							SigSpec conn; | ||||||
|  | 							for (int j = 0; j < port->width; j++) { | ||||||
|  | 								log_assert(co_counter + box_co_idx < (int) outputs.size()); | ||||||
|  | 								int lit = outputs[co_counter + box_co_idx++]; | ||||||
|  | 								log_assert(lit >= 0 && lit < (int) bits.size()); | ||||||
|  | 								SigBit bit = bits[lit]; | ||||||
|  | 								if (bit == RTLIL::Sm) | ||||||
|  | 									log_error("Malformed mapping (1)\n"); | ||||||
|  | 								conn.append(bit); | ||||||
|  | 							} | ||||||
|  | 							cell->setPort(port_id, conn); | ||||||
|  | 						} | ||||||
|  | 					} | ||||||
|  | 
 | ||||||
|  | 					log_assert(box_co_idx == (int) box_inputs); | ||||||
|  | 					co_counter += box_co_idx; | ||||||
|  | 				} | ||||||
|  | 				log_assert(po_num + co_counter == co_num); | ||||||
|  | 			} else if (c == '\n') { | ||||||
|  | 				break; | ||||||
|  | 			} else if (c == 'c') { | ||||||
|  | 				break; | ||||||
|  | 			} else { | ||||||
|  | 				uint32_t len = read_be32(*f); | ||||||
|  | 				f->ignore(len); | ||||||
|  | 				log_debug("  section '%c' (%d): ignoring %d bytes\n", c, c, len); | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		while (true) { | ||||||
|  | 			std::string scratch; | ||||||
|  | 			std::getline(*f, scratch); | ||||||
|  | 			if (f->eof()) | ||||||
|  | 				break; | ||||||
|  | 			log_assert(!f->fail()); | ||||||
|  | 			log("input file: %s\n", scratch.c_str()); | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		log_debug("co_counter=%d\n", co_counter); | ||||||
|  | 
 | ||||||
|  | 		// TODO: seek without close/open
 | ||||||
|  | 		map_file.close(); | ||||||
|  | 		map_file.open(map_filename); | ||||||
|  | 		while (map_file >> type) { | ||||||
|  | 			if (type == "po") { | ||||||
|  | 				int po_idx; | ||||||
|  | 				int woffset; | ||||||
|  | 				std::string name; | ||||||
|  | 				if (!(map_file >> po_idx >> woffset >> name)) | ||||||
|  | 					log_error("Bad map file (3)\n"); | ||||||
|  | 				po_idx += co_counter; | ||||||
|  | 				if (po_idx < 0 || po_idx >= (int) outputs.size()) | ||||||
|  | 					log_error("Bad map file (4)\n"); | ||||||
|  | 				int lit = outputs[po_idx]; | ||||||
|  | 				if (lit < 0 || lit >= (int) bits.size()) | ||||||
|  | 					log_error("Bad map file (5)\n"); | ||||||
|  | 				if (bits[lit] == RTLIL::Sm) | ||||||
|  | 					log_error("Bad map file (6)\n"); | ||||||
|  | 				Wire *w = module->wire(name); | ||||||
|  | 				if (!w || woffset < 0 || woffset >= w->width) | ||||||
|  | 					log_error("Map file references non-existent signal bit %s[%d]\n", | ||||||
|  | 							  name.c_str(), woffset); | ||||||
|  | 				module->connect(SigBit(w, woffset), bits[lit]); | ||||||
|  | 			} else if (type == "pseudopo") { | ||||||
|  | 				int po_idx; | ||||||
|  | 				int poffset; | ||||||
|  | 				std::string box_name; | ||||||
|  | 				std::string box_port; | ||||||
|  | 				if (!(map_file >> po_idx >> poffset >> box_name >> box_port)) | ||||||
|  | 					log_error("Bad map file (7)\n"); | ||||||
|  | 				po_idx += co_counter; | ||||||
|  | 				if (po_idx < 0 || po_idx >= (int) outputs.size()) | ||||||
|  | 					log_error("Bad map file (8)\n"); | ||||||
|  | 				int lit = outputs[po_idx]; | ||||||
|  | 				if (lit < 0 || lit >= (int) bits.size()) | ||||||
|  | 					log_error("Bad map file (9)\n"); | ||||||
|  | 				if (bits[lit] == RTLIL::Sm) | ||||||
|  | 					log_error("Bad map file (10)\n"); | ||||||
|  | 				Cell *cell = module->cell(box_name); | ||||||
|  | 				if (!cell || !cell->hasPort(box_port)) | ||||||
|  | 					log_error("Map file references non-existent box port %s/%s\n", | ||||||
|  | 							  box_name.c_str(), box_port.c_str()); | ||||||
|  | 				SigSpec &port = cell->connections_[box_port]; | ||||||
|  | 				if (poffset < 0 || poffset >= port.size()) | ||||||
|  | 					log_error("Map file references non-existent box port bit %s/%s[%d]\n", | ||||||
|  | 							  box_name.c_str(), box_port.c_str(), poffset); | ||||||
|  | 				port[poffset] = bits[lit]; | ||||||
|  | 			} else { | ||||||
|  | 				std::string scratch; | ||||||
|  | 				std::getline(map_file, scratch); | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		int box_seq = 0; | ||||||
|  | 		for (auto [cell, def] : boxes) { | ||||||
|  | 			if (!retained_boxes[box_seq++]) | ||||||
|  | 				module->remove(cell); | ||||||
|  | 		} | ||||||
|  | 	} | ||||||
|  | 
 | ||||||
|  | 	void execute(std::istream *&f, std::string filename, std::vector<std::string> args, Design *design) override | ||||||
|  | 	{ | ||||||
|  | 		log_header(design, "Executing XAIGER2 frontend.\n"); | ||||||
|  | 
 | ||||||
|  | 		if (args.size() > 1 && args[1] == "-sc_mapping") { | ||||||
|  | 			read_sc_mapping(f, filename, args, design); | ||||||
|  | 			return; | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		log_cmd_error("Mode '-sc_mapping' must be selected\n"); | ||||||
|  | 	} | ||||||
|  | } Xaiger2Frontend; | ||||||
|  | 
 | ||||||
|  | PRIVATE_NAMESPACE_END | ||||||
|  | @ -381,11 +381,10 @@ struct CellTypes | ||||||
| 		HANDLE_CELL_TYPE(modfloor) | 		HANDLE_CELL_TYPE(modfloor) | ||||||
| 		HANDLE_CELL_TYPE(pow) | 		HANDLE_CELL_TYPE(pow) | ||||||
| 		HANDLE_CELL_TYPE(pos) | 		HANDLE_CELL_TYPE(pos) | ||||||
| 		HANDLE_CELL_TYPE(buf) |  | ||||||
| 		HANDLE_CELL_TYPE(neg) | 		HANDLE_CELL_TYPE(neg) | ||||||
| #undef HANDLE_CELL_TYPE | #undef HANDLE_CELL_TYPE | ||||||
| 
 | 
 | ||||||
| 		if (type == ID($_BUF_)) | 		if (type.in(ID($_BUF_), ID($buf))) | ||||||
| 			return arg1; | 			return arg1; | ||||||
| 		if (type == ID($_NOT_)) | 		if (type == ID($_NOT_)) | ||||||
| 			return eval_not(arg1); | 			return eval_not(arg1); | ||||||
|  |  | ||||||
|  | @ -12,10 +12,12 @@ OBJS += passes/techmap/abc.o | ||||||
| OBJS += passes/techmap/abc9.o | OBJS += passes/techmap/abc9.o | ||||||
| OBJS += passes/techmap/abc9_exe.o | OBJS += passes/techmap/abc9_exe.o | ||||||
| OBJS += passes/techmap/abc9_ops.o | OBJS += passes/techmap/abc9_ops.o | ||||||
|  | OBJS += passes/techmap/abc_new.o | ||||||
| ifneq ($(ABCEXTERNAL),) | ifneq ($(ABCEXTERNAL),) | ||||||
| passes/techmap/abc.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | passes/techmap/abc.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | ||||||
| passes/techmap/abc9.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | passes/techmap/abc9.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | ||||||
| passes/techmap/abc9_exe.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | passes/techmap/abc9_exe.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | ||||||
|  | passes/techmap/abc_new.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' | ||||||
| endif | endif | ||||||
| endif | endif | ||||||
| 
 | 
 | ||||||
|  |  | ||||||
|  | @ -220,7 +220,8 @@ struct Abc9Pass : public ScriptPass | ||||||
| 			std::string arg = args[argidx]; | 			std::string arg = args[argidx]; | ||||||
| 			if ((arg == "-exe" || arg == "-script" || arg == "-D" || | 			if ((arg == "-exe" || arg == "-script" || arg == "-D" || | ||||||
| 						/*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" || | 						/*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" || | ||||||
| 						/*arg == "-box" ||*/ arg == "-W") && | 						/*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" || | ||||||
|  | 						arg == "-constr" || arg == "-dont_use" || arg == "-liberty") && | ||||||
| 					argidx+1 < args.size()) { | 					argidx+1 < args.size()) { | ||||||
| 				if (arg == "-lut" || arg == "-luts") | 				if (arg == "-lut" || arg == "-luts") | ||||||
| 					lut_mode = true; | 					lut_mode = true; | ||||||
|  |  | ||||||
|  | @ -167,8 +167,8 @@ struct abc9_output_filter | ||||||
| void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe_file, | void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe_file, | ||||||
| 		vector<int> lut_costs, bool dff_mode, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode, | 		vector<int> lut_costs, bool dff_mode, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode, | ||||||
| 		bool show_tempdir, std::string box_file, std::string lut_file, | 		bool show_tempdir, std::string box_file, std::string lut_file, | ||||||
| 		std::string wire_delay, std::string tempdir_name | 		std::vector<std::string> liberty_files, std::string wire_delay, std::string tempdir_name, | ||||||
| ) | 		std::string constr_file, std::vector<std::string> dont_use_cells) | ||||||
| { | { | ||||||
| 	std::string abc9_script; | 	std::string abc9_script; | ||||||
| 
 | 
 | ||||||
|  | @ -176,8 +176,17 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe | ||||||
| 		abc9_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str()); | 		abc9_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str()); | ||||||
| 	else if (!lut_file.empty()) | 	else if (!lut_file.empty()) | ||||||
| 		abc9_script += stringf("read_lut \"%s\"; ", lut_file.c_str()); | 		abc9_script += stringf("read_lut \"%s\"; ", lut_file.c_str()); | ||||||
| 	else | 	else if (!liberty_files.empty()) { | ||||||
| 		log_abort(); | 		std::string dont_use_args; | ||||||
|  | 		for (std::string dont_use_cell : dont_use_cells) { | ||||||
|  | 			dont_use_args += stringf("-X \"%s\" ", dont_use_cell.c_str()); | ||||||
|  | 		} | ||||||
|  | 		for (std::string liberty_file : liberty_files) { | ||||||
|  | 			abc9_script += stringf("read_lib %s -w \"%s\" ; ", dont_use_args.c_str(), liberty_file.c_str()); | ||||||
|  | 		} | ||||||
|  | 		if (!constr_file.empty()) | ||||||
|  | 			abc9_script += stringf("read_constr -v \"%s\"; ", constr_file.c_str()); | ||||||
|  | 	} | ||||||
| 
 | 
 | ||||||
| 	log_assert(!box_file.empty()); | 	log_assert(!box_file.empty()); | ||||||
| 	abc9_script += stringf("read_box \"%s\"; ", box_file.c_str()); | 	abc9_script += stringf("read_box \"%s\"; ", box_file.c_str()); | ||||||
|  | @ -359,6 +368,26 @@ struct Abc9ExePass : public Pass { | ||||||
| 		log("        of output quality):\n"); | 		log("        of output quality):\n"); | ||||||
| 		log("%s\n", fold_abc9_cmd(RTLIL::constpad.at("abc9.script.default.fast").substr(1,std::string::npos)).c_str()); | 		log("%s\n", fold_abc9_cmd(RTLIL::constpad.at("abc9.script.default.fast").substr(1,std::string::npos)).c_str()); | ||||||
| 		log("\n"); | 		log("\n"); | ||||||
|  | 		log("    -constr <file>\n"); | ||||||
|  | 		log("        pass this file with timing constraints to ABC.\n"); | ||||||
|  | 		log("        use with -liberty.\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("        a constr file contains two lines:\n"); | ||||||
|  | 		log("            set_driving_cell <cell_name>\n"); | ||||||
|  | 		log("            set_load <floating_point_number>\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("        the set_driving_cell statement defines which cell type is assumed to\n"); | ||||||
|  | 		log("        drive the primary inputs and the set_load statement sets the load in\n"); | ||||||
|  | 		log("        femtofarads for each primary output.\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    -liberty <file>\n"); | ||||||
|  | 		log("        read the given Liberty file as a description of the target cell library.\n"); | ||||||
|  | 		log("        this option can be used multiple times.\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    -dont_use <cell_name>\n"); | ||||||
|  | 		log("        avoid usage of the technology cell <cell_name> when mapping the design.\n"); | ||||||
|  | 		log("        this option can be used multiple times.\n"); | ||||||
|  | 		log("\n"); | ||||||
| 		log("    -D <picoseconds>\n"); | 		log("    -D <picoseconds>\n"); | ||||||
| 		log("        set delay target. the string {D} in the default scripts above is\n"); | 		log("        set delay target. the string {D} in the default scripts above is\n"); | ||||||
| 		log("        replaced by this option when used, and an empty string otherwise\n"); | 		log("        replaced by this option when used, and an empty string otherwise\n"); | ||||||
|  | @ -411,7 +440,8 @@ struct Abc9ExePass : public Pass { | ||||||
| 		log_header(design, "Executing ABC9_EXE pass (technology mapping using ABC9).\n"); | 		log_header(design, "Executing ABC9_EXE pass (technology mapping using ABC9).\n"); | ||||||
| 
 | 
 | ||||||
| 		std::string exe_file = yosys_abc_executable; | 		std::string exe_file = yosys_abc_executable; | ||||||
| 		std::string script_file, clk_str, box_file, lut_file; | 		std::string script_file, clk_str, box_file, lut_file, constr_file; | ||||||
|  | 		std::vector<std::string> liberty_files, dont_use_cells; | ||||||
| 		std::string delay_target, lutin_shared = "-S 1", wire_delay; | 		std::string delay_target, lutin_shared = "-S 1", wire_delay; | ||||||
| 		std::string tempdir_name; | 		std::string tempdir_name; | ||||||
| 		bool fast_mode = false, dff_mode = false; | 		bool fast_mode = false, dff_mode = false; | ||||||
|  | @ -499,6 +529,18 @@ struct Abc9ExePass : public Pass { | ||||||
| 				tempdir_name = args[++argidx]; | 				tempdir_name = args[++argidx]; | ||||||
| 				continue; | 				continue; | ||||||
| 			} | 			} | ||||||
|  | 			if (arg == "-liberty" && argidx+1 < args.size()) { | ||||||
|  | 				liberty_files.push_back(args[++argidx]); | ||||||
|  | 				continue; | ||||||
|  | 			} | ||||||
|  | 			if (arg == "-dont_use" && argidx+1 < args.size()) { | ||||||
|  | 				dont_use_cells.push_back(args[++argidx]); | ||||||
|  | 				continue; | ||||||
|  | 			} | ||||||
|  | 			if (arg == "-constr" && argidx+1 < args.size()) { | ||||||
|  | 				constr_file = args[++argidx]; | ||||||
|  | 				continue; | ||||||
|  | 			} | ||||||
| 			break; | 			break; | ||||||
| 		} | 		} | ||||||
| 		extra_args(args, argidx, design); | 		extra_args(args, argidx, design); | ||||||
|  | @ -562,7 +604,8 @@ struct Abc9ExePass : public Pass { | ||||||
| 
 | 
 | ||||||
| 		abc9_module(design, script_file, exe_file, lut_costs, dff_mode, | 		abc9_module(design, script_file, exe_file, lut_costs, dff_mode, | ||||||
| 				delay_target, lutin_shared, fast_mode, show_tempdir, | 				delay_target, lutin_shared, fast_mode, show_tempdir, | ||||||
| 				box_file, lut_file, wire_delay, tempdir_name); | 				box_file, lut_file, liberty_files, wire_delay, tempdir_name, | ||||||
|  | 				constr_file, dont_use_cells); | ||||||
| 	} | 	} | ||||||
| } Abc9ExePass; | } Abc9ExePass; | ||||||
| 
 | 
 | ||||||
|  |  | ||||||
							
								
								
									
										153
									
								
								passes/techmap/abc_new.cc
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										153
									
								
								passes/techmap/abc_new.cc
									
										
									
									
									
										Normal file
									
								
							|  | @ -0,0 +1,153 @@ | ||||||
|  | /*
 | ||||||
|  |  *  yosys -- Yosys Open SYnthesis Suite | ||||||
|  |  * | ||||||
|  |  *  Copyright (C) 2024  Martin Povišer <povik@cutebit.org> | ||||||
|  |  * | ||||||
|  |  *  Permission to use, copy, modify, and/or distribute this software for any | ||||||
|  |  *  purpose with or without fee is hereby granted, provided that the above | ||||||
|  |  *  copyright notice and this permission notice appear in all copies. | ||||||
|  |  * | ||||||
|  |  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES | ||||||
|  |  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF | ||||||
|  |  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR | ||||||
|  |  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES | ||||||
|  |  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN | ||||||
|  |  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF | ||||||
|  |  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. | ||||||
|  |  * | ||||||
|  |  */ | ||||||
|  | 
 | ||||||
|  | #include "kernel/register.h" | ||||||
|  | #include "kernel/rtlil.h" | ||||||
|  | 
 | ||||||
|  | USING_YOSYS_NAMESPACE | ||||||
|  | PRIVATE_NAMESPACE_BEGIN | ||||||
|  | 
 | ||||||
|  | struct AbcNewPass : public ScriptPass { | ||||||
|  | 	AbcNewPass() : ScriptPass("abc_new", "(experimental) use ABC for SC technology mapping (new)") | ||||||
|  | 	{ | ||||||
|  | 		experimental(); | ||||||
|  | 	} | ||||||
|  | 
 | ||||||
|  | 	void help() override | ||||||
|  | 	{ | ||||||
|  | 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    abc_new [options] [selection]\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("This command uses the ABC tool [1] to optimize the current design and map it to\n"); | ||||||
|  | 		log("the target standard cell library.\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    -run <from_label>:<to_label>\n"); | ||||||
|  | 		log("        only run the commands between the labels (see below). an empty\n"); | ||||||
|  | 		log("        from label is synonymous to 'begin', and empty to label is\n"); | ||||||
|  | 		log("        synonymous to the end of the command list.\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("    -exe <command>\n"); | ||||||
|  | 		log("    -script <file>\n"); | ||||||
|  | 		log("    -D <picoseconds>\n"); | ||||||
|  | 		log("    -constr <file>\n"); | ||||||
|  | 		log("    -dont_use <cell_name>\n"); | ||||||
|  | 		log("    -liberty <file>\n"); | ||||||
|  | 		log("        these options are passed on to the 'abc9_exe' command which invokes\n"); | ||||||
|  | 		log("        the ABC tool on individual modules of the design. please see\n"); | ||||||
|  | 		log("        'help abc9_exe' for more details\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		log("[1] http://www.eecs.berkeley.edu/~alanmi/abc/\n"); | ||||||
|  | 		log("\n"); | ||||||
|  | 		help_script(); | ||||||
|  | 		log("\n"); | ||||||
|  | 	} | ||||||
|  | 
 | ||||||
|  | 	bool cleanup; | ||||||
|  | 	std::string abc_exe_options; | ||||||
|  | 
 | ||||||
|  | 	void execute(std::vector<std::string> args, RTLIL::Design *d) override | ||||||
|  | 	{ | ||||||
|  | 		std::string run_from, run_to; | ||||||
|  | 		cleanup = true; | ||||||
|  | 		size_t argidx; | ||||||
|  | 		for (argidx = 1; argidx < args.size(); argidx++) { | ||||||
|  | 			if (args[argidx] == "-exe" || args[argidx] == "-script" || | ||||||
|  | 					args[argidx] == "-D" || | ||||||
|  | 					args[argidx] == "-constr" || args[argidx] == "-dont_use" || | ||||||
|  | 					args[argidx] == "-liberty") { | ||||||
|  | 				abc_exe_options += " " + args[argidx] + " " + args[argidx + 1]; | ||||||
|  | 				argidx++; | ||||||
|  | 			} else if (args[argidx] == "-run" && argidx + 1 < args.size()) { | ||||||
|  | 				size_t pos = args[++argidx].find(':'); | ||||||
|  | 				if (pos == std::string::npos) | ||||||
|  | 					break; | ||||||
|  | 				run_from = args[argidx].substr(0, pos); | ||||||
|  | 				run_to = args[argidx].substr(pos + 1); | ||||||
|  | 			} else if (args[argidx] == "-nocleanup") { | ||||||
|  | 				cleanup = false; | ||||||
|  | 			} else { | ||||||
|  | 				break; | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 		extra_args(args, argidx, d); | ||||||
|  | 
 | ||||||
|  | 		log_header(d, "Executing ABC_NEW pass.\n"); | ||||||
|  | 		log_push(); | ||||||
|  | 		run_script(d, run_from, run_to); | ||||||
|  | 		log_pop(); | ||||||
|  | 	} | ||||||
|  | 
 | ||||||
|  | 	void script() override | ||||||
|  | 	{ | ||||||
|  | 		if (check_label("check")) { | ||||||
|  | 			run("abc9_ops -check");	 | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		if (check_label("prep_boxes")) { | ||||||
|  | 			run("box_derive"); | ||||||
|  | 			run("abc9_ops -prep_box"); | ||||||
|  | 		} | ||||||
|  | 
 | ||||||
|  | 		if (check_label("map")) { | ||||||
|  | 			std::vector<Module *> selected_modules; | ||||||
|  | 
 | ||||||
|  | 			if (!help_mode) { | ||||||
|  | 				selected_modules = active_design->selected_whole_modules_warn(); | ||||||
|  | 				active_design->selection_stack.emplace_back(false); | ||||||
|  | 			} else { | ||||||
|  | 				selected_modules = {nullptr}; | ||||||
|  | 				run("foreach module in selection"); | ||||||
|  | 			} | ||||||
|  | 
 | ||||||
|  | 			for (auto mod : selected_modules) { | ||||||
|  | 				std::string tmpdir = "<abc-temp-dir>"; | ||||||
|  | 				std::string modname = "<module>"; | ||||||
|  | 				std::string exe_options = "[options]"; | ||||||
|  | 				if (!help_mode) { | ||||||
|  | 					tmpdir = cleanup ? (get_base_tmpdir() + "/") : "_tmp_"; | ||||||
|  | 					tmpdir += proc_program_prefix() + "yosys-abc-XXXXXX"; | ||||||
|  | 					tmpdir = make_temp_dir(tmpdir); | ||||||
|  | 					modname = mod->name.str(); | ||||||
|  | 					exe_options = abc_exe_options; | ||||||
|  | 					log_header(active_design, "Mapping module '%s'.\n", log_id(mod)); | ||||||
|  | 					log_push(); | ||||||
|  | 					active_design->selection().select(mod); | ||||||
|  | 				} | ||||||
|  | 
 | ||||||
|  | 				run(stringf("  abc9_ops -write_box %s/input.box", tmpdir.c_str())); | ||||||
|  | 				run(stringf("  write_xaiger2 -mapping_prep -map2 %s/input.map2 %s/input.xaig", tmpdir.c_str(), tmpdir.c_str())); | ||||||
|  | 				run(stringf("  abc9_exe %s -cwd %s -box %s/input.box", exe_options.c_str(), tmpdir.c_str(), tmpdir.c_str())); | ||||||
|  | 				run(stringf("  read_xaiger2 -sc_mapping -module_name %s -map2 %s/input.map2 %s/output.aig", | ||||||
|  | 							modname.c_str(), tmpdir.c_str(), tmpdir.c_str())); | ||||||
|  | 
 | ||||||
|  | 				if (!help_mode) { | ||||||
|  | 					active_design->selection().selected_modules.clear(); | ||||||
|  | 					log_pop(); | ||||||
|  | 				} | ||||||
|  | 			} | ||||||
|  | 
 | ||||||
|  | 			if (!help_mode) { | ||||||
|  | 				active_design->selection_stack.pop_back(); | ||||||
|  | 			} | ||||||
|  | 		} | ||||||
|  | 	} | ||||||
|  | } AbcNewPass; | ||||||
|  | 
 | ||||||
|  | PRIVATE_NAMESPACE_END | ||||||
|  | @ -84,14 +84,14 @@ assign name``_y2 = op name``_a2; | ||||||
| `BIOP(xnor, ~^, 3, 3, 3) | `BIOP(xnor, ~^, 3, 3, 3) | ||||||
| `BIOP(logic_and, &&, 3, 3, 1) | `BIOP(logic_and, &&, 3, 3, 1) | ||||||
| `BIOP(logic_or, ||, 3, 3, 1) | `BIOP(logic_or, ||, 3, 3, 1) | ||||||
| `BIOP(logic_eq, ==, 3, 3, 1) | `BIOP(eq, ==, 3, 3, 1) | ||||||
| `BIOP(logic_ne, !=, 3, 3, 1) | `BIOP(ne, !=, 3, 3, 1) | ||||||
| `BIOP(logic_lt, <, 3, 3, 1) | `BIOP(lt, <, 3, 3, 1) | ||||||
| `BIOP(logic_le, <=, 3, 3, 1) | `BIOP(le, <=, 3, 3, 1) | ||||||
| `BIOP(logic_gt, >, 3, 3, 1) | `BIOP(gt, >, 3, 3, 1) | ||||||
| `BIOP(logic_ge, >=, 3, 3, 1) | `BIOP(ge, >=, 3, 3, 1) | ||||||
| `UNOP(pos, +, 3) | `UNOP(pos, +, 3) | ||||||
| `UNOP(neg, ~, 3) | `UNOP(not, ~, 3) | ||||||
| `UNOP_REDUCE(logic_not, !, 3) | `UNOP_REDUCE(logic_not, !, 3) | ||||||
| `UNOP_REDUCE(reduce_and, &, 3) | `UNOP_REDUCE(reduce_and, &, 3) | ||||||
| `UNOP_REDUCE(reduce_or, |, 3) | `UNOP_REDUCE(reduce_or, |, 3) | ||||||
|  |  | ||||||
							
								
								
									
										224
									
								
								tests/various/aiger2.ys
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										224
									
								
								tests/various/aiger2.ys
									
										
									
									
									
										Normal file
									
								
							|  | @ -0,0 +1,224 @@ | ||||||
|  | read_verilog -icells <<EOF | ||||||
|  | module test(); | ||||||
|  | `define CELL_AY(typ)  \ | ||||||
|  | wire typ``_a, typ``_y; \ | ||||||
|  | $``typ typ(.A(typ``_a), .Y(typ``_y)); | ||||||
|  | `define CELL_ABY(typ)  \ | ||||||
|  | wire typ``_a, typ``_b, typ``_y; \ | ||||||
|  | $``typ typ(.A(typ``_a), .B(typ``_b), .Y(typ``_y)); | ||||||
|  | `define CELL_SABY(typ)  \ | ||||||
|  | wire typ``_a, typ``_b, typ``_y, typ``_s; \ | ||||||
|  | $``typ typ(.A(typ``_a), .B(typ``_b), .Y(typ``_y), .S(typ``_s)); | ||||||
|  | `define CELL_ABCY(typ)  \ | ||||||
|  | wire typ``_a, typ``_b, typ``_c, typ``_y; \ | ||||||
|  | $``typ typ(.A(typ``_a), .B(typ``_b), .C(typ``_c), .Y(typ``_y)); | ||||||
|  | `define CELL_ABCDY(typ)  \ | ||||||
|  | wire typ``_a, typ``_b, typ``_c, typ``_d, typ``_y; \ | ||||||
|  | $``typ typ(.A(typ``_a), .B(typ``_b), .C(typ``_c), .D(typ``_d), .Y(typ``_y)); | ||||||
|  | 
 | ||||||
|  | `CELL_AY(_BUF_) | ||||||
|  | `CELL_AY(_NOT_) | ||||||
|  | `CELL_ABY(_AND_) | ||||||
|  | `CELL_ABY(_NAND_) | ||||||
|  | `CELL_ABY(_OR_) | ||||||
|  | `CELL_ABY(_NOR_) | ||||||
|  | `CELL_ABY(_XOR_) | ||||||
|  | `CELL_ABY(_XNOR_) | ||||||
|  | `CELL_ABY(_ANDNOT_) | ||||||
|  | `CELL_ABY(_ORNOT_) | ||||||
|  | `CELL_SABY(_MUX_) | ||||||
|  | `CELL_SABY(_NMUX_) | ||||||
|  | `CELL_ABCY(_AOI3_) | ||||||
|  | `CELL_ABCY(_OAI3_) | ||||||
|  | `CELL_ABCDY(_AOI4_) | ||||||
|  | `CELL_ABCDY(_OAI4_) | ||||||
|  | endmodule | ||||||
|  | EOF | ||||||
|  | 
 | ||||||
|  | expose -input c:* %ci* w:* %i | ||||||
|  | expose c:* %co* w:* %i | ||||||
|  | copy test gold | ||||||
|  | select test | ||||||
|  | write_aiger2 aiger2_gates.aig | ||||||
|  | select -clear | ||||||
|  | delete test | ||||||
|  | read_aiger -module_name test aiger2_gates.aig | ||||||
|  | select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D | ||||||
|  | miter -equiv -make_outcmp -flatten gold test miter | ||||||
|  | sat -verify -show-ports -prove trigger 0 miter | ||||||
|  | 
 | ||||||
|  | design -reset | ||||||
|  | read_verilog -icells <<EOF | ||||||
|  | module test(); | ||||||
|  | 
 | ||||||
|  | `define BIOP(name,op,w1,w2,wy) \ | ||||||
|  | wire [w1-1:0] name``_a1; \ | ||||||
|  | wire [w2-1:0] name``_b1; \ | ||||||
|  | wire [wy-1:0] name``_y1; \ | ||||||
|  | assign name``_y1 = name``_a1 op name``_b1; \ | ||||||
|  | wire signed [w1-1:0] name``_a2; \ | ||||||
|  | wire signed [w2-1:0] name``_b2; \ | ||||||
|  | wire [wy-1:0] name``_y2; \ | ||||||
|  | assign name``_y2 = name``_a2 op name``_b2; | ||||||
|  | 
 | ||||||
|  | `define UNOP(name,op,w1) \ | ||||||
|  | wire signed [w1-1:0] name``_a1; \ | ||||||
|  | wire signed [w1-1:0] name``_y1; \ | ||||||
|  | assign name``_y1 = op name``_a1; \ | ||||||
|  | wire [w1-1:0] name``_a2; \ | ||||||
|  | wire [w1-1:0] name``_y2; \ | ||||||
|  | assign name``_y2 = op name``_a2; | ||||||
|  | 
 | ||||||
|  | `define UNOP_REDUCE(name,op,w1) \ | ||||||
|  | wire signed [w1-1:0] name``_a1; \ | ||||||
|  | wire name``_y1; \ | ||||||
|  | assign name``_y1 = op name``_a1; \ | ||||||
|  | wire [w1-1:0] name``_a2; \ | ||||||
|  | wire name``_y2; \ | ||||||
|  | assign name``_y2 = op name``_a2; | ||||||
|  | 
 | ||||||
|  | `BIOP(and, &, 3, 4, 5) | ||||||
|  | `BIOP(or, |, 4, 3, 2) | ||||||
|  | `BIOP(xor, ^, 3, 3, 3) | ||||||
|  | `BIOP(xnor, ~^, 3, 3, 3) | ||||||
|  | `BIOP(logic_and, &&, 4, 3, 1) | ||||||
|  | `BIOP(logic_or, ||, 3, 3, 2) | ||||||
|  | `BIOP(eq, ==, 3, 3, 1) | ||||||
|  | `BIOP(ne, !=, 3, 3, 1) | ||||||
|  | `BIOP(lt, <, 3, 3, 1) | ||||||
|  | `BIOP(le, <=, 3, 3, 1) | ||||||
|  | `BIOP(gt, >, 3, 3, 1) | ||||||
|  | `BIOP(ge, >=, 3, 3, 1) | ||||||
|  | `UNOP(not, ~, 3) | ||||||
|  | `UNOP_REDUCE(logic_not, !, 3) | ||||||
|  | `UNOP_REDUCE(reduce_and, &, 3) | ||||||
|  | `UNOP_REDUCE(reduce_or, |, 3) | ||||||
|  | `UNOP_REDUCE(reduce_xor, ^, 3) | ||||||
|  | `UNOP_REDUCE(reduce_xnor, ~^, 3) | ||||||
|  | 
 | ||||||
|  | wire [3:0] mux_a, mux_b, mux_s, mux_y; | ||||||
|  | assign mux_y = mux_s ? mux_b : mux_a; | ||||||
|  | 
 | ||||||
|  | wire [1:0] fa_a, fa_b, fa_c, fa_x, fa_y; | ||||||
|  | \$fa #( | ||||||
|  | 	.WIDTH(2) | ||||||
|  | ) fa(.A(fa_a), .B(fa_b), .C(fa_c), .X(fa_x), .Y(fa_y)); | ||||||
|  | 
 | ||||||
|  | wire [1:0] bwmux_a, bwmux_b, bwmux_s, bwmux_y; | ||||||
|  | \$bwmux #( | ||||||
|  | 	.WIDTH(2) | ||||||
|  | ) bwmux(.A(bwmux_a), .B(bwmux_b), .S(bwmux_s), .Y(bwmux_y)); | ||||||
|  | endmodule | ||||||
|  | EOF | ||||||
|  | 
 | ||||||
|  | expose -input c:* %ci* w:* %i | ||||||
|  | expose c:* %co* w:* %i | ||||||
|  | splitnets -ports | ||||||
|  | copy test gold | ||||||
|  | select test | ||||||
|  | write_aiger2 aiger2_ops.aig | ||||||
|  | select -clear | ||||||
|  | delete test | ||||||
|  | read_aiger -module_name test aiger2_ops.aig | ||||||
|  | select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D | ||||||
|  | miter -equiv -make_outcmp -flatten gold test miter | ||||||
|  | sat -verify -show-ports -prove trigger 0 miter | ||||||
|  | 
 | ||||||
|  | design -reset | ||||||
|  | read_verilog -icells <<EOF | ||||||
|  | module submodule1(a, y1, y2); | ||||||
|  | 	input wire [2:0] a; | ||||||
|  | 	output wire [2:0] y1 = a + 1; | ||||||
|  | 	output wire [2:0] y2 = a + 2; | ||||||
|  | endmodule | ||||||
|  | 
 | ||||||
|  | module submodule2(a, y1); | ||||||
|  | 	input wire [2:0] a; | ||||||
|  | 	output wire [2:0] y1 = ~a; | ||||||
|  | endmodule | ||||||
|  | 
 | ||||||
|  | module test(a, y1, y2); | ||||||
|  | 	input wire [2:0] a; | ||||||
|  | 	output wire [2:0] y1; | ||||||
|  | 	output wire [2:0] y2; | ||||||
|  | 
 | ||||||
|  | 	wire [2:0] m1; | ||||||
|  | 	wire [2:0] m2; | ||||||
|  | 
 | ||||||
|  | 	submodule2 s1(.a(a), .y1(m1)); | ||||||
|  | 	submodule1 s2(.a(m1), .y1(y1), .y2(m2)); | ||||||
|  | 	submodule2 s3(.a(m2), .y1(y2)); | ||||||
|  | endmodule | ||||||
|  | EOF | ||||||
|  | 
 | ||||||
|  | expose -input c:* %ci* w:* %i | ||||||
|  | expose c:* %co* w:* %i | ||||||
|  | splitnets -ports | ||||||
|  | copy test gold | ||||||
|  | flatten gold | ||||||
|  | techmap submodule1 | ||||||
|  | select test | ||||||
|  | write_aiger2 -flatten aiger2_ops.aig | ||||||
|  | select -clear | ||||||
|  | delete test | ||||||
|  | read_aiger -module_name test aiger2_ops.aig | ||||||
|  | select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D | ||||||
|  | miter -equiv -flatten gold test miter | ||||||
|  | sat -verify -prove trigger 0 miter | ||||||
|  | 
 | ||||||
|  | design -reset | ||||||
|  | read_verilog -icells <<EOF | ||||||
|  | module test(); | ||||||
|  | wire [1:0] pmux_a, pmux_s, pmux_y; | ||||||
|  | wire [3:0] pmux_b; | ||||||
|  | \$pmux #( | ||||||
|  | 	.S_WIDTH(2), | ||||||
|  | 	.WIDTH(2) | ||||||
|  | ) pmux(.A(pmux_a), .B(pmux_b), .S(pmux_s), .Y(pmux_y)); | ||||||
|  | endmodule | ||||||
|  | EOF | ||||||
|  | 
 | ||||||
|  | expose -input c:* %ci* w:* %i | ||||||
|  | expose c:* %co* w:* %i | ||||||
|  | splitnets -ports | ||||||
|  | opt_clean | ||||||
|  | copy test gold | ||||||
|  | select test | ||||||
|  | write_aiger2 aiger2_xmodel.aig | ||||||
|  | select -clear | ||||||
|  | delete test | ||||||
|  | read_aiger -module_name test aiger2_xmodel.aig | ||||||
|  | select -assert-none test/t:$_AND_ test/t:$_NOT_ %% test/c:* %D | ||||||
|  | 
 | ||||||
|  | equiv_make gold test equiv | ||||||
|  | equiv_induct -undef equiv | ||||||
|  | equiv_status -assert equiv | ||||||
|  | 
 | ||||||
|  | design -reset | ||||||
|  | read_verilog -icells <<EOF | ||||||
|  | module sm2(input wire [1:0] a, output wire [1:0] y); | ||||||
|  | 	assign y = a + 1; | ||||||
|  | endmodule | ||||||
|  | 
 | ||||||
|  | module sm1(input wire [2:0] a, output wire [2:0] y); | ||||||
|  | 	sm2 inst(a[1:0], y[2:1]); | ||||||
|  | 	assign y[0] = !a[2]; | ||||||
|  | endmodule | ||||||
|  | 
 | ||||||
|  | module top(input wire [4:0] a, output wire [4:0] y); | ||||||
|  | 	sm1 i1(.a(a[2:0]), .y(y[2:0])); | ||||||
|  | 	sm2 i2(.a(a[4:3]), .y(y[4:3])); | ||||||
|  | endmodule | ||||||
|  | EOF | ||||||
|  | 
 | ||||||
|  | prep -top top | ||||||
|  | # deal with arithmetic which is unsupported inside aiger2 | ||||||
|  | techmap t:$add | ||||||
|  | 
 | ||||||
|  | splitnets -ports top | ||||||
|  | write_aiger2 -flatten aiger2_flatten.aig | ||||||
|  | flatten | ||||||
|  | rename top gold | ||||||
|  | read_aiger -module_name gate aiger2_flatten.aig | ||||||
|  | miter -equiv -flatten gold gate miter | ||||||
|  | sat -verify -prove trigger 0 miter | ||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue