mirror of https://github.com/YosysHQ/yosys.git
Rename satgen_algo.h -> algo.h, code cleanup and refactoring
This commit is contained in:
Bogdan Vukobratovic
parent
9892df17ef
commit
d69989b8d2
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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;
|
||||
SatGen satgen(ez.get(), &net.sigmap);
|
||||
|
||||
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);
|
||||
}
|
||||
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));
|
||||
}
|
||||
|
||||
RTLIL::Const sigbit_init_val = val_init.extract(position);
|
||||
int reg_init = satgen.importSigSpec(sigbit_init_val).front();
|
||||
int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
|
||||
|
||||
int output_a = satgen.importSigSpec(d_sigbit).front();
|
||||
modelExpressions.push_back(output_a);
|
||||
int q_sat_pi = satgen.importSigBit(q_sigbit);
|
||||
int d_sat_pi = satgen.importSigBit(d_sigbit);
|
||||
|
||||
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));
|
||||
// }
|
||||
// }
|
||||
// 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;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue