1 |
16 |
dgisselq |
////////////////////////////////////////////////////////////////////////////////
|
2 |
|
|
//
|
3 |
|
|
// Filename: wbm2axilite.v (Wishbone master to AXI slave, pipelined)
|
4 |
|
|
//
|
5 |
|
|
// Project: Pipelined Wishbone to AXI converter
|
6 |
|
|
//
|
7 |
|
|
// Purpose: Convert from a wishbone master to an AXI lite interface. The
|
8 |
|
|
// big difference is that AXI lite doesn't support bursting,
|
9 |
|
|
// or transaction ID's. This actually makes the task a *LOT* easier.
|
10 |
|
|
//
|
11 |
|
|
// Creator: Dan Gisselquist, Ph.D.
|
12 |
|
|
// Gisselquist Technology, LLC
|
13 |
|
|
//
|
14 |
|
|
////////////////////////////////////////////////////////////////////////////////
|
15 |
|
|
//
|
16 |
|
|
// Copyright (C) 2018-2019, Gisselquist Technology, LLC
|
17 |
|
|
//
|
18 |
|
|
// This file is part of the pipelined Wishbone to AXI converter project, a
|
19 |
|
|
// project that contains multiple bus bridging designs and formal bus property
|
20 |
|
|
// sets.
|
21 |
|
|
//
|
22 |
|
|
// The bus bridge designs and property sets are free RTL designs: you can
|
23 |
|
|
// redistribute them and/or modify any of them under the terms of the GNU
|
24 |
|
|
// Lesser General Public License as published by the Free Software Foundation,
|
25 |
|
|
// either version 3 of the License, or (at your option) any later version.
|
26 |
|
|
//
|
27 |
|
|
// The bus bridge designs and property sets are distributed in the hope that
|
28 |
|
|
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
|
29 |
|
|
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
30 |
|
|
// GNU Lesser General Public License for more details.
|
31 |
|
|
//
|
32 |
|
|
// You should have received a copy of the GNU Lesser General Public License
|
33 |
|
|
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
|
34 |
|
|
// with no target there if the PDF file isn't present.) If not, see
|
35 |
|
|
// <http://www.gnu.org/licenses/> for a copy.
|
36 |
|
|
//
|
37 |
|
|
// License: LGPL, v3, as defined and found on www.gnu.org,
|
38 |
|
|
// http://www.gnu.org/licenses/lgpl.html
|
39 |
|
|
//
|
40 |
|
|
////////////////////////////////////////////////////////////////////////////////
|
41 |
|
|
//
|
42 |
|
|
//
|
43 |
|
|
`default_nettype none
|
44 |
|
|
//
|
45 |
|
|
module wbm2axilite (
|
46 |
|
|
i_clk, i_reset,
|
47 |
|
|
// AXI write address channel signals
|
48 |
|
|
i_axi_awready, o_axi_awaddr, o_axi_awcache, o_axi_awprot, o_axi_awvalid,
|
49 |
|
|
// AXI write data channel signals
|
50 |
|
|
i_axi_wready, o_axi_wdata, o_axi_wstrb, o_axi_wvalid,
|
51 |
|
|
// AXI write response channel signals
|
52 |
|
|
i_axi_bresp, i_axi_bvalid, o_axi_bready,
|
53 |
|
|
// AXI read address channel signals
|
54 |
|
|
i_axi_arready, o_axi_araddr, o_axi_arcache, o_axi_arprot, o_axi_arvalid,
|
55 |
|
|
// AXI read data channel signals
|
56 |
|
|
i_axi_rresp, i_axi_rvalid, i_axi_rdata, o_axi_rready,
|
57 |
|
|
// We'll share the clock and the reset
|
58 |
|
|
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel,
|
59 |
|
|
o_wb_ack, o_wb_stall, o_wb_data, o_wb_err);
|
60 |
|
|
|
61 |
|
|
localparam C_AXI_DATA_WIDTH = 32;// Width of the AXI R&W data
|
62 |
|
|
parameter C_AXI_ADDR_WIDTH = 28;// AXI Address width
|
63 |
|
|
localparam DW = C_AXI_DATA_WIDTH;// Wishbone data width
|
64 |
|
|
parameter AW = C_AXI_ADDR_WIDTH-2;// WB addr width (log wordsize)
|
65 |
|
|
input wire i_clk; // System clock
|
66 |
|
|
input wire i_reset;// Reset signal,drives AXI rst
|
67 |
|
|
|
68 |
|
|
// AXI write address channel signals
|
69 |
|
|
input wire i_axi_awready;//Slave is ready to accept
|
70 |
|
|
output reg [C_AXI_ADDR_WIDTH-1:0] o_axi_awaddr; // Write address
|
71 |
|
|
output wire [3:0] o_axi_awcache; // Write Cache type
|
72 |
|
|
output wire [2:0] o_axi_awprot; // Write Protection type
|
73 |
|
|
output reg o_axi_awvalid; // Write address valid
|
74 |
|
|
|
75 |
|
|
// AXI write data channel signals
|
76 |
|
|
input wire i_axi_wready; // Write data ready
|
77 |
|
|
output reg [C_AXI_DATA_WIDTH-1:0] o_axi_wdata; // Write data
|
78 |
|
|
output reg [C_AXI_DATA_WIDTH/8-1:0] o_axi_wstrb; // Write strobes
|
79 |
|
|
output reg o_axi_wvalid; // Write valid
|
80 |
|
|
|
81 |
|
|
// AXI write response channel signals
|
82 |
|
|
input wire [1:0] i_axi_bresp; // Write response
|
83 |
|
|
input wire i_axi_bvalid; // Write reponse valid
|
84 |
|
|
output wire o_axi_bready; // Response ready
|
85 |
|
|
|
86 |
|
|
// AXI read address channel signals
|
87 |
|
|
input wire i_axi_arready; // Read address ready
|
88 |
|
|
output reg [C_AXI_ADDR_WIDTH-1:0] o_axi_araddr; // Read address
|
89 |
|
|
output wire [3:0] o_axi_arcache; // Read Cache type
|
90 |
|
|
output wire [2:0] o_axi_arprot; // Read Protection type
|
91 |
|
|
output reg o_axi_arvalid; // Read address valid
|
92 |
|
|
|
93 |
|
|
// AXI read data channel signals
|
94 |
|
|
input wire [1:0] i_axi_rresp; // Read response
|
95 |
|
|
input wire i_axi_rvalid; // Read reponse valid
|
96 |
|
|
input wire [C_AXI_DATA_WIDTH-1:0] i_axi_rdata; // Read data
|
97 |
|
|
output wire o_axi_rready; // Read Response ready
|
98 |
|
|
|
99 |
|
|
// We'll share the clock and the reset
|
100 |
|
|
input wire i_wb_cyc;
|
101 |
|
|
input wire i_wb_stb;
|
102 |
|
|
input wire i_wb_we;
|
103 |
|
|
input wire [(AW-1):0] i_wb_addr;
|
104 |
|
|
input wire [(DW-1):0] i_wb_data;
|
105 |
|
|
input wire [(DW/8-1):0] i_wb_sel;
|
106 |
|
|
output reg o_wb_ack;
|
107 |
|
|
output wire o_wb_stall;
|
108 |
|
|
output reg [(DW-1):0] o_wb_data;
|
109 |
|
|
output reg o_wb_err;
|
110 |
|
|
|
111 |
|
|
//*****************************************************************************
|
112 |
|
|
// Local Parameter declarations
|
113 |
|
|
//*****************************************************************************
|
114 |
|
|
|
115 |
|
|
localparam LG_AXI_DW = ( C_AXI_DATA_WIDTH == 8) ? 3
|
116 |
|
|
: ((C_AXI_DATA_WIDTH == 16) ? 4
|
117 |
|
|
: ((C_AXI_DATA_WIDTH == 32) ? 5
|
118 |
|
|
: ((C_AXI_DATA_WIDTH == 64) ? 6
|
119 |
|
|
: ((C_AXI_DATA_WIDTH == 128) ? 7
|
120 |
|
|
: 8))));
|
121 |
|
|
|
122 |
|
|
localparam LG_WB_DW = ( DW == 8) ? 3
|
123 |
|
|
: ((DW == 16) ? 4
|
124 |
|
|
: ((DW == 32) ? 5
|
125 |
|
|
: ((DW == 64) ? 6
|
126 |
|
|
: ((DW == 128) ? 7
|
127 |
|
|
: 8))));
|
128 |
|
|
localparam LGFIFOLN = 5;
|
129 |
|
|
localparam FIFOLN = (1<<LGFIFOLN);
|
130 |
|
|
|
131 |
|
|
|
132 |
|
|
//*****************************************************************************
|
133 |
|
|
// Internal register and wire declarations
|
134 |
|
|
//*****************************************************************************
|
135 |
|
|
|
136 |
|
|
// Things we're not changing ...
|
137 |
|
|
assign o_axi_awcache = 4'h3; // Normal: no cache, no buffer
|
138 |
|
|
assign o_axi_arcache = 4'h3; // Normal: no cache, no buffer
|
139 |
|
|
assign o_axi_awprot = 3'b000; // Unpriviledged, unsecure, data access
|
140 |
|
|
assign o_axi_arprot = 3'b000; // Unpriviledged, unsecure, data access
|
141 |
|
|
|
142 |
|
|
reg full_fifo, err_state, axi_reset_state, wb_we;
|
143 |
|
|
reg [3:0] reset_count;
|
144 |
|
|
reg pending;
|
145 |
|
|
reg [LGFIFOLN-1:0] outstanding, err_pending;
|
146 |
|
|
|
147 |
|
|
|
148 |
|
|
// Master bridge logic
|
149 |
|
|
assign o_wb_stall = (full_fifo)
|
150 |
|
|
||((!i_wb_we)&&( wb_we)&&(pending))
|
151 |
|
|
||(( i_wb_we)&&(!wb_we)&&(pending))
|
152 |
|
|
||(err_state)||(axi_reset_state)
|
153 |
|
|
||(o_axi_arvalid)&&(!i_axi_arready)
|
154 |
|
|
||(o_axi_awvalid)&&(!i_axi_awready)
|
155 |
|
|
||(o_axi_wvalid)&&(!i_axi_wready);
|
156 |
|
|
|
157 |
|
|
initial axi_reset_state = 1'b1;
|
158 |
|
|
initial reset_count = 4'hf;
|
159 |
|
|
always @(posedge i_clk)
|
160 |
|
|
if (i_reset)
|
161 |
|
|
begin
|
162 |
|
|
axi_reset_state <= 1'b1;
|
163 |
|
|
if (reset_count > 0)
|
164 |
|
|
reset_count <= reset_count - 1'b1;
|
165 |
|
|
end else if ((axi_reset_state)&&(reset_count > 0))
|
166 |
|
|
reset_count <= reset_count - 1'b1;
|
167 |
|
|
else begin
|
168 |
|
|
axi_reset_state <= 1'b0;
|
169 |
|
|
reset_count <= 4'hf;
|
170 |
|
|
end
|
171 |
|
|
|
172 |
|
|
// Count outstanding transactions
|
173 |
|
|
initial pending = 0;
|
174 |
|
|
initial outstanding = 0;
|
175 |
|
|
always @(posedge i_clk)
|
176 |
|
|
if ((i_reset)||(axi_reset_state))
|
177 |
|
|
begin
|
178 |
|
|
pending <= 0;
|
179 |
|
|
outstanding <= 0;
|
180 |
|
|
full_fifo <= 0;
|
181 |
|
|
end else if ((err_state)||(!i_wb_cyc))
|
182 |
|
|
begin
|
183 |
|
|
pending <= 0;
|
184 |
|
|
outstanding <= 0;
|
185 |
|
|
full_fifo <= 0;
|
186 |
|
|
end else case({ ((i_wb_stb)&&(!o_wb_stall)), (o_wb_ack) })
|
187 |
|
|
2'b01: begin
|
188 |
|
|
outstanding <= outstanding - 1'b1;
|
189 |
|
|
pending <= (outstanding >= 2);
|
190 |
|
|
full_fifo <= 1'b0;
|
191 |
|
|
end
|
192 |
|
|
2'b10: begin
|
193 |
|
|
outstanding <= outstanding + 1'b1;
|
194 |
|
|
pending <= 1'b1;
|
195 |
|
|
full_fifo <= (outstanding >= {{(LGFIFOLN-2){1'b1}},2'b01});;
|
196 |
|
|
end
|
197 |
|
|
default: begin end
|
198 |
|
|
endcase
|
199 |
|
|
|
200 |
|
|
always @(posedge i_clk)
|
201 |
|
|
if ((i_wb_stb)&&(!o_wb_stall))
|
202 |
|
|
wb_we <= i_wb_we;
|
203 |
|
|
|
204 |
|
|
//
|
205 |
|
|
//
|
206 |
|
|
// Write address logic
|
207 |
|
|
//
|
208 |
|
|
initial o_axi_awvalid = 0;
|
209 |
|
|
always @(posedge i_clk)
|
210 |
|
|
if (i_reset)
|
211 |
|
|
o_axi_awvalid <= 0;
|
212 |
|
|
else
|
213 |
|
|
o_axi_awvalid <= (!o_wb_stall)&&(i_wb_stb)&&(i_wb_we)
|
214 |
|
|
||(o_axi_awvalid)&&(!i_axi_awready);
|
215 |
|
|
|
216 |
|
|
always @(posedge i_clk)
|
217 |
|
|
if (!o_wb_stall)
|
218 |
|
|
o_axi_awaddr <= { i_wb_addr, 2'b00 };
|
219 |
|
|
|
220 |
|
|
//
|
221 |
|
|
//
|
222 |
|
|
// Read address logic
|
223 |
|
|
//
|
224 |
|
|
initial o_axi_arvalid = 1'b0;
|
225 |
|
|
always @(posedge i_clk)
|
226 |
|
|
if (i_reset)
|
227 |
|
|
o_axi_arvalid <= 1'b0;
|
228 |
|
|
else
|
229 |
|
|
o_axi_arvalid <= (!o_wb_stall)&&(i_wb_stb)&&(!i_wb_we)
|
230 |
|
|
||((o_axi_arvalid)&&(!i_axi_arready));
|
231 |
|
|
always @(posedge i_clk)
|
232 |
|
|
if (!o_wb_stall)
|
233 |
|
|
o_axi_araddr <= { i_wb_addr, 2'b00 };
|
234 |
|
|
|
235 |
|
|
//
|
236 |
|
|
//
|
237 |
|
|
// Write data logic
|
238 |
|
|
//
|
239 |
|
|
always @(posedge i_clk)
|
240 |
|
|
if (!o_wb_stall)
|
241 |
|
|
begin
|
242 |
|
|
o_axi_wdata <= i_wb_data;
|
243 |
|
|
o_axi_wstrb <= i_wb_sel;
|
244 |
|
|
end
|
245 |
|
|
|
246 |
|
|
initial o_axi_wvalid = 0;
|
247 |
|
|
always @(posedge i_clk)
|
248 |
|
|
if (i_reset)
|
249 |
|
|
o_axi_wvalid <= 0;
|
250 |
|
|
else
|
251 |
|
|
o_axi_wvalid <= ((!o_wb_stall)&&(i_wb_stb)&&(i_wb_we))
|
252 |
|
|
||((o_axi_wvalid)&&(!i_axi_wready));
|
253 |
|
|
|
254 |
|
|
initial o_wb_ack = 1'b0;
|
255 |
|
|
always @(posedge i_clk)
|
256 |
|
|
if ((i_reset)||(!i_wb_cyc)||(err_state))
|
257 |
|
|
o_wb_ack <= 1'b0;
|
258 |
|
|
else if (err_state)
|
259 |
|
|
o_wb_ack <= 1'b0;
|
260 |
|
|
else if ((i_axi_bvalid)&&(!i_axi_bresp[1]))
|
261 |
|
|
o_wb_ack <= 1'b1;
|
262 |
|
|
else if ((i_axi_rvalid)&&(!i_axi_rresp[1]))
|
263 |
|
|
o_wb_ack <= 1'b1;
|
264 |
|
|
else
|
265 |
|
|
o_wb_ack <= 1'b0;
|
266 |
|
|
|
267 |
|
|
always @(posedge i_clk)
|
268 |
|
|
o_wb_data <= i_axi_rdata;
|
269 |
|
|
|
270 |
|
|
// Read data channel / response logic
|
271 |
|
|
assign o_axi_rready = 1'b1;
|
272 |
|
|
assign o_axi_bready = 1'b1;
|
273 |
|
|
|
274 |
|
|
initial o_wb_err = 1'b0;
|
275 |
|
|
always @(posedge i_clk)
|
276 |
|
|
if ((i_reset)||(!i_wb_cyc)||(err_state))
|
277 |
|
|
o_wb_err <= 1'b0;
|
278 |
|
|
else if ((i_axi_bvalid)&&(i_axi_bresp[1]))
|
279 |
|
|
o_wb_err <= 1'b1;
|
280 |
|
|
else if ((i_axi_rvalid)&&(i_axi_rresp[1]))
|
281 |
|
|
o_wb_err <= 1'b1;
|
282 |
|
|
else
|
283 |
|
|
o_wb_err <= 1'b0;
|
284 |
|
|
|
285 |
|
|
initial err_state = 1'b0;
|
286 |
|
|
always @(posedge i_clk)
|
287 |
|
|
if (i_reset)
|
288 |
|
|
err_state <= 0;
|
289 |
|
|
else if ((i_axi_bvalid)&&(i_axi_bresp[1]))
|
290 |
|
|
err_state <= 1'b1;
|
291 |
|
|
else if ((i_axi_rvalid)&&(i_axi_rresp[1]))
|
292 |
|
|
err_state <= 1'b1;
|
293 |
|
|
else if ((pending)&&(!i_wb_cyc))
|
294 |
|
|
err_state <= 1'b1;
|
295 |
|
|
else if (err_pending == 0)
|
296 |
|
|
err_state <= 0;
|
297 |
|
|
|
298 |
|
|
initial err_pending = 0;
|
299 |
|
|
always @(posedge i_clk)
|
300 |
|
|
if (i_reset)
|
301 |
|
|
err_pending <= 0;
|
302 |
|
|
else case({ ((i_wb_stb)&&(!o_wb_stall)),
|
303 |
|
|
((i_axi_bvalid)||(i_axi_rvalid)) })
|
304 |
|
|
2'b01: err_pending <= err_pending - 1'b1;
|
305 |
|
|
2'b10: err_pending <= err_pending + 1'b1;
|
306 |
|
|
default: begin end
|
307 |
|
|
endcase
|
308 |
|
|
|
309 |
|
|
// Make verilator happy
|
310 |
|
|
// verilator lint_off UNUSED
|
311 |
|
|
wire [2:0] unused;
|
312 |
|
|
assign unused = { i_wb_cyc, i_axi_bresp[0], i_axi_rresp[0] };
|
313 |
|
|
// verilator lint_on UNUSED
|
314 |
|
|
|
315 |
|
|
/////////////////////////////////////////////////////////////////////////
|
316 |
|
|
//
|
317 |
|
|
//
|
318 |
|
|
//
|
319 |
|
|
// Formal methods section
|
320 |
|
|
//
|
321 |
|
|
// These are only relevant when *proving* that this translator works
|
322 |
|
|
//
|
323 |
|
|
//
|
324 |
|
|
//
|
325 |
|
|
/////////////////////////////////////////////////////////////////////////
|
326 |
|
|
`ifdef FORMAL
|
327 |
|
|
reg f_past_valid;
|
328 |
|
|
//
|
329 |
|
|
`define ASSUME assume
|
330 |
|
|
`define ASSERT assert
|
331 |
|
|
|
332 |
|
|
// Parameters
|
333 |
|
|
initial assert(DW == 32);
|
334 |
|
|
initial assert(C_AXI_ADDR_WIDTH == AW+2);
|
335 |
|
|
//
|
336 |
|
|
|
337 |
|
|
//
|
338 |
|
|
// Setup
|
339 |
|
|
//
|
340 |
|
|
initial f_past_valid = 1'b0;
|
341 |
|
|
always @(posedge i_clk)
|
342 |
|
|
f_past_valid <= 1'b1;
|
343 |
|
|
|
344 |
|
|
always @(*)
|
345 |
|
|
if (!f_past_valid)
|
346 |
|
|
`ASSUME(i_reset);
|
347 |
|
|
|
348 |
|
|
//////////////////////////////////////////////
|
349 |
|
|
//
|
350 |
|
|
//
|
351 |
|
|
// Assumptions about the WISHBONE inputs
|
352 |
|
|
//
|
353 |
|
|
//
|
354 |
|
|
//////////////////////////////////////////////
|
355 |
|
|
assume property(f_past_valid || i_reset);
|
356 |
|
|
|
357 |
|
|
wire [(LGFIFOLN-1):0] f_wb_nreqs, f_wb_nacks,f_wb_outstanding;
|
358 |
|
|
fwb_slave #(.DW(DW),.AW(AW),
|
359 |
|
|
.F_MAX_STALL(0),
|
360 |
|
|
.F_MAX_ACK_DELAY(0),
|
361 |
|
|
.F_LGDEPTH(LGFIFOLN),
|
362 |
|
|
.F_MAX_REQUESTS(FIFOLN-2))
|
363 |
|
|
f_wb(i_clk, i_reset, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr,
|
364 |
|
|
i_wb_data, i_wb_sel,
|
365 |
|
|
o_wb_ack, o_wb_stall, o_wb_data, o_wb_err,
|
366 |
|
|
f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
|
367 |
|
|
|
368 |
|
|
wire [(LGFIFOLN-1):0] f_axi_rd_outstanding,
|
369 |
|
|
f_axi_wr_outstanding,
|
370 |
|
|
f_axi_awr_outstanding;
|
371 |
|
|
|
372 |
|
|
faxil_master #(
|
373 |
|
|
// .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
|
374 |
|
|
.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
|
375 |
|
|
.F_LGDEPTH(LGFIFOLN),
|
376 |
|
|
.F_AXI_MAXWAIT(3),
|
377 |
|
|
.F_OPT_HAS_CACHE(1'b1),
|
378 |
|
|
.F_AXI_MAXDELAY(3))
|
379 |
|
|
f_axil(.i_clk(i_clk),
|
380 |
|
|
.i_axi_reset_n((!i_reset)&&(!axi_reset_state)),
|
381 |
|
|
// Write address channel
|
382 |
|
|
.i_axi_awready(i_axi_awready),
|
383 |
|
|
.i_axi_awaddr( o_axi_awaddr),
|
384 |
|
|
.i_axi_awcache(o_axi_awcache),
|
385 |
|
|
.i_axi_awprot( o_axi_awprot),
|
386 |
|
|
.i_axi_awvalid(o_axi_awvalid),
|
387 |
|
|
// Write data channel
|
388 |
|
|
.i_axi_wready( i_axi_wready),
|
389 |
|
|
.i_axi_wdata( o_axi_wdata),
|
390 |
|
|
.i_axi_wstrb( o_axi_wstrb),
|
391 |
|
|
.i_axi_wvalid( o_axi_wvalid),
|
392 |
|
|
// Write response channel
|
393 |
|
|
.i_axi_bresp( i_axi_bresp),
|
394 |
|
|
.i_axi_bvalid( i_axi_bvalid),
|
395 |
|
|
.i_axi_bready( o_axi_bready),
|
396 |
|
|
// Read address channel
|
397 |
|
|
.i_axi_arready(i_axi_arready),
|
398 |
|
|
.i_axi_araddr( o_axi_araddr),
|
399 |
|
|
.i_axi_arcache(o_axi_arcache),
|
400 |
|
|
.i_axi_arprot( o_axi_arprot),
|
401 |
|
|
.i_axi_arvalid(o_axi_arvalid),
|
402 |
|
|
// Read data channel
|
403 |
|
|
.i_axi_rresp( i_axi_rresp),
|
404 |
|
|
.i_axi_rvalid( i_axi_rvalid),
|
405 |
|
|
.i_axi_rdata( i_axi_rdata),
|
406 |
|
|
.i_axi_rready( o_axi_rready),
|
407 |
|
|
// Counts
|
408 |
|
|
.f_axi_rd_outstanding( f_axi_rd_outstanding),
|
409 |
|
|
.f_axi_wr_outstanding( f_axi_wr_outstanding),
|
410 |
|
|
.f_axi_awr_outstanding( f_axi_awr_outstanding)
|
411 |
|
|
);
|
412 |
|
|
|
413 |
|
|
//////////////////////////////////////////////
|
414 |
|
|
//
|
415 |
|
|
//
|
416 |
|
|
// Assumptions about the AXI inputs
|
417 |
|
|
//
|
418 |
|
|
//
|
419 |
|
|
//////////////////////////////////////////////
|
420 |
|
|
|
421 |
|
|
|
422 |
|
|
//////////////////////////////////////////////
|
423 |
|
|
//
|
424 |
|
|
//
|
425 |
|
|
// Assertions about the AXI4 ouputs
|
426 |
|
|
//
|
427 |
|
|
//
|
428 |
|
|
//////////////////////////////////////////////
|
429 |
|
|
|
430 |
|
|
// Write response channel
|
431 |
|
|
always @(posedge i_clk)
|
432 |
|
|
// We keep bready high, so the other condition doesn't
|
433 |
|
|
// need to be checked
|
434 |
|
|
assert(o_axi_bready);
|
435 |
|
|
|
436 |
|
|
// AXI read data channel signals
|
437 |
|
|
always @(posedge i_clk)
|
438 |
|
|
// We keep o_axi_rready high, so the other condition's
|
439 |
|
|
// don't need to be checked here
|
440 |
|
|
assert(o_axi_rready);
|
441 |
|
|
|
442 |
|
|
//
|
443 |
|
|
// Let's look into write requests
|
444 |
|
|
//
|
445 |
|
|
initial assert(!o_axi_awvalid);
|
446 |
|
|
initial assert(!o_axi_wvalid);
|
447 |
|
|
always @(posedge i_clk)
|
448 |
|
|
if ((!f_past_valid)||($past(i_reset))||($past(axi_reset_state)))
|
449 |
|
|
begin
|
450 |
|
|
assert(!o_axi_awvalid);
|
451 |
|
|
assert(!o_axi_wvalid);
|
452 |
|
|
end
|
453 |
|
|
|
454 |
|
|
always @(posedge i_clk)
|
455 |
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
456 |
|
|
&&($past((i_wb_stb)&&(i_wb_we)&&(!o_wb_stall))))
|
457 |
|
|
begin
|
458 |
|
|
// Following any write request that we accept, awvalid
|
459 |
|
|
// and wvalid should both be true
|
460 |
|
|
assert(o_axi_awvalid);
|
461 |
|
|
assert(o_axi_wvalid);
|
462 |
|
|
assert(wb_we);
|
463 |
|
|
end else if ((f_past_valid)&&($past(i_reset)))
|
464 |
|
|
begin
|
465 |
|
|
if ($past(i_axi_awready))
|
466 |
|
|
assert(!o_axi_awvalid);
|
467 |
|
|
if ($past(i_axi_wready))
|
468 |
|
|
assert(!o_axi_wvalid);
|
469 |
|
|
end
|
470 |
|
|
|
471 |
|
|
//
|
472 |
|
|
// AXI write address channel
|
473 |
|
|
//
|
474 |
|
|
always @(posedge i_clk)
|
475 |
|
|
if ((f_past_valid)&&($past((i_wb_stb)&&(i_wb_we)&&(!o_wb_stall))))
|
476 |
|
|
assert(o_axi_awaddr == { $past(i_wb_addr[AW-1:0]), 2'b00 });
|
477 |
|
|
|
478 |
|
|
//
|
479 |
|
|
// AXI write data channel
|
480 |
|
|
//
|
481 |
|
|
always @(posedge i_clk)
|
482 |
|
|
if ((f_past_valid)&&($past(i_wb_stb)&&(i_wb_we)&&(!$past(o_wb_stall))))
|
483 |
|
|
begin
|
484 |
|
|
assert(o_axi_wdata == $past(i_wb_data));
|
485 |
|
|
assert(o_axi_wstrb == $past(i_wb_sel));
|
486 |
|
|
end
|
487 |
|
|
|
488 |
|
|
//
|
489 |
|
|
// AXI read address channel
|
490 |
|
|
//
|
491 |
|
|
initial assert(!o_axi_arvalid);
|
492 |
|
|
always @(posedge i_clk)
|
493 |
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
494 |
|
|
&&($past((i_wb_stb)&&(!i_wb_we)&&(!o_wb_stall))))
|
495 |
|
|
begin
|
496 |
|
|
assert(o_axi_arvalid);
|
497 |
|
|
assert(o_axi_araddr == { $past(i_wb_addr), 2'b00 });
|
498 |
|
|
end
|
499 |
|
|
//
|
500 |
|
|
|
501 |
|
|
//
|
502 |
|
|
// AXI write response channel
|
503 |
|
|
//
|
504 |
|
|
|
505 |
|
|
//
|
506 |
|
|
// AXI read data channel signals
|
507 |
|
|
//
|
508 |
|
|
always @(posedge i_clk)
|
509 |
|
|
if ((f_past_valid)&&(($past(i_reset))||($past(axi_reset_state))))
|
510 |
|
|
begin
|
511 |
|
|
// Relate err_pending to outstanding
|
512 |
|
|
assert(outstanding == 0);
|
513 |
|
|
assert(err_pending == 0);
|
514 |
|
|
end else if (!err_state)
|
515 |
|
|
assert(err_pending == outstanding - ((o_wb_ack)||(o_wb_err)));
|
516 |
|
|
|
517 |
|
|
always @(posedge i_clk)
|
518 |
|
|
if ((f_past_valid)&&(($past(i_reset))||($past(axi_reset_state))))
|
519 |
|
|
begin
|
520 |
|
|
assert(f_axi_awr_outstanding == 0);
|
521 |
|
|
assert(f_axi_wr_outstanding == 0);
|
522 |
|
|
assert(f_axi_rd_outstanding == 0);
|
523 |
|
|
|
524 |
|
|
assert(f_wb_outstanding == 0);
|
525 |
|
|
assert(!pending);
|
526 |
|
|
assert(outstanding == 0);
|
527 |
|
|
assert(err_pending == 0);
|
528 |
|
|
end else if (wb_we)
|
529 |
|
|
begin
|
530 |
|
|
case({o_axi_awvalid,o_axi_wvalid})
|
531 |
|
|
2'b00: begin
|
532 |
|
|
`ASSERT(f_axi_awr_outstanding == err_pending);
|
533 |
|
|
`ASSERT(f_axi_wr_outstanding == err_pending);
|
534 |
|
|
end
|
535 |
|
|
2'b01: begin
|
536 |
|
|
`ASSERT(f_axi_awr_outstanding == err_pending);
|
537 |
|
|
`ASSERT(f_axi_wr_outstanding +1 == err_pending);
|
538 |
|
|
end
|
539 |
|
|
2'b10: begin
|
540 |
|
|
`ASSERT(f_axi_awr_outstanding+1 == err_pending);
|
541 |
|
|
`ASSERT(f_axi_wr_outstanding == err_pending);
|
542 |
|
|
end
|
543 |
|
|
2'b11: begin
|
544 |
|
|
`ASSERT(f_axi_awr_outstanding+1 == err_pending);
|
545 |
|
|
`ASSERT(f_axi_wr_outstanding +1 == err_pending);
|
546 |
|
|
end
|
547 |
|
|
endcase
|
548 |
|
|
|
549 |
|
|
//
|
550 |
|
|
`ASSERT(!o_axi_arvalid);
|
551 |
|
|
`ASSERT(f_axi_rd_outstanding == 0);
|
552 |
|
|
end else begin
|
553 |
|
|
if (!o_axi_arvalid)
|
554 |
|
|
`ASSERT(f_axi_rd_outstanding == err_pending);
|
555 |
|
|
else
|
556 |
|
|
`ASSERT(f_axi_rd_outstanding+1 == err_pending);
|
557 |
|
|
|
558 |
|
|
`ASSERT(!o_axi_awvalid);
|
559 |
|
|
`ASSERT(!o_axi_wvalid);
|
560 |
|
|
`ASSERT(f_axi_awr_outstanding == 0);
|
561 |
|
|
`ASSERT(f_axi_wr_outstanding == 0);
|
562 |
|
|
end
|
563 |
|
|
|
564 |
|
|
always @(*)
|
565 |
|
|
if ((!i_reset)&&(i_wb_cyc)&&(!err_state))
|
566 |
|
|
`ASSERT(f_wb_outstanding == outstanding);
|
567 |
|
|
|
568 |
|
|
always @(posedge i_clk)
|
569 |
|
|
if ((f_past_valid)&&(err_state))
|
570 |
|
|
`ASSERT((o_wb_err)||(f_wb_outstanding == 0));
|
571 |
|
|
|
572 |
|
|
always @(posedge i_clk)
|
573 |
|
|
`ASSERT(pending == (outstanding != 0));
|
574 |
|
|
//
|
575 |
|
|
// Make sure we only create one request at a time
|
576 |
|
|
always @(posedge i_clk)
|
577 |
|
|
`ASSERT((!o_axi_arvalid)||(!o_axi_wvalid));
|
578 |
|
|
always @(posedge i_clk)
|
579 |
|
|
`ASSERT((!o_axi_arvalid)||(!o_axi_awvalid));
|
580 |
|
|
always @(posedge i_clk)
|
581 |
|
|
if (wb_we)
|
582 |
|
|
`ASSERT(!o_axi_arvalid);
|
583 |
|
|
else
|
584 |
|
|
`ASSERT((!o_axi_awvalid)&&(!o_axi_wvalid));
|
585 |
|
|
|
586 |
|
|
always @(*)
|
587 |
|
|
if (&outstanding[LGFIFOLN-1:1])
|
588 |
|
|
`ASSERT(full_fifo);
|
589 |
|
|
always @(*)
|
590 |
|
|
assert(outstanding < {(LGFIFOLN){1'b1}});
|
591 |
|
|
|
592 |
|
|
// AXI cover results
|
593 |
|
|
always @(*)
|
594 |
|
|
cover(i_axi_bvalid && o_axi_bready);
|
595 |
|
|
always @(*)
|
596 |
|
|
cover(i_axi_rvalid && o_axi_rready);
|
597 |
|
|
|
598 |
|
|
always @(posedge i_clk)
|
599 |
|
|
cover(i_axi_bvalid && o_axi_bready
|
600 |
|
|
&& $past(i_axi_bvalid && o_axi_bready)
|
601 |
|
|
&& $past(i_axi_bvalid && o_axi_bready,2));
|
602 |
|
|
|
603 |
|
|
always @(posedge i_clk)
|
604 |
|
|
cover(i_axi_rvalid && o_axi_rready
|
605 |
|
|
&& $past(i_axi_rvalid && o_axi_rready)
|
606 |
|
|
&& $past(i_axi_rvalid && o_axi_rready,2));
|
607 |
|
|
|
608 |
|
|
// AXI cover requests
|
609 |
|
|
always @(posedge i_clk)
|
610 |
|
|
cover(o_axi_arvalid && i_axi_arready
|
611 |
|
|
&& $past(o_axi_arvalid && i_axi_arready)
|
612 |
|
|
&& $past(o_axi_arvalid && i_axi_arready,2));
|
613 |
|
|
|
614 |
|
|
always @(posedge i_clk)
|
615 |
|
|
cover(o_axi_awvalid && i_axi_awready
|
616 |
|
|
&& $past(o_axi_awvalid && i_axi_awready)
|
617 |
|
|
&& $past(o_axi_awvalid && i_axi_awready,2));
|
618 |
|
|
|
619 |
|
|
always @(posedge i_clk)
|
620 |
|
|
cover(o_axi_wvalid && i_axi_wready
|
621 |
|
|
&& $past(o_axi_wvalid && i_axi_wready)
|
622 |
|
|
&& $past(o_axi_wvalid && i_axi_wready,2));
|
623 |
|
|
|
624 |
|
|
always @(*)
|
625 |
|
|
cover(i_axi_rvalid && o_axi_rready);
|
626 |
|
|
|
627 |
|
|
// Wishbone cover results
|
628 |
|
|
always @(*)
|
629 |
|
|
cover(i_wb_cyc && o_wb_ack);
|
630 |
|
|
|
631 |
|
|
always @(posedge i_clk)
|
632 |
|
|
cover(i_wb_cyc && o_wb_ack
|
633 |
|
|
&& $past(o_wb_ack)&&$past(o_wb_ack,2));
|
634 |
|
|
|
635 |
|
|
`endif
|
636 |
|
|
endmodule
|