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

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [axlite2wbsp.v] - Blame information for rev 16

Details | Compare with Previous | View Log


////////////////////////////////////////////////////////////////////////////////
//
// Filename:    axlite2wbsp.v
//
// Project:     Pipelined Wishbone to AXI converter
//
// Purpose:     Take an AXI lite input, and convert it into WB.
//
//      We'll treat AXI as two separate busses: one for writes, another for
//      reads, further, we'll insist that the two channels AXI uses for writes
//      combine into one channel for our purposes.
//
//
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2016-2019, Gisselquist Technology, LLC
//
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs.  (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:     LGPL, v3, as defined and found on www.gnu.org,
//              http://www.gnu.org/licenses/lgpl.html
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype        none
//
module axlite2wbsp( i_clk, i_axi_reset_n,
        //
        o_axi_awready, i_axi_awaddr, i_axi_awcache, i_axi_awprot,i_axi_awvalid,
        //
        o_axi_wready, i_axi_wdata, i_axi_wstrb, i_axi_wvalid,
        //
        o_axi_bresp, o_axi_bvalid, i_axi_bready,
        //
        o_axi_arready, i_axi_araddr, i_axi_arcache, i_axi_arprot, i_axi_arvalid,
        //
        o_axi_rresp, o_axi_rvalid, o_axi_rdata, i_axi_rready,
        //
        // Wishbone interface
        o_reset, o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err);
        //
        parameter C_AXI_DATA_WIDTH      = 32;// Width of the AXI R&W data
        parameter C_AXI_ADDR_WIDTH      = 28;   // AXI Address width
        parameter               LGFIFO = 4;
        parameter               F_MAXSTALL = 3;
        parameter               F_MAXDELAY = 3;
        parameter       [0:0]     OPT_READONLY  = 1'b0;
        parameter       [0:0]     OPT_WRITEONLY = 1'b0;
        localparam      F_LGDEPTH = LGFIFO+1;
        //
        input   wire                    i_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_ADDR_WIDTH-1:0]   i_axi_awaddr;   // Write address
        input   wire    [3:0]            i_axi_awcache;  // Write Cache type
        input   wire    [2:0]            i_axi_awprot;   // Write Protection type
        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_wvalid;   // Write valid
 
// AXI write response channel signals
        output  wire [1:0]               o_axi_bresp;    // Write response
        output  wire                    o_axi_bvalid;  // Write reponse valid
        input   wire                    i_axi_bready;  // Response ready
 
// AXI read address channel signals
        output  wire                    o_axi_arready;  // Read address ready
        input   wire    [C_AXI_ADDR_WIDTH-1:0]   i_axi_araddr;   // Read address
        input   wire    [3:0]            i_axi_arcache;  // Read Cache type
        input   wire    [2:0]            i_axi_arprot;   // Read Protection type
        input   wire                    i_axi_arvalid;  // Read address valid
 
// AXI read data channel signals
        output  wire [1:0]               o_axi_rresp;   // Read response
        output  wire                    o_axi_rvalid;  // Read reponse valid
        output  wire [C_AXI_DATA_WIDTH-1:0] o_axi_rdata;    // Read data
        input   wire                    i_axi_rready;  // Read Response ready
 
        // We'll share the clock and the reset
        output  wire                    o_reset;
        output  wire                    o_wb_cyc;
        output  wire                    o_wb_stb;
        output  wire                    o_wb_we;
        output  wire [(C_AXI_ADDR_WIDTH-3):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   wire [(C_AXI_DATA_WIDTH-1):0]            i_wb_data;
        input   wire                    i_wb_err;
 
 
        localparam DW = C_AXI_DATA_WIDTH;
        localparam AW = C_AXI_ADDR_WIDTH-2;
        //
        //
        //
 
        wire    [(AW-1):0]                       w_wb_addr, r_wb_addr;
        wire    [(C_AXI_DATA_WIDTH-1):0] w_wb_data;
        wire    [(C_AXI_DATA_WIDTH/8-1):0]       w_wb_sel;
        wire    r_wb_err, r_wb_cyc, r_wb_stb, r_wb_stall, r_wb_ack;
        wire    w_wb_err, w_wb_cyc, w_wb_stb, w_wb_stall, w_wb_ack;
 
        // verilator lint_off UNUSED
        wire    r_wb_we, w_wb_we;
 
        assign  r_wb_we = 1'b0;
        assign  w_wb_we = 1'b1;
        // verilator lint_on  UNUSED
 
`ifdef  FORMAL
        wire    [LGFIFO:0]       f_wr_fifo_first, f_rd_fifo_first,
                                f_wr_fifo_mid,   f_rd_fifo_mid,
                                f_wr_fifo_last,  f_rd_fifo_last;
        wire    [(F_LGDEPTH-1):0]        f_wb_nreqs, f_wb_nacks,
                                        f_wb_outstanding;
        wire    [(F_LGDEPTH-1):0]        f_wb_wr_nreqs, f_wb_wr_nacks,
                                        f_wb_wr_outstanding;
        wire    [(F_LGDEPTH-1):0]        f_wb_rd_nreqs, f_wb_rd_nacks,
                                        f_wb_rd_outstanding;
        wire                    f_pending_awvalid, f_pending_wvalid;
`endif
 
        //
        // AXI-lite write channel to WB processing
        //
        generate if (!OPT_READONLY)
        begin : AXI_WR
        axilwr2wbsp #(
                // .F_LGDEPTH(F_LGDEPTH),
                // .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
                .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), // .AW(AW),
                .LGFIFO(LGFIFO))
                axi_write_decoder(
                        .i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
                        //
                        .o_axi_awready(o_axi_awready),
                        .i_axi_awaddr( i_axi_awaddr),
                        .i_axi_awcache(i_axi_awcache),
                        .i_axi_awprot( i_axi_awprot),
                        .i_axi_awvalid(i_axi_awvalid),
                        //
                        .o_axi_wready( o_axi_wready),
                        .i_axi_wdata(  i_axi_wdata),
                        .i_axi_wstrb(  i_axi_wstrb),
                        .i_axi_wvalid( i_axi_wvalid),
                        //
                        .o_axi_bresp(o_axi_bresp),
                        .o_axi_bvalid(o_axi_bvalid),
                        .i_axi_bready(i_axi_bready),
                        //
                        .o_wb_cyc(  w_wb_cyc),
                        .o_wb_stb(  w_wb_stb),
                        .o_wb_addr( w_wb_addr),
                        .o_wb_data( w_wb_data),
                        .o_wb_sel(  w_wb_sel),
                        .i_wb_ack(  w_wb_ack),
                        .i_wb_stall(w_wb_stall),
                        .i_wb_err(  w_wb_err)
`ifdef  FORMAL
                        ,
                        .f_first(f_wr_fifo_first),
                        .f_mid(  f_wr_fifo_mid),
                        .f_last( f_wr_fifo_last),
                        .f_wpending({ f_pending_awvalid, f_pending_wvalid })
`endif
                );
        end else begin
                assign  w_wb_cyc  = 0;
                assign  w_wb_stb  = 0;
                assign  w_wb_addr = 0;
                assign  w_wb_data = 0;
                assign  w_wb_sel  = 0;
                assign  o_axi_awready = 0;
                assign  o_axi_wready  = 0;
                assign  o_axi_bvalid  = (i_axi_wvalid);
                assign  o_axi_bresp   = 2'b11;
`ifdef  FORMAL
                assign  f_wr_fifo_first = 0;
                assign  f_wr_fifo_mid   = 0;
                assign  f_wr_fifo_last  = 0;
                assign  f_pending_awvalid=0;
                assign  f_pending_wvalid =0;
`endif
        end endgenerate
        assign  w_wb_we = 1'b1;
 
        //
        // AXI-lite read channel to WB processing
        //
        generate if (!OPT_WRITEONLY)
        begin : AXI_RD
        axilrd2wbsp #(
                // .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
                .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
                .LGFIFO(LGFIFO))
                axi_read_decoder(
                        .i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
                        //
                        .o_axi_arready(o_axi_arready),
                        .i_axi_araddr( i_axi_araddr),
                        .i_axi_arcache(i_axi_arcache),
                        .i_axi_arprot( i_axi_arprot),
                        .i_axi_arvalid(i_axi_arvalid),
                        //
                        .o_axi_rresp( o_axi_rresp),
                        .o_axi_rvalid(o_axi_rvalid),
                        .o_axi_rdata( o_axi_rdata),
                        .i_axi_rready(i_axi_rready),
                        //
                        .o_wb_cyc(  r_wb_cyc),
                        .o_wb_stb(  r_wb_stb),
                        .o_wb_addr( r_wb_addr),
                        .i_wb_ack(  r_wb_ack),
                        .i_wb_stall(r_wb_stall),
                        .i_wb_data( i_wb_data),
                        .i_wb_err(  r_wb_err)
`ifdef  FORMAL
                        ,
                        .f_first(f_rd_fifo_first),
                        .f_mid(  f_rd_fifo_mid),
                        .f_last( f_rd_fifo_last)
`endif
                        );
        end else begin
                assign  r_wb_cyc  = 0;
                assign  r_wb_stb  = 0;
                assign  r_wb_addr = 0;
                //
                assign o_axi_arready = 1'b1;
                assign o_axi_rvalid  = (i_axi_arvalid)&&(o_axi_arready);
                assign o_axi_rresp   = (i_axi_arvalid) ? 2'b11 : 2'b00;
                assign o_axi_rdata   = 0;
`ifdef  FORMAL
                assign  f_rd_fifo_first = 0;
                assign  f_rd_fifo_mid   = 0;
                assign  f_rd_fifo_last  = 0;
`endif
        end endgenerate
 
        //
        //
        // The arbiter that pastes the two sides together
        //
        //
        generate if (OPT_READONLY)
        begin : ARB_RD
                assign  o_wb_cyc  = r_wb_cyc;
                assign  o_wb_stb  = r_wb_stb;
                assign  o_wb_we   = 1'b0;
                assign  o_wb_addr = r_wb_addr;
                assign  o_wb_data = 32'h0;
                assign  o_wb_sel  = 0;
                assign  r_wb_ack  = i_wb_ack;
                assign  r_wb_stall= i_wb_stall;
                assign  r_wb_ack  = i_wb_ack;
                assign  r_wb_err  = i_wb_err;
 
`ifdef  FORMAL
                fwb_master #(.DW(DW), .AW(AW),
                        .F_LGDEPTH(F_LGDEPTH),
                        .F_MAX_STALL(F_MAXSTALL),
                        .F_MAX_ACK_DELAY(F_MAXDELAY))
                f_wb(i_clk, !i_axi_reset_n,
                        o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
                                o_wb_sel,
                        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
                        f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
 
                assign f_wb_rd_nreqs = f_wb_nreqs;
                assign f_wb_rd_nacks = f_wb_nacks;
                assign f_wb_rd_outstanding = f_wb_outstanding;
                //
                assign f_wb_wr_nreqs = 0;
                assign f_wb_wr_nacks = 0;
                assign f_wb_wr_outstanding = 0;
`endif
        end else if (OPT_WRITEONLY)
        begin : ARB_WR
                assign  o_wb_cyc  = w_wb_cyc;
                assign  o_wb_stb  = w_wb_stb;
                assign  o_wb_we   = 1'b1;
                assign  o_wb_addr = w_wb_addr;
                assign  o_wb_data = w_wb_data;
                assign  o_wb_sel  = w_wb_sel;
                assign  w_wb_ack  = i_wb_ack;
                assign  w_wb_stall= i_wb_stall;
                assign  w_wb_ack  = i_wb_ack;
                assign  w_wb_err  = i_wb_err;
 
`ifdef FORMAL
                fwb_master #(.DW(DW), .AW(AW),
                        .F_LGDEPTH(F_LGDEPTH),
                        .F_MAX_STALL(F_MAXSTALL),
                        .F_MAX_ACK_DELAY(F_MAXDELAY))
                f_wb(i_clk, !i_axi_reset_n,
                        o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
                                o_wb_sel,
                        i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
                        f_wb_nreqs, f_wb_nacks, f_wb_outstanding);
 
                assign f_wb_wr_nreqs = f_wb_nreqs;
                assign f_wb_wr_nacks = f_wb_nacks;
                assign f_wb_wr_outstanding = f_wb_outstanding;
                //
                assign f_wb_rd_nreqs = 0;
                assign f_wb_rd_nacks = 0;
                assign f_wb_rd_outstanding = 0;
`endif
        end else begin : ARB_WB
                wbarbiter       #(.DW(DW), .AW(AW),
                        .F_LGDEPTH(F_LGDEPTH),
                        .F_MAX_STALL(F_MAXSTALL),
                        .F_MAX_ACK_DELAY(F_MAXDELAY))
                        readorwrite(i_clk, !i_axi_reset_n,
                        r_wb_cyc, r_wb_stb, 1'b0, r_wb_addr, w_wb_data, w_wb_sel,
                                r_wb_ack, r_wb_stall, r_wb_err,
                        w_wb_cyc, w_wb_stb, 1'b1, w_wb_addr, w_wb_data, w_wb_sel,
                                w_wb_ack, w_wb_stall, w_wb_err,
                        o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,
                                i_wb_ack, i_wb_stall, i_wb_err
`ifdef  FORMAL
                        ,
                        f_wb_rd_nreqs, f_wb_rd_nacks, f_wb_rd_outstanding,
                        f_wb_wr_nreqs, f_wb_wr_nacks, f_wb_wr_outstanding,
                        f_wb_nreqs, f_wb_nacks, f_wb_outstanding
`endif
                        );
        end endgenerate
 
        assign  o_reset = (i_axi_reset_n == 1'b0);
 
`ifdef  FORMAL
        reg     f_past_valid;
 
        initial f_past_valid = 1'b0;
        always @(posedge i_clk)
                f_past_valid = 1'b1;
 
        initial assume(!i_axi_reset_n);
        always @(*)
        if (!f_past_valid)
                assume(!i_axi_reset_n);
 
        wire    [(F_LGDEPTH-1):0]        f_axi_rd_outstanding,
                                        f_axi_wr_outstanding,
                                        f_axi_awr_outstanding;
        wire    [(F_LGDEPTH-1):0]        f_axi_rd_id_outstanding,
                                        f_axi_awr_id_outstanding,
                                        f_axi_wr_id_outstanding;
        wire    [8:0]                    f_axi_wr_pending,
                                        f_axi_rd_count,
                                        f_axi_wr_count;
 
        faxil_slave #(
                        // .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
                        .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
                        .F_LGDEPTH(F_LGDEPTH),
                        .F_AXI_MAXWAIT(0),
                        .F_AXI_MAXDELAY(0))
                f_axi(.i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),
                        // AXI write address channnel
                        .i_axi_awready(o_axi_awready),
                        .i_axi_awaddr( i_axi_awaddr),
                        .i_axi_awcache(i_axi_awcache),
                        .i_axi_awprot( i_axi_awprot),
                        .i_axi_awvalid(i_axi_awvalid),
                        // AXI write data channel
                        .i_axi_wready( o_axi_wready),
                        .i_axi_wdata(  i_axi_wdata),
                        .i_axi_wstrb(  i_axi_wstrb),
                        .i_axi_wvalid( i_axi_wvalid),
                        // AXI write acknowledgement channel
                        .i_axi_bresp( o_axi_bresp),
                        .i_axi_bvalid(o_axi_bvalid),
                        .i_axi_bready(i_axi_bready),
                        // AXI read address channel
                        .i_axi_arready(o_axi_arready),
                        .i_axi_araddr( i_axi_araddr),
                        .i_axi_arcache(i_axi_arcache),
                        .i_axi_arprot( i_axi_arprot),
                        .i_axi_arvalid(i_axi_arvalid),
                        // AXI read data return
                        .i_axi_rresp(  o_axi_rresp),
                        .i_axi_rvalid( o_axi_rvalid),
                        .i_axi_rdata(  o_axi_rdata),
                        .i_axi_rready( i_axi_rready),
                        // Quantify where we are within a transaction
                        .f_axi_rd_outstanding( f_axi_rd_outstanding),
                        .f_axi_wr_outstanding( f_axi_wr_outstanding),
                        .f_axi_awr_outstanding(f_axi_awr_outstanding));
 
        wire    f_axi_ard_req, f_axi_awr_req, f_axi_wr_req,
                f_axi_rd_ack, f_axi_wr_ack;
 
        assign  f_axi_ard_req = (i_axi_arvalid)&&(o_axi_arready);
        assign  f_axi_awr_req = (i_axi_awvalid)&&(o_axi_awready);
        assign  f_axi_wr_req  = (i_axi_wvalid)&&(o_axi_wready);
        assign  f_axi_wr_ack  = (o_axi_bvalid)&&(i_axi_bready);
        assign  f_axi_rd_ack  = (o_axi_rvalid)&&(i_axi_rready);
 
        wire    [LGFIFO:0]       f_awr_fifo_axi_used,
                                f_dwr_fifo_axi_used,
                                f_rd_fifo_axi_used,
                                f_wr_fifo_wb_outstanding,
                                f_rd_fifo_wb_outstanding;
 
        assign  f_awr_fifo_axi_used = f_wr_fifo_first - f_wr_fifo_last;
        assign  f_rd_fifo_axi_used  = f_rd_fifo_first - f_rd_fifo_last;
        assign  f_wr_fifo_wb_outstanding = f_wr_fifo_first - f_wr_fifo_last;
        assign  f_rd_fifo_wb_outstanding = f_rd_fifo_first - f_rd_fifo_last;
 
        always @(*)
        begin
                assert(f_axi_rd_outstanding  == f_rd_fifo_axi_used);
                assert(f_axi_awr_outstanding == f_awr_fifo_axi_used+ (f_pending_awvalid?1:0));
                assert(f_axi_wr_outstanding  == f_awr_fifo_axi_used+ (f_pending_wvalid?1:0));
        end
 
        always @(*)
        if (OPT_READONLY)
        begin
                assert(f_axi_awr_outstanding == 0);
                assert(f_axi_wr_outstanding  == 0);
        end
 
        always @(*)
        if (OPT_WRITEONLY)
        begin
                assert(f_axi_ard_outstanding == 0);
        end
 
        //
        initial assert((!OPT_READONLY)||(!OPT_WRITEONLY));
 
        always @(*)
        if (OPT_READONLY)
        begin
                assume(i_axi_awvalid == 0);
                assume(i_axi_wvalid == 0);
 
                assert(o_axi_bvalid == 0);
        end
 
        always @(*)
        if (OPT_WRITEONLY)
        begin
                assume(i_axi_arvalid == 0);
                assert(o_axi_rvalid == 0);
        end
`endif
endmodule
 

Browse

Tools

Subversion Repositories wb2axip

[/] [wb2axip/] [trunk/] [rtl/] [axlite2wbsp.v] - Blame information for rev 16

Line No.	Rev	Author	Line
1	16	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
2			`//`
3			`// Filename: axlite2wbsp.v`
4			`//`
5			`// Project: Pipelined Wishbone to AXI converter`
6			`//`
7			`// Purpose: Take an AXI lite input, and convert it into WB.`
8			`//`
9			`// We'll treat AXI as two separate busses: one for writes, another for`
10			`// reads, further, we'll insist that the two channels AXI uses for writes`
11			`// combine into one channel for our purposes.`
12			`//`
13			`//`
14			`// Creator: Dan Gisselquist, Ph.D.`
15			`// Gisselquist Technology, LLC`
16			`//`
17			`////////////////////////////////////////////////////////////////////////////////`
18			`//`
19			`// Copyright (C) 2016-2019, Gisselquist Technology, LLC`
20			`//`
21			`// This file is part of the pipelined Wishbone to AXI converter project, a`
22			`// project that contains multiple bus bridging designs and formal bus property`
23			`// sets.`
24			`//`
25			`// The bus bridge designs and property sets are free RTL designs: you can`
26			`// redistribute them and/or modify any of them under the terms of the GNU`
27			`// Lesser General Public License as published by the Free Software Foundation,`
28			`// either version 3 of the License, or (at your option) any later version.`
29			`//`
30			`// The bus bridge designs and property sets are distributed in the hope that`
31			`// they will be useful, but WITHOUT ANY WARRANTY; without even the implied`
32			`// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the`
33			`// GNU Lesser General Public License for more details.`
34			`//`
35			`// You should have received a copy of the GNU Lesser General Public License`
36			`// along with these designs. (It's in the $(ROOT)/doc directory. Run make`
37			`// with no target there if the PDF file isn't present.) If not, see`
38			`// <http://www.gnu.org/licenses/> for a copy.`
39			`//`
40			`// License: LGPL, v3, as defined and found on www.gnu.org,`
41			`// http://www.gnu.org/licenses/lgpl.html`
42			`//`
43			`////////////////////////////////////////////////////////////////////////////////`
44			`//`
45			`//`
46			`default_nettype none
47			`//`
48			`module axlite2wbsp( i_clk, i_axi_reset_n,`
49			`//`
50			`o_axi_awready, i_axi_awaddr, i_axi_awcache, i_axi_awprot,i_axi_awvalid,`
51			`//`
52			`o_axi_wready, i_axi_wdata, i_axi_wstrb, i_axi_wvalid,`
53			`//`
54			`o_axi_bresp, o_axi_bvalid, i_axi_bready,`
55			`//`
56			`o_axi_arready, i_axi_araddr, i_axi_arcache, i_axi_arprot, i_axi_arvalid,`
57			`//`
58			`o_axi_rresp, o_axi_rvalid, o_axi_rdata, i_axi_rready,`
59			`//`
60			`// Wishbone interface`
61			`o_reset, o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,`
62			`i_wb_ack, i_wb_stall, i_wb_data, i_wb_err);`
63			`//`
64			`parameter C_AXI_DATA_WIDTH = 32;// Width of the AXI R&W data`
65			`parameter C_AXI_ADDR_WIDTH = 28; // AXI Address width`
66			`parameter LGFIFO = 4;`
67			`parameter F_MAXSTALL = 3;`
68			`parameter F_MAXDELAY = 3;`
69			`parameter [0:0] OPT_READONLY = 1'b0;`
70			`parameter [0:0] OPT_WRITEONLY = 1'b0;`
71			`localparam F_LGDEPTH = LGFIFO+1;`
72			`//`
73			`input wire i_clk; // System clock`
74			`input wire i_axi_reset_n;`
75
76			`// AXI write address channel signals`
77			`output wire o_axi_awready;//Slave is ready to accept`
78			`input wire [C_AXI_ADDR_WIDTH-1:0] i_axi_awaddr; // Write address`
79			`input wire [3:0] i_axi_awcache; // Write Cache type`
80			`input wire [2:0] i_axi_awprot; // Write Protection type`
81			`input wire i_axi_awvalid; // Write address valid`
82
83			`// AXI write data channel signals`
84			`output wire o_axi_wready; // Write data ready`
85			`input wire [C_AXI_DATA_WIDTH-1:0] i_axi_wdata; // Write data`
86			`input wire [C_AXI_DATA_WIDTH/8-1:0] i_axi_wstrb; // Write strobes`
87			`input wire i_axi_wvalid; // Write valid`
88
89			`// AXI write response channel signals`
90			`output wire [1:0] o_axi_bresp; // Write response`
91			`output wire o_axi_bvalid; // Write reponse valid`
92			`input wire i_axi_bready; // Response ready`
93
94			`// AXI read address channel signals`
95			`output wire o_axi_arready; // Read address ready`
96			`input wire [C_AXI_ADDR_WIDTH-1:0] i_axi_araddr; // Read address`
97			`input wire [3:0] i_axi_arcache; // Read Cache type`
98			`input wire [2:0] i_axi_arprot; // Read Protection type`
99			`input wire i_axi_arvalid; // Read address valid`
100
101			`// AXI read data channel signals`
102			`output wire [1:0] o_axi_rresp; // Read response`
103			`output wire o_axi_rvalid; // Read reponse valid`
104			`output wire [C_AXI_DATA_WIDTH-1:0] o_axi_rdata; // Read data`
105			`input wire i_axi_rready; // Read Response ready`
106
107			`// We'll share the clock and the reset`
108			`output wire o_reset;`
109			`output wire o_wb_cyc;`
110			`output wire o_wb_stb;`
111			`output wire o_wb_we;`
112			`output wire [(C_AXI_ADDR_WIDTH-3):0] o_wb_addr;`
113			`output wire [(C_AXI_DATA_WIDTH-1):0] o_wb_data;`
114			`output wire [(C_AXI_DATA_WIDTH/8-1):0] o_wb_sel;`
115			`input wire i_wb_ack;`
116			`input wire i_wb_stall;`
117			`input wire [(C_AXI_DATA_WIDTH-1):0] i_wb_data;`
118			`input wire i_wb_err;`
119
120
121			`localparam DW = C_AXI_DATA_WIDTH;`
122			`localparam AW = C_AXI_ADDR_WIDTH-2;`
123			`//`
124			`//`
125			`//`
126
127			`wire [(AW-1):0] w_wb_addr, r_wb_addr;`
128			`wire [(C_AXI_DATA_WIDTH-1):0] w_wb_data;`
129			`wire [(C_AXI_DATA_WIDTH/8-1):0] w_wb_sel;`
130			`wire r_wb_err, r_wb_cyc, r_wb_stb, r_wb_stall, r_wb_ack;`
131			`wire w_wb_err, w_wb_cyc, w_wb_stb, w_wb_stall, w_wb_ack;`
132
133			`// verilator lint_off UNUSED`
134			`wire r_wb_we, w_wb_we;`
135
136			`assign r_wb_we = 1'b0;`
137			`assign w_wb_we = 1'b1;`
138			`// verilator lint_on UNUSED`
139
140			`ifdef FORMAL
141			`wire [LGFIFO:0] f_wr_fifo_first, f_rd_fifo_first,`
142			`f_wr_fifo_mid, f_rd_fifo_mid,`
143			`f_wr_fifo_last, f_rd_fifo_last;`
144			`wire [(F_LGDEPTH-1):0] f_wb_nreqs, f_wb_nacks,`
145			`f_wb_outstanding;`
146			`wire [(F_LGDEPTH-1):0] f_wb_wr_nreqs, f_wb_wr_nacks,`
147			`f_wb_wr_outstanding;`
148			`wire [(F_LGDEPTH-1):0] f_wb_rd_nreqs, f_wb_rd_nacks,`
149			`f_wb_rd_outstanding;`
150			`wire f_pending_awvalid, f_pending_wvalid;`
151			`endif
152
153			`//`
154			`// AXI-lite write channel to WB processing`
155			`//`
156			`generate if (!OPT_READONLY)`
157			`begin : AXI_WR`
158			`axilwr2wbsp #(`
159			`// .F_LGDEPTH(F_LGDEPTH),`
160			`// .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),`
161			`.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), // .AW(AW),`
162			`.LGFIFO(LGFIFO))`
163			`axi_write_decoder(`
164			`.i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),`
165			`//`
166			`.o_axi_awready(o_axi_awready),`
167			`.i_axi_awaddr( i_axi_awaddr),`
168			`.i_axi_awcache(i_axi_awcache),`
169			`.i_axi_awprot( i_axi_awprot),`
170			`.i_axi_awvalid(i_axi_awvalid),`
171			`//`
172			`.o_axi_wready( o_axi_wready),`
173			`.i_axi_wdata( i_axi_wdata),`
174			`.i_axi_wstrb( i_axi_wstrb),`
175			`.i_axi_wvalid( i_axi_wvalid),`
176			`//`
177			`.o_axi_bresp(o_axi_bresp),`
178			`.o_axi_bvalid(o_axi_bvalid),`
179			`.i_axi_bready(i_axi_bready),`
180			`//`
181			`.o_wb_cyc( w_wb_cyc),`
182			`.o_wb_stb( w_wb_stb),`
183			`.o_wb_addr( w_wb_addr),`
184			`.o_wb_data( w_wb_data),`
185			`.o_wb_sel( w_wb_sel),`
186			`.i_wb_ack( w_wb_ack),`
187			`.i_wb_stall(w_wb_stall),`
188			`.i_wb_err( w_wb_err)`
189			`ifdef FORMAL
190			`,`
191			`.f_first(f_wr_fifo_first),`
192			`.f_mid( f_wr_fifo_mid),`
193			`.f_last( f_wr_fifo_last),`
194			`.f_wpending({ f_pending_awvalid, f_pending_wvalid })`
195			`endif
196			`);`
197			`end else begin`
198			`assign w_wb_cyc = 0;`
199			`assign w_wb_stb = 0;`
200			`assign w_wb_addr = 0;`
201			`assign w_wb_data = 0;`
202			`assign w_wb_sel = 0;`
203			`assign o_axi_awready = 0;`
204			`assign o_axi_wready = 0;`
205			`assign o_axi_bvalid = (i_axi_wvalid);`
206			`assign o_axi_bresp = 2'b11;`
207			`ifdef FORMAL
208			`assign f_wr_fifo_first = 0;`
209			`assign f_wr_fifo_mid = 0;`
210			`assign f_wr_fifo_last = 0;`
211			`assign f_pending_awvalid=0;`
212			`assign f_pending_wvalid =0;`
213			`endif
214			`end endgenerate`
215			`assign w_wb_we = 1'b1;`
216
217			`//`
218			`// AXI-lite read channel to WB processing`
219			`//`
220			`generate if (!OPT_WRITEONLY)`
221			`begin : AXI_RD`
222			`axilrd2wbsp #(`
223			`// .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),`
224			`.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),`
225			`.LGFIFO(LGFIFO))`
226			`axi_read_decoder(`
227			`.i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),`
228			`//`
229			`.o_axi_arready(o_axi_arready),`
230			`.i_axi_araddr( i_axi_araddr),`
231			`.i_axi_arcache(i_axi_arcache),`
232			`.i_axi_arprot( i_axi_arprot),`
233			`.i_axi_arvalid(i_axi_arvalid),`
234			`//`
235			`.o_axi_rresp( o_axi_rresp),`
236			`.o_axi_rvalid(o_axi_rvalid),`
237			`.o_axi_rdata( o_axi_rdata),`
238			`.i_axi_rready(i_axi_rready),`
239			`//`
240			`.o_wb_cyc( r_wb_cyc),`
241			`.o_wb_stb( r_wb_stb),`
242			`.o_wb_addr( r_wb_addr),`
243			`.i_wb_ack( r_wb_ack),`
244			`.i_wb_stall(r_wb_stall),`
245			`.i_wb_data( i_wb_data),`
246			`.i_wb_err( r_wb_err)`
247			`ifdef FORMAL
248			`,`
249			`.f_first(f_rd_fifo_first),`
250			`.f_mid( f_rd_fifo_mid),`
251			`.f_last( f_rd_fifo_last)`
252			`endif
253			`);`
254			`end else begin`
255			`assign r_wb_cyc = 0;`
256			`assign r_wb_stb = 0;`
257			`assign r_wb_addr = 0;`
258			`//`
259			`assign o_axi_arready = 1'b1;`
260			`assign o_axi_rvalid = (i_axi_arvalid)&&(o_axi_arready);`
261			`assign o_axi_rresp = (i_axi_arvalid) ? 2'b11 : 2'b00;`
262			`assign o_axi_rdata = 0;`
263			`ifdef FORMAL
264			`assign f_rd_fifo_first = 0;`
265			`assign f_rd_fifo_mid = 0;`
266			`assign f_rd_fifo_last = 0;`
267			`endif
268			`end endgenerate`
269
270			`//`
271			`//`
272			`// The arbiter that pastes the two sides together`
273			`//`
274			`//`
275			`generate if (OPT_READONLY)`
276			`begin : ARB_RD`
277			`assign o_wb_cyc = r_wb_cyc;`
278			`assign o_wb_stb = r_wb_stb;`
279			`assign o_wb_we = 1'b0;`
280			`assign o_wb_addr = r_wb_addr;`
281			`assign o_wb_data = 32'h0;`
282			`assign o_wb_sel = 0;`
283			`assign r_wb_ack = i_wb_ack;`
284			`assign r_wb_stall= i_wb_stall;`
285			`assign r_wb_ack = i_wb_ack;`
286			`assign r_wb_err = i_wb_err;`
287
288			`ifdef FORMAL
289			`fwb_master #(.DW(DW), .AW(AW),`
290			`.F_LGDEPTH(F_LGDEPTH),`
291			`.F_MAX_STALL(F_MAXSTALL),`
292			`.F_MAX_ACK_DELAY(F_MAXDELAY))`
293			`f_wb(i_clk, !i_axi_reset_n,`
294			`o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,`
295			`o_wb_sel,`
296			`i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,`
297			`f_wb_nreqs, f_wb_nacks, f_wb_outstanding);`
298
299			`assign f_wb_rd_nreqs = f_wb_nreqs;`
300			`assign f_wb_rd_nacks = f_wb_nacks;`
301			`assign f_wb_rd_outstanding = f_wb_outstanding;`
302			`//`
303			`assign f_wb_wr_nreqs = 0;`
304			`assign f_wb_wr_nacks = 0;`
305			`assign f_wb_wr_outstanding = 0;`
306			`endif
307			`end else if (OPT_WRITEONLY)`
308			`begin : ARB_WR`
309			`assign o_wb_cyc = w_wb_cyc;`
310			`assign o_wb_stb = w_wb_stb;`
311			`assign o_wb_we = 1'b1;`
312			`assign o_wb_addr = w_wb_addr;`
313			`assign o_wb_data = w_wb_data;`
314			`assign o_wb_sel = w_wb_sel;`
315			`assign w_wb_ack = i_wb_ack;`
316			`assign w_wb_stall= i_wb_stall;`
317			`assign w_wb_ack = i_wb_ack;`
318			`assign w_wb_err = i_wb_err;`
319
320			`ifdef FORMAL
321			`fwb_master #(.DW(DW), .AW(AW),`
322			`.F_LGDEPTH(F_LGDEPTH),`
323			`.F_MAX_STALL(F_MAXSTALL),`
324			`.F_MAX_ACK_DELAY(F_MAXDELAY))`
325			`f_wb(i_clk, !i_axi_reset_n,`
326			`o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,`
327			`o_wb_sel,`
328			`i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,`
329			`f_wb_nreqs, f_wb_nacks, f_wb_outstanding);`
330
331			`assign f_wb_wr_nreqs = f_wb_nreqs;`
332			`assign f_wb_wr_nacks = f_wb_nacks;`
333			`assign f_wb_wr_outstanding = f_wb_outstanding;`
334			`//`
335			`assign f_wb_rd_nreqs = 0;`
336			`assign f_wb_rd_nacks = 0;`
337			`assign f_wb_rd_outstanding = 0;`
338			`endif
339			`end else begin : ARB_WB`
340			`wbarbiter #(.DW(DW), .AW(AW),`
341			`.F_LGDEPTH(F_LGDEPTH),`
342			`.F_MAX_STALL(F_MAXSTALL),`
343			`.F_MAX_ACK_DELAY(F_MAXDELAY))`
344			`readorwrite(i_clk, !i_axi_reset_n,`
345			`r_wb_cyc, r_wb_stb, 1'b0, r_wb_addr, w_wb_data, w_wb_sel,`
346			`r_wb_ack, r_wb_stall, r_wb_err,`
347			`w_wb_cyc, w_wb_stb, 1'b1, w_wb_addr, w_wb_data, w_wb_sel,`
348			`w_wb_ack, w_wb_stall, w_wb_err,`
349			`o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, o_wb_sel,`
350			`i_wb_ack, i_wb_stall, i_wb_err`
351			`ifdef FORMAL
352			`,`
353			`f_wb_rd_nreqs, f_wb_rd_nacks, f_wb_rd_outstanding,`
354			`f_wb_wr_nreqs, f_wb_wr_nacks, f_wb_wr_outstanding,`
355			`f_wb_nreqs, f_wb_nacks, f_wb_outstanding`
356			`endif
357			`);`
358			`end endgenerate`
359
360			`assign o_reset = (i_axi_reset_n == 1'b0);`
361
362			`ifdef FORMAL
363			`reg f_past_valid;`
364
365			`initial f_past_valid = 1'b0;`
366			`always @(posedge i_clk)`
367			`f_past_valid = 1'b1;`
368
369			`initial assume(!i_axi_reset_n);`
370			`always @(*)`
371			`if (!f_past_valid)`
372			`assume(!i_axi_reset_n);`
373
374			`wire [(F_LGDEPTH-1):0] f_axi_rd_outstanding,`
375			`f_axi_wr_outstanding,`
376			`f_axi_awr_outstanding;`
377			`wire [(F_LGDEPTH-1):0] f_axi_rd_id_outstanding,`
378			`f_axi_awr_id_outstanding,`
379			`f_axi_wr_id_outstanding;`
380			`wire [8:0] f_axi_wr_pending,`
381			`f_axi_rd_count,`
382			`f_axi_wr_count;`
383
384			`faxil_slave #(`
385			`// .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),`
386			`.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),`
387			`.F_LGDEPTH(F_LGDEPTH),`
388			`.F_AXI_MAXWAIT(0),`
389			`.F_AXI_MAXDELAY(0))`
390			`f_axi(.i_clk(i_clk), .i_axi_reset_n(i_axi_reset_n),`
391			`// AXI write address channnel`
392			`.i_axi_awready(o_axi_awready),`
393			`.i_axi_awaddr( i_axi_awaddr),`
394			`.i_axi_awcache(i_axi_awcache),`
395			`.i_axi_awprot( i_axi_awprot),`
396			`.i_axi_awvalid(i_axi_awvalid),`
397			`// AXI write data channel`
398			`.i_axi_wready( o_axi_wready),`
399			`.i_axi_wdata( i_axi_wdata),`
400			`.i_axi_wstrb( i_axi_wstrb),`
401			`.i_axi_wvalid( i_axi_wvalid),`
402			`// AXI write acknowledgement channel`
403			`.i_axi_bresp( o_axi_bresp),`
404			`.i_axi_bvalid(o_axi_bvalid),`
405			`.i_axi_bready(i_axi_bready),`
406			`// AXI read address channel`
407			`.i_axi_arready(o_axi_arready),`
408			`.i_axi_araddr( i_axi_araddr),`
409			`.i_axi_arcache(i_axi_arcache),`
410			`.i_axi_arprot( i_axi_arprot),`
411			`.i_axi_arvalid(i_axi_arvalid),`
412			`// AXI read data return`
413			`.i_axi_rresp( o_axi_rresp),`
414			`.i_axi_rvalid( o_axi_rvalid),`
415			`.i_axi_rdata( o_axi_rdata),`
416			`.i_axi_rready( i_axi_rready),`
417			`// Quantify where we are within a transaction`
418			`.f_axi_rd_outstanding( f_axi_rd_outstanding),`
419			`.f_axi_wr_outstanding( f_axi_wr_outstanding),`
420			`.f_axi_awr_outstanding(f_axi_awr_outstanding));`
421
422			`wire f_axi_ard_req, f_axi_awr_req, f_axi_wr_req,`
423			`f_axi_rd_ack, f_axi_wr_ack;`
424
425			`assign f_axi_ard_req = (i_axi_arvalid)&&(o_axi_arready);`
426			`assign f_axi_awr_req = (i_axi_awvalid)&&(o_axi_awready);`
427			`assign f_axi_wr_req = (i_axi_wvalid)&&(o_axi_wready);`
428			`assign f_axi_wr_ack = (o_axi_bvalid)&&(i_axi_bready);`
429			`assign f_axi_rd_ack = (o_axi_rvalid)&&(i_axi_rready);`
430
431			`wire [LGFIFO:0] f_awr_fifo_axi_used,`
432			`f_dwr_fifo_axi_used,`
433			`f_rd_fifo_axi_used,`
434			`f_wr_fifo_wb_outstanding,`
435			`f_rd_fifo_wb_outstanding;`
436
437			`assign f_awr_fifo_axi_used = f_wr_fifo_first - f_wr_fifo_last;`
438			`assign f_rd_fifo_axi_used = f_rd_fifo_first - f_rd_fifo_last;`
439			`assign f_wr_fifo_wb_outstanding = f_wr_fifo_first - f_wr_fifo_last;`
440			`assign f_rd_fifo_wb_outstanding = f_rd_fifo_first - f_rd_fifo_last;`
441
442			`always @(*)`
443			`begin`
444			`assert(f_axi_rd_outstanding == f_rd_fifo_axi_used);`
445			`assert(f_axi_awr_outstanding == f_awr_fifo_axi_used+ (f_pending_awvalid?1:0));`
446			`assert(f_axi_wr_outstanding == f_awr_fifo_axi_used+ (f_pending_wvalid?1:0));`
447			`end`
448
449			`always @(*)`
450			`if (OPT_READONLY)`
451			`begin`
452			`assert(f_axi_awr_outstanding == 0);`
453			`assert(f_axi_wr_outstanding == 0);`
454			`end`
455
456			`always @(*)`
457			`if (OPT_WRITEONLY)`
458			`begin`
459			`assert(f_axi_ard_outstanding == 0);`
460			`end`
461
462			`//`
463			`initial assert((!OPT_READONLY)\|\|(!OPT_WRITEONLY));`
464
465			`always @(*)`
466			`if (OPT_READONLY)`
467			`begin`
468			`assume(i_axi_awvalid == 0);`
469			`assume(i_axi_wvalid == 0);`
470
471			`assert(o_axi_bvalid == 0);`
472			`end`
473
474			`always @(*)`
475			`if (OPT_WRITEONLY)`
476			`begin`
477			`assume(i_axi_arvalid == 0);`
478			`assert(o_axi_rvalid == 0);`
479			`end`
480			`endif
481			`endmodule`
482