New xprop pass to encode 3-valued x-propagation using 2-valued logic

7 files changed, 2001 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index 42c5eaf47..495abdd29 100644
--- a/Makefile
+++ b/Makefile
@@ -881,6 +881,7 @@ test: $(TARGETS) $(EXTRA_TARGETS)
 	+cd tests/rpc && bash run-test.sh
 	+cd tests/memfile && bash run-test.sh
 	+cd tests/verilog && bash run-test.sh
+	+cd tests/xprop && bash run-test.sh $(SEEDOPT)
 	@echo ""
 	@echo "  Passed \"make test\"."
 	@echo ""
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index 16a38b511..8c7a18d02 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -43,3 +43,4 @@ OBJS += passes/cmds/logger.o
 OBJS += passes/cmds/printattrs.o
 OBJS += passes/cmds/sta.o
 OBJS += passes/cmds/clean_zerowidth.o
+OBJS += passes/cmds/xprop.o
diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
new file mode 100644
index 000000000..c2a1b5c44
--- /dev/null
+++ b/passes/cmds/xprop.cc
@@ -0,0 +1,1198 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2022  Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ *  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/celltypes.h"
+#include "kernel/ffinit.h"
+#include "kernel/ff.h"
+#include "kernel/modtools.h"
+#include "kernel/sigtools.h"
+#include "kernel/utils.h"
+#include "kernel/yosys.h"
+#include <deque>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct XpropOptions
+{
+	bool split_inputs = false;
+	bool split_outputs = false;
+	bool assume_encoding = false;
+	bool assert_encoding = false;
+	bool assume_def_inputs = false;
+	bool required = false;
+	bool formal = false;
+	bool debug_asserts = false;
+};
+
+struct XpropWorker
+{
+	struct EncodedBit {
+		SigBit is_0, is_1, is_x;
+		bool driven;
+	};
+
+	struct EncodedSig {
+		SigSpec is_0, is_1, is_x;
+		Module *module;
+
+		void invert() { std::swap(is_0, is_1); }
+		void auto_0() { connect_0(module->Not(NEW_ID, module->Or(NEW_ID, is_1, is_x))); }
+		void auto_1() { connect_1(module->Not(NEW_ID, module->Or(NEW_ID, is_0, is_x))); }
+		void auto_x() { connect_x(module->Not(NEW_ID, module->Or(NEW_ID, is_0, is_1))); }
+
+		void connect_0(SigSpec sig) { module->connect(is_0, sig); }
+		void connect_1(SigSpec sig) { module->connect(is_1, sig); }
+		void connect_x(SigSpec sig) { module->connect(is_x, sig); }
+
+		void connect_1_under_x(SigSpec sig) { connect_1(module->And(NEW_ID, sig, module->Not(NEW_ID, is_x))); }
+		void connect_0_under_x(SigSpec sig) { connect_0(module->And(NEW_ID, sig, module->Not(NEW_ID, is_x))); }
+
+		void connect_x_under_0(SigSpec sig) { connect_x(module->And(NEW_ID, sig, module->Not(NEW_ID, is_0))); }
+
+		void connect_as_bool() {
+			int width = GetSize(is_0);
+			if (width <= 1)
+				return;
+			module->connect(is_0.extract(1, width - 1), Const(State::S1, width - 1));
+			module->connect(is_1.extract(1, width - 1), Const(State::S0, width - 1));
+			module->connect(is_x.extract(1, width - 1), Const(State::S0, width - 1));
+			is_0 = is_0[0];
+			is_1 = is_1[0];
+			is_x = is_x[0];
+		}
+
+		int size() const { return is_0.size(); }
+	};
+
+	Module *module;
+	XpropOptions options;
+	ModWalker modwalker;
+	SigMap &sigmap;
+	FfInitVals initvals;
+
+	pool<SigBit> maybe_x_bits;
+	dict<SigBit, EncodedBit> encoded_bits;
+
+	pool<Cell *> pending_cells;
+	std::deque<Cell *> pending_cell_queue;
+
+	XpropWorker(Module *module, XpropOptions options) :
+		module(module), options(options),
+		modwalker(module->design), sigmap(modwalker.sigmap)
+	{
+		modwalker.setup(module);
+		initvals.set(&modwalker.sigmap, module);
+
+		maybe_x_bits.insert(State::Sx);
+
+		for (auto cell : module->cells()) {
+			pending_cells.insert(cell);
+			pending_cell_queue.push_back(cell);
+		}
+
+		if (!options.assume_def_inputs) {
+			for (auto port : module->ports) {
+				auto wire = module->wire(port);
+				if (wire->port_input)
+					mark_maybe_x(SigSpec(wire));
+			}
+		}
+	}
+
+	bool maybe_x(SigBit bit)
+	{
+		return maybe_x_bits.count(sigmap(bit));
+	}
+
+	bool maybe_x(const SigSpec &sig)
+	{
+		for (auto bit : sig)
+			if (maybe_x(bit)) return true;
+		return false;
+	}
+
+	bool ports_maybe_x(Cell *cell)
+	{
+		for (auto &conn : cell->connections())
+			if (maybe_x(conn.second))
+				return true;
+		return false;
+	}
+
+	bool inputs_maybe_x(Cell *cell)
+	{
+		for (auto &conn : cell->connections())
+			if (cell->input(conn.first) && maybe_x(conn.second))
+				return true;
+		return false;
+	}
+
+	void mark_maybe_x(SigBit bit)
+	{
+		sigmap.apply(bit);
+		if (!maybe_x_bits.insert(bit).second)
+			return;
+		auto it = modwalker.signal_consumers.find(bit);
+		if (it == modwalker.signal_consumers.end())
+			return;
+		for (auto &consumer : it->second)
+			if (pending_cells.insert(consumer.cell).second)
+				pending_cell_queue.push_back(consumer.cell);
+	}
+
+	void mark_maybe_x(const SigSpec &sig)
+	{
+		for (auto bit : sig)
+			mark_maybe_x(bit);
+	}
+
+	void mark_outputs_maybe_x(Cell *cell)
+	{
+		for (auto &conn : cell->connections())
+			if (cell->output(conn.first))
+				mark_maybe_x(conn.second);
+	}
+
+	EncodedSig encoded(SigSpec sig, bool driving = false)
+	{
+		EncodedSig result;
+		SigSpec invert;
+
+		if (driving)
+			result.module = module;
+
+		int new_bits = 0;
+
+		sigmap.apply(sig);
+
+		for (auto bit : sig) {
+			if (!bit.is_wire())
+				continue;
+			else if (!maybe_x(bit) && !driving)
+				invert.append(bit);
+			else if (!encoded_bits.count(bit)) {
+				new_bits += 1;
+				encoded_bits.emplace(bit, {
+					State::Sm, State::Sm, State::Sm, false
+				});
+			}
+		}
+
+		if (!invert.empty() && !driving)
+			invert = module->Not(NEW_ID, invert);
+
+		EncodedSig new_sigs;
+		if (new_bits > 0) {
+			new_sigs.is_0 = module->addWire(NEW_ID, new_bits);
+			new_sigs.is_1 = module->addWire(NEW_ID, new_bits);
+			new_sigs.is_x = module->addWire(NEW_ID, new_bits);
+		}
+
+		int invert_pos = 0;
+		int new_pos = 0;
+
+		SigSpec driven_orig;
+		EncodedSig driven_enc;
+		SigSig driven_never_x;
+
+		for (auto bit : sig)
+		{
+			if (!bit.is_wire()) {
+				result.is_0.append(bit == State::S0 ? State::S1 : State::S0);
+				result.is_1.append(bit == State::S1 ? State::S1 : State::S0);
+				result.is_x.append(bit == State::Sx ? State::S1 : State::S0);
+				continue;
+			} else if (!maybe_x(bit) && !driving) {
+				result.is_0.append(invert[invert_pos++]);
+				result.is_1.append(bit);
+				result.is_x.append(State::S0);
+				continue;
+			}
+			auto &enc = encoded_bits.at(bit);
+			if (enc.is_0 == State::Sm) {
+				enc.is_0 = new_sigs.is_0[new_pos];
+				enc.is_1 = new_sigs.is_1[new_pos];
+				enc.is_x = new_sigs.is_x[new_pos];
+				new_pos++;
+			}
+			if (driving) {
+				log_assert(!enc.driven);
+				enc.driven = true;
+				if (maybe_x(bit)) {
+					driven_orig.append(bit);
+					driven_enc.is_0.append(enc.is_0);
+					driven_enc.is_1.append(enc.is_1);
+					driven_enc.is_x.append(enc.is_x);
+				} else {
+					driven_never_x.first.append(bit);
+					driven_never_x.second.append(enc.is_1);
+				}
+			}
+			result.is_0.append(enc.is_0);
+			result.is_1.append(enc.is_1);
+			result.is_x.append(enc.is_x);
+		}
+
+		if (!driven_orig.empty()) {
+			module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+		}
+		if (!driven_never_x.first.empty()) {
+			module->connect(driven_never_x);
+		}
+
+		if (driving && (options.assert_encoding || options.assume_encoding)) {
+			auto not_0 = module->Not(NEW_ID, result.is_0);
+			auto not_1 = module->Not(NEW_ID, result.is_1);
+			auto not_x = module->Not(NEW_ID, result.is_x);
+			auto valid = module->ReduceAnd(NEW_ID, {
+				module->Eq(NEW_ID, result.is_0, module->And(NEW_ID, not_1, not_x)),
+				module->Eq(NEW_ID, result.is_1, module->And(NEW_ID, not_0, not_x)),
+				module->Eq(NEW_ID, result.is_x, module->And(NEW_ID, not_0, not_1)),
+			});
+			if (options.assert_encoding)
+				module->addAssert(NEW_ID_SUFFIX("xprop_enc"), valid, State::S1);
+			else
+				module->addAssume(NEW_ID_SUFFIX("xprop_enc"), valid, State::S1);
+			if (options.debug_asserts) {
+				auto bad_bits = module->Bweqx(NEW_ID, {result.is_0, result.is_1, result.is_x}, Const(State::Sx, GetSize(result) * 3));
+				module->addAssert(NEW_ID_SUFFIX("xprop_debug"), module->LogicNot(NEW_ID, bad_bits), State::S1);
+			}
+		}
+
+		return result;
+	}
+
+	void mark_all_maybe_x()
+	{
+		while (!pending_cell_queue.empty()) {
+			Cell *cell = pending_cell_queue.front();
+			pending_cell_queue.pop_front();
+			pending_cells.erase(cell);
+
+			mark_maybe_x(cell);
+		}
+	}
+
+	void mark_maybe_x(Cell *cell) {
+		if (cell->type.in(ID($bweqx), ID($eqx), ID($nex), ID($initstate), ID($assert), ID($assume), ID($cover), ID($anyseq), ID($anyconst)))
+			return;
+
+		if (cell->type.in(ID($pmux))) {
+			mark_outputs_maybe_x(cell);
+			return;
+		}
+
+		if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
+			FfData ff(&initvals, cell);
+
+			if (cell->type != ID($anyinit))
+				for (int i = 0; i < ff.width; i++)
+					if (ff.val_init[i] == State::Sx)
+						mark_maybe_x(ff.sig_q[i]);
+
+			for (int i = 0; i < ff.width; i++)
+				if (maybe_x(ff.sig_d[i]))
+					mark_maybe_x(ff.sig_q[i]);
+
+			if ((ff.has_clk || ff.has_gclk) && !ff.has_ce && !ff.has_aload && !ff.has_srst && !ff.has_arst && !ff.has_sr)
+				return;
+		}
+
+		if (cell->type == ID($not)) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A); sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+			for (int i = 0; i < GetSize(sig_y); i++)
+				if (maybe_x(sig_a[i]))
+					mark_maybe_x(sig_y[i]);
+			return;
+		}
+
+		if (cell->type.in(ID($and), ID($or), ID($xor), ID($xnor))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A); sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+			auto sig_b = cell->getPort(ID::B); sig_b.extend_u0(GetSize(sig_y), cell->getParam(ID::B_SIGNED).as_bool());
+			for (int i = 0; i < GetSize(sig_y); i++)
+				if (maybe_x(sig_a[i]) || maybe_x(sig_b[i]))
+					mark_maybe_x(sig_y[i]);
+			return;
+		}
+
+		if (cell->type.in(ID($bwmux))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+			auto &sig_s = cell->getPort(ID::S);
+			for (int i = 0; i < GetSize(sig_y); i++)
+				if (maybe_x(sig_a[i]) || maybe_x(sig_b[i]) || maybe_x(sig_s[i]))
+					mark_maybe_x(sig_y[i]);
+			return;
+		}
+
+		if (cell->type.in(ID($_MUX_), ID($mux), ID($bmux))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+			auto &sig_s = cell->getPort(ID::S);
+			if (maybe_x(sig_s)) {
+				mark_maybe_x(sig_y);
+				return;
+			}
+			for (int i = 0; i < GetSize(sig_y); i++) {
+				if (maybe_x(sig_a[i])) {
+					mark_maybe_x(sig_y[i]);
+					continue;
+				}
+				for (int j = i; j < GetSize(sig_b); j += GetSize(sig_y)) {
+					if (maybe_x(sig_b[j])) {
+						mark_maybe_x(sig_y[i]);
+						break;
+					}
+				}
+			}
+			return;
+		}
+
+		if (cell->type.in(ID($demux))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_s = cell->getPort(ID::S);
+			if (maybe_x(sig_s)) {
+				mark_maybe_x(sig_y);
+				return;
+			}
+			for (int i = 0; i < GetSize(sig_a); i++)
+				if (maybe_x(sig_a[i]))
+					for (int j = i; j < GetSize(sig_y); j += GetSize(sig_a))
+						mark_maybe_x(sig_y[j]);
+			return;
+		}
+
+		if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift))) {
+			auto &sig_b = cell->getPort(ID::B);
+			auto &sig_y = cell->getPort(ID::Y);
+
+			if (maybe_x(sig_b)) {
+				mark_maybe_x(sig_y);
+				return;
+			}
+
+			auto &sig_a = cell->getPort(ID::A);
+
+			if (maybe_x(sig_a)) {
+				// We could be more precise for shifts, but that's not required
+				// for correctness, so let's keep it simple
+				mark_maybe_x(sig_y);
+				return;
+			}
+			return;
+		}
+
+		if (cell->type.in(ID($shiftx))) {
+			auto &sig_b = cell->getPort(ID::B);
+			auto &sig_y = cell->getPort(ID::Y);
+
+			if (cell->getParam(ID::B_SIGNED).as_bool() || GetSize(sig_b) >= 30) {
+				mark_maybe_x(sig_y);
+			} else {
+				int max_shift = (1 << GetSize(sig_b)) - 1;
+
+				auto &sig_a = cell->getPort(ID::A);
+
+				for (int i = 0; i < GetSize(sig_y); i++)
+					if (i + max_shift >= GetSize(sig_a))
+						mark_maybe_x(sig_y[i]);
+			}
+
+			if (maybe_x(sig_b)) {
+				mark_maybe_x(sig_y);
+				return;
+			}
+
+			auto &sig_a = cell->getPort(ID::A);
+			if (maybe_x(sig_a)) {
+				// We could be more precise for shifts, but that's not required
+				// for correctness, so let's keep it simple
+				mark_maybe_x(sig_y);
+				return;
+			}
+			return;
+		}
+
+		if (cell->type.in(ID($add), ID($sub), ID($mul), ID($neg))) {
+			if (inputs_maybe_x(cell))
+				mark_outputs_maybe_x(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
+			mark_outputs_maybe_x(cell);
+			return;
+		}
+
+		if (cell->type.in(
+			ID($le), ID($lt), ID($ge), ID($gt),
+			ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_xnor),
+			ID($reduce_bool), ID($logic_not), ID($logic_or), ID($logic_and),
+			ID($eq), ID($ne),
+
+			ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_ANDNOT_), ID($_OR_), ID($_NOR_), ID($_ORNOT_), ID($_XOR_), ID($_XNOR_)
+		)) {
+			auto &sig_y = cell->getPort(ID::Y);
+			if (inputs_maybe_x(cell))
+				mark_maybe_x(sig_y[0]);
+			return;
+		}
+
+		log_warning("Unhandled cell %s (%s) during maybe-x marking\n", log_id(cell), log_id(cell->type));
+		mark_outputs_maybe_x(cell);
+	}
+
+	void process_cells()
+	{
+		for (auto cell : module->selected_cells())
+			process_cell(cell);
+	}
+
+	void process_cell(Cell *cell)
+	{
+		if (!ports_maybe_x(cell)) {
+
+			if (cell->type == ID($bweq)) {
+				auto sig_y = cell->getPort(ID::Y);
+				auto sig_a = cell->getPort(ID::A);
+				auto sig_b = cell->getPort(ID::B);
+
+				auto name = cell->name;
+				module->remove(cell);
+				module->addXnor(name, sig_a, sig_b, sig_y);
+				return;
+			}
+
+			if (cell->type.in(ID($nex), ID($eqx))) {
+				auto sig_y = cell->getPort(ID::Y);
+				auto sig_a = cell->getPort(ID::A);
+				auto sig_b = cell->getPort(ID::B);
+
+				auto name = cell->name;
+				module->remove(cell);
+				if (cell->type == ID($eqx))
+					module->addEq(name, sig_a, sig_b, sig_y);
+				else
+					module->addNe(name, sig_a, sig_b, sig_y);
+				return;
+			}
+
+			return;
+		}
+
+		if (cell->type.in(ID($not), ID($_NOT_))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A);
+			if (cell->type == ID($not))
+				sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+
+			auto enc_a = encoded(sig_a);
+			auto enc_y = encoded(sig_y, true);
+
+			enc_y.connect_x(enc_a.is_x);
+			enc_y.connect_0(enc_a.is_1);
+			enc_y.connect_1(enc_a.is_0);
+
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($and), ID($or), ID($_AND_), ID($_OR_), ID($_NAND_), ID($_NOR_), ID($_ANDNOT_), ID($_ORNOT_))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A);
+			auto sig_b = cell->getPort(ID::B);
+			if (cell->type.in(ID($and), ID($or))) {
+				sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+				sig_b.extend_u0(GetSize(sig_y), cell->getParam(ID::B_SIGNED).as_bool());
+			}
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_y = encoded(sig_y, true);
+
+			if (cell->type.in(ID($or), ID($_OR_)))
+				enc_a.invert(), enc_b.invert(), enc_y.invert();
+			if (cell->type.in(ID($_NAND_), ID($_NOR_)))
+				enc_y.invert();
+			if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
+				enc_b.invert();
+
+			enc_y.connect_0(module->Or(NEW_ID, enc_a.is_0, enc_b.is_0));
+			enc_y.connect_1(module->And(NEW_ID, enc_a.is_1, enc_b.is_1));
+			enc_y.auto_x();
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool), ID($logic_not))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+
+			auto enc_a = encoded(sig_a);
+			auto enc_y = encoded(sig_y, true);
+
+			enc_y.connect_as_bool();
+
+			if (cell->type.in(ID($reduce_or), ID($reduce_bool)))
+				enc_a.invert(), enc_y.invert();
+			if (cell->type == ID($logic_not))
+				enc_a.invert();
+
+			enc_y.connect_0(module->ReduceOr(NEW_ID, enc_a.is_0));
+			enc_y.connect_1(module->ReduceAnd(NEW_ID, enc_a.is_1));
+			enc_y.auto_x();
+			module->remove(cell);
+
+			return;
+		}
+
+		if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+
+			auto enc_a = encoded(sig_a);
+			auto enc_y = encoded(sig_y, true);
+
+			enc_y.connect_as_bool();
+			if (cell->type == ID($reduce_xnor))
+				enc_y.invert();
+
+
+			enc_y.connect_x(module->ReduceOr(NEW_ID, enc_a.is_x));
+			enc_y.connect_1_under_x(module->ReduceXor(NEW_ID, enc_a.is_1));
+			enc_y.auto_0();
+			module->remove(cell);
+
+			return;
+		}
+
+		if (cell->type.in(ID($logic_and), ID($logic_or))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_y = encoded(sig_y, true);
+
+			enc_y.connect_as_bool();
+
+			auto a_is_1 = module->ReduceOr(NEW_ID, enc_a.is_1);
+			auto a_is_0 = module->ReduceAnd(NEW_ID, enc_a.is_0);
+			auto b_is_1 = module->ReduceOr(NEW_ID, enc_b.is_1);
+			auto b_is_0 = module->ReduceAnd(NEW_ID, enc_b.is_0);
+
+			if (cell->type == ID($logic_or))
+				 enc_y.invert(), std::swap(a_is_0, a_is_1), std::swap(b_is_0, b_is_1);
+
+			enc_y.connect_0(module->Or(NEW_ID, a_is_0, b_is_0));
+			enc_y.connect_1(module->And(NEW_ID, a_is_1, b_is_1));
+			enc_y.auto_x();
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($xor), ID($xnor), ID($_XOR_), ID($_XNOR_))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A);
+			auto sig_b = cell->getPort(ID::B);
+			if (cell->type.in(ID($xor), ID($xnor))) {
+				sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
+				sig_b.extend_u0(GetSize(sig_y), cell->getParam(ID::B_SIGNED).as_bool());
+			}
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_y = encoded(sig_y, true);
+
+			if (cell->type.in(ID($xnor), ID($_XNOR_)))
+				enc_y.invert();
+
+			enc_y.connect_x(module->Or(NEW_ID, enc_a.is_x, enc_b.is_x));
+			enc_y.connect_1_under_x(module->Xor(NEW_ID, enc_a.is_1, enc_b.is_1));
+			enc_y.auto_0();
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($eq), ID($ne))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A);
+			auto sig_b = cell->getPort(ID::B);
+			int width = std::max(GetSize(sig_a), GetSize(sig_b));
+			sig_a.extend_u0(width, cell->getParam(ID::A_SIGNED).as_bool());
+			sig_b.extend_u0(width, cell->getParam(ID::B_SIGNED).as_bool());
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_y = encoded(sig_y, true);
+			enc_y.connect_as_bool();
+
+			if (cell->type == ID($ne))
+				enc_y.invert();
+
+			auto delta = module->Xor(NEW_ID, enc_a.is_1, enc_b.is_1);
+			auto xpos = module->Or(NEW_ID, enc_a.is_x, enc_b.is_x);
+
+			enc_y.connect_0(module->ReduceOr(NEW_ID, module->And(NEW_ID, delta, module->Not(NEW_ID, xpos))));
+			enc_y.connect_x_under_0(module->ReduceOr(NEW_ID, xpos));
+			enc_y.auto_1();
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($eqx), ID($nex))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto sig_a = cell->getPort(ID::A);
+			auto sig_b = cell->getPort(ID::B);
+			int width = std::max(GetSize(sig_a), GetSize(sig_b));
+			sig_a.extend_u0(width, cell->getParam(ID::A_SIGNED).as_bool());
+			sig_b.extend_u0(width, cell->getParam(ID::B_SIGNED).as_bool());
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+
+			auto delta_0 = module->Xnor(NEW_ID, enc_a.is_0, enc_b.is_0);
+			auto delta_1 = module->Xnor(NEW_ID, enc_a.is_1, enc_b.is_1);
+
+			auto eq = module->ReduceAnd(NEW_ID, {delta_0, delta_1});
+
+			auto res = cell->type == ID($nex) ? module->Not(NEW_ID, eq) : eq;
+
+			module->connect(sig_y[0], res);
+			if (GetSize(sig_y) > 1)
+				module->connect(sig_y.extract(1, GetSize(sig_y) - 1), Const(State::S0, GetSize(sig_y) - 1));
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($bweqx))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+
+			auto delta_0 = module->Xnor(NEW_ID, enc_a.is_0, enc_b.is_0);
+			auto delta_1 = module->Xnor(NEW_ID, enc_a.is_1, enc_b.is_1);
+			module->addAnd(NEW_ID, delta_0, delta_1, sig_y);
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($_MUX_), ID($mux), ID($bwmux))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+			auto sig_s = cell->getPort(ID::S);
+
+			if (cell->type == ID($mux))
+				sig_s = SigSpec(sig_s[0], GetSize(sig_y));
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_s = encoded(sig_s);
+			auto enc_y = encoded(sig_y, true);
+
+			enc_y.connect_1(module->And(NEW_ID,
+					module->Or(NEW_ID, enc_a.is_1, enc_s.is_1),
+					module->Or(NEW_ID, enc_b.is_1, enc_s.is_0)));
+			enc_y.connect_0(module->And(NEW_ID,
+					module->Or(NEW_ID, enc_a.is_0, enc_s.is_1),
+					module->Or(NEW_ID, enc_b.is_0, enc_s.is_0)));
+			enc_y.auto_x();
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($pmux))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+			auto &sig_s = cell->getPort(ID::S);
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_s = encoded(sig_s);
+			auto enc_y = encoded(sig_y, true);
+
+			int width = GetSize(enc_y);
+
+			auto all_x = module->ReduceOr(NEW_ID, {
+				enc_s.is_x,
+				module->And(NEW_ID, enc_s.is_1, module->Sub(NEW_ID, enc_s.is_1, Const(1, width)))
+			});
+
+			auto selected = enc_a;
+
+			for (int i = 0; i < GetSize(enc_s); i++) {
+				auto sel_bit = enc_s.is_1[i];
+				selected.is_0 = module->Mux(NEW_ID, selected.is_0, enc_b.is_0.extract(i * width, width), sel_bit);
+				selected.is_1 = module->Mux(NEW_ID, selected.is_1, enc_b.is_1.extract(i * width, width), sel_bit);
+				selected.is_x = module->Mux(NEW_ID, selected.is_x, enc_b.is_x.extract(i * width, width), sel_bit);
+			}
+
+			enc_y.connect_0(module->Mux(NEW_ID, selected.is_0, Const(State::S0, width), all_x));
+			enc_y.connect_1(module->Mux(NEW_ID, selected.is_1, Const(State::S0, width), all_x));
+			enc_y.connect_x(module->Mux(NEW_ID, selected.is_x, Const(State::S1, width), all_x));
+
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) {
+			auto &sig_y = cell->getPort(ID::Y);
+			auto &sig_a = cell->getPort(ID::A);
+			auto &sig_b = cell->getPort(ID::B);
+
+			auto enc_a = encoded(sig_a);
+			auto enc_b = encoded(sig_b);
+			auto enc_y = encoded(sig_y, true);
+
+			auto all_x = module->ReduceOr(NEW_ID, enc_b.is_x)[0];
+			auto not_all_x = module->Not(NEW_ID, all_x)[0];
+
+			SigSpec y_not_0 = module->addWire(NEW_ID, GetSize(sig_y));
+			SigSpec y_1 = module->addWire(NEW_ID, GetSize(sig_y));
+			SigSpec y_x = module->addWire(NEW_ID, GetSize(sig_y));
+
+			auto encoded_type = cell->type == ID($shiftx) ? ID($shift) : cell->type;
+
+			if (cell->type == ID($shiftx)) {
+				std::swap(enc_a.is_0, enc_a.is_x);
+			}
+
+			auto shift_0 = module->addCell(NEW_ID, encoded_type);
+			shift_0->parameters = cell->parameters;
+			shift_0->setPort(ID::A, module->Not(NEW_ID, enc_a.is_0));
+			shift_0->setPort(ID::B, enc_b.is_1);
+			shift_0->setPort(ID::Y, y_not_0);
+
+			auto shift_1 = module->addCell(NEW_ID, encoded_type);
+			shift_1->parameters = cell->parameters;
+			shift_1->setPort(ID::A, enc_a.is_1);
+			shift_1->setPort(ID::B, enc_b.is_1);
+			shift_1->setPort(ID::Y, y_1);
+
+			auto shift_x = module->addCell(NEW_ID, encoded_type);
+			shift_x->parameters = cell->parameters;
+			shift_x->setPort(ID::A, enc_a.is_x);
+			shift_x->setPort(ID::B, enc_b.is_1);
+			shift_x->setPort(ID::Y, y_x);
+
+			SigSpec y_0 = module->Not(NEW_ID, y_not_0);
+
+			if (cell->type == ID($shiftx))
+				std::swap(y_0, y_x);
+
+			enc_y.connect_0(module->And(NEW_ID, y_0, SigSpec(not_all_x, GetSize(sig_y))));
+			enc_y.connect_1(module->And(NEW_ID, y_1, SigSpec(not_all_x, GetSize(sig_y))));
+			enc_y.connect_x(module->Or(NEW_ID, y_x, SigSpec(all_x, GetSize(sig_y))));
+
+			module->remove(cell);
+			return;
+		}
+
+		if (cell->type.in(ID($ff))) {
+			auto &sig_d = cell->getPort(ID::D);
+			auto &sig_q = cell->getPort(ID::Q);
+
+			auto init_q = initvals(sig_q);
+			auto init_q_is_1 = init_q;
+			auto init_q_is_x = init_q;
+
+			for (auto &bit : init_q_is_1)
+				bit = bit == State::S1 ? State::S1 : State::S0;
+			for (auto &bit : init_q_is_x)
+				bit = bit == State::Sx ? State::S1 : State::S0;
+
+			initvals.remove_init(sig_q);
+
+			auto enc_d = encoded(sig_d);
+			auto enc_q = encoded(sig_q, true);
+
+			auto data_q = module->addWire(NEW_ID, GetSize(sig_q));
+
+			module->addFf(NEW_ID, enc_d.is_1, data_q);
+			module->addFf(NEW_ID, enc_d.is_x, enc_q.is_x);
+
+			initvals.set_init(data_q, init_q_is_1);
+			initvals.set_init(enc_q.is_x, init_q_is_x);
+
+			enc_q.connect_1_under_x(data_q);
+			enc_q.auto_0();
+
+			module->remove(cell);
+			return;
+		}
+
+		if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
+			FfData ff(&initvals, cell);
+
+			if ((ff.has_clk || ff.has_gclk) && !ff.has_ce && !ff.has_aload && !ff.has_srst && !ff.has_arst && !ff.has_sr) {
+				if (ff.has_clk && maybe_x(ff.sig_clk)) {
+					log_warning("Only non-x CLK inputs are currently supported for %s (%s)\n", log_id(cell), log_id(cell->type));
+				} else {
+					auto init_q = ff.val_init;
+					auto init_q_is_1 = init_q;
+					auto init_q_is_x = init_q;
+
+					if (ff.is_anyinit) {
+						for (auto &bit : init_q_is_1)
+							bit = State::Sx;
+						for (auto &bit : init_q_is_x)
+							bit = State::S0;
+					} else {
+						for (auto &bit : init_q_is_1)
+							bit = bit == State::S1 ? State::S1 : State::S0;
+						for (auto &bit : init_q_is_x)
+							bit = bit == State::Sx ? State::S1 : State::S0;
+					}
+
+					ff.remove();
+
+					auto enc_d = encoded(ff.sig_d);
+					auto enc_q = encoded(ff.sig_q, true);
+
+					auto data_q = module->addWire(NEW_ID, GetSize(ff.sig_q));
+
+					ff.sig_d = enc_d.is_1;
+					ff.sig_q = data_q;
+					ff.val_init = init_q_is_1;
+					ff.emit();
+
+					ff.name = NEW_ID;
+					ff.cell = nullptr;
+					ff.sig_d = enc_d.is_x;
+					ff.sig_q = enc_q.is_x;
+					ff.is_anyinit = false;
+					ff.val_init = init_q_is_x;
+					ff.emit();
+
+
+					enc_q.connect_1_under_x(data_q);
+					enc_q.auto_0();
+
+					return;
+				}
+			} else {
+				log_warning("Unhandled FF-cell %s (%s), consider running clk2fflogic, async2sync and/or dffunmap\n", log_id(cell), log_id(cell->type));
+			}
+		}
+
+		// Celltypes where any input x bit makes the whole output x
+		if (cell->type.in(
+			ID($neg),
+			ID($le), ID($lt), ID($ge), ID($gt),
+			ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor)
+		)) {
+
+			SigSpec inbits_x;
+			for (auto &conn : cell->connections()) {
+				if (cell->input(conn.first)) {
+					auto enc_port = encoded(conn.second);
+					inbits_x.append(enc_port.is_x);
+					cell->setPort(conn.first, enc_port.is_1);
+				}
+			}
+
+			if (cell->type.in(ID($div), ID($mod), ID($divfloor), ID($modfloor))) {
+				auto sig_b = cell->getPort(ID::B);
+				auto invalid = module->LogicNot(NEW_ID, sig_b);
+				inbits_x.append(invalid);
+				sig_b[0] = module->Or(NEW_ID, sig_b[0], invalid);
+				cell->setPort(ID::B, sig_b);
+			}
+
+			SigBit outbits_x = (GetSize(inbits_x) == 1 ? inbits_x : module->ReduceOr(NEW_ID, inbits_x));
+
+			bool bool_out = cell->type.in(ID($le), ID($lt), ID($ge), ID($gt));
+
+			for (auto &conn : cell->connections()) {
+				if (cell->output(conn.first)) {
+					auto enc_port = encoded(conn.second, true);
+					if (bool_out)
+						enc_port.connect_as_bool();
+
+					SigSpec new_output = module->addWire(NEW_ID, GetSize(conn.second));
+
+					enc_port.connect_1_under_x(bool_out ? new_output.extract(0) : new_output);
+					enc_port.connect_x(SigSpec(outbits_x, GetSize(enc_port)));
+					enc_port.auto_0();
+
+					cell->setPort(conn.first, new_output);
+				}
+			}
+
+			return;
+		}
+
+		if (cell->type == ID($bmux)) // TODO might want to support bmux natively anyway
+			log("Running 'bmuxmap' preserves x-propagation and can be run before 'xprop'.\n");
+		if (cell->type == ID($demux)) // TODO might want to support demux natively anyway
+			log("Running 'demuxmap' preserves x-propagation and can be run before 'xprop'.\n");
+
+		if (options.required)
+			log_error("Unhandled cell %s (%s)\n", log_id(cell), log_id(cell->type));
+		else
+			log_warning("Unhandled cell %s (%s)\n", log_id(cell), log_id(cell->type));
+	}
+
+	void split_ports()
+	{
+		if (!options.split_inputs && !options.split_outputs)
+			return;
+
+		vector<IdString> new_ports;
+
+		for (auto port : module->ports) {
+			auto wire = module->wire(port);
+			if (module->design->selected(module, wire)) {
+				if (wire->port_input == wire->port_output) {
+					log_warning("Port %s not an input or an output port which is not supported by xprop\n", log_id(wire));
+				} else if ((options.split_inputs && !options.assume_def_inputs && wire->port_input) || (options.split_outputs && wire->port_output)) {
+					auto port_d = module->uniquify(stringf("%s_d", port.c_str()));
+					auto port_x = module->uniquify(stringf("%s_x", port.c_str()));
+
+					auto wire_d = module->addWire(port_d, GetSize(wire));
+					auto wire_x = module->addWire(port_x, GetSize(wire));
+
+					wire_d->port_input = wire->port_input;
+					wire_d->port_output = wire->port_output;
+					wire_d->port_id = GetSize(new_ports) + 1;
+
+					wire_x->port_input = wire->port_input;
+					wire_x->port_output = wire->port_output;
+					wire_x->port_id = GetSize(new_ports) + 2;
+
+					if (wire->port_output) {
+						auto enc = encoded(wire);
+						module->connect(wire_d, enc.is_1);
+						module->connect(wire_x, enc.is_x);
+					} else {
+						auto enc = encoded(wire, true);
+
+						enc.connect_x(wire_x);
+						enc.connect_1_under_x(wire_d);
+						enc.auto_0();
+					}
+
+					wire->port_input = wire->port_output = false;
+					wire->port_id = 0;
+
+					new_ports.push_back(port_d);
+					new_ports.push_back(port_x);
+
+					continue;
+				}
+			}
+			wire->port_id = GetSize(new_ports) + 1;
+			new_ports.push_back(port);
+		}
+
+		module->ports = new_ports;
+
+		module->fixup_ports();
+	}
+
+	void encode_remaining()
+	{
+		pool<Wire *> enc_undriven_wires;
+
+		for (auto &enc_bit : encoded_bits) {
+			if (!enc_bit.second.driven) {
+				log_assert(enc_bit.first.is_wire());
+				enc_undriven_wires.insert(enc_bit.first.wire);
+			}
+		}
+
+		if (options.formal && !enc_undriven_wires.empty()) {
+			for (auto &bit : enc_undriven_wires)
+				log_warning("Found encoded wire %s having a non-encoded driver\n", log_signal(bit));
+
+			log_error("Found encoded wires having a non-encoded driver, not allowed in -formal mode\n");
+		}
+
+
+		for (auto wire : enc_undriven_wires) {
+			SigSpec sig(sigmap(wire));
+
+			SigSpec orig;
+			EncodedSig enc;
+
+			for (auto bit : sig) {
+				auto it = encoded_bits.find(bit);
+				if (it == encoded_bits.end() || it->second.driven)
+					continue;
+				orig.append(bit);
+				enc.is_0.append(it->second.is_0);
+				enc.is_1.append(it->second.is_1);
+				enc.is_x.append(it->second.is_x);
+				it->second.driven = true;
+			}
+
+			module->addBweqx(NEW_ID, orig, Const(State::S0, GetSize(orig)), enc.is_0);
+			module->addBweqx(NEW_ID, orig, Const(State::S1, GetSize(orig)), enc.is_1);
+			module->addBweqx(NEW_ID, orig, Const(State::Sx, GetSize(orig)), enc.is_x);
+		}
+	}
+};
+
+struct XpropPass : public Pass {
+	XpropPass() : Pass("xprop", "formal x propagation") {}
+	void help() override
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    xprop [options] [selection]\n");
+		log("\n");
+		log("This pass transforms the circuit into an equivalent circuit that explicitly\n");
+		log("encodes the propagation of x values using purely 2-valued logic. On the\n");
+		log("interface between xprop-transformed and non-transformed parts of the design,\n");
+		log("appropriate conversions are inserted automatically.\n");
+		log("\n");
+		log("    -split-inputs\n");
+		log("    -split-outputs\n");
+		log("    -split-ports\n");
+		log("        Replace each input/output/port with two new ports, one carrying the\n");
+		log("        defined values (named <portname>_d) and one carrying the mask of which\n");
+		log("        bits are x (named <portname>_x). When a bit in the <portname>_x is set\n");
+		log("        the corresponding bit in <portname>_d is ignored for inputs and\n");
+		log("        guaranteed to be 0 for outputs.\n");
+		log("\n");
+		log("    -assume-encoding\n");
+		log("        Add encoding invariants as assumptions. This can speed up formal\n");
+		log("        verification tasks.\n");
+		log("\n");
+		log("    -assert-encoding\n");
+		log("        Add encoding invariants as assertions. Used for testing the xprop\n");
+		log("        pass itself.\n");
+		log("\n");
+		log("    -assume-def-inputs\n");
+		log("        Assume all inputs are fully defined. This adds corresponding\n");
+		log("        assumptions to the design and uses these assumptions to optimize the\n");
+		log("        xprop encoding.\n");
+		log("\n");
+		log("    -required\n");
+		log("        Produce a runtime error if any encountered cell could not be encoded.\n");
+		log("\n");
+		log("    -formal\n");
+		log("        Produce a runtime error if any encoded cell uses a signal that is\n");
+		log("		 neither known to be non-x nor driven by another encoded cell.\n");
+		log("\n");
+		log("    -debug-asserts\n");
+		log("        Add assertions checking that the encoding used by this pass never\n");
+		log("        produces x values within the encoded signals.\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		XpropOptions options;
+
+		log_header(design, "Executing XPROP pass.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-split-ports") {
+				options.split_inputs = true;
+				options.split_outputs = true;
+				continue;
+			}
+			if (args[argidx] == "-split-inputs") {
+				options.split_inputs = true;
+				continue;
+			}
+			if (args[argidx] == "-split-outputs") {
+				options.split_outputs = true;
+				continue;
+			}
+			if (args[argidx] == "-assume-encoding") {
+				options.assume_encoding = true;
+				continue;
+			}
+			if (args[argidx] == "-assert-encoding") {
+				options.assert_encoding = true;
+				continue;
+			}
+			if (args[argidx] == "-assume-def-inputs") {
+				options.assume_def_inputs = true;
+				continue;
+			}
+			if (args[argidx] == "-required") {
+				options.required = true; // TODO check more
+				continue;
+			}
+			if (args[argidx] == "-formal") {
+				options.formal = true;
+				options.required = true;
+				continue;
+			}
+			if (args[argidx] == "-debug-asserts") { // TODO documented
+				options.debug_asserts = true;
+				options.assert_encoding = true;
+				continue;
+			}
+			break;
+		}
+
+		if (options.assert_encoding && options.assume_encoding)
+			log_cmd_error("The options -assert-encoding and -assume-encoding are exclusive.\n");
+
+		extra_args(args, argidx, design);
+
+		log_push();
+		Pass::call(design, "bmuxmap");
+		Pass::call(design, "demuxmap");
+		log_pop();
+
+		for (auto module : design->selected_modules()) {
+			if (options.assume_def_inputs) {
+				for (auto port : module->ports) {
+					auto wire = module->wire(port);
+					if (!module->design->selected(module, wire))
+						continue;
+
+					if (wire->port_input) {
+						module->addAssume(NEW_ID, module->Not(NEW_ID, module->ReduceOr(NEW_ID, module->Bweqx(NEW_ID, wire, Const(State::Sx, GetSize(wire))))), State::S1);
+					}
+				}
+			}
+
+			XpropWorker worker(module, options);
+			log_debug("Marking all x-bits.\n");
+			worker.mark_all_maybe_x();
+			log_debug("Repalcing cells.\n");
+			worker.process_cells();
+			log_debug("Splitting ports.\n");
+			worker.split_ports();
+			log_debug("Encode remaining signals.\n");
+			worker.encode_remaining();
+
+		}
+	}
+} XpropPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/tests/xprop/.gitignore b/tests/xprop/.gitignore
new file mode 100644
index 000000000..ff0b65b54
--- /dev/null
+++ b/tests/xprop/.gitignore
@@ -0,0 +1,2 @@
+/xprop_*
+/run-test.mk
diff --git a/tests/xprop/generate.py b/tests/xprop/generate.py
new file mode 100644
index 000000000..eef8dc36e
--- /dev/null
+++ b/tests/xprop/generate.py
@@ -0,0 +1,278 @@
+import os
+import re
+import sys
+import random
+import argparse
+
+parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed', type=int, help='seed for PRNG')
+parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test')
+parser.add_argument('-f', '--filter', default='', help='regular expression to filter tests to generate')
+args = parser.parse_args()
+
+if args.seed is None:
+    args.seed = random.randrange(1 << 32)
+
+print(f"xprop PRNG seed: {args.seed}")
+
+makefile = open("run-test.mk", "w")
+
+def add_test(name, src, seq=False):
+    if not re.search(args.filter, name):
+        return
+    workdir = f"xprop_{name}"
+
+    os.makedirs(workdir, exist_ok=True)
+    with open(f"{workdir}/uut.v", "w") as uut:
+        print(src, file=uut)
+    print(f"all: {workdir}", file=makefile)
+    print(f".PHONY: {workdir}", file=makefile)
+    print(f"{workdir}:", file=makefile)
+    seq_arg = " -s" if seq else ""
+    print(
+        f"\t@cd {workdir} && python3 -u ../test.py -S {args.seed} -c {args.count}{seq_arg} > test.log 2>&1 || echo {workdir}: failed > status\n"
+        f"\t@cat {workdir}/status\n"
+        # f"\t@grep '^.*: ok' {workdir}/status\n"
+        ,
+        file=makefile,
+    )
+
+def cell_test(name, cell, inputs, outputs, params, initial={}, defclock=False, seq=False):
+    ports = []
+    port_conns = []
+    for inport, width in inputs.items():
+        ports.append(f"input [{width-1}:0] {inport}")
+        if defclock and inport in ["C", "CLK"]:
+            port_conns.append(f".{inport}({inport} !== 0)")
+        else:
+            port_conns.append(f".{inport}({inport})")
+    for outport, width in outputs.items():
+        reg = " reg" if outport in initial else ""
+        ports.append(f"output{reg} [{width-1}:0] {outport}")
+        port_conns.append(f".{outport}({outport})")
+    param_defs = []
+    for param, value in params.items():
+        param_defs.append(f".{param}({value})")
+    initials = []
+    # for port, value in initial.items():
+    #     initials.append(f"initial {port} = {value};\n")
+    add_test(name,
+        f"module uut({', '.join(ports)});\n"
+        f"\\${cell} #({', '.join(param_defs)}) cell ({', '.join(port_conns)});\n"
+        f"{''.join(initials)}"
+        "endmodule",
+        seq=seq,
+    )
+
+def unary_test(cell, width, signed, out_width):
+    add_test(
+        f"{cell}_{width}{'us'[signed]}_{out_width}",
+        f"module uut(input [{width-1}:0] A, output [{out_width}-1:0] Y);\n"
+        f"\\${cell} #(.A_WIDTH({width}), .A_SIGNED({int(signed)}), .Y_WIDTH({out_width}))"
+        " cell (.A(A), .Y(Y));\n"
+        "endmodule",
+    )
+
+def binary_test(cell, a_width, b_width, signed, out_width):
+    add_test(
+        f"{cell}_{a_width}{'us'[signed]}{b_width}_{out_width}",
+        f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n"
+        f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(signed)}), .Y_WIDTH({out_width}))"
+        " cell (.A(A), .B(B), .Y(Y));\n"
+        "endmodule",
+    )
+
+def shift_test(cell, a_width, b_width, a_signed, b_signed, out_width):
+    add_test(
+        f"{cell}_{a_width}{'us'[a_signed]}{b_width}{'us'[b_signed]}_{out_width}",
+        f"module uut(input [{a_width-1}:0] A, input [{b_width-1}:0] B, output [{out_width}-1:0] Y);\n"
+        f"\\${cell} #(.A_WIDTH({a_width}), .A_SIGNED({int(a_signed)}), .B_WIDTH({b_width}), .B_SIGNED({int(b_signed)}), .Y_WIDTH({out_width}))"
+        " cell (.A(A), .B(B), .Y(Y));\n"
+        "endmodule",
+    )
+
+def mux_test(width):
+    cell_test(f"mux_{width}", 'mux', {"A": width, "B": width, "S": 1}, {"Y": width}, {"WIDTH": width})
+
+def bmux_test(width, s_width):
+    cell_test(f"bmux_{width}_{s_width}", 'bmux', {"A": width << s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def demux_test(width, s_width):
+    cell_test(f"demux_{width}_{s_width}", 'demux', {"A": width, "S": s_width}, {"Y": width << s_width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def pmux_test(width, s_width):
+    cell_test(f"pmux_{width}_{s_width}", 'pmux', {"A": width, "B": width * s_width, "S": s_width}, {"Y": width}, {"WIDTH": width, "S_WIDTH": s_width})
+
+def bwmux_test(width):
+    cell_test(f"bwmux_{width}", 'bwmux', {"A": width, "B": width, "S": width}, {"Y": width}, {"WIDTH": width})
+
+def bweqx_test(width):
+    cell_test(f"bweqx_{width}", 'bweqx', {"A": width, "B": width}, {"Y": width}, {"WIDTH": width})
+
+def ff_test(width):
+    cell_test(f"ff_{width}", 'ff', {"D": width}, {"Q": width}, {"WIDTH": width}, seq=True)
+
+def dff_test(width, pol, defclock):
+    cell_test(f"dff_{width}{'np'[pol]}{'xd'[defclock]}", 'dff', {"CLK": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol)}, defclock=defclock, seq=True)
+
+def dffe_test(width, pol, enpol, defclock):
+    cell_test(f"dffe_{width}{'np'[pol]}{'np'[enpol]}{'xd'[defclock]}", 'dffe', {"CLK": 1, "EN": 1, "D": width}, {"Q": width}, {"WIDTH": width, "CLK_POLARITY": int(pol), "EN_POLARITY": int(enpol)}, defclock=defclock, seq=True)
+
+
+print(".PHONY: all", file=makefile)
+print("all:\n\t@echo done\n", file=makefile)
+
+for cell in ["not", "pos", "neg"]:
+    unary_test(cell, 1, False, 1)
+    unary_test(cell, 3, False, 3)
+    unary_test(cell, 3, True, 3)
+    unary_test(cell, 3, True, 1)
+    unary_test(cell, 3, False, 5)
+    unary_test(cell, 3, True, 5)
+
+for cell in ["and", "or", "xor", "xnor"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 1, 1, True, 2)
+    binary_test(cell, 2, 2, False, 2)
+    binary_test(cell, 2, 2, False, 1)
+    binary_test(cell, 2, 1, False, 2)
+    binary_test(cell, 2, 1, False, 1)
+
+# [, "pow"] are not implemented yet
+for cell in ["add", "sub", "mul", "div", "mod", "divfloor", "modfloor"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 1, 1, False, 2)
+    binary_test(cell, 3, 3, False, 1)
+    binary_test(cell, 3, 3, False, 3)
+    binary_test(cell, 3, 3, False, 6)
+    binary_test(cell, 3, 3, True, 1)
+    binary_test(cell, 3, 3, True, 3)
+    binary_test(cell, 3, 3, True, 6)
+    binary_test(cell, 5, 3, False, 3)
+    binary_test(cell, 5, 3, True, 3)
+
+for cell in ["lt", "le", "eq", "ne", "eqx", "nex", "ge", "gt"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 1, 1, False, 2)
+    binary_test(cell, 3, 3, False, 1)
+    binary_test(cell, 3, 3, False, 2)
+    binary_test(cell, 3, 3, True, 1)
+    binary_test(cell, 3, 3, True, 2)
+    binary_test(cell, 5, 3, False, 1)
+    binary_test(cell, 5, 3, True, 1)
+    binary_test(cell, 5, 3, False, 2)
+    binary_test(cell, 5, 3, True, 2)
+
+for cell in ["reduce_and", "reduce_or", "reduce_xor", "reduce_xnor"]:
+    unary_test(cell, 1, False, 1)
+    unary_test(cell, 3, False, 1)
+    unary_test(cell, 3, True, 1)
+    unary_test(cell, 3, False, 3)
+    unary_test(cell, 3, True, 3)
+
+for cell in ["reduce_bool", "logic_not"]:
+    unary_test(cell, 1, False, 1)
+    unary_test(cell, 3, False, 3)
+    unary_test(cell, 3, True, 3)
+    unary_test(cell, 3, True, 1)
+
+for cell in ["logic_and", "logic_or"]:
+    binary_test(cell, 1, 1, False, 1)
+    binary_test(cell, 3, 3, False, 3)
+    binary_test(cell, 3, 3, True, 3)
+    binary_test(cell, 3, 3, True, 1)
+
+for cell in ["shl", "shr", "sshl", "sshr", "shift"]:
+    shift_test(cell, 2, 1, False, False, 2)
+    shift_test(cell, 2, 1, True, False, 2)
+    shift_test(cell, 2, 1, False, False, 4)
+    shift_test(cell, 2, 1, True, False, 4)
+    shift_test(cell, 4, 2, False, False, 4)
+    shift_test(cell, 4, 2, True, False, 4)
+    shift_test(cell, 4, 2, False, False, 8)
+    shift_test(cell, 4, 2, True, False, 8)
+    shift_test(cell, 4, 3, False, False, 3)
+    shift_test(cell, 4, 3, True, False, 3)
+
+for cell in ["shift"]:
+    shift_test(cell, 2, 1, False, True, 2)
+    shift_test(cell, 2, 1, True, True, 2)
+    shift_test(cell, 2, 1, False, True, 4)
+    shift_test(cell, 2, 1, True, True, 4)
+    shift_test(cell, 4, 2, False, True, 4)
+    shift_test(cell, 4, 2, True, True, 4)
+    shift_test(cell, 4, 2, False, True, 8)
+    shift_test(cell, 4, 2, True, True, 8)
+    shift_test(cell, 4, 3, False, True, 3)
+    shift_test(cell, 4, 3, True, True, 3)
+
+for cell in ["shiftx"]:
+    shift_test(cell, 2, 1, False, True, 2)
+    shift_test(cell, 2, 1, False, True, 4)
+    shift_test(cell, 4, 2, False, True, 4)
+    shift_test(cell, 4, 2, False, True, 8)
+    shift_test(cell, 4, 3, False, True, 3)
+
+mux_test(1)
+mux_test(3)
+
+bmux_test(1, 2)
+bmux_test(2, 2)
+bmux_test(3, 1)
+
+demux_test(1, 2)
+demux_test(2, 2)
+demux_test(3, 1)
+
+pmux_test(1, 4)
+pmux_test(2, 2)
+pmux_test(3, 1)
+pmux_test(4, 4)
+
+bwmux_test(1)
+bwmux_test(3)
+
+bweqx_test(1)
+bweqx_test(3)
+
+ff_test(1)
+ff_test(3)
+
+dff_test(1, True, True)
+dff_test(1, False, True)
+dff_test(3, True, True)
+dff_test(3, False, True)
+
+# dff_test(1, True, False)  # TODO support x clocks
+# dff_test(1, False, False)  # TODO support x clocks
+# dff_test(3, True, False)  # TODO support x clocks
+# dff_test(3, False, False)  # TODO support x clocks
+
+dffe_test(1, True, False, True)
+dffe_test(1, False, False, True)
+dffe_test(3, True, False, True)
+dffe_test(3, False, False, True)
+dffe_test(1, True, True, True)
+dffe_test(1, False, True, True)
+dffe_test(3, True, True, True)
+dffe_test(3, False, True, True)
+
+
+
+# TODO "shift", "shiftx"
+
+# TODO "fa", "lcu", "alu", "macc", "lut", "sop"
+
+# TODO "slice", "concat"
+
+# TODO "tribuf", "specify2", "specify3", "specrule"
+
+# TODO "assert", "assume", "live", "fair", "cover", "initstate", "anyconst", "anyseq", "anyinit", "allconst", "allseq", "equiv",
+
+# TODO "bweqx", "bwmux"
+
+# TODO "sr", "ff", "dff", "dffe", "dffsr", "sffsre", "adff", "aldff", "sdff", "adffe", "aldffe", "sdffe", "sdffce", "dlatch", "adlatch", "dlatchsr"
+
+# TODO "fsm"
+
+# TODO "memrd", "memrd_v2", "memwr", "memwr_v2", "meminit", "meminit_v2", "mem", "mem_v2"
diff --git a/tests/xprop/run-test.sh b/tests/xprop/run-test.sh
new file mode 100755
index 000000000..1fc7e10b6
--- /dev/null
+++ b/tests/xprop/run-test.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+set -e
+
+python3 generate.py $@
+make -f run-test.mk
diff --git a/tests/xprop/test.py b/tests/xprop/test.py
new file mode 100644
index 000000000..84ad0a1f4
--- /dev/null
+++ b/tests/xprop/test.py
@@ -0,0 +1,516 @@
+import os
+import re
+import subprocess
+import itertools
+import random
+import argparse
+from pathlib import Path
+
+parser = argparse.ArgumentParser(formatter_class=argparse.ArgumentDefaultsHelpFormatter)
+parser.add_argument('-S', '--seed', type=int, help='seed for PRNG')
+parser.add_argument('-c', '--count', type=int, default=32, help='number of random patterns to test')
+parser.add_argument('-s', '--seq', action='store_true', help='run a sequential test')
+parser.add_argument('steps', nargs='*', help='steps to run')
+args = parser.parse_args()
+
+if args.seed is None:
+    args.seed = random.randrange(1 << 32)
+
+print(f"PRNG seed: {args.seed}")
+random.seed(args.seed)
+
+steps = args.steps
+
+all_outputs = [
+    "sim",
+    "sim_xprop",
+    "vsim_expr",
+    "vsim_expr_xprop",
+    "vsim_noexpr",
+    "vsim_noexpr_xprop",
+    "sat",
+    "sat_xprop",
+]
+
+if not args.seq:
+    all_outputs += ["opt_expr", "opt_expr_xprop"]
+
+if not steps:
+    steps = ["clean", "prepare", "verify", *all_outputs, "compare"]
+
+if "clean" in steps:
+    for output in all_outputs:
+        try:
+            os.unlink(f"{output}.out")
+        except FileNotFoundError:
+            pass
+
+
+def yosys(command):
+    subprocess.check_call(["yosys", "-Qp", command])
+
+def remove(file):
+    try:
+        os.unlink(file)
+    except FileNotFoundError:
+        pass
+
+
+def vcdextract(signals, on_change, file, output, limit=None):
+    scope = []
+    ids = {}
+    prefix = []
+
+    for line in file:
+        line = prefix + line.split()
+        if line[-1] != "$end":
+            prefix = line
+            continue
+        prefix = []
+
+        if not line:
+            continue
+        if line[0] == "$scope":
+            scope.append(line[2].lstrip("\\"))
+        elif line[0] == "$upscope":
+            scope.pop()
+        elif line[0] == "$var":
+            ids[".".join(scope + [line[4].lstrip("\\")])] = line[3]
+        elif line[0] == "$enddefinitions":
+            break
+        elif line[0] in ["$version", "$date", "$comment"]:
+            continue
+        else:
+            raise RuntimeError(f"unexpected input in vcd {line}")
+
+    dump_pos = {}
+
+    for i, sig in enumerate(signals + on_change):
+        dump_pos[ids[sig]] = i
+
+    values = [None] * len(signals + on_change)
+
+    last_values = []
+
+    counter = 0
+
+    for line in file:
+        if line.startswith("#"):
+            if None in values:
+                continue
+
+            if values != last_values:
+                last_values = list(values)
+                if limit is None or counter < limit:
+                    print(*values[:len(signals)], file=output)
+                    counter += 1
+            continue
+
+        if line.startswith("b"):
+            value, id = line[1:].split()
+        else:
+            value, id = line[:1], line[1:]
+
+        pos = dump_pos.get(id)
+        if pos is None:
+            continue
+
+        values[pos] = value
+
+    if values != last_values:
+        if limit is None or counter < limit:
+            print(*values[:len(signals)], file=output)
+
+
+share = Path(__file__).parent / ".." / ".." / "share"
+
+simlibs = [str(share / "simlib.v"), str(share / "simcells.v")]
+
+if "prepare" in steps:
+    yosys(
+        """
+            read_verilog -icells uut.v
+            hierarchy -top uut; proc -noopt
+            write_rtlil uut.il
+            dump -o ports.list uut/x:*
+        """
+    )
+
+inputs = []
+outputs = []
+
+with open("ports.list") as ports_file:
+    for line in ports_file:
+        line = line.split()
+        if not line or line[0] != "wire":
+            continue
+        line = line[1:]
+        width = 1
+        if line[0] == "width":
+            width = int(line[1])
+            line = line[2:]
+        direction, seq, name = line
+        assert name.startswith("\\")
+        name = name[1:]
+        seq = int(seq)
+
+        if direction == "input":
+            inputs.append((seq, name, width))
+        else:
+            outputs.append((seq, name, width))
+
+inputs.sort()
+outputs.sort()
+
+input_width = sum(width for seq, name, width in inputs)
+output_width = sum(width for seq, name, width in outputs)
+
+if "prepare" in steps:
+    if args.seq:
+        patterns = [''.join(random.choices('01x', k=input_width)) for i in range(args.count)]
+    else:
+        if 3**input_width <= args.count * 2:
+            patterns = ["".join(bits) for bits in itertools.product(*["01x"] * input_width)]
+        else:
+            patterns = set()
+
+            for bit in '01x':
+                patterns.add(bit * input_width)
+
+            for bits in itertools.combinations('01x', 2):
+                for bit1, bit2 in itertools.permutations(bits):
+                    for i in range(input_width):
+                        pattern = [bit1] * input_width
+                        pattern[i] = bit2
+                        patterns.add(''.join(pattern))
+
+                    for i, j in itertools.combinations(range(input_width), 2):
+                        pattern = [bit1] * input_width
+                        pattern[i] = bit2
+                        pattern[j] = bit2
+                        patterns.add(''.join(pattern))
+
+            for bit1, bit2, bit3 in itertools.permutations('01x'):
+                for i, j in itertools.combinations(range(input_width), 2):
+                    pattern = [bit1] * input_width
+                    pattern[i] = bit2
+                    pattern[j] = bit3
+                    patterns.add(''.join(pattern))
+
+            if len(patterns) > args.count // 2:
+                patterns = sorted(patterns)
+                random.shuffle(patterns)
+                patterns = set(patterns[:args.count // 2])
+
+            while len(patterns) < args.count:
+                pattern = ''.join(random.choices('01x', k=input_width))
+                patterns.add(pattern)
+
+        patterns = sorted(patterns)
+    with open("patterns.list", "w") as f:
+        for pattern in patterns:
+            print(pattern, file=f)
+else:
+    with open("patterns.list") as f:
+        patterns = [pattern.strip() for pattern in f]
+
+
+if "prepare" in steps:
+    with open("wrapper.v", "w") as wrapper_file:
+        print(
+            "module wrapper("
+            f"input [{input_width-1}:0] A, "
+            f"output [{output_width-1}:0] Y);",
+            file=wrapper_file,
+        )
+
+        connections = []
+        pos = 0
+        for seq, name, width in inputs:
+            connections.append(f".{name}(A[{pos+width-1}:{pos}])")
+            pos += width
+        pos = 0
+        for seq, name, width in outputs:
+            connections.append(f".{name}(Y[{pos+width-1}:{pos}])")
+            pos += width
+
+        print(f"uut uut({', '.join(connections)});", file=wrapper_file)
+        print("endmodule", file=wrapper_file)
+
+    yosys(
+        """
+            read_rtlil uut.il
+            read_verilog wrapper.v
+            hierarchy -top wrapper; proc -noopt
+            flatten; clean;
+            rename wrapper uut
+            write_rtlil wrapped.il
+        """
+    )
+
+    try:
+        yosys(
+            """
+                read_rtlil wrapped.il
+                dffunmap
+                xprop -required
+                check -assert
+                write_rtlil wrapped_xprop.il
+            """
+        )
+    except subprocess.CalledProcessError:
+        remove("wrapped_xprop.il")
+
+    with open("verilog_sim_tb.v", "w") as tb_file:
+        print("module top();", file=tb_file)
+        print(f"reg gclk;", file=tb_file)
+        print(f"reg [{input_width-1}:0] A;", file=tb_file)
+        print(f"wire [{output_width-1}:0] Y;", file=tb_file)
+        print(f"uut uut(.A(A), .Y(Y));", file=tb_file)
+        print("initial begin", file=tb_file)
+
+        for pattern in patterns:
+            print(
+                f'    gclk = 1; #0; A[0] = 1\'b{pattern[-1]}; #0; A = {input_width}\'b{pattern}; #5; gclk = 0; $display("%b %b", A, Y); #5',
+                file=tb_file,
+            )
+
+        print("    $finish;", file=tb_file)
+        print("end", file=tb_file)
+        print("endmodule", file=tb_file)
+
+    with open("synth_tb.v", "w") as tb_file:
+        print("module top(input clk);", file=tb_file)
+        print(f"reg [{len(patterns).bit_length() - 1}:0] counter = 0;", file=tb_file)
+        print(f"reg [{input_width-1}:0] A;", file=tb_file)
+        print(f"(* gclk *) reg gclk;", file=tb_file)
+        print(f"wire [{output_width-1}:0] Y;", file=tb_file)
+        print(f"uut uut(.A(A), .Y(Y));", file=tb_file)
+        print(f"always @(posedge gclk) counter <= counter + 1;", file=tb_file)
+        print(f"always @* case (counter)", file=tb_file)
+        for i, pattern in enumerate(patterns):
+            print(f"    {i:7} : A = {input_width}'b{pattern};", file=tb_file)
+        print(f"    default : A = {input_width}'b{'x' * input_width};", file=tb_file)
+        print(f"endcase", file=tb_file)
+        print("endmodule", file=tb_file)
+
+    with open("const_tb.v", "w") as tb_file:
+        print("module top();", file=tb_file)
+        for i, pattern in enumerate(patterns):
+            print(
+                f"(* keep *) wire [{output_width-1}:0] Y_{i}; "
+                f"uut uut_{i}(.A({input_width}'b{pattern}), .Y(Y_{i}));",
+                file=tb_file,
+            )
+        print("endmodule", file=tb_file)
+
+if "verify" in steps:
+    try:
+        seq_args = " -tempinduct -set-init-undef" if args.seq else ""
+        yosys(
+            f"""
+                read_rtlil wrapped.il
+                copy uut gold
+                rename uut gate
+                design -push-copy
+                dffunmap
+                xprop -formal -split-inputs -required -debug-asserts gate
+                clk2fflogic
+                sat{seq_args} -enable_undef -set-def-inputs -prove-asserts -verify -show-all gate
+                design -pop
+
+                dffunmap
+                xprop -required -assume-encoding gate
+                miter -equiv -make_assert -flatten gold gate miter
+                clk2fflogic
+                sat{seq_args} -enable_undef -set-assumes -prove-asserts -verify -show-all miter
+            """
+        )
+        with open("verified", "w") as f:
+            pass
+    except subprocess.CalledProcessError:
+        remove("verified")
+
+
+for mode in ["", "_xprop"]:
+    if not Path(f"wrapped{mode}.il").is_file():
+        for expr in [f"expr{mode}", f"noexpr{mode}"]:
+            remove(f"vsim_{expr}.out")
+        continue
+
+    if "prepare" in steps:
+        yosys(
+            f"""
+                read_rtlil wrapped{mode}.il
+                chformal -remove
+                dffunmap
+                write_verilog -noparallelcase vsim_expr{mode}.v
+                write_verilog -noexpr vsim_noexpr{mode}.v
+            """
+        )
+
+    for expr in [f"expr{mode}", f"noexpr{mode}"]:
+        if f"vsim_{expr}" in steps:
+            subprocess.check_call(
+                [
+                    "iverilog",
+                    "-DSIMLIB_FF",
+                    "-DSIMLIB_GLOBAL_CLOCK=top.gclk",
+                    f"-DDUMPFILE=\"vsim_{expr}.vcd\"",
+                    "verilog_sim_tb.v",
+                    f"vsim_{expr}.v",
+                    *simlibs,
+                    "-o",
+                    f"vsim_{expr}",
+                ]
+            )
+            with open(f"vsim_{expr}.out", "w") as f:
+                subprocess.check_call([f"./vsim_{expr}"], stdout=f)
+
+for mode in ["", "_xprop"]:
+    if f"sim{mode}" not in steps:
+        continue
+    if not Path(f"wrapped{mode}.il").is_file():
+        remove(f"sim{mode}.out")
+        continue
+    yosys(
+        f"""
+            read_verilog synth_tb.v
+            read_rtlil wrapped{mode}.il
+            hierarchy -top top; proc -noopt
+            dffunmap
+            sim -clock clk -n {len(patterns) // 2} -vcd sim{mode}.vcd top
+        """
+    )
+
+    with open(f"sim{mode}.vcd") as fin, open(f"sim{mode}.out", "w") as fout:
+        vcdextract(["top.A", "top.Y"], ["top.counter"], fin, fout, len(patterns))
+
+for mode in ["", "_xprop"]:
+    if f"sat{mode}" not in steps:
+        continue
+    if not Path(f"wrapped{mode}.il").is_file():
+        remove(f"sat{mode}.out")
+        continue
+    chunk_size = len(patterns) if args.seq else 32
+    last_progress = 0
+    with open(f"sat{mode}.ys", "w") as ys:
+        for chunk_start in range(0, len(patterns), chunk_size):
+            chunk = patterns[chunk_start : chunk_start + chunk_size]
+            progress = (10 * chunk_start) // len(patterns)
+            if progress > last_progress:
+                print(f"log sat {progress}0%", file=ys)
+                last_progress = progress
+
+            append = "-a" if chunk_start else "-o"
+            print(
+                end=f"tee -q {append} sat{mode}.log sat -set-init-undef -seq {len(chunk)}"
+                " -show A -show Y -dump_vcd sat.vcd -enable_undef",
+                file=ys,
+            )
+            for i, pattern in enumerate(chunk, 1):
+                ad = pattern.replace("x", "0")
+                ax = pattern.replace("1", "0").replace("x", "1")
+                print(end=f" -set-at {i} A {input_width}'b{pattern}", file=ys)
+            print(file=ys)
+        print(f"log sat 100%", file=ys)
+
+    try:
+        yosys(
+            f"""
+                read_rtlil wrapped{mode}.il
+                clk2fflogic
+                script sat{mode}.ys
+            """
+        )
+    except subprocess.CalledProcessError:
+        remove(f"sat{mode}.out")
+    else:
+        sig_re = re.compile(
+            r" *[0-9]+ +\\([AY]) +(?:--|[0-9]+) +(?:--|[0-9a-f]+) +([01x]+)"
+        )
+        current_input = None
+        with open(f"sat{mode}.log") as logfile, open(f"sat{mode}.out", "w") as outfile:
+            for line in logfile:
+                match = sig_re.match(line)
+                if match:
+                    if match[1] == "A":
+                        current_input = match[2]
+                    else:
+                        print(current_input, match[2], file=outfile)
+
+for mode in ["", "_xprop"]:
+    if f"opt_expr{mode}" not in steps:
+        continue
+    if not Path(f"wrapped{mode}.il").is_file():
+        remove(f"opt_expr{mode}.out")
+        continue
+    yosys(
+        f"""
+            read_verilog const_tb.v
+            read_rtlil wrapped{mode}.il
+            hierarchy -top top; proc -noopt
+            flatten
+            opt_expr -keepdc; clean
+            dump -o opt_expr{mode}.list */\Y_*
+        """
+    )
+
+    values = []
+
+    connect_re = re.compile(r" *connect +\\Y_([0-9]+) +[0-9]+'([01x]+)$")
+    with open(f"opt_expr{mode}.list") as connections:
+        for line in connections:
+            match = connect_re.match(line)
+            if match:
+                seq = int(match[1])
+                data = match[2]
+                if len(data) < output_width:
+                    data = data * output_width
+                values.append((seq, data))
+
+        values.sort()
+
+        with open(f"opt_expr{mode}.out", "w") as outfile:
+            for seq, data in values:
+                print(patterns[seq], data, file=outfile)
+
+
+if "compare" in steps:
+    groups = {}
+    missing = []
+
+    for output in all_outputs:
+        try:
+            with open(f"{output}.out") as f:
+                groups.setdefault(f.read(), []).append(output)
+        except FileNotFoundError:
+            missing.append(output)
+
+    verified = Path(f"verified").is_file()
+
+    with open("status", "w") as status:
+        name = Path('.').absolute().name
+
+        status_list = []
+
+        if len(groups) > 1:
+            status_list.append("mismatch")
+        if not verified:
+            status_list.append("failed-verify")
+        if missing:
+            status_list.append("missing")
+        if not status_list:
+            status_list.append("ok")
+        print(f"{name}: {', '.join(status_list)}", file=status)
+
+        if len(groups) > 1:
+            print("output differences:", file=status)
+            for group in groups.values():
+                print("  -", *group, file=status)
+        if missing:
+            print("missing:", file=status)
+            print("  -", *missing, file=status)
+
+    with open("status") as status:
+        print(end=status.read())