1 |
2 |
dsmv |
|
2 |
|
|
//-----------------------------------------------------------------------------
|
3 |
|
|
//
|
4 |
|
|
// (c) Copyright 2009-2010 Xilinx, Inc. All rights reserved.
|
5 |
|
|
//
|
6 |
|
|
// This file contains confidential and proprietary information
|
7 |
|
|
// of Xilinx, Inc. and is protected under U.S. and
|
8 |
|
|
// international copyright and other intellectual property
|
9 |
|
|
// laws.
|
10 |
|
|
//
|
11 |
|
|
// DISCLAIMER
|
12 |
|
|
// This disclaimer is not a license and does not grant any
|
13 |
|
|
// rights to the materials distributed herewith. Except as
|
14 |
|
|
// otherwise provided in a valid license issued to you by
|
15 |
|
|
// Xilinx, and to the maximum extent permitted by applicable
|
16 |
|
|
// law: (1) THESE MATERIALS ARE MADE AVAILABLE "AS IS" AND
|
17 |
|
|
// WITH ALL FAULTS, AND XILINX HEREBY DISCLAIMS ALL WARRANTIES
|
18 |
|
|
// AND CONDITIONS, EXPRESS, IMPLIED, OR STATUTORY, INCLUDING
|
19 |
|
|
// BUT NOT LIMITED TO WARRANTIES OF MERCHANTABILITY, NON-
|
20 |
|
|
// INFRINGEMENT, OR FITNESS FOR ANY PARTICULAR PURPOSE; and
|
21 |
|
|
// (2) Xilinx shall not be liable (whether in contract or tort,
|
22 |
|
|
// including negligence, or under any other theory of
|
23 |
|
|
// liability) for any loss or damage of any kind or nature
|
24 |
|
|
// related to, arising under or in connection with these
|
25 |
|
|
// materials, including for any direct, or any indirect,
|
26 |
|
|
// special, incidental, or consequential loss or damage
|
27 |
|
|
// (including loss of data, profits, goodwill, or any type of
|
28 |
|
|
// loss or damage suffered as a result of any action brought
|
29 |
|
|
// by a third party) even if such damage or loss was
|
30 |
|
|
// reasonably foreseeable or Xilinx had been advised of the
|
31 |
|
|
// possibility of the same.
|
32 |
|
|
//
|
33 |
|
|
// CRITICAL APPLICATIONS
|
34 |
|
|
// Xilinx products are not designed or intended to be fail-
|
35 |
|
|
// safe, or for use in any application requiring fail-safe
|
36 |
|
|
// performance, such as life-support or safety devices or
|
37 |
|
|
// systems, Class III medical devices, nuclear facilities,
|
38 |
|
|
// applications related to the deployment of airbags, or any
|
39 |
|
|
// other applications that could lead to death, personal
|
40 |
|
|
// injury, or severe property or environmental damage
|
41 |
|
|
// (individually and collectively, "Critical
|
42 |
|
|
// Applications"). Customer assumes the sole risk and
|
43 |
|
|
// liability of any use of Xilinx products in Critical
|
44 |
|
|
// Applications, subject only to applicable laws and
|
45 |
|
|
// regulations governing limitations on product liability.
|
46 |
|
|
//
|
47 |
|
|
// THIS COPYRIGHT NOTICE AND DISCLAIMER MUST BE RETAINED AS
|
48 |
|
|
// PART OF THIS FILE AT ALL TIMES.
|
49 |
|
|
//
|
50 |
|
|
//-----------------------------------------------------------------------------
|
51 |
|
|
// Project : V5-Block Plus for PCI Express
|
52 |
|
|
// File : pcie_blk_ll_oqbqfifo.v
|
53 |
|
|
//--------------------------------------------------------------------------------
|
54 |
|
|
//--------------------------------------------------------------------------------
|
55 |
|
|
//--
|
56 |
|
|
//-- Description: First word Fall-Thru FIFO with separate storage areas
|
57 |
|
|
//-- for Non-posted and posted/completion TLPs
|
58 |
|
|
//--
|
59 |
|
|
//--------------------------------------------------------------------------------
|
60 |
|
|
|
61 |
|
|
`timescale 1ns/1ns
|
62 |
|
|
`ifndef TCQ
|
63 |
|
|
`define TCQ 1
|
64 |
|
|
`endif
|
65 |
|
|
|
66 |
|
|
module pcie_blk_ll_oqbqfifo
|
67 |
|
|
//{{{ Port List
|
68 |
|
|
(
|
69 |
|
|
// Clock and reset
|
70 |
|
|
|
71 |
|
|
input wire clk,
|
72 |
|
|
input wire rst_n,
|
73 |
|
|
|
74 |
|
|
// Outputs
|
75 |
|
|
output reg trn_rsrc_rdy = 0,
|
76 |
|
|
output reg [63:0] trn_rd = 0,
|
77 |
|
|
output reg [7:0] trn_rrem = 0,
|
78 |
|
|
output reg trn_rsof = 0,
|
79 |
|
|
output reg trn_reof = 0,
|
80 |
|
|
output reg trn_rerrfwd = 0,
|
81 |
|
|
output reg [6:0] trn_rbar_hit = 0,
|
82 |
|
|
output reg fifo_np_ok = 1,
|
83 |
|
|
output reg fifo_pcpl_ok = 1,
|
84 |
|
|
|
85 |
|
|
// Inputs
|
86 |
|
|
input trn_rdst_rdy,
|
87 |
|
|
input trn_rnp_ok,
|
88 |
|
|
input fifo_wren,
|
89 |
|
|
input [63:0] fifo_data,
|
90 |
|
|
input fifo_rem,
|
91 |
|
|
input fifo_sof,
|
92 |
|
|
input fifo_preeof,
|
93 |
|
|
input fifo_eof,
|
94 |
|
|
input fifo_dsc,
|
95 |
|
|
input fifo_np,
|
96 |
|
|
input [3:0] fifo_barenc, // Encoded BAR hit
|
97 |
|
|
input fifo_np_req,
|
98 |
|
|
input fifo_pcpl_req,
|
99 |
|
|
input fifo_np_abort,
|
100 |
|
|
input fifo_pcpl_abort
|
101 |
|
|
);
|
102 |
|
|
//}}}
|
103 |
|
|
//{{{ Wire/Reg declarations
|
104 |
|
|
wire [71:0] oq_din, bq_din;
|
105 |
|
|
wire [71:0] oq_dout, bq_dout;
|
106 |
|
|
wire [63:0] oq_dataout, bq_dataout;
|
107 |
|
|
wire oq_sofout, bq_sofout;
|
108 |
|
|
wire oq_preeofout, bq_preeofout;
|
109 |
|
|
wire oq_remout, bq_remout;
|
110 |
|
|
wire oq_errout, bq_errout;
|
111 |
|
|
wire [3:0] oq_barout, bq_barout;
|
112 |
|
|
wire oq_wren, bq_wren;
|
113 |
|
|
wire oq_rden, bq_rden;
|
114 |
|
|
wire oq_full, bq_full;
|
115 |
|
|
wire oq_afull, bq_afull;
|
116 |
|
|
wire oq_rdy, bq_rdy;
|
117 |
|
|
wire oq_valid, bq_valid;
|
118 |
|
|
wire oq_empty, bq_empty;
|
119 |
|
|
wire oq_trn_in_progress, bq_trn_in_progress;
|
120 |
|
|
wire trigger_oq_trn, trigger_bq_trn;
|
121 |
|
|
wire oq_memrd;
|
122 |
|
|
wire poisoned;
|
123 |
|
|
reg poisoned_reg = 0;
|
124 |
|
|
reg packet_in_progress = 0;
|
125 |
|
|
reg packet_in_progress_bq = 0;
|
126 |
|
|
reg packet_in_progress_oq = 0;
|
127 |
|
|
wire trigger_bypass;
|
128 |
|
|
wire oq_byp_in_progress;
|
129 |
|
|
reg oq_byp_in_progress_reg;
|
130 |
|
|
reg [3:0] np_count = 0;
|
131 |
|
|
reg trn_np = 0;
|
132 |
|
|
reg trn_drain_np = 0;
|
133 |
|
|
reg fifo_discard_np = 0;
|
134 |
|
|
reg trn_rnp_ok_d = 1;
|
135 |
|
|
reg [8:0] oq_pktcnt = 0;
|
136 |
|
|
reg [3:0] bq_pktcnt = 0;
|
137 |
|
|
reg oq_pkt_avail = 0;
|
138 |
|
|
reg bq_pkt_avail = 0;
|
139 |
|
|
reg oq_write_pkt_in_progress_reg = 0;
|
140 |
|
|
reg new_oq_pkt_wr =0;
|
141 |
|
|
reg new_oq_pkt_wr_d =0;
|
142 |
|
|
reg new_oq_pkt_wr_d2 =0;
|
143 |
|
|
integer i;
|
144 |
|
|
//}}}
|
145 |
|
|
//{{{ Functions
|
146 |
|
|
function [6:0] barhit;
|
147 |
|
|
input [3:0] selector;
|
148 |
|
|
begin
|
149 |
|
|
casex (selector)
|
150 |
|
|
4'b0000: barhit = 7'b0000001;
|
151 |
|
|
4'b0001: barhit = 7'b0000010;
|
152 |
|
|
4'b0010: barhit = 7'b0000100;
|
153 |
|
|
4'b0011: barhit = 7'b0001000;
|
154 |
|
|
4'b0100: barhit = 7'b0010000;
|
155 |
|
|
4'b0101: barhit = 7'b0100000;
|
156 |
|
|
4'b0110: barhit = 7'b1000000;
|
157 |
|
|
4'b0111: barhit = 7'b0000011;
|
158 |
|
|
4'b1000: barhit = 7'b0000110;
|
159 |
|
|
4'b1001: barhit = 7'b0001100;
|
160 |
|
|
4'b1010: barhit = 7'b0011000;
|
161 |
|
|
4'b1011: barhit = 7'b0110000;
|
162 |
|
|
default: barhit = 7'b0000000; // No BAR hit (cpl)
|
163 |
|
|
endcase
|
164 |
|
|
end
|
165 |
|
|
endfunction
|
166 |
|
|
|
167 |
|
|
function nonposted;
|
168 |
|
|
input [7:0] header;
|
169 |
|
|
begin
|
170 |
|
|
casex (header[6:0])
|
171 |
|
|
7'b0x0000x: nonposted = 1'b1; //MRd, MRdLk
|
172 |
|
|
7'bx000010: nonposted = 1'b1; //IO
|
173 |
|
|
7'bx00010x: nonposted = 1'b1; //Cfg
|
174 |
|
|
default: nonposted = 1'b0;
|
175 |
|
|
endcase
|
176 |
|
|
end
|
177 |
|
|
endfunction
|
178 |
|
|
|
179 |
|
|
//}}}
|
180 |
|
|
|
181 |
|
|
//{{{ Ordered Queue (OQ) FIFO
|
182 |
|
|
// Map module inputs and internal signals to BRAM inputs
|
183 |
|
|
wire nonposted_or_rem = fifo_sof ? nonposted(fifo_data[63:56]) : fifo_rem;
|
184 |
|
|
// 71 70 69 68 67:64 63:0
|
185 |
|
|
assign oq_din = {fifo_sof, fifo_eof, nonposted_or_rem, poisoned, fifo_barenc, fifo_data};
|
186 |
|
|
assign oq_sofout = oq_dout[71];
|
187 |
|
|
assign oq_eofout = oq_dout[70];
|
188 |
|
|
assign oq_remout = oq_eofout ? oq_dout[69] : 1'b1;
|
189 |
|
|
assign oq_errout = oq_dout[68];
|
190 |
|
|
assign oq_barout = oq_dout[67:64];
|
191 |
|
|
assign oq_dataout = oq_dout[63:0];
|
192 |
|
|
assign oq_valid = !oq_empty;
|
193 |
|
|
assign oq_memrd = oq_sofout && oq_valid && oq_dout[69]; //bit69 indicates nonposted during SOF
|
194 |
|
|
assign oq_wren = (oq_write_pkt_in_progress_reg || fifo_sof) && fifo_wren;
|
195 |
|
|
assign oq_rden = ((oq_trn_in_progress && (trn_rdst_rdy || !trn_rsrc_rdy)) ||
|
196 |
|
|
oq_byp_in_progress);
|
197 |
|
|
|
198 |
|
|
always @(posedge clk) begin
|
199 |
|
|
if (!rst_n)
|
200 |
|
|
oq_write_pkt_in_progress_reg <= #`TCQ 1'b0;
|
201 |
|
|
else if (fifo_wren && fifo_sof)
|
202 |
|
|
oq_write_pkt_in_progress_reg <= #`TCQ 1'b1;
|
203 |
|
|
else if (fifo_wren && (fifo_eof || fifo_dsc))
|
204 |
|
|
oq_write_pkt_in_progress_reg <= #`TCQ 1'b0;
|
205 |
|
|
end
|
206 |
|
|
|
207 |
|
|
|
208 |
|
|
sync_fifo
|
209 |
|
|
#(
|
210 |
|
|
.WIDTH (72),
|
211 |
|
|
.DEPTH (512),
|
212 |
|
|
.STYLE ("BRAM"),
|
213 |
|
|
.AFASSERT (512 - 66 - 14),
|
214 |
|
|
.FWFT (1),
|
215 |
|
|
.SUP_REWIND (1)
|
216 |
|
|
) oq_fifo (
|
217 |
|
|
.clk ( clk ),
|
218 |
|
|
.rst_n ( rst_n ),
|
219 |
|
|
.din ( oq_din ),
|
220 |
|
|
.dout ( oq_dout ),
|
221 |
|
|
.wr_en ( oq_wren ),
|
222 |
|
|
.rd_en ( oq_rden ),
|
223 |
|
|
.full ( oq_full ),
|
224 |
|
|
.afull ( oq_afull ),
|
225 |
|
|
.empty ( oq_empty ),
|
226 |
|
|
.aempty ( ),
|
227 |
|
|
.data_count ( ),
|
228 |
|
|
.mark_addr ( fifo_sof && oq_wren ),
|
229 |
|
|
.clear_addr ( fifo_eof && oq_wren ),
|
230 |
|
|
.rewind ( fifo_dsc && oq_wren )
|
231 |
|
|
);
|
232 |
|
|
//}}}
|
233 |
|
|
|
234 |
|
|
//{{{ Bypass Queue (BQ) FIFO
|
235 |
|
|
// Instantiate SRLFIFO for storing BQ data.
|
236 |
|
|
assign bq_din = oq_dout;
|
237 |
|
|
assign bq_sofout = bq_dout[71];
|
238 |
|
|
assign bq_eofout = bq_dout[70];
|
239 |
|
|
assign bq_remout = bq_dout[69];
|
240 |
|
|
assign bq_errout = bq_dout[68];
|
241 |
|
|
assign bq_barout = bq_dout[67:64];
|
242 |
|
|
assign bq_dataout = bq_dout[63:0];
|
243 |
|
|
assign bq_valid = !bq_empty;
|
244 |
|
|
assign bq_wren = oq_valid && oq_byp_in_progress;
|
245 |
|
|
assign bq_rden = bq_valid && bq_trn_in_progress && (trn_rdst_rdy || !trn_rsrc_rdy);
|
246 |
|
|
|
247 |
|
|
sync_fifo
|
248 |
|
|
#(
|
249 |
|
|
.WIDTH (72),
|
250 |
|
|
.DEPTH (16),
|
251 |
|
|
.FWFT (1),
|
252 |
|
|
.STYLE ("SRL")
|
253 |
|
|
) bq_fifo (
|
254 |
|
|
.din ( bq_din ),
|
255 |
|
|
.dout ( bq_dout ),
|
256 |
|
|
.wr_en ( bq_wren ),
|
257 |
|
|
.rd_en ( bq_rden ),
|
258 |
|
|
.full ( bq_full ),
|
259 |
|
|
.afull ( bq_afull ),
|
260 |
|
|
.empty ( bq_empty ),
|
261 |
|
|
.aempty ( ),
|
262 |
|
|
.data_count ( ),
|
263 |
|
|
.clk ( clk ),
|
264 |
|
|
.rst_n ( rst_n )
|
265 |
|
|
);
|
266 |
|
|
//}}}
|
267 |
|
|
|
268 |
|
|
//{{{ OQ/BQ Arbitration Logic; Bypass
|
269 |
|
|
assign trigger_bypass = (oq_memrd && !bq_afull && !trn_rnp_ok_d);
|
270 |
|
|
assign oq_byp_in_progress = oq_byp_in_progress_reg || trigger_bypass;
|
271 |
|
|
|
272 |
|
|
assign bq_rdy = bq_pkt_avail;
|
273 |
|
|
assign oq_rdy = !bq_rdy && oq_pkt_avail && !oq_byp_in_progress;
|
274 |
|
|
|
275 |
|
|
assign trigger_bq_trn = bq_rdy && !trn_rsrc_rdy && !packet_in_progress;
|
276 |
|
|
assign bq_trn_in_progress = packet_in_progress_bq || trigger_bq_trn;
|
277 |
|
|
|
278 |
|
|
assign trigger_oq_trn = oq_rdy && !trn_rsrc_rdy && !packet_in_progress;
|
279 |
|
|
assign oq_trn_in_progress = packet_in_progress_oq || trigger_oq_trn;
|
280 |
|
|
|
281 |
|
|
|
282 |
|
|
always @(posedge clk) begin
|
283 |
|
|
if (!rst_n)
|
284 |
|
|
oq_byp_in_progress_reg <= #`TCQ 1'b0;
|
285 |
|
|
else if (trigger_bypass)
|
286 |
|
|
oq_byp_in_progress_reg <= #`TCQ 1'b1;
|
287 |
|
|
else if (oq_eofout && oq_valid)
|
288 |
|
|
oq_byp_in_progress_reg <= #`TCQ 1'b0;
|
289 |
|
|
end
|
290 |
|
|
//}}}
|
291 |
|
|
|
292 |
|
|
//{{{ TRN Interface
|
293 |
|
|
always @(posedge clk) begin
|
294 |
|
|
if (!rst_n) begin
|
295 |
|
|
trn_rd <= #`TCQ 'h0;
|
296 |
|
|
trn_rsof <= #`TCQ 1'b0;
|
297 |
|
|
trn_reof <= #`TCQ 1'b0;
|
298 |
|
|
trn_rrem <= #`TCQ 8'hFF;
|
299 |
|
|
trn_rbar_hit <= #`TCQ 'h0;
|
300 |
|
|
trn_rsrc_rdy <= #`TCQ 1'b0;
|
301 |
|
|
trn_rerrfwd <= #`TCQ 1'b0;
|
302 |
|
|
packet_in_progress <= #`TCQ 1'b0;
|
303 |
|
|
packet_in_progress_bq <= #`TCQ 1'b0;
|
304 |
|
|
packet_in_progress_oq <= #`TCQ 1'b0;
|
305 |
|
|
end else begin
|
306 |
|
|
//Case 1: Waiting for EOF to be accepted (stalled with DST RDY)
|
307 |
|
|
if (trn_rsrc_rdy && trn_reof && !trn_rdst_rdy) begin
|
308 |
|
|
packet_in_progress <= #`TCQ 1'b0;
|
309 |
|
|
packet_in_progress_bq <= #`TCQ 1'b0;
|
310 |
|
|
packet_in_progress_oq <= #`TCQ 1'b0;
|
311 |
|
|
trn_rd <= #`TCQ trn_rd;
|
312 |
|
|
trn_rsof <= #`TCQ trn_rsof;
|
313 |
|
|
trn_reof <= #`TCQ trn_reof;
|
314 |
|
|
trn_rrem <= #`TCQ trn_rrem;
|
315 |
|
|
trn_rsrc_rdy <= #`TCQ trn_rsrc_rdy && !trn_rdst_rdy;
|
316 |
|
|
trn_rbar_hit <= #`TCQ trn_rbar_hit;
|
317 |
|
|
trn_rerrfwd <= #`TCQ trn_rerrfwd;
|
318 |
|
|
end
|
319 |
|
|
//Case 2: Packet in progress from BQ queue, or starting new one from idle
|
320 |
|
|
else if (bq_trn_in_progress) begin
|
321 |
|
|
// Filling accepted data
|
322 |
|
|
if ((trn_rdst_rdy || !trn_rsrc_rdy) && bq_valid) begin
|
323 |
|
|
packet_in_progress <= #`TCQ (!bq_eofout || bq_rdy) || (bq_eofout && oq_rdy);
|
324 |
|
|
packet_in_progress_bq <= #`TCQ !bq_eofout || bq_rdy;
|
325 |
|
|
packet_in_progress_oq <= #`TCQ bq_eofout && oq_rdy && !oq_byp_in_progress;
|
326 |
|
|
trn_rd <= #`TCQ bq_dataout;
|
327 |
|
|
trn_rsof <= #`TCQ bq_sofout;
|
328 |
|
|
trn_rrem <= #`TCQ {4'hF, { 4{bq_remout} }};
|
329 |
|
|
trn_rbar_hit <= #`TCQ barhit(bq_barout);
|
330 |
|
|
trn_rerrfwd <= #`TCQ bq_errout;
|
331 |
|
|
end
|
332 |
|
|
if ((trn_rdst_rdy || !trn_rsrc_rdy) && bq_valid) begin
|
333 |
|
|
trn_rsrc_rdy <= #`TCQ 1'b1;
|
334 |
|
|
trn_reof <= #`TCQ bq_eofout;
|
335 |
|
|
// Packet in progress from BQ queue; queue pauses
|
336 |
|
|
end else if (!bq_valid) begin
|
337 |
|
|
trn_rsrc_rdy <= #`TCQ trn_rsrc_rdy && !trn_rdst_rdy;
|
338 |
|
|
trn_reof <= #`TCQ bq_eofout && !trn_rdst_rdy;
|
339 |
|
|
end
|
340 |
|
|
end
|
341 |
|
|
//Case 3: Packet in progress from OQ queue, or starting new one from idle
|
342 |
|
|
else if (oq_trn_in_progress && !oq_byp_in_progress) begin
|
343 |
|
|
//packet_in_progress_oq || (oq_rdy && !trn_rsrc_rdy && !packet_in_progress)) begin
|
344 |
|
|
if ((trn_rdst_rdy || !trn_rsrc_rdy) && oq_valid) begin
|
345 |
|
|
packet_in_progress <= #`TCQ (!oq_eofout || oq_rdy) || (oq_eofout && bq_rdy);
|
346 |
|
|
packet_in_progress_bq <= #`TCQ oq_eofout && bq_rdy;
|
347 |
|
|
packet_in_progress_oq <= #`TCQ !oq_eofout || oq_rdy;
|
348 |
|
|
trn_rd <= #`TCQ oq_dataout;
|
349 |
|
|
trn_rsof <= #`TCQ oq_sofout;
|
350 |
|
|
trn_rrem <= #`TCQ {4'hF, { 4{oq_remout} }};
|
351 |
|
|
trn_rbar_hit <= #`TCQ barhit(oq_barout);
|
352 |
|
|
trn_rerrfwd <= #`TCQ oq_errout;
|
353 |
|
|
trn_rsrc_rdy <= #`TCQ 1'b1;
|
354 |
|
|
trn_reof <= #`TCQ oq_eofout;
|
355 |
|
|
// Packet in progress from OQ queue; queue pauses
|
356 |
|
|
end else if (!oq_valid) begin
|
357 |
|
|
trn_rsrc_rdy <= #`TCQ trn_rsrc_rdy && !trn_rdst_rdy;
|
358 |
|
|
trn_reof <= #`TCQ oq_eofout && !trn_rdst_rdy;
|
359 |
|
|
end
|
360 |
|
|
end
|
361 |
|
|
//Case 4: Idle
|
362 |
|
|
else begin
|
363 |
|
|
packet_in_progress <= #`TCQ 1'b0;
|
364 |
|
|
packet_in_progress_bq <= #`TCQ 1'b0;
|
365 |
|
|
packet_in_progress_oq <= #`TCQ 1'b0;
|
366 |
|
|
trn_rd <= #`TCQ trn_rd;
|
367 |
|
|
trn_rsof <= #`TCQ 1'b0;
|
368 |
|
|
trn_reof <= #`TCQ 1'b0;
|
369 |
|
|
trn_rrem <= #`TCQ 8'hFF;
|
370 |
|
|
trn_rsrc_rdy <= #`TCQ 1'b0;
|
371 |
|
|
trn_rbar_hit <= #`TCQ 'h0;
|
372 |
|
|
trn_rerrfwd <= #`TCQ 1'b0;
|
373 |
|
|
end
|
374 |
|
|
end
|
375 |
|
|
end
|
376 |
|
|
//}}}
|
377 |
|
|
|
378 |
|
|
//{{{ ASSERTIONS: LocalLink and TRN
|
379 |
|
|
`ifdef SV
|
380 |
|
|
//synthesis translate_off
|
381 |
|
|
ASSERT_LL_DOUBLESOF: assert property (@(posedge clk)
|
382 |
|
|
(trn_rsof && trn_rdst_rdy && trn_rsrc_rdy) |-> ##1 !(trn_rsof && trn_rdst_rdy && trn_rsrc_rdy)
|
383 |
|
|
) else $fatal;
|
384 |
|
|
ASSERT_LL_DOUBLEEOF: assert property (@(posedge clk)
|
385 |
|
|
(trn_reof && trn_rdst_rdy && trn_rsrc_rdy) |-> ##1 !(trn_reof && trn_rdst_rdy && trn_rsrc_rdy)
|
386 |
|
|
) else $fatal;
|
387 |
|
|
ASSERT_RDST_HOLDS_OUTPUT: assert property (@(posedge clk)
|
388 |
|
|
!trn_rdst_rdy && trn_rsrc_rdy |-> ##1 $stable(trn_rd) &&
|
389 |
|
|
$stable(trn_rsof) &&
|
390 |
|
|
$stable(trn_reof) &&
|
391 |
|
|
$stable(trn_rrem) &&
|
392 |
|
|
$stable(trn_rbar_hit) &&
|
393 |
|
|
$stable(trn_rerrfwd)
|
394 |
|
|
) else $fatal;
|
395 |
|
|
//TLPs s/b back2back if possible, if there is a valid dword in OQ or BQ after
|
396 |
|
|
//a non-stalled EOF, unless:
|
397 |
|
|
//a) OQ->BQ bypass is occurring, and BQ output is empty or stalled due to RNP_OK deassertion
|
398 |
|
|
//b) RNP_OK is deasserted, and either OQ not available or it is a NP
|
399 |
|
|
ASSERT_RX_TRN_BACK2BACK_NP: assert property (@(posedge clk)
|
400 |
|
|
!(!trn_rdst_rdy && trn_rsrc_rdy && trn_reof) && (bq_valid && (bq_pktcnt>0) && trn_rnp_ok_d) ##1
|
401 |
|
|
trn_rdst_rdy && trn_rsrc_rdy && trn_reof |-> ##1
|
402 |
|
|
(trn_rsof && trn_rsrc_rdy && nonposted(trn_rd[63:56]))
|
403 |
|
|
) else $fatal;
|
404 |
|
|
ASSERT_RX_TRN_BACK2BACK_PCPL:assert property (@(posedge clk)
|
405 |
|
|
!(!trn_rdst_rdy && trn_rsrc_rdy && trn_reof) && !(bq_valid && (bq_pktcnt>0) && trn_rnp_ok_d) &&
|
406 |
|
|
(oq_valid && (oq_pktcnt>0) && !oq_byp_in_progress && !(!trn_rnp_ok_d && oq_memrd)) ##1
|
407 |
|
|
trn_rdst_rdy && trn_rsrc_rdy && trn_reof |-> ##1
|
408 |
|
|
(trn_rsof && trn_rsrc_rdy) || oq_byp_in_progress
|
409 |
|
|
) else $fatal;
|
410 |
|
|
ASSERT_PROGRESS_MUTEX1: assert property (@(posedge clk)
|
411 |
|
|
bq_trn_in_progress |-> !oq_trn_in_progress
|
412 |
|
|
) else $fatal;
|
413 |
|
|
ASSERT_PROGRESS_MUTEX2: assert property (@(posedge clk)
|
414 |
|
|
oq_trn_in_progress |-> !bq_trn_in_progress && (!oq_byp_in_progress || (trn_reof && trn_rsrc_rdy))
|
415 |
|
|
) else $fatal;
|
416 |
|
|
ASSERT_PROGRESS_MUTEX3: assert property (@(posedge clk)
|
417 |
|
|
oq_byp_in_progress && !(trn_reof && trn_rsrc_rdy) |-> !oq_trn_in_progress
|
418 |
|
|
) else $fatal;
|
419 |
|
|
ASSERT_PACKETINPROGRESS2: assert property (@(posedge clk)
|
420 |
|
|
packet_in_progress_oq |-> !packet_in_progress_bq && packet_in_progress
|
421 |
|
|
) else $fatal;
|
422 |
|
|
ASSERT_PACKETINPROGRESS3: assert property (@(posedge clk)
|
423 |
|
|
packet_in_progress |-> packet_in_progress_bq || packet_in_progress_oq
|
424 |
|
|
) else $fatal;
|
425 |
|
|
ASSERT_BYPASS_OQ_MUTEX: assert property (@(posedge clk)
|
426 |
|
|
!(bq_wren && oq_trn_in_progress && !(trn_reof && trn_rsrc_rdy))
|
427 |
|
|
) else $fatal;
|
428 |
|
|
ASSERT_BQ_WRITE_BYP_ONLY: assert property (@(posedge clk)
|
429 |
|
|
!(bq_wren && !oq_byp_in_progress)
|
430 |
|
|
) else $fatal;
|
431 |
|
|
ASSERT_RNPOK_STOPS_NP: assert property (@(posedge clk)
|
432 |
|
|
!trn_rnp_ok ##1 !trn_rnp_ok ##1 !trn_rnp_ok |-> ##1
|
433 |
|
|
!(trn_rsof && trn_rsrc_rdy && nonposted(trn_rd[64:56]))
|
434 |
|
|
) else $fatal;
|
435 |
|
|
//synthesis translate_on
|
436 |
|
|
`endif
|
437 |
|
|
//}}}
|
438 |
|
|
|
439 |
|
|
//{{{ Poisoned bit logic
|
440 |
|
|
// Assert poisoned when starting or continuing a poisoned TLP
|
441 |
|
|
assign poisoned = poisoned_reg || (fifo_data[46] && fifo_sof);
|
442 |
|
|
|
443 |
|
|
// Continue wrtrans* and poisoned signals after SOF until EOF
|
444 |
|
|
always @(posedge clk) begin
|
445 |
|
|
if (!rst_n) begin
|
446 |
|
|
poisoned_reg <= #`TCQ 0;
|
447 |
|
|
end else if (fifo_sof && !fifo_eof && fifo_wren) begin
|
448 |
|
|
poisoned_reg <= #`TCQ fifo_data[46];
|
449 |
|
|
end else if (fifo_eof && fifo_wren) begin
|
450 |
|
|
poisoned_reg <= #`TCQ 0;
|
451 |
|
|
end
|
452 |
|
|
end
|
453 |
|
|
//}}}
|
454 |
|
|
|
455 |
|
|
//{{{ FIFO-fullness counting logic
|
456 |
|
|
always @(posedge clk) begin
|
457 |
|
|
if (!rst_n) begin
|
458 |
|
|
fifo_np_ok <= #`TCQ 1'b1;
|
459 |
|
|
fifo_pcpl_ok <= #`TCQ 1'b1;
|
460 |
|
|
trn_np <= #`TCQ 1'b0;
|
461 |
|
|
trn_drain_np <= #`TCQ 1'b0;
|
462 |
|
|
fifo_discard_np <= #`TCQ 1'b0;
|
463 |
|
|
np_count <= #`TCQ 'h0;
|
464 |
|
|
trn_rnp_ok_d <= #`TCQ 1'b1;
|
465 |
|
|
new_oq_pkt_wr <= #`TCQ 1'b0;
|
466 |
|
|
new_oq_pkt_wr_d <= #`TCQ 1'b0;
|
467 |
|
|
new_oq_pkt_wr_d2 <= #`TCQ 1'b0;
|
468 |
|
|
oq_pktcnt <= #`TCQ 'h0;
|
469 |
|
|
bq_pktcnt <= #`TCQ 'h0;
|
470 |
|
|
oq_pkt_avail <= #`TCQ 'b0;
|
471 |
|
|
bq_pkt_avail <= #`TCQ 'b0;
|
472 |
|
|
end else begin
|
473 |
|
|
fifo_np_ok <= #`TCQ (np_count<8) && !oq_afull;
|
474 |
|
|
fifo_pcpl_ok <= #`TCQ !oq_afull;
|
475 |
|
|
if (trn_rsof && nonposted(trn_rd[63:56]) && trn_rsrc_rdy)
|
476 |
|
|
trn_np <= #`TCQ 1'b1;
|
477 |
|
|
else if (trn_rsof && trn_rsrc_rdy)
|
478 |
|
|
trn_np <= #`TCQ 1'b0;
|
479 |
|
|
trn_drain_np <= #`TCQ trn_np && trn_reof && trn_rsrc_rdy && trn_rdst_rdy;
|
480 |
|
|
fifo_discard_np <= #`TCQ fifo_np && fifo_wren && fifo_dsc;
|
481 |
|
|
case ({fifo_np_req,trn_drain_np,fifo_discard_np})
|
482 |
|
|
3'b000 : np_count <= #`TCQ np_count;
|
483 |
|
|
3'b001 : np_count <= #`TCQ np_count - 1;
|
484 |
|
|
3'b010 : np_count <= #`TCQ np_count - 1;
|
485 |
|
|
3'b011 : np_count <= #`TCQ np_count - 2;
|
486 |
|
|
3'b100 : np_count <= #`TCQ np_count + 1;
|
487 |
|
|
3'b101 : np_count <= #`TCQ np_count;
|
488 |
|
|
3'b110 : np_count <= #`TCQ np_count;
|
489 |
|
|
3'b111 : np_count <= #`TCQ np_count - 1;
|
490 |
|
|
default: np_count <= #`TCQ np_count;
|
491 |
|
|
endcase
|
492 |
|
|
trn_rnp_ok_d <= #`TCQ trn_rnp_ok;
|
493 |
|
|
new_oq_pkt_wr <= #`TCQ oq_wren && fifo_eof && !fifo_dsc;
|
494 |
|
|
new_oq_pkt_wr_d <= #`TCQ new_oq_pkt_wr;
|
495 |
|
|
new_oq_pkt_wr_d2 <= #`TCQ new_oq_pkt_wr_d;
|
496 |
|
|
if (new_oq_pkt_wr_d2 && !(oq_rden && oq_sofout && oq_valid)) begin
|
497 |
|
|
oq_pktcnt <= #`TCQ oq_pktcnt + 1;
|
498 |
|
|
oq_pkt_avail <= #`TCQ 1'b1;
|
499 |
|
|
end
|
500 |
|
|
else if (!new_oq_pkt_wr_d2 && (oq_rden && oq_sofout && oq_valid)) begin
|
501 |
|
|
oq_pktcnt <= #`TCQ oq_pktcnt - 1;
|
502 |
|
|
oq_pkt_avail <= #`TCQ (oq_pktcnt>1);
|
503 |
|
|
end else begin
|
504 |
|
|
oq_pkt_avail <= #`TCQ (oq_pktcnt>0);
|
505 |
|
|
end
|
506 |
|
|
if ( (bq_wren && oq_eofout) &&
|
507 |
|
|
!(bq_rden && bq_sofout && bq_valid)) begin
|
508 |
|
|
bq_pktcnt <= #`TCQ bq_pktcnt + 1;
|
509 |
|
|
bq_pkt_avail <= #`TCQ trn_rnp_ok_d;
|
510 |
|
|
end
|
511 |
|
|
else if (!(bq_wren && oq_eofout) &&
|
512 |
|
|
(bq_rden && bq_sofout && bq_valid)) begin
|
513 |
|
|
bq_pktcnt <= #`TCQ bq_pktcnt - 1;
|
514 |
|
|
bq_pkt_avail <= #`TCQ (bq_pktcnt>1) && trn_rnp_ok_d;
|
515 |
|
|
end else begin
|
516 |
|
|
bq_pkt_avail <= #`TCQ (bq_pktcnt>0) && trn_rnp_ok_d;
|
517 |
|
|
end
|
518 |
|
|
end
|
519 |
|
|
end
|
520 |
|
|
|
521 |
|
|
|
522 |
|
|
|
523 |
|
|
//}}}
|
524 |
|
|
|
525 |
|
|
//{{{ ASSERTIONS: npcount
|
526 |
|
|
`ifdef SV
|
527 |
|
|
//synthesis translate_off
|
528 |
|
|
ASSERT_NPCOUNT_IS_0_WHEN_IDLE: assert property (@(posedge clk)
|
529 |
|
|
(!oq_valid && !bq_valid && !trn_rsrc_rdy && !fifo_np_req)[*20]
|
530 |
|
|
|-> (np_count == 0)
|
531 |
|
|
|
532 |
|
|
) else $fatal;
|
533 |
|
|
ASSERT_NPCOUNT_IS_8_OR_LESS: assert property (@(posedge clk)
|
534 |
|
|
!(np_count > 8 )
|
535 |
|
|
) else $fatal;
|
536 |
|
|
//synthesis translate_on
|
537 |
|
|
`endif
|
538 |
|
|
//}}}
|
539 |
|
|
|
540 |
|
|
endmodule
|
541 |
|
|
|