From d25b9088c83ba68b938ef9f0d97793a08001a9fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Wed, 4 Aug 2021 00:02:16 +0200 Subject: Refactor common parts of SAT-using optimizations into a helper. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- passes/memory/memory_share.cc | 71 ++++++------------------------------------- 1 file changed, 10 insertions(+), 61 deletions(-) (limited to 'passes/memory/memory_share.cc') 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); -- cgit v1.2.3