Merge pull request #3502 from jix/equiv_opt_fixes

equiv_opt and clk2fflogic fixes

3 files changed, 112 insertions, 185 deletions

diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 7ef2827bf..27cec7549 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -40,16 +40,6 @@ struct EquivMakeWorker
 	pool<SigBit> undriven_bits;
 	SigMap assign_map;
 
-	dict<SigBit, pool<Cell*>> bit2driven; // map: bit <--> and its driven cells
-
-	CellTypes comb_ct;
-
-	EquivMakeWorker()
-	{
-		comb_ct.setup_internals();
-		comb_ct.setup_stdcells();
-	}
-
 	void read_blacklists()
 	{
 		for (auto fn : blacklists)
@@ -147,6 +137,7 @@ struct EquivMakeWorker
 	{
 		SigMap assign_map(equiv_mod);
 		SigMap rd_signal_map;
+		SigPool primary_inputs;
 
 		// list of cells without added $equiv cells
 		auto cells_list = equiv_mod->cells().to_vector();
@@ -262,6 +253,9 @@ struct EquivMakeWorker
 				gate_wire->port_input = false;
 				equiv_mod->connect(gold_wire, wire);
 				equiv_mod->connect(gate_wire, wire);
+				primary_inputs.add(assign_map(gold_wire));
+				primary_inputs.add(assign_map(gate_wire));
+				primary_inputs.add(wire);
 			}
 			else
 			{
@@ -288,31 +282,19 @@ struct EquivMakeWorker
 			}
 		}
 
-		init_bit2driven();
-
-		pool<Cell*> visited_cells;
 		for (auto c : cells_list)
 		for (auto &conn : c->connections())
 			if (!ct.cell_output(c->type, conn.first)) {
 				SigSpec old_sig = assign_map(conn.second);
 				SigSpec new_sig = rd_signal_map(old_sig);
-
-				if(old_sig != new_sig) {
-					SigSpec tmp_sig = old_sig;
-					for (int i = 0; i < GetSize(old_sig); i++) {
-						SigBit old_bit = old_sig[i], new_bit = new_sig[i];
-
-						visited_cells.clear();
-						if (check_signal_in_fanout(visited_cells, old_bit, new_bit))
-							continue;
-
-						log("Changing input %s of cell %s (%s): %s -> %s\n",
-								log_id(conn.first), log_id(c), log_id(c->type),
-								log_signal(old_bit), log_signal(new_bit));
-
-						tmp_sig[i] = new_bit;
-					}
-					c->setPort(conn.first, tmp_sig);
+				for (int i = 0; i < GetSize(old_sig); i++)
+					if (primary_inputs.check(old_sig[i]))
+						new_sig[i] = old_sig[i];
+				if (old_sig != new_sig) {
+					log("Changing input %s of cell %s (%s): %s -> %s\n",
+							log_id(conn.first), log_id(c), log_id(c->type),
+							log_signal(old_sig), log_signal(new_sig));
+					c->setPort(conn.first, new_sig);
 				}
 			}
 
@@ -403,57 +385,6 @@ struct EquivMakeWorker
 		}
 	}
 
-	void init_bit2driven()
-	{
-		for (auto cell : equiv_mod->cells()) {
-			if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_)))
-				continue;
-			for (auto &conn : cell->connections())
-			{
-				if (yosys_celltypes.cell_input(cell->type, conn.first))
-					for (auto bit : assign_map(conn.second))
-					{
-						bit2driven[bit].insert(cell);
-					}
-			}
-		}
-	}
-
-	bool check_signal_in_fanout(pool<Cell*> & visited_cells, SigBit source_bit, SigBit target_bit)
-	{
-		if (source_bit == target_bit)
-			return true;
-
-		if (bit2driven.count(source_bit) == 0)
-			return false;
-
-		auto driven_cells = bit2driven.at(source_bit);
-		for (auto driven_cell: driven_cells)
-		{
-			bool is_comb = comb_ct.cell_known(driven_cell->type);
-			if (!is_comb)
-				continue;
-
-			if (visited_cells.count(driven_cell) > 0)
-				continue;
-			visited_cells.insert(driven_cell);
-
-			for (auto &conn: driven_cell->connections())
-			{
-				if (yosys_celltypes.cell_input(driven_cell->type, conn.first))
-					continue;
-
-				for (auto bit: conn.second) {
-					bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit);
-					if (is_in_fanout == true)
-						return true;
-				}
-			}
-		}
-
-		return false;
-	}
-
 	void run()
 	{
 		copy_to_equiv();
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 4d0400448..f5eb75730 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -60,13 +60,16 @@ struct EquivOptPass:public ScriptPass
 		log("    -undef\n");
 		log("        enable modelling of undef states during equiv_induct.\n");
 		log("\n");
+		log("    -nocheck\n");
+		log("        disable running check before and after the command under test.\n");
+		log("\n");
 		log("The following commands are executed by this verification command:\n");
 		help_script();
 		log("\n");
 	}
 
 	std::string command, techmap_opts, make_opts;
-	bool assert, undef, multiclock, async2sync;
+	bool assert, undef, multiclock, async2sync, nocheck;
 
 	void clear_flags() override
 	{
@@ -77,6 +80,7 @@ struct EquivOptPass:public ScriptPass
 		undef = false;
 		multiclock = false;
 		async2sync = false;
+		nocheck = false;
 	}
 
 	void execute(std::vector < std::string > args, RTLIL::Design * design) override
@@ -110,6 +114,10 @@ struct EquivOptPass:public ScriptPass
 				undef = true;
 				continue;
 			}
+			if (args[argidx] == "-nocheck") {
+				nocheck = true;
+				continue;
+			}
 			if (args[argidx] == "-multiclock") {
 				multiclock = true;
 				continue;
@@ -153,10 +161,14 @@ struct EquivOptPass:public ScriptPass
 		if (check_label("run_pass")) {
 			run("hierarchy -auto-top");
 			run("design -save preopt");
+			if (!nocheck)
+				run("check -assert", "(unless -nocheck)");
 			if (help_mode)
 				run("[command]");
 			else
 				run(command);
+			if (!nocheck)
+				run("check -assert", "(unless -nocheck)");
 			run("design -stash postopt");
 		}
 
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index 2384ffced..bba2cbbec 100644
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.cc
@@ -26,6 +26,11 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+struct SampledSig {
+	SigSpec sampled, current;
+	SigSpec &operator[](bool get_current) { return get_current ? current : sampled; }
+};
+
 struct Clk2fflogicPass : public Pass {
 	Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { }
 	void help() override
@@ -38,37 +43,65 @@ struct Clk2fflogicPass : public Pass {
 		log("implicit global clock. This is useful for formal verification of designs with\n");
 		log("multiple clocks.\n");
 		log("\n");
+		log("This pass assumes negative hold time for the async FF inputs. For example when\n");
+		log("a reset deasserts with the clock edge, then the FF output will still drive the\n");
+		log("reset value in the next cycle regardless of the data-in value at the time of\n");
+		log("the clock edge.\n");
+		log("\n");
 	}
-	SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, bool is_fine, IdString past_sig_id) {
-		if (!is_fine)
-			return wrap_async_control(module, sig, polarity, past_sig_id);
-		return wrap_async_control_gate(module, sig, polarity, past_sig_id);
+	// Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
+	SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
+		if (!polarity) {
+			if (is_fine)
+				sig = module->NotGate(NEW_ID, sig);
+			else
+				sig = module->Not(NEW_ID, sig);
+		}
+		std::string sig_str = log_signal(sig);
+		sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+		sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig));
+		if (is_fine)
+			module->addFfGate(NEW_ID, sig, sampled_sig);
+		else
+			module->addFf(NEW_ID, sig, sampled_sig);
+		return {sampled_sig, sig};
 	}
-	SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) {
-		Wire *past_sig = module->addWire(past_sig_id, GetSize(sig));
-		past_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S0 : State::S1, GetSize(sig));
-		module->addFf(NEW_ID, sig, past_sig);
-		if (polarity)
-			sig = module->Or(NEW_ID, sig, past_sig);
+	// Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge.
+	SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) {
+		std::string sig_str = log_signal(sig);
+		sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+		sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig));
+		if (is_fine)
+			module->addFfGate(NEW_ID, sig, sampled_sig);
 		else
-			sig = module->And(NEW_ID, sig, past_sig);
-		if (polarity)
-			return sig;
+			module->addFf(NEW_ID, sig, sampled_sig);
+		return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0});
+	}
+	// Sampled and current value of a data signal.
+	SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) {
+		std::string sig_str = log_signal(sig);
+		sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
+		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
+		sampled_sig->attributes[ID::init] = init;
+		if (is_fine)
+			module->addFfGate(NEW_ID, sig, sampled_sig);
 		else
-			return module->Not(NEW_ID, sig);
+			module->addFf(NEW_ID, sig, sampled_sig);
+		return {sampled_sig, sig};
 	}
-	SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) {
-		Wire *past_sig = module->addWire(past_sig_id);
-		past_sig->attributes[ID::init] = polarity ? State::S0 : State::S1;
-		module->addFfGate(NEW_ID, sig, past_sig);
-		if (polarity)
-			sig = module->OrGate(NEW_ID, sig, past_sig);
+	SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) {
+		if (is_fine)
+			return module->MuxGate(NEW_ID, a, b, s);
 		else
-			sig = module->AndGate(NEW_ID, sig, past_sig);
-		if (polarity)
-			return sig;
+			return module->Mux(NEW_ID, a, b, s);
+	}
+	SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) {
+		if (is_fine)
+			return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r));
 		else
-			return module->NotGate(NEW_ID, sig);
+			return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r));
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
@@ -177,96 +210,47 @@ struct Clk2fflogicPass : public Pass {
 
 					ff.remove();
 
-					// Strip spaces from signal name, since Yosys IDs can't contain spaces
-					// Spaces only occur when we have a signal that's a slice of a larger bus,
-					// e.g. "\myreg [5:0]", so removing spaces shouldn't result in loss of uniqueness
-					std::string sig_q_str = log_signal(ff.sig_q);
-					sig_q_str.erase(std::remove(sig_q_str.begin(), sig_q_str.end(), ' '), sig_q_str.end());
-
-					Wire *past_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_q_wire", sig_q_str.c_str())), ff.width);
-          
-					if (!ff.is_fine) {
-						module->addFf(NEW_ID, ff.sig_q, past_q);
-					} else {
-						module->addFfGate(NEW_ID, ff.sig_q, past_q);
-					}
-					if (!ff.val_init.is_fully_undef())
-						initvals.set_init(past_q, ff.val_init);
-
-					if (ff.has_clk) {
+					if (ff.has_clk)
 						ff.unmap_ce_srst();
 
-						Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_clk#%s", sig_q_str.c_str(), log_signal(ff.sig_clk))));
-						initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0);
-
-						if (!ff.is_fine)
-							module->addFf(NEW_ID, ff.sig_clk, past_clk);
-						else
-							module->addFfGate(NEW_ID, ff.sig_clk, past_clk);
+					auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled;
 
-						SigSpec clock_edge_pattern;
-
-						if (ff.pol_clk) {
-							clock_edge_pattern.append(State::S0);
-							clock_edge_pattern.append(State::S1);
-						} else {
-							clock_edge_pattern.append(State::S1);
-							clock_edge_pattern.append(State::S0);
-						}
-
-						SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern);
-
-						Wire *past_d = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_d_wire", sig_q_str.c_str())), ff.width);
-						if (!ff.is_fine)
-							module->addFf(NEW_ID, ff.sig_d, past_d);
-						else
-							module->addFfGate(NEW_ID, ff.sig_d, past_d);
-
-						if (!ff.val_init.is_fully_undef())
-							initvals.set_init(past_d, ff.val_init);
-
-						if (!ff.is_fine)
-							qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
-						else
-							qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge);
-					} else {
-						qval = past_q;
+					if (ff.has_clk) {
+						// The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs
+						auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
+						auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
+						next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
 					}
 
+					SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
 					// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
 					// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
 					// generating a lot of extra logic.
-					if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) {
-						SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID);
-
-						if (!ff.is_fine)
-							qval = module->Mux(NEW_ID, qval, ff.sig_ad, sig_aload);
-						else
-							qval = module->MuxGate(NEW_ID, qval, ff.sig_ad, sig_aload);
+					bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
+					if (has_nonconst_aload) {
+						sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
+						// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
+						sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
 					}
-
 					if (ff.has_sr) {
-						SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set, ff.is_fine, NEW_ID);
-						SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine, NEW_ID);
-						if (!ff.is_fine) {
-							clrval = module->Not(NEW_ID, clrval);
-							qval = module->Or(NEW_ID, qval, setval);
-							module->addAnd(NEW_ID, qval, clrval, ff.sig_q);
-						} else {
-							clrval = module->NotGate(NEW_ID, clrval);
-							qval = module->OrGate(NEW_ID, qval, setval);
-							module->addAndGate(NEW_ID, qval, clrval, ff.sig_q);
-						}
-					} else if (ff.has_arst) {
-						IdString id = NEW_ID_SUFFIX(stringf("%s#past_arst#%s", sig_q_str.c_str(), log_signal(ff.sig_arst)));
-						SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine, id);
-						if (!ff.is_fine)
-							module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q);
-						else
-							module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q);
-					} else {
-						module->connect(ff.sig_q, qval);
+						sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
+						sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
+					}
+					if (ff.has_arst)
+						sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
+
+					// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
+					// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
+					for (int current = 0; current < 2; current++) {
+						if (has_nonconst_aload)
+							next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
+						if (ff.has_sr)
+							next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
+						if (ff.has_arst)
+							next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
 					}
+
+					module->connect(ff.sig_q, next_q);
 				}
 			}
 		}