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
|
vunit i_avm_cache(avm_cache(synthesis))
{
-- set all declarations to run on clk_i
default clock is rising_edge(clk_i);
-- Additional signals used during formal verification
signal f_s_rd_burstcount : integer;
signal f_m_rd_burstcount : integer;
p_s_rd_burstcount : process (clk_i)
begin
if rising_edge(clk_i) then
if s_avm_readdatavalid_o then
f_s_rd_burstcount <= f_s_rd_burstcount - 1;
end if;
if s_avm_read_i and not s_avm_waitrequest_o then
f_s_rd_burstcount <= to_integer(s_avm_burstcount_i);
end if;
if rst_i then
f_s_rd_burstcount <= 0;
end if;
end if;
end process p_s_rd_burstcount;
p_m_rd_burstcount : process (clk_i)
begin
if rising_edge(clk_i) then
if m_avm_readdatavalid_i then
f_m_rd_burstcount <= f_m_rd_burstcount - 1;
end if;
if m_avm_read_o and not m_avm_waitrequest_i then
f_m_rd_burstcount <= to_integer(m_avm_burstcount_o);
end if;
if rst_i then
f_m_rd_burstcount <= 0;
end if;
end if;
end process p_m_rd_burstcount;
signal f_s_written : std_logic := '0';
signal f_s_data : std_logic_vector(G_DATA_SIZE-1 downto 0);
signal f_s_read : std_logic := '0';
signal f_m_written : std_logic := '0';
signal f_m_data : std_logic_vector(G_DATA_SIZE-1 downto 0);
signal f_m_read : std_logic := '0';
signal f_addr : std_logic_vector(G_ADDRESS_SIZE-1 downto 0);
attribute anyconst : boolean;
attribute anyconst of f_addr : signal is true;
p_s_write : process (clk_i)
begin
if rising_edge(clk_i) then
if s_avm_write_i and not s_avm_waitrequest_o then
if s_avm_address_i = f_addr then
f_s_data <= s_avm_writedata_i;
f_s_written <= '1';
end if;
end if;
end if;
end process p_s_write;
p_s_read : process (clk_i)
begin
if rising_edge(clk_i) then
if s_avm_read_i and not s_avm_waitrequest_o then
if s_avm_address_i = f_addr then
f_s_read <= '1';
end if;
end if;
if f_s_read = '1' and s_avm_readdatavalid_o = '1' then
f_s_read <= '0';
end if;
end if;
end process p_s_read;
p_m_write : process (clk_i)
begin
if rising_edge(clk_i) then
if m_avm_write_o and not m_avm_waitrequest_i then
if m_avm_address_o = f_addr then
f_m_data <= m_avm_writedata_o;
f_m_written <= '1';
end if;
end if;
end if;
end process p_m_write;
p_m_read : process (clk_i)
begin
if rising_edge(clk_i) then
if m_avm_read_o and not m_avm_waitrequest_i then
if m_avm_address_o = f_addr then
f_m_read <= '1';
end if;
end if;
if f_m_read = '1' and m_avm_readdatavalid_i = '1' then
f_m_read <= '0';
end if;
end if;
end process p_m_read;
f_slave : assert always f_s_written and f_s_read and s_avm_readdatavalid_o |-> s_avm_readdata_o = f_s_data;
f_master : assume always f_m_written and f_m_read and m_avm_readdatavalid_i |-> m_avm_readdata_i = f_m_data;
-----------------------------
-- ASSERTIONS ABOUT OUTPUTS
-----------------------------
-- Master must be empty after reset
f_master_after_reset_empty : assert always {rst_i} |=> not (m_avm_write_o or m_avm_read_o);
-- Master may not assert both write and read.
f_master_not_double: assert always rst_i or not (m_avm_write_o and m_avm_read_o);
-- Master must be stable until accepted
f_master_stable : assert always {(m_avm_write_o or m_avm_read_o) and m_avm_waitrequest_i and not rst_i} |=>
{stable(m_avm_write_o) and stable(m_avm_read_o) and stable(m_avm_address_o) and stable(m_avm_writedata_o) and
stable(m_avm_byteenable_o) and stable(m_avm_burstcount_o)};
f_master_burst_valid : assert always rst_i or not (m_avm_read_o and not m_avm_waitrequest_i and nor(m_avm_burstcount_o));
f_slave_burst_reset : assert always rst_i |=> {f_s_rd_burstcount = 0};
f_slave_burst_range : assert always rst_i or f_s_rd_burstcount >= 0;
f_slave_burst_block : assert always rst_i or f_s_rd_burstcount = 0 or s_avm_waitrequest_o or (f_s_rd_burstcount = 1 and s_avm_readdatavalid_o = '1');
f_slave_no_data : assert always rst_i or not (f_s_rd_burstcount = 0 and s_avm_readdatavalid_o = '1');
-----------------------------
-- ASSUMPTIONS ABOUT INPUTS
-----------------------------
-- Require reset at startup.
f_reset : assume {rst_i};
-- Slave must be empty after reset
f_slave_after_reset_empty : assume always {rst_i} |=> not (s_avm_write_i or s_avm_read_i);
-- Slave may not assert both write and read.
f_slave_not_double: assume always not (s_avm_write_i and s_avm_read_i);
-- Slaves must be stable until accepted
f_slave_input_stable : assume always {(s_avm_write_i or s_avm_read_i) and s_avm_waitrequest_o and not rst_i} |=>
{stable(s_avm_write_i) and stable(s_avm_read_i) and stable(s_avm_address_i) and stable(s_avm_writedata_i) and
stable(s_avm_byteenable_i) and stable(s_avm_burstcount_i)};
f_slave_burst_valid : assume always rst_i or not (s_avm_read_i and not s_avm_waitrequest_o and nor(s_avm_burstcount_i));
f_master_burst_reset : assume always rst_i |=> {f_m_rd_burstcount = 0};
f_master_burst_range : assume always rst_i or f_m_rd_burstcount >= 0;
f_master_burst_block : assume always rst_i or f_m_rd_burstcount = 0 or m_avm_waitrequest_i or (f_m_rd_burstcount = 1 and m_avm_readdatavalid_i = '1');
f_master_no_data : assume always rst_i or not (f_m_rd_burstcount = 0 and m_avm_readdatavalid_i = '1');
--------------------------------------------
-- COVER STATEMENTS TO VERIFY REACHABILITY
--------------------------------------------
} -- vunit i_avm_cache(avm_cache(synthesis))
|
