2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2021 Marcelina Kościelnicka <mwk@0x04.net>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
23 #include "kernel/satgen.h"
24 #include "kernel/modtools.h"
28 // This is a helper class meant for easy construction of quick SAT queries
29 // to a combinatorial input cone of some set of signals, meant for SAT-based
30 // optimizations. Various knobs are provided to set just how much of the
31 // cone should be included in the model — since this class is meant for
32 // optimization, it should not be a correctness problem when some cells are
33 // skipped and the solver spuriously returns SAT with a solution that
34 // cannot exist in reality due to skipped constraints (ie. only UNSAT results
35 // from this class should be considered binding).
41 // The effort level knobs.
43 // The maximum "complexity level" of cells that will be imported.
44 // - 1: bitwise operations, muxes, equality comparisons, lut, sop, fa
45 // - 2: addition, subtraction, greater/less than comparisons, lcu
47 // - 4: multiplication, division, power
48 int max_cell_complexity
= 2;
49 // The maximum number of cells to import, or 0 for no limit.
50 int max_cell_count
= 0;
51 // If non-0, skip importing cells with more than this number of output bits.
52 int max_cell_outs
= 0;
55 pool
<RTLIL::Cell
*> imported_cells
;
56 pool
<RTLIL::Wire
*> imported_onehot
;
57 pool
<RTLIL::SigBit
> bits_queue
;
59 QuickConeSat(ModWalker
&modwalker
) : modwalker(modwalker
), ez(), satgen(ez
.get(), &modwalker
.sigmap
) {}
61 // Imports a signal into the SAT solver, queues its input cone to be
62 // imported in the next prepare() call.
63 std::vector
<int> importSig(SigSpec sig
);
64 int importSigBit(SigBit bit
);
66 // Imports the input cones of all previously importSig'd signals into
70 // Returns the "complexity level" of a given cell.
71 static int cell_complexity(RTLIL::Cell
*cell
);