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
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
+write_verilog -noexpr -norename
+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