read_verilog <<EOT
module top(input a, output [3:0] y);
assign y[0] = a^1'b0;
assign y[1] = 1'b1^a;
assign y[2] = a~^1'b0;
assign y[3] = 1'b1^~a;
endmodule
EOT
design -save read
select -assert-count 2 t:$xor
select -assert-count 2 t:$xnor

equiv_opt opt_expr
design -load postopt
select -assert-none t:$xor
select -assert-none t:$xnor
select -assert-count 2 t:$not


design -load read
simplemap
equiv_opt opt_expr
design -load postopt
select -assert-none t:$_XOR_
select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
select -assert-count 3 t:$_NOT_


design -reset
read_verilog -icells <<EOT
module top(input a, output [1:0] y);
$_XNOR_ u0(.A(a), .B(1'b0), .Y(y[0]));
$_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
endmodule
EOT
select -assert-count 2 t:$_XNOR_
equiv_opt opt_expr
design -load postopt
select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
select -assert-count 1 t:$_NOT_


design -reset
read_verilog <<EOT
module top(input a, output [1:0] w, x, y, z);
assign w = a^1'b0;
assign x = a^1'b1;
assign y = a~^1'b0;
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