Merge pull request #1075 from YosysHQ/eddie/muxpack

Add new "muxpack" command for packing chains of $mux cells

5 files changed, 897 insertions, 0 deletions

diff --git a/CHANGELOG b/CHANGELOG
index 128f6c6ff..8c88a7db8 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -20,6 +20,7 @@ Yosys 0.8 .. Yosys 0.8-dev
     - Added "muxcover -mux{4,8,16}=<cost>"
     - Added "muxcover -dmux=<cost>"
     - Added "muxcover -nopartial"
+    - Added "muxpack" pass
     - "synth_xilinx" to now infer hard shift registers, using new "shregmap -tech xilinx"
     - Fixed sign extension of unsized constants with 'bx and 'bz MSB
 
diff --git a/passes/opt/Makefile.inc b/passes/opt/Makefile.inc
index 337fee9e4..ea3646330 100644
--- a/passes/opt/Makefile.inc
+++ b/passes/opt/Makefile.inc
@@ -14,5 +14,6 @@ OBJS += passes/opt/opt_demorgan.o
 OBJS += passes/opt/rmports.o
 OBJS += passes/opt/opt_lut.o
 OBJS += passes/opt/pmux2shiftx.o
+OBJS += passes/opt/muxpack.o
 endif
 
diff --git a/passes/opt/muxpack.cc b/passes/opt/muxpack.cc
new file mode 100644
index 000000000..6697d6ca1
--- /dev/null
+++ b/passes/opt/muxpack.cc
@@ -0,0 +1,368 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *                2019  Eddie Hung    <eddie@fpgeh.com>
+ *
+ *  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"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct ExclusiveDatabase
+{
+	Module *module;
+	const SigMap &sigmap;
+
+	dict<SigBit, std::pair<SigSpec,std::vector<Const>>> sig_cmp_prev;
+
+	ExclusiveDatabase(Module *module, const SigMap &sigmap) : module(module), sigmap(sigmap)
+	{
+		SigSpec const_sig, nonconst_sig;
+		SigBit y_port;
+		pool<Cell*> reduce_or;
+		for (auto cell : module->cells()) {
+			if (cell->type == "$eq") {
+				nonconst_sig = sigmap(cell->getPort("\\A"));
+				const_sig = sigmap(cell->getPort("\\B"));
+				if (!const_sig.is_fully_const()) {
+					if (!nonconst_sig.is_fully_const())
+						continue;
+					std::swap(nonconst_sig, const_sig);
+				}
+				y_port = sigmap(cell->getPort("\\Y"));
+			}
+			else if (cell->type == "$logic_not") {
+				nonconst_sig = sigmap(cell->getPort("\\A"));
+				const_sig = Const(RTLIL::S0, GetSize(nonconst_sig));
+				y_port = sigmap(cell->getPort("\\Y"));
+			}
+			else if (cell->type == "$reduce_or") {
+				reduce_or.insert(cell);
+				continue;
+			}
+			else continue;
+
+			log_assert(!nonconst_sig.empty());
+			log_assert(!const_sig.empty());
+			sig_cmp_prev[y_port] = std::make_pair(nonconst_sig,std::vector<Const>{const_sig.as_const()});
+		}
+
+		for (auto cell : reduce_or) {
+			nonconst_sig = SigSpec();
+			std::vector<Const> values;
+			SigSpec a_port = sigmap(cell->getPort("\\A"));
+			for (auto bit : a_port) {
+				auto it = sig_cmp_prev.find(bit);
+				if (it == sig_cmp_prev.end()) {
+					nonconst_sig = SigSpec();
+					break;
+				}
+				if (nonconst_sig.empty())
+					nonconst_sig = it->second.first;
+				else if (nonconst_sig != it->second.first) {
+					nonconst_sig = SigSpec();
+					break;
+				}
+				for (auto value : it->second.second)
+					values.push_back(value);
+			}
+			if (nonconst_sig.empty())
+				continue;
+			y_port = sigmap(cell->getPort("\\Y"));
+			sig_cmp_prev[y_port] = std::make_pair(nonconst_sig,std::move(values));
+		}
+	}
+
+	bool query(const SigSpec &sig) const
+	{
+		SigSpec nonconst_sig;
+		pool<Const> const_values;
+
+		for (auto bit : sig.bits()) {
+			auto it = sig_cmp_prev.find(bit);
+			if (it == sig_cmp_prev.end())
+				return false;
+
+			if (nonconst_sig.empty())
+				nonconst_sig = it->second.first;
+			else if (nonconst_sig != it->second.first)
+				return false;
+
+			for (auto value : it->second.second)
+				if (!const_values.insert(value).second)
+					return false;
+		}
+
+		return true;
+	}
+};
+
+
+struct MuxpackWorker
+{
+	Module *module;
+	SigMap sigmap;
+
+	int mux_count, pmux_count;
+
+	pool<Cell*> remove_cells;
+
+	dict<SigSpec, Cell*> sig_chain_next;
+	dict<SigSpec, Cell*> sig_chain_prev;
+	pool<SigBit> sigbit_with_non_chain_users;
+	pool<Cell*> chain_start_cells;
+	pool<Cell*> candidate_cells;
+
+	ExclusiveDatabase excl_db;
+
+	void make_sig_chain_next_prev()
+	{
+		for (auto wire : module->wires())
+		{
+			if (wire->port_output || wire->get_bool_attribute("\\keep")) {
+				for (auto bit : sigmap(wire))
+					sigbit_with_non_chain_users.insert(bit);
+			}
+		}
+
+		for (auto cell : module->cells())
+		{
+			if (cell->type.in("$mux", "$pmux") && !cell->get_bool_attribute("\\keep"))
+			{
+				SigSpec a_sig = sigmap(cell->getPort("\\A"));
+				SigSpec b_sig;
+				if (cell->type == "$mux")
+					b_sig = sigmap(cell->getPort("\\B"));
+				SigSpec y_sig = sigmap(cell->getPort("\\Y"));
+   
+				if (sig_chain_next.count(a_sig))
+					for (auto a_bit : a_sig.bits())
+						sigbit_with_non_chain_users.insert(a_bit);
+				else {
+					sig_chain_next[a_sig] = cell;
+					candidate_cells.insert(cell);
+				}
+
+				if (!b_sig.empty()) {
+					if (sig_chain_next.count(b_sig))
+						for (auto b_bit : b_sig.bits())
+							sigbit_with_non_chain_users.insert(b_bit);
+					else {
+						sig_chain_next[b_sig] = cell;
+						candidate_cells.insert(cell);
+					}
+				}
+
+				sig_chain_prev[y_sig] = cell;
+				continue;
+			}
+
+			for (auto conn : cell->connections())
+				if (cell->input(conn.first))
+					for (auto bit : sigmap(conn.second))
+						sigbit_with_non_chain_users.insert(bit);
+		}
+	}
+
+	void find_chain_start_cells()
+	{
+		for (auto cell : candidate_cells)
+		{
+			log_debug("Considering %s (%s)\n", log_id(cell), log_id(cell->type));
+
+			SigSpec a_sig = sigmap(cell->getPort("\\A"));
+			if (cell->type == "$mux") {
+				SigSpec b_sig = sigmap(cell->getPort("\\B"));
+				if (sig_chain_prev.count(a_sig) + sig_chain_prev.count(b_sig) != 1)
+					goto start_cell;
+
+				if (!sig_chain_prev.count(a_sig))
+					a_sig = b_sig;
+			}
+			else if (cell->type == "$pmux") {
+				if (!sig_chain_prev.count(a_sig))
+					goto start_cell;
+			}
+			else log_abort();
+
+			for (auto bit : a_sig.bits())
+				if (sigbit_with_non_chain_users.count(bit))
+					goto start_cell;
+
+			{
+				Cell *prev_cell = sig_chain_prev.at(a_sig);
+				log_assert(prev_cell);
+				SigSpec s_sig = sigmap(cell->getPort("\\S"));
+				s_sig.append(sigmap(prev_cell->getPort("\\S")));
+				if (!excl_db.query(s_sig))
+					goto start_cell;
+			}
+
+			continue;
+
+		start_cell:
+			chain_start_cells.insert(cell);
+		}
+	}
+
+	vector<Cell*> create_chain(Cell *start_cell)
+	{
+		vector<Cell*> chain;
+
+		Cell *c = start_cell;
+		while (c != nullptr)
+		{
+			chain.push_back(c);
+
+			SigSpec y_sig = sigmap(c->getPort("\\Y"));
+
+			if (sig_chain_next.count(y_sig) == 0)
+				break;
+
+			c = sig_chain_next.at(y_sig);
+			if (chain_start_cells.count(c) != 0)
+				break;
+		}
+
+		return chain;
+	}
+
+	void process_chain(vector<Cell*> &chain)
+	{
+		if (GetSize(chain) < 2)
+			return;
+
+		int cursor = 0;
+		while (cursor < GetSize(chain))
+		{
+			int cases = GetSize(chain) - cursor;
+
+			Cell *first_cell = chain[cursor];
+			dict<int, SigBit> taps_dict;
+
+			if (cases < 2) {
+				cursor++;
+				continue;
+			}
+
+			Cell *last_cell = chain[cursor+cases-1];
+
+			log("Converting %s.%s ... %s.%s to a pmux with %d cases.\n",
+				log_id(module), log_id(first_cell), log_id(module), log_id(last_cell), cases);
+
+			mux_count += cases;
+			pmux_count += 1;
+
+			first_cell->type = "$pmux";
+			SigSpec b_sig = first_cell->getPort("\\B");
+			SigSpec s_sig = first_cell->getPort("\\S");
+
+			for (int i = 1; i < cases; i++) {
+				Cell* prev_cell = chain[cursor+i-1];
+				Cell* cursor_cell = chain[cursor+i];
+				if (sigmap(prev_cell->getPort("\\Y")) == sigmap(cursor_cell->getPort("\\A"))) {
+					b_sig.append(cursor_cell->getPort("\\B"));
+					s_sig.append(cursor_cell->getPort("\\S"));
+				}
+				else {
+					log_assert(cursor_cell->type == "$mux");
+					b_sig.append(cursor_cell->getPort("\\A"));
+					s_sig.append(module->LogicNot(NEW_ID, cursor_cell->getPort("\\S")));
+				}
+				remove_cells.insert(cursor_cell);
+			}
+
+			first_cell->setPort("\\B", b_sig);
+			first_cell->setPort("\\S", s_sig);
+			first_cell->setParam("\\S_WIDTH", GetSize(s_sig));
+			first_cell->setPort("\\Y", last_cell->getPort("\\Y"));
+
+			cursor += cases;
+		}
+	}
+
+	void cleanup()
+	{
+		for (auto cell : remove_cells)
+			module->remove(cell);
+
+		remove_cells.clear();
+		sig_chain_next.clear();
+		sig_chain_prev.clear();
+		chain_start_cells.clear();
+		candidate_cells.clear();
+	}
+
+	MuxpackWorker(Module *module) :
+			module(module), sigmap(module), mux_count(0), pmux_count(0), excl_db(module, sigmap)
+	{
+		make_sig_chain_next_prev();
+		find_chain_start_cells();
+
+		for (auto c : chain_start_cells) {
+			vector<Cell*> chain = create_chain(c);
+			process_chain(chain);
+		}
+
+		cleanup();
+	}
+};
+
+struct MuxpackPass : public Pass {
+	MuxpackPass() : Pass("muxpack", "$mux/$pmux cascades to $pmux") { }
+	void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    muxpack [selection]\n");
+		log("\n");
+		log("This pass converts cascaded chains of $pmux cells (e.g. those create from case\n");
+		log("constructs) and $mux cells (e.g. those created by if-else constructs) into\n");
+		log("$pmux cells.\n");
+		log("\n");
+		log("This optimisation is conservative --- it will only pack $mux or $pmux cells\n");
+		log("whose select lines are driven by '$eq' cells with other such cells if it can be\n");
+		log("certain that their select inputs are mutually exclusive.\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+	{
+		log_header(design, "Executing MUXPACK pass ($mux cell cascades to $pmux).\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		int mux_count = 0;
+		int pmux_count = 0;
+
+		for (auto module : design->selected_modules()) {
+			MuxpackWorker worker(module);
+			mux_count += worker.mux_count;
+			pmux_count += worker.pmux_count;
+		}
+
+		log("Converted %d (p)mux cells into %d pmux cells.\n", mux_count, pmux_count);
+	}
+} MuxpackPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/tests/various/muxpack.v b/tests/various/muxpack.v
new file mode 100644
index 000000000..33ece1f16
--- /dev/null
+++ b/tests/various/muxpack.v
@@ -0,0 +1,259 @@
+module mux_if_unbal_4_1 #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s == 0) o <= i[0*W+:W];
+    else if (s == 1) o <= i[1*W+:W];
+    else if (s == 2) o <= i[2*W+:W];
+    else if (s == 3) o <= i[3*W+:W];
+    else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3 #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 0) o <= i[0*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 2) o <= i[2*W+:W];
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+end
+endmodule
+
+module mux_if_unbal_5_3_invert #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s != 0) 
+	   	if (s != 1) 
+			if (s != 2)
+				if (s != 3)
+					if (s != 4) o <= i[4*W+:W];
+					else o <= i[0*W+:W];
+				else o <= i[3*W+:W];
+			else o <= i[2*W+:W];
+		else o <= i[1*W+:W];
+    else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3_width_mismatch #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 0) o <= i[0*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 2) o[W-2:0] <= i[2*W+:W-1];
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+end
+endmodule
+
+module mux_if_unbal_4_1_missing #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    if (s == 0) o <= i[0*W+:W];
+//    else if (s == 1) o <= i[1*W+:W];
+//    else if (s == 2) o <= i[2*W+:W];
+    else if (s == 3) o <= i[3*W+:W];
+    else o <= {W{1'bx}};
+end
+endmodule
+
+module mux_if_unbal_5_3_order #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 2) o <= i[2*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+    if (s == 0) o <= i[0*W+:W];
+end
+endmodule
+
+module mux_if_unbal_4_1_nonexcl #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s == 0) o <= i[0*W+:W];
+    else if (s == 1) o <= i[1*W+:W];
+    else if (s == 2) o <= i[2*W+:W];
+    else if (s == 3) o <= i[3*W+:W];
+	else if (s == 0) o <= {W{1'b0}};
+    else o <= {W{1'bx}};
+endmodule
+
+module mux_if_unbal_5_3_nonexcl #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    if (s == 0) o <= i[0*W+:W];
+    if (s == 1) o <= i[1*W+:W];
+    if (s == 2) o <= i[2*W+:W];
+    if (s == 3) o <= i[3*W+:W];
+    if (s == 4) o <= i[4*W+:W];
+	if (s == 0) o <= i[2*W+:W];
+end
+endmodule
+
+module mux_case_unbal_8_7#(parameter N=8, parameter W=7) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @* begin
+    o <= {W{1'bx}};
+    case (s)
+    0: o <= i[0*W+:W];
+    default:
+        case (s)
+        1: o <= i[1*W+:W];
+        2: o <= i[2*W+:W];
+        default:
+            case (s)
+            3: o <= i[3*W+:W];
+            4: o <= i[4*W+:W];
+            5: o <= i[5*W+:W];
+            default:
+                case (s)
+                    6: o <= i[6*W+:W];
+                    default: o <= i[7*W+:W];
+                endcase
+            endcase
+        endcase
+    endcase
+end
+endmodule
+
+module mux_if_bal_8_2 #(parameter N=8, parameter W=2) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[0*W+:W];
+      else
+       o <= i[1*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[2*W+:W];
+      else
+       o <= i[3*W+:W];
+    else
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[4*W+:W];
+      else
+       o <= i[5*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[6*W+:W];
+      else
+       o <= i[7*W+:W];
+endmodule
+
+module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o);
+always @*
+    if (s[0] == 1'b0)
+     if (s[1] == 1'b0)
+      if (s[2] == 1'b0)
+       o <= i[0*W+:W];
+      else
+       o <= i[1*W+:W];
+     else
+      if (s[2] == 1'b0)
+       o <= i[2*W+:W];
+      else
+       o <= i[3*W+:W];
+    else
+     o <= i[4*W+:W];
+endmodule
+
+module cliffordwolf_nonexclusive_select (
+        input wire x, y, z,
+        input wire a, b, c, d,
+        output reg o
+);
+        always @* begin
+                o = a;
+                if (x) o = b;
+                if (y) o = c;
+                if (z) o = d;
+        end
+endmodule
+
+module cliffordwolf_freduce (
+        input wire [1:0] s,
+        input wire a, b, c, d,
+        output reg [3:0] o
+);
+        always @* begin
+                o = {4{a}};
+                if (s == 0) o = {3{b}};
+                if (s == 1) o = {2{c}};
+                if (s == 2) o = d;
+        end
+endmodule
+
+module case_nonexclusive_select (
+        input wire [1:0] x, y,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0: o = b;
+                2: o = b;
+                1: o = c;
+                default: begin
+                    o = a;
+                    if (y == 0) o = d;
+                    if (y == 1) o = e;
+                end
+        endcase
+        end
+endmodule
+
+module case_nonoverlap (
+        input wire [2:0] x,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0, 2: o = b; // Creates $reduce_or
+                1: o = c;
+                default:
+                    case (x)
+                        3: o = d; 4: o = d; // Creates $reduce_or
+                        5: o = e;
+                        default: o = 1'b0;
+                    endcase
+        endcase
+        end
+endmodule
+
+module case_overlap (
+        input wire [2:0] x,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0, 2: o = b; // Creates $reduce_or
+                1: o = c;
+                default:
+                    case (x)
+                        0: o = 1'b1; // OVERLAP!
+                        3, 4: o = d; // Creates $reduce_or
+                        5: o = e;
+                        default: o = 1'b0;
+                    endcase
+        endcase
+        end
+endmodule
+
+module case_overlap2 (
+        input wire [2:0] x,
+        input wire a, b, c, d, e,
+        output reg o
+);
+        always @* begin
+            case (x)
+                0: o = b; 2: o = b; // Creates $reduce_or
+                1: o = c;
+                default:
+                    case (x)
+                        0: o = d; 2: o = d; // Creates $reduce_or
+                        3: o = d; 4: o = d; // Creates $reduce_or
+                        5: o = e;
+                        default: o = 1'b0;
+                    endcase
+        endcase
+        end
+endmodule
diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys
new file mode 100644
index 000000000..af23fcec8
--- /dev/null
+++ b/tests/various/muxpack.ys
@@ -0,0 +1,268 @@
+read_verilog muxpack.v
+design -save read
+
+hierarchy -top mux_if_unbal_4_1
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+# TODO: Currently ExclusiveDatabase only analyses $eq cells
+#design -load read
+#hierarchy -top mux_if_unbal_5_3_invert
+#prep
+#design -save gold
+#muxpack
+#opt
+#stat
+#select -assert-count 0 t:$mux
+#select -assert-count 1 t:$pmux
+#design -stash gate
+#design -import gold -as gold
+#design -import gate -as gate
+#miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3_width_mismatch
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_4_1_missing
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3_order
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_4_1_nonexcl
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_unbal_5_3_nonexcl
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_case_unbal_8_7
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_bal_8_2
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 7 t:$mux
+select -assert-count 0 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top mux_if_bal_5_1
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 4 t:$mux
+select -assert-count 0 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top cliffordwolf_nonexclusive_select
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 3 t:$mux
+select -assert-count 0 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+#design -load read
+#hierarchy -top cliffordwolf_freduce
+#prep
+#design -save gold
+#proc; opt; freduce; opt
+#show
+#muxpack
+#opt
+#stat
+#select -assert-count 0 t:$mux
+#select -assert-count 1 t:$pmux
+#design -stash gate
+#design -import gold -as gold
+#design -import gate -as gate
+#miter -equiv -flatten -make_assert -make_outputs gold gate miter
+#sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_nonexclusive_select
+prep
+design -save gold
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_nonoverlap
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 1 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_overlap
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load read
+hierarchy -top case_overlap2
+#prep # Do not prep otherwise $pmux's overlapping entry will get removed
+proc
+design -save gold
+opt -fast -mux_undef
+select -assert-count 2 t:$pmux
+muxpack
+opt
+stat
+select -assert-count 0 t:$mux
+select -assert-count 2 t:$pmux
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter