1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
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 -assert 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 -assert opt_expr
design -load postopt
select -assert-none t:$_XOR_
select -assert-none t:$_XNOR_
select -assert-count 2 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 -assert opt_expr
design -load postopt
select -assert-none t:$_XNOR_
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 -assert 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
|
