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

3 files changed, 182 insertions, 2 deletions

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 <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;
+}
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 <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