Merge remote-tracking branch 'origin/xaig_dff' into eddie/abc9_refactor

CHANGELOG

@@ -57,6 +57,7 @@ Yosys 0.9 .. Yosys 0.9-dev
       always_latch and always_ff)
     - Added "xilinx_dffopt" pass
     - Added "scratchpad" pass
+    - Added "synth_xilinx -dff"
 
 Yosys 0.8 .. Yosys 0.9
 ----------------------

Makefile

@@ -128,7 +128,7 @@ bumpversion:
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = 623b5e8
+ABCREV = c4b12fa
 ABCPULL = 1
 ABCURL ?= https://github.com/berkeley-abc/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1

README.md

@@ -378,6 +378,12 @@ Verilog Attributes and non-standard features
   for example, to specify the clk-to-Q delay of a flip-flop for consideration
   during techmapping.
 
+- The module attribute ``abc9_flop`` is a boolean marking the module as a
+  whitebox that describes the synchronous behaviour of a flip-flop.
+
+- The cell attribute ``abc9_keep`` is a boolean indicating that this black/
+  white box should be preserved through `abc9` mapping.
+
 - The frontend sets attributes ``always_comb``, ``always_latch`` and
   ``always_ff`` on processes derived from SystemVerilog style always blocks
   according to the type of the always. These are checked for correctness in

backends/aiger/xaiger.cc

@@ -78,10 +78,11 @@ struct XAigerWriter
 	Module *module;
 	SigMap sigmap;
 
-	pool<SigBit> input_bits, output_bits;
+	pool<SigBit> input_bits, output_bits, external_bits;
 	dict<SigBit, SigBit> not_map, alias_map;
 	dict<SigBit, pair<SigBit, SigBit>> and_map;
 	vector<SigBit> ci_bits, co_bits;
+	dict<SigBit, std::pair<int,int>> ff_bits;
 	dict<SigBit, float> arrival_times;
 
 	vector<pair<int, int>> aig_gates;
@@ -92,7 +93,6 @@ struct XAigerWriter
 	dict<SigBit, int> ordered_outputs;
 
 	vector<Cell*> box_list;
-	bool omode = false;
 
 	int mkgate(int a0, int a1)
 	{
@@ -140,7 +140,7 @@ struct XAigerWriter
 	{
 		pool<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
-		pool<SigBit> keep_bits;
+		pool<SigBit> inout_bits;
 
 		// promote public wires
 		for (auto wire : module->wires())
@@ -152,52 +152,52 @@ struct XAigerWriter
 			if (wire->port_input)
 				sigmap.add(wire);
 
+		// promote keep wires
 		for (auto wire : module->wires())
-		{
+			if (wire->get_bool_attribute(ID::keep))
-			bool keep = wire->attributes.count("\\keep");
+				sigmap.add(wire);
 
+		for (auto wire : module->wires())
 			for (int i = 0; i < GetSize(wire); i++)
 			{
 				SigBit wirebit(wire, i);
 				SigBit bit = sigmap(wirebit);
 
-				if (bit.wire) {
+				if (bit.wire == nullptr) {
-					undriven_bits.insert(bit);
+					if (wire->port_output) {
-					unused_bits.insert(bit);
+						aig_map[wirebit] = (bit == State::S1) ? 1 : 0;
-				}
+						if (holes_mode)
-
+							output_bits.insert(wirebit);
-				if (keep)
+						//external_bits.insert(wirebit);
-					keep_bits.insert(wirebit);
-
-				if (wire->port_input || keep) {
-					if (bit != wirebit)
-						alias_map[bit] = wirebit;
-					input_bits.insert(wirebit);
-				}
-
-				if (wire->port_output || keep) {
-					if (bit != RTLIL::Sx) {
-						if (bit != wirebit)
-							alias_map[wirebit] = bit;
-						output_bits.insert(wirebit);
 					}
-					else
+					continue;
-						log_debug("Skipping PO '%s' driven by 1'bx\n", log_signal(wirebit));
 				}
-			}
-		}
 
-		for (auto bit : input_bits)
+				undriven_bits.insert(bit);
-			undriven_bits.erase(sigmap(bit));
+				unused_bits.insert(bit);
-		for (auto bit : output_bits)
+
-			if (!bit.wire->port_input)
+				if (wire->port_input)
-				unused_bits.erase(bit);
+					input_bits.insert(bit);
+
+				if (wire->port_output) {
+					if (bit != wirebit)
+						alias_map[wirebit] = bit;
+					if (holes_mode)
+						output_bits.insert(wirebit);
+					else
+						external_bits.insert(wirebit);
+				}
+
+				if (wire->port_input && wire->port_output)
+					inout_bits.insert(wirebit);
+			}
 
 		// TODO: Speed up toposort -- ultimately we care about
 		//       box ordering, but not individual AIG cells
 		dict<SigBit, pool<IdString>> bit_drivers, bit_users;
 		TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
 		bool abc9_box_seen = false;
+		std::vector<Cell*> flop_boxes;
 
 		for (auto cell : module->selected_cells()) {
 			if (cell->type == "$_NOT_")
@@ -235,75 +235,81 @@ struct XAigerWriter
 
 			log_assert(!holes_mode);
 
-			RTLIL::Module* inst_module = module->design->module(cell->type);
+			if (cell->type == "$__ABC9_FF_")
-			if (inst_module && inst_module->attributes.count("\\abc9_box_id")) {
+			{
-				abc9_box_seen = true;
+				SigBit D = sigmap(cell->getPort("\\D").as_bit());
+				SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
+				unused_bits.erase(D);
+				undriven_bits.erase(Q);
+				alias_map[Q] = D;
+				auto r = ff_bits.insert(std::make_pair(D, std::make_pair(0, 2)));
+				log_assert(r.second);
+				continue;
+			}
 
-				if (!holes_mode) {
+			RTLIL::Module* inst_module = module->design->module(cell->type);
-					toposort.node(cell->name);
+			if (inst_module) {
-					for (const auto &conn : cell->connections()) {
+				bool abc9_box = inst_module->attributes.count("\\abc9_box_id") && !cell->get_bool_attribute("\\abc9_keep");
-						auto port_wire = inst_module->wire(conn.first);
+
-						if (port_wire->port_input) {
+				for (const auto &conn : cell->connections()) {
-							// Ignore inout for the sake of topographical ordering
+					auto port_wire = inst_module->wire(conn.first);
-							if (port_wire->port_output) continue;
+
+					if (port_wire->port_output) {
+						int arrival = 0;
+						auto it = port_wire->attributes.find("\\abc9_arrival");
+						if (it != port_wire->attributes.end()) {
+							if (it->second.flags != 0)
+								log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
+							arrival = it->second.as_int();
+						}
+						if (arrival)
+							for (auto bit : sigmap(conn.second))
+								arrival_times[bit] = arrival;
+					}
+
+					if (abc9_box) {
+						// Ignore inout for the sake of topographical ordering
+						if (port_wire->port_input && !port_wire->port_output)
 							for (auto bit : sigmap(conn.second))
 								bit_users[bit].insert(cell->name);
-						}
-
 						if (port_wire->port_output)
 							for (auto bit : sigmap(conn.second))
 								bit_drivers[bit].insert(cell->name);
 					}
 				}
+
+                                if (abc9_box) {
+                                        abc9_box_seen = true;
+
+                                        toposort.node(cell->name);
+
+                                        if (inst_module->attributes.count("\\abc9_flop"))
+                                                flop_boxes.push_back(cell);
+                                        continue;
+                                }
 			}
-			else {
-				bool cell_known = inst_module || cell->known();
-				for (const auto &c : cell->connections()) {
-					if (c.second.is_fully_const()) continue;
-					auto port_wire = inst_module ? inst_module->wire(c.first) : nullptr;
-					auto is_input = (port_wire && port_wire->port_input) || !cell_known || cell->input(c.first);
-					auto is_output = (port_wire && port_wire->port_output) || !cell_known || cell->output(c.first);
-					if (!is_input && !is_output)
-						log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
 
-					if (is_input) {
+			bool cell_known = inst_module || cell->known();
-						for (auto b : c.second) {
+			for (const auto &c : cell->connections()) {
-							Wire *w = b.wire;
+				if (c.second.is_fully_const()) continue;
-							if (!w) continue;
+				auto port_wire = inst_module ? inst_module->wire(c.first) : nullptr;
-							if (!w->port_output || !cell_known) {
+				auto is_input = (port_wire && port_wire->port_input) || !cell_known || cell->input(c.first);
-								SigBit I = sigmap(b);
+				auto is_output = (port_wire && port_wire->port_output) || !cell_known || cell->output(c.first);
-								if (I != b)
+				if (!is_input && !is_output)
-									alias_map[b] = I;
+					log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
+
+				if (is_input) {
+					for (auto b : c.second) {
+						Wire *w = b.wire;
+						if (!w) continue;
+						if (!w->port_output || !cell_known) {
+							SigBit I = sigmap(b);
+							if (I != b)
+								alias_map[b] = I;
+							if (holes_mode)
 								output_bits.insert(b);
-								unused_bits.erase(b);
+							else
-
+								external_bits.insert(b);
-								if (!cell_known)
-									keep_bits.insert(b);
-							}
-						}
-					}
-					if (is_output) {
-						int arrival = 0;
-						if (port_wire) {
-							auto it = port_wire->attributes.find("\\abc9_arrival");
-							if (it != port_wire->attributes.end()) {
-								if (it->second.flags != 0)
-									log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
-								arrival = it->second.as_int();
-							}
-						}
-
-						for (auto b : c.second) {
-							Wire *w = b.wire;
-							if (!w) continue;
-							input_bits.insert(b);
-							SigBit O = sigmap(b);
-							if (O != b)
-								alias_map[O] = b;
-							undriven_bits.erase(O);
-
-							if (arrival)
-								arrival_times[b] = arrival;
 						}
 					}
 				}
@@ -313,6 +319,60 @@ struct XAigerWriter
 		}
 
 		if (abc9_box_seen) {
+			dict<IdString, std::pair<IdString,int>> flop_q;
+			for (auto cell : flop_boxes) {
+				auto r = flop_q.insert(std::make_pair(cell->type, std::make_pair(IdString(), 0)));
+				SigBit d;
+				if (r.second) {
+					for (const auto &conn : cell->connections()) {
+						const SigSpec &rhs = conn.second;
+						if (!rhs.is_bit())
+							continue;
+						if (!ff_bits.count(rhs))
+							continue;
+						r.first->second.first = conn.first;
+						Module *inst_module = module->design->module(cell->type);
+						Wire *wire = inst_module->wire(conn.first);
+						log_assert(wire);
+						auto jt = wire->attributes.find("\\abc9_arrival");
+						if (jt != wire->attributes.end()) {
+							if (jt->second.flags != 0)
+								log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(wire), log_id(cell->type));
+							r.first->second.second = jt->second.as_int();
+						}
+						d = rhs;
+						log_assert(d == sigmap(d));
+						break;
+					}
+				}
+				else
+					d = cell->getPort(r.first->second.first);
+
+				auto &rhs = ff_bits.at(d);
+
+				auto it = cell->attributes.find(ID(abc9_mergeability));
+				log_assert(it != cell->attributes.end());
+				rhs.first = it->second.as_int();
+				cell->attributes.erase(it);
+
+				it = cell->attributes.find(ID(abc9_init));
+				log_assert(it != cell->attributes.end());
+				log_assert(GetSize(it->second) == 1);
+				if (it->second[0] == State::S1)
+					rhs.second = 1;
+				else if (it->second[0] == State::S0)
+					rhs.second = 0;
+				else {
+					log_assert(it->second[0] == State::Sx);
+					rhs.second = 0;
+				}
+				cell->attributes.erase(it);
+
+				auto arrival = r.first->second.second;
+				if (arrival)
+					arrival_times[d] = arrival;
+			}
+
 			for (auto &it : bit_users)
 				if (bit_drivers.count(it.first))
 					for (auto driver_cell : bit_drivers.at(it.first))
@@ -341,7 +401,8 @@ struct XAigerWriter
 				log_assert(cell);
 
 				RTLIL::Module* box_module = module->design->module(cell->type);
-				if (!box_module || !box_module->attributes.count("\\abc9_box_id"))
+				if (!box_module || !box_module->attributes.count("\\abc9_box_id")
+						|| cell->get_bool_attribute("\\abc9_keep"))
 					continue;
 
 				bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */);
@@ -377,7 +438,7 @@ struct XAigerWriter
 									alias_map[b] = I;
 							}
 							co_bits.emplace_back(b);
-							unused_bits.erase(b);
+							unused_bits.erase(I);
 						}
 					}
 					if (w->port_output) {
@@ -401,62 +462,75 @@ struct XAigerWriter
 							SigBit O = sigmap(b);
 							if (O != b)
 								alias_map[O] = b;
+							input_bits.erase(O);
 							undriven_bits.erase(O);
-							input_bits.erase(b);
 						}
 					}
 				}
+
+				// Connect <cell>.$abc9_currQ (inserted by abc9_map.v) as an input to the flop box
+				if (box_module->get_bool_attribute("\\abc9_flop")) {
+					SigSpec rhs = module->wire(stringf("%s.$abc9_currQ", cell->name.c_str()));
+					if (rhs.empty())
+						log_error("'%s.$abc9_currQ' is not a wire present in module '%s'.\n", log_id(cell), log_id(module));
+
+					for (auto b : rhs) {
+						SigBit I = sigmap(b);
+						if (b == RTLIL::Sx)
+							b = State::S0;
+						else if (I != b) {
+							if (I == RTLIL::Sx)
+								alias_map[b] = State::S0;
+							else
+								alias_map[b] = I;
+						}
+						co_bits.emplace_back(b);
+						unused_bits.erase(I);
+					}
+				}
+
 				box_list.emplace_back(cell);
 			}
 
 			// TODO: Free memory from toposort, bit_drivers, bit_users
 		}
 
-		for (auto bit : input_bits) {
+		if (!holes_mode)
-			if (!output_bits.count(bit))
+			for (auto cell : module->cells())
+				if (!module->selected(cell))
+					for (auto &conn : cell->connections())
+						if (cell->input(conn.first))
+							for (auto wirebit : conn.second)
+								if (sigmap(wirebit).wire)
+									external_bits.insert(wirebit);
+
+		// For all bits consumed outside of the selected cells,
+		//   but driven from a selected cell, then add it as
+		//   a primary output
+		for (auto wirebit : external_bits) {
+			SigBit bit = sigmap(wirebit);
+			if (!bit.wire)
 				continue;
-			RTLIL::Wire *wire = bit.wire;
+			if (!undriven_bits.count(bit)) {
-			// If encountering an inout port, or a keep-ed wire, then create a new wire
+				if (bit != wirebit)
-			// with $inout.out suffix, make it a PO driven by the existing inout, and
+					alias_map[wirebit] = bit;
-			// inherit existing inout's drivers
+				output_bits.insert(wirebit);
-			if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
-					|| keep_bits.count(bit)) {
-				RTLIL::IdString wire_name = stringf("$%s$inout.out", wire->name.c_str());
-				RTLIL::Wire *new_wire = module->wire(wire_name);
-				if (!new_wire)
-					new_wire = module->addWire(wire_name, GetSize(wire));
-				SigBit new_bit(new_wire, bit.offset);
-				module->connect(new_bit, bit);
-				if (not_map.count(bit)) {
-					auto a = not_map.at(bit);
-					not_map[new_bit] = a;
-				}
-				else if (and_map.count(bit)) {
-					auto a = and_map.at(bit);
-					and_map[new_bit] = a;
-				}
-				else if (alias_map.count(bit)) {
-					auto a = alias_map.at(bit);
-					alias_map[new_bit] = a;
-				}
-				else
-					alias_map[new_bit] = bit;
-				output_bits.erase(bit);
-				output_bits.insert(new_bit);
 			}
 		}
 
+		for (auto bit : input_bits)
+			undriven_bits.erase(sigmap(bit));
+		for (auto bit : output_bits)
+			unused_bits.erase(sigmap(bit));
 		for (auto bit : unused_bits)
 			undriven_bits.erase(bit);
 
-		if (!undriven_bits.empty() && !holes_mode) {
+		// Make all undriven bits a primary input
-			undriven_bits.sort();
+		if (!holes_mode)
 			for (auto bit : undriven_bits) {
-				log_warning("Treating undriven bit %s.%s like $anyseq.\n", log_id(module), log_signal(bit));
 				input_bits.insert(bit);
+				undriven_bits.erase(bit);
 			}
-			log_warning("Treating a total of %d undriven bits in %s like $anyseq.\n", GetSize(undriven_bits), log_id(module));
-		}
 
 		if (holes_mode) {
 			struct sort_by_port_id {
@@ -484,25 +558,36 @@ struct XAigerWriter
 			aig_map[bit] = 2*aig_m;
 		}
 
-		for (auto bit : ci_bits) {
+		for (const auto &i : ff_bits) {
+			const SigBit &bit = i.first;
 			aig_m++, aig_i++;
+			log_assert(!aig_map.count(bit));
 			aig_map[bit] = 2*aig_m;
 		}
 
+		dict<SigBit, int> ff_aig_map;
+		for (auto &bit : ci_bits) {
+			aig_m++, aig_i++;
+			auto r = aig_map.insert(std::make_pair(bit, 2*aig_m));
+			if (!r.second)
+				ff_aig_map[bit] = 2*aig_m;
+		}
+
 		for (auto bit : co_bits) {
 			ordered_outputs[bit] = aig_o++;
 			aig_outputs.push_back(bit2aig(bit));
 		}
 
-		if (output_bits.empty()) {
-			output_bits.insert(State::S0);
-			omode = true;
-		}
-
 		for (auto bit : output_bits) {
 			ordered_outputs[bit] = aig_o++;
 			aig_outputs.push_back(bit2aig(bit));
 		}
+
+		for (auto &i : ff_bits) {
+			const SigBit &bit = i.first;
+			aig_o++;
+			aig_outputs.push_back(ff_aig_map.at(bit));
+		}
 	}
 
 	void write_aiger(std::ostream &f, bool ascii_mode)
@@ -564,7 +649,6 @@ struct XAigerWriter
 
 		f << "c";
 
-		log_assert(!output_bits.empty());
 		auto write_buffer = [](std::stringstream &buffer, int i32) {
 			int32_t i32_be = to_big_endian(i32);
 			buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
@@ -572,14 +656,14 @@ struct XAigerWriter
 		std::stringstream h_buffer;
 		auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
 		write_h_buffer(1);
-		log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
+		log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ff_bits) + GetSize(ci_bits));
-		write_h_buffer(input_bits.size() + ci_bits.size());
+		write_h_buffer(input_bits.size() + ff_bits.size() + ci_bits.size());
-		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
+		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(ff_bits) + GetSize(co_bits));
-		write_h_buffer(output_bits.size() + GetSize(co_bits));
+		write_h_buffer(output_bits.size() + GetSize(ff_bits) + GetSize(co_bits));
-		log_debug("piNum = %d\n", GetSize(input_bits));
+		log_debug("piNum = %d\n", GetSize(input_bits) + GetSize(ff_bits));
-		write_h_buffer(input_bits.size());
+		write_h_buffer(input_bits.size() + ff_bits.size());
-		log_debug("poNum = %d\n", GetSize(output_bits));
+		log_debug("poNum = %d\n", GetSize(output_bits) + GetSize(ff_bits));
-		write_h_buffer(output_bits.size());
+		write_h_buffer(output_bits.size() + ff_bits.size());
 		log_debug("boxNum = %d\n", GetSize(box_list));
 		write_h_buffer(box_list.size());
 
@@ -595,7 +679,7 @@ struct XAigerWriter
 		//for (auto bit : output_bits)
 		//	write_o_buffer(0);
 
-		if (!box_list.empty()) {
+		if (!box_list.empty() || !ff_bits.empty()) {
 			RTLIL::Module *holes_module = module->design->addModule("$__holes__");
 			log_assert(holes_module);
 
@@ -609,7 +693,7 @@ struct XAigerWriter
 				IdString derived_name = orig_box_module->derive(module->design, cell->parameters);
 				RTLIL::Module* box_module = module->design->module(derived_name);
 				if (box_module->has_processes())
-					log_error("ABC9 box '%s' contains processes!\n", box_module->name.c_str());
+					Pass::call_on_module(module->design, box_module, "proc");
 
 				int box_inputs = 0, box_outputs = 0;
 				auto r = cell_cache.insert(std::make_pair(derived_name, nullptr));
@@ -655,9 +739,9 @@ struct XAigerWriter
 						box_outputs += GetSize(w);
 						for (int i = 0; i < GetSize(w); i++) {
 							if (GetSize(w) == 1)
-								holes_wire = holes_module->addWire(stringf("%s.%s", cell->name.c_str(), log_id(w->name)));
+								holes_wire = holes_module->addWire(stringf("$abc%s.%s", cell->name.c_str(), log_id(w->name)));
 							else
-								holes_wire = holes_module->addWire(stringf("%s.%s[%d]", cell->name.c_str(), log_id(w->name), i));
+								holes_wire = holes_module->addWire(stringf("$abc%s.%s[%d]", cell->name.c_str(), log_id(w->name), i));
 							holes_wire->port_output = true;
 							holes_wire->port_id = port_id++;
 							holes_module->ports.push_back(holes_wire->name);
@@ -675,6 +759,23 @@ struct XAigerWriter
 					}
 				}
 
+				// For flops only, create an extra 1-bit input that drives a new wire
+				//   called "<cell>.$abc9_currQ" that is used below
+				if (box_module->get_bool_attribute("\\abc9_flop")) {
+					log_assert(holes_cell);
+
+					box_inputs++;
+					Wire *holes_wire = holes_module->wire(stringf("\\i%d", box_inputs));
+					if (!holes_wire) {
+						holes_wire = holes_module->addWire(stringf("\\i%d", box_inputs));
+						holes_wire->port_input = true;
+						holes_wire->port_id = port_id++;
+						holes_module->ports.push_back(holes_wire->name);
+					}
+					Wire *w = holes_module->addWire(stringf("%s.$abc9_currQ", cell->name.c_str()));
+					holes_module->connect(w, holes_wire);
+				}
+
 				write_h_buffer(box_inputs);
 				write_h_buffer(box_outputs);
 				write_h_buffer(box_module->attributes.at("\\abc9_box_id").as_int());
@@ -683,13 +784,36 @@ struct XAigerWriter
 
 			std::stringstream r_buffer;
 			auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
-			write_r_buffer(0);
+			log_debug("flopNum = %d\n", GetSize(ff_bits));
+			write_r_buffer(ff_bits.size());
+
+			std::stringstream s_buffer;
+			auto write_s_buffer = std::bind(write_buffer, std::ref(s_buffer), std::placeholders::_1);
+			write_s_buffer(ff_bits.size());
+
+			for (const auto &i : ff_bits) {
+				const SigBit &bit = i.first;
+				int mergeability = i.second.first;
+				log_assert(mergeability > 0);
+				write_r_buffer(mergeability);
+				int init = i.second.second;
+				write_s_buffer(init);
+				write_i_buffer(arrival_times.at(bit, 0));
+				//write_o_buffer(0);
+			}
+
 			f << "r";
 			std::string buffer_str = r_buffer.str();
 			int32_t buffer_size_be = to_big_endian(buffer_str.size());
 			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
 			f.write(buffer_str.data(), buffer_str.size());
 
+			f << "s";
+			buffer_str = s_buffer.str();
+			buffer_size_be = to_big_endian(buffer_str.size());
+			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+			f.write(buffer_str.data(), buffer_str.size());
+
 			if (holes_module) {
 				log_push();
 
@@ -697,34 +821,64 @@ struct XAigerWriter
 				//holes_module->fixup_ports();
 				holes_module->check();
 
-				holes_module->design->selection_stack.emplace_back(false);
-				RTLIL::Selection& sel = holes_module->design->selection_stack.back();
-				sel.select(holes_module);
-
-				Pass::call(holes_module->design, "flatten -wb");
-
 				// Cannot techmap/aigmap/check all lib_whitebox-es outside of write_xaiger
 				//   since boxes may contain parameters in which case `flatten` would have
 				//   created a new $paramod ...
-				Pass::call(holes_module->design, "techmap");
+				Pass::call_on_module(holes_module->design, holes_module, "flatten -wb; techmap; aigmap");
-				Pass::call(holes_module->design, "aigmap");
-				for (auto cell : holes_module->cells())
-					if (!cell->type.in("$_NOT_", "$_AND_"))
-						log_error("Whitebox contents cannot be represented as AIG. Please verify whiteboxes are synthesisable.\n");
 
-				holes_module->design->selection_stack.pop_back();
+				dict<SigSig, SigSig> replace;
+				for (auto it = holes_module->cells_.begin(); it != holes_module->cells_.end(); ) {
+					auto cell = it->second;
+					if (cell->type.in("$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
+								"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1", "$_DFF_PP0_", "$_DFF_PP1_")) {
+						SigBit D = cell->getPort("\\D");
+						SigBit Q = cell->getPort("\\Q");
+						// Remove the DFF cell from what needs to be a combinatorial box
+						it = holes_module->cells_.erase(it);
+						Wire *port;
+						if (GetSize(Q.wire) == 1)
+							port = holes_module->wire(stringf("$abc%s", Q.wire->name.c_str()));
+						else
+							port = holes_module->wire(stringf("$abc%s[%d]", Q.wire->name.c_str(), Q.offset));
+						log_assert(port);
+						// Prepare to replace "assign <port> = DFF.Q;" with "assign <port> = DFF.D;"
+						//   in order to extract the combinatorial control logic that feeds the box
+						//   (i.e. clock enable, synchronous reset, etc.)
+						replace.insert(std::make_pair(SigSig(port,Q), SigSig(port,D)));
+						// Since `flatten` above would have created wires named "<cell>.Q",
+						//   extract the pre-techmap cell name
+						auto pos = Q.wire->name.str().rfind(".");
+						log_assert(pos != std::string::npos);
+						IdString driver = Q.wire->name.substr(0, pos);
+						// And drive the signal that was previously driven by "DFF.Q" (typically
+						//   used to implement clock-enable functionality) with the "<cell>.$abc9_currQ"
+						//   wire (which itself is driven an input port) we inserted above
+						Wire *currQ = holes_module->wire(stringf("%s.$abc9_currQ", driver.c_str()));
+						log_assert(currQ);
+						holes_module->connect(Q, currQ);
+						continue;
+					}
+					else if (!cell->type.in("$_NOT_", "$_AND_"))
+						log_error("Whitebox contents cannot be represented as AIG. Please verify whiteboxes are synthesisable.\n");
+					++it;
+				}
+
+				for (auto &conn : holes_module->connections_) {
+					auto it = replace.find(conn);
+					if (it != replace.end())
+						conn = it->second;
+				}
 
 				// Move into a new (temporary) design so that "clean" will only
 				// operate (and run checks on) this one module
 				RTLIL::Design *holes_design = new RTLIL::Design;
-				holes_module->design->modules_.erase(holes_module->name);
+				module->design->modules_.erase(holes_module->name);
 				holes_design->add(holes_module);
-				Pass::call(holes_design, "clean -purge");
+				Pass::call(holes_design, "opt -purge");
 
 				std::stringstream a_buffer;
 				XAigerWriter writer(holes_module, true /* holes_mode */);
 				writer.write_aiger(a_buffer, false /*ascii_mode*/);
-
 				delete holes_design;
 
 				f << "a";
@@ -755,6 +909,11 @@ struct XAigerWriter
 		//f.write(buffer_str.data(), buffer_str.size());
 
 		f << stringf("Generated by %s\n", yosys_version_str);
+
+		module->design->scratchpad_set_int("write_xaiger.num_ands", and_map.size());
+		module->design->scratchpad_set_int("write_xaiger.num_wires", aig_map.size());
+		module->design->scratchpad_set_int("write_xaiger.num_inputs", input_bits.size());
+		module->design->scratchpad_set_int("write_xaiger.num_outputs", output_bits.size());
 	}
 
 	void write_map(std::ostream &f, bool verbose_map)
@@ -781,7 +940,8 @@ struct XAigerWriter
 
 				if (output_bits.count(b)) {
 					int o = ordered_outputs.at(b);
-					output_lines[o] += stringf("output %d %d %s\n", o - GetSize(co_bits), i, log_id(wire));
+					int init = 2;
+					output_lines[o] += stringf("output %d %d %s %d\n", o - GetSize(co_bits), i, log_id(wire), init);
 					continue;
 				}
 
@@ -805,8 +965,6 @@ struct XAigerWriter
 			f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name));
 
 		output_lines.sort();
-		if (omode)
-			output_lines[State::S0] = "output 0 0 $__dummy__\n";
 		for (auto &it : output_lines)
 			f << it.second;
 		log_assert(output_lines.size() == output_bits.size());

frontends/aiger/aigerparse.cc

@@ -255,7 +255,7 @@ end_of_header:
 	else
 		log_abort();
 
-	RTLIL::Wire* n0 = module->wire("\\__0__");
+	RTLIL::Wire* n0 = module->wire("$0");
 	if (n0)
 		module->connect(n0, State::S0);
 
@@ -316,14 +316,14 @@ static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned litera
 {
 	const unsigned variable = literal >> 1;
 	const bool invert = literal & 1;
-	RTLIL::IdString wire_name(stringf("\\__%d%s__", variable, invert ? "b" : ""));
+	RTLIL::IdString wire_name(stringf("$%d%s", variable, invert ? "b" : ""));
 	RTLIL::Wire *wire = module->wire(wire_name);
 	if (wire) return wire;
 	log_debug2("Creating %s\n", wire_name.c_str());
 	wire = module->addWire(wire_name);
 	wire->port_input = wire->port_output = false;
 	if (!invert) return wire;
-	RTLIL::IdString wire_inv_name(stringf("\\__%d__", variable));
+	RTLIL::IdString wire_inv_name(stringf("$%d", variable));
 	RTLIL::Wire *wire_inv = module->wire(wire_inv_name);
 	if (wire_inv) {
 		if (module->cell(wire_inv_name)) return wire;
@@ -335,7 +335,7 @@ static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned litera
 	}
 
 	log_debug2("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str());
-	module->addNotGate(stringf("\\__%d__$not", variable), wire_inv, wire);
+	module->addNotGate(stringf("$%d$not", variable), wire_inv, wire);
 
 	return wire;
 }
@@ -372,108 +372,102 @@ void AigerReader::parse_xaiger(const dict<int,IdString> &box_lookup)
 	else
 		log_abort();
 
-	RTLIL::Wire* n0 = module->wire("\\__0__");
+	RTLIL::Wire* n0 = module->wire("$0");
 	if (n0)
 		module->connect(n0, State::S0);
 
+	int c = f.get();
+	if (c != 'c')
+		log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c);
+	if (f.peek() == '\n')
+		f.get();
+
 	// Parse footer (symbol table, comments, etc.)
 	std::string s;
-	bool comment_seen = false;
+	for (int c = f.get(); c != EOF; c = f.get()) {
-	for (int c = f.peek(); c != EOF; c = f.peek()) {
+		// XAIGER extensions
-		if (comment_seen || c == 'c') {
+		if (c == 'm') {
-			if (!comment_seen) {
+			uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				f.ignore(1);
+			uint32_t lutNum = parse_xaiger_literal(f);
-				c = f.peek();
+			uint32_t lutSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				comment_seen = true;
+			log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize, lutNum, lutSize);
-			}
+			ConstEvalAig ce(module);
-			if (c == '\n')
+			for (unsigned i = 0; i < lutNum; ++i) {
-				break;
+				uint32_t rootNodeID = parse_xaiger_literal(f);
-			f.ignore(1);
+				uint32_t cutLeavesM = parse_xaiger_literal(f);
-			// XAIGER extensions
+				log_debug2("rootNodeID=%d cutLeavesM=%d\n", rootNodeID, cutLeavesM);
-			if (c == 'm') {
+				RTLIL::Wire *output_sig = module->wire(stringf("$%d", rootNodeID));
-				uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+				uint32_t nodeID;
-				uint32_t lutNum = parse_xaiger_literal(f);
+				RTLIL::SigSpec input_sig;
-				uint32_t lutSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+				for (unsigned j = 0; j < cutLeavesM; ++j) {
-				log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize, lutNum, lutSize);
+					nodeID = parse_xaiger_literal(f);
-				ConstEvalAig ce(module);
+					log_debug2("\t%u\n", nodeID);
-				for (unsigned i = 0; i < lutNum; ++i) {
+					RTLIL::Wire *wire = module->wire(stringf("$%d", nodeID));
-					uint32_t rootNodeID = parse_xaiger_literal(f);
+					log_assert(wire);
-					uint32_t cutLeavesM = parse_xaiger_literal(f);
+					input_sig.append(wire);
-					log_debug2("rootNodeID=%d cutLeavesM=%d\n", rootNodeID, cutLeavesM);
-					RTLIL::Wire *output_sig = module->wire(stringf("\\__%d__", rootNodeID));
-					uint32_t nodeID;
-					RTLIL::SigSpec input_sig;
-					for (unsigned j = 0; j < cutLeavesM; ++j) {
-						nodeID = parse_xaiger_literal(f);
-						log_debug2("\t%u\n", nodeID);
-						RTLIL::Wire *wire = module->wire(stringf("\\__%d__", nodeID));
-						log_assert(wire);
-						input_sig.append(wire);
-					}
-					// TODO: Compute LUT mask from AIG in less than O(2 ** input_sig.size())
-					ce.clear();
-					ce.compute_deps(output_sig, input_sig.to_sigbit_pool());
-					RTLIL::Const lut_mask(RTLIL::State::Sx, 1 << input_sig.size());
-					for (int j = 0; j < (1 << cutLeavesM); ++j) {
-						int gray = j ^ (j >> 1);
-						ce.set_incremental(input_sig, RTLIL::Const{gray, static_cast<int>(cutLeavesM)});
-						RTLIL::SigBit o(output_sig);
-						bool success YS_ATTRIBUTE(unused) = ce.eval(o);
-						log_assert(success);
-						log_assert(o.wire == nullptr);
-						lut_mask[gray] = o.data;
-					}
-					RTLIL::Cell *output_cell = module->cell(stringf("\\__%d__$and", rootNodeID));
-					log_assert(output_cell);
-					module->remove(output_cell);
-					module->addLut(stringf("\\__%d__$lut", rootNodeID), input_sig, output_sig, std::move(lut_mask));
 				}
-			}
+				// TODO: Compute LUT mask from AIG in less than O(2 ** input_sig.size())
-			else if (c == 'r') {
+				ce.clear();
-				uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+				ce.compute_deps(output_sig, input_sig.to_sigbit_pool());
-				flopNum = parse_xaiger_literal(f);
+				RTLIL::Const lut_mask(RTLIL::State::Sx, 1 << input_sig.size());
-				log_debug("flopNum: %u\n", flopNum);
+				for (int j = 0; j < (1 << cutLeavesM); ++j) {
-				log_assert(dataSize == (flopNum+1) * sizeof(uint32_t));
+					int gray = j ^ (j >> 1);
-				f.ignore(flopNum * sizeof(uint32_t));
+					ce.set_incremental(input_sig, RTLIL::Const{gray, static_cast<int>(cutLeavesM)});
-			}
+					RTLIL::SigBit o(output_sig);
-			else if (c == 'n') {
+					bool success YS_ATTRIBUTE(unused) = ce.eval(o);
-				parse_xaiger_literal(f);
+					log_assert(success);
-				f >> s;
+					log_assert(o.wire == nullptr);
-				log_debug("n: '%s'\n", s.c_str());
+					lut_mask[gray] = o.data;
-			}
-			else if (c == 'h') {
-				f.ignore(sizeof(uint32_t));
-				uint32_t version YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				log_assert(version == 1);
-				uint32_t ciNum YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				log_debug("ciNum = %u\n", ciNum);
-				uint32_t coNum YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				log_debug("coNum = %u\n", coNum);
-				piNum = parse_xaiger_literal(f);
-				log_debug("piNum = %u\n", piNum);
-				uint32_t poNum YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				log_debug("poNum = %u\n", poNum);
-				uint32_t boxNum = parse_xaiger_literal(f);
-				log_debug("boxNum = %u\n", boxNum);
-				for (unsigned i = 0; i < boxNum; i++) {
-					f.ignore(2*sizeof(uint32_t));
-					uint32_t boxUniqueId = parse_xaiger_literal(f);
-					log_assert(boxUniqueId > 0);
-					uint32_t oldBoxNum = parse_xaiger_literal(f);
-					RTLIL::Cell* cell = module->addCell(stringf("$__box%u__", oldBoxNum), box_lookup.at(boxUniqueId));
-					boxes.emplace_back(cell);
 				}
-			}
+				RTLIL::Cell *output_cell = module->cell(stringf("$%d$and", rootNodeID));
-			else if (c == 'a' || c == 'i' || c == 'o') {
+				log_assert(output_cell);
-				uint32_t dataSize = parse_xaiger_literal(f);
+				module->remove(output_cell);
-				f.ignore(dataSize);
+				module->addLut(stringf("$%d$lut", rootNodeID), input_sig, output_sig, std::move(lut_mask));
-			}
-			else {
-				break;
 			}
 		}
-		else
+		else if (c == 'r') {
-			log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c);
+			uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			flopNum = parse_xaiger_literal(f);
+			log_debug("flopNum = %u\n", flopNum);
+			log_assert(dataSize == (flopNum+1) * sizeof(uint32_t));
+			f.ignore(flopNum * sizeof(uint32_t));
+		}
+		else if (c == 'n') {
+			parse_xaiger_literal(f);
+			f >> s;
+			log_debug("n: '%s'\n", s.c_str());
+		}
+		else if (c == 'h') {
+			f.ignore(sizeof(uint32_t));
+			uint32_t version YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			log_assert(version == 1);
+			uint32_t ciNum YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			log_debug("ciNum = %u\n", ciNum);
+			uint32_t coNum YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			log_debug("coNum = %u\n", coNum);
+			piNum = parse_xaiger_literal(f);
+			log_debug("piNum = %u\n", piNum);
+			uint32_t poNum YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			log_debug("poNum = %u\n", poNum);
+			uint32_t boxNum = parse_xaiger_literal(f);
+			log_debug("boxNum = %u\n", boxNum);
+			for (unsigned i = 0; i < boxNum; i++) {
+				f.ignore(2*sizeof(uint32_t));
+				uint32_t boxUniqueId = parse_xaiger_literal(f);
+				log_assert(boxUniqueId > 0);
+				uint32_t oldBoxNum = parse_xaiger_literal(f);
+				RTLIL::Cell* cell = module->addCell(stringf("$__box%u", oldBoxNum), box_lookup.at(boxUniqueId));
+				boxes.emplace_back(cell);
+			}
+		}
+		else if (c == 'a' || c == 'i' || c == 'o' || c == 's') {
+			uint32_t dataSize = parse_xaiger_literal(f);
+			f.ignore(dataSize);
+			log_debug("ignoring '%c'\n", c);
+		}
+		else {
+			break;
+		}
 	}
 
 	post_process();
@@ -550,7 +544,7 @@ void AigerReader::parse_aiger_ascii()
 		log_debug2("%d is an output\n", l1);
 		const unsigned variable = l1 >> 1;
 		const bool invert = l1 & 1;
-		RTLIL::IdString wire_name(stringf("\\__%d%s__", variable, invert ? "b" : "")); // FIXME: is "b" the right suffix?
+		RTLIL::IdString wire_name(stringf("$%d%s", variable, invert ? "b" : "")); // FIXME: is "b" the right suffix?
 		RTLIL::Wire *wire = module->wire(wire_name);
 		if (!wire)
 			wire = createWireIfNotExists(module, l1);
@@ -616,11 +610,12 @@ void AigerReader::parse_aiger_binary()
 	std::string line;
 
 	// Parse inputs
+	int digits = ceil(log10(I));
 	for (unsigned i = 1; i <= I; ++i) {
 		log_debug2("%d is an input\n", i);
-		RTLIL::Wire *wire = createWireIfNotExists(module, i << 1);
+		RTLIL::Wire *wire = module->addWire(stringf("$i%0*d", digits, i));
 		wire->port_input = true;
-		log_assert(!wire->port_output);
+		module->connect(createWireIfNotExists(module, i << 1), wire);
 		inputs.push_back(wire);
 	}
 
@@ -670,23 +665,15 @@ void AigerReader::parse_aiger_binary()
 	}
 
 	// Parse outputs
+	digits = ceil(log10(O));
 	for (unsigned i = 0; i < O; ++i, ++line_count) {
 		if (!(f >> l1))
 			log_error("Line %u cannot be interpreted as an output!\n", line_count);
 
 		log_debug2("%d is an output\n", l1);
-		const unsigned variable = l1 >> 1;
+		RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
-		const bool invert = l1 & 1;
-		RTLIL::IdString wire_name(stringf("\\__%d%s__", variable, invert ? "b" : "")); // FIXME: is "_b" the right suffix?
-		RTLIL::Wire *wire = module->wire(wire_name);
-		if (!wire)
-			wire = createWireIfNotExists(module, l1);
-		else if (wire->port_input || wire->port_output) {
-			RTLIL::Wire *new_wire = module->addWire(NEW_ID);
-			module->connect(new_wire, wire);
-			wire = new_wire;
-		}
 		wire->port_output = true;
+		module->connect(wire, createWireIfNotExists(module, l1));
 		outputs.push_back(wire);
 	}
 	std::getline(f, line); // Ignore up to start of next line
@@ -734,12 +721,19 @@ void AigerReader::parse_aiger_binary()
 void AigerReader::post_process()
 {
 	pool<IdString> seen_boxes;
-	unsigned ci_count = 0, co_count = 0;
+	pool<IdString> flops;
+	unsigned ci_count = 0, co_count = 0, flop_count = 0;
 	for (auto cell : boxes) {
 		RTLIL::Module* box_module = design->module(cell->type);
 		log_assert(box_module);
 
+		bool is_flop = false;
 		if (seen_boxes.insert(cell->type).second) {
+			if (box_module->attributes.count("\\abc9_flop")) {
+				log_assert(flop_count < flopNum);
+				flops.insert(cell->type);
+				is_flop = true;
+			}
 			auto it = box_module->attributes.find("\\abc9_carry");
 			if (it != box_module->attributes.end()) {
 				RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
@@ -779,6 +773,8 @@ void AigerReader::post_process()
 				carry_out->port_id = ports.size();
 			}
 		}
+		else
+			is_flop = flops.count(cell->type);
 
 		// NB: Assume box_module->ports are sorted alphabetically
 		//     (as RTLIL::Module::fixup_ports() would do)
@@ -804,9 +800,32 @@ void AigerReader::post_process()
 				}
 				rhs.append(wire);
 			}
-
 			cell->setPort(port_name, rhs);
 		}
+
+		if (is_flop) {
+			log_assert(co_count < outputs.size());
+			Wire *wire = outputs[co_count++];
+			log_assert(wire);
+			log_assert(wire->port_output);
+			wire->port_output = false;
+
+			RTLIL::Wire *d = outputs[outputs.size() - flopNum + flop_count];
+			log_assert(d);
+			log_assert(d->port_output);
+			d->port_output = false;
+
+			RTLIL::Wire *q = inputs[piNum - flopNum + flop_count];
+			log_assert(q);
+			log_assert(q->port_input);
+			q->port_input = false;
+
+			auto ff = module->addCell(NEW_ID, "$__ABC9_FF_");
+			ff->setPort("\\D", d);
+			ff->setPort("\\Q", q);
+			flop_count++;
+			continue;
+		}
 	}
 
 	dict<RTLIL::IdString, int> wideports_cache;
@@ -868,16 +887,7 @@ void AigerReader::post_process()
 					// simply connect the latter to the former
 					RTLIL::Wire* existing = module->wire(escaped_s);
 					if (!existing) {
-						if (escaped_s.ends_with("$inout.out")) {
+						module->rename(wire, escaped_s);
-							wire->port_output = false;
-							RTLIL::Wire *in_wire = module->wire(escaped_s.substr(1, escaped_s.size()-11));
-							log_assert(in_wire);
-							log_assert(in_wire->port_input && !in_wire->port_output);
-							in_wire->port_output = true;
-							module->connect(in_wire, wire);
-						}
-						else
-							module->rename(wire, escaped_s);
 					}
 					else {
 						wire->port_output = false;
@@ -889,19 +899,9 @@ void AigerReader::post_process()
 					std::string indexed_name = stringf("%s[%d]", escaped_s.c_str(), index);
 					RTLIL::Wire* existing = module->wire(indexed_name);
 					if (!existing) {
-						if (escaped_s.ends_with("$inout.out")) {
+						module->rename(wire, indexed_name);
-							wire->port_output = false;
+						if (wideports)
-							RTLIL::Wire *in_wire = module->wire(stringf("%s[%d]", escaped_s.substr(1, escaped_s.size()-11).c_str(), index));
+							wideports_cache[escaped_s] = std::max(wideports_cache[escaped_s], index);
-							log_assert(in_wire);
-							log_assert(in_wire->port_input && !in_wire->port_output);
-							in_wire->port_output = true;
-							module->connect(in_wire, wire);
-						}
-						else {
-							module->rename(wire, indexed_name);
-							if (wideports)
-								wideports_cache[escaped_s] = std::max(wideports_cache[escaped_s], index);
-						}
 					}
 					else {
 						module->connect(wire, existing);
@@ -909,9 +909,13 @@ void AigerReader::post_process()
 					}
 				}
 				log_debug(" -> %s\n", log_id(wire));
+				int init;
+				mf >> init;
+				if (init < 2)
+					wire->attributes["\\init"] = init;
 			}
 			else if (type == "box") {
-				RTLIL::Cell* cell = module->cell(stringf("$__box%d__", variable));
+				RTLIL::Cell* cell = module->cell(stringf("$__box%d", variable));
 				if (cell) { // ABC could have optimised this box away
 					module->rename(cell, escaped_s);
 					for (const auto &i : cell->connections()) {
@@ -968,15 +972,10 @@ void AigerReader::post_process()
 			if (other_wire) {
 				other_wire->port_input = false;
 				other_wire->port_output = false;
-			}
+				if (wire->port_input)
-			if (wire->port_input) {
-				if (other_wire)
 					module->connect(other_wire, SigSpec(wire, i));
-			}
+				else
-			else {
+					module->connect(SigSpec(wire, i), other_wire);
-								  // Since we skip POs that are connected to Sx,
-								  // re-connect them here
-				module->connect(SigSpec(wire, i), other_wire ? other_wire : SigSpec(RTLIL::Sx));
 			}
 		}
 	}

passes/techmap/abc9.cc

@@ -80,8 +80,6 @@ struct Abc9Pass : public ScriptPass
 		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("        (indicating best possible delay).\n");
-//		log("        This also replaces 'dretime' with 'dretime; retime -o {D}' in the\n");
-//		log("        default scripts above.\n");
 		log("\n");
 //		log("    -S <num>\n");
 //		log("        maximum number of LUT inputs shared.\n");
@@ -103,19 +101,6 @@ struct Abc9Pass : public ScriptPass
 		log("        generate netlist using luts. Use the specified costs for luts with 1,\n");
 		log("        2, 3, .. inputs.\n");
 		log("\n");
-//		log("    -dff\n");
-//		log("        also pass $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many\n");
-//		log("        clock domains are automatically partitioned in clock domains and each\n");
-//		log("        domain is passed through ABC independently.\n");
-//		log("\n");
-//		log("    -clk [!]<clock-signal-name>[,[!]<enable-signal-name>]\n");
-//		log("        use only the specified clock domain. this is like -dff, but only FF\n");
-//		log("        cells that belong to the specified clock domain are used.\n");
-//		log("\n");
-//		log("    -keepff\n");
-//		log("        set the \"keep\" attribute on flip-flop output wires. (and thus preserve\n");
-//		log("        them, for example for equivalence checking.)\n");
-//		log("\n");
 		log("    -nocleanup\n");
 		log("        when this option is used, the temporary files created by this pass\n");
 		log("        are not removed. this is useful for debugging.\n");
@@ -136,8 +121,17 @@ struct Abc9Pass : public ScriptPass
 		log("internally. This is not going to \"run ABC on your design\". It will instead run\n");
 		log("ABC on logic snippets extracted from your design. You will not get any useful\n");
 		log("output when passing an ABC script that writes a file. Instead write your full\n");
-		log("design as BLIF file with write_blif and then load that into ABC externally if\n");
+		log("design as an XAIGER file with write_xaiger and then load that into ABC externally\n");
-		log("you want to use ABC to convert your design into another format.\n");
+		log("if you want to use ABC to convert your design into another format.\n");
+		log("\n");
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("Delay targets can also be specified on a per clock basis by attaching a\n");
+		log("'(* abc9_period = <int> *)' attribute onto clock wires (specifically, onto wires\n");
+		log("that appear inside any special '$abc9_clock' wires inserted by abc9_map.v). This\n");
+		log("can be achieved by modifying the source directly, or through a `setattr`\n");
+		log("invocation. Since such attributes cannot yet be propagated through a\n");
+		log("hierarchical design (whether or not it has been uniquified) it is recommended\n");
+		log("that the design be flattened when using this feature.\n");
 		log("\n");
 		log("[1] http://www.eecs.berkeley.edu/~alanmi/abc/\n");
 		log("\n");

passes/techmap/abc9_map.cc

@@ -65,11 +65,6 @@ PRIVATE_NAMESPACE_BEGIN
 
 bool markgroups;
 int map_autoidx;
-SigMap assign_map;
-RTLIL::Module *module;
-
-bool clk_polarity, en_polarity;
-RTLIL::SigSpec clk_sig, en_sig;
 
 inline std::string remap_name(RTLIL::IdString abc9_name)
 {
@@ -201,64 +196,30 @@ struct abc9_output_filter
 	}
 };
 
-void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
+void abc9_module(RTLIL::Design *design, RTLIL::Module *module, std::string script_file, std::string exe_file,
-		/*bool cleanup,*/ vector<int> lut_costs, bool dff_mode, std::string clk_str,
+		vector<int> lut_costs, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode,
-		bool /*keepff*/, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode,
+		const std::vector<RTLIL::Cell*> &/*cells*/, 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, const dict<int,IdString> &box_lookup, bool nomfs, std::string tempdir_name
 )
 {
-	module = current_module;
 	map_autoidx = autoidx++;
 
-	if (clk_str != "$")
+	//FIXME:
-	{
+	//log_header(design, "Extracting gate netlist of module `%s' to `%s/input.xaig'..\n",
-		clk_polarity = true;
+	//		module->name.c_str(), replace_tempdir(tempdir_name, tempdir_name, show_tempdir).c_str());
-		clk_sig = RTLIL::SigSpec();
-
-		en_polarity = true;
-		en_sig = RTLIL::SigSpec();
-	}
-
-	if (!clk_str.empty() && clk_str != "$")
-	{
-		if (clk_str.find(',') != std::string::npos) {
-			int pos = clk_str.find(',');
-			std::string en_str = clk_str.substr(pos+1);
-			clk_str = clk_str.substr(0, pos);
-			if (en_str[0] == '!') {
-				en_polarity = false;
-				en_str = en_str.substr(1);
-			}
-			if (module->wires_.count(RTLIL::escape_id(en_str)) != 0)
-				en_sig = assign_map(RTLIL::SigSpec(module->wires_.at(RTLIL::escape_id(en_str)), 0));
-		}
-		if (clk_str[0] == '!') {
-			clk_polarity = false;
-			clk_str = clk_str.substr(1);
-		}
-		if (module->wires_.count(RTLIL::escape_id(clk_str)) != 0)
-			clk_sig = assign_map(RTLIL::SigSpec(module->wires_.at(RTLIL::escape_id(clk_str)), 0));
-	}
-
-	if (dff_mode && clk_sig.empty())
-		log_cmd_error("Clock domain %s not found.\n", clk_str.c_str());
-
-	log_header(design, "Extracting gate netlist of module `%s' to `%s/input.xaig'..\n",
-			module->name.c_str(), replace_tempdir(tempdir_name, tempdir_name, show_tempdir).c_str());
 
 	std::string abc9_script;
 
 	if (!lut_costs.empty()) {
 		abc9_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str());
 		if (!box_file.empty())
-			abc9_script += stringf("read_box -v %s; ", box_file.c_str());
+			abc9_script += stringf("read_box %s; ", box_file.c_str());
 	}
 	else
 	if (!lut_file.empty()) {
 		abc9_script += stringf("read_lut %s; ", lut_file.c_str());
 		if (!box_file.empty())
-			abc9_script += stringf("read_box -v %s; ", box_file.c_str());
+			abc9_script += stringf("read_box %s; ", box_file.c_str());
 	}
 	else
 		log_abort();
@@ -277,20 +238,10 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		} else
 			abc9_script += stringf("source %s", script_file.c_str());
 	} else if (!lut_costs.empty() || !lut_file.empty()) {
-		//bool all_luts_cost_same = true;
-		//for (int this_cost : lut_costs)
-		//	if (this_cost != lut_costs.front())
-		//		all_luts_cost_same = false;
 		abc9_script += fast_mode ? ABC_FAST_COMMAND_LUT : ABC_COMMAND_LUT;
-		//if (all_luts_cost_same && !fast_mode)
-		//	abc9_script += "; lutpack {S}";
 	} else
 		log_abort();
 
-	//if (script_file.empty() && !delay_target.empty())
-	//	for (size_t pos = abc9_script.find("dretime;"); pos != std::string::npos; pos = abc9_script.find("dretime;", pos+1))
-	//		abc9_script = abc9_script.substr(0, pos) + "dretime; retime -o {D};" + abc9_script.substr(pos+8);
-
 	for (size_t pos = abc9_script.find("{D}"); pos != std::string::npos; pos = abc9_script.find("{D}", pos))
 		abc9_script = abc9_script.substr(0, pos) + delay_target + abc9_script.substr(pos+3);
 
@@ -304,7 +255,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		for (size_t pos = abc9_script.find("&mfs"); pos != std::string::npos; pos = abc9_script.find("&mfs", pos))
 			abc9_script = abc9_script.erase(pos, strlen("&mfs"));
 
-	abc9_script += stringf("; &write %s/output.aig", tempdir_name.c_str());
+	abc9_script += stringf("; &write -n %s/output.aig", tempdir_name.c_str());
 	abc9_script = add_echos_to_abc9_cmd(abc9_script);
 
 	for (size_t i = 0; i+1 < abc9_script.size(); i++)
@@ -315,22 +266,17 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 	fprintf(f, "%s\n", abc9_script.c_str());
 	fclose(f);
 
-	if (dff_mode || !clk_str.empty())
-	{
-		if (clk_sig.size() == 0)
-			log("No%s clock domain found. Not extracting any FF cells.\n", clk_str.empty() ? "" : " matching");
-		else {
-			log("Found%s %s clock domain: %s", clk_str.empty() ? "" : " matching", clk_polarity ? "posedge" : "negedge", log_signal(clk_sig));
-			if (en_sig.size() != 0)
-				log(", enabled by %s%s", en_polarity ? "" : "!", log_signal(en_sig));
-			log("\n");
-		}
-	}
-
 	log_push();
 
-	//if (count_output)
+	// FIXME:
-	{
+	/*int count_outputs = design->scratchpad_get_int("write_xaiger.num_outputs");
+	log("Extracted %d AND gates and %d wires to a netlist network with %d inputs and %d outputs.\n",
+			design->scratchpad_get_int("write_xaiger.num_ands"),
+			design->scratchpad_get_int("write_xaiger.num_wires"),
+			design->scratchpad_get_int("write_xaiger.num_inputs"),
+			count_outputs);
+
+	if (count_outputs > 0)*/ {
 		std::string buffer;
 		std::ifstream ifs;
 #if 0
@@ -342,14 +288,14 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		log_assert(!design->module(ID($__abc9__)));
 		{
 			AigerReader reader(design, ifs, ID($__abc9__), "" /* clk_name */, buffer.c_str() /* map_filename */, true /* wideports */);
-			reader.parse_xaiger();
+			reader.parse_xaiger(box_lookup);
 		}
 		ifs.close();
-		Pass::call(design, stringf("write_verilog -noexpr -norename"));
+		Pass::call_on_module(design, design->module(ID($__abc9__)), stringf("write_verilog -noexpr -norename -selected"));
 		design->remove(design->module(ID($__abc9__)));
 #endif
 
-		log_header(design, "Executing ABC9_MAP.\n");
+		log_header(design, "Executing ABC9.\n");
 
 		if (!lut_costs.empty()) {
 			buffer = stringf("%s/lutdefs.txt", tempdir_name.c_str());
@@ -398,7 +344,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		ifs.close();
 
 #if 0
-		Pass::call(design, stringf("write_verilog -noexpr -norename"));
+		Pass::call_on_module(design, design->module(ID($__abc9__)), stringf("write_verilog -noexpr -norename -selected"));
 #endif
 
 		log_header(design, "Re-integrating ABC9 results.\n");
@@ -406,33 +352,16 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		if (mapped_mod == NULL)
 			log_error("ABC output file does not contain a module `$__abc9__'.\n");
 
-		pool<RTLIL::SigBit> output_bits;
 		for (auto &it : mapped_mod->wires_) {
 			RTLIL::Wire *w = it.second;
 			RTLIL::Wire *remap_wire = module->addWire(remap_name(w->name), GetSize(w));
 			if (markgroups) remap_wire->attributes[ID(abcgroup)] = map_autoidx;
-			if (w->port_output) {
-				RTLIL::Wire *wire = module->wire(w->name);
-				log_assert(wire);
-				for (int i = 0; i < GetSize(w); i++)
-					output_bits.insert({wire, i});
-			}
-		}
-
-		for (auto &it : module->connections_) {
-			auto &signal = it.first;
-			auto bits = signal.bits();
-			for (auto &b : bits)
-				if (output_bits.count(b))
-					b = module->addWire(NEW_ID);
-			signal = std::move(bits);
 		}
 
 		dict<IdString, bool> abc9_box;
 		vector<RTLIL::Cell*> boxes;
-		for (const auto &it : module->cells_) {
+		for (auto cell : module->selected_cells()) {
-			auto cell = it.second;
+			if (cell->type.in(ID($_AND_), ID($_NOT_), ID($__ABC9_FF_))) {
-			if (cell->type.in(ID($_AND_), ID($_NOT_))) {
 				module->remove(cell);
 				continue;
 			}
@@ -441,8 +370,16 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 				RTLIL::Module* box_module = design->module(cell->type);
 				jt = abc9_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count(ID(abc9_box_id)))).first;
 			}
-			if (jt->second)
+			if (jt->second) {
-				boxes.emplace_back(cell);
+				auto kt = cell->attributes.find("\\abc9_keep");
+				bool abc9_keep = false;
+				if (kt != cell->attributes.end()) {
+					abc9_keep = kt->second.as_bool();
+					cell->attributes.erase(kt);
+				}
+				if (!abc9_keep)
+					boxes.emplace_back(cell);
+			}
 		}
 
 		dict<SigBit, pool<IdString>> bit_drivers, bit_users;
@@ -451,19 +388,19 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		dict<SigBit, std::vector<RTLIL::Cell*>> bit2sinks;
 
 		std::map<IdString, int> cell_stats;
-		for (auto c : mapped_mod->cells())
+		for (auto mapped_cell : mapped_mod->cells())
 		{
-			toposort.node(c->name);
+			toposort.node(mapped_cell->name);
 
 			RTLIL::Cell *cell = nullptr;
-			if (c->type == ID($_NOT_)) {
+			if (mapped_cell->type == ID($_NOT_)) {
-				RTLIL::SigBit a_bit = c->getPort(ID::A);
+				RTLIL::SigBit a_bit = mapped_cell->getPort(ID::A);
-				RTLIL::SigBit y_bit = c->getPort(ID::Y);
+				RTLIL::SigBit y_bit = mapped_cell->getPort(ID::Y);
-				bit_users[a_bit].insert(c->name);
+				bit_users[a_bit].insert(mapped_cell->name);
-				bit_drivers[y_bit].insert(c->name);
+				bit_drivers[y_bit].insert(mapped_cell->name);
 
 				if (!a_bit.wire) {
-					c->setPort(ID::Y, module->addWire(NEW_ID));
+					mapped_cell->setPort(ID::Y, module->addWire(NEW_ID));
 					RTLIL::Wire *wire = module->wire(remap_name(y_bit.wire->name));
 					log_assert(wire);
 					module->connect(RTLIL::SigBit(wire, y_bit.offset), State::S1);
@@ -487,7 +424,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 					if (!driver_lut) {
 						// If a driver couldn't be found (could be from PI or box CI)
 						// then implement using a LUT
-						cell = module->addLut(remap_name(stringf("%s$lut", c->name.c_str())),
+						cell = module->addLut(remap_name(stringf("%s$lut", mapped_cell->name.c_str())),
 								RTLIL::SigBit(module->wires_.at(remap_name(a_bit.wire->name)), a_bit.offset),
 								RTLIL::SigBit(module->wires_.at(remap_name(y_bit.wire->name)), y_bit.offset),
 								RTLIL::Const::from_string("01"));
@@ -495,7 +432,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 						cell_stats[ID($lut)]++;
 					}
 					else
-						not2drivers[c] = driver_lut;
+						not2drivers[mapped_cell] = driver_lut;
 					continue;
 				}
 				else
@@ -503,24 +440,26 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 				if (cell && markgroups) cell->attributes[ID(abcgroup)] = map_autoidx;
 				continue;
 			}
-			cell_stats[c->type]++;
+			cell_stats[mapped_cell->type]++;
 
 			RTLIL::Cell *existing_cell = nullptr;
-			if (c->type == ID($lut)) {
+			if (mapped_cell->type.in(ID($lut), ID($__ABC9_FF_))) {
-				if (GetSize(c->getPort(ID::A)) == 1 && c->getParam(ID(LUT)) == RTLIL::Const::from_string("01")) {
+				if (mapped_cell->type == ID($lut) &&
-					SigSpec my_a = module->wires_.at(remap_name(c->getPort(ID::A).as_wire()->name));
+						GetSize(mapped_cell->getPort(ID::A)) == 1 &&
-					SigSpec my_y = module->wires_.at(remap_name(c->getPort(ID::Y).as_wire()->name));
+						mapped_cell->getParam(ID(LUT)) == RTLIL::Const::from_string("01")) {
+					SigSpec my_a = module->wires_.at(remap_name(mapped_cell->getPort(ID::A).as_wire()->name));
+					SigSpec my_y = module->wires_.at(remap_name(mapped_cell->getPort(ID::Y).as_wire()->name));
 					module->connect(my_y, my_a);
-					if (markgroups) c->attributes[ID(abcgroup)] = map_autoidx;
+					if (markgroups) mapped_cell->attributes[ID(abcgroup)] = map_autoidx;
 					log_abort();
 					continue;
 				}
-				cell = module->addCell(remap_name(c->name), c->type);
+				cell = module->addCell(remap_name(mapped_cell->name), mapped_cell->type);
 			}
 			else {
-				existing_cell = module->cell(c->name);
+				existing_cell = module->cell(mapped_cell->name);
 				log_assert(existing_cell);
-				cell = module->addCell(remap_name(c->name), c->type);
+				cell = module->addCell(remap_name(mapped_cell->name), mapped_cell->type);
 			}
 
 			if (markgroups) cell->attributes[ID(abcgroup)] = map_autoidx;
@@ -529,10 +468,13 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 				cell->attributes = existing_cell->attributes;
 			}
 			else {
-				cell->parameters = c->parameters;
+				cell->parameters = mapped_cell->parameters;
-				cell->attributes = c->attributes;
+				cell->attributes = mapped_cell->attributes;
 			}
-			for (auto &conn : c->connections()) {
+
+			RTLIL::Module* box_module = design->module(mapped_cell->type);
+			auto abc9_flop = box_module && box_module->attributes.count("\\abc9_flop");
+			for (auto &conn : mapped_cell->connections()) {
 				RTLIL::SigSpec newsig;
 				for (auto c : conn.second.chunks()) {
 					if (c.width == 0)
@@ -544,15 +486,17 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 				}
 				cell->setPort(conn.first, newsig);
 
-				if (cell->input(conn.first)) {
+				if (!abc9_flop) {
-					for (auto i : newsig)
+					if (cell->input(conn.first)) {
-						bit2sinks[i].push_back(cell);
+						for (auto i : newsig)
-					for (auto i : conn.second)
+							bit2sinks[i].push_back(cell);
-						bit_users[i].insert(c->name);
+						for (auto i : conn.second)
+							bit_users[i].insert(mapped_cell->name);
+					}
+					if (cell->output(conn.first))
+						for (auto i : conn.second)
+							bit_drivers[i].insert(mapped_cell->name);
 				}
-				if (cell->output(conn.first))
-					for (auto i : conn.second)
-						bit_drivers[i].insert(c->name);
 			}
 		}
 
@@ -787,10 +731,6 @@ struct Abc9TechmapPass : public Pass {
 //		log("    -keepff\n");
 //		log("        set the \"keep\" attribute on flip-flop output wires. (and thus preserve\n");
 //		log("        them, for example for equivalence checking.)\n");
-//		log("\n");
-//		log("    -nocleanup\n");
-//		log("        when this option is used, the temporary files created by this pass\n");
-//		log("        are not removed. this is useful for debugging.\n");
 //		log("\n");
 		log("    -showtmp\n");
 		log("        print the temp dir name in log. usually this is suppressed so that the\n");
@@ -822,8 +762,6 @@ struct Abc9TechmapPass : public Pass {
 		log_header(design, "Executing ABC9_MAP pass (technology mapping using ABC9).\n");
 		log_push();
 
-		assign_map.clear();
-
 #ifdef ABCEXTERNAL
 		std::string exe_file = ABCEXTERNAL;
 #else
@@ -832,7 +770,7 @@ struct Abc9TechmapPass : public Pass {
 		std::string script_file, clk_str, box_file, lut_file;
 		std::string delay_target, lutin_shared = "-S 1", wire_delay;
 		std::string tempdir_name;
-		bool fast_mode = false, dff_mode = false, keepff = false /*, cleanup = true*/;
+		bool fast_mode = false;
 		bool show_tempdir = false;
 		bool nomfs = false;
 		vector<int> lut_costs;
@@ -923,23 +861,6 @@ struct Abc9TechmapPass : public Pass {
 				fast_mode = true;
 				continue;
 			}
-			//if (arg == "-dff") {
-			//	dff_mode = true;
-			//	continue;
-			//}
-			//if (arg == "-clk" && argidx+1 < args.size()) {
-			//	clk_str = args[++argidx];
-			//	dff_mode = true;
-			//	continue;
-			//}
-			//if (arg == "-keepff") {
-			//	keepff = true;
-			//	continue;
-			//}
-			//if (arg == "-nocleanup") {
-			//	cleanup = false;
-			//	continue;
-			//}
 			if (arg == "-showtmp") {
 				show_tempdir = true;
 				continue;
@@ -1040,174 +961,60 @@ struct Abc9TechmapPass : public Pass {
 			}
 		}
 
-		for (auto mod : design->selected_modules())
+		SigMap assign_map;
+		CellTypes ct(design);
+		for (auto module : design->selected_modules())
 		{
-			if (mod->attributes.count(ID(abc9_box_id)))
+			if (module->attributes.count(ID(abc9_box_id)))
 				continue;
 
-			if (mod->processes.size() > 0) {
+			if (module->processes.size() > 0) {
-				log("Skipping module %s as it contains processes.\n", log_id(mod));
+				log("Skipping module %s as it contains processes.\n", log_id(module));
 				continue;
 			}
 
-			assign_map.set(mod);
+			assign_map.set(module);
 
-			if (!dff_mode || !clk_str.empty()) {
+			typedef SigSpec clkdomain_t;
-				abc9_module(design, mod, script_file, exe_file, /*cleanup,*/ lut_costs, dff_mode, clk_str, keepff,
+			dict<clkdomain_t, int> clk_to_mergeability;
-						delay_target, lutin_shared, fast_mode, show_tempdir,
-						box_file, lut_file, wire_delay, box_lookup, nomfs, tempdir_name);
-				continue;
-			}
 
-			CellTypes ct(design);
+			const std::vector<RTLIL::Cell*> all_cells = module->selected_cells();
 
-			std::vector<RTLIL::Cell*> all_cells = mod->selected_cells();
+			for (auto cell : all_cells) {
-			std::set<RTLIL::Cell*> unassigned_cells(all_cells.begin(), all_cells.end());
+				auto inst_module = design->module(cell->type);
-
+				if (!inst_module || !inst_module->attributes.count("\\abc9_flop")
-			std::set<RTLIL::Cell*> expand_queue, next_expand_queue;
+						|| cell->get_bool_attribute("\\abc9_keep"))
-			std::set<RTLIL::Cell*> expand_queue_up, next_expand_queue_up;
-			std::set<RTLIL::Cell*> expand_queue_down, next_expand_queue_down;
-
-			typedef tuple<bool, RTLIL::SigSpec, bool, RTLIL::SigSpec> clkdomain_t;
-			std::map<clkdomain_t, std::vector<RTLIL::Cell*>> assigned_cells;
-			std::map<RTLIL::Cell*, clkdomain_t> assigned_cells_reverse;
-
-			std::map<RTLIL::Cell*, std::set<RTLIL::SigBit>> cell_to_bit, cell_to_bit_up, cell_to_bit_down;
-			std::map<RTLIL::SigBit, std::set<RTLIL::Cell*>> bit_to_cell, bit_to_cell_up, bit_to_cell_down;
-
-			for (auto cell : all_cells)
-			{
-				clkdomain_t key;
-
-				for (auto &conn : cell->connections())
-				for (auto bit : conn.second) {
-					bit = assign_map(bit);
-					if (bit.wire != nullptr) {
-						cell_to_bit[cell].insert(bit);
-						bit_to_cell[bit].insert(cell);
-						if (ct.cell_input(cell->type, conn.first)) {
-							cell_to_bit_up[cell].insert(bit);
-							bit_to_cell_down[bit].insert(cell);
-						}
-						if (ct.cell_output(cell->type, conn.first)) {
-							cell_to_bit_down[cell].insert(bit);
-							bit_to_cell_up[bit].insert(cell);
-						}
-					}
-				}
-
-				if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_)))
-				{
-					key = clkdomain_t(cell->type == ID($_DFF_P_), assign_map(cell->getPort(ID(C))), true, RTLIL::SigSpec());
-				}
-				else
-				if (cell->type.in(ID($_DFFE_NN_), ID($_DFFE_NP_), ID($_DFFE_PN_), ID($_DFFE_PP_)))
-				{
-					bool this_clk_pol = cell->type.in(ID($_DFFE_PN_), ID($_DFFE_PP_));
-					bool this_en_pol = cell->type.in(ID($_DFFE_NP_), ID($_DFFE_PP_));
-					key = clkdomain_t(this_clk_pol, assign_map(cell->getPort(ID(C))), this_en_pol, assign_map(cell->getPort(ID(E))));
-				}
-				else
 					continue;
 
-				unassigned_cells.erase(cell);
+				Wire *abc9_clock_wire = module->wire(stringf("%s.$abc9_clock", cell->name.c_str()));
-				expand_queue.insert(cell);
+				if (abc9_clock_wire == NULL)
-				expand_queue_up.insert(cell);
+					log_error("'%s$abc9_clock' is not a wire present in module '%s'.\n", cell->name.c_str(), log_id(module));
-				expand_queue_down.insert(cell);
+				SigSpec abc9_clock = assign_map(abc9_clock_wire);
 
-				assigned_cells[key].push_back(cell);
+				clkdomain_t key(abc9_clock);
-				assigned_cells_reverse[cell] = key;
+
+				auto r = clk_to_mergeability.insert(std::make_pair(abc9_clock, clk_to_mergeability.size() + 1));
+				auto r2 YS_ATTRIBUTE(unused) = cell->attributes.insert(std::make_pair(ID(abc9_mergeability), r.first->second));
+				log_assert(r2.second);
+
+				Wire *abc9_init_wire = module->wire(stringf("%s.$abc9_init", cell->name.c_str()));
+				if (abc9_init_wire == NULL)
+				    log_error("'%s.$abc9_init' is not a wire present in module '%s'.\n", cell->name.c_str(), log_id(module));
+				log_assert(GetSize(abc9_init_wire) == 1);
+				SigSpec abc9_init = assign_map(abc9_init_wire);
+				if (!abc9_init.is_fully_const())
+				    log_error("'%s.$abc9_init' is not a constant wire present in module '%s'.\n", cell->name.c_str(), log_id(module));
+				r2 = cell->attributes.insert(std::make_pair(ID(abc9_init), abc9_init.as_const()));
+				log_assert(r2.second);
 			}
 
-			while (!expand_queue_up.empty() || !expand_queue_down.empty())
+			design->selected_active_module = module->name.str();
-			{
+			abc9_module(design, module, script_file, exe_file, lut_costs,
-				if (!expand_queue_up.empty())
+					delay_target, lutin_shared, fast_mode, all_cells, show_tempdir,
-				{
+					box_file, lut_file, wire_delay, box_lookup, nomfs, tempdir_name);
-					RTLIL::Cell *cell = *expand_queue_up.begin();
+			design->selected_active_module.clear();
-					clkdomain_t key = assigned_cells_reverse.at(cell);
-					expand_queue_up.erase(cell);
-
-					for (auto bit : cell_to_bit_up[cell])
-					for (auto c : bit_to_cell_up[bit])
-						if (unassigned_cells.count(c)) {
-							unassigned_cells.erase(c);
-							next_expand_queue_up.insert(c);
-							assigned_cells[key].push_back(c);
-							assigned_cells_reverse[c] = key;
-							expand_queue.insert(c);
-						}
-				}
-
-				if (!expand_queue_down.empty())
-				{
-					RTLIL::Cell *cell = *expand_queue_down.begin();
-					clkdomain_t key = assigned_cells_reverse.at(cell);
-					expand_queue_down.erase(cell);
-
-					for (auto bit : cell_to_bit_down[cell])
-					for (auto c : bit_to_cell_down[bit])
-						if (unassigned_cells.count(c)) {
-							unassigned_cells.erase(c);
-							next_expand_queue_up.insert(c);
-							assigned_cells[key].push_back(c);
-							assigned_cells_reverse[c] = key;
-							expand_queue.insert(c);
-						}
-				}
-
-				if (expand_queue_up.empty() && expand_queue_down.empty()) {
-					expand_queue_up.swap(next_expand_queue_up);
-					expand_queue_down.swap(next_expand_queue_down);
-				}
-			}
-
-			while (!expand_queue.empty())
-			{
-				RTLIL::Cell *cell = *expand_queue.begin();
-				clkdomain_t key = assigned_cells_reverse.at(cell);
-				expand_queue.erase(cell);
-
-				for (auto bit : cell_to_bit.at(cell)) {
-					for (auto c : bit_to_cell[bit])
-						if (unassigned_cells.count(c)) {
-							unassigned_cells.erase(c);
-							next_expand_queue.insert(c);
-							assigned_cells[key].push_back(c);
-							assigned_cells_reverse[c] = key;
-						}
-					bit_to_cell[bit].clear();
-				}
-
-				if (expand_queue.empty())
-					expand_queue.swap(next_expand_queue);
-			}
-
-			clkdomain_t key(true, RTLIL::SigSpec(), true, RTLIL::SigSpec());
-			for (auto cell : unassigned_cells) {
-				assigned_cells[key].push_back(cell);
-				assigned_cells_reverse[cell] = key;
-			}
-
-			log_header(design, "Summary of detected clock domains:\n");
-			for (auto &it : assigned_cells)
-				log("  %d cells in clk=%s%s, en=%s%s\n", GetSize(it.second),
-						std::get<0>(it.first) ? "" : "!", log_signal(std::get<1>(it.first)),
-						std::get<2>(it.first) ? "" : "!", log_signal(std::get<3>(it.first)));
-
-			for (auto &it : assigned_cells) {
-				clk_polarity = std::get<0>(it.first);
-				clk_sig = assign_map(std::get<1>(it.first));
-				en_polarity = std::get<2>(it.first);
-				en_sig = assign_map(std::get<3>(it.first));
-				abc9_module(design, mod, script_file, exe_file, /*cleanup,*/ lut_costs, !clk_sig.empty(), "$",
-						keepff, delay_target, lutin_shared, fast_mode, show_tempdir,
-						box_file, lut_file, wire_delay, box_lookup, nomfs, tempdir_name);
-				assign_map.set(mod);
-			}
 		}
 
-		assign_map.clear();
-
 		log_pop();
 	}
 } Abc9TechmapPass;

techlibs/xilinx/abc9_map.v

@@ -18,7 +18,449 @@
  *
  */
 
-// ============================================================================
+// The following techmapping rules are intended to be run (with -max_iter 1)
+//   before invoking the `abc9` pass in order to transform the design into
+//   a format that it understands.
+//
+// For example, (complex) flip-flops are expected to be described as an
+//   combinatorial box (containing all control logic such as clock enable
+//   or synchronous resets) followed by a basic D-Q flop.
+// Yosys will automatically analyse the simulation model (described in
+//   cells_sim.v) and detach any $_DFF_P_ or $_DFF_N_ cells present in
+//   order to extract the combinatorial control logic left behind.
+//   Specifically, a simulation model similar to the one below:
+//
+//                ++===================================++
+//                ||                        Sim model  ||
+//                ||      /\/\/\/\                     ||
+//            D -->>-----<        >     +------+       ||
+//            R -->>-----<  Comb. >     |$_DFF_|       ||
+//           CE -->>-----<  logic >-----| [NP]_|---+---->>-- Q
+//                ||  +--<        >     +------+   |   ||
+//                ||  |   \/\/\/\/                 |   ||
+//                ||  |                            |   ||
+//                ||  +----------------------------+   ||
+//                ||                                   ||
+//                ++===================================++
+//
+//   is transformed into:
+//
+//                ++==================++
+//                ||         Comb box ||
+//                ||                  ||
+//                ||      /\/\/\/\    ||
+//           D  -->>-----<        >   ||
+//           R  -->>-----<  Comb. >   ||        +----------+
+//          CE  -->>-----<  logic >--->>-- $Q --|$__ABC_FF_|--+-->> Q
+// $abc9_currQ +-->>-----<        >   ||        +----------+  |
+//             |  ||      \/\/\/\/    ||                      |
+//             |  ||                  ||                      |
+//             |  ++==================++                      |
+//             |                                              |
+//             +----------------------------------------------+
+//
+// The purpose of the following FD* rules are to wrap the flop with:
+// (a) a special $__ABC9_FF_ in front of the FD*'s output, indicating to abc9
+//     the connectivity of its basic D-Q flop
+// (b) an optional $__ABC9_ASYNC_ cell in front of $__ABC_FF_'s output to
+//     capture asynchronous behaviour
+// (c) a special _TECHMAP_REPLACE_.$abc9_clock wire to capture its clock
+//     domain and polarity (used when partitioning the module so that `abc9' only
+//     performs sequential synthesis (with reachability analysis) correctly on
+//     one domain at a time) and also used to infer the optional delay target
+//     from the (* abc9_clock_period = %d *) attribute attached to any wire
+//     within
+// (d) a special _TECHMAP_REPLACE_.$abc9_init wire to encode the flop's initial
+//     state
+// (e) a special _TECHMAP_REPLACE_.$abc9_currQ wire that will be used for feedback
+//     into the (combinatorial) FD* cell to facilitate clock-enable behaviour
+//
+// In order to perform sequential synthesis, `abc9' also requires that
+// the initial value of all flops be zero.
+
+module FDRE (output Q, input C, CE, D, R);
+  parameter [0:0] INIT = 1'b0;
+  parameter [0:0] IS_C_INVERTED = 1'b0;
+  parameter [0:0] IS_D_INVERTED = 1'b0;
+  parameter [0:0] IS_R_INVERTED = 1'b0;
+`ifdef DFF_MODE
+  wire QQ, $Q;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDSE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_S_INVERTED(IS_R_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .S(R)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDRE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_R_INVERTED(IS_R_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .R(R)
+    );
+  end
+  endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, IS_C_INVERTED};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = QQ;
+`else
+  (* abc9_keep *)
+  FDRE #(
+    .INIT(INIT),
+    .IS_C_INVERTED(IS_C_INVERTED),
+    .IS_D_INVERTED(IS_D_INVERTED),
+    .IS_R_INVERTED(IS_R_INVERTED)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .R(R)
+  );
+`endif
+endmodule
+module FDRE_1 (output Q, input C, CE, D, R);
+  parameter [0:0] INIT = 1'b0;
+`ifdef DFF_MODE
+  wire QQ, $Q;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDSE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .S(R)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDRE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .R(R)
+    );
+  end
+  endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = QQ;
+`else
+  (* abc9_keep *)
+  FDRE_1 #(
+    .INIT(INIT)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .R(R)
+  );
+`endif
+endmodule
+
+module FDCE (output Q, input C, CE, D, CLR);
+  parameter [0:0] INIT = 1'b0;
+  parameter [0:0] IS_C_INVERTED = 1'b0;
+  parameter [0:0] IS_D_INVERTED = 1'b0;
+  parameter [0:0] IS_CLR_INVERTED = 1'b0;
+`ifdef DFF_MODE
+  wire QQ, $Q, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDPE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_PRE_INVERTED(IS_CLR_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .PRE(CLR)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC1 below
+    );
+    // Since this is an async flop, async behaviour is dealt with here
+    $__ABC9_ASYNC0 abc_async (.A($abc9_currQ), .S(CLR ^ IS_CLR_INVERTED), .Y(QQ));
+  end
+  else begin
+    assign Q = QQ;
+    FDCE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_CLR_INVERTED(IS_CLR_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .CLR(CLR)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC0 below
+    );
+    // Since this is an async flop, async behaviour is dealt with here
+    $__ABC9_ASYNC1 abc_async (.A($abc9_currQ), .S(CLR ^ IS_CLR_INVERTED), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q($abc9_currQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, IS_C_INVERTED};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = $abc9_currQ;
+`else
+  (* abc9_keep *)
+  FDCE #(
+    .INIT(INIT),
+    .IS_C_INVERTED(IS_C_INVERTED),
+    .IS_D_INVERTED(IS_D_INVERTED),
+    .IS_CLR_INVERTED(IS_CLR_INVERTED)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .CLR(CLR)
+  );
+`endif
+endmodule
+module FDCE_1 (output Q, input C, CE, D, CLR);
+  parameter [0:0] INIT = 1'b0;
+`ifdef DFF_MODE
+  wire QQ, $Q, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDPE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .PRE(CLR)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC1 below
+    );
+    $__ABC9_ASYNC1 abc_async (.A($abc9_currQ), .S(CLR), .Y(QQ));
+  end
+  else begin
+    assign Q = QQ;
+    FDCE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .CLR(CLR)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC0 below
+    );
+    $__ABC9_ASYNC0 abc_async (.A($abc9_currQ), .S(CLR), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q($abc9_currQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = $abc9_currQ;
+`else
+  (* abc9_keep *)
+  FDCE_1 #(
+    .INIT(INIT)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .CLR(CLR)
+  );
+`endif
+endmodule
+
+module FDPE (output Q, input C, CE, D, PRE);
+  parameter [0:0] INIT = 1'b1;
+  parameter [0:0] IS_C_INVERTED = 1'b0;
+  parameter [0:0] IS_D_INVERTED = 1'b0;
+  parameter [0:0] IS_PRE_INVERTED = 1'b0;
+`ifdef DFF_MODE
+  wire QQ, $Q, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDCE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_CLR_INVERTED(IS_PRE_INVERTED),
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .CLR(PRE)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC0 below
+    );
+    $__ABC9_ASYNC0 abc_async (.A($abc9_currQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
+  end
+  else begin
+    assign Q = QQ;
+    FDPE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_PRE_INVERTED(IS_PRE_INVERTED),
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .PRE(PRE)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC1 below
+    );
+    $__ABC9_ASYNC1 abc_async (.A($abc9_currQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q($abc9_currQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, IS_C_INVERTED};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = $abc9_currQ;
+`else
+  (* abc9_keep *)
+  FDPE #(
+    .INIT(INIT),
+    .IS_C_INVERTED(IS_C_INVERTED),
+    .IS_D_INVERTED(IS_D_INVERTED),
+    .IS_PRE_INVERTED(IS_PRE_INVERTED),
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .PRE(PRE)
+  );
+`endif
+endmodule
+module FDPE_1 (output Q, input C, CE, D, PRE);
+  parameter [0:0] INIT = 1'b1;
+`ifdef DFF_MODE
+  wire QQ, $Q, $abc9_currQ;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDCE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .CLR(PRE)
+                                            // ^^^ Note that async
+                                            //     control is not directly
+                                            //     supported by abc9 but its
+                                            //     behaviour is captured by
+                                            //     $__ABC9_ASYNC0 below
+    );
+    $__ABC9_ASYNC0 abc_async (.A($abc9_currQ), .S(PRE), .Y(QQ));
+  end
+  else begin
+    assign Q = QQ;
+    FDPE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .PRE(PRE)
+                                           // ^^^ Note that async
+                                           //     control is not directly
+                                           //     supported by abc9 but its
+                                           //     behaviour is captured by
+                                           //     $__ABC9_ASYNC1 below
+    );
+    $__ABC9_ASYNC1 abc_async (.A($abc9_currQ), .S(PRE), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q($abc9_currQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = $abc9_currQ;
+`else
+  (* abc9_keep *)
+  FDPE_1 #(
+    .INIT(INIT)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .PRE(PRE)
+  );
+`endif
+endmodule
+
+module FDSE (output Q, input C, CE, D, S);
+  parameter [0:0] INIT = 1'b1;
+  parameter [0:0] IS_C_INVERTED = 1'b0;
+  parameter [0:0] IS_D_INVERTED = 1'b0;
+  parameter [0:0] IS_S_INVERTED = 1'b0;
+`ifdef DFF_MODE
+  wire QQ, $Q;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDRE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_R_INVERTED(IS_S_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .R(S)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDSE #(
+      .INIT(1'b0),
+      .IS_C_INVERTED(IS_C_INVERTED),
+      .IS_D_INVERTED(IS_D_INVERTED),
+      .IS_S_INVERTED(IS_S_INVERTED)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .S(S)
+    );
+  end endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, IS_C_INVERTED};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = QQ;
+`else
+  (* abc9_keep *)
+  FDSE #(
+    .INIT(INIT),
+    .IS_C_INVERTED(IS_C_INVERTED),
+    .IS_D_INVERTED(IS_D_INVERTED),
+    .IS_S_INVERTED(IS_S_INVERTED)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .S(S)
+  );
+`endif
+endmodule
+module FDSE_1 (output Q, input C, CE, D, S);
+  parameter [0:0] INIT = 1'b1;
+`ifdef DFF_MODE
+  wire QQ, $Q;
+  generate if (INIT == 1'b1) begin
+    assign Q = ~QQ;
+    FDRE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(~D), .Q($Q), .C(C), .CE(CE), .R(S)
+    );
+  end
+  else begin
+    assign Q = QQ;
+    FDSE_1 #(
+      .INIT(1'b0)
+    ) _TECHMAP_REPLACE_ (
+      .D(D), .Q($Q), .C(C), .CE(CE), .S(S)
+    );
+  end endgenerate
+  $__ABC9_FF_ abc_dff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] _TECHMAP_REPLACE_.$abc9_clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.$abc9_currQ = QQ;
+`else
+  (* abc9_keep *)
+  FDSE_1 #(
+    .INIT(INIT)
+  ) _TECHMAP_REPLACE_ (
+    .D(D), .Q(Q), .C(C), .CE(CE), .S(S)
+  );
+`endif
+endmodule
 
 module RAM32X1D (
   output DPO, SPO,
@@ -30,17 +472,17 @@ module RAM32X1D (
 );
   parameter INIT = 32'h0;
   parameter IS_WCLK_INVERTED = 1'b0;
-  wire \$DPO , \$SPO ;
+  wire $DPO, $SPO;
   RAM32X1D #(
     .INIT(INIT), .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DPO(\$DPO ), .SPO(\$SPO ),
+    .DPO($DPO), .SPO($SPO),
     .D(D), .WCLK(WCLK), .WE(WE),
     .A0(A0), .A1(A1), .A2(A2), .A3(A3), .A4(A4),
     .DPRA0(DPRA0), .DPRA1(DPRA1), .DPRA2(DPRA2), .DPRA3(DPRA3), .DPRA4(DPRA4)
   );
-  \$__ABC9_LUT6 spo (.A(\$SPO ), .S({1'b1, A4, A3, A2, A1, A0}), .Y(SPO));
+  $__ABC9_LUT6 spo (.A($SPO), .S({1'b1, A4, A3, A2, A1, A0}), .Y(SPO));
-  \$__ABC9_LUT6 dpo (.A(\$DPO ), .S({1'b1, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
+  $__ABC9_LUT6 dpo (.A($DPO), .S({1'b1, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
 endmodule
 
 module RAM64X1D (
@@ -53,17 +495,17 @@ module RAM64X1D (
 );
   parameter INIT = 64'h0;
   parameter IS_WCLK_INVERTED = 1'b0;
-  wire \$DPO , \$SPO ;
+  wire $DPO, $SPO;
   RAM64X1D #(
     .INIT(INIT), .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DPO(\$DPO ), .SPO(\$SPO ),
+    .DPO($DPO), .SPO($SPO),
     .D(D), .WCLK(WCLK), .WE(WE),
     .A0(A0), .A1(A1), .A2(A2), .A3(A3), .A4(A4), .A5(A5),
     .DPRA0(DPRA0), .DPRA1(DPRA1), .DPRA2(DPRA2), .DPRA3(DPRA3), .DPRA4(DPRA4), .DPRA5(DPRA5)
   );
-  \$__ABC9_LUT6 spo (.A(\$SPO ), .S({A5, A4, A3, A2, A1, A0}), .Y(SPO));
+  $__ABC9_LUT6 spo (.A($SPO), .S({A5, A4, A3, A2, A1, A0}), .Y(SPO));
-  \$__ABC9_LUT6 dpo (.A(\$DPO ), .S({DPRA5, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
+  $__ABC9_LUT6 dpo (.A($DPO), .S({DPRA5, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
 endmodule
 
 module RAM128X1D (
@@ -75,17 +517,17 @@ module RAM128X1D (
 );
   parameter INIT = 128'h0;
   parameter IS_WCLK_INVERTED = 1'b0;
-  wire \$DPO , \$SPO ;
+  wire $DPO, $SPO;
   RAM128X1D #(
     .INIT(INIT), .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DPO(\$DPO ), .SPO(\$SPO ),
+    .DPO($DPO), .SPO($SPO),
     .D(D), .WCLK(WCLK), .WE(WE),
     .A(A),
     .DPRA(DPRA)
   );
-  \$__ABC9_LUT7 spo (.A(\$SPO ), .S(A), .Y(SPO));
+  $__ABC9_LUT7 spo (.A($SPO), .S(A), .Y(SPO));
-  \$__ABC9_LUT7 dpo (.A(\$DPO ), .S(DPRA), .Y(DPO));
+  $__ABC9_LUT7 dpo (.A($DPO), .S(DPRA), .Y(DPO));
 endmodule
 
 module RAM32M (
@@ -109,24 +551,24 @@ module RAM32M (
   parameter [63:0] INIT_C = 64'h0000000000000000;
   parameter [63:0] INIT_D = 64'h0000000000000000;
   parameter [0:0] IS_WCLK_INVERTED = 1'b0;
-  wire [1:0] \$DOA , \$DOB , \$DOC , \$DOD ;
+  wire [1:0] $DOA, $DOB, $DOC, $DOD;
   RAM32M #(
     .INIT_A(INIT_A), .INIT_B(INIT_B), .INIT_C(INIT_C), .INIT_D(INIT_D),
     .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DOA(\$DOA ), .DOB(\$DOB ), .DOC(\$DOC ), .DOD(\$DOD ),
+    .DOA($DOA), .DOB($DOB), .DOC($DOC), .DOD($DOD),
     .WCLK(WCLK), .WE(WE),
     .ADDRA(ADDRA), .ADDRB(ADDRB), .ADDRC(ADDRC), .ADDRD(ADDRD),
     .DIA(DIA), .DIB(DIB), .DIC(DIC), .DID(DID)
   );
-  \$__ABC9_LUT6 doa0 (.A(\$DOA [0]), .S({1'b1, ADDRA}), .Y(DOA[0]));
+  $__ABC9_LUT6 doa0 (.A($DOA[0]), .S({1'b1, ADDRA}), .Y(DOA[0]));
-  \$__ABC9_LUT6 doa1 (.A(\$DOA [1]), .S({1'b1, ADDRA}), .Y(DOA[1]));
+  $__ABC9_LUT6 doa1 (.A($DOA[1]), .S({1'b1, ADDRA}), .Y(DOA[1]));
-  \$__ABC9_LUT6 dob0 (.A(\$DOB [0]), .S({1'b1, ADDRB}), .Y(DOB[0]));
+  $__ABC9_LUT6 dob0 (.A($DOB[0]), .S({1'b1, ADDRB}), .Y(DOB[0]));
-  \$__ABC9_LUT6 dob1 (.A(\$DOB [1]), .S({1'b1, ADDRB}), .Y(DOB[1]));
+  $__ABC9_LUT6 dob1 (.A($DOB[1]), .S({1'b1, ADDRB}), .Y(DOB[1]));
-  \$__ABC9_LUT6 doc0 (.A(\$DOC [0]), .S({1'b1, ADDRC}), .Y(DOC[0]));
+  $__ABC9_LUT6 doc0 (.A($DOC[0]), .S({1'b1, ADDRC}), .Y(DOC[0]));
-  \$__ABC9_LUT6 doc1 (.A(\$DOC [1]), .S({1'b1, ADDRC}), .Y(DOC[1]));
+  $__ABC9_LUT6 doc1 (.A($DOC[1]), .S({1'b1, ADDRC}), .Y(DOC[1]));
-  \$__ABC9_LUT6 dod0 (.A(\$DOD [0]), .S({1'b1, ADDRD}), .Y(DOD[0]));
+  $__ABC9_LUT6 dod0 (.A($DOD[0]), .S({1'b1, ADDRD}), .Y(DOD[0]));
-  \$__ABC9_LUT6 dod1 (.A(\$DOD [1]), .S({1'b1, ADDRD}), .Y(DOD[1]));
+  $__ABC9_LUT6 dod1 (.A($DOD[1]), .S({1'b1, ADDRD}), .Y(DOD[1]));
 endmodule
 
 module RAM64M (
@@ -150,20 +592,20 @@ module RAM64M (
   parameter [63:0] INIT_C = 64'h0000000000000000;
   parameter [63:0] INIT_D = 64'h0000000000000000;
   parameter [0:0] IS_WCLK_INVERTED = 1'b0;
-  wire \$DOA , \$DOB , \$DOC , \$DOD ;
+  wire $DOA, $DOB, $DOC, $DOD;
   RAM64M #(
     .INIT_A(INIT_A), .INIT_B(INIT_B), .INIT_C(INIT_C), .INIT_D(INIT_D),
     .IS_WCLK_INVERTED(IS_WCLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .DOA(\$DOA ), .DOB(\$DOB ), .DOC(\$DOC ), .DOD(\$DOD ),
+    .DOA($DOA), .DOB($DOB), .DOC($DOC), .DOD($DOD),
     .WCLK(WCLK), .WE(WE),
     .ADDRA(ADDRA), .ADDRB(ADDRB), .ADDRC(ADDRC), .ADDRD(ADDRD),
     .DIA(DIA), .DIB(DIB), .DIC(DIC), .DID(DID)
   );
-  \$__ABC9_LUT6 doa (.A(\$DOA ), .S(ADDRA), .Y(DOA));
+  $__ABC9_LUT6 doa (.A($DOA), .S(ADDRA), .Y(DOA));
-  \$__ABC9_LUT6 dob (.A(\$DOB ), .S(ADDRB), .Y(DOB));
+  $__ABC9_LUT6 dob (.A($DOB), .S(ADDRB), .Y(DOB));
-  \$__ABC9_LUT6 doc (.A(\$DOC ), .S(ADDRC), .Y(DOC));
+  $__ABC9_LUT6 doc (.A($DOC), .S(ADDRC), .Y(DOC));
-  \$__ABC9_LUT6 dod (.A(\$DOD ), .S(ADDRD), .Y(DOD));
+  $__ABC9_LUT6 dod (.A($DOD), .S(ADDRD), .Y(DOD));
 endmodule
 
 module SRL16E (
@@ -172,14 +614,14 @@ module SRL16E (
 );
   parameter [15:0] INIT = 16'h0000;
   parameter [0:0] IS_CLK_INVERTED = 1'b0;
-  wire \$Q ;
+  wire $Q;
   SRL16E #(
     .INIT(INIT), .IS_CLK_INVERTED(IS_CLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .Q(\$Q ),
+    .Q($Q),
     .A0(A0), .A1(A1), .A2(A2), .A3(A3), .CE(CE), .CLK(CLK), .D(D)
   );
-  \$__ABC9_LUT6 q (.A(\$Q ), .S({1'b1, A3, A2, A1, A0, 1'b1}), .Y(Q));
+  $__ABC9_LUT6 q (.A($Q), .S({1'b1, A3, A2, A1, A0, 1'b1}), .Y(Q));
 endmodule
 
 module SRLC32E (
@@ -190,14 +632,14 @@ module SRLC32E (
 );
   parameter [31:0] INIT = 32'h00000000;
   parameter [0:0] IS_CLK_INVERTED = 1'b0;
-  wire \$Q ;
+  wire $Q;
   SRLC32E #(
     .INIT(INIT), .IS_CLK_INVERTED(IS_CLK_INVERTED)
   ) _TECHMAP_REPLACE_ (
-    .Q(\$Q ), .Q31(Q31),
+    .Q($Q), .Q31(Q31),
     .A(A), .CE(CE), .CLK(CLK), .D(D)
   );
-  \$__ABC9_LUT6 q (.A(\$Q ), .S({1'b1, A}), .Y(Q));
+  $__ABC9_LUT6 q (.A($Q), .S({1'b1, A}), .Y(Q));
 endmodule
 
 module DSP48E1 (
@@ -386,15 +828,15 @@ __CELL__ #(
         if (AREG == 0 && MREG == 0 && PREG == 0)
             assign iA = A, pA = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(30)) rA (.I(A), .O(iA), .Q(pA));
+            $__ABC9_REG #(.WIDTH(30)) rA (.I(A), .O(iA), .Q(pA));
         if (BREG == 0 && MREG == 0 && PREG == 0)
             assign iB = B, pB = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(18)) rB (.I(B), .O(iB), .Q(pB));
+            $__ABC9_REG #(.WIDTH(18)) rB (.I(B), .O(iB), .Q(pB));
         if (CREG == 0 && PREG == 0)
             assign iC = C, pC = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(48)) rC (.I(C), .O(iC), .Q(pC));
+            $__ABC9_REG #(.WIDTH(48)) rC (.I(C), .O(iC), .Q(pC));
         if (DREG == 0)
             assign iD = D;
         else if (techmap_guard)
@@ -405,27 +847,27 @@ __CELL__ #(
         assign pAD = 1'bx;
     if (PREG == 0) begin
         if (MREG == 1)
-        \$__ABC9_REG rM (.Q(pM));
+        $__ABC9_REG rM (.Q(pM));
         else
         assign pM = 1'bx;
         assign pP = 1'bx;
     end else begin
             assign pM = 1'bx;
-            \$__ABC9_REG rP (.Q(pP));
+            $__ABC9_REG rP (.Q(pP));
         end
 
         if (MREG == 0 && PREG == 0)
             assign mP = oP, mPCOUT = oPCOUT;
         else
             assign mP = 1'bx, mPCOUT = 1'bx;
-        \$__ABC9_DSP48E1_MULT_P_MUX muxP (
+        $__ABC9_DSP48E1_MULT_P_MUX muxP (
             .Aq(pA), .Bq(pB), .Cq(pC), .Dq(pD), .ADq(pAD), .I(oP), .Mq(pM), .P(mP), .Pq(pP), .O(P)
         );
-        \$__ABC9_DSP48E1_MULT_PCOUT_MUX muxPCOUT (
+        $__ABC9_DSP48E1_MULT_PCOUT_MUX muxPCOUT (
             .Aq(pA), .Bq(pB), .Cq(pC), .Dq(pD), .ADq(pAD), .I(oPCOUT), .Mq(pM), .P(mPCOUT), .Pq(pP), .O(PCOUT)
         );
 
-        `DSP48E1_INST(\$__ABC9_DSP48E1_MULT )
+        `DSP48E1_INST($__ABC9_DSP48E1_MULT )
     end
     else if (USE_MULT == "MULTIPLY" && USE_DPORT == "TRUE") begin
         // Disconnect the A-input if MREG is enabled, since
@@ -433,26 +875,26 @@ __CELL__ #(
         if (AREG == 0 && ADREG == 0 && MREG == 0 && PREG == 0)
             assign iA = A, pA = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(30)) rA (.I(A), .O(iA), .Q(pA));
+            $__ABC9_REG #(.WIDTH(30)) rA (.I(A), .O(iA), .Q(pA));
         if (BREG == 0 && MREG == 0 && PREG == 0)
             assign iB = B, pB = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(18)) rB (.I(B), .O(iB), .Q(pB));
+            $__ABC9_REG #(.WIDTH(18)) rB (.I(B), .O(iB), .Q(pB));
         if (CREG == 0 && PREG == 0)
             assign iC = C, pC = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(48)) rC (.I(C), .O(iC), .Q(pC));
+            $__ABC9_REG #(.WIDTH(48)) rC (.I(C), .O(iC), .Q(pC));
         if (DREG == 0 && ADREG == 0)
             assign iD = D, pD = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(25)) rD (.I(D), .O(iD), .Q(pD));
+            $__ABC9_REG #(.WIDTH(25)) rD (.I(D), .O(iD), .Q(pD));
         if (PREG == 0) begin
             if (MREG == 1) begin
                 assign pAD = 1'bx;
-        \$__ABC9_REG rM (.Q(pM));
+        $__ABC9_REG rM (.Q(pM));
             end else begin
                 if (ADREG == 1)
-                    \$__ABC9_REG rAD (.Q(pAD));
+                    $__ABC9_REG rAD (.Q(pAD));
                 else
                     assign pAD = 1'bx;
         assign pM = 1'bx;
@@ -460,21 +902,21 @@ __CELL__ #(
         assign pP = 1'bx;
     end else begin
             assign pAD = 1'bx, pM = 1'bx;
-            \$__ABC9_REG rP (.Q(pP));
+            $__ABC9_REG rP (.Q(pP));
         end
 
         if (MREG == 0 && PREG == 0)
             assign mP = oP, mPCOUT = oPCOUT;
         else
             assign mP = 1'bx, mPCOUT = 1'bx;
-        \$__ABC9_DSP48E1_MULT_DPORT_P_MUX muxP (
+        $__ABC9_DSP48E1_MULT_DPORT_P_MUX muxP (
             .Aq(pA), .Bq(pB), .Cq(pC), .Dq(pD), .ADq(pAD), .I(oP), .Mq(pM), .P(mP), .Pq(pP), .O(P)
         );
-        \$__ABC9_DSP48E1_MULT_DPORT_PCOUT_MUX muxPCOUT (
+        $__ABC9_DSP48E1_MULT_DPORT_PCOUT_MUX muxPCOUT (
             .Aq(pA), .Bq(pB), .Cq(pC), .Dq(pD), .ADq(pAD), .I(oPCOUT), .Mq(pM), .P(mPCOUT), .Pq(pP), .O(PCOUT)
         );
 
-        `DSP48E1_INST(\$__ABC9_DSP48E1_MULT_DPORT )
+        `DSP48E1_INST($__ABC9_DSP48E1_MULT_DPORT )
     end
     else if (USE_MULT == "NONE" && USE_DPORT == "FALSE") begin
         // Disconnect the A-input if MREG is enabled, since
@@ -482,15 +924,15 @@ __CELL__ #(
         if (AREG == 0 && PREG == 0)
             assign iA = A, pA = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(30)) rA (.I(A), .O(iA), .Q(pA));
+            $__ABC9_REG #(.WIDTH(30)) rA (.I(A), .O(iA), .Q(pA));
         if (BREG == 0 && PREG == 0)
             assign iB = B, pB = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(18)) rB (.I(B), .O(iB), .Q(pB));
+            $__ABC9_REG #(.WIDTH(18)) rB (.I(B), .O(iB), .Q(pB));
         if (CREG == 0 && PREG == 0)
             assign iC = C, pC = 1'bx;
         else
-            \$__ABC9_REG #(.WIDTH(48)) rC (.I(C), .O(iC), .Q(pC));
+            $__ABC9_REG #(.WIDTH(48)) rC (.I(C), .O(iC), .Q(pC));
         if (DREG == 1 && techmap_guard)
             $error("Invalid DSP48E1 configuration: DREG enabled but USE_DPORT == \"FALSE\"");
         assign pD = 1'bx;
@@ -501,7 +943,7 @@ __CELL__ #(
             $error("Invalid DSP48E1 configuration: MREG enabled but USE_MULT == \"NONE\"");
         assign pM = 1'bx;
         if (PREG == 1)
-            \$__ABC9_REG rP (.Q(pP));
+            $__ABC9_REG rP (.Q(pP));
         else
             assign pP = 1'bx;
 
@@ -509,14 +951,14 @@ __CELL__ #(
             assign mP = oP, mPCOUT = oPCOUT;
         else
             assign mP = 1'bx, mPCOUT = 1'bx;
-        \$__ABC9_DSP48E1_P_MUX muxP (
+        $__ABC9_DSP48E1_P_MUX muxP (
             .Aq(pA), .Bq(pB), .Cq(pC), .Dq(pD), .ADq(pAD), .I(oP), .Mq(pM), .P(mP), .Pq(pP), .O(P)
         );
-        \$__ABC9_DSP48E1_PCOUT_MUX muxPCOUT (
+        $__ABC9_DSP48E1_PCOUT_MUX muxPCOUT (
             .Aq(pA), .Bq(pB), .Cq(pC), .Dq(pD), .ADq(pAD), .I(oPCOUT), .Mq(pM), .P(mPCOUT), .Pq(pP), .O(PCOUT)
         );
 
-        `DSP48E1_INST(\$__ABC9_DSP48E1 )
+        `DSP48E1_INST($__ABC9_DSP48E1 )
     end
     else
         $error("Invalid DSP48E1 configuration");

techlibs/xilinx/abc9_model.v

@@ -30,7 +30,22 @@ module \$__XILINX_MUXF78 (output O, input I0, I1, I2, I3, S0, S1);
                 : (S0 ? I1 : I0);
 endmodule
 
-// Box to emulate comb/seq behaviour of RAMD{32,64} and SRL{16,32}
+module \$__ABC9_FF_ (input D, output Q);
+endmodule
+
+// Box to emulate async behaviour of FDC*
+(* abc_box_id = 1000 *)
+module \$__ABC9_ASYNC0 (input A, S, output Y);
+  assign Y = S ? 1'b0 : A;
+endmodule
+
+// Box to emulate async behaviour of FDP*
+(* abc_box_id = 1001 *)
+module \$__ABC9_ASYNC1 (input A, S, output Y);
+  assign Y = S ? 1'b0 : A;
+endmodule
+
+// Box to emulate comb/seq behaviour of RAM{32,64} and SRL{16,32}
 //   Necessary since RAMD* and SRL* have both combinatorial (i.e.
 //   same-cycle read operation) and sequential (write operation
 //   is only committed on the next clock edge).
@@ -39,7 +54,7 @@ endmodule
 (* abc9_box_id=2000 *)
 module \$__ABC9_LUT6 (input A, input [5:0] S, output Y);
 endmodule
-// Box to emulate comb/seq behaviour of RAMD128
+// Box to emulate comb/seq behaviour of RAM128
 (* abc9_box_id=2001 *)
 module \$__ABC9_LUT7 (input A, input [6:0] S, output Y);
 endmodule

techlibs/xilinx/abc9_unmap.v

@@ -20,6 +20,15 @@
 
 // ============================================================================
 
+(* techmap_celltype = "$__ABC9_ASYNC0 $__ABC9_ASYNC1" *)
+module \$__ABC9_ASYNC01 (input A, S, output Y);
+  assign Y = A;
+endmodule
+
+module \$__ABC9_FF_ (input D, output Q);
+  assign Q = D;
+endmodule
+
 module \$__ABC9_LUT6 (input A, input [5:0] S, output Y);
   assign Y = A;
 endmodule

techlibs/xilinx/abc9_xc7.box

@@ -41,6 +41,72 @@ CARRY4 4 1 10 8
 592 540 520 356 -   512 548 292 -   228
 580 526 507 398 385 508 528 378 380 114
 
+# Box to emulate async behaviour of FDC*
+# Inputs: A S
+# Outputs: Y
+$__ABC9_ASYNC0 1000 1 2 1
+0 764
+
+# Box to emulate async behaviour of FDP*
+# Inputs: A S
+# Outputs: Y
+$__ABC9_ASYNC1 1001 1 2 1
+0 764
+
+# Max delays from https://github.com/SymbiFlow/prjxray-db/blob/23c8b0851f979f0799318eaca90174413a46b257/artix7/timings/slicel.sdf#L237-L251
+#                 https://github.com/SymbiFlow/prjxray-db/blob/23c8b0851f979f0799318eaca90174413a46b257/artix7/timings/slicel.sdf#L265-L277
+
+# NB: Inputs/Outputs must be ordered alphabetically
+#     (with exception for \$currQ)
+
+# Inputs: C CE D R \$currQ
+# Outputs: Q
+FDRE 1100 1 5 1
+#0 109 -46 404 0
+0 109 0 404 0 # Clamp -46ps Tsu
+
+# Inputs: C CE D R \$currQ
+# Outputs: Q
+FDRE_1 1101 1 5 1
+#0 109 0 -46 404
+0 109 0 0 404 # Clamp -46ps Tsu
+
+# Inputs: C CE CLR D \$currQ
+# Outputs: Q
+FDCE 1102 1 5 1
+#0 109 764 -46 0
+0 109 764 0 0 # Clamp -46ps Tsu
+
+# Inputs: C CE CLR D \$currQ
+# Outputs: Q
+FDCE_1 1103 1 5 1
+#0 109 764 -46 0
+0 109 764 0 0 # Clamp -46ps Tsu
+
+# Inputs: C CE D PRE \$currQ
+# Outputs: Q
+FDPE 1104 1 5 1
+#0 109 -46 764 0
+0 109 0 764 0 # Clamp -46ps Tsu
+
+# Inputs: C CE D PRE \$currQ
+# Outputs: Q
+FDPE_1 1105 1 5 1
+#0 109 -46 764 0
+0 109 0 764 0 # Clamp -46ps Tsu
+
+# Inputs: C CE D S \$currQ
+# Outputs: Q
+FDSE 1106 1 5 1
+#0 109 -46 446 0
+0 109 0 446 0 # Clamp -46ps Tsu
+
+# Inputs: C CE D S \$currQ
+# Outputs: Q
+FDSE_1 1107 1 5 1
+#0 109 -46 446 0
+0 109 0 446 0 # Clamp -46ps Tsu
+
 # SLICEM/A6LUT
 # Box to emulate comb/seq behaviour of RAMD{32,64} and SRL{16,32}
 #   Necessary since RAMD* and SRL* have both combinatorial (i.e.
@@ -56,7 +122,7 @@ $__ABC9_LUT6 2000 0 7 1
 # SLICEM/A6LUT + F7BMUX
 # Box to emulate comb/seq behaviour of RAMD128
 # Inputs: A S0 S1 S2 S3 S4 S5 S6
-# Outputs: DPO SPO
+# Outputs: Y
 $__ABC9_LUT7 2001 0 8 1
 0 1047 1036 877 812 643 532 478
 

techlibs/xilinx/cells_sim.v

@@ -325,6 +325,7 @@ endmodule
 
 // Max delay from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L238-L250
 
+(* abc9_box_id=1100, lib_whitebox, abc9_flop *)
 module FDRE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -348,27 +349,17 @@ module FDRE (
   endcase endgenerate
 endmodule
 
-module FDSE (
+(* abc9_box_id=1101, lib_whitebox, abc9_flop *)
+module FDRE_1 (
   (* abc9_arrival=303 *)
   output reg Q,
   (* clkbuf_sink *)
-  (* invertible_pin = "IS_C_INVERTED" *)
   input C,
-  input CE,
+  input CE, D, R
-  (* invertible_pin = "IS_D_INVERTED" *)
-  input D,
-  (* invertible_pin = "IS_S_INVERTED" *)
-  input S
 );
-  parameter [0:0] INIT = 1'b1;
+  parameter [0:0] INIT = 1'b0;
-  parameter [0:0] IS_C_INVERTED = 1'b0;
-  parameter [0:0] IS_D_INVERTED = 1'b0;
-  parameter [0:0] IS_S_INVERTED = 1'b0;
   initial Q <= INIT;
-  generate case (|IS_C_INVERTED)
+  always @(negedge C) if (R) Q <= 1'b0; else if (CE) Q <= D;
-    1'b0: always @(posedge C) if (S == !IS_S_INVERTED) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-    1'b1: always @(negedge C) if (S == !IS_S_INVERTED) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-  endcase endgenerate
 endmodule
 
 module FDRSE (
@@ -406,6 +397,7 @@ module FDRSE (
       Q <= d;
 endmodule
 
+(* abc9_box_id=1102, lib_whitebox, abc9_flop *)
 module FDCE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -431,29 +423,17 @@ module FDCE (
   endcase endgenerate
 endmodule
 
-module FDPE (
+(* abc9_box_id=1103, lib_whitebox, abc9_flop *)
+module FDCE_1 (
   (* abc9_arrival=303 *)
   output reg Q,
   (* clkbuf_sink *)
-  (* invertible_pin = "IS_C_INVERTED" *)
   input C,
-  input CE,
+  input CE, D, CLR
-  (* invertible_pin = "IS_D_INVERTED" *)
-  input D,
-  (* invertible_pin = "IS_PRE_INVERTED" *)
-  input PRE
 );
-  parameter [0:0] INIT = 1'b1;
+  parameter [0:0] INIT = 1'b0;
-  parameter [0:0] IS_C_INVERTED = 1'b0;
-  parameter [0:0] IS_D_INVERTED = 1'b0;
-  parameter [0:0] IS_PRE_INVERTED = 1'b0;
   initial Q <= INIT;
-  generate case ({|IS_C_INVERTED, |IS_PRE_INVERTED})
+  always @(negedge C, posedge CLR) if (CLR) Q <= 1'b0; else if (CE) Q <= D;
-    2'b00: always @(posedge C, posedge PRE) if ( PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-    2'b01: always @(posedge C, negedge PRE) if (!PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-    2'b10: always @(negedge C, posedge PRE) if ( PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-    2'b11: always @(negedge C, negedge PRE) if (!PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-  endcase endgenerate
 endmodule
 
 module FDCPE (
@@ -501,42 +481,33 @@ module FDCPE (
   assign Q = qs ? qp : qc;
 endmodule
 
-module FDRE_1 (
+(* abc9_box_id=1104, lib_whitebox, abc9_flop *)
+module FDPE (
   (* abc9_arrival=303 *)
   output reg Q,
   (* clkbuf_sink *)
+  (* invertible_pin = "IS_C_INVERTED" *)
   input C,
-  input CE, D, R
+  input CE,
-);
+  (* invertible_pin = "IS_D_INVERTED" *)
-  parameter [0:0] INIT = 1'b0;
+  input D,
-  initial Q <= INIT;
+  (* invertible_pin = "IS_PRE_INVERTED" *)
-  always @(negedge C) if (R) Q <= 1'b0; else if(CE) Q <= D;
+  input PRE
-endmodule
-
-module FDSE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, S
 );
   parameter [0:0] INIT = 1'b1;
+  parameter [0:0] IS_C_INVERTED = 1'b0;
+  parameter [0:0] IS_D_INVERTED = 1'b0;
+  parameter [0:0] IS_PRE_INVERTED = 1'b0;
   initial Q <= INIT;
-  always @(negedge C) if (S) Q <= 1'b1; else if(CE) Q <= D;
+  generate case ({|IS_C_INVERTED, |IS_PRE_INVERTED})
-endmodule
+    2'b00: always @(posedge C, posedge PRE) if ( PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-
+    2'b01: always @(posedge C, negedge PRE) if (!PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-module FDCE_1 (
+    2'b10: always @(negedge C, posedge PRE) if ( PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-  (* abc9_arrival=303 *)
+    2'b11: always @(negedge C, negedge PRE) if (!PRE) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
-  output reg Q,
+  endcase endgenerate
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, CLR
-);
-  parameter [0:0] INIT = 1'b0;
-  initial Q <= INIT;
-  always @(negedge C, posedge CLR) if (CLR) Q <= 1'b0; else if (CE) Q <= D;
 endmodule
 
+(* abc9_box_id=1105, lib_whitebox, abc9_flop *)
 module FDPE_1 (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -549,6 +520,43 @@ module FDPE_1 (
   always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D;
 endmodule
 
+(* abc9_box_id=1106, lib_whitebox, abc9_flop *)
+module FDSE (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  (* invertible_pin = "IS_C_INVERTED" *)
+  input C,
+  input CE,
+  (* invertible_pin = "IS_D_INVERTED" *)
+  input D,
+  (* invertible_pin = "IS_S_INVERTED" *)
+  input S
+);
+  parameter [0:0] INIT = 1'b1;
+  parameter [0:0] IS_C_INVERTED = 1'b0;
+  parameter [0:0] IS_D_INVERTED = 1'b0;
+  parameter [0:0] IS_S_INVERTED = 1'b0;
+  initial Q <= INIT;
+  generate case (|IS_C_INVERTED)
+    1'b0: always @(posedge C) if (S == !IS_S_INVERTED) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
+    1'b1: always @(negedge C) if (S == !IS_S_INVERTED) Q <= 1'b1; else if (CE) Q <= D ^ IS_D_INVERTED;
+  endcase endgenerate
+endmodule
+
+(* abc9_box_id=1107, lib_whitebox, abc9_flop *)
+module FDSE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, S
+);
+  parameter [0:0] INIT = 1'b1;
+  initial Q <= INIT;
+  always @(negedge C) if (S) Q <= 1'b1; else if (CE) Q <= D;
+endmodule
+
 module LDCE (
   output reg Q,
   (* invertible_pin = "IS_CLR_INVERTED" *)

techlibs/xilinx/synth_xilinx.cc

@@ -107,6 +107,9 @@ struct SynthXilinxPass : public ScriptPass
 		log("    -flatten\n");
 		log("        flatten design before synthesis\n");
 		log("\n");
+		log("    -dff\n");
+		log("        run 'abc9' with -dff option\n");
+		log("\n");
 		log("    -retime\n");
 		log("        run 'abc' with -dff option\n");
 		log("\n");
@@ -120,7 +123,8 @@ struct SynthXilinxPass : public ScriptPass
 	}
 
 	std::string top_opt, edif_file, blif_file, family;
-	bool flatten, retime, vpr, ise, noiopad, noclkbuf, nobram, nolutram, nosrl, nocarry, nowidelut, nodsp, uram, abc9;
+	bool flatten, retime, vpr, ise, noiopad, noclkbuf, nobram, nolutram, nosrl, nocarry, nowidelut, nodsp, uram;
+	bool abc9, dff_mode;
 	bool flatten_before_abc;
 	int widemux;
 
@@ -145,6 +149,7 @@ struct SynthXilinxPass : public ScriptPass
 		nodsp = false;
 		uram = false;
 		abc9 = false;
+		dff_mode = false;
 		flatten_before_abc = false;
 		widemux = 0;
 	}
@@ -252,6 +257,10 @@ struct SynthXilinxPass : public ScriptPass
 				uram = true;
 				continue;
 			}
+			if (args[argidx] == "-dff") {
+				dff_mode = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -287,10 +296,11 @@ struct SynthXilinxPass : public ScriptPass
 			ff_map_file = "+/xilinx/xc7_ff_map.v";
 
 		if (check_label("begin")) {
+			std::string read_args;
 			if (vpr)
-				run("read_verilog -lib -D_EXPLICIT_CARRY +/xilinx/cells_sim.v");
+				read_args += " -D_EXPLICIT_CARRY";
-			else
+			read_args += " -lib +/xilinx/cells_sim.v";
-				run("read_verilog -lib +/xilinx/cells_sim.v");
+			run("read_verilog" + read_args);
 
 			run("read_verilog -lib +/xilinx/cells_xtra.v");
 
@@ -537,7 +547,10 @@ struct SynthXilinxPass : public ScriptPass
 				if (family != "xc7")
 					log_warning("'synth_xilinx -abc9' not currently supported for the '%s' family, "
 							"will use timing for 'xc7' instead.\n", family.c_str());
-				run("techmap -map +/xilinx/abc9_map.v -max_iter 1");
+				std::string techmap_args = "-map +/xilinx/abc9_map.v -max_iter 1";
+				if (dff_mode)
+					techmap_args += " -D DFF_MODE";
+				run("techmap " + techmap_args);
 				run("read_verilog -icells -lib +/xilinx/abc9_model.v");
 				std::string abc9_opts = " -box +/xilinx/abc9_xc7.box";
 				abc9_opts += stringf(" -W %d", XC7_WIRE_DELAY);
@@ -547,6 +560,7 @@ struct SynthXilinxPass : public ScriptPass
 				else
 					abc9_opts += " -lut +/xilinx/abc9_xc7.lut";
 				run("abc9" + abc9_opts);
+				run("techmap -map +/xilinx/abc9_unmap.v");
 			}
 			else {
 				if (nowidelut)
@@ -562,14 +576,11 @@ struct SynthXilinxPass : public ScriptPass
 				run("xilinx_srl -fixed -minlen 3", "(skip if '-nosrl')");
 			std::string techmap_args = "-map +/xilinx/lut_map.v -map +/xilinx/cells_map.v";
 			if (help_mode)
-				techmap_args += " [-map " + ff_map_file + "]";
+				techmap_args += stringf("[-map %s]", ff_map_file.c_str());
-			else if (abc9)
+			else if (!abc9)
-				techmap_args += " -map +/xilinx/abc9_unmap.v";
+				techmap_args += stringf(" -map %s", ff_map_file.c_str());
-			else
+			run("techmap " + techmap_args, "(option without '-abc9')");
-				techmap_args += " -map " + ff_map_file;
-			run("techmap " + techmap_args);
 			run("xilinx_dffopt");
-			run("clean");
 		}
 
 		if (check_label("finalize")) {
@@ -577,6 +588,7 @@ struct SynthXilinxPass : public ScriptPass
 				run("clkbufmap -buf BUFG O:I ", "(skip if '-noclkbuf')");
 			if (help_mode || ise)
 				run("extractinv -inv INV O:I", "(only if '-ise')");
+			run("clean");
 		}
 
 		if (check_label("check")) {

tests/arch/xilinx/abc9_map.ys

@@ -0,0 +1,91 @@
+read_verilog <<EOT
+module top(input C, CE, D, R, output [1:0] Q);
+FDRE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0]));
+FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDSE
+select -assert-count 1 t:FDSE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, S, output [1:0] Q);
+FDSE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0]));
+FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDRE
+select -assert-count 1 t:FDRE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, PRE, output [1:0] Q);
+FDPE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0]));
+FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDCE
+select -assert-count 1 t:FDCE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, CLR, output [1:0] Q);
+FDCE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0]));
+FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDPE
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter

tests/simple_abc9/abc9.v

@@ -264,3 +264,30 @@ always @*
   if (en)
     q <= d;
 endmodule
+
+module abc9_test031(input clk1, clk2, d, output reg q1, q2);
+always @(posedge clk1) q1 <= d;
+always @(negedge clk2) q2 <= q1;
+endmodule
+
+module abc9_test032(input clk, d, r, output reg q);
+always @(posedge clk or posedge r)
+    if (r) q <= 1'b0;
+    else q <= d;
+endmodule
+
+module abc9_test033(input clk, d, r, output reg q);
+always @(negedge clk or posedge r)
+    if (r) q <= 1'b1;
+    else q <= d;
+endmodule
+
+module abc9_test034(input clk, d, output reg q1, q2);
+always @(posedge clk) q1 <= d;
+always @(posedge clk) q2 <= q1;
+endmodule
+
+module abc9_test035(input clk, d, output reg [1:0] q);
+always @(posedge clk) q[0] <= d;
+always @(negedge clk) q[1] <= q[0];
+endmodule

tests/simple_abc9/run-test.sh

@@ -20,10 +20,12 @@ fi
 cp ../simple/*.v .
 cp ../simple/*.sv .
 DOLLAR='?'
-exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p '\
     hierarchy; \
     synth -run coarse; \
     opt -full; \
-    techmap; abc9 -lut 4 -box ../abc.box; \
+    techmap; \
+    abc9 -lut 4 -box ../abc.box; \
+    clean; \
     check -assert; \
     select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"

tests/various/abc9.v

@@ -9,3 +9,10 @@ wire w;
 unknown u(~i, w);
 unknown2 u2(w, o);
 endmodule
+
+module abc9_test032(input clk, d, r, output reg q);
+initial q = 1'b0;
+always @(negedge clk or negedge r)
+    if (!r) q <= 1'b0;
+    else q <= d;
+endmodule

tests/various/abc9.ys

@@ -22,3 +22,19 @@ abc9 -lut 4
 select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
 select -assert-count 1 t:unknown
 select -assert-none t:$lut t:unknown %% t: %D
+
+design -load read
+hierarchy -top abc9_test032
+proc
+clk2fflogic
+design -save gold
+
+abc9 -lut 4
+check
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 10 -verify -prove-asserts -show-ports miter