Generate satgen instance instead of calling sat pass

diff --git a/kernel/satgen_algo.h b/kernel/satgen_algo.h
index 483dfad5c74590b4d41974b039926919759261df..d475d7d64383142bf1c7f6b2319312844c65e181 100644 (file)
--- a/kernel/satgen_algo.h
+++ b/kernel/satgen_algo.h
@@ -100,7 +100,7 @@ struct DriverMap : public std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::
 
                inline RTLIL::Cell *operator*() const
                {
-                       std::pair<RTLIL::Cell *, std::set<RTLIL::SigBit>> &drv = drvmap->at(*sig);
+                       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; }
@@ -126,6 +126,48 @@ struct DriverMap : public std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::
                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;
@@ -150,6 +192,7 @@ struct DriverMap : public std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::
        }
 
        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); }
 };
 

diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 72eac9111ebe90ab4a5c03cf7bd4f0ea502fb71b..4b9fe582377c964412fc3d0dc933101e91b241d4 100644 (file)
--- 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);