Generate satgen instance instead of calling sat pass

1 files changed, 85 insertions, 23 deletions

diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 72eac9111..4b9fe5823 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -17,11 +17,14 @@
  *
  */
 
+#include "kernel/log.h"
 #include "kernel/register.h"
+#include "kernel/rtlil.h"
+#include "kernel/satgen.h"
+#include "kernel/satgen_algo.h"
 #include "kernel/sigtools.h"
-#include "kernel/log.h"
-#include <stdlib.h>
 #include <stdio.h>
+#include <stdlib.h>
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -456,36 +459,95 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass)
 	if (sat && has_init) {
 		std::vector<int> removed_sigbits;
 
+		DriverMap drvmap(mod);
+
 		// for (auto &sigbit : sig_q.bits()) {
-		for (int position =0; position < GetSize(sig_d); position += 1) {
+		for (int position = 0; position < GetSize(sig_d); position += 1) {
 			RTLIL::SigBit q_sigbit = sig_q[position];
 			RTLIL::SigBit d_sigbit = sig_d[position];
-			RTLIL::Const  sigbit_init_val = val_init.extract(position);
 
 			if ((!q_sigbit.wire) || (!d_sigbit.wire)) {
 				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));
+					}
+
+					if (sig.wire) {
+						log("        %s\n", log_id(sig.wire));
+					}
+				}
+			}
+
+			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);
+
+			//   // 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));
+			// 	}
+
+			// 	if ((*begin).wire) {
+			// 		log("Running: %s\n", log_id((*begin).wire));
+			// 	}
+			// }
+
+
 			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)) {
-				sprintf(str, "connect -set %s[%d] %s",
-								log_id(q_sigbit.wire),
-								q_sigbit.offset,
-								sigbit_init_val.as_string().c_str()
-								);
+			// 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) {
+				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();
 				pass->call(mod->design, str);