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

18 files changed, 195 insertions, 59 deletions

diff --git a/Makefile b/Makefile
index 54d508115..ac403d397 100644
--- a/Makefile
+++ b/Makefile
@@ -111,7 +111,7 @@ OBJS = kernel/version_$(GIT_REV).o
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = d1b6413
+ABCREV = 3709744
 ABCPULL = 1
 ABCURL ?= https://github.com/berkeley-abc/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 55c494996..91f238fa5 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -340,7 +340,7 @@ struct BtorWorker
 			if (cell->type == "$lt") btor_op = "lt";
 			if (cell->type == "$le") btor_op = "lte";
 			if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
-			if (cell->type.in("$ne", "$nex")) btor_op = "ne";
+			if (cell->type.in("$ne", "$nex")) btor_op = "neq";
 			if (cell->type == "$ge") btor_op = "gte";
 			if (cell->type == "$gt") btor_op = "gt";
 			log_assert(!btor_op.empty());
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 2f8715755..f6f08bb9e 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -207,9 +207,12 @@ bool RTLIL::Const::is_fully_undef() const
 	return true;
 }
 
-void RTLIL::AttrObject::set_bool_attribute(RTLIL::IdString id)
+void RTLIL::AttrObject::set_bool_attribute(RTLIL::IdString id, bool value)
 {
-	attributes[id] = RTLIL::Const(1);
+	if (value)
+		attributes[id] = RTLIL::Const(1);
+	else if (attributes.count(id))
+		attributes.erase(id);
 }
 
 bool RTLIL::AttrObject::get_bool_attribute(RTLIL::IdString id) const
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index db0a8f762..a0f1338e2 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -572,7 +572,7 @@ struct RTLIL::AttrObject
 {
 	dict<RTLIL::IdString, RTLIL::Const> attributes;
 
-	void set_bool_attribute(RTLIL::IdString id);
+	void set_bool_attribute(RTLIL::IdString id, bool value=true);
 	bool get_bool_attribute(RTLIL::IdString id) const;
 
 	bool get_blackbox_attribute(bool ignore_wb=false) const {
diff --git a/passes/cmds/setattr.cc b/passes/cmds/setattr.cc
index d38a6b3da..b9fcc3e7a 100644
--- a/passes/cmds/setattr.cc
+++ b/passes/cmds/setattr.cc
@@ -128,6 +128,45 @@ struct SetattrPass : public Pass {
 	}
 } SetattrPass;
 
+struct WbflipPass : public Pass {
+	WbflipPass() : Pass("wbflip", "flip the whitebox attribute") { }
+	void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    wbflip [selection]\n");
+		log("\n");
+		log("Flip the whitebox attribute on selected cells. I.e. if it's set, unset it, and\n");
+		log("vice-versa. Blackbox cells are not effected by this command.\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			std::string arg = args[argidx];
+			// if (arg == "-mod") {
+			// 	flag_mod = true;
+			// 	continue;
+			// }
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		for (Module *module : design->modules())
+		{
+			if (!design->selected(module))
+				continue;
+
+			if (module->get_bool_attribute("\\blackbox"))
+				continue;
+
+			module->set_bool_attribute("\\whitebox", !module->get_bool_attribute("\\whitebox"));
+		}
+	}
+} WbflipPass;
+
 struct SetparamPass : public Pass {
 	SetparamPass() : Pass("setparam", "set/unset parameters on objects") { }
 	void help() YS_OVERRIDE
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index 8b1b43f44..cf729215f 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -237,15 +237,34 @@ struct ShowWorker
 			int idx = single_idx_count++;
 			for (int rep, i = int(sig.chunks().size())-1; i >= 0; i -= rep) {
 				const RTLIL::SigChunk &c = sig.chunks().at(i);
-				net = gen_signode_simple(c, false);
-				log_assert(!net.empty());
+				if (!driver && c.wire == nullptr) {
+					RTLIL::State s1 = c.data.front();
+					for (auto s2 : c.data)
+						if (s1 != s2)
+							goto not_const_stream;
+					net.clear();
+				} else {
+			not_const_stream:
+					net = gen_signode_simple(c, false);
+					log_assert(!net.empty());
+				}
 				for (rep = 1; i-rep >= 0 && c == sig.chunks().at(i-rep); rep++) {}
 				std::string repinfo = rep > 1 ? stringf("%dx ", rep) : "";
 				if (driver) {
+					log_assert(!net.empty());
 					label_string += stringf("<s%d> %d:%d - %s%d:%d |", i, pos, pos-c.width+1, repinfo.c_str(), c.offset+c.width-1, c.offset);
 					net_conn_map[net].in.insert(stringf("x%d:s%d", idx, i));
 					net_conn_map[net].bits = rep*c.width;
 					net_conn_map[net].color = nextColor(c, net_conn_map[net].color);
+				} else
+				if (net.empty()) {
+					log_assert(rep == 1);
+					label_string += stringf("%c -&gt; %d:%d |",
+							c.data.front() == State::S0 ? '0' :
+							c.data.front() == State::S1 ? '1' :
+							c.data.front() == State::Sx ? 'X' :
+							c.data.front() == State::Sz ? 'Z' : '?',
+							pos, pos-rep*c.width+1);
 				} else {
 					label_string += stringf("<s%d> %s%d:%d - %d:%d |", i, repinfo.c_str(), c.offset+c.width-1, c.offset, pos, pos-rep*c.width+1);
 					net_conn_map[net].out.insert(stringf("x%d:s%d", idx, i));
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 86550a69b..e5dda9c24 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -134,7 +134,7 @@ struct EquivOptPass:public ScriptPass
 				opts = " -map <filename> ...";
 			else
 				opts = techmap_opts;
-			run("techmap -D EQUIV -autoproc" + opts);
+			run("techmap -wb -D EQUIV -autoproc" + opts);
 		}
 
 		if (check_label("prove")) {
diff --git a/passes/proc/proc_mux.cc b/passes/proc/proc_mux.cc
index 1329c1fef..aac0b121c 100644
--- a/passes/proc/proc_mux.cc
+++ b/passes/proc/proc_mux.cc
@@ -108,6 +108,7 @@ struct SigSnippets
 
 struct SnippetSwCache
 {
+	dict<RTLIL::SwitchRule*, pool<RTLIL::SigBit>, hash_ptr_ops> full_case_bits_cache;
 	dict<RTLIL::SwitchRule*, pool<int>, hash_ptr_ops> cache;
 	const SigSnippets *snippets;
 	int current_snippet;
@@ -268,6 +269,49 @@ void append_pmux(RTLIL::Module *mod, const RTLIL::SigSpec &signal, const std::ve
 	last_mux_cell->parameters["\\S_WIDTH"] = last_mux_cell->getPort("\\S").size();
 }
 
+const pool<SigBit> &get_full_case_bits(SnippetSwCache &swcache, RTLIL::SwitchRule *sw)
+{
+	if (!swcache.full_case_bits_cache.count(sw))
+	{
+		pool<SigBit> bits;
+
+		if (sw->get_bool_attribute("\\full_case"))
+		{
+			bool first_case = true;
+
+			for (auto cs : sw->cases)
+			{
+				pool<SigBit> case_bits;
+
+				for (auto it : cs->actions) {
+					for (auto bit : it.first)
+						case_bits.insert(bit);
+				}
+
+				for (auto it : cs->switches) {
+					for (auto bit : get_full_case_bits(swcache, it))
+						case_bits.insert(bit);
+				}
+
+				if (first_case) {
+					first_case = false;
+					bits = case_bits;
+				} else {
+					pool<SigBit> new_bits;
+					for (auto bit : bits)
+						if (case_bits.count(bit))
+							new_bits.insert(bit);
+					bits.swap(new_bits);
+				}
+			}
+		}
+
+		bits.swap(swcache.full_case_bits_cache[sw]);
+	}
+
+	return swcache.full_case_bits_cache.at(sw);
+}
+
 RTLIL::SigSpec signal_to_mux_tree(RTLIL::Module *mod, SnippetSwCache &swcache, dict<RTLIL::SwitchRule*, bool, hash_ptr_ops> &swpara,
 		RTLIL::CaseRule *cs, const RTLIL::SigSpec &sig, const RTLIL::SigSpec &defval, bool ifxmode)
 {
@@ -337,6 +381,12 @@ RTLIL::SigSpec signal_to_mux_tree(RTLIL::Module *mod, SnippetSwCache &swcache, d
 			}
 		}
 
+		// mask default bits that are irrelevant because the output is driven by a full case
+		const pool<SigBit> &full_case_bits = get_full_case_bits(swcache, sw);
+		for (int i = 0; i < GetSize(sig); i++)
+			if (full_case_bits.count(sig[i]))
+				result[i] = State::Sx;
+
 		// evaluate in reverse order to give the first entry the top priority
 		RTLIL::SigSpec initial_val = result;
 		RTLIL::Cell *last_mux_cell = NULL;
diff --git a/passes/proc/proc_rmdead.cc b/passes/proc/proc_rmdead.cc
index 7c334e661..4f40be446 100644
--- a/passes/proc/proc_rmdead.cc
+++ b/passes/proc/proc_rmdead.cc
@@ -28,7 +28,7 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-void proc_rmdead(RTLIL::SwitchRule *sw, int &counter)
+void proc_rmdead(RTLIL::SwitchRule *sw, int &counter, int &full_case_counter)
 {
 	BitPatternPool pool(sw->signal);
 
@@ -56,11 +56,16 @@ void proc_rmdead(RTLIL::SwitchRule *sw, int &counter)
 		}
 
 		for (auto switch_it : sw->cases[i]->switches)
-			proc_rmdead(switch_it, counter);
+			proc_rmdead(switch_it, counter, full_case_counter);
 
 		if (is_default)
 			pool.take_all();
 	}
+
+	if (pool.empty() && !sw->get_bool_attribute("\\full_case")) {
+		sw->set_bool_attribute("\\full_case");
+		full_case_counter++;
+	}
 }
 
 struct ProcRmdeadPass : public Pass {
@@ -87,12 +92,15 @@ struct ProcRmdeadPass : public Pass {
 			for (auto &proc_it : mod->processes) {
 				if (!design->selected(mod, proc_it.second))
 					continue;
-				int counter = 0;
+				int counter = 0, full_case_counter = 0;
 				for (auto switch_it : proc_it.second->root_case.switches)
-					proc_rmdead(switch_it, counter);
+					proc_rmdead(switch_it, counter, full_case_counter);
 				if (counter > 0)
 					log("Removed %d dead cases from process %s in module %s.\n", counter,
-							proc_it.first.c_str(), log_id(mod));
+							log_id(proc_it.first), log_id(mod));
+				if (full_case_counter > 0)
+					log("Marked %d switch rules as full_case in process %s in module %s.\n",
+							full_case_counter, log_id(proc_it.first), log_id(mod));
 				total_counter += counter;
 			}
 		}
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index d37f1b126..1a886af70 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -254,7 +254,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 
 	if (flag_flatten) {
 		log_push();
-		Pass::call_on_module(design, miter_module, "flatten; opt_expr -keepdc -undriven;;");
+		Pass::call_on_module(design, miter_module, "flatten -wb; opt_expr -keepdc -undriven;;");
 		log_pop();
 	}
 }
@@ -308,7 +308,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
 
 	if (flag_flatten) {
 		log_push();
-		Pass::call_on_module(design, module, "flatten;;");
+		Pass::call_on_module(design, module, "flatten -wb;;");
 		log_pop();
 	}
 
@@ -385,7 +385,7 @@ struct MiterPass : public Pass {
 		log("        also create an 'assert' cell that checks if trigger is always low.\n");
 		log("\n");
 		log("    -flatten\n");
-		log("        call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
+		log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
 		log("\n");
 		log("\n");
 		log("    miter -assert [options] module [miter_name]\n");
@@ -399,7 +399,7 @@ struct MiterPass : public Pass {
 		log("        keep module output ports.\n");
 		log("\n");
 		log("    -flatten\n");
-		log("        call 'flatten; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
+		log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
 		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 21b70f492..547115459 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -29,17 +29,17 @@
 // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558-562, doi:10.1145/368996.369025
 // http://en.wikipedia.org/wiki/Topological_sorting
 
-#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_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"
-
-#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 "strash; dretime; if"
-#define ABC_FAST_COMMAND_SOP "strash; dretime; cover -I {I} -P {P}"
-#define ABC_FAST_COMMAND_DFL "strash; dretime; map"
+#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; retime {D}; strash; &get -n; &dch -f; &nf {D}; &put"
+#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; retime {D}; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p"
+#define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; retime {D}; strash; dch -f; if; mfs2"
+#define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; retime {D}; strash; dch -f; cover {I} {P}"
+#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; retime {D}; strash; &get -n; &dch -f; &nf {D}; &put"
+
+#define ABC_FAST_COMMAND_LIB "strash; dretime; retime {D}; map {D}"
+#define ABC_FAST_COMMAND_CTR "strash; dretime; retime {D}; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
+#define ABC_FAST_COMMAND_LUT "strash; dretime; retime {D}; if"
+#define ABC_FAST_COMMAND_SOP "strash; dretime; retime {D}; cover -I {I} -P {P}"
+#define ABC_FAST_COMMAND_DFL "strash; dretime; retime {D}; map"
 
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -331,19 +331,23 @@ std::string remap_name(RTLIL::IdString abc_name, RTLIL::Wire **orig_wire = nullp
 {
 	std::string abc_sname = abc_name.substr(1);
 	if (abc_sname.substr(0, 5) == "ys__n") {
-		int sid = std::stoi(abc_sname.substr(5));
 		bool inv = abc_sname.back() == 'v';
-		for (auto sig : signal_list) {
-			if (sig.id == sid && sig.bit.wire != nullptr) {
-				std::stringstream sstr;
-				sstr << "$abc$" << map_autoidx << "$" << sig.bit.wire->name.substr(1);
-				if (sig.bit.wire->width != 1)
-					sstr << "[" << sig.bit.offset << "]";
-				if (inv)
-					sstr << "_inv";
-				if (orig_wire != nullptr)
-					*orig_wire = sig.bit.wire;
-				return sstr.str();
+		if (inv) abc_sname.pop_back();
+		abc_sname.erase(0, 5);
+		if (abc_sname.find_last_not_of("012345689") == std::string::npos) {
+			int sid = std::stoi(abc_sname);
+			for (auto sig : signal_list) {
+				if (sig.id == sid && sig.bit.wire != nullptr) {
+					std::stringstream sstr;
+					sstr << "$abc$" << map_autoidx << "$" << sig.bit.wire->name.substr(1);
+					if (sig.bit.wire->width != 1)
+						sstr << "[" << sig.bit.offset << "]";
+					if (inv)
+						sstr << "_inv";
+					if (orig_wire != nullptr)
+						*orig_wire = sig.bit.wire;
+					return sstr.str();
+				}
 			}
 		}
 	}
@@ -731,10 +735,6 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	else
 		abc_script += fast_mode ? ABC_FAST_COMMAND_DFL : ABC_COMMAND_DFL;
 
-	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);
 
@@ -1726,7 +1726,7 @@ struct AbcPass : public Pass {
 								signal_init[initsig[i]] = State::S0;
 								break;
 							case State::S1:
-								signal_init[initsig[i]] = State::S0;
+								signal_init[initsig[i]] = State::S1;
 								break;
 							default:
 								break;
diff --git a/passes/techmap/pmuxtree.cc b/passes/techmap/pmuxtree.cc
index b7a22dc3b..6a923f481 100644
--- a/passes/techmap/pmuxtree.cc
+++ b/passes/techmap/pmuxtree.cc
@@ -71,9 +71,9 @@ struct PmuxtreePass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    pmuxtree [options] [selection]\n");
+		log("    pmuxtree [selection]\n");
 		log("\n");
-		log("This pass transforms $pmux cells to a trees of $mux cells.\n");
+		log("This pass transforms $pmux cells to trees of $mux cells.\n");
 		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index 660b60601..f3da80c66 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -599,7 +599,7 @@ struct SimplemapPass : public Pass {
 		simplemap_get_mappers(mappers);
 
 		for (auto mod : design->modules()) {
-			if (!design->selected(mod))
+			if (!design->selected(mod) || mod->get_blackbox_attribute())
 				continue;
 			std::vector<RTLIL::Cell*> cells = mod->cells();
 			for (auto cell : cells) {
diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc
index 82c815e2e..ee319b6e6 100644
--- a/passes/techmap/techmap.cc
+++ b/passes/techmap/techmap.cc
@@ -385,7 +385,7 @@ struct TechmapWorker
 	{
 		std::string mapmsg_prefix = in_recursion ? "Recursively mapping" : "Mapping";
 
-		if (!design->selected(module))
+		if (!design->selected(module) || module->get_blackbox_attribute(ignore_wb))
 			return false;
 
 		bool log_continue = false;
@@ -927,6 +927,9 @@ struct TechmapPass : public Pass {
 		log("    -autoproc\n");
 		log("        Automatically call \"proc\" on implementations that contain processes.\n");
 		log("\n");
+		log("    -wb\n");
+		log("        Ignore the 'whitebox' attribute on cell implementations.\n");
+		log("\n");
 		log("    -assert\n");
 		log("        this option will cause techmap to exit with an error if it can't map\n");
 		log("        a selected cell. only cell types that end on an underscore are accepted\n");
@@ -1070,6 +1073,10 @@ struct TechmapPass : public Pass {
 				worker.autoproc_mode = true;
 				continue;
 			}
+			if (args[argidx] == "-wb") {
+				worker.ignore_wb = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
diff --git a/techlibs/xilinx/ff_map.v b/techlibs/xilinx/ff_map.v
index 13beaa6ae..3d5f78770 100644
--- a/techlibs/xilinx/ff_map.v
+++ b/techlibs/xilinx/ff_map.v
@@ -28,14 +28,14 @@ module  \$_DFF_P_   (input D, C, output Q);    FDRE   #(.INIT(|0)) _TECHMAP_REPL
 module  \$_DFFE_NP_ (input D, C, E, output Q); FDRE_1 #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E),    .R(1'b0)); endmodule
 module  \$_DFFE_PP_ (input D, C, E, output Q); FDRE   #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(E),    .R(1'b0)); endmodule
 
-module  \$_DFF_NN0_ (input D, C, R, output Q); FDCE_1 #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .CLR(!R)); endmodule
+module  \$_DFF_NN0_ (input D, C, R, output Q); \$_DFF_NP0_         _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C),              .R(~R)); endmodule
 module  \$_DFF_NP0_ (input D, C, R, output Q); FDCE_1 #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .CLR( R)); endmodule
-module  \$_DFF_PN0_ (input D, C, R, output Q); FDCE   #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .CLR(!R)); endmodule
+module  \$_DFF_PN0_ (input D, C, R, output Q); \$_DFF_PP0_         _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C),              .R(~R)); endmodule
 module  \$_DFF_PP0_ (input D, C, R, output Q); FDCE   #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .CLR( R)); endmodule
 
-module  \$_DFF_NN1_ (input D, C, R, output Q); FDPE_1 #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .PRE(!R)); endmodule
+module  \$_DFF_NN1_ (input D, C, R, output Q); \$_DFF_NP1          _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C),              .R(~R)); endmodule
 module  \$_DFF_NP1_ (input D, C, R, output Q); FDPE_1 #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .PRE( R)); endmodule
-module  \$_DFF_PN1_ (input D, C, R, output Q); FDPE   #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .PRE(!R)); endmodule
+module  \$_DFF_PN1_ (input D, C, R, output Q); \$_DFF_PP1          _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C),              .R(~R)); endmodule
 module  \$_DFF_PP1_ (input D, C, R, output Q); FDPE   #(.INIT(|0)) _TECHMAP_REPLACE_ (.D(D), .Q(Q), .C(C), .CE(1'b1), .PRE( R)); endmodule
 
 `endif
diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc
index 090bcce85..8a531c497 100644
--- a/techlibs/xilinx/synth_xilinx.cc
+++ b/techlibs/xilinx/synth_xilinx.cc
@@ -113,13 +113,14 @@ struct SynthXilinxPass : public Pass
 		log("        dffsr2dff\n");
 		log("        dff2dffe\n");
 		log("        opt -full\n");
-		log("        techmap -map +/techmap.v -map +/xilinx/arith_map.v -map +/xilinx/ff_map.v\n");
+		log("        techmap -map +/techmap.v -map +/xilinx/arith_map.v\n");
 		log("        opt -fast\n");
 		log("\n");
 		log("    map_luts:\n");
-		log("        abc -luts 2:2,3,6:5,10,20 [-dff] (without '-vpr' only!)\n");
-		log("        abc -lut 5 [-dff] (with '-vpr' only!)\n");
+		log("        techmap -map +/techmap.v -map +/xilinx/ff_map.v t:$_DFF_?N?\n");
+		log("        abc -luts 2:2,3,6:5,10,20 [-dff]\n");
 		log("        clean\n");
+		log("        techmap -map +/xilinx/lut_map.v -map +/xilinx/ff_map.v");
 		log("\n");
 		log("    map_cells:\n");
 		log("        techmap -map +/xilinx/cells_map.v\n");
@@ -264,9 +265,9 @@ struct SynthXilinxPass : public Pass
 			Pass::call(design, "opt -full");
 
 			if (vpr) {
-				Pass::call(design, "techmap -map +/techmap.v -map +/xilinx/arith_map.v -map +/xilinx/ff_map.v -D _EXPLICIT_CARRY");
+				Pass::call(design, "techmap -map +/techmap.v -map +/xilinx/arith_map.v -D _EXPLICIT_CARRY");
 			} else {
-				Pass::call(design, "techmap -map +/techmap.v -map +/xilinx/arith_map.v -map +/xilinx/ff_map.v");
+				Pass::call(design, "techmap -map +/techmap.v -map +/xilinx/arith_map.v");
 			}
 
 			Pass::call(design, "hierarchy -check");
@@ -275,9 +276,10 @@ struct SynthXilinxPass : public Pass
 
 		if (check_label(active, run_from, run_to, "map_luts"))
 		{
+			Pass::call(design, "techmap -map +/techmap.v -map +/xilinx/ff_map.v t:$_DFF_?N?");
 			Pass::call(design, abc + " -luts 2:2,3,6:5,10,20" + string(retime ? " -dff" : ""));
 			Pass::call(design, "clean");
-			Pass::call(design, "techmap -map +/xilinx/lut_map.v");
+			Pass::call(design, "techmap -map +/xilinx/lut_map.v -map +/xilinx/ff_map.v");
 		}
 
 		if (check_label(active, run_from, run_to, "map_cells"))
diff --git a/tests/aiger/.gitignore b/tests/aiger/.gitignore
new file mode 100644
index 000000000..073f46157
--- /dev/null
+++ b/tests/aiger/.gitignore
@@ -0,0 +1,2 @@
+*.log
+*.out
diff --git a/tests/simple/retime.v b/tests/simple/retime.v
new file mode 100644
index 000000000..30b6087dc
--- /dev/null
+++ b/tests/simple/retime.v
@@ -0,0 +1,6 @@
+module retime_test(input clk, input [7:0] a, output z);
+    reg [7:0] ff = 8'hF5;
+    always @(posedge clk)
+        ff <= {ff[6:0], ^a};
+    assign z = ff[7];
+endmodule