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
|
read_verilog -sv <<EOF
typedef logic T;
typedef T [3:0] S;
EOF
read_verilog -sv <<EOF
module example;
// S and T refer to the definitions from the first file
T t;
S s;
always @* begin
assert ($bits(t) == 1);
assert ($bits(s) == 4);
end
endmodule
typedef byte T;
typedef T S;
module top;
// S and T refer to the most recent overrides
T t;
S s;
always @* begin
assert ($bits(t) == 8);
assert ($bits(s) == 8);
end
example e();
endmodule
EOF
hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all
|
