URL https://opencores.org/ocsvn/wb2axip/wb2axip/trunk

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [aximrd2wbsp.v] - Blame information for rev 10

Go to most recent revision | Details | Compare with Previous | View Log


////////////////////////////////////////////////////////////////////////////////
//
// Filename:    aximrd2wbsp.v
//
// Project:     Pipelined Wishbone to AXI converter
//
// Purpose:     Bridge an AXI read channel pair to a single wishbone read
//              channel.
//
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2016, Gisselquist Technology, LLC
//
// This program is free software (firmware): you can redistribute it and/or
// modify it under the terms of  the GNU General Public License as published
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
// for more details.
//
// You should have received a copy of the GNU General Public License along
// with this program.  (It's in the $(ROOT)/doc directory, run make with no
// target there if the PDF file isn't present.)  If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License:     GPL, v3, as defined and found on www.gnu.org,
//              http://www.gnu.org/licenses/gpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype        none
//
module  aximrd2wbsp #(
        parameter C_AXI_ID_WIDTH        = 6, // The AXI id width used for R&W
                                             // This is an int between 1-16
        parameter C_AXI_DATA_WIDTH      = 32,// Width of the AXI R&W data
        parameter C_AXI_ADDR_WIDTH      = 28,   // AXI Address width
        parameter AW                    = 26,   // AXI Address width
        parameter LGFIFO                =  4
        // parameter    WBMODE          = "B4PIPELINE"
                // Could also be "BLOCK"
        ) (
        input   wire                    i_axi_clk,      // Bus clock
        input   wire                    i_axi_reset_n,  // Bus reset
 
// AXI read address channel signals
        output  wire                    o_axi_arready,  // Read address ready
        input   wire    [C_AXI_ID_WIDTH-1:0]     i_axi_arid,     // Read ID
        input   wire    [C_AXI_ADDR_WIDTH-1:0]   i_axi_araddr,   // Read address
        input   wire    [7:0]            i_axi_arlen,    // Read Burst Length
        input   wire    [2:0]            i_axi_arsize,   // Read Burst size
        input   wire    [1:0]            i_axi_arburst,  // Read Burst type
        input   wire    [0:0]             i_axi_arlock,   // Read lock type
        input   wire    [3:0]            i_axi_arcache,  // Read Cache type
        input   wire    [2:0]            i_axi_arprot,   // Read Protection type
        input   wire    [3:0]            i_axi_arqos,    // Read Protection type
        input   wire                    i_axi_arvalid,  // Read address valid
 
// AXI read data channel signals   
        output  wire [C_AXI_ID_WIDTH-1:0] o_axi_rid,     // Response ID
        output  wire [1:0]               o_axi_rresp,   // Read response
        output  reg                     o_axi_rvalid,  // Read reponse valid
        output  wire [C_AXI_DATA_WIDTH-1:0] o_axi_rdata,    // Read data
        output  wire                    o_axi_rlast,    // Read last
        input   wire                    i_axi_rready,  // Read Response ready
 
        // We'll share the clock and the reset
        output  reg                             o_wb_cyc,
        output  reg                             o_wb_stb,
        output  wire [(AW-1):0]  o_wb_addr,
        input   wire                            i_wb_ack,
        input   wire                            i_wb_stall,
        input   [(C_AXI_DATA_WIDTH-1):0] i_wb_data,
        input   wire                            i_wb_err
        );
 
        localparam      DW = C_AXI_DATA_WIDTH;
 
        wire    w_reset;
        assign  w_reset = (i_axi_reset_n == 1'b0);
 
 
        reg     [(C_AXI_ID_WIDTH+AW+1)-1:0]      afifo   [0:((1<<(LGFIFO))-1)];
        reg     [(DW+1)-1:0]                     dfifo   [0:((1<<(LGFIFO))-1)];
        reg     [(C_AXI_ID_WIDTH+AW+1)-1:0]      fifo_at_neck, afifo_at_tail;
        reg     [(DW+1)-1:0]                     dfifo_at_tail;
 
        // We're going to need to keep track of transaction bursts in progress,
        // since the wishbone doesn't.  For this, we'll use a FIFO, but with
        // multiple pointers:
        //
        //      fifo_head       - pointer to where to write the next incoming
        //                              bus request .. adjusted when
        //                              (o_axi_arready)&&(i_axi_arvalid)
        //      fifo_neck       - pointer to where to read from the FIFO in
        //                              order to issue another request.  Used
        //                              when (o_wb_stb)&&(!i_wb_stall)
        //      fifo_torso      - pointer to where to write a wishbone
        //                              transaction upon return.
        //                              when (i_ack)
        //      fifo_tail       - pointer to where the last transaction is to
        //                              be retired when
        //                                      (i_axi_rvalid)&&(i_axi_rready)
        //
        // All of these are to be set to zero upon a reset signal.
        //
        reg     [LGFIFO-1:0]     fifo_head, fifo_neck, fifo_torso, fifo_tail;
 
        // Since we need to insure that these pointers wrap properly at
        // LGFIFO bits, and since it is confusing to do that within IF 
        // statements, 
        wire    [LGFIFO-1:0]     next_head, next_neck, next_torso, next_tail,
                                almost_head;
        wire            fifo_full;
        assign  next_head  = fifo_head  + 1;
        assign  next_neck  = fifo_neck  + 1;
        assign  next_torso = fifo_torso + 1;
        assign  next_tail  = fifo_tail  + 1;
        assign  almost_head = fifo_head  + 1;
 
        assign fifo_full = (almost_head == fifo_tail);
 
        reg     wr_last, filling_fifo, incr;
        reg     [7:0]                    len;
        reg     [(AW-1):0]               wr_fifo_addr;
        reg     [(C_AXI_ID_WIDTH-1):0]   wr_fifo_id;
 
        //
        //
        //
        //
        // Here's our plan: Any time READY & VALID are both true, initiate a
        // transfer (unless one is ongoing).  Hold READY false while initiating
        // any burst transaction.  Keep the request RID and burst length stuffs
        // into a FIFO.
        // queue are both valid, issue the wishbone read request.  Once a read
        // request returns, retire the value in the FIFO queue.
        //
        // The FIFO queue *must* include:
        //
        //      RQ, ADDR, LAST
        //
        initial len          = 0;
        initial filling_fifo = 0;
        initial fifo_head    = 0;
        always @(posedge i_axi_clk)
        begin
                wr_last <= 1'b0;
 
                if (filling_fifo)
                begin
                        if (!fifo_full)
                        begin
                                len <= len - 1;
                                if (len == 1)
                                        filling_fifo <= 1'b0;
                                fifo_head <= next_head;
                                wr_fifo_addr <= wr_fifo_addr
                                        + {{(AW-1){1'b0}}, incr};
                                wr_last <= (len == 1);
                        end
                end else begin
                        wr_fifo_addr <= i_axi_araddr[(C_AXI_ADDR_WIDTH-1):(C_AXI_ADDR_WIDTH-AW)];
                        wr_fifo_id <= i_axi_arid;
                        incr <= i_axi_arburst[0];
                        if ((o_axi_arready)&&(i_axi_arvalid))
                        begin
                                fifo_head <= next_head;
                                len <= i_axi_arlen;
                                filling_fifo <= (i_axi_arlen != 0);
                                wr_last <= 1'b1;
                        end
                end
 
                if (w_reset)
                begin
                        len <= 0;
                        filling_fifo <= 1'b0;
                        fifo_head <= 0;
                end
        end
 
        always @(posedge i_axi_clk)
                afifo[fifo_head] <= { wr_fifo_id, wr_last, wr_fifo_addr };
 
        reg     err_state;
        initial o_wb_cyc   = 1'b0;
        initial o_wb_stb   = 1'b0;
        initial fifo_neck  = 0;
        initial fifo_torso = 0;
        initial err_state  = 0;
        always @(posedge i_axi_clk)
        begin
                if (w_reset)
                begin
                        o_wb_cyc <= 1'b0;
                        o_wb_stb <= 1'b0;
 
                        fifo_neck  <= 0;
                        fifo_torso <= 0;
 
                        err_state <= 0;
                end else if (o_wb_stb)
                begin
                        if (i_wb_err)
                        begin
                                o_wb_stb <= 1'b0;
                                err_state <= 1'b1;
                        end else if (!i_wb_stall)
                        begin
                                o_wb_stb <= (fifo_head != next_neck);
                                                // && (WBMODE != "B3SINGLE");
                                // o_wb_cyc <= (WBMODE != "B3SINGLE");
                        end
 
                        if (!i_wb_stall)
                                fifo_neck <= next_neck;
                        if (i_wb_ack)
                                fifo_torso <= next_torso;
                end else if (err_state)
                begin
                        fifo_torso <= next_torso;
                        if (fifo_neck == next_torso)
                                err_state <= 1'b0;
                        o_wb_cyc <= 1'b0;
                end else if (o_wb_cyc)
                begin
                        if (i_wb_ack)
                                fifo_torso <= next_torso;
                        if (fifo_neck == next_torso)
                                o_wb_cyc <= 1'b0;
                end else if (fifo_neck != fifo_head)
                begin
                        o_wb_cyc <= 1'b1;
                        o_wb_stb <= 1'b1;
                end
        end
 
        always @(posedge i_axi_clk)
                fifo_at_neck <= afifo[fifo_neck];
        assign  o_wb_addr = fifo_at_neck[(AW-1):0];
 
        always @(posedge i_axi_clk)
                dfifo[fifo_torso] <= { (err_state)||(i_wb_err), i_wb_data };
 
 
        always @(posedge i_axi_clk)
                if (w_reset)
                        fifo_tail <= 0;
                else if ((o_axi_rvalid)&&(i_axi_rready))
                        fifo_tail <= next_tail;
 
        always @(posedge i_axi_clk)
        begin
                afifo_at_tail <= afifo[fifo_tail];
                dfifo_at_tail <= dfifo[fifo_tail];
                // o_axi_rdata <= dfifo[fifo_tail];
                // o_axi_rlast <= afifo[fifo_tail];
                // o_axi_rid   <= afifo[fifo_tail];
        end
        assign  o_axi_rlast = afifo_at_tail[AW];
        assign  o_axi_rid   = afifo_at_tail[(C_AXI_ID_WIDTH+AW):(AW+1)];
        assign  o_axi_rresp = { (2){dfifo_at_tail[DW]} };
        assign  o_axi_rdata = dfifo_at_tail[(DW-1):0];
 
        initial o_axi_rvalid = 1'b0;
        always @(posedge i_axi_clk)
                if (w_reset)
                        o_axi_rvalid <= 0;
                else if (fifo_tail != fifo_neck)
                        o_axi_rvalid <= (fifo_tail != fifo_neck + 1);
 
        assign o_axi_arready = (!fifo_full)&&(!filling_fifo);
 
        // Make Verilator happy
        // verilator lint_off UNUSED
        wire    [(C_AXI_ID_WIDTH+1)+(C_AXI_ADDR_WIDTH-AW)
                +3+1+1+4+3+4-1:0]        unused;
        assign  unused = { i_axi_arsize, i_axi_arburst[1],
                        i_axi_arlock, i_axi_arcache, i_axi_arprot,
                        i_axi_arqos,
                        fifo_at_neck[(C_AXI_ID_WIDTH+AW+1)-1:AW],
                        i_axi_araddr[(C_AXI_ADDR_WIDTH-AW-1):0] };
        // verilator lint_on  UNUSED
 
`ifdef  FORMAL
        reg     f_past_valid;
        initial f_past_valid = 1'b0;
        always @(posedge i_axi_clk)
                f_past_valid <= 1'b1;
 
        wire    [LGFIFO-1:0]     f_fifo_used, f_fifo_neck_used,
                                f_fifo_torso_used;
        assign  f_fifo_used       = fifo_head - fifo_tail;
        assign  f_fifo_neck_used  = fifo_head - fifo_neck;
        assign  f_fifo_torso_used = fifo_head - fifo_torso;
 
        always @(*)
                assert((f_fifo_used < {(LGFIFO){1'b1}})||(!o_axi_arready));
        always @(*)
                assert(f_fifo_neck_used  <= f_fifo_used);
        always @(*)
                assert(f_fifo_torso_used <= f_fifo_used);
 
        always @(posedge i_axi_clk)
        if ((f_past_valid)&&(!$past(i_axi_reset_n)))
                assert(f_fifo_used == 0);
 
`endif
endmodule

Browse

Tools

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [aximrd2wbsp.v] - Blame information for rev 10

Line No.	Rev	Author	Line
1	8	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
2			`//`
3			`// Filename: aximrd2wbsp.v`
4			`//`
5			`// Project: Pipelined Wishbone to AXI converter`
6			`//`
7			`// Purpose: Bridge an AXI read channel pair to a single wishbone read`
8			`// channel.`
9			`//`
10			`// Creator: Dan Gisselquist, Ph.D.`
11			`// Gisselquist Technology, LLC`
12			`//`
13			`////////////////////////////////////////////////////////////////////////////////`
14			`//`
15			`// Copyright (C) 2016, Gisselquist Technology, LLC`
16			`//`
17			`// This program is free software (firmware): you can redistribute it and/or`
18			`// modify it under the terms of the GNU General Public License as published`
19			`// by the Free Software Foundation, either version 3 of the License, or (at`
20			`// your option) any later version.`
21			`//`
22			`// This program is distributed in the hope that it will be useful, but WITHOUT`
23			`// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or`
24			`// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License`
25			`// for more details.`
26			`//`
27			`// You should have received a copy of the GNU General Public License along`
28			`// with this program. (It's in the $(ROOT)/doc directory, run make with no`
29			`// target there if the PDF file isn't present.) If not, see`
30			`// <http://www.gnu.org/licenses/> for a copy.`
31			`//`
32			`// License: GPL, v3, as defined and found on www.gnu.org,`
33			`// http://www.gnu.org/licenses/gpl.html`
34			`//`
35			`//`
36			`////////////////////////////////////////////////////////////////////////////////`
37			`//`
38			`//`
39			`default_nettype none
40			`//`
41			`module aximrd2wbsp #(`
42			`parameter C_AXI_ID_WIDTH = 6, // The AXI id width used for R&W`
43			`// This is an int between 1-16`
44			`parameter C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data`
45			`parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width`
46			`parameter AW = 26, // AXI Address width`
47			`parameter LGFIFO = 4`
48			`// parameter WBMODE = "B4PIPELINE"`
49			`// Could also be "BLOCK"`
50			`) (`
51			`input wire i_axi_clk, // Bus clock`
52			`input wire i_axi_reset_n, // Bus reset`
53
54			`// AXI read address channel signals`
55			`output wire o_axi_arready, // Read address ready`
56			`input wire [C_AXI_ID_WIDTH-1:0] i_axi_arid, // Read ID`
57			`input wire [C_AXI_ADDR_WIDTH-1:0] i_axi_araddr, // Read address`
58			`input wire [7:0] i_axi_arlen, // Read Burst Length`
59			`input wire [2:0] i_axi_arsize, // Read Burst size`
60			`input wire [1:0] i_axi_arburst, // Read Burst type`
61			`input wire [0:0] i_axi_arlock, // Read lock type`
62			`input wire [3:0] i_axi_arcache, // Read Cache type`
63			`input wire [2:0] i_axi_arprot, // Read Protection type`
64			`input wire [3:0] i_axi_arqos, // Read Protection type`
65			`input wire i_axi_arvalid, // Read address valid`
66
67			`// AXI read data channel signals`
68			`output wire [C_AXI_ID_WIDTH-1:0] o_axi_rid, // Response ID`
69			`output wire [1:0] o_axi_rresp, // Read response`
70			`output reg o_axi_rvalid, // Read reponse valid`
71			`output wire [C_AXI_DATA_WIDTH-1:0] o_axi_rdata, // Read data`
72			`output wire o_axi_rlast, // Read last`
73			`input wire i_axi_rready, // Read Response ready`
74
75			`// We'll share the clock and the reset`
76			`output reg o_wb_cyc,`
77			`output reg o_wb_stb,`
78			`output wire [(AW-1):0] o_wb_addr,`
79			`input wire i_wb_ack,`
80			`input wire i_wb_stall,`
81			`input [(C_AXI_DATA_WIDTH-1):0] i_wb_data,`
82			`input wire i_wb_err`
83			`);`
84
85			`localparam DW = C_AXI_DATA_WIDTH;`
86
87			`wire w_reset;`
88			`assign w_reset = (i_axi_reset_n == 1'b0);`
89
90
91			`reg [(C_AXI_ID_WIDTH+AW+1)-1:0] afifo [0:((1<<(LGFIFO))-1)];`
92			`reg [(DW+1)-1:0] dfifo [0:((1<<(LGFIFO))-1)];`
93			`reg [(C_AXI_ID_WIDTH+AW+1)-1:0] fifo_at_neck, afifo_at_tail;`
94			`reg [(DW+1)-1:0] dfifo_at_tail;`
95
96			`// We're going to need to keep track of transaction bursts in progress,`
97			`// since the wishbone doesn't. For this, we'll use a FIFO, but with`
98			`// multiple pointers:`
99			`//`
100			`// fifo_head - pointer to where to write the next incoming`
101			`// bus request .. adjusted when`
102			`// (o_axi_arready)&&(i_axi_arvalid)`
103			`// fifo_neck - pointer to where to read from the FIFO in`
104			`// order to issue another request. Used`
105			`// when (o_wb_stb)&&(!i_wb_stall)`
106			`// fifo_torso - pointer to where to write a wishbone`
107			`// transaction upon return.`
108			`// when (i_ack)`
109			`// fifo_tail - pointer to where the last transaction is to`
110			`// be retired when`
111			`// (i_axi_rvalid)&&(i_axi_rready)`
112			`//`
113			`// All of these are to be set to zero upon a reset signal.`
114			`//`
115			`reg [LGFIFO-1:0] fifo_head, fifo_neck, fifo_torso, fifo_tail;`
116
117			`// Since we need to insure that these pointers wrap properly at`
118			`// LGFIFO bits, and since it is confusing to do that within IF`
119			`// statements,`
120			`wire [LGFIFO-1:0] next_head, next_neck, next_torso, next_tail,`
121			`almost_head;`
122			`wire fifo_full;`
123			`assign next_head = fifo_head + 1;`
124			`assign next_neck = fifo_neck + 1;`
125			`assign next_torso = fifo_torso + 1;`
126			`assign next_tail = fifo_tail + 1;`
127			`assign almost_head = fifo_head + 1;`
128
129			`assign fifo_full = (almost_head == fifo_tail);`
130
131			`reg wr_last, filling_fifo, incr;`
132			`reg [7:0] len;`
133			`reg [(AW-1):0] wr_fifo_addr;`
134			`reg [(C_AXI_ID_WIDTH-1):0] wr_fifo_id;`
135
136			`//`
137			`//`
138			`//`
139			`//`
140			`// Here's our plan: Any time READY & VALID are both true, initiate a`
141			`// transfer (unless one is ongoing). Hold READY false while initiating`
142			`// any burst transaction. Keep the request RID and burst length stuffs`
143			`// into a FIFO.`
144			`// queue are both valid, issue the wishbone read request. Once a read`
145			`// request returns, retire the value in the FIFO queue.`
146			`//`
147			`// The FIFO queue must include:`
148			`//`
149			`// RQ, ADDR, LAST`
150			`//`
151			`initial len = 0;`
152			`initial filling_fifo = 0;`
153			`initial fifo_head = 0;`
154			`always @(posedge i_axi_clk)`
155			`begin`
156			`wr_last <= 1'b0;`
157
158			`if (filling_fifo)`
159			`begin`
160			`if (!fifo_full)`
161			`begin`
162			`len <= len - 1;`
163			`if (len == 1)`
164			`filling_fifo <= 1'b0;`
165			`fifo_head <= next_head;`
166			`wr_fifo_addr <= wr_fifo_addr`
167			`+ {{(AW-1){1'b0}}, incr};`
168			`wr_last <= (len == 1);`
169			`end`
170			`end else begin`
171			`wr_fifo_addr <= i_axi_araddr[(C_AXI_ADDR_WIDTH-1):(C_AXI_ADDR_WIDTH-AW)];`
172			`wr_fifo_id <= i_axi_arid;`
173			`incr <= i_axi_arburst[0];`
174			`if ((o_axi_arready)&&(i_axi_arvalid))`
175			`begin`
176			`fifo_head <= next_head;`
177			`len <= i_axi_arlen;`
178			`filling_fifo <= (i_axi_arlen != 0);`
179			`wr_last <= 1'b1;`
180			`end`
181			`end`
182
183			`if (w_reset)`
184			`begin`
185			`len <= 0;`
186			`filling_fifo <= 1'b0;`
187			`fifo_head <= 0;`
188			`end`
189			`end`
190
191			`always @(posedge i_axi_clk)`
192			`afifo[fifo_head] <= { wr_fifo_id, wr_last, wr_fifo_addr };`
193
194			`reg err_state;`
195			`initial o_wb_cyc = 1'b0;`
196			`initial o_wb_stb = 1'b0;`
197			`initial fifo_neck = 0;`
198			`initial fifo_torso = 0;`
199			`initial err_state = 0;`
200			`always @(posedge i_axi_clk)`
201			`begin`
202			`if (w_reset)`
203			`begin`
204			`o_wb_cyc <= 1'b0;`
205			`o_wb_stb <= 1'b0;`
206
207			`fifo_neck <= 0;`
208			`fifo_torso <= 0;`
209
210			`err_state <= 0;`
211			`end else if (o_wb_stb)`
212			`begin`
213			`if (i_wb_err)`
214			`begin`
215			`o_wb_stb <= 1'b0;`
216			`err_state <= 1'b1;`
217			`end else if (!i_wb_stall)`
218			`begin`
219			`o_wb_stb <= (fifo_head != next_neck);`
220			`// && (WBMODE != "B3SINGLE");`
221			`// o_wb_cyc <= (WBMODE != "B3SINGLE");`
222			`end`
223
224			`if (!i_wb_stall)`
225			`fifo_neck <= next_neck;`
226			`if (i_wb_ack)`
227			`fifo_torso <= next_torso;`
228			`end else if (err_state)`
229			`begin`
230			`fifo_torso <= next_torso;`
231			`if (fifo_neck == next_torso)`
232			`err_state <= 1'b0;`
233			`o_wb_cyc <= 1'b0;`
234			`end else if (o_wb_cyc)`
235			`begin`
236			`if (i_wb_ack)`
237			`fifo_torso <= next_torso;`
238			`if (fifo_neck == next_torso)`
239			`o_wb_cyc <= 1'b0;`
240			`end else if (fifo_neck != fifo_head)`
241			`begin`
242			`o_wb_cyc <= 1'b1;`
243			`o_wb_stb <= 1'b1;`
244			`end`
245			`end`
246
247			`always @(posedge i_axi_clk)`
248			`fifo_at_neck <= afifo[fifo_neck];`
249			`assign o_wb_addr = fifo_at_neck[(AW-1):0];`
250
251			`always @(posedge i_axi_clk)`
252			`dfifo[fifo_torso] <= { (err_state)\|\|(i_wb_err), i_wb_data };`
253
254
255			`always @(posedge i_axi_clk)`
256			`if (w_reset)`
257			`fifo_tail <= 0;`
258			`else if ((o_axi_rvalid)&&(i_axi_rready))`
259			`fifo_tail <= next_tail;`
260
261			`always @(posedge i_axi_clk)`
262			`begin`
263			`afifo_at_tail <= afifo[fifo_tail];`
264			`dfifo_at_tail <= dfifo[fifo_tail];`
265			`// o_axi_rdata <= dfifo[fifo_tail];`
266			`// o_axi_rlast <= afifo[fifo_tail];`
267			`// o_axi_rid <= afifo[fifo_tail];`
268			`end`
269			`assign o_axi_rlast = afifo_at_tail[AW];`
270			`assign o_axi_rid = afifo_at_tail[(C_AXI_ID_WIDTH+AW):(AW+1)];`
271			`assign o_axi_rresp = { (2){dfifo_at_tail[DW]} };`
272			`assign o_axi_rdata = dfifo_at_tail[(DW-1):0];`
273
274			`initial o_axi_rvalid = 1'b0;`
275			`always @(posedge i_axi_clk)`
276			`if (w_reset)`
277			`o_axi_rvalid <= 0;`
278			`else if (fifo_tail != fifo_neck)`
279			`o_axi_rvalid <= (fifo_tail != fifo_neck + 1);`
280
281			`assign o_axi_arready = (!fifo_full)&&(!filling_fifo);`
282
283			`// Make Verilator happy`
284			`// verilator lint_off UNUSED`
285			`wire [(C_AXI_ID_WIDTH+1)+(C_AXI_ADDR_WIDTH-AW)`
286			`+3+1+1+4+3+4-1:0] unused;`
287			`assign unused = { i_axi_arsize, i_axi_arburst[1],`
288			`i_axi_arlock, i_axi_arcache, i_axi_arprot,`
289			`i_axi_arqos,`
290			`fifo_at_neck[(C_AXI_ID_WIDTH+AW+1)-1:AW],`
291			`i_axi_araddr[(C_AXI_ADDR_WIDTH-AW-1):0] };`
292			`// verilator lint_on UNUSED`
293
294			`ifdef FORMAL
295			`reg f_past_valid;`
296			`initial f_past_valid = 1'b0;`
297			`always @(posedge i_axi_clk)`
298			`f_past_valid <= 1'b1;`
299
300			`wire [LGFIFO-1:0] f_fifo_used, f_fifo_neck_used,`
301			`f_fifo_torso_used;`
302			`assign f_fifo_used = fifo_head - fifo_tail;`
303			`assign f_fifo_neck_used = fifo_head - fifo_neck;`
304			`assign f_fifo_torso_used = fifo_head - fifo_torso;`
305
306			`always @(*)`
307			`assert((f_fifo_used < {(LGFIFO){1'b1}})\|\|(!o_axi_arready));`
308			`always @(*)`
309			`assert(f_fifo_neck_used <= f_fifo_used);`
310			`always @(*)`
311			`assert(f_fifo_torso_used <= f_fifo_used);`
312
313			`always @(posedge i_axi_clk)`
314			`if ((f_past_valid)&&(!$past(i_axi_reset_n)))`
315			`assert(f_fifo_used == 0);`
316
317			`endif
318			`endmodule`