Merge branch 'eddie/abc9_refactor' into eddie/abc9_required

26 files changed, 537 insertions, 246 deletions

diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index 71b652412..76b7efbfc 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -222,6 +222,8 @@ struct XAigerWriter
 					alias_map[Q] = D;
 					auto r YS_ATTRIBUTE(unused) = ff_bits.insert(std::make_pair(D, cell));
 					log_assert(r.second);
+					if (input_bits.erase(Q))
+						log_assert(Q.wire->attributes.count(ID::keep));
 					continue;
 				}
 
@@ -589,9 +591,6 @@ struct XAigerWriter
 		//	write_o_buffer(0);
 
 		if (!box_list.empty() || !ff_bits.empty()) {
-			RTLIL::Module *holes_module = module->design->module(stringf("%s$holes", module->name.c_str()));
-			log_assert(holes_module);
-
 			dict<IdString, std::tuple<int,int,int>> cell_cache;
 
 			int box_count = 0;
@@ -678,6 +677,7 @@ struct XAigerWriter
 			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
 			f.write(buffer_str.data(), buffer_str.size());
 
+			RTLIL::Module *holes_module = module->design->module(stringf("%s$holes", module->name.c_str()));
 			if (holes_module) {
 				std::stringstream a_buffer;
 				XAigerWriter writer(holes_module, true /* holes_mode */);
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 6735d670f..60a098917 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -412,6 +412,8 @@ struct EdifBackend : public Backend {
 						for (auto &ref : it.second)
 							log_warning("Exporting x-bit on %s as zero bit.\n", ref.c_str());
 						sig = RTLIL::State::S0;
+					} else if (sig == RTLIL::State::Sz) {
+						continue;
 					} else {
 						for (auto &ref : it.second)
 							log_error("Don't know how to handle %s on %s.\n", log_signal(sig), ref.c_str());
diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc
index b5c861936..418fd722c 100644
--- a/frontends/aiger/aigerparse.cc
+++ b/frontends/aiger/aigerparse.cc
@@ -414,6 +414,10 @@ void AigerReader::parse_xaiger()
 				for (unsigned j = 0; j < cutLeavesM; ++j) {
 					nodeID = parse_xaiger_literal(f);
 					log_debug2("\t%u\n", nodeID);
+					if (nodeID == 0) {
+						log_debug("\tLUT '$lut$aiger%d$%d' input %d is constant!\n", aiger_autoidx, rootNodeID, cutLeavesM);
+						continue;
+					}
 					RTLIL::Wire *wire = module->wire(stringf("$aiger%d$%d", aiger_autoidx, nodeID));
 					log_assert(wire);
 					input_sig.append(wire);
@@ -421,10 +425,10 @@ void AigerReader::parse_xaiger()
 				// 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) {
+				RTLIL::Const lut_mask(RTLIL::State::Sx, 1 << GetSize(input_sig));
+				for (int j = 0; j < GetSize(lut_mask); ++j) {
 					int gray = j ^ (j >> 1);
-					ce.set_incremental(input_sig, RTLIL::Const{gray, static_cast<int>(cutLeavesM)});
+					ce.set_incremental(input_sig, RTLIL::Const{gray, GetSize(input_sig)});
 					RTLIL::SigBit o(output_sig);
 					bool success YS_ATTRIBUTE(unused) = ce.eval(o);
 					log_assert(success);
@@ -438,11 +442,13 @@ void AigerReader::parse_xaiger()
 			}
 		}
 		else if (c == 'r') {
-			uint32_t dataSize YS_ATTRIBUTE(unused) = parse_xaiger_literal(f);
+			uint32_t dataSize = parse_xaiger_literal(f);
 			flopNum = parse_xaiger_literal(f);
 			log_debug("flopNum = %u\n", flopNum);
 			log_assert(dataSize == (flopNum+1) * sizeof(uint32_t));
-			f.ignore(flopNum * sizeof(uint32_t));
+			mergeability.reserve(flopNum);
+			for (unsigned i = 0; i < flopNum; i++)
+				mergeability.emplace_back(parse_xaiger_literal(f));
 		}
 		else if (c == 'n') {
 			parse_xaiger_literal(f);
@@ -472,6 +478,7 @@ void AigerReader::parse_xaiger()
 				RTLIL::Cell* cell = module->addCell(stringf("$box%u", oldBoxNum), stringf("$__boxid%u", boxUniqueId));
 				cell->setPort("\\i", SigSpec(State::S0, boxInputs));
 				cell->setPort("\\o", SigSpec(State::S0, boxOutputs));
+				cell->attributes["\\abc9_box_seq"] = oldBoxNum;
 				boxes.emplace_back(cell);
 			}
 		}
@@ -770,6 +777,7 @@ void AigerReader::post_process()
 		auto ff = module->addCell(NEW_ID, "$__ABC9_FF_");
 		ff->setPort("\\D", d);
 		ff->setPort("\\Q", q);
+		ff->attributes["\\abc9_mergeability"] = mergeability[i];
 	}
 
 	dict<RTLIL::IdString, int> wideports_cache;
diff --git a/frontends/aiger/aigerparse.h b/frontends/aiger/aigerparse.h
index 722f1e472..46ac81212 100644
--- a/frontends/aiger/aigerparse.h
+++ b/frontends/aiger/aigerparse.h
@@ -45,6 +45,7 @@ struct AigerReader
     std::vector<RTLIL::Wire*> outputs;
     std::vector<RTLIL::Wire*> bad_properties;
     std::vector<RTLIL::Cell*> boxes;
+    std::vector<int> mergeability;
 
     AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports);
     void parse_aiger();
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index fb3896669..a1c8067b4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -34,13 +34,20 @@ static SigSet<sig2driver_entry_t> sig2driver, sig2user;
 static std::set<RTLIL::Cell*> muxtree_cells;
 static SigPool sig_at_port;
 
-static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, pool<Cell*> &recursion_monitor)
+static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, pool<Cell*> &recursion_monitor, dict<RTLIL::SigSpec, bool> &mux_tree_cache)
 {
+	if (mux_tree_cache.find(sig) != mux_tree_cache.end())
+		return mux_tree_cache.at(sig);
+
 	if (sig.is_fully_const() || old_sig == sig) {
+ret_true:
+		mux_tree_cache[sig] = true;
 		return true;
 	}
 
 	if (sig_at_port.check_any(assign_map(sig))) {
+ret_false:
+		mux_tree_cache[sig] = false;
 		return false;
 	}
 
@@ -49,13 +56,13 @@ static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, poo
 	for (auto &cellport : cellport_list)
 	{
 		if ((cellport.first->type != "$mux" && cellport.first->type != "$pmux") || cellport.second != "\\Y") {
-			return false;
+			goto ret_false;
 		}
 
 		if (recursion_monitor.count(cellport.first)) {
 			log_warning("logic loop in mux tree at signal %s in module %s.\n",
 					log_signal(sig), RTLIL::id2cstr(module->name));
-			return false;
+			goto ret_false;
 		}
 
 		recursion_monitor.insert(cellport.first);
@@ -63,22 +70,22 @@ static bool check_state_mux_tree(RTLIL::SigSpec old_sig, RTLIL::SigSpec sig, poo
 		RTLIL::SigSpec sig_a = assign_map(cellport.first->getPort("\\A"));
 		RTLIL::SigSpec sig_b = assign_map(cellport.first->getPort("\\B"));
 
-		if (!check_state_mux_tree(old_sig, sig_a, recursion_monitor)) {
+		if (!check_state_mux_tree(old_sig, sig_a, recursion_monitor, mux_tree_cache)) {
 			recursion_monitor.erase(cellport.first);
-			return false;
+			goto ret_false;
 		}
 
 		for (int i = 0; i < sig_b.size(); i += sig_a.size())
-			if (!check_state_mux_tree(old_sig, sig_b.extract(i, sig_a.size()), recursion_monitor)) {
+			if (!check_state_mux_tree(old_sig, sig_b.extract(i, sig_a.size()), recursion_monitor, mux_tree_cache)) {
 				recursion_monitor.erase(cellport.first);
-				return false;
+				goto ret_false;
 			}
 
 		recursion_monitor.erase(cellport.first);
 		muxtree_cells.insert(cellport.first);
 	}
 
-	return true;
+	goto ret_true;
 }
 
 static bool check_state_users(RTLIL::SigSpec sig)
@@ -143,11 +150,12 @@ static void detect_fsm(RTLIL::Wire *wire)
 		pool<Cell*> recursion_monitor;
 		RTLIL::SigSpec sig_q = assign_map(cellport.first->getPort("\\Q"));
 		RTLIL::SigSpec sig_d = assign_map(cellport.first->getPort("\\D"));
+		dict<RTLIL::SigSpec, bool> mux_tree_cache;
 
 		if (sig_q != assign_map(wire))
 			continue;
 
-		looks_like_state_reg = check_state_mux_tree(sig_q, sig_d, recursion_monitor);
+		looks_like_state_reg = check_state_mux_tree(sig_q, sig_d, recursion_monitor, mux_tree_cache);
 		looks_like_good_state_reg = check_state_users(sig_q);
 
 		if (!looks_like_state_reg)
diff --git a/passes/pmgen/ice40_dsp.cc b/passes/pmgen/ice40_dsp.cc
index f60e67158..c364cd91a 100644
--- a/passes/pmgen/ice40_dsp.cc
+++ b/passes/pmgen/ice40_dsp.cc
@@ -73,11 +73,11 @@ void create_ice40_dsp(ice40_dsp_pm &pm)
 
 	// SB_MAC16 Input Interface
 	SigSpec A = st.sigA;
-	A.extend_u0(16, st.mul->getParam(ID(A_SIGNED)).as_bool());
+	A.extend_u0(16, st.mul->parameters.at(ID(A_SIGNED), State::S0).as_bool());
 	log_assert(GetSize(A) == 16);
 
 	SigSpec B = st.sigB;
-	B.extend_u0(16, st.mul->getParam(ID(B_SIGNED)).as_bool());
+	B.extend_u0(16, st.mul->parameters.at(ID(B_SIGNED), State::S0).as_bool());
 	log_assert(GetSize(B) == 16);
 
 	SigSpec CD = st.sigCD;
@@ -248,8 +248,8 @@ void create_ice40_dsp(ice40_dsp_pm &pm)
 	cell->setParam(ID(BOTADDSUB_CARRYSELECT), Const(0, 2));
 
 	cell->setParam(ID(MODE_8x8), State::S0);
-	cell->setParam(ID(A_SIGNED), st.mul->getParam(ID(A_SIGNED)).as_bool());
-	cell->setParam(ID(B_SIGNED), st.mul->getParam(ID(B_SIGNED)).as_bool());
+	cell->setParam(ID(A_SIGNED), st.mul->parameters.at(ID(A_SIGNED), State::S0).as_bool());
+	cell->setParam(ID(B_SIGNED), st.mul->parameters.at(ID(B_SIGNED), State::S0).as_bool());
 
 	if (st.ffO) {
 		if (st.o_lo)
diff --git a/passes/pmgen/ice40_dsp.pmg b/passes/pmgen/ice40_dsp.pmg
index 6b6d2b56f..9d649cb98 100644
--- a/passes/pmgen/ice40_dsp.pmg
+++ b/passes/pmgen/ice40_dsp.pmg
@@ -56,11 +56,16 @@ code sigA sigB sigH
 			break;
 		sigH.append(O[i]);
 	}
+	// This sigM could have no users if downstream sinks (e.g. $add) is
+	//   narrower than $mul result, for example
+	if (i == 0)
+		reject;
+
 	log_assert(nusers(O.extract_end(i)) <= 1);
 endcode
 
 code argQ ffA ffAholdmux ffArstmux ffAholdpol ffArstpol sigA clock clock_pol
-	if (mul->type != \SB_MAC16 || !param(mul, \A_REG).as_bool()) {
+	if (mul->type != \SB_MAC16 || !param(mul, \A_REG, State::S0).as_bool()) {
 		argQ = sigA;
 		subpattern(in_dffe);
 		if (dff) {
@@ -81,7 +86,7 @@ code argQ ffA ffAholdmux ffArstmux ffAholdpol ffArstpol sigA clock clock_pol
 endcode
 
 code argQ ffB ffBholdmux ffBrstmux ffBholdpol ffBrstpol sigB clock clock_pol
-	if (mul->type != \SB_MAC16 || !param(mul, \B_REG).as_bool()) {
+	if (mul->type != \SB_MAC16 || !param(mul, \B_REG, State::S0).as_bool()) {
 		argQ = sigB;
 		subpattern(in_dffe);
 		if (dff) {
@@ -104,7 +109,7 @@ endcode
 code argD ffFJKG sigH clock clock_pol
 	if (nusers(sigH) == 2 &&
 			(mul->type != \SB_MAC16 ||
-			 (!param(mul, \TOP_8x8_MULT_REG).as_bool() && !param(mul, \BOT_8x8_MULT_REG).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1).as_bool()))) {
+			 (!param(mul, \TOP_8x8_MULT_REG, State::S0).as_bool() && !param(mul, \BOT_8x8_MULT_REG, State::S0).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1, State::S0).as_bool() && !param(mul, \PIPELINE_16x16_MULT_REG1, State::S0).as_bool()))) {
 		argD = sigH;
 		subpattern(out_dffe);
 		if (dff) {
@@ -143,7 +148,7 @@ endcode
 
 code argD ffH sigH sigO clock clock_pol
 	if (ffFJKG && nusers(sigH) == 2 &&
-			(mul->type != \SB_MAC16 || !param(mul, \PIPELINE_16x16_MULT_REG2).as_bool())) {
+			(mul->type != \SB_MAC16 || !param(mul, \PIPELINE_16x16_MULT_REG2, State::S0).as_bool())) {
 		argD = sigH;
 		subpattern(out_dffe);
 		if (dff) {
@@ -174,7 +179,7 @@ reject_ffH:		;
 endcode
 
 match add
-	if mul->type != \SB_MAC16 || (param(mul, \TOPOUTPUT_SELECT).as_int() == 3 && param(mul, \BOTOUTPUT_SELECT).as_int() == 3)
+	if mul->type != \SB_MAC16 || (param(mul, \TOPOUTPUT_SELECT, State::S0).as_int() == 3 && param(mul, \BOTOUTPUT_SELECT, State::S0).as_int() == 3)
 
 	select add->type.in($add)
 	choice <IdString> AB {\A, \B}
@@ -200,7 +205,7 @@ code sigCD sigO cd_signed
 		if ((actual_acc_width > actual_mul_width) && (natural_mul_width > actual_mul_width))
 			reject;
 		// If accumulator, check adder width and signedness
-		if (sigCD == sigH && (actual_acc_width != actual_mul_width) && (param(mul, \A_SIGNED).as_bool() != param(add, \A_SIGNED).as_bool()))
+		if (sigCD == sigH && (actual_acc_width != actual_mul_width) && (param(mul, \A_SIGNED, State::S0).as_bool() != param(add, \A_SIGNED).as_bool()))
 			reject;
 
 		sigO = port(add, \Y);
@@ -275,7 +280,7 @@ endcode
 
 code argQ ffCD ffCDholdmux ffCDholdpol ffCDrstpol sigCD clock clock_pol
 	if (!sigCD.empty() && sigCD != sigO &&
-			(mul->type != \SB_MAC16 || (!param(mul, \C_REG).as_bool() && !param(mul, \D_REG).as_bool()))) {
+			(mul->type != \SB_MAC16 || (!param(mul, \C_REG, State::S0).as_bool() && !param(mul, \D_REG, State::S0).as_bool()))) {
 		argQ = sigCD;
 		subpattern(in_dffe);
 		if (dff) {
@@ -328,6 +333,8 @@ arg argD argQ clock clock_pol
 
 code
 	dff = nullptr;
+	if (argQ.empty())
+		reject;
 	for (auto c : argQ.chunks()) {
 		if (!c.wire)
 			reject;
diff --git a/passes/pmgen/xilinx_dsp.pmg b/passes/pmgen/xilinx_dsp.pmg
index 5d3b9c2eb..af47ab111 100644
--- a/passes/pmgen/xilinx_dsp.pmg
+++ b/passes/pmgen/xilinx_dsp.pmg
@@ -120,7 +120,7 @@ endcode
 //      reset functionality, using a subpattern discussed above)
 //     If matched, treat 'A' input as input of ADREG
 code argQ ffAD ffADcemux ffADrstmux ffADcepol ffADrstpol sigA clock
-	if (param(dsp, \ADREG).as_int() == 0) {
+	if (param(dsp, \ADREG, 1).as_int() == 0) {
 		argQ = sigA;
 		subpattern(in_dffe);
 		if (dff) {
@@ -176,7 +176,7 @@ code argQ ffAD ffADcemux ffADrstmux ffADcepol ffADrstpol sigA clock ffA2 ffA2cem
 	// Only search for ffA2 if there was a pre-adder
 	//   (otherwise ffA2 would have been matched as ffAD)
 	if (preAdd) {
-		if (param(dsp, \AREG).as_int() == 0) {
+		if (param(dsp, \AREG, 1).as_int() == 0) {
 			argQ = sigA;
 			subpattern(in_dffe);
 			if (dff) {
@@ -237,7 +237,7 @@ endcode
 // (5) Match 'B' input for B2REG
 //     If B2REG, then match 'B' input for B1REG
 code argQ ffB2 ffB2cemux ffB2rstmux ffB2cepol ffBrstpol sigB clock ffB1 ffB1cemux ffB1rstmux ffB1cepol
-	if (param(dsp, \BREG).as_int() == 0) {
+	if (param(dsp, \BREG, 1).as_int() == 0) {
 		argQ = sigB;
 		subpattern(in_dffe);
 		if (dff) {
@@ -287,7 +287,7 @@ endcode
 
 // (6) Match 'D' input for DREG
 code argQ ffD ffDcemux ffDrstmux ffDcepol ffDrstpol sigD clock
-	if (param(dsp, \DREG).as_int() == 0) {
+	if (param(dsp, \DREG, 1).as_int() == 0) {
 		argQ = sigD;
 		subpattern(in_dffe);
 		if (dff) {
@@ -308,7 +308,7 @@ endcode
 
 // (7) Match 'P' output that exclusively drives an MREG
 code argD ffM ffMcemux ffMrstmux ffMcepol ffMrstpol sigM sigP clock
-	if (param(dsp, \MREG).as_int() == 0 && nusers(sigM) == 2) {
+	if (param(dsp, \MREG, 1).as_int() == 0 && nusers(sigM) == 2) {
 		argD = sigM;
 		subpattern(out_dffe);
 		if (dff) {
@@ -335,7 +335,7 @@ endcode
 //      recognised in xilinx_dsp.cc).
 match postAdd
 	// Ensure that Z mux is not already used
-	if port(dsp, \OPMODE, SigSpec()).extract(4,3).is_fully_zero()
+	if port(dsp, \OPMODE, SigSpec(0, 7)).extract(4,3).is_fully_zero()
 
 	select postAdd->type.in($add)
 	select GetSize(port(postAdd, \Y)) <= 48
@@ -363,7 +363,7 @@ endcode
 
 // (9) Match 'P' output that exclusively drives a PREG
 code argD ffP ffPcemux ffPrstmux ffPcepol ffPrstpol sigP clock
-	if (param(dsp, \PREG).as_int() == 0) {
+	if (param(dsp, \PREG, 1).as_int() == 0) {
 		int users = 2;
 		// If ffMcemux and no postAdd new-value net must have three users: ffMcemux, ffM and ffPcemux
 		if (ffMcemux && !postAdd) users++;
@@ -460,7 +460,7 @@ arg argD argQ clock
 
 code
 	dff = nullptr;
-	if (GetSize(argQ) == 0)
+	if (argQ.empty())
 		reject;
 	for (const auto &c : argQ.chunks()) {
 		// Abandon matches when 'Q' is a constant
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index fc3ac879e..4bb4b0edc 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -12,4 +12,5 @@ OBJS += passes/sat/supercover.o
 OBJS += passes/sat/fmcombine.o
 OBJS += passes/sat/mutate.o
 OBJS += passes/sat/cutpoint.o
+OBJS += passes/sat/fminit.o
 
diff --git a/passes/sat/fminit.cc b/passes/sat/fminit.cc
new file mode 100644
index 000000000..f3f00b382
--- /dev/null
+++ b/passes/sat/fminit.cc
@@ -0,0 +1,197 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *
+ *  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 FminitPass : public Pass {
+	FminitPass() : Pass("fminit", "set init values/sequences for formal") { }
+	void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    fminit [options] <selection>\n");
+		log("\n");
+		log("This pass creates init constraints (for example for reset sequences) in a formal\n");
+		log("model.\n");
+		log("\n");
+		log("    -seq <signal> <sequence>\n");
+		log("        Set sequence using comma-separated list of values, use 'z for\n");
+		log("        unconstrained bits. The last value is used for the remainder of the\n");
+		log("        trace.\n");
+		log("\n");
+		log("    -set <signal> <value>\n");
+		log("        Add constant value constraint\n");
+		log("\n");
+		log("    -posedge <signal>\n");
+		log("    -negedge <signal>\n");
+		log("        Set clock for init sequences\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		vector<pair<string, vector<string>>> initdata;
+		vector<pair<string, string>> setdata;
+		string clocksignal;
+		bool clockedge;
+
+		log_header(design, "Executing FMINIT pass.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			// if (args[argidx] == "-o" && argidx+1 < args.size()) {
+			// 	filename = args[++argidx];
+			// 	continue;
+			// }
+			if (args[argidx] == "-seq" && argidx+2 < args.size()) {
+				string lhs = args[++argidx];
+				string rhs = args[++argidx];
+				initdata.push_back(make_pair(lhs, split_tokens(rhs, ",")));
+				continue;
+			}
+			if (args[argidx] == "-set" && argidx+2 < args.size()) {
+				string lhs = args[++argidx];
+				string rhs = args[++argidx];
+				setdata.push_back(make_pair(lhs, rhs));
+				continue;
+			}
+			if (args[argidx] == "-posedge" && argidx+1 < args.size()) {
+				clocksignal = args[++argidx];
+				clockedge = true;
+				continue;
+			}
+			if (args[argidx] == "-negedge" && argidx+1 < args.size()) {
+				clocksignal = args[++argidx];
+				clockedge = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		Module *module = nullptr;
+
+		for (auto mod : design->selected_modules()) {
+			if (module != nullptr)
+				log_error("'fminit' requires exactly one module to be selected.\n");
+			module = mod;
+		}
+
+		if (module == nullptr)
+			log_error("'fminit' requires exactly one module to be selected.\n");
+
+		SigSpec clksig;
+		if (!clocksignal.empty()) {
+			if (!SigSpec::parse(clksig, module, clocksignal))
+				log_error("Error parsing expression '%s'.\n", clocksignal.c_str());
+		}
+
+		for (auto &it : setdata)
+		{
+			SigSpec lhs, rhs;
+
+			if (!SigSpec::parse(lhs, module, it.first))
+				log_error("Error parsing expression '%s'.\n", it.first.c_str());
+
+			if (!SigSpec::parse_rhs(lhs, rhs, module, it.second))
+				log_error("Error parsing expression '%s'.\n", it.second.c_str());
+
+			SigSpec final_lhs, final_rhs;
+
+			for (int i = 0; i < GetSize(rhs); i++)
+				if (rhs[i] != State::Sz) {
+					final_lhs.append(lhs[i]);
+					final_rhs.append(rhs[i]);
+				}
+
+			if (!final_lhs.empty()) {
+				SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs);
+				module->addAssume(NEW_ID, eq, State::S1);
+			}
+		}
+
+		vector<SigSpec> ctrlsig;
+		vector<SigSpec> ctrlsig_latched;
+
+		for (auto &it : initdata)
+		{
+			SigSpec lhs, rhs;
+
+			if (!SigSpec::parse(lhs, module, it.first))
+				log_error("Error parsing expression '%s'.\n", it.first.c_str());
+
+			for (int i = 0; i < GetSize(it.second); i++)
+			{
+				if (i >= GetSize(ctrlsig))
+				{
+					SigSpec insig = i > 0 ? ctrlsig.at(i-1) : State::S0;
+
+					Wire *outwire = module->addWire(NEW_ID);
+					outwire->attributes[ID(init)] = i > 0 ? State::S0 : State::S1;
+
+					if (clksig.empty())
+						module->addFf(NEW_ID, insig, outwire);
+					else
+						module->addDff(NEW_ID, clksig, insig, outwire, clockedge);
+
+					ctrlsig.push_back(outwire);
+					ctrlsig_latched.push_back(SigSpec());
+				}
+
+				if (i+1 == GetSize(it.second) && ctrlsig_latched[i].empty())
+				{
+					Wire *ffwire = module->addWire(NEW_ID);
+					ffwire->attributes[ID(init)] = State::S0;
+					SigSpec outsig = module->Or(NEW_ID, ffwire, ctrlsig[i]);
+
+					if (clksig.empty())
+						module->addFf(NEW_ID, outsig, ffwire);
+					else
+						module->addDff(NEW_ID, clksig, outsig, ffwire, clockedge);
+
+					ctrlsig_latched[i] = outsig;
+				}
+
+				SigSpec ctrl = i+1 == GetSize(it.second) ? ctrlsig_latched[i] : ctrlsig[i];
+
+				SigSpec final_lhs, final_rhs;
+
+				if (!SigSpec::parse_rhs(lhs, rhs, module, it.second[i]))
+					log_error("Error parsing expression '%s'.\n", it.second[i].c_str());
+
+				for (int i = 0; i < GetSize(rhs); i++)
+					if (rhs[i] != State::Sz) {
+						final_lhs.append(lhs[i]);
+						final_rhs.append(rhs[i]);
+					}
+
+				if (!final_lhs.empty()) {
+					SigSpec eq = module->Eq(NEW_ID, final_lhs, final_rhs);
+					module->addAssume(NEW_ID, eq, ctrl);
+				}
+			}
+		}
+	}
+} FminitPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index dde0a11d4..5ae2fb22a 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -240,9 +240,18 @@ struct Abc9Pass : public ScriptPass
 		}
 		extra_args(args, argidx, design);
 
+		log_assert(design);
+		if (design->selected_modules().empty()) {
+			log_warning("No modules selected for ABC9 techmapping.\n");
+			return;
+		}
+
 		log_header(design, "Executing ABC9 pass.\n");
+		log_push();
 
 		run_script(design, run_from, run_to);
+
+		log_pop();
 	}
 
 	void script() YS_OVERRIDE
@@ -284,6 +293,7 @@ struct Abc9Pass : public ScriptPass
 					}
 					log_assert(!mod->attributes.count(ID(abc9_box_id)));
 
+					log_push();
 					active_design->selection().select(mod);
 
 					if (!active_design->selected_whole_module(mod))
@@ -322,6 +332,7 @@ struct Abc9Pass : public ScriptPass
 					}
 
 					active_design->selection().selected_modules.clear();
+					log_pop();
 				}
 
 				active_design->selection_stack.pop_back();
diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc
index 484964ddf..71221951c 100644
--- a/passes/techmap/abc9_exe.cc
+++ b/passes/techmap/abc9_exe.cc
@@ -219,14 +219,14 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
 	for (size_t pos = abc9_script.find("{R}"); pos != std::string::npos; pos = abc9_script.find("{R}", pos))
 		abc9_script = abc9_script.substr(0, pos) + R + abc9_script.substr(pos+3);
 
-	abc9_script += stringf("; &ps -l; &write -n %s/output.aig;", tempdir_name.c_str());
+	abc9_script += stringf("; &ps -l; &write -n %s/output.aig", tempdir_name.c_str());
 	if (design->scratchpad_get_bool("abc9.verify")) {
 		if (dff_mode)
-			abc9_script += "verify -s;";
+			abc9_script += "; verify -s";
 		else
-			abc9_script += "verify;";
+			abc9_script += "; verify";
 	}
-	abc9_script += "time";
+	abc9_script += "; time";
 	abc9_script = add_echos_to_abc9_cmd(abc9_script);
 
 	for (size_t i = 0; i+1 < abc9_script.size(); i++)
diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc
index 13340f311..0fc4de3bb 100644
--- a/passes/techmap/abc9_ops.cc
+++ b/passes/techmap/abc9_ops.cc
@@ -184,6 +184,8 @@ void prep_dff(RTLIL::Module *module)
 		SigSpec abc9_init = assign_map(abc9_init_wire);
 		if (!abc9_init.is_fully_const())
 			log_error("'%s.init' is not a constant wire present in module '%s'.\n", cell->name.c_str(), log_id(module));
+		if (abc9_init == State::S1)
+			log_error("'%s.init' in module '%s' has value 1'b1 which is not supported by 'abc9 -dff'.\n", cell->name.c_str(), log_id(module));
 		r2 = cell->attributes.insert(std::make_pair(ID(abc9_init), abc9_init.as_const()));
 		log_assert(r2.second);
 	}
@@ -193,38 +195,44 @@ void prep_dff(RTLIL::Module *module)
 		SigMap sigmap(holes_module);
 
 		dict<SigSpec, SigSpec> replace;
-		for (auto it = holes_module->cells_.begin(); it != holes_module->cells_.end(); ) {
-			auto cell = it->second;
-			if (cell->type.in("$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
-						"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1", "$_DFF_PP0_", "$_DFF_PP1_")) {
-				SigBit D = cell->getPort("\\D");
-				SigBit Q = cell->getPort("\\Q");
-				// Remove the $_DFF_* cell from what needs to be a combinatorial box
-				it = holes_module->cells_.erase(it);
-				Wire *port;
-				if (GetSize(Q.wire) == 1)
-					port = holes_module->wire(stringf("$abc%s", Q.wire->name.c_str()));
-				else
-					port = holes_module->wire(stringf("$abc%s[%d]", Q.wire->name.c_str(), Q.offset));
-				log_assert(port);
-				// Prepare to replace "assign <port> = $_DFF_*.Q;" with "assign <port> = $_DFF_*.D;"
-				//   in order to extract just the combinatorial control logic that feeds the box
-				//   (i.e. clock enable, synchronous reset, etc.)
-				replace.insert(std::make_pair(Q,D));
-				// Since `flatten` above would have created wires named "<cell>.Q",
-				//   extract the pre-techmap cell name
-				auto pos = Q.wire->name.str().rfind(".");
-				log_assert(pos != std::string::npos);
-				IdString driver = Q.wire->name.substr(0, pos);
-				// And drive the signal that was previously driven by "DFF.Q" (typically
-				//   used to implement clock-enable functionality) with the "<cell>.$abc9_currQ"
-				//   wire (which itself is driven an by input port) we inserted above
-				Wire *currQ = holes_module->wire(stringf("%s.abc9_ff.Q", driver.c_str()));
-				log_assert(currQ);
-				holes_module->connect(Q, currQ);
-			}
+		for (auto cell : holes_module->cells().to_vector()) {
+			if (!cell->type.in("$_DFF_N_", "$_DFF_NN0_", "$_DFF_NN1_", "$_DFF_NP0_", "$_DFF_NP1_",
+						"$_DFF_P_", "$_DFF_PN0_", "$_DFF_PN1", "$_DFF_PP0_", "$_DFF_PP1_"))
+				continue;
+			SigBit D = cell->getPort("\\D");
+			SigBit Q = cell->getPort("\\Q");
+			// Emulate async control embedded inside $_DFF_* cell with mux in front of D
+			if (cell->type.in("$_DFF_NN0_", "$_DFF_PN0_"))
+				D = holes_module->MuxGate(NEW_ID, State::S0, D, cell->getPort("\\R"));
+			else if (cell->type.in("$_DFF_NN1_", "$_DFF_PN1_"))
+				D = holes_module->MuxGate(NEW_ID, State::S1, D, cell->getPort("\\R"));
+			else if (cell->type.in("$_DFF_NP0_", "$_DFF_PP0_"))
+				D = holes_module->MuxGate(NEW_ID, D, State::S0, cell->getPort("\\R"));
+			else if (cell->type.in("$_DFF_NP1_", "$_DFF_PP1_"))
+				D = holes_module->MuxGate(NEW_ID, D, State::S1, cell->getPort("\\R"));
+			// Remove the $_DFF_* cell from what needs to be a combinatorial box
+			holes_module->remove(cell);
+			Wire *port;
+			if (GetSize(Q.wire) == 1)
+				port = holes_module->wire(stringf("$abc%s", Q.wire->name.c_str()));
 			else
-				++it;
+				port = holes_module->wire(stringf("$abc%s[%d]", Q.wire->name.c_str(), Q.offset));
+			log_assert(port);
+			// Prepare to replace "assign <port> = $_DFF_*.Q;" with "assign <port> = $_DFF_*.D;"
+			//   in order to extract just the combinatorial control logic that feeds the box
+			//   (i.e. clock enable, synchronous reset, etc.)
+			replace.insert(std::make_pair(Q,D));
+			// Since `flatten` above would have created wires named "<cell>.Q",
+			//   extract the pre-techmap cell name
+			auto pos = Q.wire->name.str().rfind(".");
+			log_assert(pos != std::string::npos);
+			IdString driver = Q.wire->name.substr(0, pos);
+			// And drive the signal that was previously driven by "DFF.Q" (typically
+			//   used to implement clock-enable functionality) with the "<cell>.$abc9_currQ"
+			//   wire (which itself is driven an by input port) we inserted above
+			Wire *currQ = holes_module->wire(stringf("%s.abc9_ff.Q", driver.c_str()));
+			log_assert(currQ);
+			holes_module->connect(Q, currQ);
 		}
 
 		for (auto &conn : holes_module->connections_)
@@ -246,6 +254,8 @@ void prep_xaiger(RTLIL::Module *module, bool dff)
 	for (auto cell : module->cells()) {
 		if (cell->type == "$__ABC9_FF_")
 			continue;
+		if (cell->has_keep_attr())
+			continue;
 
 		auto inst_module = module->design->module(cell->type);
 		bool abc9_flop = inst_module && inst_module->get_bool_attribute("\\abc9_flop");
@@ -280,6 +290,7 @@ void prep_xaiger(RTLIL::Module *module, bool dff)
 		else if (!yosys_celltypes.cell_known(cell->type))
 			continue;
 
+		// TODO: Speed up toposort -- we care about box ordering only
 		for (auto conn : cell->connections()) {
 			if (cell->input(conn.first))
 				for (auto bit : sigmap(conn.second))
@@ -289,7 +300,6 @@ void prep_xaiger(RTLIL::Module *module, bool dff)
 				for (auto bit : sigmap(conn.second))
 					bit_drivers[bit].insert(cell->name);
 		}
-
 		toposort.node(cell->name);
 	}
 
@@ -589,6 +599,39 @@ void reintegrate(RTLIL::Module *module)
 	for (auto w : mapped_mod->wires())
 		module->addWire(remap_name(w->name), GetSize(w));
 
+	dict<IdString,std::vector<IdString>> box_ports;
+
+	for (auto m : design->modules()) {
+		if (!m->attributes.count(ID(abc9_box_id)))
+			continue;
+
+		auto r = box_ports.insert(m->name);
+		if (!r.second)
+			continue;
+
+		// Make carry in the last PI, and carry out the last PO
+		//   since ABC requires it this way
+		IdString carry_in, carry_out;
+		for (const auto &port_name : m->ports) {
+			auto w = m->wire(port_name);
+			log_assert(w);
+			if (w->get_bool_attribute("\\abc9_carry")) {
+				log_assert(w->port_input != w->port_output);
+				if (w->port_input)
+					carry_in = port_name;
+				else if (w->port_output)
+					carry_out = port_name;
+			}
+			else
+				r.first->second.push_back(port_name);
+		}
+
+		if (carry_in != IdString()) {
+			r.first->second.push_back(carry_in);
+			r.first->second.push_back(carry_out);
+		}
+	}
+
 	std::vector<Cell*> boxes;
 	for (auto cell : module->cells().to_vector()) {
 		if (cell->has_keep_attr())
@@ -604,10 +647,10 @@ void reintegrate(RTLIL::Module *module)
 	dict<RTLIL::Cell*,RTLIL::Cell*> not2drivers;
 	dict<SigBit, std::vector<RTLIL::Cell*>> bit2sinks;
 
-	dict<IdString,std::vector<IdString>> box_ports;
 	std::map<IdString, int> cell_stats;
 	for (auto mapped_cell : mapped_mod->cells())
 	{
+		// TODO: Speed up toposort -- we care about NOT ordering only
 		toposort.node(mapped_cell->name);
 
 		if (mapped_cell->type == ID($_NOT_)) {
@@ -690,16 +733,8 @@ void reintegrate(RTLIL::Module *module)
 			RTLIL::Cell *existing_cell = module->cell(mapped_cell->name);
 			if (!existing_cell)
 				log_error("Cannot find existing box cell with name '%s' in original design.\n", log_id(mapped_cell));
-#ifndef NDEBUG
-			RTLIL::Module* box_module = design->module(existing_cell->type);
-			IdString derived_type = box_module->derive(design, existing_cell->parameters);
-			RTLIL::Module* derived_module = design->module(derived_type);
-			log_assert(derived_module);
-			log_assert(mapped_cell->type == stringf("$__boxid%d", derived_module->attributes.at("\\abc9_box_id").as_int()));
-#endif
-			mapped_cell->type = existing_cell->type;
 
-			if (mapped_cell->type == ID($__ABC9_DELAY)) {
+			if (existing_cell->type == ID($__ABC9_DELAY)) {
 				SigBit I = mapped_cell->getPort(ID(i));
 				SigBit O = mapped_cell->getPort(ID(o));
 				if (I.wire)
@@ -710,19 +745,28 @@ void reintegrate(RTLIL::Module *module)
 				continue;
 			}
 
+#ifndef NDEBUG
+			RTLIL::Module* box_module = design->module(existing_cell->type);
+			IdString derived_type = box_module->derive(design, existing_cell->parameters);
+			RTLIL::Module* derived_module = design->module(derived_type);
+			log_assert(derived_module);
+			log_assert(mapped_cell->type == stringf("$__boxid%d", derived_module->attributes.at("\\abc9_box_id").as_int()));
+#endif
+			mapped_cell->type = existing_cell->type;
+
 			RTLIL::Cell *cell = module->addCell(remap_name(mapped_cell->name), mapped_cell->type);
 			cell->parameters = existing_cell->parameters;
 			cell->attributes = existing_cell->attributes;
 			module->swap_names(cell, existing_cell);
 
-			auto it = mapped_cell->connections_.find("\\i");
-			log_assert(it != mapped_cell->connections_.end());
-			SigSpec inputs = std::move(it->second);
-			mapped_cell->connections_.erase(it);
-			it = mapped_cell->connections_.find("\\o");
-			log_assert(it != mapped_cell->connections_.end());
-			SigSpec outputs = std::move(it->second);
-			mapped_cell->connections_.erase(it);
+			auto jt = mapped_cell->connections_.find("\\i");
+			log_assert(jt != mapped_cell->connections_.end());
+			SigSpec inputs = std::move(jt->second);
+			mapped_cell->connections_.erase(jt);
+			jt = mapped_cell->connections_.find("\\o");
+			log_assert(jt != mapped_cell->connections_.end());
+			SigSpec outputs = std::move(jt->second);
+			mapped_cell->connections_.erase(jt);
 
 			auto abc9_flop = box_module->attributes.count("\\abc9_flop");
 			if (!abc9_flop) {
@@ -734,31 +778,6 @@ void reintegrate(RTLIL::Module *module)
 						bit_drivers[i].insert(mapped_cell->name);
 			}
 
-			auto r2 = box_ports.insert(cell->type);
-			if (r2.second) {
-				// Make carry in the last PI, and carry out the last PO
-				//   since ABC requires it this way
-				IdString carry_in, carry_out;
-				for (const auto &port_name : box_module->ports) {
-					auto w = box_module->wire(port_name);
-					log_assert(w);
-					if (w->get_bool_attribute("\\abc9_carry")) {
-						log_assert(w->port_input != w->port_output);
-						if (w->port_input)
-							carry_in = port_name;
-						else if (w->port_output)
-							carry_out = port_name;
-					}
-					else
-						r2.first->second.push_back(port_name);
-				}
-
-				if (carry_in != IdString()) {
-					r2.first->second.push_back(carry_in);
-					r2.first->second.push_back(carry_out);
-				}
-			}
-
 			int input_count = 0, output_count = 0;
 			for (const auto &port_name : box_ports.at(cell->type)) {
 				RTLIL::Wire *w = box_module->wire(port_name);
@@ -847,6 +866,17 @@ void reintegrate(RTLIL::Module *module)
 		}
 	}
 
+	// ABC9 will return $_NOT_ gates in its mapping (since they are
+	//   treated as being "free"), in particular driving primary
+	//   outputs (real primary outputs, or cells treated as blackboxes)
+	//   or driving box inputs.
+	// Instead of just mapping those $_NOT_ gates into 2-input $lut-s
+	//   at an area and delay cost, see if it is possible to push
+	//   this $_NOT_ into the driving LUT, or into all sink LUTs.
+	// When this is not possible, (i.e. this signal drives two primary
+	//   outputs, only one of which is complemented) and when the driver
+	//   is a LUT, then clone the LUT so that it can be inverted without
+	//   increasing depth/delay.
 	for (auto &it : bit_users)
 		if (bit_drivers.count(it.first))
 			for (auto driver_cell : bit_drivers.at(it.first))
diff --git a/techlibs/ice40/ice40_ffinit.cc b/techlibs/ice40/ice40_ffinit.cc
index 3089d8932..c098736e9 100644
--- a/techlibs/ice40/ice40_ffinit.cc
+++ b/techlibs/ice40/ice40_ffinit.cc
@@ -78,10 +78,12 @@ struct Ice40FfinitPass : public Pass {
 						continue;
 
 					if (initbits.count(bit)) {
-						if (initbits.at(bit) != val)
-							log_error("Conflicting init values for signal %s (%s = %s, %s = %s).\n",
+						if (initbits.at(bit) != val) {
+							log_warning("Conflicting init values for signal %s (%s = %s, %s = %s).\n",
 									log_signal(bit), log_signal(SigBit(wire, i)), log_signal(val),
 									log_signal(initbit_to_wire[bit]), log_signal(initbits.at(bit)));
+							initbits.at(bit) = State::Sx;
+						}
 						continue;
 					}
 
@@ -114,6 +116,10 @@ struct Ice40FfinitPass : public Pass {
 					continue;
 
 				State val = initbits.at(bit_q);
+
+				if (val == State::Sx)
+					continue;
+
 				handled_initbits.insert(bit_q);
 
 				log("FF init value for cell %s (%s): %s = %c\n", log_id(cell), log_id(cell->type),
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index 121bcff1f..d92e40726 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -273,7 +273,8 @@ struct SynthIce40Pass : public ScriptPass
 			run("opt_expr");
 			run("opt_clean");
 			if (help_mode || dsp) {
-				run("memory_dff");
+				run("memory_dff"); // ice40_dsp will merge registers, reserve memory port registers first
+				run("wreduce t:$mul");
 				run("techmap -map +/mul2dsp.v -map +/ice40/dsp_map.v -D DSP_A_MAXWIDTH=16 -D DSP_B_MAXWIDTH=16 "
 						"-D DSP_A_MINWIDTH=2 -D DSP_B_MINWIDTH=2 -D DSP_Y_MINWIDTH=11 "
 						"-D DSP_NAME=$__MUL16X16", "(if -dsp)");
diff --git a/techlibs/xilinx/abc9_model.v b/techlibs/xilinx/abc9_model.v
index 25530acf8..782c53ab6 100644
--- a/techlibs/xilinx/abc9_model.v
+++ b/techlibs/xilinx/abc9_model.v
@@ -47,7 +47,7 @@ endmodule
 // Box to emulate async behaviour of FDP*
 (* abc9_box_id = 1001, lib_whitebox *)
 module \$__ABC9_ASYNC1 (input A, S, output Y);
-  assign Y = S ? 1'b0 : A;
+  assign Y = S ? 1'b1 : A;
 endmodule
 
 // Box to emulate comb/seq behaviour of RAM{32,64} and SRL{16,32}
diff --git a/techlibs/xilinx/arith_map.v b/techlibs/xilinx/arith_map.v
index 5c848d4e6..40c378d16 100644
--- a/techlibs/xilinx/arith_map.v
+++ b/techlibs/xilinx/arith_map.v
@@ -33,7 +33,21 @@ module _80_xilinx_lcu (P, G, CI, CO);
 
 	genvar i;
 
-`ifdef _CLB_CARRY
+`ifdef _EXPLICIT_CARRY
+
+	wire [WIDTH-1:0] C = {CO, CI};
+	wire [WIDTH-1:0] S = P & ~G;
+
+	generate for (i = 0; i < WIDTH; i = i + 1) begin:slice
+		MUXCY muxcy (
+			.CI(C[i]),
+			.DI(G[i]),
+			.S(S[i]),
+			.O(CO[i])
+		);
+	end endgenerate
+
+`else
 
 	localparam CARRY4_COUNT = (WIDTH + 3) / 4;
 	localparam MAX_WIDTH    = CARRY4_COUNT * 4;
@@ -53,9 +67,9 @@ module _80_xilinx_lcu (P, G, CI, CO);
 				(
 				.CYINIT(CI),
 				.CI    (1'd0),
-				.DI    (G [(Y_WIDTH - 1):i*4]),
-				.S     (S [(Y_WIDTH - 1):i*4]),
-				.CO    (CO[(Y_WIDTH - 1):i*4]),
+				.DI    (G [(WIDTH - 1):i*4]),
+				.S     (S [(WIDTH - 1):i*4]),
+				.CO    (CO[(WIDTH - 1):i*4]),
 				);
 			// Another one
 			end else begin
@@ -63,9 +77,9 @@ module _80_xilinx_lcu (P, G, CI, CO);
 				(
 				.CYINIT(1'd0),
 				.CI    (C [i*4 - 1]),
-				.DI    (G [(Y_WIDTH - 1):i*4]),
-				.S     (S [(Y_WIDTH - 1):i*4]),
-				.CO    (CO[(Y_WIDTH - 1):i*4]),
+				.DI    (G [(WIDTH - 1):i*4]),
+				.S     (S [(WIDTH - 1):i*4]),
+				.CO    (CO[(WIDTH - 1):i*4]),
 				);
 			end
 
@@ -97,34 +111,6 @@ module _80_xilinx_lcu (P, G, CI, CO);
 		end
 
 	end endgenerate
-
-`elsif _EXPLICIT_CARRY
-
-	wire [WIDTH-1:0] C = {CO, CI};
-	wire [WIDTH-1:0] S = P & ~G;
-
-	generate for (i = 0; i < WIDTH; i = i + 1) begin:slice
-		MUXCY muxcy (
-			.CI(C[i]),
-			.DI(G[i]),
-			.S(S[i]),
-			.O(CO[i])
-		);
-	end endgenerate
-
-`else
-
-	wire [WIDTH-1:0] C = {CO, CI};
-	wire [WIDTH-1:0] S = P & ~G;
-
-	generate for (i = 0; i < WIDTH; i = i + 1) begin:slice
-		MUXCY muxcy (
-			.CI(C[i]),
-			.DI(G[i]),
-			.S(S[i]),
-			.O(CO[i])
-		);
-	end endgenerate
 `endif
 
 endmodule
@@ -161,79 +147,7 @@ module _80_xilinx_alu (A, B, CI, BI, X, Y, CO);
 
 	genvar i;
 
-`ifdef _CLB_CARRY
-
-	localparam CARRY4_COUNT = (Y_WIDTH + 3) / 4;
-	localparam MAX_WIDTH    = CARRY4_COUNT * 4;
-	localparam PAD_WIDTH    = MAX_WIDTH - Y_WIDTH;
-
-	wire [MAX_WIDTH-1:0] S  = {{PAD_WIDTH{1'b0}}, AA ^ BB};
-	wire [MAX_WIDTH-1:0] DI = {{PAD_WIDTH{1'b0}}, AA & BB};
-
-	wire [MAX_WIDTH-1:0] C  = CO;
-
-	genvar i;
-	generate for (i = 0; i < CARRY4_COUNT; i = i + 1) begin:slice
-
-		// Partially occupied CARRY4
-		if ((i+1)*4 > Y_WIDTH) begin
-
-			// First one
-			if (i == 0) begin
-				CARRY4 carry4_1st_part
-				(
-				.CYINIT(CI),
-				.CI    (1'd0),
-				.DI    (DI[(Y_WIDTH - 1):i*4]),
-				.S     (S [(Y_WIDTH - 1):i*4]),
-				.O     (Y [(Y_WIDTH - 1):i*4]),
-				.CO    (CO[(Y_WIDTH - 1):i*4])
-				);
-			// Another one
-			end else begin
-				CARRY4 carry4_part
-				(
-				.CYINIT(1'd0),
-				.CI    (C [i*4 - 1]),
-				.DI    (DI[(Y_WIDTH - 1):i*4]),
-				.S     (S [(Y_WIDTH - 1):i*4]),
-				.O     (Y [(Y_WIDTH - 1):i*4]),
-				.CO    (CO[(Y_WIDTH - 1):i*4])
-				);
-			end
-
-		// Fully occupied CARRY4
-		end else begin
-
-			// First one
-			if (i == 0) begin
-				CARRY4 carry4_1st_full
-				(
-				.CYINIT(CI),
-				.CI    (1'd0),
-				.DI    (DI[((i+1)*4 - 1):i*4]),
-				.S     (S [((i+1)*4 - 1):i*4]),
-				.O     (Y [((i+1)*4 - 1):i*4]),
-				.CO    (CO[((i+1)*4 - 1):i*4])
-				);
-			// Another one
-			end else begin
-				CARRY4 carry4_full
-				(
-				.CYINIT(1'd0),
-				.CI    (C [i*4 - 1]),
-				.DI    (DI[((i+1)*4 - 1):i*4]),
-				.S     (S [((i+1)*4 - 1):i*4]),
-				.O     (Y [((i+1)*4 - 1):i*4]),
-				.CO    (CO[((i+1)*4 - 1):i*4])
-				);
-			end
-
-		end
-
-	end endgenerate
-
-`elsif _EXPLICIT_CARRY
+`ifdef _EXPLICIT_CARRY
 
 	wire [Y_WIDTH-1:0] S = AA ^ BB;
 	wire [Y_WIDTH-1:0] DI = AA & BB;
@@ -333,23 +247,74 @@ module _80_xilinx_alu (A, B, CI, BI, X, Y, CO);
 
 `else
 
-	wire [Y_WIDTH-1:0] S = AA ^ BB;
-	wire [Y_WIDTH-1:0] DI = AA & BB;
+	localparam CARRY4_COUNT = (Y_WIDTH + 3) / 4;
+	localparam MAX_WIDTH    = CARRY4_COUNT * 4;
+	localparam PAD_WIDTH    = MAX_WIDTH - Y_WIDTH;
 
-	wire [Y_WIDTH-1:0] C = {CO, CI};
+	wire [MAX_WIDTH-1:0] S  = {{PAD_WIDTH{1'b0}}, AA ^ BB};
+	wire [MAX_WIDTH-1:0] DI = {{PAD_WIDTH{1'b0}}, AA & BB};
+
+	wire [MAX_WIDTH-1:0] C  = CO;
+
+	genvar i;
+	generate for (i = 0; i < CARRY4_COUNT; i = i + 1) begin:slice
+
+		// Partially occupied CARRY4
+		if ((i+1)*4 > Y_WIDTH) begin
+
+			// First one
+			if (i == 0) begin
+				CARRY4 carry4_1st_part
+				(
+				.CYINIT(CI),
+				.CI    (1'd0),
+				.DI    (DI[(Y_WIDTH - 1):i*4]),
+				.S     (S [(Y_WIDTH - 1):i*4]),
+				.O     (Y [(Y_WIDTH - 1):i*4]),
+				.CO    (CO[(Y_WIDTH - 1):i*4])
+				);
+			// Another one
+			end else begin
+				CARRY4 carry4_part
+				(
+				.CYINIT(1'd0),
+				.CI    (C [i*4 - 1]),
+				.DI    (DI[(Y_WIDTH - 1):i*4]),
+				.S     (S [(Y_WIDTH - 1):i*4]),
+				.O     (Y [(Y_WIDTH - 1):i*4]),
+				.CO    (CO[(Y_WIDTH - 1):i*4])
+				);
+			end
+
+		// Fully occupied CARRY4
+		end else begin
+
+			// First one
+			if (i == 0) begin
+				CARRY4 carry4_1st_full
+				(
+				.CYINIT(CI),
+				.CI    (1'd0),
+				.DI    (DI[((i+1)*4 - 1):i*4]),
+				.S     (S [((i+1)*4 - 1):i*4]),
+				.O     (Y [((i+1)*4 - 1):i*4]),
+				.CO    (CO[((i+1)*4 - 1):i*4])
+				);
+			// Another one
+			end else begin
+				CARRY4 carry4_full
+				(
+				.CYINIT(1'd0),
+				.CI    (C [i*4 - 1]),
+				.DI    (DI[((i+1)*4 - 1):i*4]),
+				.S     (S [((i+1)*4 - 1):i*4]),
+				.O     (Y [((i+1)*4 - 1):i*4]),
+				.CO    (CO[((i+1)*4 - 1):i*4])
+				);
+			end
+
+		end
 
-	generate for (i = 0; i < Y_WIDTH; i = i + 1) begin:slice
-		MUXCY muxcy (
-			.CI(C[i]),
-			.DI(DI[i]),
-			.S(S[i]),
-			.O(CO[i])
-		);
-		XORCY xorcy (
-			.CI(C[i]),
-			.LI(S[i]),
-			.O(Y[i])
-		);
 	end endgenerate
 
 `endif
diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc
index 3dc05cd10..5c3b5179d 100644
--- a/techlibs/xilinx/synth_xilinx.cc
+++ b/techlibs/xilinx/synth_xilinx.cc
@@ -518,8 +518,6 @@ struct SynthXilinxPass : public ScriptPass
 				techmap_args += " -map +/xilinx/arith_map.v";
 				if (vpr)
 					techmap_args += " -D _EXPLICIT_CARRY";
-				else
-					techmap_args += " -D _CLB_CARRY";
 			}
 			run("techmap " + techmap_args);
 			run("opt -fast");
diff --git a/tests/arch/ice40/bug1644.il.gz b/tests/arch/ice40/bug1644.il.gz
new file mode 100644
index 000000000..363c510ef
--- /dev/null
+++ b/tests/arch/ice40/bug1644.il.gz
diff --git a/tests/arch/ice40/bug1644.ys b/tests/arch/ice40/bug1644.ys
new file mode 100644
index 000000000..5950f0e3c
--- /dev/null
+++ b/tests/arch/ice40/bug1644.ys
@@ -0,0 +1,2 @@
+read_ilang bug1644.il.gz
+synth_ice40 -top top -dsp -json adc_dac_pass_through.json -run :map_bram
diff --git a/tests/arch/ice40/ice40_dsp.ys b/tests/arch/ice40/ice40_dsp.ys
new file mode 100644
index 000000000..250273859
--- /dev/null
+++ b/tests/arch/ice40/ice40_dsp.ys
@@ -0,0 +1,11 @@
+read_verilog <<EOT
+module top(input [15:0] a, b, output [31:0] o1, o2, o5);
+SB_MAC16 m1 (.A(a), .B(16'd1234), .O(o1));
+assign o2 = a * 16'd0;
+wire [31:0] o3, o4;
+SB_MAC16 m2 (.A(a), .B(b), .O(o3));
+assign o4 = a * b;
+SB_MAC16 m3 (.A(a), .B(b), .O(o5));
+endmodule
+EOT
+ice40_dsp
diff --git a/tests/various/bug1462.ys b/tests/arch/xilinx/bug1462.ys
index 15cab5121..15cab5121 100644
--- a/tests/various/bug1462.ys
+++ b/tests/arch/xilinx/bug1462.ys
diff --git a/tests/arch/xilinx/xilinx_dsp.ys b/tests/arch/xilinx/xilinx_dsp.ys
new file mode 100644
index 000000000..3b9f52930
--- /dev/null
+++ b/tests/arch/xilinx/xilinx_dsp.ys
@@ -0,0 +1,11 @@
+read_verilog <<EOT
+module top(input [24:0] a, input [17:0] b, output [42:0] o1, o2, o5);
+DSP48E1 m1 (.A(a), .B(16'd1234), .P(o1));
+assign o2 = a * 16'd0;
+wire [42:0] o3, o4;
+DSP48E1 m2 (.A(a), .B(b), .P(o3));
+assign o4 = a * b;
+DSP48E1 m3 (.A(a), .B(b), .P(o5));
+endmodule
+EOT
+xilinx_dsp
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index 8afd0ce96..e5837d480 100644
--- a/tests/simple_abc9/abc9.v
+++ b/tests/simple_abc9/abc9.v
@@ -213,7 +213,7 @@ module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encode
   input rst;
 endmodule
 
-(* abc_box_id=1 *)
+(* abc9_box_id=1, whitebox *)
 module MUXF8(input I0, I1, S, output O);
 endmodule
 
@@ -291,3 +291,19 @@ module abc9_test035(input clk, d, output reg [1:0] q);
 always @(posedge clk) q[0] <= d;
 always @(negedge clk) q[1] <= q[0];
 endmodule
+
+module abc9_test036(input A, B, S, output [1:0] O);
+  (* keep *)
+  MUXF8 m  (
+    .I0(I0),
+    .I1(I1),
+    .O(O[0]),
+    .S(S)
+  );
+  MUXF8 m2  (
+    .I0(I0),
+    .I1(I1),
+    .O(O[1]),
+    .S(S)
+  );
+endmodule
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
index bc921daa9..32d7a80ca 100755
--- a/tests/simple_abc9/run-test.sh
+++ b/tests/simple_abc9/run-test.sh
@@ -28,4 +28,5 @@ exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p
     abc9 -lut 4 -box ../abc.box; \
     clean; \
     check -assert; \
-    select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
+    select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%; \
+    setattr -mod -unset whitebox'"
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 81d0afd1b..0c7695089 100644
--- a/tests/various/abc9.ys
+++ b/tests/various/abc9.ys
@@ -14,6 +14,7 @@ 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 abc9_test028
 proc
@@ -23,6 +24,7 @@ select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
 select -assert-count 1 t:unknown
 select -assert-none t:$lut t:unknown %% t: %D
 
+
 design -load read
 hierarchy -top abc9_test032
 proc
@@ -38,3 +40,16 @@ design -import gate -as gate
 
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -seq 10 -verify -prove-asserts -show-ports miter
+
+
+design -reset
+read_verilog -icells <<EOT
+module abc9_test036(input clk, d, output q);
+(* keep *) reg w;
+$__ABC9_FF_ ff(.D(d), .Q(w));
+wire \ff.clock = clk;
+wire \ff.init = 1'b0;
+assign q = w;
+endmodule
+EOT
+abc9 -lut 4 -dff