2 module top(input a, output [3:0] y);
10 select -assert-count 2 t:$xor
11 select -assert-count 2 t:$xnor
15 select -assert-none t:$xor
16 select -assert-none t:$xnor
17 select -assert-count 2 t:$not
24 select -assert-none t:$_XOR_
25 select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
26 select -assert-count 3 t:$_NOT_
30 read_verilog -icells <<EOT
31 module top(input a, output [1:0] y);
32 $_XNOR_ u0(.A(a), .B(1'b0), .Y(y[0]));
33 $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
36 select -assert-count 2 t:$_XNOR_
39 select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
40 select -assert-count 1 t:$_NOT_
45 module top(input a, output [1:0] w, x, y, z);
57 read_verilog -noopt <<EOT
58 module gold(input i, output o);
62 select -assert-count 1 t:$xor
65 copy gold coarse_keepdc
70 select -assert-none c:*
75 select -assert-none c:*
78 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
79 sat -verify -prove-asserts -show-ports -enable_undef miter
80 miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
81 sat -verify -prove-asserts -show-ports -enable_undef miter2
85 select -assert-count 1 c:*
90 select -assert-count 1 c:*
93 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
94 sat -verify -prove-asserts -show-ports -enable_undef miter3
95 miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
96 sat -verify -prove-asserts -show-ports -enable_undef miter4
101 read_verilog -noopt <<EOT
102 module gold(input i, output [6:0] o);
103 assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ^ {7{i}};
106 select -assert-count 1 t:$xor
109 copy gold coarse_keepdc
110 copy gold fine_keepdc
114 select -assert-count 0 t:$xor
119 select -assert-none t:$_XOR_
122 miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
123 sat -verify -prove-asserts -show-ports -enable_undef miter
124 miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
125 sat -verify -prove-asserts -show-ports -enable_undef miter2
128 opt_expr -keepdc -fine
129 select -assert-count 1 t:$xor
134 select -assert-count 3 t:$_XOR_
137 miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
138 sat -verify -prove-asserts -show-ports -enable_undef miter3
139 miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
140 sat -verify -prove-asserts -show-ports -enable_undef miter4