$(eval $(call add_include_file,kernel/macc.h))
$(eval $(call add_include_file,kernel/utils.h))
$(eval $(call add_include_file,kernel/satgen.h))
+$(eval $(call add_include_file,kernel/qcsat.h))
$(eval $(call add_include_file,kernel/ff.h))
$(eval $(call add_include_file,kernel/ffinit.h))
$(eval $(call add_include_file,kernel/mem.h))
kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"'
endif
endif
-OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/mem.o kernel/ffmerge.o
+OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o
kernel/log.o: CXXFLAGS += -DYOSYS_SRC='"$(YOSYS_SRC)"'
kernel/yosys.o: CXXFLAGS += -DYOSYS_DATDIR='"$(DATDIR)"' -DYOSYS_PROGRAM_PREFIX='"$(PROGRAM_PREFIX)"'
}
}
- ModWalker(RTLIL::Design *design) : design(design), module(NULL)
+ ModWalker(RTLIL::Design *design, RTLIL::Module *module = nullptr) : design(design), module(NULL)
{
- ct.setup(design);
+ ct.setup(design);
+ if (module)
+ setup(module);
}
void setup(RTLIL::Module *module, CellTypes *filter_ct = NULL)
--- /dev/null
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2021 Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ * 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.
+ *
+ */
+
+#include "kernel/qcsat.h"
+
+USING_YOSYS_NAMESPACE
+
+std::vector<int> QuickConeSat::importSig(SigSpec sig)
+{
+ sig = modwalker.sigmap(sig);
+ for (auto bit : sig)
+ bits_queue.insert(bit);
+ return satgen.importSigSpec(sig);
+}
+
+int QuickConeSat::importSigBit(SigBit bit)
+{
+ bit = modwalker.sigmap(bit);
+ bits_queue.insert(bit);
+ return satgen.importSigBit(bit);
+}
+
+void QuickConeSat::prepare()
+{
+ while (!bits_queue.empty())
+ {
+ pool<ModWalker::PortBit> portbits;
+ modwalker.get_drivers(portbits, bits_queue);
+
+ for (auto bit : bits_queue)
+ if (bit.wire && bit.wire->get_bool_attribute(ID::onehot) && !imported_onehot.count(bit.wire))
+ {
+ std::vector<int> bits = satgen.importSigSpec(bit.wire);
+ for (int i : bits)
+ for (int j : bits)
+ if (i != j)
+ ez->assume(ez->NOT(i), j);
+ imported_onehot.insert(bit.wire);
+ }
+
+ bits_queue.clear();
+
+ for (auto &pbit : portbits)
+ {
+ if (imported_cells.count(pbit.cell))
+ continue;
+ if (cell_complexity(pbit.cell) > max_cell_complexity)
+ continue;
+ if (max_cell_outs && GetSize(modwalker.cell_outputs[pbit.cell]) > max_cell_outs)
+ continue;
+ auto &inputs = modwalker.cell_inputs[pbit.cell];
+ bits_queue.insert(inputs.begin(), inputs.end());
+ satgen.importCell(pbit.cell);
+ imported_cells.insert(pbit.cell);
+ }
+
+ if (max_cell_count && GetSize(imported_cells) > max_cell_count)
+ break;
+ }
+}
+
+int QuickConeSat::cell_complexity(RTLIL::Cell *cell)
+{
+ if (cell->type.in(ID($concat), ID($slice), ID($pos), ID($_BUF_)))
+ return 0;
+ if (cell->type.in(ID($not), ID($and), ID($or), ID($xor), ID($xnor),
+ ID($reduce_and), ID($reduce_or), ID($reduce_xor),
+ ID($reduce_xnor), ID($reduce_bool),
+ ID($logic_not), ID($logic_and), ID($logic_or),
+ ID($eq), ID($ne), ID($eqx), ID($nex), ID($fa),
+ ID($mux), ID($pmux), ID($lut), ID($sop),
+ ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_),
+ ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_),
+ ID($_MUX_), ID($_NMUX_), ID($_MUX4_), ID($_MUX8_), ID($_MUX16_),
+ ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_)))
+ return 1;
+ if (cell->type.in(ID($neg), ID($add), ID($sub), ID($alu), ID($lcu),
+ ID($lt), ID($le), ID($gt), ID($ge)))
+ return 2;
+ if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
+ return 3;
+ if (cell->type.in(ID($mul), ID($macc), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow)))
+ return 4;
+ // Unknown cell.
+ return 5;
+}
--- /dev/null
+/* -*- c++ -*-
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2021 Marcelina Kościelnicka <mwk@0x04.net>
+ *
+ * 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 QCSAT_H
+#define QCSAT_H
+
+#include "kernel/satgen.h"
+#include "kernel/modtools.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+// This is a helper class meant for easy construction of quick SAT queries
+// to a combinatorial input cone of some set of signals, meant for SAT-based
+// optimizations. Various knobs are provided to set just how much of the
+// cone should be included in the model — since this class is meant for
+// optimization, it should not be a correctness problem when some cells are
+// skipped and the solver spuriously returns SAT with a solution that
+// cannot exist in reality due to skipped constraints (ie. only UNSAT results
+// from this class should be considered binding).
+struct QuickConeSat {
+ ModWalker &modwalker;
+ ezSatPtr ez;
+ SatGen satgen;
+
+ // The effort level knobs.
+
+ // The maximum "complexity level" of cells that will be imported.
+ // - 1: bitwise operations, muxes, equality comparisons, lut, sop, fa
+ // - 2: addition, subtraction, greater/less than comparisons, lcu
+ // - 3: shifts
+ // - 4: multiplication, division, power
+ int max_cell_complexity = 2;
+ // The maximum number of cells to import, or 0 for no limit.
+ int max_cell_count = 0;
+ // If non-0, skip importing cells with more than this number of output bits.
+ int max_cell_outs = 0;
+
+ // Internal state.
+ pool<RTLIL::Cell*> imported_cells;
+ pool<RTLIL::Wire*> imported_onehot;
+ pool<RTLIL::SigBit> bits_queue;
+
+ QuickConeSat(ModWalker &modwalker) : modwalker(modwalker), ez(), satgen(ez.get(), &modwalker.sigmap) {}
+
+ // Imports a signal into the SAT solver, queues its input cone to be
+ // imported in the next prepare() call.
+ std::vector<int> importSig(SigSpec sig);
+ int importSigBit(SigBit bit);
+
+ // Imports the input cones of all previously importSig'd signals into
+ // the SAT solver.
+ void prepare();
+
+ // Returns the "complexity level" of a given cell.
+ static int cell_complexity(RTLIL::Cell *cell);
+};
+
+YOSYS_NAMESPACE_END
+
+#endif
*/
#include "kernel/yosys.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
#include "kernel/sigtools.h"
#include "kernel/modtools.h"
#include "kernel/mem.h"
RTLIL::Module *module;
SigMap sigmap, sigmap_xmux;
ModWalker modwalker;
- CellTypes cone_ct;
bool flag_widen;
// Okay, time to actually run the SAT solver.
- ezSatPtr ez;
- SatGen satgen(ez.get(), &modwalker.sigmap);
+ QuickConeSat qcsat(modwalker);
// create SAT representation of common input cone of all considered EN signals
- pool<Wire*> one_hot_wires;
- std::set<RTLIL::Cell*> sat_cells;
- std::set<RTLIL::SigBit> bits_queue;
dict<int, int> port_to_sat_variable;
- for (auto idx : group) {
- RTLIL::SigSpec sig = modwalker.sigmap(mem.wr_ports[idx].en);
- port_to_sat_variable[idx] = ez->expression(ez->OpOr, satgen.importSigSpec(sig));
-
- std::vector<RTLIL::SigBit> bits = sig;
- bits_queue.insert(bits.begin(), bits.end());
- }
-
- while (!bits_queue.empty())
- {
- for (auto bit : bits_queue)
- if (bit.wire && bit.wire->get_bool_attribute(ID::onehot))
- one_hot_wires.insert(bit.wire);
-
- pool<ModWalker::PortBit> portbits;
- modwalker.get_drivers(portbits, bits_queue);
- bits_queue.clear();
-
- for (auto &pbit : portbits)
- if (sat_cells.count(pbit.cell) == 0 && cone_ct.cell_known(pbit.cell->type)) {
- pool<RTLIL::SigBit> &cell_inputs = modwalker.cell_inputs[pbit.cell];
- bits_queue.insert(cell_inputs.begin(), cell_inputs.end());
- sat_cells.insert(pbit.cell);
- }
- }
-
- for (auto wire : one_hot_wires) {
- log(" Adding one-hot constraint for wire %s.\n", log_id(wire));
- vector<int> ez_wire_bits = satgen.importSigSpec(wire);
- for (int i : ez_wire_bits)
- for (int j : ez_wire_bits)
- if (i != j) ez->assume(ez->NOT(i), j);
- }
+ for (auto idx : group)
+ port_to_sat_variable[idx] = qcsat.ez->expression(qcsat.ez->OpOr, qcsat.importSig(mem.wr_ports[idx].en));
- log(" Common input cone for all EN signals: %d cells.\n", int(sat_cells.size()));
+ qcsat.prepare();
- for (auto cell : sat_cells)
- satgen.importCell(cell);
+ log(" Common input cone for all EN signals: %d cells.\n", GetSize(qcsat.imported_cells));
- log(" Size of unconstrained SAT problem: %d variables, %d clauses\n", ez->numCnfVariables(), ez->numCnfClauses());
+ log(" Size of unconstrained SAT problem: %d variables, %d clauses\n", qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
// now try merging the ports.
if (port2.removed)
continue;
- if (ez->solve(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2))) {
+ if (qcsat.ez->solve(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2))) {
log(" According to SAT solver sharing of port %d with port %d is not possible.\n", idx1, idx2);
continue;
}
log(" Merging port %d into port %d.\n", idx2, idx1);
mem.prepare_wr_merge(idx1, idx2);
- port_to_sat_variable.at(idx1) = ez->OR(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2));
+ port_to_sat_variable.at(idx1) = qcsat.ez->OR(port_to_sat_variable.at(idx1), port_to_sat_variable.at(idx2));
RTLIL::SigSpec last_addr = port1.addr;
RTLIL::SigSpec last_data = port1.data;
while (consolidate_wr_by_addr(mem));
}
- cone_ct.setup_internals();
- cone_ct.cell_types.erase(ID($mul));
- cone_ct.cell_types.erase(ID($mod));
- cone_ct.cell_types.erase(ID($div));
- cone_ct.cell_types.erase(ID($modfloor));
- cone_ct.cell_types.erase(ID($divfloor));
- cone_ct.cell_types.erase(ID($pow));
- cone_ct.cell_types.erase(ID($shl));
- cone_ct.cell_types.erase(ID($shr));
- cone_ct.cell_types.erase(ID($sshl));
- cone_ct.cell_types.erase(ID($sshr));
- cone_ct.cell_types.erase(ID($shift));
- cone_ct.cell_types.erase(ID($shiftx));
-
- modwalker.setup(module, &cone_ct);
+ modwalker.setup(module);
for (auto &mem : memories)
consolidate_wr_using_sat(mem);
#include "kernel/log.h"
#include "kernel/register.h"
#include "kernel/rtlil.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
+#include "kernel/modtools.h"
#include "kernel/sigtools.h"
#include "kernel/ffinit.h"
#include "kernel/ff.h"
FfInitVals initvals;
dict<SigBit, int> bitusers;
dict<SigBit, cell_int_t> bit2mux;
- dict<SigBit, RTLIL::Cell*> bit2driver;
typedef std::map<RTLIL::SigBit, bool> pattern_t;
typedef std::set<pattern_t> patterns_t;
typedef std::pair<RTLIL::SigBit, bool> ctrl_t;
typedef std::set<ctrl_t> ctrls_t;
- ezSatPtr ez;
- SatGen satgen;
- pool<Cell*> sat_cells;
+ ModWalker modwalker;
+ QuickConeSat qcsat;
// Used as a queue.
std::vector<Cell *> dff_cells;
- OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), ez(), satgen(ez.get(), &sigmap) {
- // Gathering three kinds of information here for every sigmapped SigBit:
+ OptDffWorker(const OptDffOptions &opt, Module *mod) : opt(opt), module(mod), sigmap(mod), initvals(&sigmap, mod), modwalker(module->design, module), qcsat(modwalker) {
+ // Gathering two kinds of information here for every sigmapped SigBit:
//
// - bitusers: how many users it has (muxes will only be merged into FFs if this is 1, making the FF the only user)
// - bit2mux: the mux cell and bit index that drives it, if any
- // - bit2driver: the cell driving it, if any
for (auto wire : module->wires())
{
for (auto conn : cell->connections()) {
bool is_output = cell->output(conn.first);
- if (is_output) {
- for (auto bit : sigmap(conn.second))
- bit2driver[bit] = cell;
- }
if (!is_output || !cell->known()) {
for (auto bit : sigmap(conn.second))
bitusers[bit]++;
}
- std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
- if (!sat_cells.insert(c).second)
- return;
- if (!satgen.importCell(c))
- return;
- for (auto &conn : c->connections()) {
- if (!c->input(conn.first))
- continue;
- for (auto bit : sigmap(conn.second))
- if (bit2driver.count(bit))
- sat_import_cell(bit2driver.at(bit));
- }
- };
-
State combine_const(State a, State b) {
if (a == State::Sx && !opt.keepdc)
return b;
if (!opt.sat)
continue;
// For each register bit, try to prove that it cannot change from the initial value. If so, remove it
- if (!bit2driver.count(ff.sig_d[i]))
+ if (!modwalker.has_drivers(ff.sig_d.extract(i)))
continue;
if (val != State::S0 && val != State::S1)
continue;
- sat_import_cell(bit2driver.at(ff.sig_d[i]));
+ int init_sat_pi = qcsat.importSigBit(val);
+ int q_sat_pi = qcsat.importSigBit(ff.sig_q[i]);
+ int d_sat_pi = qcsat.importSigBit(ff.sig_d[i]);
- int init_sat_pi = satgen.importSigSpec(val).front();
- int q_sat_pi = satgen.importSigBit(ff.sig_q[i]);
- int d_sat_pi = satgen.importSigBit(ff.sig_d[i]);
+ qcsat.prepare();
// Try to find out whether the register bit can change under some circumstances
- bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
+ bool counter_example_found = qcsat.ez->solve(qcsat.ez->IFF(q_sat_pi, init_sat_pi), qcsat.ez->NOT(qcsat.ez->IFF(d_sat_pi, init_sat_pi)));
// If the register bit cannot change, we can replace it with a constant
if (counter_example_found)
*/
#include "kernel/yosys.h"
-#include "kernel/satgen.h"
+#include "kernel/qcsat.h"
#include "kernel/sigtools.h"
#include "kernel/modtools.h"
#include "kernel/utils.h"
std::map<RTLIL::Cell*, std::set<RTLIL::Cell*, cell_ptr_cmp>, cell_ptr_cmp> topo_cell_drivers;
std::map<RTLIL::SigBit, std::set<RTLIL::Cell*, cell_ptr_cmp>> topo_bit_drivers;
- std::vector<std::pair<RTLIL::SigBit, RTLIL::SigBit>> exclusive_ctrls;
-
// ------------------------------------------------------------------------------
// Find terminal bits -- i.e. bits that do not (exclusively) feed into a mux tree
recursion_state.clear();
topo_cell_drivers.clear();
topo_bit_drivers.clear();
- exclusive_ctrls.clear();
terminal_bits.clear();
shareable_cells.clear();
forbidden_controls_cache.clear();
log("Found %d cells in module %s that may be considered for resource sharing.\n",
GetSize(shareable_cells), log_id(module));
- for (auto cell : module->cells())
- if (cell->type == ID($pmux))
- for (auto bit : cell->getPort(ID::S))
- for (auto other_bit : cell->getPort(ID::S))
- if (bit < other_bit)
- exclusive_ctrls.push_back(std::pair<RTLIL::SigBit, RTLIL::SigBit>(bit, other_bit));
-
while (!shareable_cells.empty() && config.limit != 0)
{
RTLIL::Cell *cell = *shareable_cells.begin();
optimize_activation_patterns(filtered_cell_activation_patterns);
optimize_activation_patterns(filtered_other_cell_activation_patterns);
- ezSatPtr ez;
- SatGen satgen(ez.get(), &modwalker.sigmap);
+ QuickConeSat qcsat(modwalker);
+ if (config.opt_fast) {
+ qcsat.max_cell_outs = 3;
+ qcsat.max_cell_count = 100;
+ }
pool<RTLIL::Cell*> sat_cells;
std::set<RTLIL::SigBit> bits_queue;
for (auto &p : filtered_cell_activation_patterns) {
log(" Activation pattern for cell %s: %s = %s\n", log_id(cell), log_signal(p.first), log_signal(p.second));
- cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
+ cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
all_ctrl_signals.append(p.first);
}
for (auto &p : filtered_other_cell_activation_patterns) {
log(" Activation pattern for cell %s: %s = %s\n", log_id(other_cell), log_signal(p.first), log_signal(p.second));
- other_cell_active.push_back(ez->vec_eq(satgen.importSigSpec(p.first), satgen.importSigSpec(p.second)));
+ other_cell_active.push_back(qcsat.ez->vec_eq(qcsat.importSig(p.first), qcsat.importSig(p.second)));
all_ctrl_signals.append(p.first);
}
- for (auto &bit : cell_activation_signals.to_sigbit_vector())
- bits_queue.insert(bit);
-
- for (auto &bit : other_cell_activation_signals.to_sigbit_vector())
- bits_queue.insert(bit);
-
- while (!bits_queue.empty())
- {
- pool<ModWalker::PortBit> portbits;
- modwalker.get_drivers(portbits, bits_queue);
- bits_queue.clear();
-
- for (auto &pbit : portbits)
- if (sat_cells.count(pbit.cell) == 0 && cone_ct.cell_known(pbit.cell->type)) {
- if (config.opt_fast && modwalker.cell_outputs[pbit.cell].size() >= 4)
- continue;
- // log(" Adding cell %s (%s) to SAT problem.\n", log_id(pbit.cell), log_id(pbit.cell->type));
- bits_queue.insert(modwalker.cell_inputs[pbit.cell].begin(), modwalker.cell_inputs[pbit.cell].end());
- satgen.importCell(pbit.cell);
- sat_cells.insert(pbit.cell);
- }
-
- if (config.opt_fast && sat_cells.size() > 100)
- break;
- }
-
- for (auto it : exclusive_ctrls)
- if (satgen.importedSigBit(it.first) && satgen.importedSigBit(it.second)) {
- log(" Adding exclusive control bits: %s vs. %s\n", log_signal(it.first), log_signal(it.second));
- int sub1 = satgen.importSigBit(it.first);
- int sub2 = satgen.importSigBit(it.second);
- ez->assume(ez->NOT(ez->AND(sub1, sub2)));
- }
+ qcsat.prepare();
- if (!ez->solve(ez->expression(ez->OpOr, cell_active))) {
+ int sub1 = qcsat.ez->expression(qcsat.ez->OpOr, cell_active);
+ if (!qcsat.ez->solve(sub1)) {
log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(cell));
cells_to_remove.insert(cell);
break;
}
- if (!ez->solve(ez->expression(ez->OpOr, other_cell_active))) {
+ int sub2 = qcsat.ez->expression(qcsat.ez->OpOr, other_cell_active);
+ if (!qcsat.ez->solve(sub2)) {
log(" According to the SAT solver the cell %s is never active. Sharing is pointless, we simply remove it.\n", log_id(other_cell));
cells_to_remove.insert(other_cell);
shareable_cells.erase(other_cell);
continue;
}
- ez->non_incremental();
+ qcsat.ez->non_incremental();
all_ctrl_signals.sort_and_unify();
- std::vector<int> sat_model = satgen.importSigSpec(all_ctrl_signals);
+ std::vector<int> sat_model = qcsat.importSig(all_ctrl_signals);
std::vector<bool> sat_model_values;
- int sub1 = ez->expression(ez->OpOr, cell_active);
- int sub2 = ez->expression(ez->OpOr, other_cell_active);
- ez->assume(ez->AND(sub1, sub2));
+ qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
log(" Size of SAT problem: %d cells, %d variables, %d clauses\n",
- GetSize(sat_cells), ez->numCnfVariables(), ez->numCnfClauses());
+ GetSize(sat_cells), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
- if (ez->solve(sat_model, sat_model_values)) {
+ if (qcsat.ez->solve(sat_model, sat_model_values)) {
log(" According to the SAT solver this pair of cells can not be shared.\n");
log(" Model from SAT solver: %s = %d'", log_signal(all_ctrl_signals), GetSize(sat_model_values));
for (int i = GetSize(sat_model_values)-1; i >= 0; i--)
projects / yosys.git / commitdiff