From d69989b8d27eea16d793600b1779661f31161c6c Mon Sep 17 00:00:00 2001
From: Bogdan Vukobratovic <bogdan.vukobratovic@gmail.com>
Date: Wed, 12 Jun 2019 19:35:05 +0200
Subject: [PATCH] Rename satgen_algo.h -> algo.h, code cleanup and refactoring

---
 kernel/algo.h           | 239 ++++++++++++++++++++++++++++++++++++++++
 kernel/celltypes.h      |   9 +-
 kernel/satgen_algo.h    | 201 ---------------------------------
 passes/opt/opt_rmdff.cc |  95 ++++------------
 4 files changed, 265 insertions(+), 279 deletions(-)
 create mode 100644 kernel/algo.h
 delete mode 100644 kernel/satgen_algo.h

diff --git a/kernel/algo.h b/kernel/algo.h
new file mode 100644
index 000000000..6ab96a875
--- /dev/null
+++ b/kernel/algo.h
@@ -0,0 +1,239 @@
+/* -*- 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;
+	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)
+	{
+		CellTypes ct(module->design);
+		setup_netlist(module, ct);
+	}
+
+	Netlist(RTLIL::Module *module, const CellTypes &ct) : module(module), sigmap(module) { setup_netlist(module, ct); }
+
+	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, const RTLIL::SigBit *> {
+	using set_iter_t = std::set<RTLIL::SigBit>::iterator;
+
+	const Netlist &net;
+	const RTLIL::SigBit *p_sig;
+	std::stack<std::pair<set_iter_t, set_iter_t>> dfs_path_stack;
+	std::set<RTLIL::Cell *> cells_visited;
+
+	NetlistConeWireIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig) {}
+
+	const RTLIL::SigBit &operator*() const { return *p_sig; };
+	bool operator!=(const NetlistConeWireIter &other) const { return p_sig != other.p_sig; }
+	bool operator==(const NetlistConeWireIter &other) const { return p_sig == other.p_sig; }
+
+	void next_sig_in_dag()
+	{
+		while (1) {
+			if (dfs_path_stack.empty()) {
+				p_sig = NULL;
+				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) {
+				p_sig = &(*cell_inputs_iter);
+				return;
+			} else {
+				dfs_path_stack.pop();
+			}
+		}
+	}
+
+	NetlistConeWireIter &operator++()
+	{
+		if (net.sigbit_driver_map.count(*p_sig)) {
+			auto drv = net.sigbit_driver_map.at(*p_sig);
+
+			if (!cells_visited.count(drv)) {
+				auto &inputs = net.cell_inputs_map.at(drv);
+				dfs_path_stack.push(std::make_pair(inputs.begin(), inputs.end()));
+				cells_visited.insert(drv);
+				p_sig = &(*dfs_path_stack.top().first);
+			} else {
+				next_sig_in_dag();
+			}
+		} else {
+			next_sig_in_dag();
+		}
+		return *this;
+	}
+};
+
+struct NetlistConeWireIterable {
+	const Netlist &net;
+	const RTLIL::SigBit *p_sig;
+
+	NetlistConeWireIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {}
+
+	NetlistConeWireIter begin() { return NetlistConeWireIter(net, p_sig); }
+	NetlistConeWireIter end() { return NetlistConeWireIter(net); }
+};
+
+struct NetlistConeCellIter : public std::iterator<std::input_iterator_tag, const RTLIL::Cell *> {
+	const Netlist &net;
+	const RTLIL::SigBit *p_sig;
+
+	NetlistConeWireIter sig_iter;
+
+	NetlistConeCellIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig), sig_iter(net, p_sig)
+	{
+		if ((p_sig != NULL) && (!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.p_sig == NULL) {
+				return *this;
+			}
+
+			if (has_driver_cell(*sig_iter)) {
+				auto cell = net.sigbit_driver_map.at(*sig_iter);
+
+				if (!sig_iter.cells_visited.count(cell)) {
+					return *this;
+				}
+			}
+		};
+	}
+};
+
+struct NetlistConeCellIterable {
+	const Netlist &net;
+	const RTLIL::SigBit *p_sig;
+
+	NetlistConeCellIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {}
+
+	NetlistConeCellIter begin() { return NetlistConeCellIter(net, p_sig); }
+	NetlistConeCellIter end() { return NetlistConeCellIter(net); }
+};
+
+struct NetlistConeInputsIter : public std::iterator<std::input_iterator_tag, const RTLIL::Cell *> {
+	const Netlist &net;
+	const RTLIL::SigBit *p_sig;
+
+	NetlistConeWireIter sig_iter;
+
+	bool has_driver_cell(const RTLIL::SigBit &s) { return net.sigbit_driver_map.count(s); }
+
+	NetlistConeInputsIter(const Netlist &net, const RTLIL::SigBit *p_sig = NULL) : net(net), p_sig(p_sig), sig_iter(net, p_sig)
+	{
+		if ((p_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.p_sig == NULL) {
+				return *this;
+			}
+		} while (has_driver_cell(*sig_iter));
+
+		return *this;
+	}
+};
+
+struct NetlistConeInputsIterable {
+	const Netlist &net;
+	const RTLIL::SigBit *p_sig;
+
+	NetlistConeInputsIterable(const Netlist &net, const RTLIL::SigBit *p_sig) : net(net), p_sig(p_sig) {}
+
+	NetlistConeInputsIter begin() { return NetlistConeInputsIter(net, p_sig); }
+	NetlistConeInputsIter end() { return NetlistConeInputsIter(net); }
+};
+} // namespace detail
+
+detail::NetlistConeWireIterable cone(const Netlist &net, const RTLIL::SigBit &sig) { return detail::NetlistConeWireIterable(net, &sig); }
+
+// detail::NetlistConeInputsIterable cone_inputs(const RTLIL::SigBit &sig) { return NetlistConeInputsIterable(this, &sig); }
+detail::NetlistConeCellIterable cell_cone(const Netlist &net, const RTLIL::SigBit &sig) { return detail::NetlistConeCellIterable(net, &sig); }
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 4e91eddda..758661c02 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -246,24 +246,24 @@ struct CellTypes
 		cell_types.clear();
 	}
 
-	bool cell_known(RTLIL::IdString type)
+	bool cell_known(RTLIL::IdString type) const
 	{
 		return cell_types.count(type) != 0;
 	}
 
-	bool cell_output(RTLIL::IdString type, RTLIL::IdString port)
+	bool cell_output(RTLIL::IdString type, RTLIL::IdString port) const
 	{
 		auto it = cell_types.find(type);
 		return it != cell_types.end() && it->second.outputs.count(port) != 0;
 	}
 
-	bool cell_input(RTLIL::IdString type, RTLIL::IdString port)
+	bool cell_input(RTLIL::IdString type, RTLIL::IdString port) const
 	{
 		auto it = cell_types.find(type);
 		return it != cell_types.end() && it->second.inputs.count(port) != 0;
 	}
 
-	bool cell_evaluable(RTLIL::IdString type)
+	bool cell_evaluable(RTLIL::IdString type) const
 	{
 		auto it = cell_types.find(type);
 		return it != cell_types.end() && it->second.is_evaluable;
@@ -482,4 +482,3 @@ extern CellTypes yosys_celltypes;
 YOSYS_NAMESPACE_END
 
 #endif
-
diff --git a/kernel/satgen_algo.h b/kernel/satgen_algo.h
deleted file mode 100644
index d475d7d64..000000000
--- a/kernel/satgen_algo.h
+++ /dev/null
@@ -1,201 +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
-
-struct DriverMap : public std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::set<RTLIL::SigBit>>> {
-	RTLIL::Module *module;
-	SigMap sigmap;
-
-	using map_t = std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::set<RTLIL::SigBit>>>;
-
-	struct DriverMapConeWireIterator : public std::iterator<std::input_iterator_tag, const RTLIL::SigBit *> {
-		using set_iter_t = std::set<RTLIL::SigBit>::iterator;
-
-		DriverMap *drvmap;
-		const RTLIL::SigBit *sig;
-		std::stack<std::pair<set_iter_t, set_iter_t>> dfs;
-
-		DriverMapConeWireIterator(DriverMap *drvmap) : DriverMapConeWireIterator(drvmap, NULL) {}
-
-		DriverMapConeWireIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {}
-
-		inline const RTLIL::SigBit &operator*() const { return *sig; };
-		inline bool operator!=(const DriverMapConeWireIterator &other) const { return sig != other.sig; }
-		inline bool operator==(const DriverMapConeWireIterator &other) const { return sig == other.sig; }
-		inline void operator++()
-		{
-			if (drvmap->count(*sig)) {
-				std::pair<RTLIL::Cell *, std::set<RTLIL::SigBit>> &drv = drvmap->at(*sig);
-				dfs.push(std::make_pair(drv.second.begin(), drv.second.end()));
-				sig = &(*dfs.top().first);
-			} else {
-				while (1) {
-					auto &inputs_iter = dfs.top();
-
-					inputs_iter.first++;
-					if (inputs_iter.first != inputs_iter.second) {
-						sig = &(*inputs_iter.first);
-						return;
-					} else {
-						dfs.pop();
-						if (dfs.empty()) {
-							sig = NULL;
-							return;
-						}
-					}
-				}
-			}
-		}
-	};
-
-	struct DriverMapConeWireIterable {
-		DriverMap *drvmap;
-		const RTLIL::SigBit *sig;
-
-		DriverMapConeWireIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {}
-
-		inline DriverMapConeWireIterator begin() { return DriverMapConeWireIterator(drvmap, sig); }
-		inline DriverMapConeWireIterator end() { return DriverMapConeWireIterator(drvmap); }
-	};
-
-	struct DriverMapConeCellIterator : public std::iterator<std::input_iterator_tag, const RTLIL::Cell *> {
-		DriverMap *drvmap;
-		const RTLIL::SigBit *sig;
-
-		DriverMapConeWireIterator sig_iter;
-
-		DriverMapConeCellIterator(DriverMap *drvmap) : DriverMapConeCellIterator(drvmap, NULL) {}
-
-		DriverMapConeCellIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig), sig_iter(drvmap, sig)
-		{
-			if ((sig != NULL) && (!drvmap->count(*sig_iter))) {
-				++(*this);
-			}
-		}
-
-		inline RTLIL::Cell *operator*() const
-		{
-			std::pair<RTLIL::Cell *, std::set<RTLIL::SigBit>> &drv = drvmap->at(*sig_iter);
-			return drv.first;
-		};
-		inline bool operator!=(const DriverMapConeCellIterator &other) const { return sig_iter != other.sig_iter; }
-		inline bool operator==(const DriverMapConeCellIterator &other) const { return sig_iter == other.sig_iter; }
-		inline void operator++()
-		{
-			do {
-				++sig_iter;
-				if (sig_iter.sig == NULL) {
-					return;
-				}
-			} while (!drvmap->count(*sig_iter));
-		}
-	};
-
-	struct DriverMapConeCellIterable {
-		DriverMap *drvmap;
-		const RTLIL::SigBit *sig;
-
-		DriverMapConeCellIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {}
-
-		inline DriverMapConeCellIterator begin() { return DriverMapConeCellIterator(drvmap, sig); }
-		inline DriverMapConeCellIterator end() { return DriverMapConeCellIterator(drvmap); }
-	};
-
-	struct DriverMapConeInputsIterator : public std::iterator<std::input_iterator_tag, const RTLIL::Cell *> {
-		DriverMap *drvmap;
-		const RTLIL::SigBit *sig;
-
-		DriverMapConeWireIterator sig_iter;
-
-		DriverMapConeInputsIterator(DriverMap *drvmap) : DriverMapConeInputsIterator(drvmap, NULL) {}
-
-		DriverMapConeInputsIterator(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig), sig_iter(drvmap, sig)
-		{
-			if ((sig != NULL) && (drvmap->count(*sig_iter))) {
-				++(*this);
-			}
-		}
-
-		inline const RTLIL::SigBit& operator*() const
-		{
-			return *sig_iter;
-		};
-		inline bool operator!=(const DriverMapConeInputsIterator &other) const { return sig_iter != other.sig_iter; }
-		inline bool operator==(const DriverMapConeInputsIterator &other) const { return sig_iter == other.sig_iter; }
-		inline void operator++()
-		{
-			do {
-				++sig_iter;
-				if (sig_iter.sig == NULL) {
-					return;
-				}
-			} while (drvmap->count(*sig_iter));
-		}
-	};
-
-	struct DriverMapConeInputsIterable {
-		DriverMap *drvmap;
-		const RTLIL::SigBit *sig;
-
-		DriverMapConeInputsIterable(DriverMap *drvmap, const RTLIL::SigBit *sig) : drvmap(drvmap), sig(sig) {}
-
-		inline DriverMapConeInputsIterator begin() { return DriverMapConeInputsIterator(drvmap, sig); }
-		inline DriverMapConeInputsIterator end() { return DriverMapConeInputsIterator(drvmap); }
-	};
-
-	DriverMap(RTLIL::Module *module) : module(module), sigmap(module)
-	{
-		CellTypes ct;
-		ct.setup_internals();
-		ct.setup_stdcells();
-
-		for (auto &it : module->cells_) {
-			if (ct.cell_known(it.second->type)) {
-				std::set<RTLIL::SigBit> inputs, outputs;
-				for (auto &port : it.second->connections()) {
-					std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
-					if (ct.cell_output(it.second->type, port.first))
-						outputs.insert(bits.begin(), bits.end());
-					else
-						inputs.insert(bits.begin(), bits.end());
-				}
-				std::pair<RTLIL::Cell *, std::set<RTLIL::SigBit>> drv(it.second, inputs);
-				for (auto &bit : outputs)
-					(*this)[bit] = drv;
-			}
-		}
-	}
-
-	DriverMapConeWireIterable cone(const RTLIL::SigBit &sig) { return DriverMapConeWireIterable(this, &sig); }
-	DriverMapConeInputsIterable cone_inputs(const RTLIL::SigBit &sig) { return DriverMapConeInputsIterable(this, &sig); }
-	DriverMapConeCellIterable cell_cone(const RTLIL::SigBit &sig) { return DriverMapConeCellIterable(this, &sig); }
-};
-
-YOSYS_NAMESPACE_END
-
-#endif
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 4b9fe5823..b5a5735e7 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -21,7 +21,7 @@
 #include "kernel/register.h"
 #include "kernel/rtlil.h"
 #include "kernel/satgen.h"
-#include "kernel/satgen_algo.h"
+#include "kernel/algo.h"
 #include "kernel/sigtools.h"
 #include <stdio.h>
 #include <stdlib.h>
@@ -32,6 +32,7 @@ PRIVATE_NAMESPACE_BEGIN
 SigMap assign_map, dff_init_map;
 SigSet<RTLIL::Cell*> mux_drivers;
 dict<SigBit, pool<SigBit>> init_attributes;
+std::map<RTLIL::Module*, Netlist> netlists;
 bool keepdc;
 bool sat;
 
@@ -459,9 +460,12 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass)
 	if (sat && has_init) {
 		std::vector<int> removed_sigbits;
 
-		DriverMap drvmap(mod);
+		if (!netlists.count(mod)) {
+			netlists.emplace(mod, Netlist(mod, comb_cells_filt()));
+		}
+
+		Netlist &net = netlists.at(mod);
 
-		// for (auto &sigbit : sig_q.bits()) {
 		for (int position = 0; position < GetSize(sig_d); position += 1) {
 			RTLIL::SigBit q_sigbit = sig_q[position];
 			RTLIL::SigBit d_sigbit = sig_d[position];
@@ -470,83 +474,27 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass)
 				continue;
 			}
 
-			std::map<RTLIL::SigBit, int> sat_pi;
-
 			ezSatPtr ez;
-			SatGen satgen(ez.get(), &drvmap.sigmap);
-			std::set<RTLIL::Cell *> ez_cells;
-			std::vector<int> modelExpressions;
-			std::vector<bool> modelValues;
-
-			log("Optimizing: %s\n", log_id(q_sigbit.wire));
-			log("    Cells:");
-			for (const auto &cell : drvmap.cell_cone(d_sigbit)) {
-				if (ez_cells.count(cell) == 0) {
-					log("        %s\n", log_id(cell));
-					if (!satgen.importCell(cell))
-						log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name),
-							  RTLIL::id2cstr(cell->type));
-					ez_cells.insert(cell);
-				}
-			}
-
-			RTLIL::Const sigbit_init_val = val_init.extract(position);
-			int reg_init = satgen.importSigSpec(sigbit_init_val).front();
-
-			int output_a = satgen.importSigSpec(d_sigbit).front();
-			modelExpressions.push_back(output_a);
-
-			log("    Wires:");
-			for (const auto &sig : drvmap.cone_inputs(d_sigbit)) {
-				if (sat_pi.count(sig) == 0) {
-					sat_pi[sig] = satgen.importSigSpec(sig).front();
-					modelExpressions.push_back(sat_pi[sig]);
-
-					if (sig == q_sigbit) {
-						ez->assume(ez->IFF(sat_pi[sig], reg_init));
-					}
+			SatGen satgen(ez.get(), &net.sigmap);
 
-					if (sig.wire) {
-						log("        %s\n", log_id(sig.wire));
-					}
-				}
+			for (const auto &cell : cell_cone(net, d_sigbit)) {
+				if (!satgen.importCell(cell))
+					log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(cell->name),
+						  RTLIL::id2cstr(cell->type));
 			}
 
-			bool success = ez->solve(modelExpressions, modelValues, ez->IFF(output_a, reg_init));
-			// bool success = ez->solve(modelExpressions, modelValues, ez->IFF(output_a, ez->NOT(reg_init)));
-			if (ez->getSolverTimoutStatus())
-				log("Timeout\n");
-
-			log("Success: %d\n", success);
-
-			// satgen.signals_eq(big_lhs, big_rhs, timestep);
-
-			// auto iterable = drvmap.cone(d_sigbit);
+			RTLIL::Const sigbit_init_val = val_init.extract(position);
+			int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
 
-			//   // for (const auto &sig : drvmap.cone(d_sigbit))
-			// for(auto begin=iterable.begin(); begin != iterable.end(); ++begin)
-			// {
-			// 	if (drvmap.count(*begin)) {
-			// 		if (drvmap.at(*begin).first)
-			// 			log("Running: %s\n", log_id(drvmap.at(*begin).first));
-			// 	}
+			int q_sat_pi = satgen.importSigBit(q_sigbit);
+			int d_sat_pi = satgen.importSigBit(d_sigbit);
 
-			// 	if ((*begin).wire) {
-			// 		log("Running: %s\n", log_id((*begin).wire));
-			// 	}
-			// }
+			// log("DFF: %s", log_id(net.sigbit_driver_map[q_sigbit]));
 
+			bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
 
 			char str[1024];
-			// sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", log_id(d_sigbit.wire), d_sigbit.offset,
-			// 	sigbit_init_val.as_string().c_str(), log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str());
-			// log("Running: %s\n", str);
-
-			// log_flush();
-
-			// pass->call(mod->design, str);
-			// if (mod->design->scratchpad_get_bool("sat.success", false)) {
-			if (success) {
+			if (!counter_example_found) {
 				sprintf(str, "connect -set %s[%d] %s", log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str());
 				log("Running: %s\n", str);
 				log_flush();
@@ -561,6 +509,7 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass)
 		}
 	}
 
+
 	return false;
 
 delete_dff:
@@ -603,9 +552,9 @@ struct OptRmdffPass : public Pass {
 			break;
 		}
 		extra_args(args, argidx, design);
+		netlists.clear();
 
-		for (auto module : design->selected_modules())
-		{
+		for (auto module : design->selected_modules()) {
 			pool<SigBit> driven_bits;
 			dict<SigBit, State> init_bits;
 
-- 
2.30.2