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

7 files changed, 85 insertions, 7 deletions

diff --git a/passes/cmds/qwp.cc b/passes/cmds/qwp.cc
index 1c64a7b77..adbe89e31 100644
--- a/passes/cmds/qwp.cc
+++ b/passes/cmds/qwp.cc
@@ -291,7 +291,7 @@ struct QwpWorker
 		// gaussian elimination
 		for (int i = 0; i < N; i++)
 		{
-			if (config.verbose && ((i+1) % (N/15)) == 0)
+			if (config.verbose && N > 15 && ((i+1) % (N/15)) == 0)
 				log("> Solved %d%%: %d/%d\n", (100*(i+1))/N, i+1, N);
 
 			// find best row
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index e5dda9c24..3596dfd7b 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -44,7 +44,10 @@ struct EquivOptPass:public ScriptPass
 		log("        useful for handling architecture-specific primitives.\n");
 		log("\n");
 		log("    -assert\n");
-		log("        produce an error if the circuits are not equivalent\n");
+		log("        produce an error if the circuits are not equivalent.\n");
+		log("\n");
+		log("    -undef\n");
+		log("        enable modelling of undef states during equiv_induct.\n");
 		log("\n");
 		log("The following commands are executed by this verification command:\n");
 		help_script();
@@ -52,13 +55,14 @@ struct EquivOptPass:public ScriptPass
 	}
 
 	std::string command, techmap_opts;
-	bool assert;
+	bool assert, undef;
 
 	void clear_flags() YS_OVERRIDE
 	{
 		command = "";
 		techmap_opts = "";
 		assert = false;
+		undef = false;
 	}
 
 	void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@@ -84,6 +88,10 @@ struct EquivOptPass:public ScriptPass
 				assert = true;
 				continue;
 			}
+			if (args[argidx] == "-undef") {
+				undef = true;
+				continue;
+			}
 			break;
 		}
 
@@ -139,7 +147,12 @@ struct EquivOptPass:public ScriptPass
 
 		if (check_label("prove")) {
 			run("equiv_make gold gate equiv");
-			run("equiv_induct equiv");
+			if (help_mode)
+				run("equiv_induct [-undef] equiv");
+			else if (undef)
+				run("equiv_induct -undef equiv");
+			else
+				run("equiv_induct equiv");
 			if (help_mode)
 				run("equiv_status [-assert] equiv");
 			else if (assert)
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index c38e9df5e..5d95c4f1a 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -281,13 +281,26 @@ void rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 				maybe_del_wires.push_back(wire);
 			} else {
 				log_assert(GetSize(s1) == GetSize(s2));
+				Const initval;
+				if (wire->attributes.count("\\init"))
+					initval = wire->attributes.at("\\init");
+				if (GetSize(initval) != GetSize(wire))
+					initval.bits.resize(GetSize(wire), State::Sx);
 				RTLIL::SigSig new_conn;
 				for (int i = 0; i < GetSize(s1); i++)
 					if (s1[i] != s2[i]) {
+						if (s2[i] == State::Sx && (initval[i] == State::S0 || initval[i] == State::S1)) {
+							s2[i] = initval[i];
+							initval[i] = State::Sx;
+						}
 						new_conn.first.append_bit(s1[i]);
 						new_conn.second.append_bit(s2[i]);
 					}
 				if (new_conn.first.size() > 0) {
+					if (initval.is_fully_undef())
+						wire->attributes.erase("\\init");
+					else
+						wire->attributes.at("\\init") = initval;
 					used_signals.add(new_conn.first);
 					used_signals.add(new_conn.second);
 					module->connect(new_conn);
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index af6d352af..b445afdc8 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -39,6 +39,9 @@ void replace_undriven(RTLIL::Design *design, RTLIL::Module *module)
 	SigPool used_signals;
 	SigPool all_signals;
 
+	dict<SigBit, pair<Wire*, State>> initbits;
+	pool<Wire*> revisit_initwires;
+
 	for (auto cell : module->cells())
 	for (auto &conn : cell->connections()) {
 		if (!ct.cell_known(cell->type) || ct.cell_output(cell->type, conn.first))
@@ -48,6 +51,14 @@ void replace_undriven(RTLIL::Design *design, RTLIL::Module *module)
 	}
 
 	for (auto wire : module->wires()) {
+		if (wire->attributes.count("\\init")) {
+			SigSpec sig = sigmap(wire);
+			Const initval = wire->attributes.at("\\init");
+			for (int i = 0; i < GetSize(initval) && i < GetSize(wire); i++) {
+				if (initval[i] == State::S0 || initval[i] == State::S1)
+					initbits[sig[i]] = make_pair(wire, initval[i]);
+			}
+		}
 		if (wire->port_input)
 			driven_signals.add(sigmap(wire));
 		if (wire->port_output)
@@ -67,10 +78,38 @@ void replace_undriven(RTLIL::Design *design, RTLIL::Module *module)
 		if (sig.size() == 0)
 			continue;
 
-		log_debug("Setting undriven signal in %s to undef: %s\n", RTLIL::id2cstr(module->name), log_signal(c));
-		module->connect(RTLIL::SigSig(c, RTLIL::SigSpec(RTLIL::State::Sx, c.width)));
+		Const val(RTLIL::State::Sx, GetSize(sig));
+		for (int i = 0; i < GetSize(sig); i++) {
+			SigBit bit = sigmap(sig[i]);
+			auto cursor = initbits.find(bit);
+			if (cursor != initbits.end()) {
+				revisit_initwires.insert(cursor->second.first);
+				val[i] = cursor->second.second;
+			}
+		}
+
+		log_debug("Setting undriven signal in %s to constant: %s = %s\n", RTLIL::id2cstr(module->name), log_signal(sig), log_signal(val));
+		module->connect(sig, val);
 		did_something = true;
 	}
+
+	if (!revisit_initwires.empty())
+	{
+		SigMap sm2(module);
+
+		for (auto wire : revisit_initwires) {
+			SigSpec sig = sm2(wire);
+			Const initval = wire->attributes.at("\\init");
+			for (int i = 0; i < GetSize(initval) && i < GetSize(wire); i++) {
+				if (SigBit(initval[i]) == sig[i])
+					initval[i] = State::Sx;
+			}
+			if (initval.is_fully_undef())
+				wire->attributes.erase("\\init");
+			else
+				wire->attributes["\\init"] = initval;
+		}
+	}
 }
 
 void replace_cell(SigMap &assign_map, RTLIL::Module *module, RTLIL::Cell *cell, std::string info, std::string out_port, RTLIL::SigSpec out_val)
diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc
index 68e077cf9..41de8aad1 100644
--- a/passes/opt/wreduce.cc
+++ b/passes/opt/wreduce.cc
@@ -180,6 +180,8 @@ struct WreduceWorker
 			}
 
 			auto info = mi.query(sig_q[i]);
+			if (info == nullptr)
+				return;
 			if (!info->is_output && GetSize(info->ports) == 1 && !keep_bits.count(mi.sigmap(sig_q[i]))) {
 				remove_init_bits.insert(sig_q[i]);
 				sig_d.remove(i);
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 695a03e15..cbba738f0 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -1169,6 +1169,7 @@ struct SatPass : public Pass {
 			if (args[argidx] == "-tempinduct-def") {
 				tempinduct = true;
 				tempinduct_def = true;
+				enable_undef = true;
 				continue;
 			}
 			if (args[argidx] == "-tempinduct-baseonly") {
diff --git a/passes/techmap/shregmap.cc b/passes/techmap/shregmap.cc
index a541b33be..75eedfbcc 100644
--- a/passes/techmap/shregmap.cc
+++ b/passes/techmap/shregmap.cc
@@ -178,7 +178,17 @@ struct ShregmapTechXilinx7 : ShregmapTech
 
 		// Only map if $shiftx exclusively covers the shift register
 		if (shiftx->type == "$shiftx") {
-			if (GetSize(taps) != shiftx->getParam("\\A_WIDTH").as_int())
+			if (GetSize(taps) > shiftx->getParam("\\A_WIDTH").as_int())
+				return false;
+			// Due to padding the most significant bits of A may be 1'bx,
+			//   and if so, discount them
+			if (GetSize(taps) < shiftx->getParam("\\A_WIDTH").as_int()) {
+				const SigSpec A = shiftx->getPort("\\A");
+				const int A_width = shiftx->getParam("\\A_WIDTH").as_int();
+				for (int i = GetSize(taps); i < A_width; ++i)
+					if (A[i] != RTLIL::Sx) return false;
+			}
+			else if (GetSize(taps) != shiftx->getParam("\\A_WIDTH").as_int())
 				return false;
 		}
 		else if (shiftx->type == "$mux") {