diff options
Diffstat (limited to 'rtl/wb2axip/axlite2wbsp.v')
| -rw-r--r-- | rtl/wb2axip/axlite2wbsp.v | 568 |
1 files changed, 568 insertions, 0 deletions
diff --git a/rtl/wb2axip/axlite2wbsp.v b/rtl/wb2axip/axlite2wbsp.v new file mode 100644 index 0000000..b11b365 --- /dev/null +++ b/rtl/wb2axip/axlite2wbsp.v @@ -0,0 +1,568 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: axlite2wbsp.v +// {{{ +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// 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-2024, Gisselquist Technology, LLC +// {{{ +// This file is part of the WB2AXIP project. +// +// The WB2AXIP project contains free software and gateware, licensed under the +// Apache License, Version 2.0 (the "License"). You may not use this project, +// or this file, except in compliance with the License. You may obtain a copy +// of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT +// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +// License for the specific language governing permissions and limitations +// under the License. +// +//////////////////////////////////////////////////////////////////////////////// +// +// +`default_nettype none +// }}} +module axlite2wbsp #( + // {{{ + 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, +`ifdef FORMAL + parameter F_MAXSTALL = 3, + parameter F_MAXDELAY = 3, +`endif + parameter [0:0] OPT_READONLY = 1'b0, + parameter [0:0] OPT_WRITEONLY = 1'b0, + localparam AXILLSB = $clog2(C_AXI_DATA_WIDTH/8) + // }}} + ) ( + // {{{ + input wire i_clk, // System clock + input wire i_axi_reset_n, + + // AXI write address channel signals + // {{{ + input wire i_axi_awvalid, + output wire o_axi_awready, + input wire [C_AXI_ADDR_WIDTH-1:0] i_axi_awaddr, + input wire [2:0] i_axi_awprot, + // }}} + // AXI write data channel signals + // {{{ + input wire i_axi_wvalid, + output wire o_axi_wready, + input wire [C_AXI_DATA_WIDTH-1:0] i_axi_wdata, + input wire [C_AXI_DATA_WIDTH/8-1:0] i_axi_wstrb, + // }}} + // AXI write response channel signals + // {{{ + output wire o_axi_bvalid, + input wire i_axi_bready, + output wire [1:0] o_axi_bresp, + // }}} + // AXI read address channel signals + // {{{ + input wire i_axi_arvalid, + output wire o_axi_arready, + input wire [C_AXI_ADDR_WIDTH-1:0] i_axi_araddr, + input wire [2:0] i_axi_arprot, + // }}} + // AXI read data channel signals + // {{{ + output wire o_axi_rvalid, + input wire i_axi_rready, + output wire [C_AXI_DATA_WIDTH-1:0] o_axi_rdata, + output wire [1:0] o_axi_rresp, + // }}} + // Wishbone signals + // {{{ + // 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-AXILLSB-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_stall, + input wire i_wb_ack, + input wire [(C_AXI_DATA_WIDTH-1):0] i_wb_data, + input wire i_wb_err + // }}} + // }}} + ); + + // Local definitions + // {{{ + localparam DW = C_AXI_DATA_WIDTH; + localparam AW = C_AXI_ADDR_WIDTH-AXILLSB; + // + // + // + + wire [(AW-1):0] w_wb_addr, r_wb_addr; + wire [(DW-1):0] w_wb_data; + wire [(DW/8-1):0] w_wb_sel, r_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 + // {{{ + // Verilator lint_off UNUSED + localparam F_LGDEPTH = LGFIFO+1; + 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; + // Verilator lint_on UNUSED + 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), + // + .i_axi_awvalid(i_axi_awvalid), + .o_axi_awready(o_axi_awready), + .i_axi_awaddr( i_axi_awaddr), + .i_axi_awprot( i_axi_awprot), + // + .i_axi_wvalid( i_axi_wvalid), + .o_axi_wready( o_axi_wready), + .i_axi_wdata( i_axi_wdata), + .i_axi_wstrb( i_axi_wstrb), + // + .o_axi_bvalid(o_axi_bvalid), + .i_axi_bready(i_axi_bready), + .o_axi_bresp(o_axi_bresp), + // + .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_stall(w_wb_stall), + .i_wb_ack( w_wb_ack), + .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 : EMPTY_WRITES + // {{{ + 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), + // + .i_axi_arvalid(i_axi_arvalid), + .o_axi_arready(o_axi_arready), + .i_axi_araddr( i_axi_araddr), + .i_axi_arprot( i_axi_arprot), + // + .o_axi_rvalid(o_axi_rvalid), + .i_axi_rready(i_axi_rready), + .o_axi_rdata( o_axi_rdata), + .o_axi_rresp( o_axi_rresp), + // + .o_wb_cyc( r_wb_cyc), + .o_wb_stb( r_wb_stb), + .o_wb_addr( r_wb_addr), + .o_wb_sel( r_wb_sel), + .i_wb_stall(r_wb_stall), + .i_wb_ack( r_wb_ack), + .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 : EMPTY_READS + // {{{ + 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 = r_wb_sel; + 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) +`ifdef FORMAL + , .F_LGDEPTH(F_LGDEPTH), + .F_MAX_STALL(F_MAXSTALL), + .F_MAX_ACK_DELAY(F_MAXDELAY) +`endif + // }}} + ) readorwrite( + // {{{ + .i_clk(i_clk), .i_reset(!i_axi_reset_n), + // Channel A - Reads + // {{{ + .i_a_cyc(r_wb_cyc), .i_a_stb(r_wb_stb), + .i_a_we(1'b0), + .i_a_adr(r_wb_addr), + .i_a_dat(w_wb_data), + .i_a_sel(r_wb_sel), + .o_a_stall(r_wb_stall), + .o_a_ack(r_wb_ack), + .o_a_err(r_wb_err), + // }}} + // Channel B + // {{{ + .i_b_cyc(w_wb_cyc), .i_b_stb(w_wb_stb), + .i_b_we(1'b1), + .i_b_adr(w_wb_addr), + .i_b_dat(w_wb_data), + .i_b_sel(w_wb_sel), + .o_b_stall(w_wb_stall), + .o_b_ack(w_wb_ack), + .o_b_err(w_wb_err), + // }}} + // Arbitrated outgoing channel + // {{{ + .o_cyc(o_wb_cyc), .o_stb(o_wb_stb), .o_we(o_wb_we), + .o_adr(o_wb_addr), + .o_dat(o_wb_data), + .o_sel(o_wb_sel), + .i_stall(i_wb_stall), + .i_ack(i_wb_ack), + .i_err(i_wb_err) + // }}} +`ifdef FORMAL + // {{{ + , + .f_nreqs(f_wb_nreqs), .f_nacks(f_wb_nacks), + .f_outstanding(f_wb_outstanding), + .f_a_nreqs(f_wb_rd_nreqs), .f_a_nacks(f_wb_rd_nacks), + .f_a_outstanding(f_wb_rd_outstanding), + .f_b_nreqs(f_wb_wr_nreqs), .f_b_nacks(f_wb_wr_nacks), + .f_b_outstanding(f_wb_wr_outstanding) + // }}} +`endif + // }}} + ); + // }}} + end endgenerate + // }}} + assign o_reset = (i_axi_reset_n == 1'b0); + +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +// +// Formal properties +// {{{ +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +`ifdef FORMAL + // Formal declarations + // {{{ + reg f_past_valid; + + initial f_past_valid = 1'b0; + always @(posedge i_clk) + f_past_valid <= 1'b1; + + + wire [(F_LGDEPTH-1):0] f_axi_rd_outstanding, + f_axi_wr_outstanding, + f_axi_awr_outstanding; + + wire [LGFIFO:0] f_awr_fifo_axi_used, + f_rd_fifo_axi_used; + // }}} + + initial assume(!i_axi_reset_n); + always @(*) + if (!f_past_valid) + assume(!i_axi_reset_n); + + 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_awvalid(i_axi_awvalid), + .i_axi_awready(o_axi_awready), + .i_axi_awaddr( i_axi_awaddr), + .i_axi_awprot( i_axi_awprot), + // AXI write data channel + .i_axi_wvalid( i_axi_wvalid), + .i_axi_wready( o_axi_wready), + .i_axi_wdata( i_axi_wdata), + .i_axi_wstrb( i_axi_wstrb), + // AXI write acknowledgement channel + .i_axi_bvalid(o_axi_bvalid), + .i_axi_bready(i_axi_bready), + .i_axi_bresp( o_axi_bresp), + // AXI read address channel + .i_axi_arvalid(i_axi_arvalid), + .i_axi_arready(o_axi_arready), + .i_axi_araddr( i_axi_araddr), + .i_axi_arprot( i_axi_arprot), + // AXI read data return + .i_axi_rvalid( o_axi_rvalid), + .i_axi_rready( i_axi_rready), + .i_axi_rdata( o_axi_rdata), + .i_axi_rresp( o_axi_rresp), + // 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) + // }}} + ); + + 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; + + 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_rd_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 + + // Make Verilator happy + // {{{ + // Verilator lint_off UNUSED + wire unused_formal; + assign unused_formal = &{ 1'b0, f_wb_nreqs, f_wb_nacks, + f_wb_outstanding, f_wb_wr_nreqs, f_wb_wr_nacks, + f_wb_wr_outstanding, f_wb_rd_nreqs, f_wb_rd_nacks, + f_wb_rd_outstanding }; + // Verilator lint_on UNUSED + // }}} +`endif +// }}} +endmodule +`ifndef YOSYS +`default_nettype wire +`endif |