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 --- kernel/modtools.h | 6 ++-- kernel/qcsat.cc | 102 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/qcsat.h | 76 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 182 insertions(+), 2 deletions(-) create mode 100644 kernel/qcsat.cc create mode 100644 kernel/qcsat.h (limited to 'kernel') 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 -- cgit v1.2.3