Merge pull request #3537 from jix/xprop

New xprop pass

Makefile

@@ -874,6 +874,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 ""

backends/btor/btor.cc

@@ -1417,6 +1417,7 @@ struct BtorBackend : public Backend {
 		log_push();
 		Pass::call(design, "bmuxmap");
 		Pass::call(design, "demuxmap");
+		Pass::call(design, "bwmuxmap");
 		log_pop();
 
 		size_t argidx;

backends/firrtl/firrtl.cc

@@ -1215,6 +1215,7 @@ struct FirrtlBackend : public Backend {
 		Pass::call(design, "pmuxtree");
 		Pass::call(design, "bmuxmap");
 		Pass::call(design, "demuxmap");
+		Pass::call(design, "bwmuxmap");
 
 		namecache.clear();
 		autoid_counter = 0;

backends/smt2/smt2.cc

@@ -1744,6 +1744,7 @@ struct Smt2Backend : public Backend {
 		log_push();
 		Pass::call(design, "bmuxmap");
 		Pass::call(design, "demuxmap");
+		Pass::call(design, "bwmuxmap");
 		log_pop();
 
 		size_t argidx;

backends/smv/smv.cc

@@ -744,6 +744,7 @@ struct SmvBackend : public Backend {
 		log_push();
 		Pass::call(design, "bmuxmap");
 		Pass::call(design, "demuxmap");
+		Pass::call(design, "bwmuxmap");
 		log_pop();
 
 		size_t argidx;

backends/verilog/verilog_backend.cc

@@ -35,7 +35,7 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase;
 int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
 std::map<RTLIL::IdString, int> auto_name_map;
 std::set<RTLIL::IdString> reg_wires;
@@ -1209,7 +1209,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 	if (cell->type == ID($modfloor))
 	{
 		// wire truncated = $signed(A) % $signed(B);
-		// assign Y = (A[-1] == B[-1]) || truncated == 0 ? truncated : $signed(B) + $signed(truncated);
+		// assign Y = (A[-1] == B[-1]) || truncated == 0 ? $signed(truncated) : $signed(B) + $signed(truncated);
 
 		if (cell->getParam(ID::A_SIGNED).as_bool() && cell->getParam(ID::B_SIGNED).as_bool()) {
 			SigSpec sig_a = cell->getPort(ID::A);
@@ -1229,7 +1229,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 			dump_sigspec(f, sig_a.extract(sig_a.size()-1));
 			f << stringf(" == ");
 			dump_sigspec(f, sig_b.extract(sig_b.size()-1));
-			f << stringf(") || %s == 0 ? %s : ", temp_id.c_str(), temp_id.c_str());
+			f << stringf(") || %s == 0 ? $signed(%s) : ", temp_id.c_str(), temp_id.c_str());
 			dump_cell_expr_port(f, cell, "B", true);
 			f << stringf(" + $signed(%s);\n", temp_id.c_str());
 			return true;
@@ -1314,24 +1314,38 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		f << stringf("%s" "  input [%d:0] s;\n", indent.c_str(), s_width-1);
 
 		dump_attributes(f, indent + "  ", cell->attributes);
-		if (!noattr)
+		if (noparallelcase)
-			f << stringf("%s" "  (* parallel_case *)\n", indent.c_str());
+			f << stringf("%s" "  case (s)\n", indent.c_str());
-		f << stringf("%s" "  casez (s)", indent.c_str());
+		else {
-		f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+			if (!noattr)
+				f << stringf("%s" "  (* parallel_case *)\n", indent.c_str());
+			f << stringf("%s" "  casez (s)", indent.c_str());
+			f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+		}
 
 		for (int i = 0; i < s_width; i++)
 		{
 			f << stringf("%s" "    %d'b", indent.c_str(), s_width);
 
 			for (int j = s_width-1; j >= 0; j--)
-				f << stringf("%c", j == i ? '1' : '?');
+				f << stringf("%c", j == i ? '1' : noparallelcase ? '0' : '?');
 
 			f << stringf(":\n");
 			f << stringf("%s" "      %s = b[%d:%d];\n", indent.c_str(), func_name.c_str(), (i+1)*width-1, i*width);
 		}
 
-		f << stringf("%s" "    default:\n", indent.c_str());
+		if (noparallelcase) {
+			f << stringf("%s" "    %d'b", indent.c_str(), s_width);
+			for (int j = s_width-1; j >= 0; j--)
+				f << '0';
+			f << stringf(":\n");
+		} else
+			f << stringf("%s" "    default:\n", indent.c_str());
 		f << stringf("%s" "      %s = a;\n", indent.c_str(), func_name.c_str());
+		if (noparallelcase) {
+			f << stringf("%s" "    default:\n", indent.c_str());
+			f << stringf("%s" "      %s = %d'bx;\n", indent.c_str(), func_name.c_str(), width);
+		}
 
 		f << stringf("%s" "  endcase\n", indent.c_str());
 		f << stringf("%s" "endfunction\n", indent.c_str());
@@ -2136,6 +2150,11 @@ struct VerilogBackend : public Backend {
 		log("        without this option all internal cells are converted to Verilog\n");
 		log("        expressions.\n");
 		log("\n");
+		log("    -noparallelcase\n");
+		log("        With this option no parallel_case attributes are used. Instead, a case\n");
+		log("        statement that assigns don't-care values for priority dependent inputs\n");
+		log("        is generated.\n");
+		log("\n");
 		log("    -siminit\n");
 		log("        add initial statements with hierarchical refs to initialize FFs when\n");
 		log("        in -noexpr mode.\n");
@@ -2211,6 +2230,7 @@ struct VerilogBackend : public Backend {
 		decimal = false;
 		siminit = false;
 		simple_lhs = false;
+		noparallelcase = false;
 		auto_prefix = "";
 
 		bool blackboxes = false;
@@ -2246,6 +2266,10 @@ struct VerilogBackend : public Backend {
 				noexpr = true;
 				continue;
 			}
+			if (arg == "-noparallelcase") {
+				noparallelcase = true;
+				continue;
+			}
 			if (arg == "-nodec") {
 				nodec = true;
 				continue;
@@ -2302,8 +2326,11 @@ struct VerilogBackend : public Backend {
 		}
 
 		log_push();
-		Pass::call(design, "bmuxmap");
+		if (!noexpr) {
-		Pass::call(design, "demuxmap");
+			Pass::call(design, "bmuxmap");
+			Pass::call(design, "demuxmap");
+			Pass::call(design, "bwmuxmap");
+		}
 		Pass::call(design, "clean_zerowidth");
 		log_pop();
 

kernel/calc.cc

@@ -690,5 +690,28 @@ RTLIL::Const RTLIL::const_demux(const RTLIL::Const &arg1, const RTLIL::Const &ar
 	return res;
 }
 
+RTLIL::Const RTLIL::const_bweqx(const RTLIL::Const &arg1, const RTLIL::Const &arg2)
+{
+	log_assert(arg2.size() == arg1.size());
+	RTLIL::Const result(RTLIL::State::S0, arg1.size());
+	for (int i = 0; i < arg1.size(); i++)
+		result[i] = arg1[i] == arg2[i] ? State::S1 : State::S0;
+
+	return result;
+}
+
+RTLIL::Const RTLIL::const_bwmux(const RTLIL::Const &arg1, const RTLIL::Const &arg2, const RTLIL::Const &arg3)
+{
+	log_assert(arg2.size() == arg1.size());
+	log_assert(arg3.size() == arg1.size());
+	RTLIL::Const result(RTLIL::State::Sx, arg1.size());
+	for (int i = 0; i < arg1.size(); i++) {
+		if (arg3[i] != State::Sx || arg1[i] == arg2[i])
+			result[i] = arg3[i] == State::S1 ? arg2[i] : arg1[i];
+	}
+
+	return result;
+}
+
 YOSYS_NAMESPACE_END
 

kernel/celltypes.h

@@ -116,7 +116,8 @@ struct CellTypes
 			ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx),
 			ID($lt), ID($le), ID($eq), ID($ne), ID($eqx), ID($nex), ID($ge), ID($gt),
 			ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow),
-			ID($logic_and), ID($logic_or), ID($concat), ID($macc)
+			ID($logic_and), ID($logic_or), ID($concat), ID($macc),
+			ID($bweqx)
 		};
 
 		for (auto type : unary_ops)
@@ -125,7 +126,7 @@ struct CellTypes
 		for (auto type : binary_ops)
 			setup_type(type, {ID::A, ID::B}, {ID::Y}, true);
 
-		for (auto type : std::vector<RTLIL::IdString>({ID($mux), ID($pmux)}))
+		for (auto type : std::vector<RTLIL::IdString>({ID($mux), ID($pmux), ID($bwmux)}))
 			setup_type(type, {ID::A, ID::B, ID::S}, {ID::Y}, true);
 
 		for (auto type : std::vector<RTLIL::IdString>({ID($bmux), ID($demux)}))
@@ -430,6 +431,11 @@ struct CellTypes
 			return const_demux(arg1, arg2);
 		}
 
+		if (cell->type == ID($bweqx))
+		{
+			return const_bweqx(arg1, arg2);
+		}
+
 		if (cell->type == ID($lut))
 		{
 			int width = cell->parameters.at(ID::WIDTH).as_int();
@@ -490,6 +496,8 @@ struct CellTypes
 	{
 		if (cell->type.in(ID($mux), ID($_MUX_)))
 			return const_mux(arg1, arg2, arg3);
+		if (cell->type == ID($bwmux))
+			return const_bwmux(arg1, arg2, arg3);
 		if (cell->type == ID($pmux))
 			return const_pmux(arg1, arg2, arg3);
 		if (cell->type == ID($_AOI3_))

kernel/rtlil.cc

@@ -1613,6 +1613,23 @@ namespace {
 				return;
 			}
 
+			if (cell->type == ID($bweqx)) {
+				port(ID::A, param(ID::WIDTH));
+				port(ID::B, param(ID::WIDTH));
+				port(ID::Y, param(ID::WIDTH));
+				check_expected();
+				return;
+			}
+
+			if (cell->type == ID($bwmux)) {
+				port(ID::A, param(ID::WIDTH));
+				port(ID::B, param(ID::WIDTH));
+				port(ID::S, param(ID::WIDTH));
+				port(ID::Y, param(ID::WIDTH));
+				check_expected();
+				return;
+			}
+
 			if (cell->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) {
 				port(ID::A, 1);
 				port(ID::EN, 1);
@@ -2466,6 +2483,7 @@ DEF_METHOD(Sshr,     sig_a.size(), ID($sshr))
 		return sig_y;                                             \
 	}
 DEF_METHOD(Mux,      ID($mux),        0)
+DEF_METHOD(Bwmux,    ID($bwmux),      0)
 DEF_METHOD(Pmux,     ID($pmux),       1)
 #undef DEF_METHOD
 
@@ -2489,6 +2507,24 @@ DEF_METHOD(Bmux,     ID($bmux),       0)
 DEF_METHOD(Demux,    ID($demux),      1)
 #undef DEF_METHOD
 
+#define DEF_METHOD(_func, _type) \
+	RTLIL::Cell* RTLIL::Module::add ## _func(RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, const std::string &src) { \
+		RTLIL::Cell *cell = addCell(name, _type);                 \
+		cell->parameters[ID::WIDTH] = sig_a.size();               \
+		cell->setPort(ID::A, sig_a);                              \
+		cell->setPort(ID::B, sig_b);                              \
+		cell->setPort(ID::Y, sig_y);                              \
+		cell->set_src_attribute(src);                             \
+		return cell;                                              \
+	} \
+	RTLIL::SigSpec RTLIL::Module::_func(RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const std::string &src) { \
+		RTLIL::SigSpec sig_y = addWire(NEW_ID, sig_a.size());     \
+		add ## _func(name, sig_a, sig_s, sig_y, src);             \
+		return sig_y;                                             \
+	}
+DEF_METHOD(Bweqx,    ID($bweqx))
+#undef DEF_METHOD
+
 #define DEF_METHOD_2(_func, _type, _P1, _P2) \
 	RTLIL::Cell* RTLIL::Module::add ## _func(RTLIL::IdString name, const RTLIL::SigBit &sig1, const RTLIL::SigBit &sig2, const std::string &src) { \
 		RTLIL::Cell *cell = addCell(name, _type);         \

kernel/rtlil.h

@@ -505,6 +505,9 @@ namespace RTLIL
 	RTLIL::Const const_bmux        (const RTLIL::Const &arg1, const RTLIL::Const &arg2);
 	RTLIL::Const const_demux       (const RTLIL::Const &arg1, const RTLIL::Const &arg2);
 
+	RTLIL::Const const_bweqx       (const RTLIL::Const &arg1, const RTLIL::Const &arg2);
+	RTLIL::Const const_bwmux       (const RTLIL::Const &arg1, const RTLIL::Const &arg2, const RTLIL::Const &arg3);
+
 
 	// This iterator-range-pair is used for Design::modules(), Module::wires() and Module::cells().
 	// It maintains a reference counter that is used to make sure that the container is not modified while being iterated over.
@@ -1303,6 +1306,9 @@ public:
 	RTLIL::Cell* addBmux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const RTLIL::SigSpec &sig_y, const std::string &src = "");
 	RTLIL::Cell* addDemux (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const RTLIL::SigSpec &sig_y, const std::string &src = "");
 
+	RTLIL::Cell* addBweqx  (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, const std::string &src = "");
+	RTLIL::Cell* addBwmux  (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_s, const RTLIL::SigSpec &sig_y, const std::string &src = "");
+
 	RTLIL::Cell* addSlice  (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, RTLIL::Const offset, const std::string &src = "");
 	RTLIL::Cell* addConcat (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_y, const std::string &src = "");
 	RTLIL::Cell* addLut    (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_y, RTLIL::Const lut, const std::string &src = "");
@@ -1432,6 +1438,9 @@ public:
 	RTLIL::SigSpec Bmux     (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const std::string &src = "");
 	RTLIL::SigSpec Demux     (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_s, const std::string &src = "");
 
+	RTLIL::SigSpec Bweqx      (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const std::string &src = "");
+	RTLIL::SigSpec Bwmux      (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_b, const RTLIL::SigSpec &sig_s, const std::string &src = "");
+
 	RTLIL::SigBit BufGate    (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const std::string &src = "");
 	RTLIL::SigBit NotGate    (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const std::string &src = "");
 	RTLIL::SigBit AndGate    (RTLIL::IdString name, const RTLIL::SigBit &sig_a, const RTLIL::SigBit &sig_b, const std::string &src = "");

kernel/satgen.cc

@@ -223,7 +223,33 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		return true;
 	}
 
-	if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_)))
+	if (cell->type == ID($bweqx))
+	{
+		std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
+		std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
+		std::vector<int> y = importDefSigSpec(cell->getPort(ID::Y), timestep);
+
+		std::vector<int> bweqx = ez->vec_not(ez->vec_xor(a, b));
+
+		if (model_undef)
+		{
+			std::vector<int> undef_a = importUndefSigSpec(cell->getPort(ID::A), timestep);
+			std::vector<int> undef_b = importUndefSigSpec(cell->getPort(ID::B), timestep);
+			std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
+
+			std::vector<int> both_undef = ez->vec_and(undef_a, undef_b);
+			std::vector<int> both_def = ez->vec_and(ez->vec_not(undef_a), ez->vec_not(undef_b));
+
+			bweqx = ez->vec_or(both_undef, ez->vec_and(both_def, bweqx));
+
+			for (int yx : undef_y)
+				ez->assume(ez->NOT(yx));
+		}
+		ez->assume(ez->vec_eq(bweqx, y));
+		return true;
+	}
+
+	if (cell->type.in(ID($_MUX_), ID($mux), ID($_NMUX_), ID($bwmux)))
 	{
 		std::vector<int> a = importDefSigSpec(cell->getPort(ID::A), timestep);
 		std::vector<int> b = importDefSigSpec(cell->getPort(ID::B), timestep);
@@ -233,6 +259,8 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
 		if (cell->type == ID($_NMUX_))
 			ez->assume(ez->vec_eq(ez->vec_not(ez->vec_ite(s.at(0), b, a)), yy));
+		else if (cell->type == ID($bwmux))
+			ez->assume(ez->vec_eq(ez->vec_ite(s, b, a), yy));
 		else
 			ez->assume(ez->vec_eq(ez->vec_ite(s.at(0), b, a), yy));
 
@@ -245,7 +273,11 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 
 			std::vector<int> unequal_ab = ez->vec_not(ez->vec_iff(a, b));
 			std::vector<int> undef_ab = ez->vec_or(unequal_ab, ez->vec_or(undef_a, undef_b));
-			std::vector<int> yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
+			std::vector<int> yX;
+			if (cell->type == ID($bwmux))
+				yX = ez->vec_ite(undef_s, undef_ab, ez->vec_ite(s, undef_b, undef_a));
+			else
+				yX = ez->vec_ite(undef_s.at(0), undef_ab, ez->vec_ite(s.at(0), undef_b, undef_a));
 			ez->assume(ez->vec_eq(yX, undef_y));
 			undefGating(y, yy, undef_y);
 		}
@@ -375,29 +407,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 			std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
 			std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
 
-			int maybe_a = ez->CONST_TRUE;
+			int all_undef = ez->CONST_FALSE;
+			int found_active = ez->CONST_FALSE;
 
-			std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
+			std::vector<int> undef_tmp = undef_a;
-			std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
 
 			for (size_t i = 0; i < s.size(); i++)
 			{
-				std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
 				std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
 
-				int maybe_s = ez->OR(s.at(i), undef_s.at(i));
+				undef_tmp = ez->vec_ite(s.at(i), part_of_undef_b, undef_tmp);
-				int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
+				all_undef = ez->OR(all_undef, undef_s.at(i));
-
+				all_undef = ez->OR(all_undef, ez->AND(s.at(i), found_active));
-				maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
+				found_active = ez->OR(found_active, s.at(i));
-
-				bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
-				bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
 			}
 
-			bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
+			undef_tmp = ez->vec_or(undef_tmp, std::vector<int>(a.size(), all_undef));
-			bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
 
-			ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y));
+			ez->assume(ez->vec_eq(undef_tmp, undef_y));
 			undefGating(y, yy, undef_y);
 		}
 		return true;

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

passes/opt/opt_expr.cc

@@ -643,6 +643,148 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 			goto next_cell;
 		}
 
+		if (cell->type.in(ID($and), ID($or), ID($xor), ID($xnor)))
+		{
+			RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
+			RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID::B));
+
+			bool a_fully_const = (sig_a.is_fully_const() && (!keepdc || !sig_a.is_fully_undef()));
+			bool b_fully_const = (sig_b.is_fully_const() && (!keepdc || !sig_b.is_fully_undef()));
+
+			if (a_fully_const != b_fully_const)
+			{
+				cover("opt.opt_expr.bitwise_logic_one_const");
+				log_debug("Replacing %s cell `%s' in module `%s' having one fully constant input\n",
+						log_id(cell->type), log_id(cell->name), log_id(module));
+				RTLIL::SigSpec sig_y = assign_map(cell->getPort(ID::Y));
+
+				int width = GetSize(cell->getPort(ID::Y));
+
+				sig_a.extend_u0(width, cell->getParam(ID::A_SIGNED).as_bool());
+				sig_b.extend_u0(width, cell->getParam(ID::B_SIGNED).as_bool());
+
+				if (!a_fully_const)
+					std::swap(sig_a, sig_b);
+
+				RTLIL::SigSpec b_group_0, b_group_1, b_group_x;
+				RTLIL::SigSpec y_group_0, y_group_1, y_group_x;
+
+				for (int i = 0; i < width; i++) {
+					auto bit_a = sig_a[i].data;
+					if (bit_a == State::S0) b_group_0.append(sig_b[i]), y_group_0.append(sig_y[i]);
+					if (bit_a == State::S1) b_group_1.append(sig_b[i]), y_group_1.append(sig_y[i]);
+					if (bit_a == State::Sx) b_group_x.append(sig_b[i]), y_group_x.append(sig_y[i]);
+				}
+
+				if (cell->type == ID($xnor)) {
+					std::swap(b_group_0, b_group_1);
+					std::swap(y_group_0, y_group_1);
+				}
+
+				RTLIL::SigSpec y_new_0, y_new_1, y_new_x;
+
+				if (cell->type == ID($and)) {
+					if (!y_group_0.empty()) y_new_0 = Const(State::S0, GetSize(y_group_0));
+					if (!y_group_1.empty()) y_new_1 = b_group_1;
+					if (!y_group_x.empty()) {
+						if (keepdc)
+							y_new_x = module->And(NEW_ID, Const(State::Sx, GetSize(y_group_x)), b_group_x);
+						else
+							y_new_x = Const(State::S0, GetSize(y_group_x));
+					}
+				} else if (cell->type == ID($or)) {
+					if (!y_group_0.empty()) y_new_0 = b_group_0;
+					if (!y_group_1.empty()) y_new_1 = Const(State::S1, GetSize(y_group_1));
+					if (!y_group_x.empty()) {
+						if (keepdc)
+							y_new_x = module->Or(NEW_ID, Const(State::Sx, GetSize(y_group_x)), b_group_x);
+						else
+							y_new_x = Const(State::S1, GetSize(y_group_x));
+					}
+				} else if (cell->type.in(ID($xor), ID($xnor))) {
+					if (!y_group_0.empty()) y_new_0 = b_group_0;
+					if (!y_group_1.empty()) y_new_1 = module->Not(NEW_ID, b_group_1);
+					if (!y_group_x.empty()) {
+						if (keepdc)
+							y_new_x = module->Xor(NEW_ID, Const(State::Sx, GetSize(y_group_x)), b_group_x);
+						else // This should be fine even with keepdc, but opt_expr_xor.ys wants to keep the xor
+							y_new_x = Const(State::Sx, GetSize(y_group_x));
+					}
+				} else {
+					log_abort();
+				}
+
+				assign_map.add(y_group_0, y_new_0); module->connect(y_group_0, y_new_0);
+				assign_map.add(y_group_1, y_new_1); module->connect(y_group_1, y_new_1);
+				assign_map.add(y_group_x, y_new_x); module->connect(y_group_x, y_new_x);
+
+				module->remove(cell);
+				did_something = true;
+				goto next_cell;
+			}
+		}
+
+		if (cell->type == ID($bwmux))
+		{
+			RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
+			RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID::B));
+			RTLIL::SigSpec sig_s = assign_map(cell->getPort(ID::S));
+			RTLIL::SigSpec sig_y = assign_map(cell->getPort(ID::Y));
+			int width = GetSize(cell->getPort(ID::Y));
+
+			if (sig_s.is_fully_def())
+			{
+				RTLIL::SigSpec a_group_0, b_group_1;
+				RTLIL::SigSpec y_group_0, y_group_1;
+				for (int i = 0; i < width; i++) {
+					if (sig_s[i].data == State::S1)
+						y_group_1.append(sig_y[i]), b_group_1.append(sig_b[i]);
+					else
+						y_group_0.append(sig_y[i]), a_group_0.append(sig_a[i]);
+				}
+
+				assign_map.add(y_group_0, a_group_0); module->connect(y_group_0, a_group_0);
+				assign_map.add(y_group_1, b_group_1); module->connect(y_group_1, b_group_1);
+
+				module->remove(cell);
+				did_something = true;
+				goto next_cell;
+			}
+			else if (sig_a.is_fully_def() || sig_b.is_fully_def())
+			{
+				bool flip = !sig_a.is_fully_def();
+				if (flip)
+					std::swap(sig_a, sig_b);
+
+				RTLIL::SigSpec b_group_0, b_group_1;
+				RTLIL::SigSpec s_group_0, s_group_1;
+				RTLIL::SigSpec y_group_0, y_group_1;
+				for (int i = 0; i < width; i++) {
+					if (sig_a[i].data == State::S1)
+						y_group_1.append(sig_y[i]), b_group_1.append(sig_b[i]), s_group_1.append(sig_s[i]);
+					else
+						y_group_0.append(sig_y[i]), b_group_0.append(sig_b[i]), s_group_0.append(sig_s[i]);
+				}
+
+				RTLIL::SigSpec y_new_0, y_new_1;
+
+				if (flip) {
+					if (!y_group_0.empty()) y_new_0 = module->And(NEW_ID, b_group_0, module->Not(NEW_ID, s_group_0));
+					if (!y_group_1.empty()) y_new_1 = module->Or(NEW_ID, b_group_1, s_group_1);
+				} else {
+					if (!y_group_0.empty()) y_new_0 = module->And(NEW_ID, b_group_0, s_group_0);
+					if (!y_group_1.empty()) y_new_1 = module->Or(NEW_ID, b_group_1, module->Not(NEW_ID, s_group_1));
+				}
+
+				module->connect(y_group_0, y_new_0);
+				module->connect(y_group_1, y_new_1);
+
+				module->remove(cell);
+				did_something = true;
+				goto next_cell;
+			}
+		}
+
 		if (do_fine)
 		{
 			if (cell->type.in(ID($not), ID($pos), ID($and), ID($or), ID($xor), ID($xnor)))
@@ -905,7 +1047,7 @@ skip_fine_alu:
 			}
 		}
 
-		if (cell->type.in(ID($shiftx), ID($shift))) {
+		if (cell->type.in(ID($shiftx), ID($shift)) && (cell->type == ID($shiftx) || !cell->getParam(ID::A_SIGNED).as_bool())) {
 			SigSpec sig_a = assign_map(cell->getPort(ID::A));
 			int width;
 			bool trim_x = cell->type == ID($shiftx) || !keepdc;
@@ -1152,7 +1294,7 @@ skip_fine_alu:
 			goto next_cell;
 		}
 
-		if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)) && assign_map(cell->getPort(ID::B)).is_fully_const())
+		if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)) && (keepdc ? assign_map(cell->getPort(ID::B)).is_fully_def() : assign_map(cell->getPort(ID::B)).is_fully_const()))
 		{
 			bool sign_ext = cell->type == ID($sshr) && cell->getParam(ID::A_SIGNED).as_bool();
 			int shift_bits = assign_map(cell->getPort(ID::B)).as_int(cell->type.in(ID($shift), ID($shiftx)) && cell->getParam(ID::B_SIGNED).as_bool());
@@ -1163,7 +1305,7 @@ skip_fine_alu:
 			RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
 			RTLIL::SigSpec sig_y(cell->type == ID($shiftx) ? RTLIL::State::Sx : RTLIL::State::S0, cell->getParam(ID::Y_WIDTH).as_int());
 
-			if (GetSize(sig_a) < GetSize(sig_y))
+			if (cell->type != ID($shiftx) && GetSize(sig_a) < GetSize(sig_y))
 				sig_a.extend_u0(GetSize(sig_y), cell->getParam(ID::A_SIGNED).as_bool());
 
 			for (int i = 0; i < GetSize(sig_y); i++) {
@@ -1446,6 +1588,31 @@ skip_identity:
 				goto next_cell; \
 			} \
 		}
+#define FOLD_2ARG_SIMPLE_CELL(_t, B_ID) \
+		if (cell->type == ID($##_t)) { \
+			RTLIL::SigSpec a = cell->getPort(ID::A); \
+			RTLIL::SigSpec b = cell->getPort(B_ID); \
+			assign_map.apply(a), assign_map.apply(b); \
+			if (a.is_fully_const() && b.is_fully_const()) { \
+				RTLIL::SigSpec y(RTLIL::const_ ## _t(a.as_const(), b.as_const())); \
+				cover("opt.opt_expr.const.$" #_t); \
+				replace_cell(assign_map, module, cell, stringf("%s, %s", log_signal(a), log_signal(b)), ID::Y, y); \
+				goto next_cell; \
+			} \
+		}
+#define FOLD_MUX_CELL(_t) \
+		if (cell->type == ID($##_t)) { \
+			RTLIL::SigSpec a = cell->getPort(ID::A); \
+			RTLIL::SigSpec b = cell->getPort(ID::B); \
+			RTLIL::SigSpec s = cell->getPort(ID::S); \
+			assign_map.apply(a), assign_map.apply(b), assign_map.apply(s); \
+			if (a.is_fully_const() && b.is_fully_const() && s.is_fully_const()) { \
+				RTLIL::SigSpec y(RTLIL::const_ ## _t(a.as_const(), b.as_const(), s.as_const())); \
+				cover("opt.opt_expr.const.$" #_t); \
+				replace_cell(assign_map, module, cell, stringf("%s, %s, %s", log_signal(a), log_signal(b), log_signal(s)), ID::Y, y); \
+				goto next_cell; \
+			} \
+		}
 
 		FOLD_1ARG_CELL(not)
 		FOLD_2ARG_CELL(and)
@@ -1477,6 +1644,9 @@ skip_identity:
 		FOLD_2ARG_CELL(gt)
 		FOLD_2ARG_CELL(ge)
 
+		FOLD_2ARG_CELL(eqx)
+		FOLD_2ARG_CELL(nex)
+
 		FOLD_2ARG_CELL(add)
 		FOLD_2ARG_CELL(sub)
 		FOLD_2ARG_CELL(mul)
@@ -1489,6 +1659,13 @@ skip_identity:
 		FOLD_1ARG_CELL(pos)
 		FOLD_1ARG_CELL(neg)
 
+		FOLD_MUX_CELL(mux);
+		FOLD_MUX_CELL(pmux);
+		FOLD_2ARG_SIMPLE_CELL(bmux, ID::S);
+		FOLD_2ARG_SIMPLE_CELL(demux, ID::S);
+		FOLD_2ARG_SIMPLE_CELL(bweqx, ID::B);
+		FOLD_MUX_CELL(bwmux);
+
 		// be very conservative with optimizing $mux cells as we do not want to break mux trees
 		if (cell->type == ID($mux)) {
 			RTLIL::SigSpec input = assign_map(cell->getPort(ID::S));

passes/sat/formalff.cc

@@ -532,12 +532,14 @@ struct FormalFfPass : public Pass {
 						if ((int)bits.size() == ff.val_init.size()) {
 							// This check is only to make the private names more helpful for debugging
 							ff.is_anyinit = true;
+							ff.is_fine = false;
 							emit = true;
 							break;
 						}
 
 						auto slice = ff.slice(bits);
 						slice.is_anyinit = is_anyinit;
+						slice.is_fine = false;
 						slice.emit();
 					}
 				}

passes/sat/miter.cc

@@ -30,6 +30,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 	bool flag_make_outputs = false;
 	bool flag_make_outcmp = false;
 	bool flag_make_assert = false;
+	bool flag_make_cover = false;
 	bool flag_flatten = false;
 	bool flag_cross = false;
 
@@ -54,6 +55,10 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 			flag_make_assert = true;
 			continue;
 		}
+		if (args[argidx] == "-make_cover") {
+			flag_make_cover = true;
+			continue;
+		}
 		if (args[argidx] == "-flatten") {
 			flag_flatten = true;
 			continue;
@@ -237,6 +242,12 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
 				miter_module->connect(RTLIL::SigSig(w_cmp, this_condition));
 			}
 
+			if (flag_make_cover)
+			{
+				auto cover_condition = miter_module->Not(NEW_ID, this_condition);
+				miter_module->addCover("\\cover_" + RTLIL::unescape_id(gold_wire->name), cover_condition, State::S1);
+			}
+
 			all_conditions.append(this_condition);
 		}
 	}
@@ -402,6 +413,9 @@ struct MiterPass : public Pass {
 		log("    -make_assert\n");
 		log("        also create an 'assert' cell that checks if trigger is always low.\n");
 		log("\n");
+		log("    -make_cover\n");
+		log("        also create a 'cover' cell for each gold/gate output pair.\n");
+		log("\n");
 		log("    -flatten\n");
 		log("        call 'flatten -wb; opt_expr -keepdc -undriven;;' on the miter circuit.\n");
 		log("\n");

passes/sat/sim.cc

@@ -509,7 +509,7 @@ struct SimInstance
 		}
 	}
 
-	bool update_ph2()
+	bool update_ph2(bool gclk)
 	{
 		bool did_something = false;
 
@@ -567,7 +567,8 @@ struct SimInstance
 			}
 			if (ff_data.has_gclk) {
 				// $ff
-				current_q = ff.past_d;
+				if (gclk)
+					current_q = ff.past_d;
 			}
 			if (set_state(ff_data.sig_q, current_q))
 				did_something = true;
@@ -616,7 +617,7 @@ struct SimInstance
 		}
 
 		for (auto it : children)
-			if (it.second->update_ph2()) {
+			if (it.second->update_ph2(gclk)) {
 				dirty_children.insert(it.second);
 				did_something = true;
 			}
@@ -985,7 +986,7 @@ struct SimWorker : SimShared
 			writer->write(use_signal);
 	}
 
-	void update()
+	void update(bool gclk)
 	{
 		while (1)
 		{
@@ -997,7 +998,7 @@ struct SimWorker : SimShared
 			if (debug)
 				log("\n-- ph2 --\n");
 
-			if (!top->update_ph2())
+			if (!top->update_ph2(gclk))
 				break;
 		}
 
@@ -1047,7 +1048,7 @@ struct SimWorker : SimShared
 		set_inports(clock, State::Sx);
 		set_inports(clockn, State::Sx);
 
-		update();
+		update(false);
 
 		register_output_step(0);
 
@@ -1060,7 +1061,7 @@ struct SimWorker : SimShared
 			set_inports(clock, State::S0);
 			set_inports(clockn, State::S1);
 
-			update();
+			update(true);
 			register_output_step(10*cycle + 5);
 
 			if (debug)
@@ -1076,7 +1077,7 @@ struct SimWorker : SimShared
 				set_inports(resetn, State::S1);
 			}
 
-			update();
+			update(true);
 			register_output_step(10*cycle + 10);
 		}
 
@@ -1193,7 +1194,7 @@ struct SimWorker : SimShared
 					initial = false;
 				}
 				if (did_something)
-					update();
+					update(true);
 				register_output_step(time);
 
 				bool status = top->checkSignals();
@@ -1342,12 +1343,12 @@ struct SimWorker : SimShared
 						set_inports(clock, State::S0);
 						set_inports(clockn, State::S1);
 					}
-					update();
+					update(true);
 					register_output_step(10*cycle);
 					if (!multiclock && cycle) {
 						set_inports(clock, State::S0);
 						set_inports(clockn, State::S1);
-						update();
+						update(true);
 						register_output_step(10*cycle + 5);
 					}
 					cycle++;
@@ -1419,12 +1420,12 @@ struct SimWorker : SimShared
 						log("Simulating cycle %d.\n", cycle);
 					set_inports(clock, State::S1);
 					set_inports(clockn, State::S0);
-					update();
+					update(true);
 					register_output_step(10*cycle+0);
 					if (!multiclock) {
 						set_inports(clock, State::S0);
 						set_inports(clockn, State::S1);
-						update();
+						update(true);
 						register_output_step(10*cycle+5);
 					}
 					cycle++;

passes/techmap/Makefile.inc

@@ -31,6 +31,7 @@ OBJS += passes/techmap/dffinit.o
 OBJS += passes/techmap/pmuxtree.o
 OBJS += passes/techmap/bmuxmap.o
 OBJS += passes/techmap/demuxmap.o
+OBJS += passes/techmap/bwmuxmap.o
 OBJS += passes/techmap/muxcover.o
 OBJS += passes/techmap/aigmap.o
 OBJS += passes/techmap/tribuf.o

passes/techmap/bwmuxmap.cc

@@ -0,0 +1,70 @@
+/*
+ *  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/yosys.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct BwmuxmapPass : public Pass {
+	BwmuxmapPass() : Pass("bwmuxmap", "replace $bwmux cells with equivalent logic") {}
+	void help() override
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    bwmxumap [options] [selection]\n");
+		log("\n");
+		log("This pass replaces $bwmux cells with equivalent logic\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		log_header(design, "Executing BWMUXMAP pass.\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			// if (args[argidx] == "-arg") {
+			// 	continue;
+			// }
+			break;
+		}
+
+		extra_args(args, argidx, design);
+
+		for (auto module : design->selected_modules())
+		for (auto cell : module->selected_cells())
+		{
+			if (cell->type != ID($bwmux))
+				continue;
+			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 not_s = module->Not(NEW_ID, sig_s);
+			auto masked_b = module->And(NEW_ID, sig_s, sig_b);
+			auto masked_a = module->And(NEW_ID, not_s, sig_a);
+			module->addOr(NEW_ID, masked_a, masked_b, sig_y);
+
+			module->remove(cell);
+		}
+	}
+} BwmuxmapPass;
+
+PRIVATE_NAMESPACE_END

passes/techmap/simplemap.cc

@@ -58,28 +58,17 @@ void simplemap_bitop(RTLIL::Module *module, RTLIL::Cell *cell)
 	RTLIL::SigSpec sig_b = cell->getPort(ID::B);
 	RTLIL::SigSpec sig_y = cell->getPort(ID::Y);
 
-	sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
+	if (cell->type != ID($bweqx)) {
-	sig_b.extend_u0(GetSize(sig_y), cell->parameters.at(ID::B_SIGNED).as_bool());
+		sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
-
+		sig_b.extend_u0(GetSize(sig_y), cell->parameters.at(ID::B_SIGNED).as_bool());
-	if (cell->type == ID($xnor))
-	{
-		RTLIL::SigSpec sig_t = module->addWire(NEW_ID, GetSize(sig_y));
-
-		for (int i = 0; i < GetSize(sig_y); i++) {
-			RTLIL::Cell *gate = module->addCell(NEW_ID, ID($_NOT_));
-			gate->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
-			gate->setPort(ID::A, sig_t[i]);
-			gate->setPort(ID::Y, sig_y[i]);
-		}
-
-		sig_y = sig_t;
 	}
 
 	IdString gate_type;
-	if (cell->type == ID($and))  gate_type = ID($_AND_);
+	if (cell->type == ID($and))   gate_type = ID($_AND_);
-	if (cell->type == ID($or))   gate_type = ID($_OR_);
+	if (cell->type == ID($or))    gate_type = ID($_OR_);
-	if (cell->type == ID($xor))  gate_type = ID($_XOR_);
+	if (cell->type == ID($xor))   gate_type = ID($_XOR_);
-	if (cell->type == ID($xnor)) gate_type = ID($_XOR_);
+	if (cell->type == ID($xnor))  gate_type = ID($_XNOR_);
+	if (cell->type == ID($bweqx)) gate_type = ID($_XNOR_);
 	log_assert(!gate_type.empty());
 
 	for (int i = 0; i < GetSize(sig_y); i++) {
@@ -284,6 +273,23 @@ void simplemap_mux(RTLIL::Module *module, RTLIL::Cell *cell)
 	}
 }
 
+void simplemap_bwmux(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+	RTLIL::SigSpec sig_a = cell->getPort(ID::A);
+	RTLIL::SigSpec sig_b = cell->getPort(ID::B);
+	RTLIL::SigSpec sig_s = cell->getPort(ID::S);
+	RTLIL::SigSpec sig_y = cell->getPort(ID::Y);
+
+	for (int i = 0; i < GetSize(sig_y); i++) {
+		RTLIL::Cell *gate = module->addCell(NEW_ID, ID($_MUX_));
+		gate->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+		gate->setPort(ID::A, sig_a[i]);
+		gate->setPort(ID::B, sig_b[i]);
+		gate->setPort(ID::S, sig_s[i]);
+		gate->setPort(ID::Y, sig_y[i]);
+	}
+}
+
 void simplemap_tribuf(RTLIL::Module *module, RTLIL::Cell *cell)
 {
 	RTLIL::SigSpec sig_a = cell->getPort(ID::A);
@@ -409,6 +415,7 @@ void simplemap_get_mappers(dict<IdString, void(*)(RTLIL::Module*, RTLIL::Cell*)>
 	mappers[ID($or)]          = simplemap_bitop;
 	mappers[ID($xor)]         = simplemap_bitop;
 	mappers[ID($xnor)]        = simplemap_bitop;
+	mappers[ID($bweqx)]       = simplemap_bitop;
 	mappers[ID($reduce_and)]  = simplemap_reduce;
 	mappers[ID($reduce_or)]   = simplemap_reduce;
 	mappers[ID($reduce_xor)]  = simplemap_reduce;
@@ -422,6 +429,7 @@ void simplemap_get_mappers(dict<IdString, void(*)(RTLIL::Module*, RTLIL::Cell*)>
 	mappers[ID($ne)]          = simplemap_eqne;
 	mappers[ID($nex)]         = simplemap_eqne;
 	mappers[ID($mux)]         = simplemap_mux;
+	mappers[ID($bwmux)]       = simplemap_bwmux;
 	mappers[ID($tribuf)]      = simplemap_tribuf;
 	mappers[ID($bmux)]        = simplemap_bmux;
 	mappers[ID($lut)]         = simplemap_lut;

passes/techmap/simplemap.h

@@ -31,6 +31,7 @@ extern void simplemap_reduce(RTLIL::Module *module, RTLIL::Cell *cell);
 extern void simplemap_lognot(RTLIL::Module *module, RTLIL::Cell *cell);
 extern void simplemap_logbin(RTLIL::Module *module, RTLIL::Cell *cell);
 extern void simplemap_mux(RTLIL::Module *module, RTLIL::Cell *cell);
+extern void simplemap_bwmux(RTLIL::Module *module, RTLIL::Cell *cell);
 extern void simplemap_lut(RTLIL::Module *module, RTLIL::Cell *cell);
 extern void simplemap_slice(RTLIL::Module *module, RTLIL::Cell *cell);
 extern void simplemap_concat(RTLIL::Module *module, RTLIL::Cell *cell);

techlibs/common/simlib.v

@@ -1300,11 +1300,11 @@ wire [WIDTH-1:0] bm0_out, bm1_out;
 
 generate
 	if (S_WIDTH > 1) begin:muxlogic
-		\$bmux #(.WIDTH(WIDTH), .S_WIDTH(S_WIDTH-1)) bm0 (.A(A), .S(S[S_WIDTH-2:0]), .Y(bm0_out));
+		\$bmux #(.WIDTH(WIDTH), .S_WIDTH(S_WIDTH-1)) bm0 (.A(A[(WIDTH << (S_WIDTH - 1))-1:0]), .S(S[S_WIDTH-2:0]), .Y(bm0_out));
 		\$bmux #(.WIDTH(WIDTH), .S_WIDTH(S_WIDTH-1)) bm1 (.A(A[(WIDTH << S_WIDTH)-1:WIDTH << (S_WIDTH - 1)]), .S(S[S_WIDTH-2:0]), .Y(bm1_out));
 		assign Y = S[S_WIDTH-1] ? bm1_out : bm0_out;
 	end else if (S_WIDTH == 1) begin:simple
-		assign Y = S ? A[1] : A[0];
+		assign Y = S ? A[2*WIDTH-1:WIDTH] : A[WIDTH-1:0];
 	end else begin:passthru
 		assign Y = A;
 	end
@@ -1331,10 +1331,17 @@ always @* begin
 	Y = A;
 	found_active_sel_bit = 0;
 	for (i = 0; i < S_WIDTH; i = i+1)
-		if (S[i]) begin
+		case (S[i])
-			Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
+			1'b1: begin
-			found_active_sel_bit = 1;
+				Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
-		end
+				found_active_sel_bit = 1;
+			end
+			1'b0: ;
+			1'bx: begin
+				Y = 'bx;
+				found_active_sel_bit = 'bx;
+			end
+		endcase
 end
 
 endmodule
@@ -1370,7 +1377,7 @@ parameter LUT = 0;
 input [WIDTH-1:0] A;
 output Y;
 
-\$bmux #(.WIDTH(1), .S_WIDTH(WIDTH)) mux(.A(LUT), .S(A), .Y(Y));
+\$bmux #(.WIDTH(1), .S_WIDTH(WIDTH)) mux(.A(LUT[(1<<WIDTH)-1:0]), .S(A), .Y(Y));
 
 endmodule
 
@@ -1594,6 +1601,43 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$bweqx (A, B, Y);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] A, B;
+output [WIDTH-1:0] Y;
+
+genvar i;
+generate
+	for (i = 0; i < WIDTH; i = i + 1) begin:slices
+		assign Y[i] = A[i] === B[i];
+	end
+endgenerate
+
+endmodule
+
+// --------------------------------------------------------
+
+module \$bwmux (A, B, S, Y);
+
+parameter WIDTH = 0;
+
+input [WIDTH-1:0] A, B;
+input [WIDTH-1:0] S;
+output [WIDTH-1:0] Y;
+
+genvar i;
+generate
+	for (i = 0; i < WIDTH; i = i + 1) begin:slices
+		assign Y[i] = S[i] ? B[i] : A[i];
+	end
+endgenerate
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$assert (A, EN);
 
 input A, EN;
@@ -1693,6 +1737,9 @@ endmodule
 
 // --------------------------------------------------------
 `ifdef SIMLIB_FF
+`ifndef SIMLIB_GLOBAL_CLOCK
+`define SIMLIB_GLOBAL_CLOCK $global_clk
+`endif
 module \$anyinit (D, Q);
 
 parameter WIDTH = 0;
@@ -1702,7 +1749,7 @@ output reg [WIDTH-1:0] Q;
 
 initial Q <= 'bx;
 
-always @($global_clk) begin
+always @(`SIMLIB_GLOBAL_CLOCK) begin
 	Q <= D;
 end
 
@@ -1783,6 +1830,9 @@ endmodule
 `endif
 // --------------------------------------------------------
 `ifdef SIMLIB_FF
+`ifndef SIMLIB_GLOBAL_CLOCK
+`define SIMLIB_GLOBAL_CLOCK $global_clk
+`endif
 
 module \$ff (D, Q);
 
@@ -1791,7 +1841,7 @@ parameter WIDTH = 0;
 input [WIDTH-1:0] D;
 output reg [WIDTH-1:0] Q;
 
-always @($global_clk) begin
+always @(`SIMLIB_GLOBAL_CLOCK) begin
 	Q <= D;
 end
 

techlibs/common/techmap.v

@@ -59,7 +59,7 @@ module _90_simplemap_compare_ops;
 endmodule
 
 (* techmap_simplemap *)
-(* techmap_celltype = "$pos $slice $concat $mux $tribuf $bmux" *)
+(* techmap_celltype = "$pos $slice $concat $mux $tribuf $bmux $bwmux $bweqx" *)
 module _90_simplemap_various;
 endmodule
 

tests/opt/opt_expr_xnor.ys

@@ -32,7 +32,7 @@ select -assert-count 1 c:*
 cd fine_keepdc
 simplemap
 opt_expr -keepdc
-select -assert-count 1 t:$_XOR_
+select -assert-count 1 t:$_XNOR_
 
 cd
 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3

tests/opt/opt_expr_xor.ys

@@ -22,9 +22,8 @@ simplemap
 equiv_opt -assert opt_expr
 design -load postopt
 select -assert-none t:$_XOR_
-select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
+select -assert-none t:$_XNOR_
-select -assert-count 3 t:$_NOT_
+select -assert-count 2 t:$_NOT_
-
 
 design -reset
 read_verilog -icells <<EOT
@@ -36,7 +35,7 @@ EOT
 select -assert-count 2 t:$_XNOR_
 equiv_opt -assert opt_expr
 design -load postopt
-select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
+select -assert-none t:$_XNOR_
 select -assert-count 1 t:$_NOT_
 
 

tests/xprop/.gitignore

@@ -0,0 +1,2 @@
+/xprop_*
+/run-test.mk

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"

tests/xprop/run-test.sh

@@ -0,0 +1,5 @@
+#!/bin/bash
+set -e
+
+python3 generate.py $@
+make -f run-test.mk

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())