riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Generate satgen instance instead of calling sat pass

This commit is contained in:
Bogdan Vukobratovic 2019-06-11 11:47:13 +02:00
parent d097f423d1
commit 9892df17ef
2 changed files with 128 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
kernel/satgen_algo.h
View File

@ -100,7 +100,7 @@ struct DriverMap : public std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::
inline RTLIL::Cell *operator*() const 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; 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; }
@ -126,6 +126,48 @@ struct DriverMap : public std::map<RTLIL::SigBit, std::pair<RTLIL::Cell *, std::
inline DriverMapConeCellIterator end() { return DriverMapConeCellIterator(drvmap); } 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) DriverMap(RTLIL::Module *module) : module(module), sigmap(module)
{ {
CellTypes ct; 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); } 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); } DriverMapConeCellIterable cell_cone(const RTLIL::SigBit &sig) { return DriverMapConeCellIterable(this, &sig); }
}; };

106
passes/opt/opt_rmdff.cc
View File

@ -17,11 +17,14 @@
* *
*/ */
#include "kernel/register.h"
#include "kernel/sigtools.h"
#include "kernel/log.h" #include "kernel/log.h"
#include <stdlib.h> #include "kernel/register.h"
#include "kernel/rtlil.h"
#include "kernel/satgen.h"
#include "kernel/satgen_algo.h"
#include "kernel/sigtools.h"
#include <stdio.h> #include <stdio.h>
#include <stdlib.h>
USING_YOSYS_NAMESPACE USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN PRIVATE_NAMESPACE_BEGIN
@ -456,36 +459,95 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff, Pass *pass)
if (sat && has_init) { if (sat && has_init) {
std::vector<int> removed_sigbits; std::vector<int> removed_sigbits;
DriverMap drvmap(mod);
// for (auto &sigbit : sig_q.bits()) { // 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 q_sigbit = sig_q[position];
RTLIL::SigBit d_sigbit = sig_d[position]; RTLIL::SigBit d_sigbit = sig_d[position];
RTLIL::Const sigbit_init_val = val_init.extract(position);
if ((!q_sigbit.wire) || (!d_sigbit.wire)) { if ((!q_sigbit.wire) || (!d_sigbit.wire)) {
continue; 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]; char str[1024];
sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", // sprintf(str, "sat -ignore_unknown_cells -prove %s[%d] %s -set %s[%d] %s", log_id(d_sigbit.wire), d_sigbit.offset,
log_id(d_sigbit.wire), // sigbit_init_val.as_string().c_str(), log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str());
d_sigbit.offset, // log("Running: %s\n", str);
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(); // log_flush();
pass->call(mod->design, str); // pass->call(mod->design, str);
if (mod->design->scratchpad_get_bool("sat.success", false)) { // if (mod->design->scratchpad_get_bool("sat.success", false)) {
sprintf(str, "connect -set %s[%d] %s", if (success) {
log_id(q_sigbit.wire), sprintf(str, "connect -set %s[%d] %s", log_id(q_sigbit.wire), q_sigbit.offset, sigbit_init_val.as_string().c_str());
q_sigbit.offset,
sigbit_init_val.as_string().c_str()
);
log("Running: %s\n", str); log("Running: %s\n", str);
log_flush(); log_flush();
pass->call(mod->design, str); pass->call(mod->design, str);