Merge pull request #1994 from YosysHQ/eddie/fix_bug1758

opt_expr: improve single-bit $and/$or/$xor/$xnor cells; gate cells too

passes/opt/opt_expr.cc

@@ -132,7 +132,7 @@ void replace_cell(SigMap &assign_map, RTLIL::Module *module, RTLIL::Cell *cell,
 	did_something = true;
 }
 
-bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutative, SigMap &sigmap)
+bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutative, SigMap &sigmap, bool keepdc)
 {
 	IdString b_name = cell->hasPort(ID::B) ? ID::B : ID::A;
 
@@ -156,20 +156,36 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ
 		int group_idx = GRP_DYN;
 		RTLIL::SigBit bit_a = bits_a[i], bit_b = bits_b[i];
 
-		if (cell->type == ID($or) && (bit_a == RTLIL::State::S1 || bit_b == RTLIL::State::S1))
+		if (cell->type == ID($or)) {
-			bit_a = bit_b = RTLIL::State::S1;
+			if (bit_a == RTLIL::State::S1 || bit_b == RTLIL::State::S1)
+				bit_a = bit_b = RTLIL::State::S1;
+		}
+		else if (cell->type == ID($and)) {
+			if (bit_a == RTLIL::State::S0 || bit_b == RTLIL::State::S0)
+				bit_a = bit_b = RTLIL::State::S0;
+		}
+		else if (!keepdc) {
+			if (cell->type == ID($xor)) {
+				if (bit_a == bit_b)
+					bit_a = bit_b = RTLIL::State::S0;
+			}
+			else if (cell->type == ID($xnor)) {
+				if (bit_a == bit_b)
+					bit_a = bit_b = RTLIL::State::S1; // For consistency with gate-level which does $xnor -> $_XOR_ + $_NOT_
+			}
+		}
 
-		if (cell->type == ID($and) && (bit_a == RTLIL::State::S0 || bit_b == RTLIL::State::S0))
+		bool def = (bit_a != State::Sx && bit_a != State::Sz && bit_b != State::Sx && bit_b != State::Sx);
-			bit_a = bit_b = RTLIL::State::S0;
+		if (def || !keepdc) {
-
+			if (bit_a.wire == NULL && bit_b.wire == NULL)
-		if (bit_a.wire == NULL && bit_b.wire == NULL)
+				group_idx = GRP_CONST_AB;
-			group_idx = GRP_CONST_AB;
+			else if (bit_a.wire == NULL)
-		else if (bit_a.wire == NULL)
+				group_idx = GRP_CONST_A;
-			group_idx = GRP_CONST_A;
+			else if (bit_b.wire == NULL && commutative)
-		else if (bit_b.wire == NULL && commutative)
+				group_idx = GRP_CONST_A, std::swap(bit_a, bit_b);
-			group_idx = GRP_CONST_A, std::swap(bit_a, bit_b);
+			else if (bit_b.wire == NULL)
-		else if (bit_b.wire == NULL)
+				group_idx = GRP_CONST_B;
-			group_idx = GRP_CONST_B;
+		}
 
 		grouped_bits[group_idx][std::pair<RTLIL::SigBit, RTLIL::SigBit>(bit_a, bit_b)].insert(bits_y[i]);
 	}
@@ -186,26 +202,77 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ
 		if (grouped_bits[i].empty())
 			continue;
 
-		RTLIL::Wire *new_y = module->addWire(NEW_ID, GetSize(grouped_bits[i]));
+		RTLIL::SigSpec new_y = module->addWire(NEW_ID, GetSize(grouped_bits[i]));
 		RTLIL::SigSpec new_a, new_b;
 		RTLIL::SigSig new_conn;
 
 		for (auto &it : grouped_bits[i]) {
 			for (auto &bit : it.second) {
 				new_conn.first.append(bit);
-				new_conn.second.append(RTLIL::SigBit(new_y, new_a.size()));
+				new_conn.second.append(new_y[new_a.size()]);
 			}
 			new_a.append(it.first.first);
 			new_b.append(it.first.second);
 		}
 
 		if (cell->type.in(ID($and), ID($or)) && i == GRP_CONST_A) {
+			if (!keepdc) {
+				if (cell->type == ID($and))
+					new_a.replace(dict<SigBit,SigBit>{{State::Sx, State::S0}, {State::Sz, State::S0}}, &new_b);
+				else if (cell->type == ID($or))
+					new_a.replace(dict<SigBit,SigBit>{{State::Sx, State::S1}, {State::Sz, State::S1}}, &new_b);
+				else log_abort();
+			}
 			log_debug("  Direct Connection: %s (%s with %s)\n", log_signal(new_b), log_id(cell->type), log_signal(new_a));
 			module->connect(new_y, new_b);
 			module->connect(new_conn);
 			continue;
 		}
 
+		if (cell->type.in(ID($xor), ID($xnor)) && i == GRP_CONST_A) {
+			SigSpec undef_a, undef_y, undef_b;
+			SigSpec def_y, def_a, def_b;
+			for (int i = 0; i < GetSize(new_y); i++) {
+				bool undef = new_a[i] == State::Sx || new_a[i] == State::Sz;
+				if (!keepdc && (undef || new_a[i] == new_b[i])) {
+					undef_a.append(new_a[i]);
+					if (cell->type == ID($xor))
+						undef_b.append(State::S0);
+					// For consistency since simplemap does $xnor -> $_XOR_ + $_NOT_
+					else if (cell->type == ID($xnor))
+						undef_b.append(State::S1);
+					else log_abort();
+					undef_y.append(new_y[i]);
+				}
+				else if (new_a[i] == State::S0 || new_a[i] == State::S1) {
+					undef_a.append(new_a[i]);
+					if (cell->type == ID($xor))
+						undef_b.append(new_a[i] == State::S1 ? module->Not(NEW_ID, new_b[i]).as_bit() : new_b[i]);
+					else if (cell->type == ID($xnor))
+						undef_b.append(new_a[i] == State::S1 ? new_b[i] : module->Not(NEW_ID, new_b[i]).as_bit());
+					else log_abort();
+					undef_y.append(new_y[i]);
+				}
+				else {
+					def_a.append(new_a[i]);
+					def_b.append(new_b[i]);
+					def_y.append(new_y[i]);
+				}
+			}
+			if (!undef_y.empty()) {
+				log_debug("  Direct Connection: %s (%s with %s)\n", log_signal(undef_b), log_id(cell->type), log_signal(undef_a));
+				module->connect(undef_y, undef_b);
+				if (def_y.empty()) {
+					module->connect(new_conn);
+					continue;
+				}
+			}
+			new_a = std::move(def_a);
+			new_b = std::move(def_b);
+			new_y = std::move(def_y);
+		}
+
+
 		RTLIL::Cell *c = module->addCell(NEW_ID, cell->type);
 
 		c->setPort(ID::A, new_a);
@@ -219,7 +286,7 @@ bool group_cell_inputs(RTLIL::Module *module, RTLIL::Cell *cell, bool commutativ
 		}
 
 		c->setPort(ID::Y, new_y);
-		c->parameters[ID::Y_WIDTH] = new_y->width;
+		c->parameters[ID::Y_WIDTH] = GetSize(new_y);
 		c->check();
 
 		module->connect(new_conn);
@@ -476,13 +543,13 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 				}
 			}
 
-			if (detect_const_and && (found_zero || found_inv)) {
+			if (detect_const_and && (found_zero || found_inv || (found_undef && consume_x))) {
 				cover("opt.opt_expr.const_and");
 				replace_cell(assign_map, module, cell, "const_and", ID::Y, RTLIL::State::S0);
 				goto next_cell;
 			}
 
-			if (detect_const_or && (found_one || found_inv)) {
+			if (detect_const_or && (found_one || found_inv || (found_undef && consume_x))) {
 				cover("opt.opt_expr.const_or");
 				replace_cell(assign_map, module, cell, "const_or", ID::Y, RTLIL::State::S1);
 				goto next_cell;
@@ -499,6 +566,22 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 		{
 			SigBit sig_a = assign_map(cell->getPort(ID::A));
 			SigBit sig_b = assign_map(cell->getPort(ID::B));
+			if (!keepdc && (sig_a == sig_b || sig_a == State::Sx || sig_a == State::Sz || sig_b == State::Sx || sig_b == State::Sz)) {
+				if (cell->type.in(ID($xor), ID($_XOR_))) {
+					cover("opt.opt_expr.const_xor");
+					replace_cell(assign_map, module, cell, "const_xor", ID::Y, RTLIL::State::S0);
+					goto next_cell;
+				}
+				if (cell->type.in(ID($xnor), ID($_XNOR_))) {
+					cover("opt.opt_expr.const_xnor");
+					// For consistency since simplemap does $xnor -> $_XOR_ + $_NOT_
+					int width = cell->getParam(ID::Y_WIDTH).as_int();
+					replace_cell(assign_map, module, cell, "const_xnor", ID::Y, SigSpec(RTLIL::State::S1, width));
+					goto next_cell;
+				}
+				log_abort();
+			}
+
 			if (!sig_a.wire)
 				std::swap(sig_a, sig_b);
 			if (sig_b == State::S0 || sig_b == State::S1) {
@@ -550,7 +633,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 		if (do_fine)
 		{
 			if (cell->type.in(ID($not), ID($pos), ID($and), ID($or), ID($xor), ID($xnor)))
-				if (group_cell_inputs(module, cell, true, assign_map))
+				if (group_cell_inputs(module, cell, true, assign_map, keepdc))
 					goto next_cell;
 
 			if (cell->type.in(ID($logic_not), ID($logic_and), ID($logic_or), ID($reduce_or), ID($reduce_and), ID($reduce_bool)))
@@ -904,8 +987,10 @@ skip_fine_alu:
 			if (input.match("01")) ACTION_DO_Y(1);
 			if (input.match("10")) ACTION_DO_Y(1);
 			if (input.match("11")) ACTION_DO_Y(0);
-			if (input.match(" *")) ACTION_DO_Y(x);
+			if (consume_x) {
-			if (input.match("* ")) ACTION_DO_Y(x);
+				if (input.match(" *")) ACTION_DO_Y(0);
+				if (input.match("* ")) ACTION_DO_Y(0);
+			}
 		}
 
 		if (cell->type == ID($_MUX_)) {
@@ -1088,7 +1173,7 @@ skip_fine_alu:
 			goto next_cell;
 		}
 
-		if (!keepdc)
+		if (consume_x)
 		{
 			bool identity_wrt_a = false;
 			bool identity_wrt_b = false;
@@ -1980,11 +2065,12 @@ struct OptExprPass : public Pass {
 			do {
 				do {
 					did_something = false;
-					replace_const_cells(design, module, false, mux_undef, mux_bool, do_fine, keepdc, clkinv);
+					replace_const_cells(design, module, false /* consume_x */, mux_undef, mux_bool, do_fine, keepdc, clkinv);
 					if (did_something)
 						design->scratchpad_set_bool("opt.did_something", true);
 				} while (did_something);
-				replace_const_cells(design, module, true, mux_undef, mux_bool, do_fine, keepdc, clkinv);
+				if (!keepdc)
+					replace_const_cells(design, module, true /* consume_x */, mux_undef, mux_bool, do_fine, keepdc, clkinv);
 				if (did_something)
 					design->scratchpad_set_bool("opt.did_something", true);
 			} while (did_something);

tests/fsm/generate.py

@@ -36,9 +36,11 @@ parser.add_argument('-S', '--seed',  type = int, help = 'seed for PRNG')
 parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate')
 args = parser.parse_args()
 
-if args.seed is not None:
+seed = args.seed
-    print("PRNG seed: %d" % args.seed)
+if seed is None:
-    random.seed(args.seed)
+    seed = random.randrange(sys.maxsize)
+print("PRNG seed: %d" % seed)
+random.seed(seed)
 
 for idx in range(args.count):
     with open('temp/uut_%05d.v' % idx, 'w') as f:

tests/opt/bug1758.ys

@@ -0,0 +1,21 @@
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx | i;
+endmodule
+EOT
+copy gold coarse
+copy gold fine
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter
+sat -verify -prove-asserts -show-ports miter
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2

tests/opt/opt_expr_alu.ys

@@ -59,9 +59,8 @@ EOT
 alumacc
 equiv_opt -assert opt_expr -fine
 design -load postopt
-select -assert-count 1 t:$pos
 select -assert-count 1 t:$not
-select -assert-none t:$pos t:$not %% t:* %D
+select -assert-none t:$not %% t:* %D
 
 
 design -reset

tests/opt/opt_expr_and.ys

@@ -0,0 +1,85 @@
+# Single-bit $and
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx & i;
+endmodule
+EOT
+select -assert-count 1 t:$and
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $and
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} & {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$and
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -fine -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 2 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4

tests/opt/opt_expr_consumex.ys

@@ -0,0 +1,35 @@
+read_verilog <<EOT
+module top(input a, b, output o);
+wire tmp;
+assign o = tmp | 1'bx;
+assign tmp = a & 1'b0;
+endmodule
+EOT
+design -save read
+select -assert-count 1 t:$and
+select -assert-count 1 t:$or
+
+
+opt_expr
+select -assert-none t:$and t:$or
+sat -verify -enable_undef -prove o 1'bx
+
+
+design -load read
+opt_expr -keepdc
+select -assert-none t:$and t:$or
+sat -verify -enable_undef -prove o 1'bx
+
+
+design -load read
+simplemap
+opt_expr -keepdc
+select -assert-none t:$_AND_ t:$_OR_
+sat -verify -enable_undef -prove o 1'bx
+
+
+design -load read
+simplemap
+opt_expr -keepdc
+select -assert-none t:$_AND_ t:$_OR_
+sat -verify -enable_undef -prove o 1'bx

tests/opt/opt_expr_or.ys

@@ -0,0 +1,85 @@
+# Single-bit $or
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx | i;
+endmodule
+EOT
+select -assert-count 1 t:$or
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $or
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} | {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$or
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -fine -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 2 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4

tests/opt/opt_expr_xnor.ys

@@ -0,0 +1,131 @@
+# Single-bit $xnor
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx ~^ i;
+endmodule
+EOT
+select -assert-count 1 t:$xnor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none t:$xnor
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:t$_XNOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 t:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $xnor
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ~^ {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$xnor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-none t:$xnor
+
+cd fine
+simplemap
+opt_expr
+select -assert-none t:$_XNOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc -fine
+select -assert-count 1 t:$xnor
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 0 c:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Single-bit $xnor extension
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [1:0] o, p, q);
+assign o =  i ~^ i;
+assign p =  1'b0 ~^ i;
+assign q =  1'b1 ~^ i;
+endmodule
+EOT
+select -assert-count 3 t:$xnor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-none t:$xnor
+
+cd fine
+simplemap
+opt_expr
+select -assert-none t:$_XNOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc -fine
+select -assert-count 1 t:$xnor
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 0 c:$_XNOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4

tests/opt/opt_expr_xor.ys

@@ -50,3 +50,91 @@ assign z = a~^1'b1;
 endmodule
 EOT
 equiv_opt opt_expr
+
+
+# Single-bit $xor
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output o);
+assign o = 1'bx ^ i;
+endmodule
+EOT
+select -assert-count 1 t:$xor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr
+select -assert-none c:*
+
+cd fine
+simplemap
+opt_expr
+select -assert-none c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 1 c:*
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4
+
+
+# Multi-bit $xor
+design -reset
+read_verilog -noopt <<EOT
+module gold(input i, output [6:0] o);
+assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ^ {7{i}};
+endmodule
+EOT
+select -assert-count 1 t:$xor
+copy gold coarse
+copy gold fine
+copy gold coarse_keepdc
+copy gold fine_keepdc
+
+cd coarse
+opt_expr -fine
+select -assert-count 0 t:$xor
+
+cd fine
+simplemap
+opt_expr
+select -assert-none t:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
+sat -verify -prove-asserts -show-ports -enable_undef miter
+miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
+sat -verify -prove-asserts -show-ports -enable_undef miter2
+
+cd coarse_keepdc
+opt_expr -keepdc -fine
+select -assert-count 1 t:$xor
+
+cd fine_keepdc
+simplemap
+opt_expr -keepdc
+select -assert-count 3 t:$_XOR_
+
+cd
+miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
+sat -verify -prove-asserts -show-ports -enable_undef miter3
+miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
+sat -verify -prove-asserts -show-ports -enable_undef miter4