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
167
168
169
170
171
172
173
174
175
176
177
|
design -reset
read_verilog <<EOT
module test(input a, output [7:0] y);
assign y = a * 0;
endmodule
EOT
equiv_opt -assert opt_expr -fine
design -load postopt
# The multiplication by zero should be replaced with constant zero
select -assert-count 0 t:$mul
## opt.opt_expr.mul_shift
design -reset
read_verilog <<EOT
module test(input [7:0] a, output [15:0] y, output [15:0] z);
assign y = a * 8; // Multiply by 2^3 (power of 2)
assign z = 8 * a;
endmodule
EOT
equiv_opt -assert opt_expr -fine
design -load postopt
# The multiplication by 8 should be replaced with a shift by const
select -assert-count 0 t:$mul
# No shift operator cells should be present
select -assert-count 0 t:$shl
design -reset
read_verilog <<EOT
module test(input [7:0] a, output [7:0] y);
assign y = a / 4; // Division by 2^2 (power of 2)
endmodule
EOT
equiv_opt -assert opt_expr -fine
design -load postopt
# The division by 4 should be replaced with a shift by const
select -assert-count 0 t:$div
design -reset
read_verilog <<EOT
module test(input [7:0] a, output [7:0] y);
assign y = a / 0; // Division by zero should be replaced with x
endmodule
EOT
opt_expr -fine
# The division by zero should be removed
select -assert-count 0 t:$div
# No cells should be left as it's replaced with constant undef
select -assert-none t:*
design -reset
read_verilog <<EOT
module test(input s, output y);
assign y = s ? 1'b1 : 1'b0; // This is equivalent to just 's'
endmodule
EOT
equiv_opt -assert opt_expr -fine -mux_bool
design -load postopt
# The mux should be removed completely
select -assert-count 0 t:$mux
# No additional cells needed - direct connection
select -assert-none t:*
design -reset
read_verilog <<EOT
module test(input s, output y);
assign y = s ? 1'b0 : 1'b1; // This is equivalent to '!s'
endmodule
EOT
equiv_opt -assert opt_expr -fine -mux_bool
design -load postopt
# The mux should be converted to a not gate
select -assert-count 0 t:$mux
select -assert-count 1 t:$not
design -reset
read_verilog <<EOT
module test(input [3:0] a, input [3:0] b, output y);
assign y = (a == b); // Test equality optimization
endmodule
EOT
equiv_opt -assert opt_expr -fine
design -load postopt
# Check for optimization of equality comparison
select -assert-count 1 t:$eq
# opt.opt_expr.eqneq.*
design -reset
read_verilog -noopt <<EOT
module test(output y1, y2, y3, y4);
// Compare two constants that are guaranteed to be different
assign y1 = 2'b01 == 2'b10;
assign y2 = 2'b01 != 2'b10;
assign y3 = 2'b01 !== 2'b10;
assign y4 = 2'b01 === 2'b10;
endmodule
EOT
equiv_opt -assert opt_expr
select -assert-count 1 t:$eq
design -load postopt
# The comparison of different constants should be replaced with constant 0
select -assert-count 0 t:$eq
# No other cells should be present (just the constant driver)
select -assert-none t:*
# opt.opt_expr.invert.double
design -reset
read_verilog -noopt <<EOT
module test(input a, output y);
// Double negation should be optimized away
wire not_a;
assign not_a = ~a;
assign y = ~not_a;
endmodule
EOT
equiv_opt -assert opt_expr
select -assert-count 2 t:$not
design -load postopt
# Both NOT gates should be eliminated
opt_clean -purge
select -assert-count 0 t:$not
# No other cells should be present
select -assert-none t:*
# opt.opt_expr.reduce_xnor_not
design -reset
read_verilog -noopt <<EOT
module test(input a, output y);
assign y = ~^a; // XNOR reduction of a single bit
endmodule
EOT
equiv_opt -assert opt_expr -full
design -load postopt
select -assert-count 0 t:$reduce_xnor
select -assert-count 1 t:$not
## opt.opt_expr.mod_mask
design -reset
read_verilog -noopt <<EOT
module test(input [7:0] a, output [7:0] y);
assign y = a % 8; // Modulo by power of 2
endmodule
EOT
select -assert-count 1 t:$mod
equiv_opt -assert opt_expr -full
design -load postopt
select -assert-count 0 t:$mod
select -assert-count 0 t:$and
## opt.opt_expr.eqneq.empty (indirectly)
design -reset
read_verilog -noopt <<EOT
module test(output [7:0] y1);
assign y1 = 7'b1 == 7'b1;
endmodule
EOT
select -assert-count 1 t:$eq
equiv_opt -assert opt_expr -full
design -load postopt
select -assert-count 0 t:$eq
|
