Refactor "opt_rmdff -sat"

Signed-off-by: Clifford Wolf <clifford@clifford.at>

2 files changed, 46 insertions, 359 deletions

diff --git a/passes/opt/netlist.h b/passes/opt/netlist.h
deleted file mode 100644
index f029ad6ab..000000000
--- a/passes/opt/netlist.h
+++ /dev/null
@@ -1,317 +0,0 @@
-/* -*- c++ -*-
- *  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.
- *
- */
-
-#ifndef SATGEN_ALGO_H
-#define SATGEN_ALGO_H
-
-#include "kernel/celltypes.h"
-#include "kernel/rtlil.h"
-#include "kernel/sigtools.h"
-#include <stack>
-
-YOSYS_NAMESPACE_BEGIN
-
-CellTypes comb_cells_filt()
-{
-	CellTypes ct;
-
-	ct.setup_internals();
-	ct.setup_stdcells();
-
-	return ct;
-}
-
-struct Netlist {
-	RTLIL::Module *module;
-	SigMap sigmap;
-	CellTypes ct;
-	dict<RTLIL::SigBit, Cell *> sigbit_driver_map;
-	dict<RTLIL::Cell *, std::set<RTLIL::SigBit>> cell_inputs_map;
-
-	Netlist(RTLIL::Module *module) : module(module), sigmap(module), ct(module->design) { setup_netlist(module, ct); }
-
-	Netlist(RTLIL::Module *module, const CellTypes &ct) : module(module), sigmap(module), ct(ct) { setup_netlist(module, ct); }
-
-	RTLIL::Cell *driver_cell(RTLIL::SigBit sig) const
-	{
-		sig = sigmap(sig);
-		if (!sigbit_driver_map.count(sig)) {
-			return NULL;
-		}
-
-		return sigbit_driver_map.at(sig);
-	}
-
-	RTLIL::SigSpec driver_port(RTLIL::SigBit sig)
-	{
-		RTLIL::Cell *cell = driver_cell(sig);
-
-		if (!cell) {
-			return RTLIL::SigSpec();
-		}
-
-		for (auto &port : cell->connections_) {
-			if (ct.cell_output(cell->type, port.first)) {
-				RTLIL::SigSpec port_sig = sigmap(port.second);
-				for (int i = 0; i < GetSize(port_sig); i++) {
-					if (port_sig[i] == sig) {
-						return port.second[i];
-					}
-				}
-			}
-		}
-
-		return RTLIL::SigSpec();
-	}
-
-	void setup_netlist(RTLIL::Module *module, const CellTypes &ct)
-	{
-		for (auto cell : module->cells()) {
-			if (ct.cell_known(cell->type)) {
-				std::set<RTLIL::SigBit> inputs, outputs;
-				for (auto &port : cell->connections()) {
-					std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
-					if (ct.cell_output(cell->type, port.first))
-						outputs.insert(bits.begin(), bits.end());
-					else
-						inputs.insert(bits.begin(), bits.end());
-				}
-				cell_inputs_map[cell] = inputs;
-				for (auto &bit : outputs) {
-					sigbit_driver_map[bit] = cell;
-				};
-			}
-		}
-	}
-};
-
-namespace detail
-{
-struct NetlistConeWireIter : public std::iterator<std::input_iterator_tag, RTLIL::SigBit> {
-	using set_iter_t = std::set<RTLIL::SigBit>::iterator;
-
-	const Netlist &net;
-	RTLIL::SigBit sig;
-	bool sentinel;
-	CellTypes *cell_filter;
-
-	std::stack<std::pair<set_iter_t, set_iter_t>> dfs_path_stack;
-	std::set<RTLIL::Cell *> cells_visited;
-
-	NetlistConeWireIter(const Netlist &net) : net(net), sentinel(true), cell_filter(NULL) {}
-
-	NetlistConeWireIter(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL)
-	    : net(net), sig(sig), sentinel(false), cell_filter(cell_filter)
-	{
-	}
-
-	const RTLIL::SigBit &operator*() const { return sig; };
-	bool operator!=(const NetlistConeWireIter &other) const
-	{
-		if (sentinel || other.sentinel) {
-			return sentinel != other.sentinel;
-		} else {
-			return sig != other.sig;
-		}
-	}
-
-	bool operator==(const NetlistConeWireIter &other) const
-	{
-		if (sentinel || other.sentinel) {
-			return sentinel == other.sentinel;
-		} else {
-			return sig == other.sig;
-		}
-	}
-
-	void next_sig_in_dag()
-	{
-		while (1) {
-			if (dfs_path_stack.empty()) {
-				sentinel = true;
-				return;
-			}
-
-			auto &cell_inputs_iter = dfs_path_stack.top().first;
-			auto &cell_inputs_iter_guard = dfs_path_stack.top().second;
-
-			cell_inputs_iter++;
-			if (cell_inputs_iter != cell_inputs_iter_guard) {
-				sig = *cell_inputs_iter;
-				return;
-			} else {
-				dfs_path_stack.pop();
-			}
-		}
-	}
-
-	NetlistConeWireIter &operator++()
-	{
-		RTLIL::Cell *cell = net.driver_cell(sig);
-
-		if (!cell) {
-			next_sig_in_dag();
-			return *this;
-		}
-
-		if (cells_visited.count(cell)) {
-			next_sig_in_dag();
-			return *this;
-		}
-
-		if ((cell_filter) && (!cell_filter->cell_known(cell->type))) {
-			next_sig_in_dag();
-			return *this;
-		}
-
-		auto &inputs = net.cell_inputs_map.at(cell);
-		dfs_path_stack.push(std::make_pair(inputs.begin(), inputs.end()));
-		cells_visited.insert(cell);
-		sig = (*dfs_path_stack.top().first);
-		return *this;
-	}
-};
-
-struct NetlistConeWireIterable {
-	const Netlist &net;
-	RTLIL::SigBit sig;
-	CellTypes *cell_filter;
-
-	NetlistConeWireIterable(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig(sig), cell_filter(cell_filter)
-	{
-	}
-
-	NetlistConeWireIter begin() { return NetlistConeWireIter(net, sig, cell_filter); }
-	NetlistConeWireIter end() { return NetlistConeWireIter(net); }
-};
-
-struct NetlistConeCellIter : public std::iterator<std::input_iterator_tag, RTLIL::Cell *> {
-	const Netlist &net;
-
-	NetlistConeWireIter sig_iter;
-
-	NetlistConeCellIter(const Netlist &net) : net(net), sig_iter(net) {}
-
-	NetlistConeCellIter(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig_iter(net, sig, cell_filter)
-	{
-		if ((!sig_iter.sentinel) && (!has_driver_cell(*sig_iter))) {
-			++(*this);
-		}
-	}
-
-	bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); }
-
-	RTLIL::Cell *operator*() const { return net.sigbit_driver_map.at(*sig_iter); };
-
-	bool operator!=(const NetlistConeCellIter &other) const { return sig_iter != other.sig_iter; }
-	bool operator==(const NetlistConeCellIter &other) const { return sig_iter == other.sig_iter; }
-	NetlistConeCellIter &operator++()
-	{
-		while (true) {
-			++sig_iter;
-			if (sig_iter.sentinel) {
-				return *this;
-			}
-
-			RTLIL::Cell* cell = net.driver_cell(*sig_iter);
-
-			if (!cell) {
-				continue;
-			}
-
-			if ((sig_iter.cell_filter) && (!sig_iter.cell_filter->cell_known(cell->type))) {
-				continue;
-			}
-
-			if (!sig_iter.cells_visited.count(cell)) {
-				return *this;
-			}
-		}
-	}
-};
-
-struct NetlistConeCellIterable {
-	const Netlist &net;
-	RTLIL::SigBit sig;
-	CellTypes *cell_filter;
-
-	NetlistConeCellIterable(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL) : net(net), sig(sig), cell_filter(cell_filter)
-	{
-	}
-
-	NetlistConeCellIter begin() { return NetlistConeCellIter(net, sig, cell_filter); }
-	NetlistConeCellIter end() { return NetlistConeCellIter(net); }
-};
-
-// struct NetlistConeInputsIter : public std::iterator<std::input_iterator_tag, const RTLIL::Cell *> {
-// 	const Netlist &net;
-// 	RTLIL::SigBit sig;
-
-// 	NetlistConeWireIter sig_iter;
-
-// 	bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); }
-
-// 	NetlistConeInputsIter(const Netlist &net, RTLIL::SigBit sig = NULL) : net(net), sig(sig), sig_iter(net, sig)
-// 	{
-// 		if ((sig != NULL) && (has_driver_cell(sig_iter))) {
-// 			++(*this);
-// 		}
-// 	}
-
-// 	const RTLIL::SigBit &operator*() const { return sig_iter; };
-// 	bool operator!=(const NetlistConeInputsIter &other) const { return sig_iter != other.sig_iter; }
-// 	bool operator==(const NetlistConeInputsIter &other) const { return sig_iter == other.sig_iter; }
-// 	NetlistConeInputsIter &operator++()
-// 	{
-// 		do {
-// 			++sig_iter;
-// 			if (sig_iter->empty()) {
-// 				return *this;
-// 			}
-// 		} while (has_driver_cell(sig_iter));
-
-// 		return *this;
-// 	}
-// };
-
-// struct NetlistConeInputsIterable {
-// 	const Netlist &net;
-// 	RTLIL::SigBit sig;
-
-// 	NetlistConeInputsIterable(const Netlist &net, RTLIL::SigBit sig) : net(net), sig(sig) {}
-
-// 	NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, sig); }
-// 	NetlistConeInputsIter end() { return NetlistConeInputsIter(net); }
-// };
-} // namespace detail
-
-detail::NetlistConeWireIterable cone(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL)
-{
-	return detail::NetlistConeWireIterable(net, net.sigmap(sig), cell_filter = cell_filter);
-}
-
-// detail::NetlistConeInputsIterable cone_inputs(RTLIL::SigBit sig) { return NetlistConeInputsIterable(this, &sig); }
-detail::NetlistConeCellIterable cell_cone(const Netlist &net, RTLIL::SigBit sig, CellTypes *cell_filter = NULL)
-{
-	return detail::NetlistConeCellIterable(net, net.sigmap(sig), cell_filter);
-}
-
-YOSYS_NAMESPACE_END
-
-#endif
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 0ab91ca9e..5fc28ae92 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -22,7 +22,6 @@
 #include "kernel/rtlil.h"
 #include "kernel/satgen.h"
 #include "kernel/sigtools.h"
-#include "netlist.h"
 #include <stdio.h>
 #include <stdlib.h>
 
@@ -31,9 +30,8 @@ PRIVATE_NAMESPACE_BEGIN
 
 SigMap assign_map, dff_init_map;
 SigSet<RTLIL::Cell*> mux_drivers;
+dict<SigBit, RTLIL::Cell*> bit2driver;
 dict<SigBit, pool<SigBit>> init_attributes;
-std::map<RTLIL::Module*, Netlist> netlists;
-std::map<RTLIL::Module *, CellTypes> comb_filters;
 
 bool keepdc;
 bool sat;
@@ -459,41 +457,46 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 		dff->unsetPort("\\E");
 	}
 
-	if (sat && has_init) {
+	if (sat && has_init && (!sig_r.size() || val_init == val_rv))
+	{
 		bool removed_sigbits = false;
 
-		// Create netlist for the module if not already available
-		if (!netlists.count(mod)) {
-			netlists.emplace(mod, Netlist(mod));
-			comb_filters.emplace(mod, comb_cells_filt());
-		}
-
-		// Load netlist for the module from the pool
-		Netlist &net = netlists.at(mod);
-
+		ezSatPtr ez;
+		SatGen satgen(ez.get(), &assign_map);
+		pool<Cell*> sat_cells;
+
+		std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
+			if (!sat_cells.insert(c).second)
+				return;
+			if (!satgen.importCell(c))
+				return;
+			for (auto &conn : c->connections()) {
+				if (!c->input(conn.first))
+					continue;
+				for (auto bit : assign_map(conn.second))
+					if (bit2driver.count(bit))
+						sat_import_cell(bit2driver.at(bit));
+			}
+		};
 
 		// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
 		for (int position = 0; position < GetSize(sig_d); position += 1) {
 			RTLIL::SigBit q_sigbit = sig_q[position];
 			RTLIL::SigBit d_sigbit = sig_d[position];
 
-			if ((!q_sigbit.wire) || (!d_sigbit.wire)) {
+			if ((!q_sigbit.wire) || (!d_sigbit.wire))
 				continue;
-			}
 
-			ezSatPtr ez;
-			SatGen satgen(ez.get(), &net.sigmap);
+			if (!bit2driver.count(d_sigbit))
+				continue;
 
-			// Create SAT instance only for the cells that influence the register bit combinatorially
-			for (const auto &cell : cell_cone(net, d_sigbit, &comb_filters.at(mod))) {
-				if (!satgen.importCell(cell))
-					log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name),
-						  RTLIL::id2cstr(cell->type));
-			}
+			sat_import_cell(bit2driver.at(d_sigbit));
 
-			RTLIL::Const sigbit_init_val = val_init.extract(position);
-			int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
+			RTLIL::State sigbit_init_val = val_init[position];
+			if (sigbit_init_val != State::S0 && sigbit_init_val != State::S1)
+				continue;
 
+			int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
 			int q_sat_pi = satgen.importSigBit(q_sigbit);
 			int d_sat_pi = satgen.importSigBit(d_sigbit);
 
@@ -501,24 +504,21 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
 			bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
 
 			// If the register bit cannot change, we can replace it with a constant
-			if (!counter_example_found) {
-
-				RTLIL::SigSpec driver_port = net.driver_port(q_sigbit);
-				RTLIL::Wire *dummy_wire = mod->addWire(NEW_ID, 1);
-
-				for (auto &conn : mod->connections_)
-					net.sigmap(conn.first).replace(driver_port, dummy_wire, &conn.first);
-
-				remove_init_attr(driver_port);
-				driver_port = dummy_wire;
+			if (!counter_example_found)
+			{
+				log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", sigbit_init_val ? 1 : 0,
+						position, log_id(dff), log_id(dff->type), log_id(mod));
 
-				mod->connect(RTLIL::SigSig(q_sigbit, sigbit_init_val));
+				SigSpec tmp = dff->getPort("\\D");
+				tmp[position] = sigbit_init_val;
+				dff->setPort("\\D", tmp);
 
 				removed_sigbits = true;
 			}
 		}
 
 		if (removed_sigbits) {
+			handle_dff(mod, dff);
 			return true;
 		}
 	}
@@ -566,8 +566,6 @@ struct OptRmdffPass : public Pass {
 			break;
 		}
 		extra_args(args, argidx, design);
-		netlists.clear();
-		comb_filters.clear();
 
 		for (auto module : design->selected_modules()) {
 			pool<SigBit> driven_bits;
@@ -576,6 +574,7 @@ struct OptRmdffPass : public Pass {
 			assign_map.set(module);
 			dff_init_map.set(module);
 			mux_drivers.clear();
+			bit2driver.clear();
 			init_attributes.clear();
 
 			for (auto wire : module->wires())
@@ -600,17 +599,21 @@ struct OptRmdffPass : public Pass {
 						driven_bits.insert(bit);
 				}
 			}
-			mux_drivers.clear();
 
 			std::vector<RTLIL::IdString> dff_list;
 			std::vector<RTLIL::IdString> dffsr_list;
 			std::vector<RTLIL::IdString> dlatch_list;
 			for (auto cell : module->cells())
 			{
-				for (auto &conn : cell->connections())
-					if (cell->output(conn.first) || !cell->known())
-						for (auto bit : assign_map(conn.second))
+				for (auto &conn : cell->connections()) {
+					bool is_output = cell->output(conn.first);
+					if (is_output || !cell->known())
+						for (auto bit : assign_map(conn.second)) {
+							if (is_output)
+								bit2driver[bit] = cell;
 							driven_bits.insert(bit);
+						}
+				}
 
 				if (cell->type == "$mux" || cell->type == "$pmux") {
 					if (cell->getPort("\\A").size() == cell->getPort("\\B").size())
@@ -682,6 +685,7 @@ struct OptRmdffPass : public Pass {
 
 		assign_map.clear();
 		mux_drivers.clear();
+		bit2driver.clear();
 		init_attributes.clear();
 
 		if (total_count || total_initdrv)