Merge branch 'xaig' into xc7mux

37 files changed, 867 insertions, 1745 deletions

diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 000000000..9910e9954
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,13 @@
+.editorconfig

+.gitignore

+.gitmodules

+.github

+.git

+Dockerfile

+README.md

+manual

+CodingReadme

+CodeOfConduct

+.travis

+.travis.yml

+

diff --git a/CHANGELOG b/CHANGELOG
index c1b548aeb..44e32c6a8 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -17,9 +17,11 @@ Yosys 0.8 .. Yosys 0.8-dev
     - Added "rename -src"
     - Added "equiv_opt" pass
     - Added "read_aiger" frontend
-    - Added "muxpack" pass
+    - Added "abc9" pass for timing-aware techmapping (experimental, FPGA only, no FFs)
+    - Added "synth_xilinx -abc9" (experimental)
+    - Added "synth_ice40 -abc9" (experimental)
+    - Added "synth -abc9" (experimental)
     - "synth_xilinx" to now infer hard shift registers, using new "shregmap -tech xilinx"
-    - "synth_xilinx" to now infer wide multiplexers
 
 
 Yosys 0.7 .. Yosys 0.8
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 000000000..3c7188d82
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,33 @@
+FROM ubuntu:18.04 as builder
+LABEL author="Abdelrahman Hosny <abdelrahman.hosny@hotmail.com>"
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install -y build-essential \
+    clang \
+    bison \
+    flex \
+    libreadline-dev \
+    gawk \
+    tcl-dev \
+    libffi-dev \
+    git \
+    pkg-config \
+    python3 && \
+    rm -rf /var/lib/apt/lists
+COPY . /
+RUN make && \
+    make install
+
+FROM ubuntu:18.04
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && apt-get install -y libreadline-dev tcl-dev
+
+COPY --from=builder /yosys /build/yosys
+COPY --from=builder /yosys-abc /build/yosys-abc
+COPY --from=builder /yosys-config /build/yosys-config
+COPY --from=builder /yosys-filterlib /build/yosys-filterlib
+COPY --from=builder /yosys-smtbmc /build/yosys-smtbmc
+
+ENV PATH /build:$PATH
+RUN useradd -m yosys
+USER yosys
+ENTRYPOINT ["yosys"]
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index bf2f9f1bc..7cb311736 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -2,7 +2,7 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  Copyright (C) 2019  Eddie Hung <eddie@fpgeh.com>
+ *                2019  Eddie Hung <eddie@fpgeh.com>
  *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
@@ -18,14 +18,32 @@
  *
  */
 
+// https://stackoverflow.com/a/46137633
+#ifdef _MSC_VER
+#include <stdlib.h>
+#define __builtin_bswap32 _byteswap_ulong
+#elif defined(__APPLE__)
+#include <libkern/OSByteOrder.h>
+#define __builtin_bswap32 OSSwapInt32
+#endif
+
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
-#include "kernel/celltypes.h"
 #include "kernel/utils.h"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+inline int32_t to_big_endian(int32_t i32) {
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+	return __builtin_bswap32(i32);
+#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
+	return i32;
+#else
+#error "Unknown endianness"
+#endif
+}
+
 void aiger_encode(std::ostream &f, int x)
 {
 	log_assert(x >= 0);
@@ -105,7 +123,7 @@ struct XAigerWriter
 		return aig_map.at(bit);
 	}
 
-	XAigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode, bool holes_mode=false) : module(module), zinit_mode(zinit_mode), sigmap(module)
+	XAigerWriter(Module *module, bool zinit_mode, bool holes_mode=false) : module(module), zinit_mode(zinit_mode), sigmap(module)
 	{
 		pool<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
@@ -142,17 +160,11 @@ struct XAigerWriter
 				SigBit wirebit(wire, i);
 				SigBit bit = sigmap(wirebit);
 
-				if (bit.wire == nullptr) {
-					if (wire->port_output) {
-						aig_map[wirebit] = (bit == State::S1) ? 1 : 0;
-						output_bits.insert(wirebit);
-					}
-					continue;
+				if (bit.wire) {
+					undriven_bits.insert(bit);
+					unused_bits.insert(bit);
 				}
 
-				undriven_bits.insert(bit);
-				unused_bits.insert(bit);
-
 				if (wire->port_input || keep) {
 					if (bit != wirebit)
 						alias_map[bit] = wirebit;
@@ -169,57 +181,16 @@ struct XAigerWriter
 
 		for (auto bit : input_bits)
 			undriven_bits.erase(sigmap(bit));
-
 		for (auto bit : output_bits)
 			if (!bit.wire->port_input)
 				unused_bits.erase(bit);
 
-		dict<SigBit, pool<IdString>> bit_drivers, bit_users;
-		TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
-		bool abc_box_seen = false;
-
-		for (auto cell : module->cells())
-		{
-			RTLIL::Module* inst_module = module->design->module(cell->type);
-			bool builtin_type = yosys_celltypes.cell_known(cell->type);
-			bool abc_type = inst_module && inst_module->attributes.count("\\abc_box_id");
+		SigMap topomap;
+		topomap.database = sigmap.database;
 
-			if (!holes_mode) {
-				toposort.node(cell->name);
-				for (const auto &conn : cell->connections()) {
-					if (!builtin_type && !abc_type)
-						continue;
-
-					if (!cell->type.in("$_NOT_", "$_AND_")) {
-						if (builtin_type) {
-							if (conn.first.in("\\Q", "\\CTRL_OUT", "\\RD_DATA"))
-								continue;
-							if (cell->type == "$memrd" && conn.first == "\\DATA")
-								continue;
-						}
-
-						if (inst_module) {
-							RTLIL::Wire* inst_module_port = inst_module->wire(conn.first);
-							log_assert(inst_module_port);
-
-							if (inst_module_port->port_output && inst_module_port->attributes.count("\\abc_flop_q"))
-									continue;
-						}
-					}
-
-					if (cell->input(conn.first)) {
-						// Ignore inout for the sake of topographical ordering
-						if (cell->output(conn.first)) continue;
-						for (auto bit : sigmap(conn.second))
-							bit_users[bit].insert(cell->name);
-					}
-
-					if (cell->output(conn.first))
-						for (auto bit : sigmap(conn.second))
-							bit_drivers[bit].insert(cell->name);
-				}
-			}
+		bool abc_box_seen = false;
 
+		for (auto cell : module->cells()) {
 			if (cell->type == "$_NOT_")
 			{
 				SigBit A = sigmap(cell->getPort("\\A").as_bit());
@@ -227,6 +198,8 @@ struct XAigerWriter
 				unused_bits.erase(A);
 				undriven_bits.erase(Y);
 				not_map[Y] = A;
+				if (!holes_mode)
+					topomap.add(Y, A);
 				continue;
 			}
 
@@ -249,6 +222,10 @@ struct XAigerWriter
 				unused_bits.erase(B);
 				undriven_bits.erase(Y);
 				and_map[Y] = make_pair(A, B);
+				if (!holes_mode) {
+					topomap.add(Y, A);
+					topomap.add(Y, B);
+				}
 				continue;
 			}
 
@@ -260,50 +237,52 @@ struct XAigerWriter
 			//	continue;
 			//}
 
-			bool inst_flop = inst_module ? inst_module->attributes.count("\\abc_flop") : false;
-			if (inst_flop) {
-				SigBit d, q;
-				for (const auto &c : cell->connections()) {
-					auto is_input = cell->input(c.first);
-					auto is_output = cell->output(c.first);
-					log_assert(is_input || is_output);
-					RTLIL::Wire* port = inst_module->wire(c.first);
-					for (auto b : c.second.bits()) {
-						if (is_input && port->attributes.count("\\abc_flop_d")) {
-							d = b;
-							SigBit I = sigmap(d);
-							if (I != d)
-								alias_map[I] = d;
-							unused_bits.erase(d);
-						}
-						if (is_output && port->attributes.count("\\abc_flop_q")) {
-							q = b;
-							SigBit O = sigmap(q);
-							if (O != q)
-								alias_map[O] = q;
-							undriven_bits.erase(O);
-						}
-					}
-				}
-				if (!abc_box_seen)
-					abc_box_seen = inst_module->attributes.count("\\abc_box_id");
-
-				ff_bits.emplace_back(d, q);
-			}
-			else if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
+			RTLIL::Module* inst_module = module->design->module(cell->type);
+			//bool inst_flop = inst_module ? inst_module->attributes.count("\\abc_flop") : false;
+			//if (inst_flop) {
+			//	SigBit d, q;
+			//	for (const auto &c : cell->connections()) {
+			//		auto is_input = cell->input(c.first);
+			//		auto is_output = cell->output(c.first);
+			//		log_assert(is_input || is_output);
+			//		RTLIL::Wire* port = inst_module->wire(c.first);
+			//		for (auto b : c.second.bits()) {
+			//			if (is_input && port->attributes.count("\\abc_flop_d")) {
+			//				d = b;
+			//				SigBit I = sigmap(d);
+			//				if (I != d)
+			//					alias_map[I] = d;
+			//				unused_bits.erase(d);
+			//			}
+			//			if (is_output && port->attributes.count("\\abc_flop_q")) {
+			//				q = b;
+			//				SigBit O = sigmap(q);
+			//				if (O != q)
+			//					alias_map[O] = q;
+			//				undriven_bits.erase(O);
+			//			}
+			//		}
+			//	}
+			//	if (!abc_box_seen)
+			//		abc_box_seen = inst_module->attributes.count("\\abc_box_id");
+
+			//	ff_bits.emplace_back(d, q);
+			//}
+			/*else*/ if (inst_module && inst_module->attributes.count("\\abc_box_id")) {
 				abc_box_seen = true;
 			}
 			else {
 				for (const auto &c : cell->connections()) {
 					if (c.second.is_fully_const()) continue;
-					for (auto b : c.second.bits()) {
-						Wire *w = b.wire;
-						if (!w) continue;
-						auto is_input = cell->input(c.first);
-						auto is_output = cell->output(c.first);
-						log_assert(is_input || is_output);
-						if (is_input) {
-							if (!w->port_input) {
+					auto is_input = cell->input(c.first);
+					auto is_output = cell->output(c.first);
+					log_assert(is_input || is_output);
+
+					if (is_input) {
+						for (auto b : c.second.bits()) {
+							Wire *w = b.wire;
+							if (!w) continue;
+							if (!w->port_output) {
 								SigBit I = sigmap(b);
 								if (I != b)
 									alias_map[b] = I;
@@ -311,7 +290,11 @@ struct XAigerWriter
 								unused_bits.erase(b);
 							}
 						}
-						if (is_output) {
+					}
+					if (is_output) {
+						for (auto b : c.second.bits()) {
+							Wire *w = b.wire;
+							if (!w) continue;
 							input_bits.insert(b);
 							SigBit O = sigmap(b);
 							if (O != b)
@@ -325,20 +308,46 @@ struct XAigerWriter
 			//log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 		}
 
-		if (abc_box_seen) {
+		if (abc_box_seen && !holes_mode) {
+			TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
+			dict<SigBit, pool<IdString>> bit_drivers, bit_users;
+
+			for (auto cell : module->cells()) {
+				RTLIL::Module* inst_module = module->design->module(cell->type);
+				if (!inst_module || !inst_module->attributes.count("\\abc_box_id"))
+					continue;
+				toposort.node(cell->name);
+				for (const auto &conn : cell->connections()) {
+					if (cell->input(conn.first)) {
+						// Ignore inout for the sake of topographical ordering
+						if (cell->output(conn.first)) continue;
+						for (auto bit : topomap(conn.second))
+							if (bit.wire)
+								bit_users[bit].insert(cell->name);
+					}
+
+					if (cell->output(conn.first)) {
+						RTLIL::Wire* inst_module_port = inst_module->wire(conn.first);
+						log_assert(inst_module_port);
+						//if (inst_module_port->attributes.count("\\abc_flop_q"))
+						//	continue;
+						for (auto bit : topomap(conn.second))
+							bit_drivers[bit].insert(cell->name);
+					}
+				}
+			}
+
 			for (auto &it : bit_users)
 				if (bit_drivers.count(it.first))
 					for (auto driver_cell : bit_drivers.at(it.first))
-					for (auto user_cell : it.second)
-						toposort.edge(driver_cell, user_cell);
-
-			pool<RTLIL::Module*> abc_carry_modules;
+						for (auto user_cell : it.second)
+							toposort.edge(driver_cell, user_cell);
 
-#if 0
+#if 1
 			toposort.analyze_loops = true;
 #endif
 			bool no_loops = toposort.sort();
-#if 0
+#if 1
 			unsigned i = 0;
 			for (auto &it : toposort.loops) {
 				log("  loop %d", i++);
@@ -349,13 +358,14 @@ struct XAigerWriter
 #endif
 			log_assert(no_loops);
 
+			pool<RTLIL::Module*> abc_carry_modules;
 			for (auto cell_name : toposort.sorted) {
 				RTLIL::Cell *cell = module->cell(cell_name);
 				RTLIL::Module* box_module = module->design->module(cell->type);
-				if (!box_module || !box_module->attributes.count("\\abc_box_id"))
-					continue;
+				log_assert(box_module);
+				log_assert(box_module->attributes.count("\\abc_box_id"));
 
-				if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) {
+				if (!abc_carry_modules.count(box_module) && box_module->attributes.count("\\abc_carry")) {
 					RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr;
 					RTLIL::Wire* last_in = nullptr, *last_out = nullptr;
 					for (const auto &port_name : box_module->ports) {
@@ -451,8 +461,6 @@ struct XAigerWriter
 				}
 				box_list.emplace_back(cell);
 			}
-
-			// TODO: Free memory from toposort, bit_drivers, bit_users
 		}
 
 		for (auto bit : input_bits) {
@@ -483,10 +491,6 @@ struct XAigerWriter
 			}
 		}
 
-		// Erase all POs that are undriven
-		if (!holes_mode)
-			for (auto bit : undriven_bits)
-				output_bits.erase(bit);
 		for (auto bit : unused_bits)
 			undriven_bits.erase(bit);
 
@@ -543,10 +547,6 @@ struct XAigerWriter
 				ff_aig_map[bit] = 2*aig_m;
 		}
 
-		if (imode && input_bits.empty()) {
-			aig_m++, aig_i++;
-		}
-
 		//if (zinit_mode)
 		//{
 		//	for (auto it : ff_map) {
@@ -620,18 +620,9 @@ struct XAigerWriter
 			aig_outputs.push_back(ff_aig_map.at(bit));
 		}
 
-		if (omode && output_bits.empty()) {
-			aig_o++;
-			aig_outputs.push_back(0);
-		}
-
-		if (bmode) {
-			//aig_b++;
-			aig_outputs.push_back(0);
-		}
 	}
 
-	void write_aiger(std::ostream &f, bool ascii_mode, bool miter_mode, bool symbols_mode, bool omode)
+	void write_aiger(std::ostream &f, bool ascii_mode)
 	{
 		int aig_obc = aig_o;
 		int aig_obcj = aig_obc;
@@ -708,98 +699,25 @@ struct XAigerWriter
 			}
 		}
 
-		if (symbols_mode)
-		{
-			dict<string, vector<string>> symbols;
-
-			bool output_seen = false;
-			for (auto wire : module->wires())
-			{
-				//if (wire->name[0] == '$')
-				//	continue;
-
-				SigSpec sig = sigmap(wire);
-
-				for (int i = 0; i < GetSize(wire); i++)
-				{
-					RTLIL::SigBit b(wire, i);
-					if (input_bits.count(b)) {
-						int a = aig_map.at(sig[i]);
-						log_assert((a & 1) == 0);
-						if (GetSize(wire) != 1)
-							symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("%s[%d]", log_id(wire), i));
-						else
-							symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("%s", log_id(wire)));
-					}
-
-					if (output_bits.count(b)) {
-						int o = ordered_outputs.at(b);
-						output_seen = !miter_mode;
-						if (GetSize(wire) != 1)
-							symbols[stringf("%c%d", miter_mode ? 'b' : 'o', o)].push_back(stringf("%s[%d]", log_id(wire), i));
-						else
-							symbols[stringf("%c%d", miter_mode ? 'b' : 'o', o)].push_back(stringf("%s", log_id(wire)));
-					}
-
-					//if (init_inputs.count(sig[i])) {
-					//	int a = init_inputs.at(sig[i]);
-					//	log_assert((a & 1) == 0);
-					//	if (GetSize(wire) != 1)
-					//		symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("init:%s[%d]", log_id(wire), i));
-					//	else
-					//		symbols[stringf("i%d", (a >> 1)-1)].push_back(stringf("init:%s", log_id(wire)));
-					//}
-
-					if (ordered_latches.count(sig[i])) {
-						int l = ordered_latches.at(sig[i]);
-						const char *p = (zinit_mode && (aig_latchinit.at(l) == 1)) ? "!" : "";
-						if (GetSize(wire) != 1)
-							symbols[stringf("l%d", l)].push_back(stringf("%s%s[%d]", p, log_id(wire), i));
-						else
-							symbols[stringf("l%d", l)].push_back(stringf("%s%s", p, log_id(wire)));
-					}
-				}
-			}
-
-			if (omode && !output_seen)
-				symbols["o0"].push_back("__dummy_o__");
-
-			symbols.sort();
-
-			for (auto &sym : symbols) {
-				f << sym.first;
-				std::sort(sym.second.begin(), sym.second.end());
-				for (auto &s : sym.second)
-					f << " " << s;
-				f << std::endl;
-			}
-		}
-
 		f << "c";
 
 		if (!box_list.empty() || !ff_bits.empty()) {
-			std::stringstream h_buffer;
-			auto write_h_buffer = [&h_buffer](int i32) {
-				// TODO: Don't assume we're on little endian
-#ifdef _WIN32
-				int i32_be = _byteswap_ulong(i32);
-#else
-				int i32_be = __builtin_bswap32(i32);
-#endif
-				h_buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
+			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));
 			};
-			int num_outputs = output_bits.size();
-			if (omode && num_outputs == 0)
-				num_outputs = 1;
+
+			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 = %zu\n", input_bits.size() + ff_bits.size() + ci_bits.size());
 			write_h_buffer(input_bits.size() + ff_bits.size() + ci_bits.size());
-			log_debug("coNum = %zu\n", num_outputs + ff_bits.size() + co_bits.size());
-			write_h_buffer(num_outputs + ff_bits.size()+ co_bits.size());
+			log_debug("coNum = %zu\n", output_bits.size() + ff_bits.size() + co_bits.size());
+			write_h_buffer(output_bits.size() + ff_bits.size()+ co_bits.size());
 			log_debug("piNum = %zu\n", input_bits.size() + ff_bits.size());
 			write_h_buffer(input_bits.size()+ ff_bits.size());
-			log_debug("poNum = %zu\n", num_outputs + ff_bits.size());
-			write_h_buffer(num_outputs + ff_bits.size());
+			log_debug("poNum = %zu\n", output_bits.size() + ff_bits.size());
+			write_h_buffer(output_bits.size() + ff_bits.size());
 			log_debug("boxNum = %zu\n", box_list.size());
 			write_h_buffer(box_list.size());
 
@@ -869,40 +787,22 @@ struct XAigerWriter
 
 			f << "h";
 			std::string buffer_str = h_buffer.str();
-			// TODO: Don't assume we're on little endian
-#ifdef _WIN32
-			int buffer_size_be = _byteswap_ulong(buffer_str.size());
-#else
-			int buffer_size_be = __builtin_bswap32(buffer_str.size());
-#endif
+			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());
 
 			/*if (!ff_bits.empty())*/ {
 				std::stringstream r_buffer;
-				auto write_r_buffer = [&r_buffer](int i32) {
-					// TODO: Don't assume we're on little endian
-#ifdef _WIN32
-					int i32_be = _byteswap_ulong(i32);
-#else
-					int i32_be = __builtin_bswap32(i32);
-#endif
-					r_buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
-				};
+				auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
 				log_debug("flopNum = %zu\n", ff_bits.size());
 				write_r_buffer(ff_bits.size());
-				int mergeability_class = 1;
-				for (auto cell : ff_bits)
-					write_r_buffer(mergeability_class++);
+				//int mergeability_class = 1;
+				//for (auto cell : ff_bits)
+				//	write_r_buffer(mergeability_class++);
 
 				f << "r";
 				std::string buffer_str = r_buffer.str();
-				// TODO: Don't assume we're on little endian
-#ifdef _WIN32
-				int buffer_size_be = _byteswap_ulong(buffer_str.size());
-#else
-				int buffer_size_be = __builtin_bswap32(buffer_str.size());
-#endif
+				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());
 			}
@@ -923,25 +823,19 @@ struct XAigerWriter
 				Pass::call(holes_module->design, "flatten -wb");
 
 				// TODO: Should techmap all lib_whitebox-es once
-				//Pass::call(holes_module->design, "techmap");
-
+				Pass::call(holes_module->design, "techmap");
 				Pass::call(holes_module->design, "aigmap");
 				Pass::call(holes_module->design, "clean -purge");
 
 				holes_module->design->selection_stack.pop_back();
 
 				std::stringstream a_buffer;
-				XAigerWriter writer(holes_module, false /*zinit_mode*/, false /*imode*/, false /*omode*/, false /*bmode*/, true /* holes_mode */);
-				writer.write_aiger(a_buffer, false /*ascii_mode*/, false /*miter_mode*/, false /*symbols_mode*/, false /*omode*/);
+				XAigerWriter writer(holes_module, false /*zinit_mode*/, true /* holes_mode */);
+				writer.write_aiger(a_buffer, false /*ascii_mode*/);
 
 				f << "a";
 				std::string buffer_str = a_buffer.str();
-				// TODO: Don't assume we're on little endian
-#ifdef _WIN32
-				int buffer_size_be = _byteswap_ulong(buffer_str.size());
-#else
-				int buffer_size_be = __builtin_bswap32(buffer_str.size());
-#endif
+				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());
 				holes_module->design->remove(holes_module);
@@ -951,7 +845,7 @@ struct XAigerWriter
 		f << stringf("Generated by %s\n", yosys_version_str);
 	}
 
-	void write_map(std::ostream &f, bool verbose_map, bool omode)
+	void write_map(std::ostream &f, bool verbose_map)
 	{
 		dict<int, string> input_lines;
 		dict<int, string> init_lines;
@@ -1024,8 +918,6 @@ struct XAigerWriter
 		for (auto &it : output_lines)
 			f << it.second;
 		log_assert(output_lines.size() == output_bits.size());
-		if (omode && output_bits.empty())
-			f << "output " << output_lines.size() << " 0 __dummy_o__\n";
 
 		latch_lines.sort();
 		for (auto &it : latch_lines)
@@ -1055,31 +947,18 @@ struct XAigerBackend : public Backend {
 		log("        convert FFs to zero-initialized FFs, adding additional inputs for\n");
 		log("        uninitialized FFs.\n");
 		log("\n");
-		log("    -symbols\n");
-		log("        include a symbol table in the generated AIGER file\n");
-		log("\n");
 		log("    -map <filename>\n");
 		log("        write an extra file with port and latch symbols\n");
 		log("\n");
 		log("    -vmap <filename>\n");
 		log("        like -map, but more verbose\n");
 		log("\n");
-		log("    -I, -O, -B\n");
-		log("        If the design contains no input/output/assert then create one\n");
-		log("        dummy input/output/bad_state pin to make the tools reading the\n");
-		log("        AIGER file happy.\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 zinit_mode = false;
-		bool miter_mode = false;
-		bool symbols_mode = false;
 		bool verbose_map = false;
-		bool imode = false;
-		bool omode = false;
-		bool bmode = false;
 		std::string map_filename;
 
 		log_header(design, "Executing XAIGER backend.\n");
@@ -1095,10 +974,6 @@ struct XAigerBackend : public Backend {
 				zinit_mode = true;
 				continue;
 			}
-			if (args[argidx] == "-symbols") {
-				symbols_mode = true;
-				continue;
-			}
 			if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) {
 				map_filename = args[++argidx];
 				continue;
@@ -1108,18 +983,6 @@ struct XAigerBackend : public Backend {
 				verbose_map = true;
 				continue;
 			}
-			if (args[argidx] == "-I") {
-				imode = true;
-				continue;
-			}
-			if (args[argidx] == "-O") {
-				omode = true;
-				continue;
-			}
-			if (args[argidx] == "-B") {
-				bmode = true;
-				continue;
-			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
@@ -1129,15 +992,15 @@ struct XAigerBackend : public Backend {
 		if (top_module == nullptr)
 			log_error("Can't find top module in current design!\n");
 
-		XAigerWriter writer(top_module, zinit_mode, imode, omode, bmode);
-		writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode, omode);
+		XAigerWriter writer(top_module, zinit_mode);
+		writer.write_aiger(*f, ascii_mode);
 
 		if (!map_filename.empty()) {
 			std::ofstream mapf;
 			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, omode);
+			writer.write_map(mapf, verbose_map);
 		}
 	}
 } XAigerBackend;
diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index 4c19ec171..d378a07b7 100644
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -2,7 +2,7 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  Copyright (C) 2019  Eddie Hung <eddie@fpgeh.com>
+ *                2019  Eddie Hung <eddie@fpgeh.com>
  *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
@@ -24,17 +24,179 @@
 
 #ifdef _WIN32
 #include <libgen.h>
+#endif
+// https://stackoverflow.com/a/46137633
+#ifdef _MSC_VER
 #include <stdlib.h>
+#define __builtin_bswap32 _byteswap_ulong
+#elif defined(__APPLE__)
+#include <libkern/OSByteOrder.h>
+#define __builtin_bswap32 OSSwapInt32
 #endif
-#include <array>
+#include <inttypes.h>
 
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
-#include "kernel/consteval.h"
+#include "kernel/celltypes.h"
 #include "aigerparse.h"
 
 YOSYS_NAMESPACE_BEGIN
 
+inline int32_t from_big_endian(int32_t i32) {
+#if __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+	return __builtin_bswap32(i32);
+#elif __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
+	return i32;
+#else
+#error "Unknown endianness"
+#endif
+}
+
+struct ConstEvalAig
+{
+	RTLIL::Module *module;
+	dict<RTLIL::SigBit, RTLIL::State> values_map;
+	dict<RTLIL::SigBit, RTLIL::Cell*> sig2driver;
+	dict<SigBit, pool<RTLIL::SigBit>> sig2deps;
+
+	ConstEvalAig(RTLIL::Module *module) : module(module)
+	{
+		for (auto &it : module->cells_) {
+			if (!yosys_celltypes.cell_known(it.second->type))
+				continue;
+			for (auto &it2 : it.second->connections())
+				if (yosys_celltypes.cell_output(it.second->type, it2.first)) {
+					auto r = sig2driver.insert(std::make_pair(it2.second, it.second));
+					log_assert(r.second);
+				}
+		}
+	}
+
+	void clear()
+	{
+		values_map.clear();
+		sig2deps.clear();
+	}
+
+	void set(RTLIL::SigBit sig, RTLIL::State value)
+	{
+		auto it = values_map.find(sig);
+#ifndef NDEBUG
+		if (it != values_map.end()) {
+			RTLIL::State current_val = it->second;
+			log_assert(current_val == value);
+		}
+#endif
+		if (it != values_map.end())
+			it->second = value;
+		else
+			values_map[sig] = value;
+	}
+
+	void set_incremental(RTLIL::SigSpec sig, RTLIL::Const value)
+	{
+		log_assert(GetSize(sig) == GetSize(value));
+
+		for (int i = 0; i < GetSize(sig); i++) {
+			auto it = values_map.find(sig[i]);
+			if (it != values_map.end()) {
+				RTLIL::State current_val = it->second;
+				if (current_val != value[i])
+					for (auto dep : sig2deps[sig[i]])
+						values_map.erase(dep);
+				it->second = value[i];
+			}
+			else
+				values_map[sig[i]] = value[i];
+		}
+	}
+
+	void compute_deps(RTLIL::SigBit output, const pool<RTLIL::SigBit> &inputs)
+	{
+		sig2deps[output].insert(output);
+
+		RTLIL::Cell *cell = sig2driver.at(output);
+		RTLIL::SigBit sig_a = cell->getPort("\\A");
+		sig2deps[sig_a].insert(sig2deps[output].begin(), sig2deps[output].end());
+		if (!inputs.count(sig_a))
+			compute_deps(sig_a, inputs);
+
+		if (cell->type == "$_AND_") {
+			RTLIL::SigSpec sig_b = cell->getPort("\\B");
+			sig2deps[sig_b].insert(sig2deps[output].begin(), sig2deps[output].end());
+			if (!inputs.count(sig_b))
+				compute_deps(sig_b, inputs);
+		}
+		else if (cell->type == "$_NOT_") {
+		}
+		else log_abort();
+	}
+
+	bool eval(RTLIL::Cell *cell)
+	{
+		RTLIL::SigBit sig_y = cell->getPort("\\Y");
+		if (values_map.count(sig_y))
+			return true;
+
+		RTLIL::SigBit sig_a = cell->getPort("\\A");
+		if (!eval(sig_a))
+			return false;
+
+		RTLIL::State eval_ret = RTLIL::Sx;
+		if (cell->type == "$_NOT_") {
+			if (sig_a == RTLIL::S0) eval_ret = RTLIL::S1;
+			else if (sig_a == RTLIL::S1) eval_ret = RTLIL::S0;
+		}
+		else if (cell->type == "$_AND_") {
+			if (sig_a == RTLIL::S0) {
+				eval_ret = RTLIL::S0;
+				goto eval_end;
+			}
+
+			{
+				RTLIL::SigBit sig_b = cell->getPort("\\B");
+				if (!eval(sig_b))
+					return false;
+				if (sig_b == RTLIL::S0) {
+					eval_ret = RTLIL::S0;
+					goto eval_end;
+				}
+
+				if (sig_a != RTLIL::S1 || sig_b != RTLIL::S1)
+					goto eval_end;
+
+				eval_ret = RTLIL::S1;
+			}
+		}
+		else log_abort();
+
+eval_end:
+		set(sig_y, eval_ret);
+		return true;
+	}
+
+	bool eval(RTLIL::SigBit &sig)
+	{
+		auto it = values_map.find(sig);
+		if (it != values_map.end()) {
+			sig = it->second;
+			return true;
+		}
+
+		RTLIL::Cell *cell = sig2driver.at(sig);
+		if (!eval(cell))
+			return false;
+
+		it = values_map.find(sig);
+		if (it != values_map.end()) {
+			sig = it->second;
+			return true;
+		}
+
+		return false;
+	}
+};
+
 AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports)
 	: design(design), f(f), clk_name(clk_name), map_filename(map_filename), wideports(wideports)
 {
@@ -132,20 +294,15 @@ static uint32_t parse_xaiger_literal(std::istream &f)
 	uint32_t l;
 	f.read(reinterpret_cast<char*>(&l), sizeof(l));
 	if (f.gcount() != sizeof(l))
-		log_error("Offset %ld: unable to read literal!\n", static_cast<int64_t>(f.tellg()));
-	// TODO: Don't assume we're on little endian
-#ifdef _WIN32
-	return _byteswap_ulong(l);
-#else
-	return __builtin_bswap32(l);
-#endif
+		log_error("Offset %" PRId64 ": unable to read literal!\n", static_cast<int64_t>(f.tellg()));
+	return from_big_endian(l);
 }
 
 static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned literal)
 {
 	const unsigned variable = literal >> 1;
 	const bool invert = literal & 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" : ""));
 	RTLIL::Wire *wire = module->wire(wire_name);
 	if (wire) return wire;
 	log_debug("Creating %s\n", wire_name.c_str());
@@ -164,7 +321,7 @@ static RTLIL::Wire* createWireIfNotExists(RTLIL::Module *module, unsigned litera
 	}
 
 	log_debug("Creating %s = ~%s\n", wire_name.c_str(), wire_inv_name.c_str());
-	module->addNotGate(stringf("\\__%d__$not", variable), wire_inv, wire); // FIXME: is "$not" the right suffix?
+	module->addNotGate(stringf("\\__%d__$not", variable), wire_inv, wire);
 
 	return wire;
 }
@@ -210,7 +367,8 @@ void AigerReader::parse_xaiger()
 		auto it = m->attributes.find("\\abc_box_id");
 		if (it == m->attributes.end())
 			continue;
-		if (m->name[0] == '$') continue;
+		if (m->name.begins_with("$paramod"))
+			continue;
 		auto r = box_lookup.insert(std::make_pair(it->second.as_int(), m->name));
 		log_assert(r.second);
 	}
@@ -234,7 +392,7 @@ void AigerReader::parse_xaiger()
 				uint32_t lutNum = parse_xaiger_literal(f);
 				uint32_t lutSize = parse_xaiger_literal(f);
 				log_debug("m: dataSize=%u lutNum=%u lutSize=%u\n", dataSize, lutNum, lutSize);
-				ConstEval ce(module);
+				ConstEvalAig ce(module);
 				for (unsigned i = 0; i < lutNum; ++i) {
 					uint32_t rootNodeID = parse_xaiger_literal(f);
 					uint32_t cutLeavesM = parse_xaiger_literal(f);
@@ -249,14 +407,18 @@ void AigerReader::parse_xaiger()
 						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) {
-						ce.push();
-						ce.set(input_sig, RTLIL::Const{j, static_cast<int>(cutLeavesM)});
-						RTLIL::SigSpec o(output_sig);
-						ce.eval(o);
-						lut_mask[j] = o.as_const()[0];
-						ce.pop();
+						int gray = j ^ (j >> 1);
+						ce.set_incremental(input_sig, RTLIL::Const{gray, static_cast<int>(cutLeavesM)});
+						RTLIL::SigBit o(output_sig);
+						bool success = 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);
@@ -346,7 +508,7 @@ void AigerReader::parse_aiger_ascii()
 		if (!(f >> l1 >> l2))
 			log_error("Line %u cannot be interpreted as a latch!\n", line_count);
 		log_debug("%d %d is a latch\n", l1, l2);
-		log_assert(!(l1 & 1)); // TODO: Latch outputs can't be inverted?
+		log_assert(!(l1 & 1));
 		RTLIL::Wire *q_wire = createWireIfNotExists(module, l1);
 		RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
 
@@ -696,10 +858,6 @@ void AigerReader::post_process()
 				RTLIL::Wire* wire = outputs[variable + co_count];
 				log_assert(wire);
 				log_assert(wire->port_output);
-				if (escaped_s.in("\\__dummy_o__", "\\__const0__", "\\__const1__")) {
-					wire->port_output = false;
-					continue;
-				}
 
 				if (index == 0) {
 					// Cope with the fact that a CO might be identical
@@ -797,8 +955,6 @@ void AigerReader::post_process()
 				port_output = port_output || other_wire->port_output;
 			}
 		}
-		if ((port_input && port_output) || (!port_input && !port_output))
-			continue;
 
 		wire = module->addWire(name, width);
 		wire->port_input = port_input;
diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h
index 7d6d70b2c..de3c3efbc 100644
--- a/frontends/aiger/aigerparse.h
+++ b/frontends/aiger/aigerparse.h
@@ -2,7 +2,7 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *                      Eddie Hung <eddie@fpgeh.com>
+ *                2019  Eddie Hung <eddie@fpgeh.com>
  *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index d3ad57d72..f4fcf5dcf 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -276,6 +276,12 @@ namespace RTLIL
 				return std::string(c_str() + pos, len);
 		}
 
+		bool begins_with(const char* prefix) const {
+			size_t len = strlen(prefix);
+			if (size() < len) return false;
+			return substr(0, len) == prefix;
+		}
+
 		bool ends_with(const char* suffix) const {
 			size_t len = strlen(suffix);
 			if (size() < len) return false;
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index c42f7fcdd..d22685b62 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -339,9 +339,6 @@ struct StatPass : public Pass {
 				if (mod->get_bool_attribute("\\top"))
 					top_mod = mod;
 
-			if (mod->attributes.count("\\abc_box_id"))
-				continue;
-
 			statdata_t data(design, mod, width_mode, cell_area, techname);
 			mod_stat[mod->name] = data;
 
diff --git a/passes/opt/Makefile.inc b/passes/opt/Makefile.inc
index ea3646330..337fee9e4 100644
--- a/passes/opt/Makefile.inc
+++ b/passes/opt/Makefile.inc
@@ -14,6 +14,5 @@ OBJS += passes/opt/opt_demorgan.o
 OBJS += passes/opt/rmports.o
 OBJS += passes/opt/opt_lut.o
 OBJS += passes/opt/pmux2shiftx.o
-OBJS += passes/opt/muxpack.o
 endif
 
diff --git a/passes/opt/muxpack.cc b/passes/opt/muxpack.cc
deleted file mode 100644
index 8c4db4e4d..000000000
--- a/passes/opt/muxpack.cc
+++ /dev/null
@@ -1,270 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *                2019  Eddie Hung    <eddie@fpgeh.com>
- *
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include "kernel/yosys.h"
-#include "kernel/sigtools.h"
-
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-
-struct MuxpackWorker
-{
-	Module *module;
-	SigMap sigmap;
-
-	int mux_count, pmux_count;
-
-	pool<Cell*> remove_cells;
-
-	dict<SigSpec, Cell*> sig_chain_next;
-	dict<SigSpec, Cell*> sig_chain_prev;
-	pool<SigBit> sigbit_with_non_chain_users;
-	pool<Cell*> chain_start_cells;
-	pool<Cell*> candidate_cells;
-
-	void make_sig_chain_next_prev()
-	{
-		for (auto wire : module->wires())
-		{
-			if (wire->port_output || wire->get_bool_attribute("\\keep")) {
-				for (auto bit : sigmap(wire))
-					sigbit_with_non_chain_users.insert(bit);
-			}
-		}
-
-		for (auto cell : module->cells())
-		{
-			if (cell->type.in("$mux", "$pmux") && !cell->get_bool_attribute("\\keep"))
-			{
-				SigSpec a_sig = sigmap(cell->getPort("\\A"));
-				SigSpec b_sig;
-				if (cell->type == "$mux")
-					b_sig = sigmap(cell->getPort("\\B"));
-				SigSpec y_sig = sigmap(cell->getPort("\\Y"));
-   
-				if (sig_chain_next.count(a_sig))
-					for (auto a_bit : a_sig.bits())
-						sigbit_with_non_chain_users.insert(a_bit);
-				else {
-					sig_chain_next[a_sig] = cell;
-					candidate_cells.insert(cell);
-				}
-
-				if (!b_sig.empty()) {
-					if (sig_chain_next.count(b_sig))
-						for (auto b_bit : b_sig.bits())
-							sigbit_with_non_chain_users.insert(b_bit);
-					else {
-						sig_chain_next[b_sig] = cell;
-						candidate_cells.insert(cell);
-					}
-				}
-
-				sig_chain_prev[y_sig] = cell;
-				continue;
-			}
-
-			for (auto conn : cell->connections())
-				if (cell->input(conn.first))
-					for (auto bit : sigmap(conn.second))
-						sigbit_with_non_chain_users.insert(bit);
-		}
-	}
-
-	void find_chain_start_cells()
-	{
-		for (auto cell : candidate_cells)
-		{
-			log_debug("Considering %s (%s)\n", log_id(cell), log_id(cell->type));
-
-			SigSpec a_sig = cell->getPort("\\A");
-			if (cell->type == "$mux") {
-				SigSpec b_sig = cell->getPort("\\B");
-				if (sig_chain_prev.count(a_sig) + sig_chain_prev.count(b_sig) != 1)
-					goto start_cell;
-
-				if (!sig_chain_prev.count(a_sig))
-					a_sig = b_sig;
-			}
-			else if (cell->type == "$pmux") {
-				if (!sig_chain_prev.count(a_sig))
-					goto start_cell;
-			}
-			else log_abort();
-
-			{
-				for (auto bit : a_sig.bits())
-					if (sigbit_with_non_chain_users.count(bit))
-						goto start_cell;
-
-				Cell *c1 = sig_chain_prev.at(a_sig);
-				Cell *c2 = cell;
-
-				if (c1->getParam("\\WIDTH") != c2->getParam("\\WIDTH"))
-					goto start_cell;
-			}
-
-			continue;
-
-		start_cell:
-			chain_start_cells.insert(cell);
-		}
-	}
-
-	vector<Cell*> create_chain(Cell *start_cell)
-	{
-		vector<Cell*> chain;
-
-		Cell *c = start_cell;
-		while (c != nullptr)
-		{
-			chain.push_back(c);
-
-			SigSpec y_sig = sigmap(c->getPort("\\Y"));
-
-			if (sig_chain_next.count(y_sig) == 0)
-				break;
-
-			c = sig_chain_next.at(y_sig);
-			if (chain_start_cells.count(c) != 0)
-				break;
-		}
-
-		return chain;
-	}
-
-	void process_chain(vector<Cell*> &chain)
-	{
-		if (GetSize(chain) < 2)
-			return;
-
-		int cursor = 0;
-		while (cursor < GetSize(chain))
-		{
-			int cases = GetSize(chain) - cursor;
-
-			Cell *first_cell = chain[cursor];
-			dict<int, SigBit> taps_dict;
-
-			if (cases < 2) {
-				cursor++;
-				continue;
-			}
-
-			Cell *last_cell = chain[cursor+cases-1];
-
-			log("Converting %s.%s ... %s.%s to a pmux with %d cases.\n",
-				log_id(module), log_id(first_cell), log_id(module), log_id(last_cell), cases);
-
-			mux_count += cases;
-			pmux_count += 1;
-
-			first_cell->type = "$pmux";
-			SigSpec b_sig = first_cell->getPort("\\B");
-			SigSpec s_sig = first_cell->getPort("\\S");
-
-			for (int i = 1; i < cases; i++) {
-				Cell* prev_cell = chain[cursor+i-1];
-				Cell* cursor_cell = chain[cursor+i];
-				if (sigmap(prev_cell->getPort("\\Y")) == sigmap(cursor_cell->getPort("\\A"))) {
-					b_sig.append(cursor_cell->getPort("\\B"));
-					s_sig.append(cursor_cell->getPort("\\S"));
-				}
-				else {
-					b_sig.append(cursor_cell->getPort("\\A"));
-					s_sig.append(module->LogicNot(NEW_ID, cursor_cell->getPort("\\S")));
-				}
-				remove_cells.insert(cursor_cell);
-			}
-
-			first_cell->setPort("\\B", b_sig);
-			first_cell->setPort("\\S", s_sig);
-			first_cell->setParam("\\S_WIDTH", GetSize(s_sig));
-			first_cell->setPort("\\Y", last_cell->getPort("\\Y"));
-
-			cursor += cases;
-		}
-	}
-
-	void cleanup()
-	{
-		for (auto cell : remove_cells)
-			module->remove(cell);
-
-		remove_cells.clear();
-		sig_chain_next.clear();
-		sig_chain_prev.clear();
-		chain_start_cells.clear();
-		candidate_cells.clear();
-	}
-
-	MuxpackWorker(Module *module) :
-			module(module), sigmap(module), mux_count(0), pmux_count(0)
-	{
-		make_sig_chain_next_prev();
-		find_chain_start_cells();
-
-		for (auto c : chain_start_cells) {
-			vector<Cell*> chain = create_chain(c);
-			process_chain(chain);
-		}
-
-		cleanup();
-	}
-};
-
-struct MuxpackPass : public Pass {
-	MuxpackPass() : Pass("muxpack", "$mux/$pmux cascades to $pmux") { }
-	void help() YS_OVERRIDE
-	{
-		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
-		log("\n");
-		log("    muxpack [selection]\n");
-		log("\n");
-		log("This pass converts cascaded chains of $pmux cells (e.g. those create from case\n");
-		log("constructs) and $mux cells (e.g. those created by if-else constructs) into \n");
-		log("into $pmux cells.\n");
-		log("\n");
-	}
-	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
-	{
-		log_header(design, "Executing MUXPACK pass ($mux cell cascades to $pmux).\n");
-
-		size_t argidx;
-		for (argidx = 1; argidx < args.size(); argidx++)
-		{
-			break;
-		}
-		extra_args(args, argidx, design);
-
-		int mux_count = 0;
-		int pmux_count = 0;
-
-		for (auto module : design->selected_modules()) {
-			MuxpackWorker worker(module);
-			mux_count += worker.mux_count;
-			pmux_count += worker.pmux_count;
-		}
-
-		log("Converted %d (p)mux cells into %d pmux cells.\n", mux_count, pmux_count);
-	}
-} MuxpackPass;
-
-PRIVATE_NAMESPACE_END
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 5b19d84fb..15e79f9d1 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -1453,7 +1453,7 @@ struct AbcPass : 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 the load that into ABC externally if\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("\n");
 		log("[1] http://www.eecs.berkeley.edu/~alanmi/abc/\n");
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index fef977eb8..fe199f886 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -2,7 +2,7 @@
  *  yosys -- Yosys Open SYnthesis Suite
  *
  *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *  Copyright (C) 2019  Eddie Hung <eddie@fpgeh.com>
+ *                2019  Eddie Hung <eddie@fpgeh.com>
  *
  *  Permission to use, copy, modify, and/or distribute this software for any
  *  purpose with or without fee is hereby granted, provided that the above
@@ -22,18 +22,18 @@
 // Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification
 // http://www.eecs.berkeley.edu/~alanmi/abc/
 
-#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
-#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p"
-//#define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2"
-#define ABC_COMMAND_LUT "&st; &sweep; &scorr; "/*"&dc2; */"&retime; &dch -f; &ps -l; &if {W} -v; &ps -l"
-#define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P}"
-#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
+#if 0
+// Based on &flow3 - better QoR but more experimental
+#define ABC_COMMAND_LUT "&st; &ps -l; "/*"&sweep -v;"*/" &scorr; " \
+						"&st; &if {W}; &save; &st; &syn2; &if {W}; &save; &load; "\
+						"&st; &if -g -K 6; &dch -f; &if {W}; &save; &load; "\
+						"&st; &if -g -K 6; &synch2; &if {W}; &save; &load"
+#else
+#define ABC_COMMAND_LUT "&st; &sweep; &scorr; "/*"&dc2; "*/"&retime; &dch -f; &ps -l; &if {W} {D} -v; "/*"&mfs; "*/"&ps -l"
+#endif
 
-#define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}"
-#define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
-#define ABC_FAST_COMMAND_LUT "&st; &retime; &if"
-#define ABC_FAST_COMMAND_SOP "strash; dretime; cover -I {I} -P {P}"
-#define ABC_FAST_COMMAND_DFL "strash; dretime; map"
+
+#define ABC_FAST_COMMAND_LUT "&st; &retime; &if {W}"
 
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -61,17 +61,12 @@ extern "C" int Abc_RealMain(int argc, char *argv[]);
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-bool map_mux4;
-bool map_mux8;
-bool map_mux16;
-
 bool markgroups;
 int map_autoidx;
 SigMap assign_map;
 RTLIL::Module *module;
 std::map<RTLIL::SigBit, int> signal_map;
 std::map<RTLIL::SigBit, RTLIL::State> signal_init;
-pool<std::string> enabled_gates;
 bool recover_init;
 
 bool clk_polarity, en_polarity;
@@ -246,32 +241,9 @@ struct abc_output_filter
 	}
 };
 
-static std::pair<RTLIL::IdString, int> wideports_split(std::string name)
-{
-	int pos = -1;
-
-	if (name.empty() || name.back() != ']')
-		goto failed;
-
-	for (int i = 0; i+1 < GetSize(name); i++) {
-		if (name[i] == '[')
-			pos = i;
-		else if (name[i] < '0' || name[i] > '9')
-			pos = -1;
-		else if (i == pos+1 && name[i] == '0' && name[i+1] != ']')
-			pos = -1;
-	}
-
-	if (pos >= 0)
-		return std::pair<RTLIL::IdString, int>(RTLIL::escape_id(name.substr(0, pos)), atoi(name.c_str() + pos+1));
-
-failed:
-	return std::pair<RTLIL::IdString, int>(name, 0);
-}
-
 void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
-		std::string liberty_file, std::string constr_file, bool cleanup, vector<int> lut_costs, bool dff_mode, std::string clk_str,
-		bool keepff, std::string delay_target, std::string sop_inputs, std::string sop_products, std::string lutin_shared, bool fast_mode,
+		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,
 		const std::vector<RTLIL::Cell*> &cells, bool show_tempdir, bool sop_mode, std::string box_file, std::string lut_file,
 		std::string wire_delay)
 {
@@ -325,11 +297,6 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 
 	std::string abc_script;
 
-	if (!liberty_file.empty()) {
-		abc_script += stringf("read_lib -w %s; ", liberty_file.c_str());
-		if (!constr_file.empty())
-			abc_script += stringf("read_constr -v %s; ", constr_file.c_str());
-	} else
 	if (!lut_costs.empty()) {
 		abc_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str());
 		if (!box_file.empty())
@@ -342,7 +309,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 			abc_script += stringf("read_box -v %s; ", box_file.c_str());
 	}
 	else
-		abc_script += stringf("read_library %s/stdcells.genlib; ", tempdir_name.c_str());
+		log_abort();
 
 	abc_script += stringf("&read %s/input.xaig; &ps; ", tempdir_name.c_str());
 
@@ -365,28 +332,18 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		abc_script += fast_mode ? ABC_FAST_COMMAND_LUT : ABC_COMMAND_LUT;
 		//if (all_luts_cost_same && !fast_mode)
 		//	abc_script += "; lutpack {S}";
-	} else if (!liberty_file.empty())
-		abc_script += constr_file.empty() ? (fast_mode ? ABC_FAST_COMMAND_LIB : ABC_COMMAND_LIB) : (fast_mode ? ABC_FAST_COMMAND_CTR : ABC_COMMAND_CTR);
-	else if (sop_mode)
-		abc_script += fast_mode ? ABC_FAST_COMMAND_SOP : ABC_COMMAND_SOP;
-	else
-		abc_script += fast_mode ? ABC_FAST_COMMAND_DFL : ABC_COMMAND_DFL;
+	} else
+		log_abort();
 
-	if (script_file.empty() && !delay_target.empty())
-		for (size_t pos = abc_script.find("dretime;"); pos != std::string::npos; pos = abc_script.find("dretime;", pos+1))
-			abc_script = abc_script.substr(0, pos) + "dretime; retime -o {D};" + abc_script.substr(pos+8);
+	//if (script_file.empty() && !delay_target.empty())
+	//	for (size_t pos = abc_script.find("dretime;"); pos != std::string::npos; pos = abc_script.find("dretime;", pos+1))
+	//		abc_script = abc_script.substr(0, pos) + "dretime; retime -o {D};" + abc_script.substr(pos+8);
 
 	for (size_t pos = abc_script.find("{D}"); pos != std::string::npos; pos = abc_script.find("{D}", pos))
 		abc_script = abc_script.substr(0, pos) + delay_target + abc_script.substr(pos+3);
 
-	for (size_t pos = abc_script.find("{I}"); pos != std::string::npos; pos = abc_script.find("{D}", pos))
-		abc_script = abc_script.substr(0, pos) + sop_inputs + abc_script.substr(pos+3);
-
-	for (size_t pos = abc_script.find("{P}"); pos != std::string::npos; pos = abc_script.find("{D}", pos))
-		abc_script = abc_script.substr(0, pos) + sop_products + abc_script.substr(pos+3);
-
-	for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
-		abc_script = abc_script.substr(0, pos) + lutin_shared + abc_script.substr(pos+3);
+	//for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
+	//	abc_script = abc_script.substr(0, pos) + lutin_shared + abc_script.substr(pos+3);
 
 	for (size_t pos = abc_script.find("{W}"); pos != std::string::npos; pos = abc_script.find("{W}", pos))
 		abc_script = abc_script.substr(0, pos) + wire_delay + abc_script.substr(pos+3);
@@ -414,64 +371,77 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		}
 	}
 
-	design->selection_stack.emplace_back(false);
-	RTLIL::Selection& sel = design->selection_stack.back();
-	sel.select(module);
+	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;
+		}
+	}
 
-	// Behave as for "abc" where BLIF writer implicitly outputs all undef as zero
-	Pass::call(design, "setundef -zero");
+	log_push();
 
-	Pass::call(design, "aigmap");
+	if (count_output)
+	{
+		design->selection_stack.emplace_back(false);
+		RTLIL::Selection& sel = design->selection_stack.back();
+		sel.select(module);
 
-	handle_loops(design);
+		// Behave as for "abc" where BLIF writer implicitly outputs all undef as zero
+		Pass::call(design, "setundef -zero");
 
-	Pass::call(design, stringf("write_xaiger -O -map %s/input.sym %s/input.xaig; ", tempdir_name.c_str(), tempdir_name.c_str()));
+		Pass::call(design, "aigmap");
 
-#if 0
-	std::string buffer = stringf("%s/%s", tempdir_name.c_str(), "input.xaig");
-	std::ifstream ifs;
-	ifs.open(buffer);
-	if (ifs.fail())
-		log_error("Can't open ABC output file `%s'.\n", buffer.c_str());
-	buffer = stringf("%s/%s", tempdir_name.c_str(), "input.sym");
-	log_assert(!design->module("$__abc9__"));
-	AigerReader reader(design, ifs, "$__abc9__", "" /* clk_name */, buffer.c_str() /* map_filename */, false /* wideports */);
-	reader.parse_xaiger();
-	ifs.close();
-	Pass::call(design, stringf("write_verilog -noexpr -norename %s/%s", tempdir_name.c_str(), "input.v"));
-	design->remove(design->module("$__abc9__"));
-#endif
+		handle_loops(design);
 
-	design->selection_stack.pop_back();
+		//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()));
 
-	// Now 'unexpose' those wires by undoing
-	// the expose operation -- remove them from PO/PI
-	// and re-connecting them back together
-	for (auto wire : module->wires()) {
-		auto it = wire->attributes.find("\\abc_scc_break");
-		if (it != wire->attributes.end()) {
-			wire->attributes.erase(it);
-			log_assert(wire->port_output);
-			wire->port_output = false;
-			RTLIL::Wire *i_wire = module->wire(wire->name.str() + ".abci");
-			log_assert(i_wire);
-			log_assert(i_wire->port_input);
-			i_wire->port_input = false;
-			module->connect(i_wire, wire);
+		std::string buffer;
+		std::ifstream ifs;
+#if 0
+		buffer = stringf("%s/%s", tempdir_name.c_str(), "input.xaig");
+		ifs.open(buffer);
+		if (ifs.fail())
+			log_error("Can't open ABC output file `%s'.\n", buffer.c_str());
+		buffer = stringf("%s/%s", tempdir_name.c_str(), "input.sym");
+		log_assert(!design->module("$__abc9__"));
+		{
+			AigerReader reader(design, ifs, "$__abc9__", "" /* clk_name */, buffer.c_str() /* map_filename */, true /* wideports */);
+			reader.parse_xaiger();
 		}
-	}
-	module->fixup_ports();
+		ifs.close();
+		Pass::call(design, stringf("write_verilog -noexpr -norename %s/%s", tempdir_name.c_str(), "input.v"));
+		design->remove(design->module("$__abc9__"));
+#endif
 
-	//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);
+		design->selection_stack.pop_back();
+
+		// Now 'unexpose' those wires by undoing
+		// the expose operation -- remove them from PO/PI
+		// and re-connecting them back together
+		for (auto wire : module->wires()) {
+			auto it = wire->attributes.find("\\abc_scc_break");
+			if (it != wire->attributes.end()) {
+				wire->attributes.erase(it);
+				log_assert(wire->port_output);
+				wire->port_output = false;
+				RTLIL::Wire *i_wire = module->wire(wire->name.str() + ".abci");
+				log_assert(i_wire);
+				log_assert(i_wire->port_input);
+				i_wire->port_input = false;
+				module->connect(i_wire, wire);
+			}
+		}
+		module->fixup_ports();
 
-	log_push();
 
-	//if (count_output > 0)
-	{
 		log_header(design, "Executing ABC9.\n");
 
-        std::string buffer;
 		if (!lut_costs.empty()) {
 			buffer = stringf("%s/lutdefs.txt", tempdir_name.c_str());
 			f = fopen(buffer.c_str(), "wt");
@@ -507,16 +477,13 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 			log_error("ABC: execution of command \"%s\" failed: return code %d.\n", buffer.c_str(), ret);
 
 		buffer = stringf("%s/%s", tempdir_name.c_str(), "output.aig");
-		std::ifstream ifs;
 		ifs.open(buffer);
 		if (ifs.fail())
 			log_error("Can't open ABC output file `%s'.\n", buffer.c_str());
 
-		bool builtin_lib = liberty_file.empty();
-		//parse_blif(mapped_design, ifs, builtin_lib ? "\\DFF" : "\\_dff_", false, sop_mode);
 		buffer = stringf("%s/%s", tempdir_name.c_str(), "input.sym");
 		log_assert(!design->module("$__abc9__"));
-		AigerReader reader(design, ifs, "$__abc9__", "" /* clk_name */, buffer.c_str() /* map_filename */, false /* wideports */);
+		AigerReader reader(design, ifs, "$__abc9__", "" /* clk_name */, buffer.c_str() /* map_filename */, true /* wideports */);
 		reader.parse_xaiger();
 		ifs.close();
 
@@ -536,21 +503,9 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 			if (markgroups) remap_wire->attributes["\\abcgroup"] = map_autoidx;
 			if (w->port_output) {
 				RTLIL::Wire *wire = module->wire(w->name);
-				if (wire) {
-					for (int i = 0; i < GetSize(wire); i++)
-						output_bits.insert({wire, i});
-				}
-				else {
-					// Attempt another wideports_split here because there
-					// exists the possibility that different bits of a port
-					// could be an input and output, therefore parse_xaiger()
-					// could not combine it into a wideport
-					auto r = wideports_split(w->name.str());
-					wire = module->wire(r.first);
-					log_assert(wire);
-					int i = r.second;
+				log_assert(wire);
+				for (int i = 0; i < GetSize(wire); i++)
 					output_bits.insert({wire, i});
-				}
 			}
 		}
 
@@ -584,66 +539,65 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 		std::map<std::string, int> cell_stats;
 		for (auto c : mapped_mod->cells())
 		{
-			if (builtin_lib)
-			{
-				if (c->type == "$_NOT_") {
-					RTLIL::Cell *cell;
-					RTLIL::SigBit a_bit = c->getPort("\\A").as_bit();
-					RTLIL::SigBit y_bit = c->getPort("\\Y").as_bit();
-					if (!a_bit.wire) {
-						c->setPort("\\Y", module->addWire(NEW_ID));
-						module->connect(module->wires_[remap_name(y_bit.wire->name)], RTLIL::S1);
+			if (c->type == "$_NOT_") {
+				RTLIL::Cell *cell;
+				RTLIL::SigBit a_bit = c->getPort("\\A").as_bit();
+				RTLIL::SigBit y_bit = c->getPort("\\Y").as_bit();
+				if (!a_bit.wire) {
+					c->setPort("\\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), RTLIL::S1);
+				}
+				else if (!lut_costs.empty() || !lut_file.empty()) {
+					RTLIL::Cell* driving_lut = nullptr;
+					// ABC can return NOT gates that drive POs
+					if (!a_bit.wire->port_input) {
+						// If it's not a NOT gate that that comes from a PI directly,
+						// find the driving LUT and clone that to guarantee that we won't
+						// increase the max logic depth
+						// (TODO: Optimise by not cloning unless will increase depth)
+						RTLIL::IdString driver_name;
+						if (GetSize(a_bit.wire) == 1)
+							driver_name = stringf("%s$lut", a_bit.wire->name.c_str());
+						else
+							driver_name = stringf("%s[%d]$lut", a_bit.wire->name.c_str(), a_bit.offset);
+						driving_lut = mapped_mod->cell(driver_name);
 					}
-					else if (!lut_costs.empty() || !lut_file.empty()) {
-						RTLIL::Cell* driving_lut = nullptr;
-						// ABC can return NOT gates that drive POs
-						if (!a_bit.wire->port_input) {
-							// If it's not a NOT gate that that comes from a PI directly,
-							// find the driving LUT and clone that to guarantee that we won't
-							// increase the max logic depth
-							// (TODO: Optimise by not cloning unless will increase depth)
-							RTLIL::IdString driver_name;
-							if (GetSize(a_bit.wire) == 1)
-								driver_name = stringf("%s$lut", a_bit.wire->name.c_str());
-							else
-								driver_name = stringf("%s[%d]$lut", a_bit.wire->name.c_str(), a_bit.offset);
-							driving_lut = mapped_mod->cell(driver_name);
-						}
 
-						if (!driving_lut) {
-							// If a driver couldn't be found (could be from PI,
-							// or from a box) then implement using a LUT
-							cell = module->addLut(remap_name(stringf("%s$lut", c->name.c_str())),
-									RTLIL::SigBit(module->wires_[remap_name(a_bit.wire->name)], a_bit.offset),
-									RTLIL::SigBit(module->wires_[remap_name(y_bit.wire->name)], y_bit.offset),
-									1);
-						}
-						else {
-							auto driver_a = driving_lut->getPort("\\A").chunks();
-							for (auto &chunk : driver_a)
-								chunk.wire = module->wires_[remap_name(chunk.wire->name)];
-							RTLIL::Const driver_lut = driving_lut->getParam("\\LUT");
-							for (auto &b : driver_lut.bits) {
-								if (b == RTLIL::State::S0) b = RTLIL::State::S1;
-								else if (b == RTLIL::State::S1) b = RTLIL::State::S0;
-							}
-							cell = module->addLut(remap_name(stringf("%s$lut", c->name.c_str())),
-									driver_a,
-									RTLIL::SigBit(module->wires_[remap_name(y_bit.wire->name)], y_bit.offset),
-									driver_lut);
-						}
+					if (!driving_lut) {
+						// If a driver couldn't be found (could be from PI,
+						// or from a box) then implement using a LUT
+						cell = module->addLut(remap_name(stringf("%s$lut", c->name.c_str())),
+								RTLIL::SigBit(module->wires_[remap_name(a_bit.wire->name)], a_bit.offset),
+								RTLIL::SigBit(module->wires_[remap_name(y_bit.wire->name)], y_bit.offset),
+								1);
 					}
 					else {
-						cell = module->addCell(remap_name(c->name), "$_NOT_");
-						cell->setPort("\\A", RTLIL::SigBit(module->wires_[remap_name(a_bit.wire->name)], a_bit.offset));
-						cell->setPort("\\Y", RTLIL::SigBit(module->wires_[remap_name(y_bit.wire->name)], y_bit.offset));
-						cell_stats[RTLIL::unescape_id(c->type)]++;
+						auto driver_a = driving_lut->getPort("\\A").chunks();
+						for (auto &chunk : driver_a)
+							chunk.wire = module->wires_[remap_name(chunk.wire->name)];
+						RTLIL::Const driver_lut = driving_lut->getParam("\\LUT");
+						for (auto &b : driver_lut.bits) {
+							if (b == RTLIL::State::S0) b = RTLIL::State::S1;
+							else if (b == RTLIL::State::S1) b = RTLIL::State::S0;
+						}
+						cell = module->addLut(remap_name(stringf("%s$lut", c->name.c_str())),
+								driver_a,
+								RTLIL::SigBit(module->wires_[remap_name(y_bit.wire->name)], y_bit.offset),
+								driver_lut);
 					}
-					if (markgroups) cell->attributes["\\abcgroup"] = map_autoidx;
-					continue;
 				}
+				else {
+					cell = module->addCell(remap_name(c->name), "$_NOT_");
+					cell->setPort("\\A", RTLIL::SigBit(module->wires_[remap_name(a_bit.wire->name)], a_bit.offset));
+					cell->setPort("\\Y", RTLIL::SigBit(module->wires_[remap_name(y_bit.wire->name)], y_bit.offset));
+					cell_stats[RTLIL::unescape_id(c->type)]++;
+				}
+				if (markgroups) cell->attributes["\\abcgroup"] = map_autoidx;
+				continue;
 			}
-            cell_stats[RTLIL::unescape_id(c->type)]++;
+			cell_stats[RTLIL::unescape_id(c->type)]++;
 
 			if (c->type == "$lut") {
 				if (GetSize(c->getPort("\\A")) == 1 && c->getParam("\\LUT").as_int() == 2) {
@@ -654,10 +608,10 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 				}
 			}
 			else {
-                auto it = erased_boxes.find(c->name);
-                log_assert(it != erased_boxes.end());
-                c->parameters = std::move(it->second);
-            }
+				auto it = erased_boxes.find(c->name);
+				log_assert(it != erased_boxes.end());
+				c->parameters = std::move(it->second);
+			}
 
 			RTLIL::Cell* cell = module->addCell(remap_name(c->name), c->type);
 			if (markgroups) cell->attributes["\\abcgroup"] = map_autoidx;
@@ -713,22 +667,9 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 			if (!w->port_input && !w->port_output)
 				continue;
 			RTLIL::Wire *wire = module->wire(w->name);
+			log_assert(wire);
 			RTLIL::Wire *remap_wire = module->wire(remap_name(w->name));
-			RTLIL::SigSpec signal;
-			if (wire) {
-				signal = RTLIL::SigSpec(wire, 0, GetSize(remap_wire));
-			}
-			else {
-				// Attempt another wideports_split here because there
-				// exists the possibility that different bits of a port
-				// could be an input and output, therefore parse_xaiger()
-				// could not combine it into a wideport
-				auto r = wideports_split(w->name.str());
-				wire = module->wire(r.first);
-				log_assert(wire);
-				int i = r.second;
-				signal = RTLIL::SigSpec(wire, i);
-			}
+			RTLIL::SigSpec signal = RTLIL::SigSpec(wire, 0, GetSize(remap_wire));
 			log_assert(GetSize(signal) >= GetSize(remap_wire));
 
 			log_assert(w->port_input || w->port_output);
@@ -753,10 +694,10 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 
 		design->remove(mapped_mod);
 	}
-	//else
-	//{
-	//	log("Don't call ABC as there is nothing to map.\n");
-	//}
+	else
+	{
+		log("Don't call ABC as there is nothing to map.\n");
+	}
 
 	if (cleanup)
 	{
@@ -768,7 +709,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 }
 
 struct Abc9Pass : public Pass {
-	Abc9Pass() : Pass("abc9", "use ABC for technology mapping") { }
+	Abc9Pass() : Pass("abc9", "use ABC9 for technology mapping") { }
 	void help() YS_OVERRIDE
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -796,76 +737,30 @@ struct Abc9Pass : public Pass {
 		log("\n");
 		log("        if no -script parameter is given, the following scripts are used:\n");
 		log("\n");
-		log("        for -liberty without -constr:\n");
-		log("%s\n", fold_abc_cmd(ABC_COMMAND_LIB).c_str());
-		log("\n");
-		log("        for -liberty with -constr:\n");
-		log("%s\n", fold_abc_cmd(ABC_COMMAND_CTR).c_str());
-		log("\n");
 		log("        for -lut/-luts (only one LUT size):\n");
-		log("%s\n", fold_abc_cmd(ABC_COMMAND_LUT "; lutpack {S}").c_str());
+		log("%s\n", fold_abc_cmd(ABC_COMMAND_LUT /*"; lutpack {S}"*/).c_str());
 		log("\n");
 		log("        for -lut/-luts (different LUT sizes):\n");
 		log("%s\n", fold_abc_cmd(ABC_COMMAND_LUT).c_str());
 		log("\n");
-		log("        for -sop:\n");
-		log("%s\n", fold_abc_cmd(ABC_COMMAND_SOP).c_str());
-		log("\n");
-		log("        otherwise:\n");
-		log("%s\n", fold_abc_cmd(ABC_COMMAND_DFL).c_str());
-		log("\n");
 		log("    -fast\n");
 		log("        use different default scripts that are slightly faster (at the cost\n");
 		log("        of output quality):\n");
 		log("\n");
-		log("        for -liberty without -constr:\n");
-		log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_LIB).c_str());
-		log("\n");
-		log("        for -liberty with -constr:\n");
-		log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_CTR).c_str());
-		log("\n");
 		log("        for -lut/-luts:\n");
 		log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_LUT).c_str());
 		log("\n");
-		log("        for -sop:\n");
-		log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_SOP).c_str());
-		log("\n");
-		log("        otherwise:\n");
-		log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_DFL).c_str());
-		log("\n");
-		log("    -liberty <file>\n");
-		log("        generate netlists for the specified cell library (using the liberty\n");
-		log("        file format).\n");
-		log("\n");
-		log("    -constr <file>\n");
-		log("        pass this file with timing constraints to ABC. Use with -liberty.\n");
-		log("\n");
-		log("        a constr file contains two lines:\n");
-		log("            set_driving_cell <cell_name>\n");
-		log("            set_load <floating_point_number>\n");
-		log("\n");
-		log("        the set_driving_cell statement defines which cell type is assumed to\n");
-		log("        drive the primary inputs and the set_load statement sets the load in\n");
-		log("        femtofarads for each primary output.\n");
-		log("\n");
 		log("    -D <picoseconds>\n");
 		log("        set delay target. the string {D} in the default scripts above is\n");
-		log("        replaced by this option when used, and an empty string otherwise.\n");
-		log("        this also replaces 'dretime' with 'dretime; retime -o {D}' in the\n");
-		log("        default scripts above.\n");
-		log("\n");
-		log("    -I <num>\n");
-		log("        maximum number of SOP inputs.\n");
-		log("        (replaces {I} in the default scripts above)\n");
-		log("\n");
-		log("    -P <num>\n");
-		log("        maximum number of SOP products.\n");
-		log("        (replaces {P} in the default scripts above)\n");
-		log("\n");
-		log("    -S <num>\n");
-		log("        maximum number of LUT inputs shared.\n");
-		log("        (replaces {S} in the default scripts above, default: -S 1)\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");
+//		log("        (replaces {S} in the default scripts above, default: -S 1)\n");
+//		log("\n");
 		log("    -lut <width>\n");
 		log("        generate netlist using luts of (max) the specified width.\n");
 		log("\n");
@@ -882,42 +777,19 @@ 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("    -sop\n");
-		log("        map to sum-of-product cells and inverters\n");
-		log("\n");
-		// log("    -mux4, -mux8, -mux16\n");
-		// log("        try to extract 4-input, 8-input, and/or 16-input muxes\n");
-		// log("        (ignored when used with -liberty or -lut)\n");
-		// log("\n");
-		log("    -g type1,type2,...\n");
-		log("        Map to the specified list of gate types. Supported gates types are:\n");
-		log("        AND, NAND, OR, NOR, XOR, XNOR, ANDNOT, ORNOT, MUX, AOI3, OAI3, AOI4, OAI4.\n");
-		log("        (The NOT gate is always added to this list automatically.)\n");
-		log("\n");
-		log("        The following aliases can be used to reference common sets of gate types:\n");
-		log("          simple: AND OR XOR MUX\n");
-		log("          cmos2: NAND NOR\n");
-		log("          cmos3: NAND NOR AOI3 OAI3\n");
-		log("          cmos4: NAND NOR AOI3 OAI3 AOI4 OAI4\n");
-		log("          gates: AND NAND OR NOR XOR XNOR ANDNOT ORNOT\n");
-		log("          aig: AND NAND OR NOR ANDNOT ORNOT\n");
-		log("\n");
-		log("        Prefix a gate type with a '-' to remove it from the list. For example\n");
-		log("        the arguments 'AND,OR,XOR' and 'simple,-MUX' are equivalent.\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 $_DFF_?_ and $_DFFE_??_ cells through ABC. modules with many\n");
+//		log("        clock domains are automatically partitioned in clock domains and each\n");
+//		log("        domain is passed through ABC independently.\n");
+//		log("\n");
+//		log("    -clk [!]<clock-signal-name>[,[!]<enable-signal-name>]\n");
+//		log("        use only the specified clock domain. this is like -dff, but only FF\n");
+//		log("        cells that belong to the specified clock domain are used.\n");
+//		log("\n");
+//		log("    -keepff\n");
+//		log("        set the \"keep\" attribute on flip-flop output wires. (and thus preserve\n");
+//		log("        them, for example for equivalence checking.)\n");
+//		log("\n");
 		log("    -nocleanup\n");
 		log("        when this option is used, the temporary files created by this pass\n");
 		log("        are not removed. this is useful for debugging.\n");
@@ -934,14 +806,11 @@ struct Abc9Pass : public Pass {
 		log("    -box <file>\n");
 		log("        pass this file with box library to ABC. Use with -lut.\n");
 		log("\n");
-		log("When neither -liberty nor -lut is used, the Yosys standard cell library is\n");
-		log("loaded into ABC before the ABC script is executed.\n");
-		log("\n");
 		log("Note that this is a logic optimization pass within Yosys that is calling ABC\n");
 		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 the load that into ABC externally if\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("\n");
 		log("[1] http://www.eecs.berkeley.edu/~alanmi/abc/\n");
@@ -949,7 +818,7 @@ struct Abc9Pass : public Pass {
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
-		log_header(design, "Executing ABC9 pass (technology mapping using ABC).\n");
+		log_header(design, "Executing ABC9 pass (technology mapping using ABC9).\n");
 		log_push();
 
 		assign_map.clear();
@@ -963,8 +832,8 @@ struct Abc9Pass : public Pass {
 #else
 		std::string exe_file = proc_self_dirname() + "yosys-abc";
 #endif
-		std::string script_file, liberty_file, constr_file, clk_str, box_file, lut_file;
-		std::string delay_target, sop_inputs, sop_products, lutin_shared = "-S 1", wire_delay;
+		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 show_tempdir = false, sop_mode = false;
 		vector<int> lut_costs;
@@ -975,11 +844,6 @@ struct Abc9Pass : public Pass {
 		show_tempdir = true;
 #endif
 
-		map_mux4 = false;
-		map_mux8 = false;
-		map_mux16 = false;
-		enabled_gates.clear();
-
 #ifdef _WIN32
 #ifndef ABCEXTERNAL
 		if (!check_file_exists(exe_file + ".exe") && check_file_exists(proc_self_dirname() + "..\\yosys-abc.exe"))
@@ -1006,36 +870,14 @@ struct Abc9Pass : public Pass {
 					script_file = std::string(pwd) + "/" + script_file;
 				continue;
 			}
-			if (arg == "-liberty" && argidx+1 < args.size()) {
-				liberty_file = args[++argidx];
-				rewrite_filename(liberty_file);
-				if (!liberty_file.empty() && !is_absolute_path(liberty_file))
-					liberty_file = std::string(pwd) + "/" + liberty_file;
-				continue;
-			}
-			if (arg == "-constr" && argidx+1 < args.size()) {
-				constr_file = args[++argidx];
-				rewrite_filename(constr_file);
-				if (!constr_file.empty() && !is_absolute_path(constr_file))
-					constr_file = std::string(pwd) + "/" + constr_file;
-				continue;
-			}
 			if (arg == "-D" && argidx+1 < args.size()) {
 				delay_target = "-D " + args[++argidx];
 				continue;
 			}
-			if (arg == "-I" && argidx+1 < args.size()) {
-				sop_inputs = "-I " + args[++argidx];
-				continue;
-			}
-			if (arg == "-P" && argidx+1 < args.size()) {
-				sop_products = "-P " + args[++argidx];
-				continue;
-			}
-			if (arg == "-S" && argidx+1 < args.size()) {
-				lutin_shared = "-S " + args[++argidx];
-				continue;
-			}
+			//if (arg == "-S" && argidx+1 < args.size()) {
+			//	lutin_shared = "-S " + args[++argidx];
+			//	continue;
+			//}
 			if (arg == "-lut" && argidx+1 < args.size()) {
 				string arg = args[++argidx];
 				size_t pos = arg.find_first_of(':');
@@ -1079,126 +921,23 @@ struct Abc9Pass : public Pass {
 				}
 				continue;
 			}
-			if (arg == "-sop") {
-				sop_mode = true;
-				continue;
-			}
-			if (arg == "-mux4") {
-				map_mux4 = true;
-				continue;
-			}
-			if (arg == "-mux8") {
-				map_mux8 = true;
-				continue;
-			}
-			if (arg == "-mux16") {
-				map_mux16 = true;
-				continue;
-			}
-			if (arg == "-dress") {
-				// TODO
-				//abc_dress = true;
-				continue;
-			}
-			if (arg == "-g" && argidx+1 < args.size()) {
-				for (auto g : split_tokens(args[++argidx], ",")) {
-					vector<string> gate_list;
-					bool remove_gates = false;
-					if (GetSize(g) > 0 && g[0] == '-') {
-						remove_gates = true;
-						g = g.substr(1);
-					}
-					if (g == "AND") goto ok_gate;
-					if (g == "NAND") goto ok_gate;
-					if (g == "OR") goto ok_gate;
-					if (g == "NOR") goto ok_gate;
-					if (g == "XOR") goto ok_gate;
-					if (g == "XNOR") goto ok_gate;
-					if (g == "ANDNOT") goto ok_gate;
-					if (g == "ORNOT") goto ok_gate;
-					if (g == "MUX") goto ok_gate;
-					if (g == "AOI3") goto ok_gate;
-					if (g == "OAI3") goto ok_gate;
-					if (g == "AOI4") goto ok_gate;
-					if (g == "OAI4") goto ok_gate;
-					if (g == "simple") {
-						gate_list.push_back("AND");
-						gate_list.push_back("OR");
-						gate_list.push_back("XOR");
-						gate_list.push_back("MUX");
-						goto ok_alias;
-					}
-					if (g == "cmos2") {
-						gate_list.push_back("NAND");
-						gate_list.push_back("NOR");
-						goto ok_alias;
-					}
-					if (g == "cmos3") {
-						gate_list.push_back("NAND");
-						gate_list.push_back("NOR");
-						gate_list.push_back("AOI3");
-						gate_list.push_back("OAI3");
-						goto ok_alias;
-					}
-					if (g == "cmos4") {
-						gate_list.push_back("NAND");
-						gate_list.push_back("NOR");
-						gate_list.push_back("AOI3");
-						gate_list.push_back("OAI3");
-						gate_list.push_back("AOI4");
-						gate_list.push_back("OAI4");
-						goto ok_alias;
-					}
-					if (g == "gates") {
-						gate_list.push_back("AND");
-						gate_list.push_back("NAND");
-						gate_list.push_back("OR");
-						gate_list.push_back("NOR");
-						gate_list.push_back("XOR");
-						gate_list.push_back("XNOR");
-						gate_list.push_back("ANDNOT");
-						gate_list.push_back("ORNOT");
-						goto ok_alias;
-					}
-					if (g == "aig") {
-						gate_list.push_back("AND");
-						gate_list.push_back("NAND");
-						gate_list.push_back("OR");
-						gate_list.push_back("NOR");
-						gate_list.push_back("ANDNOT");
-						gate_list.push_back("ORNOT");
-						goto ok_alias;
-					}
-					cmd_error(args, argidx, stringf("Unsupported gate type: %s", g.c_str()));
-				ok_gate:
-					gate_list.push_back(g);
-				ok_alias:
-					for (auto gate : gate_list) {
-						if (remove_gates)
-							enabled_gates.erase(gate);
-						else
-							enabled_gates.insert(gate);
-					}
-				}
-				continue;
-			}
 			if (arg == "-fast") {
 				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 == "-clk" && argidx+1 < args.size()) {
+			//	clk_str = args[++argidx];
+			//	dff_mode = true;
+			//	continue;
+			//}
+			//if (arg == "-keepff") {
+			//	keepff = true;
+			//	continue;
+			//}
 			if (arg == "-nocleanup") {
 				cleanup = false;
 				continue;
@@ -1226,11 +965,6 @@ struct Abc9Pass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
-		if ((!lut_costs.empty() || !lut_file.empty()) && !liberty_file.empty())
-			log_cmd_error("Got -lut and -liberty! This two options are exclusive.\n");
-		if (!constr_file.empty() && liberty_file.empty())
-			log_cmd_error("Got -constr but no -liberty!\n");
-
 		for (auto mod : design->selected_modules())
 		{
 			if (mod->attributes.count("\\abc_box_id"))
@@ -1262,8 +996,8 @@ struct Abc9Pass : public Pass {
 				}
 
 			if (!dff_mode || !clk_str.empty()) {
-				abc9_module(design, mod, script_file, exe_file, liberty_file, constr_file, cleanup, lut_costs, dff_mode, clk_str, keepff,
-						delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, mod->selected_cells(), show_tempdir, sop_mode,
+				abc9_module(design, mod, script_file, exe_file, cleanup, lut_costs, dff_mode, clk_str, keepff,
+						delay_target, lutin_shared, fast_mode, mod->selected_cells(), show_tempdir, sop_mode,
 						box_file, lut_file, wire_delay);
 				continue;
 			}
@@ -1408,8 +1142,8 @@ struct Abc9Pass : public Pass {
 				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, liberty_file, constr_file, cleanup, lut_costs, !clk_sig.empty(), "$",
-						keepff, delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, it.second, show_tempdir, sop_mode,
+				abc9_module(design, mod, script_file, exe_file, cleanup, lut_costs, !clk_sig.empty(), "$",
+						keepff, delay_target, lutin_shared, fast_mode, it.second, show_tempdir, sop_mode,
 						box_file, lut_file, wire_delay);
 				assign_map.set(mod);
 			}
diff --git a/passes/techmap/shregmap.cc b/passes/techmap/shregmap.cc
index 46f6a79fb..21dfe9619 100644
--- a/passes/techmap/shregmap.cc
+++ b/passes/techmap/shregmap.cc
@@ -293,13 +293,10 @@ struct ShregmapWorker
 
 				if (opts.init || sigbit_init.count(q_bit) == 0)
 				{
-					auto r = sigbit_chain_next.insert(std::make_pair(d_bit, cell));
-					if (!r.second) {
+					if (sigbit_chain_next.count(d_bit)) {
 						sigbit_with_non_chain_users.insert(d_bit);
-						Wire *wire = module->addWire(NEW_ID);
-						module->connect(wire, d_bit);
-						sigbit_chain_next.insert(std::make_pair(wire, cell));
-					}
+					} else
+						sigbit_chain_next[d_bit] = cell;
 
 					sigbit_chain_prev[q_bit] = cell;
 					continue;
diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc
index ee2e86de9..555de9fba 100644
--- a/techlibs/common/synth.cc
+++ b/techlibs/common/synth.cc
@@ -76,7 +76,7 @@ struct SynthPass : public ScriptPass
 		log("        synonymous to the end of the command list.\n");
 		log("\n");
 		log("    -abc9\n");
-		log("        use abc9 instead of abc\n");
+		log("        use new ABC9 flow (EXPERIMENTAL)\n");
 		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
@@ -174,6 +174,9 @@ struct SynthPass : public ScriptPass
 		if (!design->full_selection())
 			log_cmd_error("This command only operates on fully selected designs!\n");
 
+		if (abc == "abc9" && !lut)
+			log_cmd_error("ABC9 flow only supported for FPGA synthesis (using '-lut' option)");
+
 		log_header(design, "Executing SYNTH pass.\n");
 		log_push();
 
diff --git a/techlibs/ecp5/Makefile.inc b/techlibs/ecp5/Makefile.inc
index 4db087e87..eee3b418f 100644
--- a/techlibs/ecp5/Makefile.inc
+++ b/techlibs/ecp5/Makefile.inc
@@ -11,6 +11,9 @@ $(eval $(call add_share_file,share/ecp5,techlibs/ecp5/bram.txt))
 $(eval $(call add_share_file,share/ecp5,techlibs/ecp5/arith_map.v))
 $(eval $(call add_share_file,share/ecp5,techlibs/ecp5/latches_map.v))
 
+$(eval $(call add_share_file,share/ecp5,techlibs/ecp5/abc_5g.box))
+$(eval $(call add_share_file,share/ecp5,techlibs/ecp5/abc_5g.lut))
+
 EXTRA_OBJS += techlibs/ecp5/brams_init.mk techlibs/ecp5/brams_connect.mk
 .SECONDARY: techlibs/ecp5/brams_init.mk techlibs/ecp5/brams_connect.mk
 
diff --git a/techlibs/ecp5/abc_5g.box b/techlibs/ecp5/abc_5g.box
new file mode 100644
index 000000000..72af6d9cb
--- /dev/null
+++ b/techlibs/ecp5/abc_5g.box
@@ -0,0 +1,36 @@
+# Box 1 : CCU2C (2xCARRY + 2xLUT4)
+# Outputs: S0, S1, COUT
+# 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
+
+# Box 2 : TRELLIS_DPR16X4 (16x4 dist ram)
+# Outputs: DO0, DO1, DO2, DO3, DO4
+# name            ID  w/b   ins   outs
+TRELLIS_DPR16X4   2     0   14    4
+
+#DI0   DI1   DI2   DI3   RAD0   RAD1   RAD2   RAD3   WAD0    WAD1   WAD2   WAD3  WCK   WRE
+-      -     -     -     141    379    275    379    -       -      -      -     -     -
+-      -     -     -     141    379    275    379    -       -      -      -     -     -
+-      -     -     -     141    379    275    379    -       -      -      -     -     -
+-      -     -     -     141    379    275    379    -       -      -      -     -     -
+
+# Box 3 : PFUMX (MUX2)
+# Outputs: Z
+# name  ID   w/b   ins    outs
+PFUMX   3    1     3      1
+
+#ALUT  BLUT  C0
+98     98    151
+
+# Box 4 : L6MUX21 (MUX2)
+# Outputs: Z
+# name   ID   w/b   ins    outs
+L6MUX21  4    1     3      1
+
+#D0    D1    SD
+140    141   148
diff --git a/techlibs/ecp5/abc_5g.lut b/techlibs/ecp5/abc_5g.lut
new file mode 100644
index 000000000..e8aa9b35d
--- /dev/null
+++ b/techlibs/ecp5/abc_5g.lut
@@ -0,0 +1,25 @@
+# ECP5-5G LUT library for ABC
+# Note that ECP5 architecture assigns difference
+# in LUT input delay to interconnect, so this is
+# considered too
+
+
+# Simple LUTs
+#  area  D    C    B    A
+1  1     141
+2  1     141  275
+3  1     141  275  379
+4  1     141  275  379  379
+
+# LUT5 = 2x LUT4 + PFUMX
+#  area  M0   D    C    B    A
+5  2     151  239  373  477  477
+
+# LUT6 = 2x LUT5 + MUX2
+#  area  M1   M0   D    C    B    A
+6  4     148  292  380  514  618  618
+
+# LUT7 = 2x LUT6 + MUX2
+#  area  M2   M1   M0   D    C    B    A
+7  8     148  289  433  521  655  759  759
+
diff --git a/techlibs/ecp5/cells_map.v b/techlibs/ecp5/cells_map.v
index f6c71a03d..53a89e8a3 100644
--- a/techlibs/ecp5/cells_map.v
+++ b/techlibs/ecp5/cells_map.v
@@ -70,80 +70,107 @@ module \$lut (A, Y);
     parameter WIDTH = 0;
     parameter LUT = 0;
 
+
+    // Need to swap input ordering, and fix init accordingly,
+    // to match ABC's expectation of LUT inputs in non-decreasing
+    // delay order
+    localparam P_WIDTH = WIDTH < 4 ? 4 : WIDTH;
+    function [P_WIDTH-1:0] permute_index;
+        input [P_WIDTH-1:0] i;
+        integer j;
+        begin
+            permute_index = 0;
+            for (j = 0; j < P_WIDTH; j = j + 1)
+                permute_index[P_WIDTH-1 - j] = i[j];
+        end
+    endfunction
+
+    function [2**P_WIDTH-1:0] permute_init;
+        input [2**P_WIDTH-1:0] orig;
+        integer i;
+        begin
+            permute_init = 0;
+            for (i = 0; i < 2**P_WIDTH; i = i + 1)
+                permute_init[i] = orig[permute_index(i)];
+        end
+    endfunction
+
+    parameter [2**P_WIDTH-1:0] P_LUT = permute_init(LUT);
+
     input [WIDTH-1:0] A;
     output Y;
 
     generate
         if (WIDTH == 1) begin
-            LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.Z(Y),
-                .A(A[0]), .B(1'b0), .C(1'b0), .D(1'b0));
+            LUT4 #(.INIT(P_LUT)) _TECHMAP_REPLACE_ (.Z(Y),
+                .A(1'b0), .B(1'b0), .C(1'b0), .D(A[0]));
         end else
         if (WIDTH == 2) begin
-            LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.Z(Y),
-                .A(A[0]), .B(A[1]), .C(1'b0), .D(1'b0));
+            LUT4 #(.INIT(P_LUT)) _TECHMAP_REPLACE_ (.Z(Y),
+                .A(1'b0), .B(1'b0), .C(A[1]), .D(A[0]));
         end else
         if (WIDTH == 3) begin
-            LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.Z(Y),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(1'b0));
+            LUT4 #(.INIT(P_LUT)) _TECHMAP_REPLACE_ (.Z(Y),
+                .A(1'b0), .B(A[2]), .C(A[1]), .D(A[0]));
         end else
         if (WIDTH == 4) begin
-            LUT4 #(.INIT(LUT)) _TECHMAP_REPLACE_ (.Z(Y),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
+            LUT4 #(.INIT(P_LUT)) _TECHMAP_REPLACE_ (.Z(Y),
+                .A(A[3]), .B(A[2]), .C(A[1]), .D(A[0]));
         `ifndef NO_PFUMUX
         end else
         if (WIDTH == 5) begin
             wire f0, f1;
-            LUT4 #(.INIT(LUT[15: 0])) lut0 (.Z(f0),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[31:16])) lut1 (.Z(f1),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            PFUMX mux5(.ALUT(f1), .BLUT(f0), .C0(A[4]), .Z(Y));
+            LUT4 #(.INIT(P_LUT[15: 0])) lut0 (.Z(f0),
+                .A(A[4]), .B(A[3]), .C(A[2]), .D(A[1]));
+            LUT4 #(.INIT(P_LUT[31:16])) lut1 (.Z(f1),
+                .A(A[4]), .B(A[3]), .C(A[2]), .D(A[1]));
+            PFUMX mux5(.ALUT(f1), .BLUT(f0), .C0(A[0]), .Z(Y));
         end else
         if (WIDTH == 6) begin
             wire f0, f1, f2, f3, g0, g1;
-            LUT4 #(.INIT(LUT[15: 0])) lut0 (.Z(f0),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[31:16])) lut1 (.Z(f1),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-
-            LUT4 #(.INIT(LUT[47:32])) lut2 (.Z(f2),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[63:48])) lut3 (.Z(f3),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-
-            PFUMX mux50(.ALUT(f1), .BLUT(f0), .C0(A[4]), .Z(g0));
-            PFUMX mux51(.ALUT(f3), .BLUT(f2), .C0(A[4]), .Z(g1));
-            L6MUX21 mux6 (.D0(g0), .D1(g1), .SD(A[5]), .Z(Y));
+            LUT4 #(.INIT(P_LUT[15: 0])) lut0 (.Z(f0),
+                .A(A[5]), .B(A[4]), .C(A[3]), .D(A[2]));
+            LUT4 #(.INIT(P_LUT[31:16])) lut1 (.Z(f1),
+                .A(A[5]), .B(A[4]), .C(A[3]), .D(A[2]));
+
+            LUT4 #(.INIT(P_LUT[47:32])) lut2 (.Z(f2),
+                .A(A[5]), .B(A[4]), .C(A[3]), .D(A[2]));
+            LUT4 #(.INIT(P_LUT[63:48])) lut3 (.Z(f3),
+                .A(A[5]), .B(A[4]), .C(A[3]), .D(A[2]));
+
+            PFUMX mux50(.ALUT(f1), .BLUT(f0), .C0(A[1]), .Z(g0));
+            PFUMX mux51(.ALUT(f3), .BLUT(f2), .C0(A[1]), .Z(g1));
+            L6MUX21 mux6 (.D0(g0), .D1(g1), .SD(A[0]), .Z(Y));
         end else
         if (WIDTH == 7) begin
             wire f0, f1, f2, f3, f4, f5, f6, f7, g0, g1, g2, g3, h0, h1;
-            LUT4 #(.INIT(LUT[15: 0])) lut0 (.Z(f0),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[31:16])) lut1 (.Z(f1),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-
-            LUT4 #(.INIT(LUT[47:32])) lut2 (.Z(f2),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[63:48])) lut3 (.Z(f3),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-
-            LUT4 #(.INIT(LUT[79:64])) lut4 (.Z(f4),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[95:80])) lut5 (.Z(f5),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-
-            LUT4 #(.INIT(LUT[111: 96])) lut6 (.Z(f6),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-            LUT4 #(.INIT(LUT[127:112])) lut7 (.Z(f7),
-                .A(A[0]), .B(A[1]), .C(A[2]), .D(A[3]));
-
-            PFUMX mux50(.ALUT(f1), .BLUT(f0), .C0(A[4]), .Z(g0));
-            PFUMX mux51(.ALUT(f3), .BLUT(f2), .C0(A[4]), .Z(g1));
-            PFUMX mux52(.ALUT(f5), .BLUT(f4), .C0(A[4]), .Z(g2));
-            PFUMX mux53(.ALUT(f7), .BLUT(f6), .C0(A[4]), .Z(g3));
-            L6MUX21 mux60 (.D0(g0), .D1(g1), .SD(A[5]), .Z(h0));
-            L6MUX21 mux61 (.D0(g2), .D1(g3), .SD(A[5]), .Z(h1));
-            L6MUX21 mux7  (.D0(h0), .D1(h1), .SD(A[6]), .Z(Y));
+            LUT4 #(.INIT(P_LUT[15: 0])) lut0 (.Z(f0),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+            LUT4 #(.INIT(P_LUT[31:16])) lut1 (.Z(f1),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+
+            LUT4 #(.INIT(P_LUT[47:32])) lut2 (.Z(f2),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+            LUT4 #(.INIT(P_LUT[63:48])) lut3 (.Z(f3),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+
+            LUT4 #(.INIT(P_LUT[79:64])) lut4 (.Z(f4),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+            LUT4 #(.INIT(P_LUT[95:80])) lut5 (.Z(f5),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+
+            LUT4 #(.INIT(P_LUT[111: 96])) lut6 (.Z(f6),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+            LUT4 #(.INIT(P_LUT[127:112])) lut7 (.Z(f7),
+                .A(A[6]), .B(A[5]), .C(A[4]), .D(A[3]));
+
+            PFUMX mux50(.ALUT(f1), .BLUT(f0), .C0(A[2]), .Z(g0));
+            PFUMX mux51(.ALUT(f3), .BLUT(f2), .C0(A[2]), .Z(g1));
+            PFUMX mux52(.ALUT(f5), .BLUT(f4), .C0(A[2]), .Z(g2));
+            PFUMX mux53(.ALUT(f7), .BLUT(f6), .C0(A[2]), .Z(g3));
+            L6MUX21 mux60 (.D0(g0), .D1(g1), .SD(A[1]), .Z(h0));
+            L6MUX21 mux61 (.D0(g2), .D1(g3), .SD(A[1]), .Z(h1));
+            L6MUX21 mux7  (.D0(h0), .D1(h1), .SD(A[0]), .Z(Y));
         `endif
         end else begin
             wire _TECHMAP_FAIL_ = 1;
diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v
index 1e4002ee0..f66147323 100644
--- a/techlibs/ecp5/cells_sim.v
+++ b/techlibs/ecp5/cells_sim.v
@@ -9,15 +9,17 @@ module LUT4(input A, B, C, D, output Z);
 endmodule
 
 // ---------------------------------------
-
+(* abc_box_id=4, lib_whitebox *)
 module L6MUX21 (input D0, D1, SD, output Z);
 	assign Z = SD ? D1 : D0;
 endmodule
 
 // ---------------------------------------
-
-module CCU2C(input CIN, A0, B0, C0, D0, A1, B1, C1, D1,
-	           output S0, S1, COUT);
+(* abc_box_id=1, abc_carry, lib_whitebox *)
+module CCU2C((* abc_carry_in *) input CIN,
+			   input A0, B0, C0, D0, A1, B1, C1, D1,
+	           output S0, S1,
+	         (* abc_carry_out *) output COUT);
 
 	parameter [15:0] INIT0 = 16'h0000;
 	parameter [15:0] INIT1 = 16'h0000;
@@ -26,9 +28,13 @@ module CCU2C(input CIN, A0, B0, C0, D0, A1, B1, C1, D1,
 
 	// First half
 	wire LUT4_0, LUT2_0;
+`ifdef _ABC
+	assign LUT4_0 = INIT0[{D0, C0, B0, A0}];
+	assign LUT2_0 = INIT0[{2'b00, B0, A0}];
+`else
 	LUT4 #(.INIT(INIT0)) lut4_0(.A(A0), .B(B0), .C(C0), .D(D0), .Z(LUT4_0));
 	LUT2 #(.INIT(INIT0[3:0])) lut2_0(.A(A0), .B(B0), .Z(LUT2_0));
-
+`endif
 	wire gated_cin_0 = (INJECT1_0 == "YES") ? 1'b0 : CIN;
 	assign S0 = LUT4_0 ^ gated_cin_0;
 
@@ -37,9 +43,13 @@ module CCU2C(input CIN, A0, B0, C0, D0, A1, B1, C1, D1,
 
 	// Second half
 	wire LUT4_1, LUT2_1;
+`ifdef _ABC
+	assign LUT4_1 = INIT1[{D1, C1, B1, A1}];
+	assign LUT2_1 = INIT1[{2'b00, B1, A1}];
+`else
 	LUT4 #(.INIT(INIT1)) lut4_1(.A(A1), .B(B1), .C(C1), .D(D1), .Z(LUT4_1));
 	LUT2 #(.INIT(INIT1[3:0])) lut2_1(.A(A1), .B(B1), .Z(LUT2_1));
-
+`endif
 	wire gated_cin_1 = (INJECT1_1 == "YES") ? 1'b0 : cout_0;
 	assign S1 = LUT4_1 ^ gated_cin_1;
 
@@ -90,13 +100,13 @@ module TRELLIS_RAM16X2 (
 endmodule
 
 // ---------------------------------------
-
+(* abc_box_id=3, lib_whitebox *)
 module PFUMX (input ALUT, BLUT, C0, output Z);
 	assign Z = C0 ? ALUT : BLUT;
 endmodule
 
 // ---------------------------------------
-
+//(* abc_box_id=2 *)
 module TRELLIS_DPR16X4 (
 	input [3:0] DI,
 	input [3:0] WAD,
diff --git a/techlibs/ecp5/synth_ecp5.cc b/techlibs/ecp5/synth_ecp5.cc
index c6e12248e..b271500f1 100644
--- a/techlibs/ecp5/synth_ecp5.cc
+++ b/techlibs/ecp5/synth_ecp5.cc
@@ -82,6 +82,9 @@ struct SynthEcp5Pass : public ScriptPass
 		log("    -abc2\n");
 		log("        run two passes of 'abc' for slightly improved logic density\n");
 		log("\n");
+		log("    -abc9\n");
+		log("        use new ABC9 flow (EXPERIMENTAL)\n");
+		log("\n");
 		log("    -vpr\n");
 		log("        generate an output netlist (and BLIF file) suitable for VPR\n");
 		log("        (this feature is experimental and incomplete)\n");
@@ -93,7 +96,7 @@ struct SynthEcp5Pass : public ScriptPass
 	}
 
 	string top_opt, blif_file, edif_file, json_file;
-	bool noccu2, nodffe, nobram, nodram, nomux, flatten, retime, abc2, vpr;
+	bool noccu2, nodffe, nobram, nodram, nomux, flatten, retime, abc2, abc9, vpr;
 
 	void clear_flags() YS_OVERRIDE
 	{
@@ -110,6 +113,7 @@ struct SynthEcp5Pass : public ScriptPass
 		retime = false;
 		abc2 = false;
 		vpr = false;
+		abc9 = false;
 	}
 
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -184,6 +188,10 @@ struct SynthEcp5Pass : public ScriptPass
 				vpr = true;
 				continue;
 			}
+			if (args[argidx] == "-abc9") {
+				abc9 = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -203,7 +211,7 @@ struct SynthEcp5Pass : public ScriptPass
 	{
 		if (check_label("begin"))
 		{
-			run("read_verilog -lib +/ecp5/cells_sim.v +/ecp5/cells_bb.v");
+			run("read_verilog -D_ABC -lib +/ecp5/cells_sim.v +/ecp5/cells_bb.v");
 			run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt.c_str()));
 		}
 
@@ -264,10 +272,15 @@ struct SynthEcp5Pass : public ScriptPass
 				run("abc", "      (only if -abc2)");
 			}
 			run("techmap -map +/ecp5/latches_map.v");
-			if (nomux)
-				run("abc -lut 4 -dress");
-			else
-				run("abc -lut 4:7 -dress");
+			if (abc9) {
+				run("abc9 -lut +/ecp5/abc_5g.lut -box +/ecp5/abc_5g.box -W 200");
+			} else {
+				if (nomux)
+					run("abc -lut 4 -dress");
+				else
+					run("abc -lut 4:7 -dress");
+			}
+
 			run("clean");
 		}
 
diff --git a/techlibs/ice40/abc_lp.box b/techlibs/ice40/abc_lp.box
index dbc98d0c4..eb1cd0937 100644
--- a/techlibs/ice40/abc_lp.box
+++ b/techlibs/ice40/abc_lp.box
@@ -110,4 +110,4 @@ SB_CARRY 21 1 3 1
 # Inputs: I0 I1 I2 I3
 # Outputs: O
 SB_LUT4 22 1 4 1
-465 558 589 661
+661 589 558 465
diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index 523dd8cbe..031afa85c 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -143,8 +143,7 @@ endmodule
 
 // Positive Edge SiliconBlue FF Cells
 
-(* abc_box_id = 1, abc_flop, lib_whitebox *)
-module SB_DFF ((* abc_flop_q *) output `SB_DFF_REG, input C, (* abc_flop_d *) input D);
+module SB_DFF (output `SB_DFF_REG, input C, D);
 `ifndef _ABC
 	always @(posedge C)
 		Q <= D;
@@ -153,15 +152,13 @@ module SB_DFF ((* abc_flop_q *) output `SB_DFF_REG, input C, (* abc_flop_d *) in
 `endif
 endmodule
 
-//(* abc_box_id = 2, abc_flop *)
-module SB_DFFE ((* abc_flop_q *) output `SB_DFF_REG, input C, E, (* abc_flop_d *) input D);
+module SB_DFFE (output `SB_DFF_REG, input C, E, D);
 	always @(posedge C)
 		if (E)
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 3, abc_flop *)
-module SB_DFFSR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d *) input D);
+module SB_DFFSR (output `SB_DFF_REG, input C, R, D);
 	always @(posedge C)
 		if (R)
 			Q <= 0;
@@ -169,8 +166,7 @@ module SB_DFFSR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 4, abc_flop *)
-module SB_DFFR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d *) input D);
+module SB_DFFR (output `SB_DFF_REG, input C, R, D);
 	always @(posedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -178,8 +174,7 @@ module SB_DFFR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d *
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 5, abc_flop *)
-module SB_DFFSS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d *) input D);
+module SB_DFFSS (output `SB_DFF_REG, input C, S, D);
 	always @(posedge C)
 		if (S)
 			Q <= 1;
@@ -187,8 +182,7 @@ module SB_DFFSS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 6, abc_flop *)
-module SB_DFFS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d *) input D);
+module SB_DFFS (output `SB_DFF_REG, input C, S, D);
 	always @(posedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -196,8 +190,7 @@ module SB_DFFS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d *
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 7, abc_flop *)
-module SB_DFFESR ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flop_d *) input D);
+module SB_DFFESR (output `SB_DFF_REG, input C, E, R, D);
 	always @(posedge C)
 		if (E) begin
 			if (R)
@@ -207,8 +200,7 @@ module SB_DFFESR ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flo
 		end
 endmodule
 
-//(* abc_box_id = 8, abc_flop *)
-module SB_DFFER ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flop_d *) input D);
+module SB_DFFER (output `SB_DFF_REG, input C, E, R, D);
 	always @(posedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -216,8 +208,7 @@ module SB_DFFER ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flop
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 9, abc_flop *)
-module SB_DFFESS ((* abc_flop_q *) output `SB_DFF_REG, input C, E, S, (* abc_flop_d *) input D);
+module SB_DFFESS (output `SB_DFF_REG, input C, E, S, D);
 	always @(posedge C)
 		if (E) begin
 			if (S)
@@ -227,8 +218,7 @@ module SB_DFFESS ((* abc_flop_q *) output `SB_DFF_REG, input C, E, S, (* abc_flo
 		end
 endmodule
 
-//(* abc_box_id = 10, abc_flop *)
-module SB_DFFES ((* abc_flop_q *) output `SB_DFF_REG, input C, E, S, (* abc_flop_d *) input D);
+module SB_DFFES (output `SB_DFF_REG, input C, E, S, D);
 	always @(posedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -238,21 +228,18 @@ endmodule
 
 // Negative Edge SiliconBlue FF Cells
 
-//(* abc_box_id = 11, abc_flop *)
-module SB_DFFN ((* abc_flop_q *) output `SB_DFF_REG, input C, (* abc_flop_d *) input D);
+module SB_DFFN (output `SB_DFF_REG, input C, D);
 	always @(negedge C)
 		Q <= D;
 endmodule
 
-//(* abc_box_id = 12, abc_flop *)
-module SB_DFFNE ((* abc_flop_q *) output `SB_DFF_REG, input C, E, (* abc_flop_d *) input D);
+module SB_DFFNE (output `SB_DFF_REG, input C, E, D);
 	always @(negedge C)
 		if (E)
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 13, abc_flop *)
-module SB_DFFNSR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d *) input D);
+module SB_DFFNSR (output `SB_DFF_REG, input C, R, D);
 	always @(negedge C)
 		if (R)
 			Q <= 0;
@@ -260,8 +247,7 @@ module SB_DFFNSR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 14, abc_flop *)
-module SB_DFFNR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d *) input D);
+module SB_DFFNR (output `SB_DFF_REG, input C, R, D);
 	always @(negedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -269,8 +255,7 @@ module SB_DFFNR ((* abc_flop_q *) output `SB_DFF_REG, input C, R, (* abc_flop_d
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 15, abc_flop *)
-module SB_DFFNSS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d *) input D);
+module SB_DFFNSS (output `SB_DFF_REG, input C, S, D);
 	always @(negedge C)
 		if (S)
 			Q <= 1;
@@ -278,8 +263,7 @@ module SB_DFFNSS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 16, abc_flop *)
-module SB_DFFNS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d *) input D);
+module SB_DFFNS (output `SB_DFF_REG, input C, S, D);
 	always @(negedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -287,8 +271,7 @@ module SB_DFFNS ((* abc_flop_q *) output `SB_DFF_REG, input C, S, (* abc_flop_d
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 17, abc_flop *)
-module SB_DFFNESR ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flop_d *) input D);
+module SB_DFFNESR (output `SB_DFF_REG, input C, E, R, D);
 	always @(negedge C)
 		if (E) begin
 			if (R)
@@ -298,8 +281,7 @@ module SB_DFFNESR ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_fl
 		end
 endmodule
 
-//(* abc_box_id = 18, abc_flop *)
-module SB_DFFNER ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flop_d *) input D);
+module SB_DFFNER (output `SB_DFF_REG, input C, E, R, D);
 	always @(negedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -307,8 +289,7 @@ module SB_DFFNER ((* abc_flop_q *) output `SB_DFF_REG, input C, E, R, (* abc_flo
 			Q <= D;
 endmodule
 
-//(* abc_box_id = 19, abc_flop *)
-module SB_DFFNESS ((* abc_flop_q *) output `SB_DFF_REG, input C, E, S, (* abc_flop_d *) input D);
+module SB_DFFNESS (output `SB_DFF_REG, input C, E, S, D);
 	always @(negedge C)
 		if (E) begin
 			if (S)
@@ -318,8 +299,7 @@ module SB_DFFNESS ((* abc_flop_q *) output `SB_DFF_REG, input C, E, S, (* abc_fl
 		end
 endmodule
 
-//(* abc_box_id = 20, abc_flop *)
-module SB_DFFNES ((* abc_flop_q *) output `SB_DFF_REG, input C, E, S, (* abc_flop_d *) input D);
+module SB_DFFNES (output `SB_DFF_REG, input C, E, S, D);
 	always @(negedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -330,7 +310,7 @@ endmodule
 // SiliconBlue RAM Cells
 
 module SB_RAM40_4K (
-	(* abc_flop_q *) output [15:0] RDATA,
+	output [15:0] RDATA,
 	input         RCLK, RCLKE, RE,
 	input  [10:0] RADDR,
 	input         WCLK, WCLKE, WE,
@@ -498,7 +478,7 @@ module SB_RAM40_4K (
 endmodule
 
 module SB_RAM40_4KNR (
-	(* abc_flop_q *) output [15:0] RDATA,
+	output [15:0] RDATA,
 	input         RCLKN, RCLKE, RE,
 	input  [10:0] RADDR,
 	input         WCLK, WCLKE, WE,
@@ -563,7 +543,7 @@ module SB_RAM40_4KNR (
 endmodule
 
 module SB_RAM40_4KNW (
-	(* abc_flop_q *) output [15:0] RDATA,
+	output [15:0] RDATA,
 	input         RCLK, RCLKE, RE,
 	input  [10:0] RADDR,
 	input         WCLKN, WCLKE, WE,
@@ -628,7 +608,7 @@ module SB_RAM40_4KNW (
 endmodule
 
 module SB_RAM40_4KNRNW (
-	(* abc_flop_q *) output [15:0] RDATA,
+	output [15:0] RDATA,
 	input         RCLKN, RCLKE, RE,
 	input  [10:0] RADDR,
 	input         WCLKN, WCLKE, WE,
@@ -922,7 +902,7 @@ module SB_SPRAM256KA (
 	input [15:0] DATAIN,
 	input [3:0] MASKWREN,
 	input WREN, CHIPSELECT, CLOCK, STANDBY, SLEEP, POWEROFF,
-	(* abc_flop_q *) output reg [15:0] DATAOUT
+	output reg [15:0] DATAOUT
 );
 `ifndef BLACKBOX
 `ifndef EQUIV
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index 5afa042b0..d8e9786c5 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -97,7 +97,7 @@ struct SynthIce40Pass : public ScriptPass
 		log("        (this feature is experimental and incomplete)\n");
 		log("\n");
 		log("    -abc9\n");
-		log("        use abc9 instead of abc\n");
+		log("        use new ABC9 flow (EXPERIMENTAL)\n");
 		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
@@ -332,7 +332,7 @@ struct SynthIce40Pass : public ScriptPass
 			}
 			if (!noabc) {
 				if (abc == "abc9")
-					run(abc + stringf(" -dress -lut +/ice40/abc_%s.lut -box +/ice40/abc_%s.box", device_opt.c_str(), device_opt.c_str()), "(skip if -noabc)");
+					run(abc + stringf(" -lut +/ice40/abc_%s.lut -box +/ice40/abc_%s.box", device_opt.c_str(), device_opt.c_str()), "(skip if -noabc)");
 				else
 					run(abc + " -dress -lut 4", "(skip if -noabc)");
 			}
diff --git a/techlibs/xilinx/Makefile.inc b/techlibs/xilinx/Makefile.inc
index 2f3945167..1a652eb27 100644
--- a/techlibs/xilinx/Makefile.inc
+++ b/techlibs/xilinx/Makefile.inc
@@ -30,9 +30,8 @@ $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/drams_map.v))
 $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/arith_map.v))
 $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/ff_map.v))
 $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/lut_map.v))
-$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/mux_map.v))
-$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/abc.box))
-$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/abc.lut))
+$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/abc_xc7.box))
+$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/abc_xc7.lut))
 
 $(eval $(call add_gen_share_file,share/xilinx,techlibs/xilinx/brams_init_36.vh))
 $(eval $(call add_gen_share_file,share/xilinx,techlibs/xilinx/brams_init_32.vh))
diff --git a/techlibs/xilinx/abc.lut b/techlibs/xilinx/abc.lut
deleted file mode 100644
index 3a7dc268d..000000000
--- a/techlibs/xilinx/abc.lut
+++ /dev/null
@@ -1,14 +0,0 @@
-# Max delays from https://github.com/SymbiFlow/prjxray-db/blob/34ea6eb08a63d21ec16264ad37a0a7b142ff6031/artix7/timings/CLBLL_L.sdf
-
-# K	area	delay
-1 	1	124
-2	2	124 235
-3	3	124 235 399
-4	3	124 235 399 490
-5	3	124 235 399 490 620
-6	5	124 235 399 490 620 632
-                # F7BMUX
-7	10	296 420 531 695 756 916 928
-                # F8MUX
-                    # F8MUX+F7BMUX
-8	20	273 569 693 804 968 1029 1189 1201
diff --git a/techlibs/xilinx/abc.box b/techlibs/xilinx/abc_xc7.box
index a4182ed63..8a48bad4e 100644
--- a/techlibs/xilinx/abc.box
+++ b/techlibs/xilinx/abc_xc7.box
@@ -54,9 +54,9 @@ FDSE 7 0 4 1
 # Inputs: C CE CLR D
 # Outputs: Q
 FDCE 8 0 4 1
-- - 404 -
+- - - -
 
 # Inputs: C CE D PRE
 # Outputs: Q
 FDPE 9 0 4 1
-- - - 404
+- - - -
diff --git a/techlibs/xilinx/abc_xc7.lut b/techlibs/xilinx/abc_xc7.lut
new file mode 100644
index 000000000..2e6906945
--- /dev/null
+++ b/techlibs/xilinx/abc_xc7.lut
@@ -0,0 +1,15 @@
+# Max delays from https://github.com/SymbiFlow/prjxray-db/blob/82bf5f158cd8e9a11ac4d04f1aeef48ed1a528a5/artix7/timings/CLBLL_L.sdf
+#            and  https://github.com/SymbiFlow/prjxray-db/blob/82bf5f158cd8e9a11ac4d04f1aeef48ed1a528a5/artix7/tile_type_CLBLL_L.json
+
+# K	area	delay
+1 	1	127
+2	2	127 238
+3	3	127 238 407
+4	3	127 238 407 472
+5	3	127 238 407 472 631
+6	5	127 238 407 472 631 642
+        # F7AMUX + F7BMUX / 2
+7	10	286 413 524 693 758 917 928
+        # F8MUX
+            # F8MUX+F7MUX
+8	20	273 559 686 797 966 1031 1190 1201
diff --git a/techlibs/xilinx/brams_bb.v b/techlibs/xilinx/brams_bb.v
index f540d299d..a682ba4a7 100644
--- a/techlibs/xilinx/brams_bb.v
+++ b/techlibs/xilinx/brams_bb.v
@@ -19,10 +19,10 @@ module RAMB18E1 (
 	input [1:0] WEA,
 	input [3:0] WEBWE,
 
-	(* abc_flop_q *) output [15:0] DOADO,
-	(* abc_flop_q *) output [15:0] DOBDO,
-	(* abc_flop_q *) output [1:0] DOPADOP,
-	(* abc_flop_q *) output [1:0] DOPBDOP
+	output [15:0] DOADO,
+	output [15:0] DOBDO,
+	output [1:0] DOPADOP,
+	output [1:0] DOPBDOP
 );
 	parameter INITP_00 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
 	parameter INITP_01 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
@@ -143,10 +143,10 @@ module RAMB36E1 (
 	input [3:0] WEA,
 	input [7:0] WEBWE,
 
-	(* abc_flop_q *) output [31:0] DOADO,
-	(* abc_flop_q *) output [31:0] DOBDO,
-	(* abc_flop_q *) output [3:0] DOPADOP,
-	(* abc_flop_q *) output [3:0] DOPBDOP
+	output [31:0] DOADO,
+	output [31:0] DOBDO,
+	output [3:0] DOPADOP,
+	output [3:0] DOPBDOP
 );
 	parameter INITP_00 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
 	parameter INITP_01 = 256'h0000000000000000000000000000000000000000000000000000000000000000;
diff --git a/techlibs/xilinx/cells_map.v b/techlibs/xilinx/cells_map.v
index f8f9356bc..b5114758c 100644
--- a/techlibs/xilinx/cells_map.v
+++ b/techlibs/xilinx/cells_map.v
@@ -18,6 +18,18 @@
  *
  */
 
+// Convert negative-polarity reset to positive-polarity
+(* techmap_celltype = "$_DFF_NN0_" *)
+module _90_dff_nn0_to_np0(input D, C, R, output Q); \$_DFF_NP0_  _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule
+(* techmap_celltype = "$_DFF_PN0_" *)
+module _90_dff_pn0_to_pp0(input D, C, R, output Q); \$_DFF_PP0_  _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule
+
+(* techmap_celltype = "$_DFF_NN1_" *)
+module _90_dff_nn1_to_np1 (input D, C, R, output Q); \$_DFF_NP1   _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule
+(* techmap_celltype = "$_DFF_PN1_" *)
+module _90_dff_pn1_to_pp1 (input D, C, R, output Q); \$_DFF_PP1   _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .R(~R)); endmodule
+
+
 module \$__SHREG_ (input C, input D, input E, output Q);
   parameter DEPTH = 0;
   parameter [DEPTH-1:0] INIT = 0;
@@ -142,123 +154,3 @@ module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, o
     end
   endgenerate
 endmodule
-
-module \$__XILINX_SHIFTX (A, B, Y);
-  parameter A_SIGNED = 0;
-  parameter B_SIGNED = 0;
-  parameter A_WIDTH = 1;
-  parameter B_WIDTH = 1;
-  parameter Y_WIDTH = 1;
-
-  input [A_WIDTH-1:0] A;
-  input [B_WIDTH-1:0] B;
-  output [Y_WIDTH-1:0] Y;
-
-  parameter [A_WIDTH-1:0] _TECHMAP_CONSTMSK_A_ = 0;
-  parameter [A_WIDTH-1:0] _TECHMAP_CONSTVAL_A_ = 0;
-  parameter [B_WIDTH-1:0] _TECHMAP_CONSTMSK_B_ = 0;
-  parameter [B_WIDTH-1:0] _TECHMAP_CONSTVAL_B_ = 0;
-
-  function integer compute_num_leading_X_in_A;
-    integer i, c;
-  begin
-    compute_num_leading_X_in_A = 0;
-    c = 1;
-    for (i = A_WIDTH-1; i >= 0; i=i-1) begin
-      if (!_TECHMAP_CONSTMSK_A_[i] || _TECHMAP_CONSTVAL_A_[i] !== 1'bx)
-        c = 0;
-      compute_num_leading_X_in_A = compute_num_leading_X_in_A + c;
-    end
-  end
-  endfunction
-  localparam num_leading_X_in_A = compute_num_leading_X_in_A();
-
-  generate
-    genvar i, j;
-    // Bit-blast
-    if (Y_WIDTH > 1) begin
-      for (i = 0; i < Y_WIDTH; i++)
-        \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(A_WIDTH-Y_WIDTH+1), .B_WIDTH(B_WIDTH), .Y_WIDTH(1'd1)) bitblast (.A(A[A_WIDTH-Y_WIDTH+i:i]), .B(B), .Y(Y[i]));
-    end
-    // If the LSB of B is constant zero (and Y_WIDTH is 1) then
-    //   we can optimise by removing every other entry from A
-    //   and popping the constant zero from B
-    else if (_TECHMAP_CONSTMSK_B_[0] && !_TECHMAP_CONSTVAL_B_[0]) begin
-      wire [(A_WIDTH+1)/2-1:0] A_i;
-      for (i = 0; i < (A_WIDTH+1)/2; i++)
-        assign A_i[i] = A[i*2];
-      \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH((A_WIDTH+1'd1)/2'd2), .B_WIDTH(B_WIDTH-1'd1), .Y_WIDTH(Y_WIDTH)) _TECHMAP_REPLACE_ (.A(A_i), .B(B[B_WIDTH-1:1]), .Y(Y));
-    end
-    // Trim off any leading 1'bx -es in A, and resize B accordingly
-    else if (num_leading_X_in_A > 0) begin
-      localparam A_WIDTH_new = A_WIDTH - num_leading_X_in_A;
-      localparam B_WIDTH_new = $clog2(A_WIDTH_new);
-      \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(A_WIDTH_new), .B_WIDTH(B_WIDTH_new), .Y_WIDTH(Y_WIDTH)) _TECHMAP_REPLACE_ (.A(A[A_WIDTH_new-1:0]), .B(B[B_WIDTH_new-1:0]), .Y(Y));
-    end
-    else if (B_WIDTH < 3 || A_WIDTH <= 4) begin
-      \$shiftx  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(A_WIDTH), .B_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) _TECHMAP_REPLACE_ (.A(A), .B(B), .Y(Y));
-    end
-    else if (B_WIDTH == 3) begin
-      localparam a_width0 = 2 ** 2;
-      localparam a_widthN = A_WIDTH - a_width0;
-      wire T0, T1;
-      \$shiftx  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(a_width0), .B_WIDTH(2),                .Y_WIDTH(Y_WIDTH)) fpga_soft_mux      (.A(A[a_width0-1:0]),       .B(B[2-1:0]),                .Y(T0));
-      if (a_widthN > 1)
-        \$shiftx  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(a_widthN), .B_WIDTH($clog2(a_widthN)), .Y_WIDTH(Y_WIDTH)) fpga_soft_mux_last (.A(A[A_WIDTH-1:a_width0]), .B(B[$clog2(a_widthN)-1:0]), .Y(T1));
-      else
-        assign T1 = A[A_WIDTH-1];
-      MUXF7 fpga_hard_mux (.I0(T0), .I1(T1), .S(B[B_WIDTH-1]), .O(Y));
-    end
-    else if (B_WIDTH == 4) begin
-      localparam a_width0 = 2 ** 2;
-      localparam num_mux8 = A_WIDTH / a_width0;
-      localparam a_widthN = A_WIDTH - num_mux8*a_width0;
-      wire [4-1:0] T;
-      wire T0, T1;
-      for (i = 0; i < 4; i++)
-        if (i < num_mux8)
-          \$shiftx  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(a_width0), .B_WIDTH(2),                .Y_WIDTH(Y_WIDTH)) fpga_soft_mux      (.A(A[i*a_width0+:a_width0]), .B(B[2-1:0]),                .Y(T[i]));
-        else if (i == num_mux8 && a_widthN > 0) begin
-          if (a_widthN > 1)
-            \$shiftx  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(a_widthN), .B_WIDTH($clog2(a_widthN)), .Y_WIDTH(Y_WIDTH)) fpga_soft_mux_last (.A(A[A_WIDTH-1:i*a_width0]), .B(B[$clog2(a_widthN)-1:0]), .Y(T[i]));
-          else
-            assign T[i] = A[A_WIDTH-1];
-        end
-        else
-          assign T[i] = 1'bx;
-      MUXF7 fpga_hard_mux_0 (.I0(T[0]), .I1(T[1]), .S(B[2]), .O(T0));
-      MUXF7 fpga_hard_mux_1 (.I0(T[2]), .I1(T[3]), .S(B[2]), .O(T1));
-      MUXF8 fpga_hard_mux_2 (.I0(T0),   .I1(T1),   .S(B[3]), .O(Y));
-    end
-    else begin
-      localparam a_width0 = 2 ** 4;
-      localparam num_mux16 = A_WIDTH / a_width0;
-      localparam a_widthN = A_WIDTH - num_mux16*a_width0;
-      wire [(2**(B_WIDTH-4))-1:0] T;
-      for (i = 0; i < 2 ** (B_WIDTH-4); i++)
-        if (i < num_mux16)
-          \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(a_width0), .B_WIDTH(4),                .Y_WIDTH(Y_WIDTH)) fpga_soft_mux      (.A(A[i*a_width0+:a_width0]), .B(B[4-1:0]),                .Y(T[i]));
-        else if (i == num_mux16 && a_widthN > 0) begin
-          if (a_widthN > 1)
-            \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(a_widthN), .B_WIDTH($clog2(a_widthN)), .Y_WIDTH(Y_WIDTH)) fpga_soft_mux_last (.A(A[A_WIDTH-1:i*a_width0]), .B(B[$clog2(a_widthN)-1:0]), .Y(T[i]));
-          else
-            assign T[i] = A[A_WIDTH-1];
-        end
-        else
-          assign T[i] = 1'bx;
-      \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(2**(B_WIDTH-4)), .B_WIDTH(B_WIDTH-4), .Y_WIDTH(Y_WIDTH)) _TECHMAP_REPLACE_ (.A(T), .B(B[B_WIDTH-1:4]), .Y(Y));
-    end
-  endgenerate
-endmodule
-
-module \$_MUX8_ (A, B, C, D, E, F, G, H, S, T, U, Y);
-input A, B, C, D, E, F, G, H, S, T, U;
-output Y;
-  \$__XILINX_SHIFTX  #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(8), .B_WIDTH(3), .Y_WIDTH(1)) _TECHMAP_REPLACE_ (.A({H,G,F,E,D,C,B,A}), .B({U,T,S}), .Y(Y));
-endmodule
-
-module \$_MUX16_ (A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, S, T, U, V, Y);
-input A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, S, T, U, V;
-output Y;
-  \$__XILINX_SHIFTX  #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(16), .B_WIDTH(4), .Y_WIDTH(1)) _TECHMAP_REPLACE_ (.A({P,O,N,M,L,K,J,I,H,G,F,E,D,C,B,A}), .B({V,U,T,S}), .Y(Y));
-endmodule
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index d9aa36666..bf7a0ed44 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/techlibs/xilinx/cells_sim.v
@@ -205,7 +205,7 @@ endmodule
 
 `endif
 
-module FDRE ((* abc_flop_q *) output reg Q, input C, CE, D, R);
+module FDRE (output reg 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;
@@ -217,7 +217,7 @@ module FDRE ((* abc_flop_q *) output reg Q, input C, CE, D, R);
   endcase endgenerate
 endmodule
 
-module FDSE ((* abc_flop_q *) output reg Q, input C, CE, D, S);
+module FDSE (output reg Q, input C, CE, D, S);
   parameter [0:0] INIT = 1'b0;
   parameter [0:0] IS_C_INVERTED = 1'b0;
   parameter [0:0] IS_D_INVERTED = 1'b0;
@@ -229,7 +229,7 @@ module FDSE ((* abc_flop_q *) output reg Q, input C, CE, D, S);
   endcase endgenerate
 endmodule
 
-module FDCE ((* abc_flop_q *) output reg Q, input C, CE, D, CLR);
+module FDCE (output reg 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;
@@ -243,7 +243,7 @@ module FDCE ((* abc_flop_q *) output reg Q, input C, CE, D, CLR);
   endcase endgenerate
 endmodule
 
-module FDPE ((* abc_flop_q *) output reg Q, input C, CE, D, PRE);
+module FDPE (output reg Q, input C, CE, D, PRE);
   parameter [0:0] INIT = 1'b0;
   parameter [0:0] IS_C_INVERTED = 1'b0;
   parameter [0:0] IS_D_INVERTED = 1'b0;
@@ -257,25 +257,25 @@ module FDPE ((* abc_flop_q *) output reg Q, input C, CE, D, PRE);
   endcase endgenerate
 endmodule
 
-module FDRE_1 ((* abc_flop_q *) output reg Q, input C, CE, D, R);
+module FDRE_1 (output reg Q, input C, 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 ((* abc_flop_q *) output reg Q, input C, CE, D, S);
+module FDSE_1 (output reg Q, input C, 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 ((* abc_flop_q *) output reg Q, input C, CE, D, CLR);
+module FDCE_1 (output reg Q, input C, 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 ((* abc_flop_q *) output reg Q, input C, CE, D, PRE);
+module FDPE_1 (output reg Q, input C, 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;
@@ -315,7 +315,7 @@ module RAM128X1D (
 endmodule
 
 module SRL16E (
-  (* abc_flop_q *) output Q,
+  output Q,
   input A0, A1, A2, A3, CE, CLK, D
 );
   parameter [15:0] INIT = 16'h0000;
@@ -333,7 +333,7 @@ module SRL16E (
 endmodule
 
 module SRLC32E (
-  (* abc_flop_q *) output Q,
+  output Q,
   output Q31,
   input [4:0] A,
   input CE, CLK, D
diff --git a/techlibs/xilinx/mux_map.v b/techlibs/xilinx/mux_map.v
deleted file mode 100644
index 0fa8db736..000000000
--- a/techlibs/xilinx/mux_map.v
+++ /dev/null
@@ -1,52 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *                2019  Eddie Hung    <eddie@fpgeh.com>
- *
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-module \$shiftx (A, B, Y);
-  parameter A_SIGNED = 0;
-  parameter B_SIGNED = 0;
-  parameter A_WIDTH = 1;
-  parameter B_WIDTH = 1;
-  parameter Y_WIDTH = 1;
-
-  input [A_WIDTH-1:0] A;
-  input [B_WIDTH-1:0] B;
-  output [Y_WIDTH-1:0] Y;
-
-  parameter [B_WIDTH-1:0] _TECHMAP_CONSTMSK_B_ = 0;
-  parameter [B_WIDTH-1:0] _TECHMAP_CONSTVAL_B_ = 0;
-
-  generate
-    genvar i, j;
-    // TODO: Check if this opt still necessary
-    if (B_SIGNED) begin
-      if (_TECHMAP_CONSTMSK_B_[B_WIDTH-1] && _TECHMAP_CONSTVAL_B_[B_WIDTH-1] == 1'b0)
-        // Optimisation to remove B_SIGNED if sign bit of B is constant-0
-        \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(0), .A_WIDTH(A_WIDTH), .B_WIDTH(B_WIDTH-1'd1), .Y_WIDTH(Y_WIDTH)) _TECHMAP_REPLACE_ (.A(A), .B(B[B_WIDTH-2:0]), .Y(Y));
-      else
-        wire _TECHMAP_FAIL_ = 1;
-    end
-    else if (B_WIDTH < 3 || A_WIDTH <= 4) begin
-      wire _TECHMAP_FAIL_ = 1;
-    end
-    else begin
-        \$__XILINX_SHIFTX  #(.A_SIGNED(A_SIGNED), .B_SIGNED(B_SIGNED), .A_WIDTH(A_WIDTH), .B_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) _TECHMAP_REPLACE_ (.A(A), .B(B), .Y(Y));
-    end
-  endgenerate
-endmodule
diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc
index f966115cd..a11648873 100644
--- a/techlibs/xilinx/synth_xilinx.cc
+++ b/techlibs/xilinx/synth_xilinx.cc
@@ -25,6 +25,8 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+#define XC7_WIRE_DELAY "160"
+
 struct SynthXilinxPass : public ScriptPass
 {
 	SynthXilinxPass() : ScriptPass("synth_xilinx", "synthesis for Xilinx FPGAs") { }
@@ -70,9 +72,6 @@ struct SynthXilinxPass : public ScriptPass
 		log("    -nosrl\n");
 		log("        disable inference of shift registers\n");
 		log("\n");
-		log("    -nomux\n");
-		log("        disable inference of wide multiplexers\n");
-		log("\n");
 		log("    -run <from_label>:<to_label>\n");
 		log("        only run the commands between the labels (see below). an empty\n");
 		log("        from label is synonymous to 'begin', and empty to label is\n");
@@ -85,7 +84,7 @@ struct SynthXilinxPass : public ScriptPass
 		log("        run 'abc' with -dff option\n");
 		log("\n");
 		log("    -abc9\n");
-		log("        use abc9 instead of abc\n");
+		log("        use new ABC9 flow (EXPERIMENTAL)\n");
 		log("\n");
 		log("\n");
 		log("The following commands are executed by this synthesis command:\n");
@@ -94,7 +93,7 @@ struct SynthXilinxPass : public ScriptPass
 	}
 
 	std::string top_opt, edif_file, blif_file, abc, arch;
-	bool flatten, retime, vpr, nocarry, nobram, nodram, nosrl, nomux;
+	bool flatten, retime, vpr, nocarry, nobram, nodram, nosrl;
 
 	void clear_flags() YS_OVERRIDE
 	{
@@ -109,7 +108,6 @@ struct SynthXilinxPass : public ScriptPass
 		nobram = false;
 		nodram = false;
 		nosrl = false;
-		nomux = false;
 		arch = "xc7";
 	}
 
@@ -173,10 +171,6 @@ struct SynthXilinxPass : public ScriptPass
 				nosrl = true;
 				continue;
 			}
-			if (args[argidx] == "-nomux") {
-				nomux = true;
-				continue;
-			}
 			if (args[argidx] == "-abc9") {
 				abc = "abc9";
 				continue;
@@ -225,15 +219,11 @@ struct SynthXilinxPass : public ScriptPass
 		if (check_label("coarse")) {
 			run("synth -run coarse");
 
-			//if (!nomux || help_mode)
-			//	run("muxpack", "(skip if '-nomux')");
-
 			// shregmap -tech xilinx can cope with $shiftx and $mux
 			//   cells for identifying variable-length shift registers,
 			//   so attempt to convert $pmux-es to the former
-			// Also: wide multiplexer inference benefits from this too
-			if (!(nosrl && nomux) || help_mode)
-				run("pmux2shiftx", "(skip if '-nosrl' and '-nomux')");
+			if (!nosrl || help_mode)
+				run("pmux2shiftx", "(skip if '-nosrl')");
 
 			// Run a number of peephole optimisations, including one
 			//   that optimises $mul cells driving $shiftx's B input
@@ -272,32 +262,26 @@ struct SynthXilinxPass : public ScriptPass
 
 			std::string techmap_files = " -map +/techmap.v";
 			if (help_mode)
-					techmap_files += " [-map +/xilinx/mux_map.v]";
-			else if (!nomux)
-					techmap_files += " -map +/xilinx/mux_map.v";
-			if (help_mode)
-					techmap_files += " [-map +/xilinx/arith_map.v]";
+				techmap_files += " [-map +/xilinx/arith_map.v]";
 			else if (!nocarry) {
-					techmap_files += " -map +/xilinx/arith_map.v";
-					if (vpr)
-							techmap_files += " -D _EXPLICIT_CARRY";
-					else if (abc == "abc9")
-							techmap_files += " -D _CLB_CARRY";
+				techmap_files += " -map +/xilinx/arith_map.v";
+				if (vpr)
+					techmap_files += " -D _EXPLICIT_CARRY";
+				else if (abc == "abc9")
+					techmap_files += " -D _CLB_CARRY";
 			}
 			run("techmap " + techmap_files);
 			run("opt -fast");
 		}
 
 		if (check_label("map_cells")) {
-			if (!nomux || help_mode)
-				run("muxcover -mux8 -mux16", "(skip if '-nomux')");
 			run("techmap -map +/techmap.v -map +/xilinx/cells_map.v");
 			run("clean");
 		}
 
 		if (check_label("map_luts")) {
 			if (abc == "abc9")
-				run(abc + " -lut +/xilinx/abc.lut -box +/xilinx/abc.box -W 160" + string(retime ? " -dff" : ""));
+				run(abc + " -lut +/xilinx/abc_xc7.lut -box +/xilinx/abc_xc7.box -W " + XC7_WIRE_DELAY + string(retime ? " -dff" : ""));
 			else if (help_mode)
 				run(abc + " -luts 2:2,3,6:5,10,20 [-dff]");
 			else
@@ -308,7 +292,7 @@ struct SynthXilinxPass : public ScriptPass
 			//   has performed any necessary retiming
 			if (!nosrl || help_mode)
 				run("shregmap -minlen 3 -init -params -enpol any_or_none", "(skip if '-nosrl')");
-			run("techmap -map +/xilinx/lut_map.v -map +/xilinx/cells_map.v -map +/xilinx/ff_map.v");
+			run("techmap -map +/xilinx/lut_map.v -map +/xilinx/ff_map.v -map +/xilinx/cells_map.v");
 			run("dffinit -ff FDRE Q INIT -ff FDCE Q INIT -ff FDPE Q INIT -ff FDSE Q INIT "
 					"-ff FDRE_1 Q INIT -ff FDCE_1 Q INIT -ff FDPE_1 Q INIT -ff FDSE_1 Q INIT");
 			run("clean");
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index 2752ff8cc..0b83c34a3 100644
--- a/tests/simple_abc9/abc9.v
+++ b/tests/simple_abc9/abc9.v
@@ -250,3 +250,15 @@ module abc9_test023 #(
 	wire [2*M-1:0] mask = {M{1'b1}};
 	assign dout = (mask << din[N-1:0]) >> M;
 endmodule
+
+module abc9_test024(input [3:0] i, output [3:0] o);
+abc9_test024_sub a(i[1:0], o[1:0]);
+endmodule
+
+module abc9_test024_sub(input [1:0] i, output [1:0] o);
+assign o = i;
+endmodule
+
+module abc9_test025(input [3:0] i, output [3:0] o);
+abc9_test024_sub a(i[2:1], o[2:1]);
+endmodule
diff --git a/tests/various/muxpack.v b/tests/various/muxpack.v
deleted file mode 100644
index f1bd5ea8e..000000000
--- a/tests/various/muxpack.v
+++ /dev/null
@@ -1,138 +0,0 @@
-module mux_if_unbal_4_1 #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @*
-    if (s == 0) o <= i[0*W+:W];
-    else if (s == 1) o <= i[1*W+:W];
-    else if (s == 2) o <= i[2*W+:W];
-    else if (s == 3) o <= i[3*W+:W];
-    else o <= {W{1'bx}};
-endmodule
-
-module mux_if_unbal_5_3 #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @* begin
-    o <= {W{1'bx}};
-    if (s == 0) o <= i[0*W+:W];
-    if (s == 1) o <= i[1*W+:W];
-    if (s == 2) o <= i[2*W+:W];
-    if (s == 3) o <= i[3*W+:W];
-    if (s == 4) o <= i[4*W+:W];
-end
-endmodule
-
-module mux_if_unbal_5_3_invert #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @*
-    if (s != 0) 
-	   	if (s != 1) 
-			if (s != 2)
-				if (s != 3)
-					if (s != 4) o <= i[4*W+:W];
-					else o <= i[0*W+:W];
-				else o <= i[3*W+:W];
-			else o <= i[2*W+:W];
-		else o <= i[1*W+:W];
-    else o <= {W{1'bx}};
-endmodule
-
-module mux_if_unbal_5_3_width_mismatch #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @* begin
-    o <= {W{1'bx}};
-    if (s == 0) o <= i[0*W+:W];
-    if (s == 1) o <= i[1*W+:W];
-    if (s == 2) o[W-2:0] <= i[2*W+:W-1];
-    if (s == 3) o <= i[3*W+:W];
-    if (s == 4) o <= i[4*W+:W];
-end
-endmodule
-
-module mux_if_unbal_4_1_missing #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @* begin
-    if (s == 0) o <= i[0*W+:W];
-//    else if (s == 1) o <= i[1*W+:W];
-//    else if (s == 2) o <= i[2*W+:W];
-    else if (s == 3) o <= i[3*W+:W];
-    else o <= {W{1'bx}};
-end
-endmodule
-
-module mux_if_unbal_5_3_order #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @* begin
-    o <= {W{1'bx}};
-    if (s == 3) o <= i[3*W+:W];
-    if (s == 2) o <= i[2*W+:W];
-    if (s == 1) o <= i[1*W+:W];
-    if (s == 4) o <= i[4*W+:W];
-    if (s == 0) o <= i[0*W+:W];
-end
-endmodule
-
-module mux_if_unbal_4_1_nonexcl #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @*
-    if (s == 0) o <= i[0*W+:W];
-    else if (s == 1) o <= i[1*W+:W];
-    else if (s == 2) o <= i[2*W+:W];
-    else if (s == 3) o <= i[3*W+:W];
-	else if (s == 0) o <= {W{1'b0}};
-    else o <= {W{1'bx}};
-endmodule
-
-module mux_if_unbal_5_3_nonexcl #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @* begin
-    o <= {W{1'bx}};
-    if (s == 0) o <= i[0*W+:W];
-    if (s == 1) o <= i[1*W+:W];
-    if (s == 2) o <= i[2*W+:W];
-    if (s == 3) o <= i[3*W+:W];
-    if (s == 4) o <= i[4*W+:W];
-	if (s == 0) o <= i[2*W+:W];
-end
-endmodule
-
-module mux_case_unbal_8_7#(parameter N=8, parameter W=7) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @* begin
-    o <= {W{1'bx}};
-    case (s)
-    0: o <= i[0*W+:W];
-    default:
-        case (s)
-        1: o <= i[1*W+:W];
-        2: o <= i[2*W+:W];
-        default:
-            case (s)
-            3: o <= i[3*W+:W];
-            4: o <= i[4*W+:W];
-            5: o <= i[5*W+:W];
-            default:
-                case (s)
-                    6: o <= i[6*W+:W];
-                    default: o <= i[7*W+:W];
-                endcase
-            endcase
-        endcase
-    endcase
-end
-endmodule
-
-module mux_if_bal_8_2 #(parameter N=8, parameter W=2) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
-always @*
-    if (s[0] == 1'b0)
-     if (s[1] == 1'b0)
-      if (s[2] == 1'b0)
-       o <= i[0*W+:W];
-      else
-       o <= i[1*W+:W];
-     else
-      if (s[2] == 1'b0)
-       o <= i[2*W+:W];
-      else
-       o <= i[3*W+:W];
-    else
-     if (s[1] == 1'b0)
-      if (s[2] == 1'b0)
-       o <= i[4*W+:W];
-      else
-       o <= i[5*W+:W];
-     else
-      if (s[2] == 1'b0)
-       o <= i[6*W+:W];
-      else
-       o <= i[7*W+:W];
-endmodule
diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys
deleted file mode 100644
index 9ea743b9f..000000000
--- a/tests/various/muxpack.ys
+++ /dev/null
@@ -1,150 +0,0 @@
-read_verilog muxpack.v
-design -save read
-hierarchy -top mux_if_unbal_4_1
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_5_3
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_5_3_invert
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_5_3_width_mismatch
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 2 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_4_1_missing
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_5_3_order
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_4_1_nonexcl
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_unbal_5_3_nonexcl
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_case_unbal_8_7
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 0 t:$mux
-select -assert-count 1 t:$pmux
-design -stash gate
-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 miter
-
-design -load read
-hierarchy -top mux_if_bal_8_2
-prep
-design -save gold
-muxpack
-opt
-stat
-select -assert-count 7 t:$mux
-select -assert-count 0 t:$pmux
-design -stash gate
-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 miter
diff --git a/tests/various/shregmap.v b/tests/various/shregmap.v
deleted file mode 100644
index 56e05c2c0..000000000
--- a/tests/various/shregmap.v
+++ /dev/null
@@ -1,22 +0,0 @@
-module shregmap_test(input i, clk, output [1:0] q);
-reg head = 1'b0;
-reg [3:0] shift1 = 4'b0000;
-reg [3:0] shift2 = 4'b0000;
-
-always @(posedge clk) begin
-    head <= i;
-    shift1 <= {shift1[2:0], head};
-    shift2 <= {shift2[2:0], head};
-end
-
-assign q = {shift2[3], shift1[3]};
-endmodule
-
-module $__SHREG_DFF_P_(input C, D, output Q);
-parameter DEPTH = 1;
-parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
-reg [DEPTH-1:0] r = INIT;
-always @(posedge C) 
-    r <= { r[DEPTH-2:0], D };
-assign Q = r[DEPTH-1];
-endmodule
diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys
deleted file mode 100644
index ca7f47015..000000000
--- a/tests/various/shregmap.ys
+++ /dev/null
@@ -1,31 +0,0 @@
-read_verilog shregmap.v
-design -copy-to model $__SHREG_DFF_P_
-hierarchy -top shregmap_test
-prep
-design -save gold
-
-techmap
-shregmap -init
-
-opt
-
-stat
-# show -width
-select -assert-count 1 t:$_DFF_P_
-select -assert-count 2 t:$__SHREG_DFF_P_
-
-design -stash gate
-
-design -import gold -as gold
-design -import gate -as gate
-design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_
-prep
-
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-sat -verify -prove-asserts -show-ports -seq 5 miter
-
-design -load gold
-stat
-
-design -load gate
-stat