Merge remote-tracking branch 'origin/master' into xc7mux

22 files changed, 335 insertions, 171 deletions

diff --git a/Makefile b/Makefile
index fd4e90c15..d33f27b63 100644
--- a/Makefile
+++ b/Makefile
@@ -666,6 +666,12 @@ else
 SEEDOPT=""
 endif
 
+ifneq ($(ABCEXTERNAL),)
+ABCOPT="-A $(ABCEXTERNAL)"
+else
+ABCOPT=""
+endif
+
 test: $(TARGETS) $(EXTRA_TARGETS)
 	+cd tests/simple && bash run-test.sh $(SEEDOPT)
 	+cd tests/hana && bash run-test.sh $(SEEDOPT)
@@ -674,13 +680,14 @@ test: $(TARGETS) $(EXTRA_TARGETS)
 	+cd tests/share && bash run-test.sh $(SEEDOPT)
 	+cd tests/fsm && bash run-test.sh $(SEEDOPT)
 	+cd tests/techmap && bash run-test.sh
-	+cd tests/memories && bash run-test.sh $(SEEDOPT)
+	+cd tests/memories && bash run-test.sh $(ABCOPT) $(SEEDOPT)
 	+cd tests/bram && bash run-test.sh $(SEEDOPT)
 	+cd tests/various && bash run-test.sh
 	+cd tests/sat && bash run-test.sh
 	+cd tests/svinterfaces && bash run-test.sh $(SEEDOPT)
 	+cd tests/opt && bash run-test.sh
-	+cd tests/aiger && bash run-test.sh
+	+cd tests/aiger && bash run-test.sh $(ABCOPT)
+	+cd tests/arch && bash run-test.sh
 	+cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT)
 	@echo ""
 	@echo "  Passed \"make test\"."
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 2815abda8..7c851bb91 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -70,35 +70,35 @@ struct AigerWriter
 
 	int bit2aig(SigBit bit)
 	{
-		if (aig_map.count(bit) == 0)
-		{
-			aig_map[bit] = -1;
-
-			if (initstate_bits.count(bit)) {
-				log_assert(initstate_ff > 0);
-				aig_map[bit] = initstate_ff;
-			} else
-			if (not_map.count(bit)) {
-				int a = bit2aig(not_map.at(bit)) ^ 1;
-				aig_map[bit] = a;
-			} else
-			if (and_map.count(bit)) {
-				auto args = and_map.at(bit);
-				int a0 = bit2aig(args.first);
-				int a1 = bit2aig(args.second);
-				aig_map[bit] = mkgate(a0, a1);
-			} else
-			if (alias_map.count(bit)) {
-				int a = bit2aig(alias_map.at(bit));
-				aig_map[bit] = a;
-			}
+		auto it = aig_map.find(bit);
+		if (it != aig_map.end()) {
+			log_assert(it->second >= 0);
+			return it->second;
+		}
 
-			if (bit == State::Sx || bit == State::Sz)
-				log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+		// NB: Cannot use iterator returned from aig_map.insert()
+		//     since this function is called recursively
+
+		int a = -1;
+		if (not_map.count(bit)) {
+			a = bit2aig(not_map.at(bit)) ^ 1;
+		} else
+		if (and_map.count(bit)) {
+			auto args = and_map.at(bit);
+			int a0 = bit2aig(args.first);
+			int a1 = bit2aig(args.second);
+			a = mkgate(a0, a1);
+		} else
+		if (alias_map.count(bit)) {
+			a = bit2aig(alias_map.at(bit));
 		}
 
-		log_assert(aig_map.at(bit) >= 0);
-		return aig_map.at(bit);
+		if (bit == State::Sx || bit == State::Sz)
+			log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
+
+		log_assert(a >= 0);
+		aig_map[bit] = a;
+		return a;
 	}
 
 	AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 92df899c2..eb3d47569 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -25,6 +25,21 @@
 #elif defined(__APPLE__)
 #include <libkern/OSByteOrder.h>
 #define __builtin_bswap32 OSSwapInt32
+#elif !defined(__GNUC__)
+#include <cstdint>
+inline uint32_t __builtin_bswap32(uint32_t x)
+{
+	// https://stackoverflow.com/a/27796212
+	register uint32_t value = number_to_be_reversed;
+	uint8_t lolo = (value >> 0) & 0xFF;
+	uint8_t lohi = (value >> 8) & 0xFF;
+	uint8_t hilo = (value >> 16) & 0xFF;
+	uint8_t hihi = (value >> 24) & 0xFF;
+	return (hihi << 24)
+		| (hilo << 16)
+		| (lohi << 8)
+		| (lolo << 0);
+}
 #endif
 
 #include "kernel/yosys.h"
@@ -284,8 +299,6 @@ struct XAigerWriter
 					for (auto user_cell : it.second)
 						toposort.edge(driver_cell, user_cell);
 
-			pool<RTLIL::Module*> abc_carry_modules;
-
 #if 0
 			toposort.analyze_loops = true;
 #endif
@@ -303,54 +316,54 @@ struct XAigerWriter
 #endif
 			log_assert(no_loops);
 
+			pool<IdString> seen_boxes;
 			for (auto cell_name : toposort.sorted) {
 				RTLIL::Cell *cell = module->cell(cell_name);
+				log_assert(cell);
+
 				RTLIL::Module* box_module = module->design->module(cell->type);
 				if (!box_module || !box_module->attributes.count("\\abc_box_id"))
 					continue;
 
-				if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) {
-					RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr;
-					auto &ports = box_module->ports;
-					for (auto it = ports.begin(); it != ports.end(); ) {
-						RTLIL::Wire* w = box_module->wire(*it);
-						log_assert(w);
-						if (w->port_input && w->attributes.count("\\abc_carry_in")) {
-							if (carry_in)
-								log_error("More than one port with attribute 'abc_carry_in' found in module '%s'\n", log_id(box_module));
-							carry_in = w;
-							it = ports.erase(it);
-							continue;
-						}
-						if (w->port_output && w->attributes.count("\\abc_carry_out")) {
-							if (carry_out)
-								log_error("More than one port with attribute 'abc_carry_out' found in module '%s'\n", log_id(box_module));
-							carry_out = w;
-							it = ports.erase(it);
-							continue;
+				if (seen_boxes.insert(cell->type).second) {
+					auto it = box_module->attributes.find("\\abc_carry");
+					if (it != box_module->attributes.end()) {
+						RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
+						auto carry_in_out = it->second.decode_string();
+						auto pos = carry_in_out.find(',');
+						if (pos == std::string::npos)
+							log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type));
+						auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos));
+						carry_in = box_module->wire(carry_in_name);
+						if (!carry_in || !carry_in->port_input)
+							log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str());
+
+						auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1));
+						carry_out = box_module->wire(carry_out_name);
+						if (!carry_out || !carry_out->port_output)
+							log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str());
+
+						auto &ports = box_module->ports;
+						for (auto jt = ports.begin(); jt != ports.end(); ) {
+							RTLIL::Wire* w = box_module->wire(*jt);
+							log_assert(w);
+							if (w == carry_in || w == carry_out) {
+								jt = ports.erase(jt);
+								continue;
+							}
+							if (w->port_id > carry_in->port_id)
+								--w->port_id;
+							if (w->port_id > carry_out->port_id)
+								--w->port_id;
+							log_assert(w->port_input || w->port_output);
+							log_assert(ports[w->port_id-1] == w->name);
+							++jt;
 						}
-						++it;
-					}
-
-					if (!carry_in)
-						log_error("Port with attribute 'abc_carry_in' not found in module '%s'\n", log_id(box_module));
-					if (!carry_out)
-						log_error("Port with attribute 'abc_carry_out' not found in module '%s'\n", log_id(box_module));
-
-					for (const auto port_name : ports) {
-						RTLIL::Wire* w = box_module->wire(port_name);
-						log_assert(w);
-						if (w->port_id > carry_in->port_id)
-							--w->port_id;
-						if (w->port_id > carry_out->port_id)
-							--w->port_id;
-						log_assert(w->port_input || w->port_output);
-						log_assert(ports[w->port_id-1] == w->name);
+						ports.push_back(carry_in->name);
+						carry_in->port_id = ports.size();
+						ports.push_back(carry_out->name);
+						carry_out->port_id = ports.size();
 					}
-					ports.push_back(carry_in->name);
-					carry_in->port_id = ports.size();
-					ports.push_back(carry_out->name);
-					carry_out->port_id = ports.size();
 				}
 
 				// Fully pad all unused input connections of this box cell with S0
@@ -438,14 +451,18 @@ struct XAigerWriter
 					new_wire = module->addWire(wire_name, GetSize(wire));
 				SigBit new_bit(new_wire, bit.offset);
 				module->connect(new_bit, bit);
-				if (not_map.count(bit))
-					not_map[new_bit] = not_map.at(bit);
+				if (not_map.count(bit)) {
+					auto a = not_map.at(bit);
+					not_map[new_bit] = a;
+				}
 				else if (and_map.count(bit)) {
-				    //and_map[new_bit] = and_map.at(bit); // Breaks gcc-4.8
-				    and_map.insert(std::make_pair(new_bit, and_map.at(bit)));
+					auto a = and_map.at(bit);
+					and_map[new_bit] = a;
+				}
+				else if (alias_map.count(bit)) {
+					auto a = alias_map.at(bit);
+					alias_map[new_bit] = a;
 				}
-				else if (alias_map.count(bit))
-					alias_map[new_bit] = alias_map.at(bit);
 				else
 					alias_map[new_bit] = bit;
 				output_bits.erase(bit);
diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index 43337f4c2..7008d0542 100644
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -732,44 +732,50 @@ void AigerReader::parse_aiger_binary()
 
 void AigerReader::post_process()
 {
-	pool<RTLIL::Module*> abc_carry_modules;
+	pool<IdString> seen_boxes;
 	unsigned ci_count = 0, co_count = 0;
 	for (auto cell : boxes) {
 		RTLIL::Module* box_module = design->module(cell->type);
 		log_assert(box_module);
 
-		if (box_module->attributes.count("\\abc_carry") && !abc_carry_modules.count(box_module)) {
-			RTLIL::Wire* carry_in = nullptr, *carry_out = nullptr;
-			RTLIL::Wire* last_in = nullptr, *last_out = nullptr;
-			for (const auto &port_name : box_module->ports) {
-				RTLIL::Wire* w = box_module->wire(port_name);
-				log_assert(w);
-				if (w->port_input) {
-					if (w->attributes.count("\\abc_carry_in")) {
-						log_assert(!carry_in);
-						carry_in = w;
-					}
-					log_assert(!last_in || last_in->port_id < w->port_id);
-					last_in = w;
-				}
-				if (w->port_output) {
-					if (w->attributes.count("\\abc_carry_out")) {
-						log_assert(!carry_out);
-						carry_out = w;
+		if (seen_boxes.insert(cell->type).second) {
+			auto it = box_module->attributes.find("\\abc_carry");
+			if (it != box_module->attributes.end()) {
+				RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr;
+				auto carry_in_out = it->second.decode_string();
+				auto pos = carry_in_out.find(',');
+				if (pos == std::string::npos)
+					log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type));
+				auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos));
+				carry_in = box_module->wire(carry_in_name);
+				if (!carry_in || !carry_in->port_input)
+					log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str());
+
+				auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1));
+				carry_out = box_module->wire(carry_out_name);
+				if (!carry_out || !carry_out->port_output)
+					log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str());
+
+				auto &ports = box_module->ports;
+				for (auto jt = ports.begin(); jt != ports.end(); ) {
+					RTLIL::Wire* w = box_module->wire(*jt);
+					log_assert(w);
+					if (w == carry_in || w == carry_out) {
+						jt = ports.erase(jt);
+						continue;
 					}
-					log_assert(!last_out || last_out->port_id < w->port_id);
-					last_out = w;
+					if (w->port_id > carry_in->port_id)
+						--w->port_id;
+					if (w->port_id > carry_out->port_id)
+						--w->port_id;
+					log_assert(w->port_input || w->port_output);
+					log_assert(ports[w->port_id-1] == w->name);
+					++jt;
 				}
-			}
-
-			if (carry_in != last_in) {
-				std::swap(box_module->ports[carry_in->port_id], box_module->ports[last_in->port_id]);
-				std::swap(carry_in->port_id, last_in->port_id);
-			}
-			if (carry_out != last_out) {
-				log_assert(last_out);
-				std::swap(box_module->ports[carry_out->port_id], box_module->ports[last_out->port_id]);
-				std::swap(carry_out->port_id, last_out->port_id);
+				ports.push_back(carry_in->name);
+				carry_in->port_id = ports.size();
+				ports.push_back(carry_out->name);
+				carry_out->port_id = ports.size();
 			}
 		}
 
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 4e91eddda..758661c02 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -246,24 +246,24 @@ struct CellTypes
 		cell_types.clear();
 	}
 
-	bool cell_known(RTLIL::IdString type)
+	bool cell_known(RTLIL::IdString type) const
 	{
 		return cell_types.count(type) != 0;
 	}
 
-	bool cell_output(RTLIL::IdString type, RTLIL::IdString port)
+	bool cell_output(RTLIL::IdString type, RTLIL::IdString port) const
 	{
 		auto it = cell_types.find(type);
 		return it != cell_types.end() && it->second.outputs.count(port) != 0;
 	}
 
-	bool cell_input(RTLIL::IdString type, RTLIL::IdString port)
+	bool cell_input(RTLIL::IdString type, RTLIL::IdString port) const
 	{
 		auto it = cell_types.find(type);
 		return it != cell_types.end() && it->second.inputs.count(port) != 0;
 	}
 
-	bool cell_evaluable(RTLIL::IdString type)
+	bool cell_evaluable(RTLIL::IdString type) const
 	{
 		auto it = cell_types.find(type);
 		return it != cell_types.end() && it->second.is_evaluable;
@@ -482,4 +482,3 @@ extern CellTypes yosys_celltypes;
 YOSYS_NAMESPACE_END
 
 #endif
-
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 94dbf31c0..a09f4a0d1 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1595,10 +1595,9 @@ void RTLIL::Module::remove(RTLIL::Cell *cell)
 	while (!cell->connections_.empty())
 		cell->unsetPort(cell->connections_.begin()->first);
 
-	auto it = cells_.find(cell->name);
-	log_assert(it != cells_.end());
+	log_assert(cells_.count(cell->name) != 0);
 	log_assert(refcount_cells_ == 0);
-	cells_.erase(it);
+	cells_.erase(cell->name);
 	delete cell;
 }
 
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index a4aca2fee..e9a43e0f3 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -44,7 +44,7 @@ struct OptPass : public Pass {
 		log("        opt_muxtree\n");
 		log("        opt_reduce [-fine] [-full]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff [-keepdc]\n");
+		log("        opt_rmdff [-keepdc] [-sat]\n");
 		log("        opt_clean [-purge]\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("    while <changed design>\n");
@@ -54,7 +54,7 @@ struct OptPass : public Pass {
 		log("    do\n");
 		log("        opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
 		log("        opt_merge [-share_all]\n");
-		log("        opt_rmdff [-keepdc]\n");
+		log("        opt_rmdff [-keepdc] [-sat]\n");
 		log("        opt_clean [-purge]\n");
 		log("    while <changed design in opt_rmdff>\n");
 		log("\n");
@@ -112,6 +112,10 @@ struct OptPass : public Pass {
 				opt_rmdff_args += " -keepdc";
 				continue;
 			}
+			if (args[argidx] == "-sat") {
+				opt_rmdff_args += " -sat";
+				continue;
+			}
 			if (args[argidx] == "-share_all") {
 				opt_merge_args += " -share_all";
 				continue;
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index eeb992a3e..be6ac2d30 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -17,19 +17,24 @@
  *
  */
 
+#include "kernel/log.h"
 #include "kernel/register.h"
+#include "kernel/rtlil.h"
+#include "kernel/satgen.h"
 #include "kernel/sigtools.h"
-#include "kernel/log.h"
-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
 SigMap assign_map, dff_init_map;
 SigSet<RTLIL::Cell*> mux_drivers;
+dict<SigBit, RTLIL::Cell*> bit2driver;
 dict<SigBit, pool<SigBit>> init_attributes;
+
 bool keepdc;
+bool sat;
 
 void remove_init_attr(SigSpec sig)
 {
@@ -452,12 +457,84 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 		dff->unsetPort("\\E");
 	}
 
+	if (sat && has_init && (!sig_r.size() || val_init == val_rv))
+	{
+		bool removed_sigbits = false;
+
+		ezSatPtr ez;
+		SatGen satgen(ez.get(), &assign_map);
+		pool<Cell*> sat_cells;
+
+		std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
+			if (!sat_cells.insert(c).second)
+				return;
+			if (!satgen.importCell(c))
+				return;
+			for (auto &conn : c->connections()) {
+				if (!c->input(conn.first))
+					continue;
+				for (auto bit : assign_map(conn.second))
+					if (bit2driver.count(bit))
+						sat_import_cell(bit2driver.at(bit));
+			}
+		};
+
+		// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
+		for (int position = 0; position < GetSize(sig_d); position += 1) {
+			RTLIL::SigBit q_sigbit = sig_q[position];
+			RTLIL::SigBit d_sigbit = sig_d[position];
+
+			if ((!q_sigbit.wire) || (!d_sigbit.wire))
+				continue;
+
+			if (!bit2driver.count(d_sigbit))
+				continue;
+
+			sat_import_cell(bit2driver.at(d_sigbit));
+
+			RTLIL::State sigbit_init_val = val_init[position];
+			if (sigbit_init_val != State::S0 && sigbit_init_val != State::S1)
+				continue;
+
+			int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
+			int q_sat_pi = satgen.importSigBit(q_sigbit);
+			int d_sat_pi = satgen.importSigBit(d_sigbit);
+
+			// Try to find out whether the register bit can change under some circumstances
+			bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
+
+			// If the register bit cannot change, we can replace it with a constant
+			if (!counter_example_found)
+			{
+				log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", sigbit_init_val ? 1 : 0,
+						position, log_id(dff), log_id(dff->type), log_id(mod));
+
+				SigSpec tmp = dff->getPort("\\D");
+				tmp[position] = sigbit_init_val;
+				dff->setPort("\\D", tmp);
+
+				removed_sigbits = true;
+			}
+		}
+
+		if (removed_sigbits) {
+			handle_dff(mod, dff);
+			return true;
+		}
+	}
+
+
 	return false;
 
 delete_dff:
 	log("Removing %s (%s) from module %s.\n", log_id(dff), log_id(dff->type), log_id(mod));
 	remove_init_attr(dff->getPort("\\Q"));
 	mod->remove(dff);
+
+	for (auto &entry : bit2driver)
+		if (entry.second == dff)
+			bit2driver.erase(entry.first);
+
 	return true;
 }
 
@@ -467,11 +544,15 @@ struct OptRmdffPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    opt_rmdff [-keepdc] [selection]\n");
+		log("    opt_rmdff [-keepdc] [-sat] [selection]\n");
 		log("\n");
 		log("This pass identifies flip-flops with constant inputs and replaces them with\n");
 		log("a constant driver.\n");
 		log("\n");
+		log("    -sat\n");
+		log("        additionally invoke SAT solver to detect and remove flip-flops (with \n");
+		log("        non-constant inputs) that can also be replaced with a constant driver\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
@@ -479,6 +560,7 @@ struct OptRmdffPass : public Pass {
 		log_header(design, "Executing OPT_RMDFF pass (remove dff with constant values).\n");
 
 		keepdc = false;
+		sat = false;
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++) {
@@ -486,18 +568,22 @@ struct OptRmdffPass : public Pass {
 				keepdc = true;
 				continue;
 			}
+			if (args[argidx] == "-sat") {
+				sat = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
-		for (auto module : design->selected_modules())
-		{
+		for (auto module : design->selected_modules()) {
 			pool<SigBit> driven_bits;
 			dict<SigBit, State> init_bits;
 
 			assign_map.set(module);
 			dff_init_map.set(module);
 			mux_drivers.clear();
+			bit2driver.clear();
 			init_attributes.clear();
 
 			for (auto wire : module->wires())
@@ -522,17 +608,21 @@ struct OptRmdffPass : public Pass {
 						driven_bits.insert(bit);
 				}
 			}
-			mux_drivers.clear();
 
 			std::vector<RTLIL::IdString> dff_list;
 			std::vector<RTLIL::IdString> dffsr_list;
 			std::vector<RTLIL::IdString> dlatch_list;
 			for (auto cell : module->cells())
 			{
-				for (auto &conn : cell->connections())
-					if (cell->output(conn.first) || !cell->known())
-						for (auto bit : assign_map(conn.second))
+				for (auto &conn : cell->connections()) {
+					bool is_output = cell->output(conn.first);
+					if (is_output || !cell->known())
+						for (auto bit : assign_map(conn.second)) {
+							if (is_output)
+								bit2driver[bit] = cell;
 							driven_bits.insert(bit);
+						}
+				}
 
 				if (cell->type == "$mux" || cell->type == "$pmux") {
 					if (cell->getPort("\\A").size() == cell->getPort("\\B").size())
@@ -604,6 +694,7 @@ struct OptRmdffPass : public Pass {
 
 		assign_map.clear();
 		mux_drivers.clear();
+		bit2driver.clear();
 		init_attributes.clear();
 
 		if (total_count || total_initdrv)
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index dbdd775f8..f107f9947 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -33,7 +33,7 @@
 #endif
 
 
-#define ABC_FAST_COMMAND_LUT "&st; &retime; &if {W}"
+#define ABC_FAST_COMMAND_LUT "&st; &if {W} {D}"
 
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -80,7 +80,7 @@ void handle_loops(RTLIL::Design *design)
 {
 	Pass::call(design, "scc -set_attr abc_scc_id {}");
 
-        dict<IdString, vector<IdString>> module_break;
+        dict<IdString, vector<IdString>> abc_scc_break;
 
 	// For every unique SCC found, (arbitrarily) find the first
 	// cell in the component, and select (and mark) all its output
@@ -116,12 +116,11 @@ void handle_loops(RTLIL::Design *design)
 			cell->attributes.erase(it);
 		}
 
-		auto jt = module_break.find(cell->type);
-		if (jt == module_break.end()) {
+		auto jt = abc_scc_break.find(cell->type);
+		if (jt == abc_scc_break.end()) {
 			std::vector<IdString> ports;
-			if (!yosys_celltypes.cell_known(cell->type)) {
-				RTLIL::Module* box_module = design->module(cell->type);
-				log_assert(box_module);
+			RTLIL::Module* box_module = design->module(cell->type);
+			if (box_module) {
 				auto ports_csv = box_module->attributes.at("\\abc_scc_break", RTLIL::Const::from_string("")).decode_string();
 				for (const auto &port_name : split_tokens(ports_csv, ",")) {
 					auto port_id = RTLIL::escape_id(port_name);
@@ -131,7 +130,7 @@ void handle_loops(RTLIL::Design *design)
 					ports.push_back(port_id);
 				}
 			}
-			jt = module_break.insert(std::make_pair(cell->type, std::move(ports))).first;
+			jt = abc_scc_break.insert(std::make_pair(cell->type, std::move(ports))).first;
 		}
 
 		for (auto port_name : jt->second) {
@@ -554,15 +553,20 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri
 			signal = std::move(bits);
 		}
 
+		dict<IdString, bool> abc_box;
 		vector<RTLIL::Cell*> boxes;
-		for (auto it = module->cells_.begin(); it != module->cells_.end(); ++it) {
-			RTLIL::Cell *cell = it->second;
-			if (cell->type.in("$_AND_", "$_NOT_", "$__ABC_FF_")) {
+		for (const auto &it : module->cells_) {
+			auto cell = it.second;
+			if (cell->type.in("$_AND_", "$_NOT_")) {
 				module->remove(cell);
 				continue;
 			}
-			RTLIL::Module* box_module = design->module(cell->type);
-			if (box_module && box_module->attributes.count("\\abc_box_id"))
+			auto jt = abc_box.find(cell->type);
+			if (jt == abc_box.end()) {
+				RTLIL::Module* box_module = design->module(cell->type);
+				jt = abc_box.insert(std::make_pair(cell->type, box_module && box_module->attributes.count("\\abc_box_id"))).first;
+			}
+			if (jt->second)
 				boxes.emplace_back(cell);
 		}
 
diff --git a/techlibs/ecp5/abc_5g.box b/techlibs/ecp5/abc_5g.box
index 5309aca87..c757d137d 100644
--- a/techlibs/ecp5/abc_5g.box
+++ b/techlibs/ecp5/abc_5g.box
@@ -16,7 +16,7 @@ CCU2C   1      1   9      3
 516  516  516  516  412   412  278  278  43
 
 # Box 2 : TRELLIS_DPR16X4 (16x4 dist ram)
-# Outputs: DO0, DO1, DO2, DO3, DO4
+# Outputs: DO0, DO1, DO2, DO3
 # name            ID  w/b   ins   outs
 TRELLIS_DPR16X4   2     0   14    4
 
diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v
index 08ae0a112..ca88d0a5b 100644
--- a/techlibs/ecp5/cells_sim.v
+++ b/techlibs/ecp5/cells_sim.v
@@ -15,11 +15,9 @@ module L6MUX21 (input D0, D1, SD, output Z);
 endmodule
 
 // ---------------------------------------
-(* 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);
+(* abc_box_id=1, abc_carry="CIN,COUT", lib_whitebox *)
+module CCU2C(input CIN, A0, B0, C0, D0, A1, B1, C1, D1,
+	           output S0, S1, COUT);
 
 	parameter [15:0] INIT0 = 16'h0000;
 	parameter [15:0] INIT1 = 16'h0000;
@@ -106,7 +104,7 @@ module PFUMX (input ALUT, BLUT, C0, output Z);
 endmodule
 
 // ---------------------------------------
-(* abc_box_id=2, abc_scc_break="DI,WRE" *)
+//(* abc_box_id=2, abc_scc_break="DI,WAD,WRE" *)
 module TRELLIS_DPR16X4 (
 	input [3:0] DI,
 	input [3:0] WAD,
diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index 317ae2c1f..b746ba4e5 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -136,20 +136,16 @@ module SB_LUT4 (output O, input I0, I1, I2, I3);
 	assign O = I0 ? s1[1] : s1[0];
 endmodule
 
-(* abc_box_id = 1, abc_carry, lib_whitebox *)
-module SB_CARRY ((* abc_carry_out *) output CO, input I0, I1, (* abc_carry_in *) input CI);
+(* abc_box_id = 1, abc_carry="CI,CO", lib_whitebox *)
+module SB_CARRY (output CO, input I0, I1, CI);
 	assign CO = (I0 && I1) || ((I0 || I1) && CI);
 endmodule
 
 // Positive Edge SiliconBlue FF Cells
 
 module SB_DFF (output `SB_DFF_REG, input C, D);
-`ifndef _ABC
 	always @(posedge C)
 		Q <= D;
-`else
-    always @* Q <= D;
-`endif
 endmodule
 
 module SB_DFFE (output `SB_DFF_REG, input C, E, D);
@@ -896,7 +892,6 @@ module SB_WARMBOOT (
 );
 endmodule
 
-(* nomem2reg *)
 module SB_SPRAM256KA (
 	input [13:0] ADDRESS,
 	input [15:0] DATAIN,
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index a782f00b9..9dd5d81f7 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -38,8 +38,8 @@ struct SynthIce40Pass : public ScriptPass
 		log("This command runs synthesis for iCE40 FPGAs.\n");
 		log("\n");
 		log("    -device < hx | lp | u >\n");
-		log("        optimise the synthesis netlist for the specified device.\n");
-		log("        HX is the default target if no device argument specified.\n");
+		log("        relevant only for '-abc9' flow, optimise timing for the specified device.\n");
+		log("        default: hx\n");
 		log("\n");
 		log("    -top <module>\n");
 		log("        use the specified module as top module\n");
@@ -105,7 +105,6 @@ struct SynthIce40Pass : public ScriptPass
 		log("\n");
 	}
 
-
 	string top_opt, blif_file, edif_file, json_file, abc, device_opt;
 	bool nocarry, nodffe, nobram, dsp, flatten, retime, relut, noabc, abc2, vpr;
 	int min_ce_use;
diff --git a/techlibs/xilinx/cells_map.v b/techlibs/xilinx/cells_map.v
index 61c2c8f94..cce70d69e 100644
--- a/techlibs/xilinx/cells_map.v
+++ b/techlibs/xilinx/cells_map.v
@@ -20,16 +20,14 @@
 
 // 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
+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
-
+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;
diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v
index 4a1e334d6..94bc3ef86 100644
--- a/techlibs/xilinx/cells_sim.v
+++ b/techlibs/xilinx/cells_sim.v
@@ -181,8 +181,8 @@ module XORCY(output O, input CI, LI);
   assign O = CI ^ LI;
 endmodule
 
-(* abc_box_id = 4, abc_carry, lib_whitebox *)
-module CARRY4((* abc_carry_out *) output [3:0] CO, output [3:0] O, (* abc_carry_in *) input CI, input CYINIT, input [3:0] DI, S);
+(* abc_box_id = 3, abc_carry="CI,CO", lib_whitebox *)
+module CARRY4(output [3:0] CO, O, input CI, CYINIT, input [3:0] DI, S);
   assign O = S ^ {CO[2:0], CI | CYINIT};
   assign CO[0] = S[0] ? CI | CYINIT : DI[0];
   assign CO[1] = S[1] ? CO[0] : DI[1];
diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc
index c72c0ba8c..0a30848aa 100644
--- a/techlibs/xilinx/synth_xilinx.cc
+++ b/techlibs/xilinx/synth_xilinx.cc
@@ -62,9 +62,6 @@ struct SynthXilinxPass : public ScriptPass
 		log("        generate an output netlist (and BLIF file) suitable for VPR\n");
 		log("        (this feature is experimental and incomplete)\n");
 		log("\n");
-		log("    -nocarry\n");
-		log("        disable inference of carry chains\n");
-		log("\n");
 		log("    -nobram\n");
 		log("        disable inference of block rams\n");
 		log("\n");
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index 5246c1b48..deaf48a3d 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -2,6 +2,16 @@
 
 set -e
 
+OPTIND=1
+abcprog="../../yosys-abc"    # default to built-in version of abc
+while getopts "A:" opt
+do
+    case "$opt" in
+	A) abcprog="$OPTARG" ;;
+    esac
+done
+shift "$((OPTIND-1))"
+
 # NB: *.aag and *.aig must contain a symbol table naming the primary
 #     inputs and outputs, otherwise ABC and Yosys will name them
 #     arbitrarily (and inconsistently with each other).
@@ -11,7 +21,7 @@ for aag in *.aag; do
     # (which would have been created by the reference aig2aig utility,
     #  available from http://fmv.jku.at/aiger/)
     echo "Checking $aag."
-    ../../yosys-abc -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
+    $abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
     ../../yosys -qp "
 read_verilog ${aag%.*}_ref.v
 prep
@@ -28,7 +38,7 @@ done
 
 for aig in *.aig; do
     echo "Checking $aig."
-    ../../yosys-abc -q "read -c $aig; write ${aig%.*}_ref.v"
+    $abcprog -q "read -c $aig; write ${aig%.*}_ref.v"
     ../../yosys -qp "
 read_verilog ${aig%.*}_ref.v
 prep
diff --git a/tests/arch/run-test.sh b/tests/arch/run-test.sh
new file mode 100755
index 000000000..5292d1615
--- /dev/null
+++ b/tests/arch/run-test.sh
@@ -0,0 +1,18 @@
+#!/bin/bash
+
+set -e
+
+echo "Running syntax check on arch sim models"
+for arch in ../../techlibs/*; do
+	find $arch -name cells_sim.v | while read path; do
+		echo -n "Test $path ->"
+		iverilog -t null -I$arch $path
+		echo " ok"
+	done
+done
+
+for path in "../../techlibs/common/simcells.v"  "../../techlibs/common/simlib.v"; do
+	echo -n "Test $path ->"
+	iverilog -t null $path
+	echo " ok"
+done
diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh
index d0537bb98..76acaa9cd 100755
--- a/tests/memories/run-test.sh
+++ b/tests/memories/run-test.sh
@@ -4,15 +4,17 @@ set -e
 
 OPTIND=1
 seed=""    # default to no seed specified
-while getopts "S:" opt
+abcopt=""
+while getopts "A:S:" opt
 do
     case "$opt" in
+	A) abcopt="-A $OPTARG" ;;
 	S) seed="-S $OPTARG" ;;
     esac
 done
 shift "$((OPTIND-1))"
 
-bash ../tools/autotest.sh $seed -G *.v
+bash ../tools/autotest.sh $abcopt $seed -G *.v
 
 for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do
 	echo -n "Testing expectations for $f .."
diff --git a/tests/opt/opt_ff_sat.v b/tests/opt/opt_ff_sat.v
new file mode 100644
index 000000000..5a0a6fe37
--- /dev/null
+++ b/tests/opt/opt_ff_sat.v
@@ -0,0 +1,12 @@
+module top (
+	input clk,
+	output reg [7:0] cnt
+);
+	initial cnt = 0;
+	always @(posedge clk) begin
+		if (cnt < 20)
+			cnt <= cnt + 1;
+		else
+			cnt <= 0;
+	end
+endmodule
diff --git a/tests/opt/opt_ff_sat.ys b/tests/opt/opt_ff_sat.ys
new file mode 100644
index 000000000..4e7cc6ca4
--- /dev/null
+++ b/tests/opt/opt_ff_sat.ys
@@ -0,0 +1,5 @@
+read_verilog opt_ff_sat.v
+prep -flatten
+opt_rmdff -sat
+synth
+select -assert-count 5 t:$_DFF_P_
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 96d9cdda9..7b64b357f 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -23,12 +23,13 @@ warn_iverilog_git=false
 # The tests are skipped if firrtl2verilog is the empty string (the default).
 firrtl2verilog=""
 xfirrtl="../xfirrtl"
+abcprog="$toolsdir/../../yosys-abc"
 
 if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdata ]; then
 	( set -ex; ${CC:-gcc} -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1
 fi
 
-while getopts xmGl:wkjvref:s:p:n:S:I:-: opt; do
+while getopts xmGl:wkjvref:s:p:n:S:I:A:-: opt; do
 	case "$opt" in
 		x)
 			use_xsim=true ;;
@@ -65,6 +66,8 @@ while getopts xmGl:wkjvref:s:p:n:S:I:-: opt; do
 			include_opts="$include_opts -I $OPTARG"
 			xinclude_opts="$xinclude_opts -i $OPTARG"
 			minclude_opts="$minclude_opts +incdir+$OPTARG" ;;
+		A)
+			abcprog="$OPTARG" ;;
 		-)
 			case "${OPTARG}" in
 			    xfirrtl)
@@ -147,7 +150,7 @@ do
 		if [[ "$ext" == "v" ]]; then
 			egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
 		elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then
-			"$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.${refext}"
+			$abcprog -c "read_aiger ../${fn}; write ${bn}_ref.${refext}"
 		else
 			refext=$ext
 			cp ../${fn} ${bn}_ref.${refext}