Merge remote-tracking branch 'origin/master' into eddie/abc9_mfs

30 files changed, 1575 insertions, 1078 deletions

diff --git a/CHANGELOG b/CHANGELOG
index 01ae17c2b..481ba266e 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -57,6 +57,8 @@ Yosys 0.9 .. Yosys 0.9-dev
       always_latch and always_ff)
     - Added "xilinx_dffopt" pass
     - Added "scratchpad" pass
+    - Added "abc9 -dff"
+    - Added "synth_xilinx -dff"
 
 Yosys 0.8 .. Yosys 0.9
 ----------------------
diff --git a/Makefile b/Makefile
index 6a8051b65..fd95219ee 100644
--- a/Makefile
+++ b/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 = 1485e63
+ABCREV = 144c5be
 ABCPULL = 1
 ABCURL ?= https://github.com/berkeley-abc/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1
diff --git a/README.md b/README.md
index 0250c7846..77e9410da 100644
--- a/README.md
+++ b/README.md
@@ -376,7 +376,11 @@ Verilog Attributes and non-standard features
 - The port attribute ``abc9_arrival`` specifies an integer (for output ports
   only) to be used as the arrival time of this sequential port. It can be used,
   for example, to specify the clk-to-Q delay of a flip-flop for consideration
-  during techmapping.
+  during `abc9` techmapping.
+
+- The module attribute ``abc9_flop`` is a boolean marking the module as a
+  flip-flop. This allows `abc9` to analyse its contents in order to perform
+  sequential synthesis.
 
 - The frontend sets attributes ``always_comb``, ``always_latch`` and
   ``always_ff`` on processes derived from SystemVerilog style always blocks
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 44718baae..a51e3648c 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -787,6 +787,14 @@ struct AigerBackend : public Backend {
 		if (top_module == nullptr)
 			log_error("Can't find top module in current design!\n");
 
+		if (!design->selected_whole_module(top_module))
+			log_cmd_error("Can't handle partially selected module %s!\n", log_id(top_module));
+
+		if (!top_module->processes.empty())
+			log_error("Found unmapped processes in module %s: unmapped processes are not supported in AIGER backend!\n", log_id(top_module));
+		if (!top_module->memories.empty())
+			log_error("Found unmapped memories in module %s: unmapped memories are not supported in AIGER backend!\n", log_id(top_module));
+
 		AigerWriter writer(top_module, zinit_mode, imode, omode, bmode, lmode);
 		writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
 
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 445103771..05e9678ee 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -82,6 +82,7 @@ struct XAigerWriter
 	dict<SigBit, SigBit> not_map, alias_map;
 	dict<SigBit, pair<SigBit, SigBit>> and_map;
 	vector<SigBit> ci_bits, co_bits;
+	dict<SigBit, Cell*> ff_bits;
 	dict<SigBit, float> arrival_times;
 
 	vector<pair<int, int>> aig_gates;
@@ -92,7 +93,7 @@ struct XAigerWriter
 	dict<SigBit, int> ordered_outputs;
 
 	vector<Cell*> box_list;
-	bool omode = false;
+	dict<IdString, std::vector<IdString>> box_ports;
 
 	int mkgate(int a0, int a1)
 	{
@@ -140,7 +141,6 @@ struct XAigerWriter
 	{
 		pool<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
-		pool<SigBit> keep_bits;
 
 		// promote public wires
 		for (auto wire : module->wires())
@@ -152,46 +152,38 @@ struct XAigerWriter
 			if (wire->port_input)
 				sigmap.add(wire);
 
+		// promote keep wires
 		for (auto wire : module->wires())
-		{
-			bool keep = wire->attributes.count("\\keep");
+			if (wire->get_bool_attribute(ID::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) {
-					undriven_bits.insert(bit);
-					unused_bits.insert(bit);
+				if (bit.wire == nullptr) {
+					if (wire->port_output) {
+						aig_map[wirebit] = (bit == State::S1) ? 1 : 0;
+						output_bits.insert(wirebit);
+					}
+					continue;
 				}
 
-				if (keep)
-					keep_bits.insert(wirebit);
+				undriven_bits.insert(bit);
+				unused_bits.insert(bit);
 
-				if (wire->port_input || keep) {
-					if (bit != wirebit)
-						alias_map[bit] = wirebit;
-					input_bits.insert(wirebit);
-				}
+				if (wire->port_input)
+					input_bits.insert(bit);
 
-				if (wire->port_output || keep) {
-					if (bit != RTLIL::Sx) {
-						if (bit != wirebit)
-							alias_map[wirebit] = bit;
-						output_bits.insert(wirebit);
-					}
-					else
-						log_debug("Skipping PO '%s' driven by 1'bx\n", log_signal(wirebit));
+				if (wire->port_output) {
+					if (bit != wirebit)
+						alias_map[wirebit] = bit;
+					output_bits.insert(wirebit);
 				}
 			}
-		}
-
-		for (auto bit : input_bits)
-			undriven_bits.erase(sigmap(bit));
-		for (auto bit : output_bits)
-			if (!bit.wire->port_input)
-				unused_bits.erase(bit);
 
 		// TODO: Speed up toposort -- ultimately we care about
 		//       box ordering, but not individual AIG cells
@@ -207,11 +199,9 @@ struct XAigerWriter
 				unused_bits.erase(A);
 				undriven_bits.erase(Y);
 				not_map[Y] = A;
-				if (!holes_mode) {
-					toposort.node(cell->name);
-					bit_users[A].insert(cell->name);
-					bit_drivers[Y].insert(cell->name);
-				}
+				toposort.node(cell->name);
+				bit_users[A].insert(cell->name);
+				bit_drivers[Y].insert(cell->name);
 				continue;
 			}
 
@@ -224,89 +214,92 @@ struct XAigerWriter
 				unused_bits.erase(B);
 				undriven_bits.erase(Y);
 				and_map[Y] = make_pair(A, B);
-				if (!holes_mode) {
-					toposort.node(cell->name);
-					bit_users[A].insert(cell->name);
-					bit_users[B].insert(cell->name);
-					bit_drivers[Y].insert(cell->name);
-				}
+				toposort.node(cell->name);
+				bit_users[A].insert(cell->name);
+				bit_users[B].insert(cell->name);
+				bit_drivers[Y].insert(cell->name);
 				continue;
 			}
 
-			log_assert(!holes_mode);
+			if (cell->type == "$__ABC9_FF_" &&
+                                        // The presence of an abc9_mergeability attribute indicates
+                                        //   that we do want to pass this flop to ABC
+                                        cell->attributes.count("\\abc9_mergeability"))
+			{
+				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 YS_ATTRIBUTE(unused) = ff_bits.insert(std::make_pair(D, cell));
+				log_assert(r.second);
+				continue;
+			}
 
 			RTLIL::Module* inst_module = module->design->module(cell->type);
-			if (inst_module && inst_module->attributes.count("\\abc9_box_id")) {
-				abc9_box_seen = true;
-
-				if (!holes_mode) {
-					toposort.node(cell->name);
-					for (const auto &conn : cell->connections()) {
-						auto port_wire = inst_module->wire(conn.first);
-						if (port_wire->port_input) {
-							// Ignore inout for the sake of topographical ordering
-							if (port_wire->port_output) continue;
+			if (inst_module) {
+				bool abc9_box = inst_module->attributes.count("\\abc9_box_id");
+				bool abc9_flop = inst_module->get_bool_attribute("\\abc9_flop");
+				if (abc9_box && cell->get_bool_attribute("\\abc9_keep"))
+					abc9_box = false;
+
+				for (const auto &conn : cell->connections()) {
+					auto port_wire = inst_module->wire(conn.first);
+
+					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);
-					}
-				}
-			}
-			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) {
-						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;
-								output_bits.insert(b);
-								unused_bits.erase(b);
 
-								if (!cell_known)
-									keep_bits.insert(b);
-							}
-						}
+						if (!abc9_flop)
+							continue;
 					}
-					if (is_output) {
+
+					if (port_wire->port_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();
-							}
+						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;
+					}
+				}
 
-						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 (abc9_box) {
+					abc9_box_seen = true;
+					toposort.node(cell->name);
+					continue;
+				}
+			}
 
-							if (arrival)
-								arrival_times[b] = arrival;
+			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)
+					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;
+							output_bits.insert(b);
 						}
 					}
-				}
 			}
 
 			//log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
@@ -346,12 +339,44 @@ struct XAigerWriter
 
 				bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */);
 
+				auto r = box_ports.insert(cell->type);
+				if (r.second) {
+					// Make carry in the last PI, and carry out the last PO
+					//   since ABC requires it this way
+					IdString carry_in, carry_out;
+					for (const auto &port_name : box_module->ports) {
+						auto w = box_module->wire(port_name);
+						log_assert(w);
+						if (w->get_bool_attribute("\\abc9_carry")) {
+							if (w->port_input) {
+								if (carry_in != IdString())
+									log_error("Module '%s' contains more than one 'abc9_carry' input port.\n", log_id(box_module));
+								carry_in = port_name;
+							}
+							if (w->port_output) {
+								if (carry_out != IdString())
+									log_error("Module '%s' contains more than one 'abc9_carry' output port.\n", log_id(box_module));
+								carry_out = port_name;
+							}
+						}
+						else
+							r.first->second.push_back(port_name);
+					}
+
+					if (carry_in != IdString() && carry_out == IdString())
+						log_error("Module '%s' contains an 'abc9_carry' input port but no output port.\n", log_id(box_module));
+					if (carry_in == IdString() && carry_out != IdString())
+						log_error("Module '%s' contains an 'abc9_carry' output port but no input port.\n", log_id(box_module));
+					if (carry_in != IdString()) {
+						r.first->second.push_back(carry_in);
+						r.first->second.push_back(carry_out);
+					}
+				}
+
 				// Fully pad all unused input connections of this box cell with S0
 				// Fully pad all undriven output connections of this box cell with anonymous wires
-				// NB: Assume box_module->ports are sorted alphabetically
-				//     (as RTLIL::Module::fixup_ports() would do)
-				for (const auto &port_name : box_module->ports) {
-					RTLIL::Wire* w = box_module->wire(port_name);
+				for (auto port_name : r.first->second) {
+					auto w = box_module->wire(port_name);
 					log_assert(w);
 					auto it = cell->connections_.find(port_name);
 					if (w->port_input) {
@@ -366,7 +391,7 @@ struct XAigerWriter
 							cell->setPort(port_name, rhs);
 						}
 
-						for (auto b : rhs.bits()) {
+						for (auto b : rhs) {
 							SigBit I = sigmap(b);
 							if (b == RTLIL::Sx)
 								b = State::S0;
@@ -377,7 +402,7 @@ struct XAigerWriter
 									alias_map[b] = I;
 							}
 							co_bits.emplace_back(b);
-							unused_bits.erase(b);
+							unused_bits.erase(I);
 						}
 					}
 					if (w->port_output) {
@@ -397,65 +422,53 @@ struct XAigerWriter
 						}
 
 						for (const auto &b : rhs.bits()) {
-							ci_bits.emplace_back(b);
 							SigBit O = sigmap(b);
 							if (O != b)
 								alias_map[O] = b;
+							ci_bits.emplace_back(b);
 							undriven_bits.erase(O);
-							input_bits.erase(b);
 						}
 					}
 				}
+
+				// Connect <cell>.abc9_ff.Q (inserted by abc9_map.v) as the last input to the flop box
+				if (box_module->get_bool_attribute("\\abc9_flop")) {
+					SigSpec rhs = module->wire(stringf("%s.abc9_ff.Q", cell->name.c_str()));
+					if (rhs.empty())
+						log_error("'%s.abc9_ff.Q' 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 (!output_bits.count(bit))
-				continue;
-			RTLIL::Wire *wire = bit.wire;
-			// If encountering an inout port, or a keep-ed wire, then create a new wire
-			// with $inout.out suffix, make it a PO driven by the existing inout, and
-			// inherit existing inout's drivers
-			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(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) {
-			undriven_bits.sort();
-			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);
-			}
-			log_warning("Treating a total of %d undriven bits in %s like $anyseq.\n", GetSize(undriven_bits), log_id(module));
+		// Make all undriven bits a primary input
+		for (auto bit : undriven_bits) {
+			input_bits.insert(bit);
+			undriven_bits.erase(bit);
 		}
 
 		if (holes_mode) {
@@ -467,25 +480,27 @@ struct XAigerWriter
 			input_bits.sort(sort_by_port_id());
 			output_bits.sort(sort_by_port_id());
 		}
-		else {
-			input_bits.sort();
-			output_bits.sort();
-		}
-
-		not_map.sort();
-		and_map.sort();
 
 		aig_map[State::S0] = 0;
 		aig_map[State::S1] = 1;
 
-		for (auto bit : input_bits) {
+		for (const auto &bit : input_bits) {
 			aig_m++, aig_i++;
 			log_assert(!aig_map.count(bit));
 			aig_map[bit] = 2*aig_m;
 		}
 
-		for (auto bit : ci_bits) {
+		for (const auto &i : ff_bits) {
+			const Cell *cell = i.second;
+			const SigBit &q = sigmap(cell->getPort("\\Q"));
+			aig_m++, aig_i++;
+			log_assert(!aig_map.count(q));
+			aig_map[q] = 2*aig_m;
+		}
+
+		for (auto &bit : ci_bits) {
 			aig_m++, aig_i++;
+			log_assert(!aig_map.count(bit));
 			aig_map[bit] = 2*aig_m;
 		}
 
@@ -494,15 +509,16 @@ struct XAigerWriter
 			aig_outputs.push_back(bit2aig(bit));
 		}
 
-		if (output_bits.empty()) {
-			output_bits.insert(State::S0);
-			omode = true;
-		}
-
-		for (auto bit : output_bits) {
+		for (const auto &bit : output_bits) {
 			ordered_outputs[bit] = aig_o++;
 			aig_outputs.push_back(bit2aig(bit));
 		}
+
+		for (auto &i : ff_bits) {
+			const SigBit &d = i.first;
+			aig_o++;
+			aig_outputs.push_back(aig_map.at(d));
+		}
 	}
 
 	void write_aiger(std::ostream &f, bool ascii_mode)
@@ -564,7 +580,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 +587,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));
-		write_h_buffer(input_bits.size() + ci_bits.size());
-		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
-		write_h_buffer(output_bits.size() + GetSize(co_bits));
-		log_debug("piNum = %d\n", GetSize(input_bits));
-		write_h_buffer(input_bits.size());
-		log_debug("poNum = %d\n", GetSize(output_bits));
-		write_h_buffer(output_bits.size());
+		log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ff_bits) + GetSize(ci_bits));
+		write_h_buffer(input_bits.size() + ff_bits.size() + ci_bits.size());
+		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(ff_bits) + GetSize(co_bits));
+		write_h_buffer(output_bits.size() + GetSize(ff_bits) + GetSize(co_bits));
+		log_debug("piNum = %d\n", GetSize(input_bits) + GetSize(ff_bits));
+		write_h_buffer(input_bits.size() + ff_bits.size());
+		log_debug("poNum = %d\n", GetSize(output_bits) + GetSize(ff_bits));
+		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 +610,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,35 +624,23 @@ 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));
 				Cell *holes_cell = r.first->second;
 				if (r.second && box_module->get_bool_attribute("\\whitebox")) {
 					holes_cell = holes_module->addCell(cell->name, cell->type);
 					holes_cell->parameters = cell->parameters;
 					r.first->second = holes_cell;
-
-					// Since Module::derive() will create a new module, there
-					//   is a chance that the ports will be alphabetically ordered
-					//   again, which is a problem when carry-chains are involved.
-					//   Inherit the port ordering from the original module here...
-					//   (and set the port_id below, when iterating through those)
-					log_assert(GetSize(box_module->ports) == GetSize(orig_box_module->ports));
-					box_module->ports = orig_box_module->ports;
 				}
 
-				// NB: Assume box_module->ports are sorted alphabetically
-				//     (as RTLIL::Module::fixup_ports() would do)
-				int box_port_id = 1;
-				for (const auto &port_name : box_module->ports) {
+				int box_inputs = 0, box_outputs = 0;
+				for (auto port_name : box_ports.at(cell->type)) {
 					RTLIL::Wire *w = box_module->wire(port_name);
 					log_assert(w);
-					if (r.second)
-						w->port_id = box_port_id++;
 					RTLIL::Wire *holes_wire;
 					RTLIL::SigSpec port_sig;
+
 					if (w->port_input)
 						for (int i = 0; i < GetSize(w); i++) {
 							box_inputs++;
@@ -655,9 +658,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 +678,23 @@ struct XAigerWriter
 					}
 				}
 
+				// For flops only, create an extra 1-bit input that drives a new wire
+				//   called "<cell>.abc9_ff.Q" 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_ff.Q", 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 +703,48 @@ 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 &d = i.first;
+				const Cell *cell = i.second;
+
+				int mergeability = cell->attributes.at(ID(abc9_mergeability)).as_int();
+				log_assert(mergeability > 0);
+				write_r_buffer(mergeability);
+
+				Const init = cell->attributes.at(ID(abc9_init));
+				log_assert(GetSize(init) == 1);
+				if (init == State::S1)
+					write_s_buffer(1);
+				else if (init == State::S0)
+					write_s_buffer(0);
+				else {
+					log_assert(init == State::Sx);
+					write_s_buffer(0);
+				}
+
+				write_i_buffer(arrival_times.at(d, 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 +752,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(holes_module->design, "aigmap");
-				for (auto cell : holes_module->cells())
-					if (!cell->type.in("$_NOT_", "$_AND_"))
+				Pass::call_on_module(holes_module->design, holes_module, "flatten -wb; techmap; aigmap");
+
+				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_ff.Q"
+						//   wire (which itself is driven an input port) we inserted above
+						Wire *currQ = holes_module->wire(stringf("%s.abc9_ff.Q", 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;
+				}
 
-				holes_module->design->selection_stack.pop_back();
+				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,19 +840,20 @@ 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)
+	void write_map(std::ostream &f)
 	{
 		dict<int, string> input_lines;
 		dict<int, string> output_lines;
-		dict<int, string> wire_lines;
 
 		for (auto wire : module->wires())
 		{
-			//if (!verbose_map && wire->name[0] == '$')
-			//	continue;
-
 			SigSpec sig = sigmap(wire);
 
 			for (int i = 0; i < GetSize(wire); i++)
@@ -781,17 +867,10 @@ 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;
 				}
-
-				if (verbose_map) {
-					if (aig_map.count(sig[i]) == 0)
-						continue;
-
-					int a = aig_map.at(sig[i]);
-					wire_lines[a] += stringf("wire %d %d %s\n", a, i, log_id(wire));
-				}
 			}
 		}
 
@@ -805,15 +884,9 @@ 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());
-
-		wire_lines.sort();
-		for (auto &it : wire_lines)
-			f << it.second;
 	}
 };
 
@@ -825,8 +898,10 @@ struct XAigerBackend : public Backend {
 		log("\n");
 		log("    write_xaiger [options] [filename]\n");
 		log("\n");
-		log("Write the current design to an XAIGER file. The design must be flattened and\n");
-		log("all unsupported cells will be converted into psuedo-inputs and pseudo-outputs.\n");
+		log("Write the top module (according to the (* top *) attribute or if only one module\n");
+		log("is currently selected) to an XAIGER file. Any non $_NOT_, $_AND_, $_ABC9_FF_, or");
+		log("non (* abc9_box_id *) cells will be converted into psuedo-inputs and\n");
+		log("pseudo-outputs.\n");
 		log("\n");
 		log("    -ascii\n");
 		log("        write ASCII version of AIGER format\n");
@@ -834,14 +909,10 @@ struct XAigerBackend : public Backend {
 		log("    -map <filename>\n");
 		log("        write an extra file with port and box symbols\n");
 		log("\n");
-		log("    -vmap <filename>\n");
-		log("        like -map, but more verbose\n");
-		log("\n");
 	}
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
 		bool ascii_mode = false;
-		bool verbose_map = false;
 		std::string map_filename;
 
 		log_header(design, "Executing XAIGER backend.\n");
@@ -857,11 +928,6 @@ struct XAigerBackend : public Backend {
 				map_filename = args[++argidx];
 				continue;
 			}
-			if (map_filename.empty() && args[argidx] == "-vmap" && argidx+1 < args.size()) {
-				map_filename = args[++argidx];
-				verbose_map = true;
-				continue;
-			}
 			break;
 		}
 		extra_args(f, filename, args, argidx, !ascii_mode);
@@ -871,6 +937,14 @@ struct XAigerBackend : public Backend {
 		if (top_module == nullptr)
 			log_error("Can't find top module in current design!\n");
 
+		if (!design->selected_whole_module(top_module))
+			log_cmd_error("Can't handle partially selected module %s!\n", log_id(top_module));
+
+		if (!top_module->processes.empty())
+			log_error("Found unmapped processes in module %s: unmapped processes are not supported in XAIGER backend!\n", log_id(top_module));
+		if (!top_module->memories.empty())
+			log_error("Found unmapped memories in module %s: unmapped memories are not supported in XAIGER backend!\n", log_id(top_module));
+
 		XAigerWriter writer(top_module);
 		writer.write_aiger(*f, ascii_mode);
 
@@ -879,7 +953,7 @@ struct XAigerBackend : public Backend {
 			mapf.open(map_filename.c_str(), std::ofstream::trunc);
 			if (mapf.fail())
 				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
-			writer.write_map(mapf, verbose_map);
+			writer.write_map(mapf);
 		}
 	}
 } XAigerBackend;
diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index cf060193d..8a114b18c 100644
--- a/frontends/aiger/aigerparse.cc
+++ b/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);
 
@@ -271,14 +271,24 @@ end_of_header:
 			if ((c == 'i' && l1 > inputs.size()) || (c == 'l' && l1 > latches.size()) || (c == 'o' && l1 > outputs.size()))
 				log_error("Line %u has invalid symbol position!\n", line_count);
 
+			RTLIL::IdString escaped_s = stringf("\\%s", s.c_str());
 			RTLIL::Wire* wire;
 			if (c == 'i') wire = inputs[l1];
 			else if (c == 'l') wire = latches[l1];
-			else if (c == 'o') wire = outputs[l1];
+			else if (c == 'o') {
+				wire = module->wire(escaped_s);
+				if (wire) {
+					// Could have been renamed by a latch
+					module->swap_names(wire, outputs[l1]);
+					module->connect(outputs[l1], wire);
+					goto next;
+				}
+				wire = outputs[l1];
+			}
 			else if (c == 'b') wire = bad_properties[l1];
 			else log_abort();
 
-			module->rename(wire, stringf("\\%s", s.c_str()));
+			module->rename(wire, escaped_s);
 		}
 		else if (c == 'j' || c == 'f') {
 			// TODO
@@ -293,6 +303,7 @@ end_of_header:
 		}
 		else
 			log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c);
+next:
 		std::getline(f, line); // Ignore up to start of next line
 	}
 
@@ -316,14 +327,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,12 +346,12 @@ 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;
 }
 
-void AigerReader::parse_xaiger(const dict<int,IdString> &box_lookup)
+void AigerReader::parse_xaiger()
 {
 	std::string header;
 	f >> header;
@@ -372,108 +383,117 @@ 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();
+
+	dict<int,IdString> box_lookup;
+	for (auto m : design->modules()) {
+		auto it = m->attributes.find(ID(abc9_box_id));
+		if (it == m->attributes.end())
+			continue;
+		if (m->name.begins_with("$paramod"))
+			continue;
+		auto id = it->second.as_int();
+		auto r = box_lookup.insert(std::make_pair(id, m->name));
+		if (!r.second)
+			log_error("Module '%s' has the same abc9_box_id = %d value as '%s'.\n",
+					log_id(m), id, log_id(r.first->second));
+		log_assert(r.second);
+	}
+
 	// Parse footer (symbol table, comments, etc.)
 	std::string s;
-	bool comment_seen = false;
-	for (int c = f.peek(); c != EOF; c = f.peek()) {
-		if (comment_seen || c == 'c') {
-			if (!comment_seen) {
-				f.ignore(1);
-				c = f.peek();
-				comment_seen = true;
-			}
-			if (c == '\n')
-				break;
-			f.ignore(1);
-			// XAIGER extensions
-			if (c == 'm') {
-				uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				uint32_t lutNum = parse_xaiger_literal(f);
-				uint32_t lutSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
-				log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize, lutNum, lutSize);
-				ConstEvalAig ce(module);
-				for (unsigned i = 0; i < lutNum; ++i) {
-					uint32_t rootNodeID = parse_xaiger_literal(f);
-					uint32_t cutLeavesM = parse_xaiger_literal(f);
-					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));
+	for (int c = f.get(); c != EOF; c = f.get()) {
+		// XAIGER extensions
+		if (c == 'm') {
+			uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			uint32_t lutNum = parse_xaiger_literal(f);
+			uint32_t lutSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize, lutNum, lutSize);
+			ConstEvalAig ce(module);
+			for (unsigned i = 0; i < lutNum; ++i) {
+				uint32_t rootNodeID = parse_xaiger_literal(f);
+				uint32_t cutLeavesM = parse_xaiger_literal(f);
+				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);
 				}
-			}
-			else if (c == 'r') {
-				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);
+				// 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));
 			}
-			else if (c == 'a' || c == 'i' || c == 'o') {
-				uint32_t dataSize = parse_xaiger_literal(f);
-				f.ignore(dataSize);
-			}
-			else {
-				break;
+		}
+		else if (c == 'r') {
+			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
-			log_error("Line %u: cannot interpret first character '%c'!\n", line_count, c);
+		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();
@@ -487,13 +507,15 @@ void AigerReader::parse_aiger_ascii()
 	unsigned l1, l2, l3;
 
 	// Parse inputs
+	int digits = ceil(log10(I));
 	for (unsigned i = 1; i <= I; ++i, ++line_count) {
 		if (!(f >> l1))
 			log_error("Line %u cannot be interpreted as an input!\n", line_count);
 		log_debug2("%d is an input\n", l1);
 		log_assert(!(l1 & 1)); // Inputs can't be inverted
-		RTLIL::Wire *wire = createWireIfNotExists(module, l1);
+		RTLIL::Wire *wire = module->addWire(stringf("$i%0*d", digits, l1 >> 1));
 		wire->port_input = true;
+		module->connect(createWireIfNotExists(module, l1), wire);
 		inputs.push_back(wire);
 	}
 
@@ -507,12 +529,14 @@ void AigerReader::parse_aiger_ascii()
 		clk_wire->port_input = true;
 		clk_wire->port_output = false;
 	}
+	digits = ceil(log10(L));
 	for (unsigned i = 0; i < L; ++i, ++line_count) {
 		if (!(f >> l1 >> l2))
 			log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 		log_debug2("%d %d is a latch\n", l1, l2);
 		log_assert(!(l1 & 1));
-		RTLIL::Wire *q_wire = createWireIfNotExists(module, l1);
+		RTLIL::Wire *q_wire = module->addWire(stringf("$l%0*d", digits, l1 >> 1));
+		module->connect(createWireIfNotExists(module, l1), q_wire);
 		RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
 
 		if (clk_wire)
@@ -550,7 +574,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 +640,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);
 	}
 
@@ -634,12 +659,14 @@ void AigerReader::parse_aiger_binary()
 		clk_wire->port_input = true;
 		clk_wire->port_output = false;
 	}
+	digits = ceil(log10(L));
 	l1 = (I+1) * 2;
 	for (unsigned i = 0; i < L; ++i, ++line_count, l1 += 2) {
 		if (!(f >> l2))
 			log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 		log_debug("%d %d is a latch\n", l1, l2);
-		RTLIL::Wire *q_wire = createWireIfNotExists(module, l1);
+		RTLIL::Wire *q_wire = module->addWire(stringf("$l%0*d", digits, l1 >> 1));
+		module->connect(createWireIfNotExists(module, l1), q_wire);
 		RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
 
 		if (clk_wire)
@@ -670,23 +697,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;
-		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;
-		}
+		RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
 		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
@@ -733,56 +752,37 @@ void AigerReader::parse_aiger_binary()
 
 void AigerReader::post_process()
 {
-	pool<IdString> seen_boxes;
-	unsigned ci_count = 0, co_count = 0;
+	dict<IdString, std::vector<IdString>> box_ports;
+	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);
 
-		if (seen_boxes.insert(cell->type).second) {
-			auto it = box_module->attributes.find("\\abc9_carry");
-			if (it != box_module->attributes.end()) {
-				RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
-				auto carry_in_out = it->second.decode_string();
-				auto pos = carry_in_out.find(',');
-				if (pos == std::string::npos)
-					log_error("'abc9_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type));
-				auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos));
-				carry_in = box_module->wire(carry_in_name);
-				if (!carry_in || !carry_in->port_input)
-					log_error("'abc9_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str());
-
-				auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1));
-				carry_out = box_module->wire(carry_out_name);
-				if (!carry_out || !carry_out->port_output)
-					log_error("'abc9_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str());
-
-				auto &ports = box_module->ports;
-				for (auto jt = ports.begin(); jt != ports.end(); ) {
-					RTLIL::Wire* w = box_module->wire(*jt);
-					log_assert(w);
-					if (w == carry_in || w == carry_out) {
-						jt = ports.erase(jt);
-						continue;
-					}
-					if (w->port_id > carry_in->port_id)
-						--w->port_id;
-					if (w->port_id > carry_out->port_id)
-						--w->port_id;
-					log_assert(w->port_input || w->port_output);
-					log_assert(ports[w->port_id-1] == w->name);
-					++jt;
+		auto r = box_ports.insert(cell->type);
+		if (r.second) {
+			// Make carry in the last PI, and carry out the last PO
+			//   since ABC requires it this way
+			IdString carry_in, carry_out;
+			for (const auto &port_name : box_module->ports) {
+				auto w = box_module->wire(port_name);
+				log_assert(w);
+				if (w->get_bool_attribute("\\abc9_carry")) {
+					if (w->port_input)
+						carry_in = port_name;
+					if (w->port_output)
+						carry_out = port_name;
 				}
-				ports.push_back(carry_in->name);
-				carry_in->port_id = ports.size();
-				ports.push_back(carry_out->name);
-				carry_out->port_id = ports.size();
+				else
+					r.first->second.push_back(port_name);
+			}
+			if (carry_in != IdString()) {
+				log_assert(carry_out != IdString());
+				r.first->second.push_back(carry_in);
+				r.first->second.push_back(carry_out);
 			}
 		}
 
-		// NB: Assume box_module->ports are sorted alphabetically
-		//     (as RTLIL::Module::fixup_ports() would do)
-		for (auto port_name : box_module->ports) {
+		for (auto port_name : box_ports.at(cell->type)) {
 			RTLIL::Wire* port = box_module->wire(port_name);
 			log_assert(port);
 			RTLIL::SigSpec rhs;
@@ -804,9 +804,32 @@ void AigerReader::post_process()
 				}
 				rhs.append(wire);
 			}
-
 			cell->setPort(port_name, rhs);
 		}
+
+		if (box_module->attributes.count("\\abc9_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 +891,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")) {
-							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);
+						module->rename(wire, escaped_s);
 					}
 					else {
 						wire->port_output = false;
@@ -889,19 +903,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")) {
-							wire->port_output = false;
-							RTLIL::Wire *in_wire = module->wire(stringf("%s[%d]", escaped_s.substr(1, escaped_s.size()-11).c_str(), 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);
-						}
+						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 +913,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 +976,10 @@ void AigerReader::post_process()
 			if (other_wire) {
 				other_wire->port_input = false;
 				other_wire->port_output = false;
-			}
-			if (wire->port_input) {
-				if (other_wire)
+				if (wire->port_input)
 					module->connect(other_wire, SigSpec(wire, i));
-			}
-			else {
-								  // 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));
+				else
+					module->connect(SigSpec(wire, i), other_wire);
 			}
 		}
 	}
@@ -1032,7 +1035,7 @@ struct AigerFrontend : public Frontend {
 	{
 		log_header(design, "Executing AIGER frontend.\n");
 
-		RTLIL::IdString clk_name = "\\clk";
+		RTLIL::IdString clk_name;
 		RTLIL::IdString module_name;
 		std::string map_filename;
 		bool wideports = false;
diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h
index 583c9d0f9..de3c3efbc 100644
--- a/frontends/aiger/aigerparse.h
+++ b/frontends/aiger/aigerparse.h
@@ -47,7 +47,7 @@ struct AigerReader
 
     AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports);
     void parse_aiger();
-    void parse_xaiger(const dict<int,IdString> &box_lookup);
+    void parse_xaiger();
     void parse_aiger_ascii();
     void parse_aiger_binary();
     void post_process();
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index 17caf6c7a..8cb34e523 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -63,22 +63,16 @@ extern "C" int Abc_RealMain(int argc, char *argv[]);
 USING_YOSYS_NAMESPACE
 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)
 {
 	return stringf("$abc$%d$%s", map_autoidx, abc9_name.c_str()+1);
 }
 
-void handle_loops(RTLIL::Design *design)
+void handle_loops(RTLIL::Design *design, RTLIL::Module *module)
 {
-	Pass::call(design, "scc -set_attr abc9_scc_id {}");
+	Pass::call(design, "scc -set_attr abc9_scc_id {} % w:*");
 
 	// For every unique SCC found, (arbitrarily) find the first
 	// cell in the component, and select (and mark) all its output
@@ -253,49 +247,14 @@ struct abc9_output_filter
 	}
 };
 
-void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
-		bool cleanup, vector<int> lut_costs, bool dff_mode, std::string clk_str,
-		bool /*keepff*/, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode,
+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 delay_target, std::string /*lutin_shared*/, bool fast_mode,
 		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 wire_delay, bool nomfs
 )
 {
-	module = current_module;
 	map_autoidx = autoidx++;
 
-	if (clk_str != "$")
-	{
-		clk_polarity = true;
-		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());
-
 	std::string tempdir_name = "/tmp/yosys-abc-XXXXXX";
 	if (!cleanup)
 		tempdir_name[0] = tempdir_name[4] = '_';
@@ -308,13 +267,13 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 	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();
@@ -333,20 +292,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);
 
@@ -360,7 +309,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++)
@@ -371,45 +320,22 @@ 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");
-		}
-	}
-
-	bool count_output = false;
-	for (auto port_name : module->ports) {
-		RTLIL::Wire *port_wire = module->wire(port_name);
-		log_assert(port_wire);
-		if (port_wire->port_output) {
-			count_output = true;
-			break;
-		}
-	}
-
 	log_push();
 
-	if (count_output)
-	{
-		design->selection_stack.emplace_back(false);
-		RTLIL::Selection& sel = design->selection_stack.back();
-		sel.select(module);
-
-		handle_loops(design);
+	handle_loops(design, module);
 
-		Pass::call(design, "aigmap");
+	Pass::call(design, "aigmap -select");
 
-		//log("Extracted %d gates and %d wires to a netlist network with %d inputs and %d outputs.\n",
-		//		count_gates, GetSize(signal_list), count_input, count_output);
+	Pass::call(design, stringf("write_xaiger -map %s/input.sym %s/input.xaig", tempdir_name.c_str(), tempdir_name.c_str()));
 
-		Pass::call(design, stringf("write_xaiger -map %s/input.sym %s/input.xaig", tempdir_name.c_str(), tempdir_name.c_str()));
+	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
@@ -420,16 +346,14 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		buffer = stringf("%s/%s", tempdir_name.c_str(), "input.sym");
 		log_assert(!design->module(ID($__abc9__)));
 		{
-			AigerReader reader(design, ifs, ID($__abc9__), "" /* clk_name */, buffer.c_str() /* map_filename */, true /* wideports */);
+			AigerReader reader(design, ifs, ID($__abc9__), "" /* clk_name */, /*buffer.c_str()*/ "" /* map_filename */, true /* wideports */);
 			reader.parse_xaiger();
 		}
 		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
 
-		design->selection_stack.pop_back();
-
 		log_header(design, "Executing ABC9.\n");
 
 		if (!lut_costs.empty()) {
@@ -475,11 +399,11 @@ 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(box_lookup);
+		reader.parse_xaiger();
 		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");
@@ -487,43 +411,32 @@ 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);
-		}
+		for (auto w : mapped_mod->wires())
+			module->addWire(remap_name(w->name), GetSize(w));
 
 		dict<IdString, bool> abc9_box;
 		vector<RTLIL::Cell*> boxes;
-		for (const auto &it : module->cells_) {
-			auto cell = it.second;
-			if (cell->type.in(ID($_AND_), ID($_NOT_))) {
-				module->remove(cell);
+		for (auto it = module->cells_.begin(); it != module->cells_.end(); ) {
+			auto cell = it->second;
+			if (cell->type.in(ID($_AND_), ID($_NOT_), ID($__ABC9_FF_))) {
+				it = module->cells_.erase(it);
 				continue;
 			}
+			++it;
+			RTLIL::Module* box_module = design->module(cell->type);
 			auto jt = abc9_box.find(cell->type);
-			if (jt == abc9_box.end()) {
-				RTLIL::Module* box_module = design->module(cell->type);
+			if (jt == abc9_box.end())
 				jt = abc9_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count(ID(abc9_box_id)))).first;
+			if (jt->second) {
+				if (box_module->get_bool_attribute("\\abc9_flop")) {
+					if (dff_mode)
+						boxes.emplace_back(cell);
+					else
+						box_module->set_bool_attribute("\\abc9_keep", false);
+				}
+				else
+					boxes.emplace_back(cell);
 			}
-			if (jt->second)
-				boxes.emplace_back(cell);
 		}
 
 		dict<SigBit, pool<IdString>> bit_drivers, bit_users;
@@ -532,19 +445,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_)) {
-				RTLIL::SigBit a_bit = c->getPort(ID::A);
-				RTLIL::SigBit y_bit = c->getPort(ID::Y);
-				bit_users[a_bit].insert(c->name);
-				bit_drivers[y_bit].insert(c->name);
+			if (mapped_cell->type == ID($_NOT_)) {
+				RTLIL::SigBit a_bit = mapped_cell->getPort(ID::A);
+				RTLIL::SigBit y_bit = mapped_cell->getPort(ID::Y);
+				bit_users[a_bit].insert(mapped_cell->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);
@@ -568,7 +481,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"));
@@ -576,44 +489,46 @@ 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
 					log_abort();
-				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 (GetSize(c->getPort(ID::A)) == 1 && c->getParam(ID(LUT)) == RTLIL::Const::from_string("01")) {
-					SigSpec my_a = module->wires_.at(remap_name(c->getPort(ID::A).as_wire()->name));
-					SigSpec my_y = module->wires_.at(remap_name(c->getPort(ID::Y).as_wire()->name));
+			if (mapped_cell->type.in(ID($lut), ID($__ABC9_FF_))) {
+				if (mapped_cell->type == ID($lut) &&
+						GetSize(mapped_cell->getPort(ID::A)) == 1 &&
+						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;
 					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;
 			if (existing_cell) {
 				cell->parameters = existing_cell->parameters;
 				cell->attributes = existing_cell->attributes;
 			}
 			else {
-				cell->parameters = c->parameters;
-				cell->attributes = c->attributes;
+				cell->parameters = mapped_cell->parameters;
+				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->get_bool_attribute("\\abc9_flop");
+			for (auto &conn : mapped_cell->connections()) {
 				RTLIL::SigSpec newsig;
 				for (auto c : conn.second.chunks()) {
 					if (c.width == 0)
@@ -625,15 +540,17 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 				}
 				cell->setPort(conn.first, newsig);
 
-				if (cell->input(conn.first)) {
-					for (auto i : newsig)
-						bit2sinks[i].push_back(cell);
-					for (auto i : conn.second)
-						bit_users[i].insert(c->name);
+				if (!abc9_flop) {
+					if (cell->input(conn.first)) {
+						for (auto i : newsig)
+							bit2sinks[i].push_back(cell);
+						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);
 			}
 		}
 
@@ -821,7 +738,7 @@ struct Abc9Pass : public Pass {
 		log("    abc9 [options] [selection]\n");
 		log("\n");
 		log("This pass uses the ABC tool [1] for technology mapping of yosys's internal gate\n");
-		log("library to a target architecture.\n");
+		log("library to a target architecture. Only fully-selected modules are supported.\n");
 		log("\n");
 		log("    -exe <command>\n");
 #ifdef ABCEXTERNAL
@@ -842,7 +759,7 @@ struct Abc9Pass : public Pass {
 		log("        if no -script parameter is given, the following scripts are used:\n");
 		log("\n");
 		log("        for -lut/-luts (only one LUT size):\n");
-		log("%s\n", fold_abc9_cmd(ABC_COMMAND_LUT /*"; lutpack {S}"*/).c_str());
+		log("%s\n", fold_abc9_cmd(ABC_COMMAND_LUT).c_str());
 		log("\n");
 		log("        for -lut/-luts (different LUT sizes):\n");
 		log("%s\n", fold_abc9_cmd(ABC_COMMAND_LUT).c_str());
@@ -858,8 +775,6 @@ struct Abc9Pass : public Pass {
 		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");
@@ -881,19 +796,10 @@ struct Abc9Pass : public Pass {
 		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("    -dff\n");
+		log("        also pass $_ABC9_FF_ cells through to ABC. modules with many clock\n");
+		log("        domains are marked as such and automatically partitioned by ABC.\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");
@@ -902,11 +808,6 @@ struct Abc9Pass : public Pass {
 		log("        print the temp dir name in log. usually this is suppressed so that the\n");
 		log("        command output is identical across runs.\n");
 		log("\n");
-		log("    -markgroups\n");
-		log("        set a 'abcgroup' attribute on all objects created by ABC. The value of\n");
-		log("        this attribute is a unique integer for each ABC process started. This\n");
-		log("        is useful for debugging the partitioning of clock domains.\n");
-		log("\n");
 		log("    -box <file>\n");
 		log("        pass this file with box library to ABC. Use with -lut.\n");
 		log("\n");
@@ -914,8 +815,8 @@ struct Abc9Pass : public Pass {
 		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("you want to use ABC to convert your design into another format.\n");
+		log("design as an XAIGER file with `write_xaiger' and then load that into ABC\n");
+		log("externally if you want to use ABC to convert your design into another format.\n");
 		log("\n");
 		log("[1] http://www.eecs.berkeley.edu/~alanmi/abc/\n");
 		log("\n");
@@ -925,8 +826,6 @@ struct Abc9Pass : public Pass {
 		log_header(design, "Executing ABC9 pass (technology mapping using ABC9).\n");
 		log_push();
 
-		assign_map.clear();
-
 #ifdef ABCEXTERNAL
 		std::string exe_file = ABCEXTERNAL;
 #else
@@ -934,11 +833,10 @@ struct Abc9Pass : public Pass {
 #endif
 		std::string script_file, clk_str, box_file, lut_file;
 		std::string delay_target, lutin_shared = "-S 1", wire_delay;
-		bool fast_mode = false, dff_mode = false, keepff = false, cleanup = true;
+		bool fast_mode = false, dff_mode = false, cleanup = true;
 		bool show_tempdir = false;
 		bool nomfs = false;
 		vector<int> lut_costs;
-		markgroups = false;
 
 #if 0
 		cleanup = false;
@@ -962,9 +860,9 @@ struct Abc9Pass : public Pass {
 		lut_arg = design->scratchpad_get_string("abc9.lut", lut_arg);
 		luts_arg = design->scratchpad_get_string("abc9.luts", luts_arg);
 		fast_mode = design->scratchpad_get_bool("abc9.fast", fast_mode);
+		dff_mode = design->scratchpad_get_bool("abc9.dff", dff_mode);
 		cleanup = !design->scratchpad_get_bool("abc9.nocleanup", !cleanup);
 		show_tempdir = design->scratchpad_get_bool("abc9.showtmp", show_tempdir);
-		markgroups = design->scratchpad_get_bool("abc9.markgroups", markgroups);
 		box_file = design->scratchpad_get_string("abc9.box", box_file);
 		if (design->scratchpad.count("abc9.W")) {
 			wire_delay = "-W " + design->scratchpad_get_string("abc9.W");
@@ -1010,19 +908,10 @@ struct Abc9Pass : 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 == "-dff") {
+				dff_mode = true;
+				continue;
+			}
 			if (arg == "-nocleanup") {
 				cleanup = false;
 				continue;
@@ -1031,10 +920,6 @@ struct Abc9Pass : public Pass {
 				show_tempdir = true;
 				continue;
 			}
-			if (arg == "-markgroups") {
-				markgroups = true;
-				continue;
-			}
 			if (arg == "-box" && argidx+1 < args.size()) {
 				box_file = args[++argidx];
 				continue;
@@ -1105,235 +990,65 @@ struct Abc9Pass : public Pass {
 		if (!box_file.empty() && !is_absolute_path(box_file) && box_file[0] != '+')
 		    box_file = std::string(pwd) + "/" + box_file;
 
-		dict<int,IdString> box_lookup;
-		for (auto m : design->modules()) {
-			auto it = m->attributes.find(ID(abc9_box_id));
-			if (it == m->attributes.end())
-				continue;
-			if (m->name.begins_with("$paramod"))
-				continue;
-			auto id = it->second.as_int();
-			auto r = box_lookup.insert(std::make_pair(id, m->name));
-			if (!r.second)
-				log_error("Module '%s' has the same abc9_box_id = %d value as '%s'.\n",
-						log_id(m), id, log_id(r.first->second));
-			log_assert(r.second);
-
-			RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
-			for (auto p : m->ports) {
-				auto w = m->wire(p);
-				log_assert(w);
-				if (w->attributes.count(ID(abc9_carry))) {
-					if (w->port_input) {
-						if (carry_in)
-							log_error("Module '%s' contains more than one 'abc9_carry' input port.\n", log_id(m));
-						carry_in = w;
-					}
-					else if (w->port_output) {
-						if (carry_out)
-							log_error("Module '%s' contains more than one 'abc9_carry' input port.\n", log_id(m));
-						carry_out = w;
-					}
-				}
-			}
-			if (carry_in || carry_out) {
-				if (carry_in && !carry_out)
-					log_error("Module '%s' contains an 'abc9_carry' input port but no output port.\n", log_id(m));
-				if (!carry_in && carry_out)
-					log_error("Module '%s' contains an 'abc9_carry' output port but no input port.\n", log_id(m));
-				// Make carry_in the last PI, and carry_out the last PO
-				//   since ABC requires it this way
-				auto &ports = m->ports;
-				for (auto it = ports.begin(); it != ports.end(); ) {
-					RTLIL::Wire* w = m->wire(*it);
-					log_assert(w);
-					if (w == carry_in || w == carry_out) {
-						it = ports.erase(it);
-						continue;
-					}
-					if (w->port_id > carry_in->port_id)
-						--w->port_id;
-					if (w->port_id > carry_out->port_id)
-						--w->port_id;
-					log_assert(w->port_input || w->port_output);
-					log_assert(ports[w->port_id-1] == w->name);
-					++it;
-				}
-				ports.push_back(carry_in->name);
-				carry_in->port_id = ports.size();
-				ports.push_back(carry_out->name);
-				carry_out->port_id = ports.size();
-			}
-		}
-
-		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)))
-				continue;
-
-			if (mod->processes.size() > 0) {
-				log("Skipping module %s as it contains processes.\n", log_id(mod));
+			if (module->processes.size() > 0) {
+				log("Skipping module %s as it contains processes.\n", log_id(module));
 				continue;
 			}
+			log_assert(!module->attributes.count(ID(abc9_box_id)));
 
-			assign_map.set(mod);
-
-			if (!dff_mode || !clk_str.empty()) {
-				abc9_module(design, mod, script_file, exe_file, cleanup, lut_costs, dff_mode, clk_str, keepff,
-						delay_target, lutin_shared, fast_mode, show_tempdir,
-						box_file, lut_file, wire_delay, box_lookup, nomfs);
-				continue;
-			}
-
-			CellTypes ct(design);
-
-			std::vector<RTLIL::Cell*> all_cells = mod->selected_cells();
-			std::set<RTLIL::Cell*> unassigned_cells(all_cells.begin(), all_cells.end());
-
-			std::set<RTLIL::Cell*> expand_queue, next_expand_queue;
-			std::set<RTLIL::Cell*> expand_queue_up, next_expand_queue_up;
-			std::set<RTLIL::Cell*> expand_queue_down, next_expand_queue_down;
+			if (!design->selected_whole_module(module))
+				log_error("Can't handle partially selected module %s!\n", log_id(module));
 
-			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;
+			assign_map.set(module);
 
-			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);
-						}
-					}
-				}
+			typedef SigSpec clkdomain_t;
+			dict<clkdomain_t, int> clk_to_mergeability;
 
-				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);
-				expand_queue.insert(cell);
-				expand_queue_up.insert(cell);
-				expand_queue_down.insert(cell);
-
-				assigned_cells[key].push_back(cell);
-				assigned_cells_reverse[cell] = key;
-			}
-
-			while (!expand_queue_up.empty() || !expand_queue_down.empty())
-			{
-				if (!expand_queue_up.empty())
-				{
-					RTLIL::Cell *cell = *expand_queue_up.begin();
-					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 (dff_mode)
+				for (auto cell : module->cells()) {
+					if (cell->type != "$__ABC9_FF_")
+						continue;
 
-				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);
+					Wire *abc9_clock_wire = module->wire(stringf("%s.clock", cell->name.c_str()));
+					if (abc9_clock_wire == NULL)
+						log_error("'%s.clock' is not a wire present in module '%s'.\n", cell->name.c_str(), log_id(module));
+					SigSpec abc9_clock = assign_map(abc9_clock_wire);
+
+					clkdomain_t key(abc9_clock);
+
+					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.init", cell->name.c_str()));
+					if (abc9_init_wire == NULL)
+						log_error("'%s.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.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.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();
+			else
+				for (auto cell : module->cells()) {
+					auto inst_module = design->module(cell->type);
+					if (!inst_module || !inst_module->get_bool_attribute("\\abc9_flop"))
+						continue;
+					cell->set_bool_attribute("\\abc9_keep");
 				}
 
-				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);
-				assign_map.set(mod);
-			}
+			design->selected_active_module = module->name.str();
+			abc9_module(design, module, script_file, exe_file, cleanup, lut_costs, dff_mode,
+					delay_target, lutin_shared, fast_mode, show_tempdir,
+					box_file, lut_file, wire_delay, nomfs);
+			design->selected_active_module.clear();
 		}
 
-		assign_map.clear();
-
 		log_pop();
 	}
 } Abc9Pass;
diff --git a/techlibs/ecp5/abc9_5g.box b/techlibs/ecp5/abc9_5g.box
index 2bc945a54..f153a665e 100644
--- a/techlibs/ecp5/abc9_5g.box
+++ b/techlibs/ecp5/abc9_5g.box
@@ -1,43 +1,36 @@
-# NB: Inputs/Outputs must be ordered alphabetically
-#     (with exceptions for carry in/out)
+# NB: Box inputs/outputs must each be in the same order
+#     as their corresponding module definition
+#     (with exceptions detailed below)
 
 # Box 1 : CCU2C (2xCARRY + 2xLUT4)
-# Outputs: S0, S1, COUT
-#   (NB: carry chain input/output must be last
-#        input/output and bus has been moved
-#        there overriding the otherwise
+#   (Exception: carry chain input/output must be the
+#        last input and output and the entire bus has been
+#        moved there overriding the otherwise
 #        alphabetical ordering)
 # name  ID   w/b   ins    outs
 CCU2C   1      1   9      3
-
-#A0   A1   B0   B1   C0    C1  D0   D1   CIN
-379  -    379  -    275   -    141  -    257
-630  379  630  379  526   275  392  141  273
-516  516  516  516  412   412  278  278  43
+#A0  B0   C0    D0   A1   B1   C1   D1   CIN
+379  379  275   141  -    -    -    -    257 # S0
+630  630  526   392  379  379  275  141  273 # S1
+516  516  412   278  516  516  412  278   43 # COUT
 
 # Box 2 : TRELLIS_DPR16X4_COMB (16x4 dist ram)
-# Outputs: DO0, DO1, DO2, DO3
 # name               ID  w/b   ins   outs
 $__ABC9_DPR16X4_COMB  2     0   8    4
-
-#A0   A1   A2   A3   RAD0   RAD1   RAD2   RAD3
-0     0    0    0    141    379    275    379
-0     0    0    0    141    379    275    379
-0     0    0    0    141    379    275    379
-0     0    0    0    141    379    275    379
+#$DO0 $DO1 $DO2 $DO3 RAD0   RAD1   RAD2   RAD3
+0     0    0    0    141    379    275    379 # DO0
+0     0    0    0    141    379    275    379 # DO1
+0     0    0    0    141    379    275    379 # DO2
+0     0    0    0    141    379    275    379 # DO3
 
 # Box 3 : PFUMX (MUX2)
-# Outputs: Z
 # name  ID   w/b   ins    outs
 PFUMX   3    1     3      1
-
 #ALUT  BLUT  C0
-98     98    151
+98     98    151 # Z
 
 # Box 4 : L6MUX21 (MUX2)
-# Outputs: Z
 # name   ID   w/b   ins    outs
 L6MUX21  4    1     3      1
-
 #D0    D1    SD
-140    141   148
+140    141   148 # Z
diff --git a/techlibs/ecp5/abc9_map.v b/techlibs/ecp5/abc9_map.v
index d8d70f9f6..113a35b91 100644
--- a/techlibs/ecp5/abc9_map.v
+++ b/techlibs/ecp5/abc9_map.v
@@ -1,24 +1,27 @@
 // ---------------------------------------
 
+// Attach a (combinatorial) black-box onto the output
+//   of this LUTRAM primitive to capture its
+//   asynchronous read behaviour
 module TRELLIS_DPR16X4 (
-	input  [3:0] DI,
-	input  [3:0] WAD,
-	input        WRE,
-	input        WCK,
-	input  [3:0] RAD,
+	(* techmap_autopurge *) input  [3:0] DI,
+	(* techmap_autopurge *) input  [3:0] WAD,
+	(* techmap_autopurge *) input        WRE,
+	(* techmap_autopurge *) input        WCK,
+	(* techmap_autopurge *) input  [3:0] RAD,
 	output [3:0] DO
 );
 	parameter WCKMUX = "WCK";
 	parameter WREMUX = "WRE";
 	parameter [63:0] INITVAL = 64'h0000000000000000;
-    wire [3:0] \$DO ;
+    wire [3:0] $DO;
 
     TRELLIS_DPR16X4 #(
       .WCKMUX(WCKMUX), .WREMUX(WREMUX), .INITVAL(INITVAL)
     ) _TECHMAP_REPLACE_ (
       .DI(DI), .WAD(WAD), .WRE(WRE), .WCK(WCK),
-      .RAD(RAD), .DO(\$DO )
+      .RAD(RAD), .DO($DO)
     );
 
-    \$__ABC9_DPR16X4_COMB do (.A(\$DO ), .S(RAD), .Y(DO));
+    $__ABC9_DPR16X4_COMB do (.$DO($DO), .RAD(RAD), .DO(DO));
 endmodule
diff --git a/techlibs/ecp5/abc9_model.v b/techlibs/ecp5/abc9_model.v
index 1dc8b5617..81e5cd070 100644
--- a/techlibs/ecp5/abc9_model.v
+++ b/techlibs/ecp5/abc9_model.v
@@ -1,5 +1,5 @@
 // ---------------------------------------
 
 (* abc9_box_id=2 *)
-module \$__ABC9_DPR16X4_COMB (input [3:0] A, S, output [3:0] Y);
+module \$__ABC9_DPR16X4_COMB (input [3:0] $DO, RAD, output [3:0] DO);
 endmodule
diff --git a/techlibs/ecp5/abc9_unmap.v b/techlibs/ecp5/abc9_unmap.v
index 9ae143c46..cbdffdaf1 100644
--- a/techlibs/ecp5/abc9_unmap.v
+++ b/techlibs/ecp5/abc9_unmap.v
@@ -1,5 +1,5 @@
 // ---------------------------------------
 
-module \$__ABC9_DPR16X4_COMB (input [3:0] A, S, output [3:0] Y);
-    assign Y = A;
+module \$__ABC9_DPR16X4_COMB (input [3:0] $DO, RAD, output [3:0] DO);
+    assign DO = $DO;
 endmodule
diff --git a/techlibs/ice40/abc9_hx.box b/techlibs/ice40/abc9_hx.box
index 3ea70bc91..31e743669 100644
--- a/techlibs/ice40/abc9_hx.box
+++ b/techlibs/ice40/abc9_hx.box
@@ -1,13 +1,17 @@
 # From https://github.com/cliffordwolf/icestorm/blob/be0bca0/icefuzz/timings_hx8k.txt
 
-# NB: Inputs/Outputs must be ordered alphabetically
-#     (with exceptions for carry in/out)
+# NB: Box inputs/outputs must each be in the same order
+#     as their corresponding module definition
+#     (with exceptions detailed below)
 
-# Inputs: A B I0 I3 CI
-# Outputs: O CO
-#   (NB: carry chain input/output must be last
-#        input/output and have been moved there
-#        overriding the alphabetical ordering)
-$__ICE40_CARRY_WRAPPER 1 1 5 2
-400 379 449 316 316
-259 231 -   -   126
+# Box 1 : $__ICE40_CARRY_WRAPPER (private cell used to preserve
+#                                 SB_LUT4+SB_CARRY)
+#   (Exception: carry chain input/output must be the
+#        last input and output and the entire bus has been
+#        moved there overriding the otherwise
+#        alphabetical ordering)
+# name                 ID  w/b ins outs
+$__ICE40_CARRY_WRAPPER 1   1   5   2
+#A  B   I0  I3  CI
+400 379 449 316 316 # O
+259 231 -   -   126 # CO
diff --git a/techlibs/ice40/abc9_lp.box b/techlibs/ice40/abc9_lp.box
index 473e92fe9..71986a67b 100644
--- a/techlibs/ice40/abc9_lp.box
+++ b/techlibs/ice40/abc9_lp.box
@@ -1,13 +1,17 @@
 # From https://github.com/cliffordwolf/icestorm/blob/be0bca0/icefuzz/timings_lp8k.txt
 
-# NB: Inputs/Outputs must be ordered alphabetically
-#     (with exceptions for carry in/out)
+# NB: Box inputs/outputs must each be in the same order
+#     as their corresponding module definition
+#     (with exceptions detailed below)
 
-# Inputs: A B I0 I3 CI
-# Outputs: O CO
-#   (NB: carry chain input/output must be last
-#        input/output and have been moved there
-#        overriding the alphabetical ordering)
-$__ICE40_CARRY_WRAPPER 1 1 5 2
-589 558 661 465 465
-675 609 -   -   186
+# Box 1 : $__ICE40_CARRY_WRAPPER (private cell used to preserve
+#                                 SB_LUT4+SB_CARRY)
+#   (Exception: carry chain input/output must be the
+#        last input and output and the entire bus has been
+#        moved there overriding the otherwise
+#        alphabetical ordering)
+# name                 ID  w/b ins outs
+$__ICE40_CARRY_WRAPPER 1   1   5   2
+#A  B   I0  I3  CI
+589 558 661 465 465 # O
+675 609 -   -   186 # CO
diff --git a/techlibs/ice40/abc9_u.box b/techlibs/ice40/abc9_u.box
index f00e247b8..48a51463e 100644
--- a/techlibs/ice40/abc9_u.box
+++ b/techlibs/ice40/abc9_u.box
@@ -1,13 +1,18 @@
 # From https://github.com/cliffordwolf/icestorm/blob/be0bca0/icefuzz/timings_up5k.txt
 
-# NB: Inputs/Outputs must be ordered alphabetically
-#     (with exceptions for carry in/out)
+# NB: Box inputs/outputs must each be in the same order
+#     as their corresponding module definition
+#     (with exceptions detailed below)
 
-# Inputs: A B I0 I3 CI
-# Outputs: O CO
-#   (NB: carry chain input/output must be last
-#        input/output and have been moved there
-#        overriding the alphabetical ordering)
-$__ICE40_CARRY_WRAPPER 1 1 5 2
-1231 1205 1285 874 874
-675  609  -    -   278
+# Box 1 : $__ICE40_CARRY_WRAPPER (private cell used to preserve
+#                                 SB_LUT4+SB_CARRY)
+# Outputs: O, CO
+#   (Exception: carry chain input/output must be the
+#        last input and output and the entire bus has been
+#        moved there overriding the otherwise
+#        alphabetical ordering)
+# name                 ID  w/b ins outs
+$__ICE40_CARRY_WRAPPER 1   1   5   2
+#A  B   I0  I3  CI
+1231 1205 1285 874 874 # O
+675  609  -    -   278 # CO
diff --git a/techlibs/xilinx/abc9_map.v b/techlibs/xilinx/abc9_map.v
index cbe2a8cef..0652064cb 100644
--- a/techlibs/xilinx/abc9_map.v
+++ b/techlibs/xilinx/abc9_map.v
@@ -18,8 +18,366 @@
  *
  */
 
-// ============================================================================
+// 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.
 
+`ifdef DFF_MODE
+// 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 --|$__ABC9_FF_|--+-->> Q
+//   abc9_ff.Q +-->>-----<        >   ||        +-----------+  |
+//             |  ||      \/\/\/\/    ||                       |
+//             |  ||                  ||                       |
+//             |  ++==================++                       |
+//             |                                               |
+//             +-----------------------------------------------+
+//
+// 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 abc9_ff.clock wire to capture its clock domain and polarity
+//     (indicated to `abc9' so that it only performs sequential synthesis
+//     (with reachability analysis) correctly on one domain at a time)
+// (d) a special abc9_ff.init wire to encode the flop's initial state
+//     NOTE: in order to perform sequential synthesis, `abc9' also requires
+//     that the initial value of all flops be zero
+// (e) a special _TECHMAP_REPLACE_.abc9_ff.Q wire that will be used for feedback
+//     into the (combinatorial) FD* cell to facilitate clock-enable behaviour
+
+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;
+  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_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+endmodule
+module FDRE_1 (output Q, input C, CE, D, R);
+  parameter [0:0] INIT = 1'b0;
+  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_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+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;
+  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_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+endmodule
+module FDSE_1 (output Q, input C, CE, D, S);
+  parameter [0:0] INIT = 1'b1;
+  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_ abc9_ff (.D($Q), .Q(QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = QQ;
+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;
+  wire QQ, $Q, $QQ;
+  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_ASYNC1 abc_async (.A($QQ), .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_ASYNC0 abc_async (.A($QQ), .S(CLR ^ IS_CLR_INVERTED), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+module FDCE_1 (output Q, input C, CE, D, CLR);
+  parameter [0:0] INIT = 1'b0;
+  wire QQ, $Q, $QQ;
+  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($QQ), .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($QQ), .S(CLR), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+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;
+  wire QQ, $Q, $QQ;
+  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($QQ), .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($QQ), .S(PRE ^ IS_PRE_INVERTED), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, IS_C_INVERTED};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+module FDPE_1 (output Q, input C, CE, D, PRE);
+  parameter [0:0] INIT = 1'b1;
+  wire QQ, $Q, $QQ;
+  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($QQ), .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($QQ), .S(PRE), .Y(QQ));
+  end endgenerate
+  $__ABC9_FF_ abc9_ff (.D($Q), .Q($QQ));
+
+  // Special signals
+  wire [1:0] abc9_ff.clock = {C, 1'b1 /* IS_C_INVERTED */};
+  wire [0:0] abc9_ff.init = 1'b0;
+  wire [0:0] _TECHMAP_REPLACE_.abc9_ff.Q = $QQ;
+endmodule
+`endif
+
+// Attach a (combinatorial) black-box onto the output
+//   of thes LUTRAM primitives to capture their
+//   asynchronous read behaviour
 module RAM32X1D (
   output DPO, SPO,
   (* techmap_autopurge *) input  D,
@@ -30,17 +388,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 dpo (.A(\$DPO ), .S({1'b1, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
+  $__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));
 endmodule
 
 module RAM64X1D (
@@ -53,17 +411,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 dpo (.A(\$DPO ), .S({DPRA5, DPRA4, DPRA3, DPRA2, DPRA1, DPRA0}), .Y(DPO));
+  $__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));
 endmodule
 
 module RAM128X1D (
@@ -75,17 +433,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 dpo (.A(\$DPO ), .S(DPRA), .Y(DPO));
+  $__ABC9_LUT7 spo (.A($SPO), .S(A), .Y(SPO));
+  $__ABC9_LUT7 dpo (.A($DPO), .S(DPRA), .Y(DPO));
 endmodule
 
 module RAM32M (
@@ -109,24 +467,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 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 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 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 dod1 (.A(\$DOD [1]), .S({1'b1, ADDRD}), .Y(DOD[1]));
+  $__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 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 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 dod0 (.A($DOD[0]), .S({1'b1, ADDRD}), .Y(DOD[0]));
+  $__ABC9_LUT6 dod1 (.A($DOD[1]), .S({1'b1, ADDRD}), .Y(DOD[1]));
 endmodule
 
 module RAM64M (
@@ -150,20 +508,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 dob (.A(\$DOB ), .S(ADDRB), .Y(DOB));
-  \$__ABC9_LUT6 doc (.A(\$DOC ), .S(ADDRC), .Y(DOC));
-  \$__ABC9_LUT6 dod (.A(\$DOD ), .S(ADDRD), .Y(DOD));
+  $__ABC9_LUT6 doa (.A($DOA), .S(ADDRA), .Y(DOA));
+  $__ABC9_LUT6 dob (.A($DOB), .S(ADDRB), .Y(DOB));
+  $__ABC9_LUT6 doc (.A($DOC), .S(ADDRC), .Y(DOC));
+  $__ABC9_LUT6 dod (.A($DOD), .S(ADDRD), .Y(DOD));
 endmodule
 
 module SRL16E (
@@ -172,14 +530,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 +548,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 (
diff --git a/techlibs/xilinx/abc9_model.v b/techlibs/xilinx/abc9_model.v
index 18d59dcd6..204fa883f 100644
--- a/techlibs/xilinx/abc9_model.v
+++ b/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*
+(* abc9_box_id = 1000, lib_whitebox *)
+module \$__ABC9_ASYNC0 (input A, S, output Y);
+  assign Y = S ? 1'b0 : A;
+endmodule
+
+// Box to emulate async behaviour of FDP*
+(* abc9_box_id = 1001, lib_whitebox *)
+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
diff --git a/techlibs/xilinx/abc9_unmap.v b/techlibs/xilinx/abc9_unmap.v
index 64135e9a7..f2342ce62 100644
--- a/techlibs/xilinx/abc9_unmap.v
+++ b/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
diff --git a/techlibs/xilinx/abc9_xc7.box b/techlibs/xilinx/abc9_xc7.box
index 9fb1cc0ef..64170546c 100644
--- a/techlibs/xilinx/abc9_xc7.box
+++ b/techlibs/xilinx/abc9_xc7.box
@@ -1,64 +1,142 @@
 # Max delays from https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf
 #                 https://github.com/SymbiFlow/prjxray-db/blob/23c8b0851f979f0799318eaca90174413a46b257/artix7/timings/slicel.sdf
 
-# NB: Inputs/Outputs must be ordered alphabetically
-#     (with exceptions for carry in/out)
+# NB: Box inputs/outputs must each be in the same order
+#     as their corresponding module definition
+#     (with exceptions detailed below)
 
-# Average across F7[AB]MUX
-# Inputs: I0 I1 S0
-# Outputs: O
-MUXF7 1 1 3 1
-204 208 286
+# Box 1 : MUXF7
+#   Max delays from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L451-L453
+# name ID w/b ins outs
+MUXF7  1  1   3   1
+#I0 I1  S0
+204 208 286 # O
 
-# Inputs: I0 I1 S0
-# Outputs: O
-MUXF8 2 1 3 1
-104 94 273
+# Box 2 : MUXF8
+#   Max delays from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L462-L464
+# name ID w/b ins outs
+MUXF8  2  1   3   1
+#I0 I1 S0
+104 94 273 # O
 
-# Box containing MUXF7.[AB] + MUXF8,
-#   Necessary to make these an atomic unit so that
-#   ABC cannot optimise just one of the MUXF7 away
-#   and expect to save on its delay
-# Inputs: I0 I1 I2 I3 S0 S1
-# Outputs: O
-$__MUXF78 3 1 6 1
-294 297 311 317 390 273
+# Box 3 : $__MUXF78
+#         (private cell used to preserve 2xMUXF7 + 1xMUXF8
+#          an atomic unit so that ABC cannot optimise just
+#          one of the MUXF7 away and expect to save on its
+#          delay, since MUXF8 is only reachable through an
+#          MUXF7)
+# name    ID w/b ins outs
+$__MUXF78 3  1   6   1
+#I0 I1  I2  I3  S0  S1
+294 297 311 317 390 273 # O
 
-# CARRY4 + CARRY4_[ABCD]X
-# Inputs: CYINIT DI0 DI1 DI2 DI3 S0 S1 S2 S3 CI
-# Outputs:  O0 O1 O2 O3 CO0 CO1 CO2 CO3
-#   (NB: carry chain input/output must be last
-#        input/output and the entire bus has been
+# Box 4 : CARRY4 + CARRY4_[ABCD]X
+#   (Exception: carry chain input/output must be the
+#        last input and output and the entire bus has been
 #        moved there overriding the otherwise
 #        alphabetical ordering)
-CARRY4 4 1 10 8
-482 -   -   -   -   223 -   -   -   222
-598 407 -   -   -   400 205 -   -   334
-584 556 537 -   -   523 558 226 -   239
-642 615 596 438 -   582 618 330 227 313
-536 379 -   -   -   340 -   -   -   271
-494 465 445 -   -   433 469 -   -   157
-592 540 520 356 -   512 548 292 -   228
-580 526 507 398 385 508 528 378 380 114
+#   Max delays from: https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf#L11-L46
+# name ID w/b ins outs
+CARRY4 4  1   10  8
+#CYINIT DI0 DI1 DI2 DI3 S0  S1  S2  S3  CI
+482     -   -   -   -   223 -   -   -   222 # O0
+598     407 -   -   -   400 205 -   -   334 # O1
+584     556 537 -   -   523 558 226 -   239 # O2
+642     615 596 438 -   582 618 330 227 313 # O3
+536     379 -   -   -   340 -   -   -   271 # CO0
+494     465 445 -   -   433 469 -   -   157 # CO1
+592     540 520 356 -   512 548 292 -   228 # CO2
+580     526 507 398 385 508 528 378 380 114 # CO3
 
+# Box 1000 : $__ABC9_ASYNC0
+#            (private cell to emulate async behaviour of FDC*)
+# name         ID   w/b ins outs
+$__ABC9_ASYNC0 1000 1   2   1
+#A S
+0  764 # Y
+
+# Box 1001 : $__ABC9_ASYNC1
+#            (private cell to emulate async behaviour of FDP*)
+# name         ID   w/b ins outs
+$__ABC9_ASYNC1 1001 1   2   1
+#A S
+0  764 # Y
+
+# Flop boxes:
+# * 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
+# * Exception: $abc9_currQ is a special input (located last) necessary for clock-enable functionality
+
+# Box 1100 : FDRE
+# name ID   w/b ins outs
+FDRE   1100 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1101 : FDRE_1
+# name ID   w/b ins outs
+FDRE_1 1101 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1102 : FDSE
+# name ID   w/b ins outs
+FDSE   1102 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1103 : FDSE_1
+# name ID   w/b ins outs
+FDSE_1 1103 1   5   1
+#C CE  D   R   $abc9_currQ
+#0 109 -46 404 0
+0 109 0   404 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1104 : FDCE
+# name ID   w/b ins outs
+FDCE   1104 1   5   1
+#C CE  CLR D   $abc9_currQ
+#0 109 764 -46 0
+0 109 764 0   0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1105 : FDCE_1
+# name ID   w/b ins outs
+FDCE_1 1105 1   5   1
+#C CE  CLR D   $abc9_currQ
+#0 109 764 -46 0
+0 109 764 0   0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1106 : FDPE
+# name ID   w/b ins outs
+FDPE   1106 1   5   1
+#C CE  D   PRE $abc9_currQ
+#0 109 -46 764 0
+0 109 0   764 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 1107 : FDPE_1
+# name ID   w/b ins outs
+FDPE_1 1107 1   5   1
+#C CE  D   PRE $abc9_currQ
+#0 109 -46 764 0
+0 109 0   764 0 # Q (-46ps Tsu clamped to 0)
+
+# Box 2000 : $__ABC9_LUT6
+#            (private cell to emulate async behaviour of LUTRAMs)
 # 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.
-#   same-cycle read operation) and sequential (write operation
-#   is only committed on the next clock edge).
-#   To model the combinatorial path, such cells have to be split
-#   into comb and seq parts, with this box modelling only the former.
-# Inputs: A S0 S1 S2 S3 S4 S5
-# Outputs: Y
-$__ABC9_LUT6 2000 0 7 1
-0 642 631 472 407 238 127
+# name       ID   w/b ins outs
+$__ABC9_LUT6 2000 0   7   1
+#A S0  S1  S2  S3  S4  S5
+0  642 631 472 407 238 127 # Y
 
-# SLICEM/A6LUT + F7BMUX
-# Box to emulate comb/seq behaviour of RAMD128
-# Inputs: A S0 S1 S2 S3 S4 S5 S6
-# Outputs: DPO SPO
+# Box 2001 : $__ABC9_LUT6
+#            (private cell to emulate async behaviour of LUITRAMs)
+# name       ID   w/b ins outs
 $__ABC9_LUT7 2001 0 8 1
-0 1047 1036 877 812 643 532 478
+#A S0   S1   S2  S3  S4  S5  S6
+0  1047 1036 877 812 643 532 478 # Y
 
 # Boxes used to represent the comb behaviour of various modes
 #   of DSP48E1
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index 1cd4d2f30..22dca3c47 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/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,6 +349,20 @@ module FDRE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1101, lib_whitebox, abc9_flop *)
+module FDRE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, R
+);
+  parameter [0:0] INIT = 1'b0;
+  initial Q <= INIT;
+  always @(negedge C) if (R) Q <= 1'b0; else if (CE) Q <= D;
+endmodule
+
+(* abc9_box_id=1102, lib_whitebox, abc9_flop *)
 module FDSE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -371,6 +386,19 @@ module FDSE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1103, 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 FDRSE (
   output reg Q,
   (* clkbuf_sink *)
@@ -406,6 +434,7 @@ module FDRSE (
       Q <= d;
 endmodule
 
+(* abc9_box_id=1104, lib_whitebox, abc9_flop *)
 module FDCE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -413,10 +442,10 @@ module FDCE (
   (* invertible_pin = "IS_C_INVERTED" *)
   input C,
   input CE,
-  (* invertible_pin = "IS_D_INVERTED" *)
-  input D,
   (* invertible_pin = "IS_CLR_INVERTED" *)
-  input CLR
+  input CLR,
+  (* invertible_pin = "IS_D_INVERTED" *)
+  input D
 );
   parameter [0:0] INIT = 1'b0;
   parameter [0:0] IS_C_INVERTED = 1'b0;
@@ -431,6 +460,20 @@ module FDCE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1105, lib_whitebox, abc9_flop *)
+module FDCE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* 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=1106, lib_whitebox, abc9_flop *)
 module FDPE (
   (* abc9_arrival=303 *)
   output reg Q,
@@ -456,6 +499,19 @@ module FDPE (
   endcase endgenerate
 endmodule
 
+(* abc9_box_id=1107, lib_whitebox, abc9_flop *)
+module FDPE_1 (
+  (* abc9_arrival=303 *)
+  output reg Q,
+  (* clkbuf_sink *)
+  input C,
+  input CE, D, PRE
+);
+  parameter [0:0] INIT = 1'b1;
+  initial Q <= INIT;
+  always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D;
+endmodule
+
 module FDCPE (
   output wire Q,
   (* clkbuf_sink *)
@@ -501,54 +557,6 @@ module FDCPE (
   assign Q = qs ? qp : qc;
 endmodule
 
-module FDRE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, R
-);
-  parameter [0:0] INIT = 1'b0;
-  initial Q <= INIT;
-  always @(negedge C) if (R) Q <= 1'b0; else if(CE) Q <= D;
-endmodule
-
-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 FDCE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* 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
-
-module FDPE_1 (
-  (* abc9_arrival=303 *)
-  output reg Q,
-  (* clkbuf_sink *)
-  input C,
-  input CE, D, PRE
-);
-  parameter [0:0] INIT = 1'b1;
-  initial Q <= INIT;
-  always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D;
-endmodule
-
 module LDCE (
   output reg Q,
   (* invertible_pin = "IS_CLR_INVERTED" *)
@@ -2388,8 +2396,8 @@ module DSP48E1 (
                     if (CEB2) Br2 <= Br1;
                 end
         end else if (BREG == 1) begin
-            //initial Br1 = 25'b0;
-            initial Br2 = 25'b0;
+            //initial Br1 = 18'b0;
+            initial Br2 = 18'b0;
             always @(posedge CLK)
                 if (RSTB) begin
                     Br1 <= 18'b0;
@@ -2436,7 +2444,7 @@ module DSP48E1 (
     endgenerate
 
     // A/D input selection and pre-adder
-    wire signed [29:0] Ar12_muxed = INMODEr[0] ? Ar1 : Ar2;
+    wire signed [24:0] Ar12_muxed = INMODEr[0] ? Ar1 : Ar2;
     wire signed [24:0] Ar12_gated = INMODEr[1] ? 25'b0 : Ar12_muxed;
     wire signed [24:0] Dr_gated   = INMODEr[2] ? Dr : 25'b0;
     wire signed [24:0] AD_result  = INMODEr[3] ? (Dr_gated - Ar12_gated) : (Dr_gated + Ar12_gated);
diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc
index e1748562e..63d00027a 100644
--- a/techlibs/xilinx/synth_xilinx.cc
+++ b/techlibs/xilinx/synth_xilinx.cc
@@ -107,8 +107,12 @@ struct SynthXilinxPass : public ScriptPass
 		log("    -flatten\n");
 		log("        flatten design before synthesis\n");
 		log("\n");
+		log("    -dff\n");
+		log("        run 'abc'/'abc9' with -dff option\n");
+		log("\n");
 		log("    -retime\n");
-		log("        run 'abc' with '-dff -D 1' options\n");
+		log("        run 'abc' with '-D 1' option to enable flip-flop retiming.\n");
+		log("        implies -dff.\n");
 		log("\n");
 		log("    -abc9\n");
 		log("        use new ABC9 flow (EXPERIMENTAL)\n");
@@ -120,7 +124,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 +150,7 @@ struct SynthXilinxPass : public ScriptPass
 		nodsp = false;
 		uram = false;
 		abc9 = false;
+		dff_mode = false;
 		flatten_before_abc = false;
 		widemux = 0;
 	}
@@ -190,6 +196,7 @@ struct SynthXilinxPass : public ScriptPass
 				continue;
 			}
 			if (args[argidx] == "-retime") {
+				dff_mode = true;
 				retime = true;
 				continue;
 			}
@@ -252,6 +259,10 @@ struct SynthXilinxPass : public ScriptPass
 				uram = true;
 				continue;
 			}
+			if (args[argidx] == "-dff") {
+				dff_mode = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -287,10 +298,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");
-			else
-				run("read_verilog -lib +/xilinx/cells_sim.v");
+				read_args += " -D_EXPLICIT_CARRY";
+			read_args += " -lib +/xilinx/cells_sim.v";
+			run("read_verilog" + read_args);
 
 			run("read_verilog -lib +/xilinx/cells_xtra.v");
 
@@ -532,12 +544,15 @@ struct SynthXilinxPass : public ScriptPass
 			if (flatten_before_abc)
 				run("flatten");
 			if (help_mode)
-				run("abc -luts 2:2,3,6:5[,10,20] [-dff]", "(option for 'nowidelut'; option for '-retime')");
+				run("abc -luts 2:2,3,6:5[,10,20] [-dff] [-D 1]", "(option for 'nowidelut', '-dff', '-retime')");
 			else if (abc9) {
 				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);
@@ -545,13 +560,22 @@ struct SynthXilinxPass : public ScriptPass
 					abc9_opts += " -lut +/xilinx/abc9_xc7_nowide.lut";
 				else
 					abc9_opts += " -lut +/xilinx/abc9_xc7.lut";
+				if (dff_mode)
+					abc9_opts += " -dff";
 				run("abc9" + abc9_opts);
+				run("techmap -map +/xilinx/abc9_unmap.v");
 			}
 			else {
+				std::string abc_opts;
 				if (nowidelut)
-					run("abc -luts 2:2,3,6:5" + string(retime ? " -dff -D 1" : ""));
+					abc_opts += " -luts 2:2,3,6:5";
 				else
-					run("abc -luts 2:2,3,6:5,10,20" + string(retime ? " -dff -D 1" : ""));
+					abc_opts += " -luts 2:2,3,6:5,10,20";
+				if (dff_mode)
+					abc_opts += " -dff";
+				if (retime)
+					abc_opts += " -D 1";
+				run("abc" + abc_opts);
 			}
 			run("clean");
 
@@ -561,14 +585,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 + "]";
-			else if (abc9)
-				techmap_args += " -map +/xilinx/abc9_unmap.v";
-			else
-				techmap_args += " -map " + ff_map_file;
-			run("techmap " + techmap_args);
+				techmap_args += stringf("[-map %s]", ff_map_file.c_str());
+			else if (!abc9)
+				techmap_args += stringf(" -map %s", ff_map_file.c_str());
+			run("techmap " + techmap_args, "(only if '-abc9')");
 			run("xilinx_dffopt");
-			run("clean");
 		}
 
 		if (check_label("finalize")) {
@@ -576,6 +597,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")) {
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index deaf48a3d..8e932b091 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -33,7 +33,7 @@ design -import gold -as gold
 design -import gate -as gate
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -show-ports -seq 16 miter
-"
+" -l ${aag}.log
 done
 
 for aig in *.aig; do
@@ -50,5 +50,5 @@ design -import gold -as gold
 design -import gate -as gate
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -show-ports -seq 16 miter
-"
+" -l ${aig}.log
 done
diff --git a/tests/aiger/symbols.aag b/tests/aiger/symbols.aag
new file mode 100644
index 000000000..93f8989f2
--- /dev/null
+++ b/tests/aiger/symbols.aag
@@ -0,0 +1,9 @@
+aag 2 1 1 1 0
+2
+4 2 1
+4
+i0 d
+l0 q
+o0 q
+c
+Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os)
diff --git a/tests/aiger/symbols.aig b/tests/aiger/symbols.aig
new file mode 100644
index 000000000..a7922ab46
--- /dev/null
+++ b/tests/aiger/symbols.aig
@@ -0,0 +1,8 @@
+aig 2 1 1 1 0
+2 1
+4
+i0 d
+l0 q
+o0 q
+c
+Generated by Yosys 0.9+932 (git sha1 baba33fb, clang 9.0.0-2 -fPIC -Os)
diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys
new file mode 100644
index 000000000..b457cefce
--- /dev/null
+++ b/tests/arch/xilinx/abc9_dff.ys
@@ -0,0 +1,32 @@
+read_verilog <<EOT
+module top(input C, D, output [7:0] Q);
+FDRE   fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
+FDSE   fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
+FDCE   fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
+FDPE   fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
+FDRE_1 fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
+FDSE_1 fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
+FDCE_1 fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
+FDPE_1 fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
+endmodule
+EOT
+equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
+design -load postopt
+select -assert-none t:FD*
+
+design -reset
+read_verilog <<EOT
+module top(input C, D, output [7:0] Q);
+FDRE   fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
+FDSE   fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
+FDCE   fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
+FDPE   fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
+FDRE_1 fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
+FDSE_1 fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
+FDCE_1 fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
+FDPE_1 fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
+endmodule
+EOT
+equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
+design -load postopt
+select -assert-none t:FD*
diff --git a/tests/arch/xilinx/abc9_map.ys b/tests/arch/xilinx/abc9_map.ys
new file mode 100644
index 000000000..4a7b9384a
--- /dev/null
+++ b/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 -D DFF_MODE
+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 -D DFF_MODE
+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 -D DFF_MODE
+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 -D DFF_MODE
+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
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index de60619d1..8afd0ce96 100644
--- a/tests/simple_abc9/abc9.v
+++ b/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
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
index 0d4262005..bc921daa9 100755
--- a/tests/simple_abc9/run-test.sh
+++ b/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_ %%'"
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index 30ebd4e26..f0b3f6837 100644
--- a/tests/various/abc9.v
+++ b/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
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 5c9a4075d..81d0afd1b 100644
--- a/tests/various/abc9.ys
+++ b/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