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

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [aximwr2wbsp.v] - Blame information for rev 8

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


////////////////////////////////////////////////////////////////////////////////
//
// Filename:    aximwr2wbsp.v
//
// Project:     Pipelined Wishbone to AXI converter
//
// Purpose:     Convert the three AXI4 write channels to a single wishbone
//              channel to write the results.
//
//      Still need to implement the lock feature.
//
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-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 aximwr2wbsp #(
        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,
        parameter LGFIFO                =  4
        ) (
        input   wire                    i_axi_clk,      // System clock
        input   wire                    i_axi_reset_n,
 
// AXI write address channel signals
        output  wire                    o_axi_awready, // Slave is ready to accept
        input   wire    [C_AXI_ID_WIDTH-1:0]     i_axi_awid,     // Write ID
        input   wire    [C_AXI_ADDR_WIDTH-1:0]   i_axi_awaddr,   // Write address
        input   wire    [7:0]            i_axi_awlen,    // Write Burst Length
        input   wire    [2:0]            i_axi_awsize,   // Write Burst size
        input   wire    [1:0]            i_axi_awburst,  // Write Burst type
        input   wire    [0:0]             i_axi_awlock,   // Write lock type
        input   wire    [3:0]            i_axi_awcache,  // Write Cache type
        input   wire    [2:0]            i_axi_awprot,   // Write Protection type
        input   wire    [3:0]            i_axi_awqos,    // Write Quality of Svc
        input   wire                    i_axi_awvalid,  // Write address valid
 
// AXI write data channel signals
        output  wire                    o_axi_wready,  // Write data ready
        input   wire    [C_AXI_DATA_WIDTH-1:0]   i_axi_wdata,    // Write data
        input   wire    [C_AXI_DATA_WIDTH/8-1:0] i_axi_wstrb,    // Write strobes
        input   wire                    i_axi_wlast,    // Last write transaction   
        input   wire                    i_axi_wvalid,   // Write valid
 
// AXI write response channel signals
        output  wire [C_AXI_ID_WIDTH-1:0] o_axi_bid,     // Response ID
        output  wire [1:0]               o_axi_bresp,    // Write response
        output  wire                    o_axi_bvalid,  // Write reponse valid
        input   wire                    i_axi_bready,  // 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,
        output  wire [(C_AXI_DATA_WIDTH-1):0]    o_wb_data,
        output  wire [(C_AXI_DATA_WIDTH/8-1):0]  o_wb_sel,
        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     [LGFIFO-1:0]     fifo_ahead, fifo_dhead, fifo_neck, fifo_torso,
                                fifo_tail;
        wire    [LGFIFO-1:0]     next_ahead, next_dhead, next_neck, next_torso,
                                next_tail;
        assign  next_ahead = fifo_ahead + 1;
        assign  next_dhead = fifo_dhead + 1;
        assign  next_neck  = fifo_neck  + 1;
        assign  next_torso = fifo_torso + 1;
        assign  next_tail  = fifo_tail  + 1;
 
        reg     [(C_AXI_ID_WIDTH+AW)-1:0]        afifo   [0:((1<<(LGFIFO))-1)];
        reg     [(DW + DW/8)-1:0]                dfifo   [0:((1<<(LGFIFO))-1)];
        reg     [((1<<(LGFIFO))-1):0]            efifo;
 
        reg     [(C_AXI_ID_WIDTH+AW)-1:0]        afifo_at_neck, afifo_at_tail;
        reg     [(DW + DW/8)-1:0]                dfifo_at_neck;
        reg                                     efifo_at_tail;
 
        reg     filling_fifo, incr;
        reg     [7:0]    len;
        reg     [(AW-1):0]       wr_fifo_addr;
        reg     [(C_AXI_ID_WIDTH-1):0]   wr_fifo_id;
 
        wire    axi_aw_req, axi_wr_req;
        assign  axi_aw_req = (o_axi_awready)&&(i_axi_awvalid);
        assign  axi_wr_req = (o_axi_wready)&&(i_axi_wvalid);
 
        wire    fifo_full;
        assign  fifo_full = (next_ahead == fifo_tail)||(next_dhead ==fifo_tail);
 
        initial fifo_ahead = 0;
        initial fifo_dhead = 0;
        always @(posedge i_axi_clk)
        begin
                if (filling_fifo)
                begin
                        if (!fifo_full)
                        begin
                                len <= len - 1;
                                if (len == 1)
                                        filling_fifo <= 1'b0;
                                fifo_ahead <= next_ahead;
                                wr_fifo_addr <= wr_fifo_addr
                                        + {{(AW-1){1'b0}},incr};
                        end
                end else begin
                        wr_fifo_addr <= i_axi_awaddr[(C_AXI_ADDR_WIDTH-1):(C_AXI_ADDR_WIDTH-AW)];
                        wr_fifo_id   <= i_axi_awid;
                        incr         <= i_axi_awburst[0];
                        if (axi_aw_req)
                        begin
                                fifo_ahead <= next_ahead;
                                len <= i_axi_awlen;
                                filling_fifo <= (i_axi_awlen != 0);
                        end
                end
 
                if (w_reset)
                begin
                        fifo_ahead <= 0;
                        len <= 0;
                        filling_fifo <= 0;
                end
        end
 
        always @(posedge i_axi_clk)
                afifo[fifo_ahead] <= { wr_fifo_id, wr_fifo_addr };
 
        initial fifo_dhead = 0;
        always @(posedge i_axi_clk)
                if (w_reset)
                        fifo_dhead <= 0;
                else if (axi_wr_req)
                        fifo_dhead <= next_dhead;
 
        always @(posedge i_axi_clk)
                dfifo[fifo_dhead] <= { i_axi_wstrb, i_axi_wdata };
 
 
        reg     err_state;
 
        initial o_wb_cyc   = 0;
        initial o_wb_stb   = 0;
        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 <= 0;
                        o_wb_stb <= 0;
 
                        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'b0;
                        end
                        else if (!i_wb_stall)
                                o_wb_stb <= (fifo_ahead != next_neck)
                                        &&(fifo_dhead != next_neck);
 
                        if ((!i_wb_stall)&&(fifo_neck != fifo_ahead)&&(fifo_neck != fifo_dhead))
                                fifo_neck <= next_neck;
 
                        if (i_wb_ack)
                                fifo_torso <= next_torso;
 
                        if (fifo_neck == next_torso)
                                o_wb_cyc <= 1'b0;
                end else if (err_state)
                begin
                        o_wb_cyc <= 1'b0;
                        if (fifo_torso != fifo_neck)
                                fifo_torso <= next_torso;
                        if (fifo_neck == next_torso)
                                err_state <= 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_ahead!= fifo_neck)&&(fifo_dhead != fifo_neck))
                begin
                        o_wb_cyc <= 1;
                        o_wb_stb <= 1;
                end
        end
 
        initial efifo = 0;
        always @(posedge i_axi_clk)
                if(w_reset)
                        efifo <= 0;
                else
                        efifo[fifo_torso] <= (i_wb_err)||(err_state);
 
        always @(posedge i_axi_clk)
                afifo_at_neck <= afifo[fifo_neck];
        assign  o_wb_addr = afifo_at_neck[(AW-1):0];
 
        always @(posedge i_axi_clk)
                dfifo_at_neck <= dfifo[fifo_neck];
        assign  o_wb_data = dfifo_at_neck[DW-1:0];
        assign  o_wb_sel  = dfifo_at_neck[(DW+(DW/8))-1:DW];
 
        initial fifo_tail = 0;
        always @(posedge i_axi_clk)
                if (w_reset)
                        fifo_tail <= 0;
                else if ((o_axi_bvalid)&&(i_axi_bready))
                        fifo_tail <= next_tail;
 
        always @(posedge i_axi_clk)
                afifo_at_tail <= afifo[fifo_tail];
        always @(posedge i_axi_clk)
                efifo_at_tail <= efifo[fifo_tail];
 
        assign  o_axi_bid   = afifo_at_tail[(C_AXI_ID_WIDTH+AW)-1:AW];
        assign  o_axi_bresp = {(2){efifo_at_tail}};
 
        assign  o_axi_bvalid  = (fifo_tail  != fifo_torso);
        assign  o_axi_awready = (next_ahead != fifo_tail);
        assign  o_axi_wready  = (next_dhead != fifo_tail);
 
        // Make Verilator happy
        // verilator lint_on  UNUSED
        wire    [(C_AXI_ID_WIDTH+AW+C_AXI_ADDR_WIDTH-AW)
                +(1)+1+3+1+4+3+4-1:0]    unused;
        assign  unused = { i_axi_awburst[1], i_axi_awsize,
                        i_axi_awlock, i_axi_awcache, i_axi_awprot,
                        i_axi_awqos, i_axi_wlast,
                        afifo_at_neck[(C_AXI_ID_WIDTH+AW-1):AW],
                        afifo_at_tail[(AW-1):0],
                        i_axi_awaddr[(C_AXI_ADDR_WIDTH-AW)-1:0] };
        // verilator lint_off UNUSED
 
`ifdef  FORMAL
        always @(*)
                assume(!i_axi_awburst[1]);
 
        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_afifo_used, f_dfifo_used,
                                f_fifo_neck_used, f_fifo_torso_used;
 
        assign  f_afifo_used      = fifo_ahead - fifo_tail;
        assign  f_dfifo_used      = fifo_dhead - fifo_tail;
        assign  f_fifo_neck_used  = fifo_dhead - fifo_neck;
        assign  f_fifo_torso_used = fifo_dhead - fifo_torso;
 
        always @(*)
                assert((f_afifo_used < {(LGFIFO){1'b1}})||(!o_axi_awready));
        always @(*)
                assert((f_dfifo_used < {(LGFIFO){1'b1}})||(!o_axi_wready));
        always @(*)
                assert(f_fifo_neck_used  <= f_dfifo_used);
        always @(*)
                assert(f_fifo_torso_used <= f_dfifo_used);
        always @(*)
                assert((!o_wb_stb)||
                        ((fifo_neck != fifo_ahead)
                                &&(fifo_neck != fifo_dhead)));
`endif
endmodule
 

Browse

Tools

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [aximwr2wbsp.v] - Blame information for rev 8

Line No.	Rev	Author	Line
1	8	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
2			`//`
3			`// Filename: aximwr2wbsp.v`
4			`//`
5			`// Project: Pipelined Wishbone to AXI converter`
6			`//`
7			`// Purpose: Convert the three AXI4 write channels to a single wishbone`
8			`// channel to write the results.`
9			`//`
10			`// Still need to implement the lock feature.`
11			`//`
12			`// Creator: Dan Gisselquist, Ph.D.`
13			`// Gisselquist Technology, LLC`
14			`//`
15			`////////////////////////////////////////////////////////////////////////////////`
16			`//`
17			`// Copyright (C) 2015-2016, Gisselquist Technology, LLC`
18			`//`
19			`// This program is free software (firmware): you can redistribute it and/or`
20			`// modify it under the terms of the GNU General Public License as published`
21			`// by the Free Software Foundation, either version 3 of the License, or (at`
22			`// your option) any later version.`
23			`//`
24			`// This program is distributed in the hope that it will be useful, but WITHOUT`
25			`// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or`
26			`// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License`
27			`// for more details.`
28			`//`
29			`// You should have received a copy of the GNU General Public License along`
30			`// with this program. (It's in the $(ROOT)/doc directory, run make with no`
31			`// target there if the PDF file isn't present.) If not, see`
32			`// <http://www.gnu.org/licenses/> for a copy.`
33			`//`
34			`// License: GPL, v3, as defined and found on www.gnu.org,`
35			`// http://www.gnu.org/licenses/gpl.html`
36			`//`
37			`//`
38			`////////////////////////////////////////////////////////////////////////////////`
39			`//`
40			`//`
41			`default_nettype none
42			`//`
43			`//`
44			`module aximwr2wbsp #(`
45			`parameter C_AXI_ID_WIDTH = 6, // The AXI id width used for R&W`
46			`// This is an int between 1-16`
47			`parameter C_AXI_DATA_WIDTH = 32,// Width of the AXI R&W data`
48			`parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width`
49			`parameter AW = 26,`
50			`parameter LGFIFO = 4`
51			`) (`
52			`input wire i_axi_clk, // System clock`
53			`input wire i_axi_reset_n,`
54
55			`// AXI write address channel signals`
56			`output wire o_axi_awready, // Slave is ready to accept`
57			`input wire [C_AXI_ID_WIDTH-1:0] i_axi_awid, // Write ID`
58			`input wire [C_AXI_ADDR_WIDTH-1:0] i_axi_awaddr, // Write address`
59			`input wire [7:0] i_axi_awlen, // Write Burst Length`
60			`input wire [2:0] i_axi_awsize, // Write Burst size`
61			`input wire [1:0] i_axi_awburst, // Write Burst type`
62			`input wire [0:0] i_axi_awlock, // Write lock type`
63			`input wire [3:0] i_axi_awcache, // Write Cache type`
64			`input wire [2:0] i_axi_awprot, // Write Protection type`
65			`input wire [3:0] i_axi_awqos, // Write Quality of Svc`
66			`input wire i_axi_awvalid, // Write address valid`
67
68			`// AXI write data channel signals`
69			`output wire o_axi_wready, // Write data ready`
70			`input wire [C_AXI_DATA_WIDTH-1:0] i_axi_wdata, // Write data`
71			`input wire [C_AXI_DATA_WIDTH/8-1:0] i_axi_wstrb, // Write strobes`
72			`input wire i_axi_wlast, // Last write transaction`
73			`input wire i_axi_wvalid, // Write valid`
74
75			`// AXI write response channel signals`
76			`output wire [C_AXI_ID_WIDTH-1:0] o_axi_bid, // Response ID`
77			`output wire [1:0] o_axi_bresp, // Write response`
78			`output wire o_axi_bvalid, // Write reponse valid`
79			`input wire i_axi_bready, // Response ready`
80
81			`// We'll share the clock and the reset`
82			`output reg o_wb_cyc,`
83			`output reg o_wb_stb,`
84			`output wire [(AW-1):0] o_wb_addr,`
85			`output wire [(C_AXI_DATA_WIDTH-1):0] o_wb_data,`
86			`output wire [(C_AXI_DATA_WIDTH/8-1):0] o_wb_sel,`
87			`input wire i_wb_ack,`
88			`input wire i_wb_stall,`
89			`// input [(C_AXI_DATA_WIDTH-1):0] i_wb_data,`
90			`input wire i_wb_err`
91			`);`
92
93			`localparam DW = C_AXI_DATA_WIDTH;`
94
95			`wire w_reset;`
96			`assign w_reset = (i_axi_reset_n == 1'b0);`
97
98			`//`
99			`//`
100			`//`
101			`reg [LGFIFO-1:0] fifo_ahead, fifo_dhead, fifo_neck, fifo_torso,`
102			`fifo_tail;`
103			`wire [LGFIFO-1:0] next_ahead, next_dhead, next_neck, next_torso,`
104			`next_tail;`
105			`assign next_ahead = fifo_ahead + 1;`
106			`assign next_dhead = fifo_dhead + 1;`
107			`assign next_neck = fifo_neck + 1;`
108			`assign next_torso = fifo_torso + 1;`
109			`assign next_tail = fifo_tail + 1;`
110
111			`reg [(C_AXI_ID_WIDTH+AW)-1:0] afifo [0:((1<<(LGFIFO))-1)];`
112			`reg [(DW + DW/8)-1:0] dfifo [0:((1<<(LGFIFO))-1)];`
113			`reg [((1<<(LGFIFO))-1):0] efifo;`
114
115			`reg [(C_AXI_ID_WIDTH+AW)-1:0] afifo_at_neck, afifo_at_tail;`
116			`reg [(DW + DW/8)-1:0] dfifo_at_neck;`
117			`reg efifo_at_tail;`
118
119			`reg filling_fifo, incr;`
120			`reg [7:0] len;`
121			`reg [(AW-1):0] wr_fifo_addr;`
122			`reg [(C_AXI_ID_WIDTH-1):0] wr_fifo_id;`
123
124			`wire axi_aw_req, axi_wr_req;`
125			`assign axi_aw_req = (o_axi_awready)&&(i_axi_awvalid);`
126			`assign axi_wr_req = (o_axi_wready)&&(i_axi_wvalid);`
127
128			`wire fifo_full;`
129			`assign fifo_full = (next_ahead == fifo_tail)\|\|(next_dhead ==fifo_tail);`
130
131			`initial fifo_ahead = 0;`
132			`initial fifo_dhead = 0;`
133			`always @(posedge i_axi_clk)`
134			`begin`
135			`if (filling_fifo)`
136			`begin`
137			`if (!fifo_full)`
138			`begin`
139			`len <= len - 1;`
140			`if (len == 1)`
141			`filling_fifo <= 1'b0;`
142			`fifo_ahead <= next_ahead;`
143			`wr_fifo_addr <= wr_fifo_addr`
144			`+ {{(AW-1){1'b0}},incr};`
145			`end`
146			`end else begin`
147			`wr_fifo_addr <= i_axi_awaddr[(C_AXI_ADDR_WIDTH-1):(C_AXI_ADDR_WIDTH-AW)];`
148			`wr_fifo_id <= i_axi_awid;`
149			`incr <= i_axi_awburst[0];`
150			`if (axi_aw_req)`
151			`begin`
152			`fifo_ahead <= next_ahead;`
153			`len <= i_axi_awlen;`
154			`filling_fifo <= (i_axi_awlen != 0);`
155			`end`
156			`end`
157
158			`if (w_reset)`
159			`begin`
160			`fifo_ahead <= 0;`
161			`len <= 0;`
162			`filling_fifo <= 0;`
163			`end`
164			`end`
165
166			`always @(posedge i_axi_clk)`
167			`afifo[fifo_ahead] <= { wr_fifo_id, wr_fifo_addr };`
168
169			`initial fifo_dhead = 0;`
170			`always @(posedge i_axi_clk)`
171			`if (w_reset)`
172			`fifo_dhead <= 0;`
173			`else if (axi_wr_req)`
174			`fifo_dhead <= next_dhead;`
175
176			`always @(posedge i_axi_clk)`
177			`dfifo[fifo_dhead] <= { i_axi_wstrb, i_axi_wdata };`
178
179
180			`reg err_state;`
181
182			`initial o_wb_cyc = 0;`
183			`initial o_wb_stb = 0;`
184			`initial fifo_neck = 0;`
185			`initial fifo_torso = 0;`
186			`initial err_state = 0;`
187			`always @(posedge i_axi_clk)`
188			`begin`
189			`if (w_reset)`
190			`begin`
191			`o_wb_cyc <= 0;`
192			`o_wb_stb <= 0;`
193
194			`fifo_neck <= 0;`
195			`fifo_torso <= 0;`
196
197			`err_state <= 0;`
198			`end else if (o_wb_stb)`
199			`begin`
200			`if (i_wb_err)`
201			`begin`
202			`o_wb_stb <= 1'b0;`
203			`err_state <= 1'b0;`
204			`end`
205			`else if (!i_wb_stall)`
206			`o_wb_stb <= (fifo_ahead != next_neck)`
207			`&&(fifo_dhead != next_neck);`
208
209			`if ((!i_wb_stall)&&(fifo_neck != fifo_ahead)&&(fifo_neck != fifo_dhead))`
210			`fifo_neck <= next_neck;`
211
212			`if (i_wb_ack)`
213			`fifo_torso <= next_torso;`
214
215			`if (fifo_neck == next_torso)`
216			`o_wb_cyc <= 1'b0;`
217			`end else if (err_state)`
218			`begin`
219			`o_wb_cyc <= 1'b0;`
220			`if (fifo_torso != fifo_neck)`
221			`fifo_torso <= next_torso;`
222			`if (fifo_neck == next_torso)`
223			`err_state <= 1'b0;`
224			`end else if (o_wb_cyc)`
225			`begin`
226			`if (i_wb_ack)`
227			`fifo_torso <= next_torso;`
228			`if (fifo_neck == next_torso)`
229			`o_wb_cyc <= 1'b0;`
230			`end else if((fifo_ahead!= fifo_neck)&&(fifo_dhead != fifo_neck))`
231			`begin`
232			`o_wb_cyc <= 1;`
233			`o_wb_stb <= 1;`
234			`end`
235			`end`
236
237			`initial efifo = 0;`
238			`always @(posedge i_axi_clk)`
239			`if(w_reset)`
240			`efifo <= 0;`
241			`else`
242			`efifo[fifo_torso] <= (i_wb_err)\|\|(err_state);`
243
244			`always @(posedge i_axi_clk)`
245			`afifo_at_neck <= afifo[fifo_neck];`
246			`assign o_wb_addr = afifo_at_neck[(AW-1):0];`
247
248			`always @(posedge i_axi_clk)`
249			`dfifo_at_neck <= dfifo[fifo_neck];`
250			`assign o_wb_data = dfifo_at_neck[DW-1:0];`
251			`assign o_wb_sel = dfifo_at_neck[(DW+(DW/8))-1:DW];`
252
253			`initial fifo_tail = 0;`
254			`always @(posedge i_axi_clk)`
255			`if (w_reset)`
256			`fifo_tail <= 0;`
257			`else if ((o_axi_bvalid)&&(i_axi_bready))`
258			`fifo_tail <= next_tail;`
259
260			`always @(posedge i_axi_clk)`
261			`afifo_at_tail <= afifo[fifo_tail];`
262			`always @(posedge i_axi_clk)`
263			`efifo_at_tail <= efifo[fifo_tail];`
264
265			`assign o_axi_bid = afifo_at_tail[(C_AXI_ID_WIDTH+AW)-1:AW];`
266			`assign o_axi_bresp = {(2){efifo_at_tail}};`
267
268			`assign o_axi_bvalid = (fifo_tail != fifo_torso);`
269			`assign o_axi_awready = (next_ahead != fifo_tail);`
270			`assign o_axi_wready = (next_dhead != fifo_tail);`
271
272			`// Make Verilator happy`
273			`// verilator lint_on UNUSED`
274			`wire [(C_AXI_ID_WIDTH+AW+C_AXI_ADDR_WIDTH-AW)`
275			`+(1)+1+3+1+4+3+4-1:0] unused;`
276			`assign unused = { i_axi_awburst[1], i_axi_awsize,`
277			`i_axi_awlock, i_axi_awcache, i_axi_awprot,`
278			`i_axi_awqos, i_axi_wlast,`
279			`afifo_at_neck[(C_AXI_ID_WIDTH+AW-1):AW],`
280			`afifo_at_tail[(AW-1):0],`
281			`i_axi_awaddr[(C_AXI_ADDR_WIDTH-AW)-1:0] };`
282			`// verilator lint_off UNUSED`
283
284			`ifdef FORMAL
285			`always @(*)`
286			`assume(!i_axi_awburst[1]);`
287
288			`reg f_past_valid;`
289			`initial f_past_valid = 1'b0;`
290			`always @(posedge i_axi_clk)`
291			`f_past_valid <= 1'b1;`
292
293			`wire [LGFIFO-1:0] f_afifo_used, f_dfifo_used,`
294			`f_fifo_neck_used, f_fifo_torso_used;`
295
296			`assign f_afifo_used = fifo_ahead - fifo_tail;`
297			`assign f_dfifo_used = fifo_dhead - fifo_tail;`
298			`assign f_fifo_neck_used = fifo_dhead - fifo_neck;`
299			`assign f_fifo_torso_used = fifo_dhead - fifo_torso;`
300
301			`always @(*)`
302			`assert((f_afifo_used < {(LGFIFO){1'b1}})\|\|(!o_axi_awready));`
303			`always @(*)`
304			`assert((f_dfifo_used < {(LGFIFO){1'b1}})\|\|(!o_axi_wready));`
305			`always @(*)`
306			`assert(f_fifo_neck_used <= f_dfifo_used);`
307			`always @(*)`
308			`assert(f_fifo_torso_used <= f_dfifo_used);`
309			`always @(*)`
310			`assert((!o_wb_stb)\|\|`
311			`((fifo_neck != fifo_ahead)`
312			`&&(fifo_neck != fifo_dhead)));`
313			`endif
314			`endmodule`
315