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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
read_verilog <<EOT
module top(A, B, X, Y);
input [7:0] A, B;
output [7:0] X, Y;
assign X = A + B;
assign Y = A + B;
endmodule
EOT
# Most basic case
# Binary
select -assert-count 2 t:$add
equiv_opt -assert opt_merge
design -load postopt
select -assert-count 1 t:$add
design -reset
read_verilog <<EOT
module top(A, B, C, X, Y);
input [7:0] A, B, C;
output [7:0] X, Y;
assign X = A + B;
assign Y = A + C; // <- look here
endmodule
EOT
# Reject on a different input
select -assert-count 2 t:$add
opt_merge
select -assert-count 2 t:$add
design -reset
read_verilog <<EOT
module top(A, X, Y);
input [7:0] A;
output X, Y;
assign X = ^A;
assign Y = ^A;
endmodule
EOT
# Unary
select -assert-count 2 t:$reduce_xor
dump
opt_merge
select -assert-count 1 t:$reduce_xor
design -reset
read_verilog -icells <<EOT
module top(A, B, X, Y);
input [7:0] A, B;
output X, Y;
\$reduce_xor #(
.A_SIGNED(32'd0),
.A_WIDTH(32'd16),
.Y_WIDTH(32'd1),
) one (
.A({A, B}), // <- look here
.Y(X)
);
\$reduce_xor #(
.A_SIGNED(32'd0),
.A_WIDTH(32'd16),
.Y_WIDTH(32'd1),
) other (
.A({B, A}), // <- look here
.Y(Y)
);
endmodule
EOT
# Unary is sorted
opt_expr
select -assert-count 2 t:$reduce_xor
equiv_opt -assert opt_merge
design -load postopt
select -assert-count 1 t:$reduce_xor
design -reset
read_verilog -icells <<EOT
module top(A, B, X, Y);
input [7:0] A, B;
output X, Y;
\$reduce_or #(
.A_SIGNED(32'd0),
.A_WIDTH(32'd24),
.Y_WIDTH(32'd1),
) one (
.A({A, B, B}), // <- look here
.Y(X)
);
\$reduce_or #(
.A_SIGNED(32'd0),
.A_WIDTH(32'd24),
.Y_WIDTH(32'd1),
) other (
.A({A, A, B}), // <- look here
.Y(Y)
);
endmodule
EOT
# Unary is unified when valid
opt_expr
select -assert-count 2 t:$reduce_or
equiv_opt -assert opt_merge
design -load postopt
select -assert-count 1 t:$reduce_or
design -reset
read_verilog -icells <<EOT
module top(A, B, X, Y);
input [7:0] A, B;
output X, Y;
\$reduce_xor #(
.A_SIGNED(32'd0),
.A_WIDTH(32'd24),
.Y_WIDTH(32'd1),
) one (
.A({A, B, B}), // <- look here
.Y(X)
);
\$reduce_xor #(
.A_SIGNED(32'd0),
.A_WIDTH(32'd24),
.Y_WIDTH(32'd1),
) other (
.A({A, A, B}), // <- look here
.Y(Y)
);
endmodule
EOT
# Unary isn't unified when that would be invalid
opt_expr
select -assert-count 2 t:$reduce_xor
equiv_opt -assert opt_merge
design -load postopt
select -assert-count 2 t:$reduce_xor
# TODO pmux
design -reset
read_verilog <<EOT
module top(A, B, X, Y);
input [7:0] A, B;
output X, Y;
assign X = A > B;
assign Y = A > B;
endmodule
EOT
# Exercise the general case in hash_cell_inputs - accept
opt_expr
select -assert-count 2 t:$gt
equiv_opt -assert opt_merge
design -load postopt
select -assert-count 1 t:$gt
design -reset
read_verilog <<EOT
module top(A, B, C, X, Y);
input [7:0] A, B, C;
output X, Y;
assign X = A > B;
assign Y = A > C; // <- look here
endmodule
EOT
# Exercise the general case in hash_cell_inputs - reject
opt_expr
select -assert-count 2 t:$gt
opt_merge
select -assert-count 2 t:$gt
|
