From: Marcelina Kościelnicka Date: Tue, 3 Aug 2021 22:02:16 +0000 (+0200) Subject: Refactor common parts of SAT-using optimizations into a helper. X-Git-Tag: yosys-0.10~58 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d25b9088c83ba68b938ef9f0d97793a08001a9fe;p=yosys.git Refactor common parts of SAT-using optimizations into a helper. This also aligns the functionality: - in all cases, the onehot attribute is used to create appropriate constraints (previously, opt_dff didn't do it at all, and share created one-hot constraints based on $pmux presence alone, which is unsound) - in all cases, shift and mul/div/pow cells are now skipped when importing the SAT problem (previously only memory_share did this) — this avoids creating clauses for hard cells that are unlikely to help with proving the UNSATness needed for optimization --- diff --git a/Makefile b/Makefile index 8a7d938df..4e13da31c 100644 --- a/Makefile +++ b/Makefile @@ -575,6 +575,7 @@ $(eval $(call add_include_file,kernel/modtools.h)) $(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)) @@ -599,7 +600,7 @@ ifneq ($(ABCEXTERNAL),) 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)"' diff --git a/kernel/modtools.h b/kernel/modtools.h index bd393b5d5..4cbaf78d0 100644 --- a/kernel/modtools.h +++ b/kernel/modtools.h @@ -380,9 +380,11 @@ struct ModWalker } } - 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) diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc new file mode 100644 index 000000000..b7da958db --- /dev/null +++ b/kernel/qcsat.cc @@ -0,0 +1,102 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2021 Marcelina Kościelnicka + * + * 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 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 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 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; +} diff --git a/kernel/qcsat.h b/kernel/qcsat.h new file mode 100644 index 000000000..e4d3c3c5d --- /dev/null +++ b/kernel/qcsat.h @@ -0,0 +1,76 @@ +/* -*- c++ -*- + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2021 Marcelina Kościelnicka + * + * 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 imported_cells; + pool imported_onehot; + pool 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 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 diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc index 4e6a30ef1..91f36ce05 100644 --- a/passes/memory/memory_share.cc +++ b/passes/memory/memory_share.cc @@ -18,7 +18,7 @@ */ #include "kernel/yosys.h" -#include "kernel/satgen.h" +#include "kernel/qcsat.h" #include "kernel/sigtools.h" #include "kernel/modtools.h" #include "kernel/mem.h" @@ -32,7 +32,6 @@ struct MemoryShareWorker RTLIL::Module *module; SigMap sigmap, sigmap_xmux; ModWalker modwalker; - CellTypes cone_ct; bool flag_widen; @@ -358,56 +357,20 @@ struct MemoryShareWorker // 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 one_hot_wires; - std::set sat_cells; - std::set bits_queue; dict 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 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 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 &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 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. @@ -422,14 +385,14 @@ struct MemoryShareWorker 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; @@ -511,21 +474,7 @@ struct MemoryShareWorker 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); diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 94d6d5443..ddf08392b 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -21,7 +21,8 @@ #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" @@ -51,26 +52,23 @@ struct OptDffWorker FfInitVals initvals; dict bitusers; dict bit2mux; - dict bit2driver; typedef std::map pattern_t; typedef std::set patterns_t; typedef std::pair ctrl_t; typedef std::set ctrls_t; - ezSatPtr ez; - SatGen satgen; - pool sat_cells; + ModWalker modwalker; + QuickConeSat qcsat; // Used as a queue. std::vector 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()) { @@ -88,10 +86,6 @@ struct OptDffWorker 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]++; @@ -104,20 +98,6 @@ struct OptDffWorker } - std::function 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; @@ -594,19 +574,19 @@ struct OptDffWorker 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) diff --git a/passes/opt/share.cc b/passes/opt/share.cc index 88c4dee8b..ee1acfb7f 100644 --- a/passes/opt/share.cc +++ b/passes/opt/share.cc @@ -18,7 +18,7 @@ */ #include "kernel/yosys.h" -#include "kernel/satgen.h" +#include "kernel/qcsat.h" #include "kernel/sigtools.h" #include "kernel/modtools.h" #include "kernel/utils.h" @@ -58,8 +58,6 @@ struct ShareWorker std::map, cell_ptr_cmp> topo_cell_drivers; std::map> topo_bit_drivers; - std::vector> exclusive_ctrls; - // ------------------------------------------------------------------------------ // Find terminal bits -- i.e. bits that do not (exclusively) feed into a mux tree @@ -1156,7 +1154,6 @@ struct ShareWorker recursion_state.clear(); topo_cell_drivers.clear(); topo_bit_drivers.clear(); - exclusive_ctrls.clear(); terminal_bits.clear(); shareable_cells.clear(); forbidden_controls_cache.clear(); @@ -1171,13 +1168,6 @@ struct ShareWorker 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(bit, other_bit)); - while (!shareable_cells.empty() && config.limit != 0) { RTLIL::Cell *cell = *shareable_cells.begin(); @@ -1256,8 +1246,11 @@ struct ShareWorker 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 sat_cells; std::set bits_queue; @@ -1267,77 +1260,45 @@ struct ShareWorker 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 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 sat_model = satgen.importSigSpec(all_ctrl_signals); + std::vector sat_model = qcsat.importSig(all_ctrl_signals); std::vector 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--)