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
|
# Regression test for #3467
read_verilog <<EOT
module bit_buf (
input wire bit_in,
output wire bit_out
);
assign bit_out = bit_in;
endmodule
module top (
input wire [3:0] data_in,
output wire [3:0] data_out
);
wire [3:0] data [0:4];
assign data[0] = data_in;
assign data_out = data[4];
genvar i;
generate
for (i=0; i<=3; i=i+1) begin
bit_buf bit_buf_instance[3:0] (
.bit_in(data[i]),
.bit_out(data[i + 1])
);
end
endgenerate
endmodule
module top2 (
input wire [3:0] data_in,
output wire [3:0] data_out
);
assign data_out = data_in;
endmodule
EOT
hierarchy
proc
miter -equiv -make_assert -flatten top top2 miter
sat -prove-asserts -verify miter
|
