--- /dev/null
+/* -*- 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
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;
YOSYS_NAMESPACE_END
#endif
-
+++ /dev/null
-/* -*- 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
#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>
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;
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];
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();
}
}
+
return false;
delete_dff:
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;
projects / yosys.git / commitdiff