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
|
# Test "casez to if/elif/else conversion" in backend
read_verilog <<EOT
module top(a, b, c, out);
input wire a, b, c;
output reg [3:0] out;
always @(*) begin
casez ({c, b, a})
3'b??1: begin
out = 0;
end
3'b?1?: begin
out = 1;
end
3'b1??: begin
out = 2;
end
default: begin
out = 3;
end
endcase
end
endmodule
EOT
write_verilog roundtrip_proc_1.v
design -stash gold
read_verilog roundtrip_proc_1.v
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
prep
miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
sat -prove-asserts -verify
design -reset
read_verilog <<EOT
module top(a, b, c, out);
input wire a, b, c;
output reg [3:0] out;
always @(*) begin
out <= 0;
if (a) begin
if (b)
out <= 1;
end else begin
if (c)
out <= 2;
else
out <= 3;
end
end
endmodule
EOT
proc_clean
write_verilog roundtrip_proc_2.v
design -stash gold
read_verilog roundtrip_proc_2.v
design -stash gate
design -copy-from gold -as gold top
design -copy-from gate -as gate top
prep
miter -equiv -flatten -make_assert gold gate miter
hierarchy -top miter
sat -prove-asserts -verify
|
