From 3038edc09a2eb15762f2e58533f429489107520b Mon Sep 17 00:00:00 2001 From: Alejandro Soto Date: Wed, 6 Mar 2024 02:38:24 -0600 Subject: rtl/wb2axip: add to version control --- rtl/wb2axip/wbm2axisp.v | 1155 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1155 insertions(+) create mode 100644 rtl/wb2axip/wbm2axisp.v (limited to 'rtl/wb2axip/wbm2axisp.v') diff --git a/rtl/wb2axip/wbm2axisp.v b/rtl/wb2axip/wbm2axisp.v new file mode 100644 index 0000000..9c7909a --- /dev/null +++ b/rtl/wb2axip/wbm2axisp.v @@ -0,0 +1,1155 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: wbm2axisp.v (Wishbone master to AXI slave, pipelined) +// {{{ +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: The B4 Wishbone SPEC allows transactions at a speed as fast as +// one per clock. The AXI bus allows transactions at a speed of +// one read and one write transaction per clock. These capabilities work +// by allowing requests to take place prior to responses, such that the +// requests might go out at once per clock and take several clocks, and +// the responses may start coming back several clocks later. In other +// words, both protocols allow multiple transactions to be "in flight" at +// the same time. Current wishbone to AXI converters, however, handle only +// one transaction at a time: initiating the transaction, and then waiting +// for the transaction to complete before initiating the next. +// +// The purpose of this core is to maintain the speed of both buses, while +// transiting from the Wishbone (as master) to the AXI bus (as slave) and +// back again. +// +// 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 wbm2axisp #( + // {{{ + parameter C_AXI_DATA_WIDTH = 128,// Width of the AXI R&W data + parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width (log wordsize) + parameter C_AXI_ID_WIDTH = 1, + parameter DW = 32, // Wishbone data width + parameter AW = 26, // Wishbone address width (log wordsize) + parameter [C_AXI_ID_WIDTH-1:0] AXI_WRITE_ID = 1'b0, + parameter [C_AXI_ID_WIDTH-1:0] AXI_READ_ID = 1'b1, + // + // OPT_LITTLE_ENDIAN controls which word has the greatest address + // when the bus size is adjusted. If OPT_LITTLE_ENDIAN is true, + // the biggest address is in the most significant word(s), otherwise + // the least significant word(s). This parameter is ignored if + // C_AXI_DATA_WIDTH == DW. + parameter [0:0] OPT_LITTLE_ENDIAN = 1'b1, + parameter LGFIFO = 6 + // }}} + ) ( + // {{{ + input wire i_clk, // System clock + input wire i_reset,// Reset signal,drives AXI rst + + // AXI write address channel signals + output reg o_axi_awvalid, // Write address valid + input wire i_axi_awready, // Slave is ready to accept + output wire [C_AXI_ID_WIDTH-1:0] o_axi_awid, // Write ID + output reg [C_AXI_ADDR_WIDTH-1:0] o_axi_awaddr, // Write address + output wire [7:0] o_axi_awlen, // Write Burst Length + output wire [2:0] o_axi_awsize, // Write Burst size + output wire [1:0] o_axi_awburst, // Write Burst type + output wire [0:0] o_axi_awlock, // Write lock type + output wire [3:0] o_axi_awcache, // Write Cache type + output wire [2:0] o_axi_awprot, // Write Protection type + output wire [3:0] o_axi_awqos, // Write Quality of Svc + +// AXI write data channel signals + output reg o_axi_wvalid, // Write valid + input wire i_axi_wready, // Write data ready + output reg [C_AXI_DATA_WIDTH-1:0] o_axi_wdata, // Write data + output reg [C_AXI_DATA_WIDTH/8-1:0] o_axi_wstrb, // Write strobes + output wire o_axi_wlast, // Last write transaction + +// AXI write response channel signals + input wire i_axi_bvalid, // Write reponse valid + output wire o_axi_bready, // Response ready + input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID + input wire [1:0] i_axi_bresp, // Write response + +// AXI read address channel signals + output reg o_axi_arvalid, // Read address valid + input wire i_axi_arready, // Read address ready + output wire [C_AXI_ID_WIDTH-1:0] o_axi_arid, // Read ID + output reg [C_AXI_ADDR_WIDTH-1:0] o_axi_araddr, // Read address + output wire [7:0] o_axi_arlen, // Read Burst Length + output wire [2:0] o_axi_arsize, // Read Burst size + output wire [1:0] o_axi_arburst, // Read Burst type + output wire [0:0] o_axi_arlock, // Read lock type + output wire [3:0] o_axi_arcache, // Read Cache type + output wire [2:0] o_axi_arprot, // Read Protection type + output wire [3:0] o_axi_arqos, // Read Protection type + +// AXI read data channel signals + input wire i_axi_rvalid, // Read reponse valid + output wire o_axi_rready, // Read Response ready + input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID + input wire [C_AXI_DATA_WIDTH-1:0] i_axi_rdata, // Read data + input wire [1:0] i_axi_rresp, // Read response + input wire i_axi_rlast, // Read last + + // We'll share the clock and the reset + input wire i_wb_cyc, + input wire i_wb_stb, + input wire i_wb_we, + input wire [(AW-1):0] i_wb_addr, + input wire [(DW-1):0] i_wb_data, + input wire [(DW/8-1):0] i_wb_sel, + output reg o_wb_stall, + output reg o_wb_ack, + output reg [(DW-1):0] o_wb_data, + output reg o_wb_err + // }}} +); + //////////////////////////////////////////////////////////////////////// + // + // Localparameter declarations, initial parameter consistency check + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + localparam LG_AXI_DW = $clog2(C_AXI_DATA_WIDTH); + localparam LG_WB_DW = $clog2(DW); + // localparam FIFOLN = (1<> (fifo_value * DW); + + end else begin : BIG_ENDIAN_RDATA + + reg [SUBW-1:0] neg_fifo_value; + + always @(*) + neg_fifo_value = ~fifo_value; + + assign return_data = i_axi_rdata + >> (neg_fifo_value * DW); + + end + + always @(posedge i_clk) + o_wb_data <= return_data[DW-1:0]; + + // Make Verilator happy here + // verilator lint_off UNUSED + if (C_AXI_DATA_WIDTH > DW) + begin : UNUSED_DATA + wire unused_data; + assign unused_data = &{ 1'b0, + return_data[C_AXI_DATA_WIDTH-1:DW] }; + end + // verilator lint_on UNUSED +`ifdef FORMAL + always @(*) + assert(wr_addr - rd_addr == npending); + + always @(*) + assert(empty == (wr_addr == rd_addr)); + + + // + // ... + // +`endif + // }}} + end endgenerate + // }}} + + // Read data channel / response logic + assign o_axi_rready = 1'b1; + assign o_axi_bready = 1'b1; + // }}} + + // Make verilator's -Wall happy + // {{{ + // verilator lint_off UNUSED + wire unused; + assign unused = &{ 1'b0, full, i_axi_bid, i_axi_bresp[0], i_axi_rid, i_axi_rresp[0], i_axi_rlast, m_data, m_sel }; + generate if (C_AXI_DATA_WIDTH > DW) + begin : GEN_UNUSED_DW + wire [C_AXI_DATA_WIDTH-1:DW] unused_data; + assign unused_data = i_axi_rdata[C_AXI_DATA_WIDTH-1:DW]; + end endgenerate + // verilator lint_on UNUSED + // }}} + +///////////////////////////////////////////////////////////////////////// +///////////////////////////////////////////////////////////////////////// +///////////////////////////////////////////////////////////////////////// +// +// Formal methods section +// {{{ +// Below are a scattering of the formal properties used. They are not the +// complete set of properties. Those are maintained elsewhere. +///////////////////////////////////////////////////////////////////////// +///////////////////////////////////////////////////////////////////////// +///////////////////////////////////////////////////////////////////////// +`ifdef FORMAL + // + // ... + // + + // Parameters + initial assert( (C_AXI_DATA_WIDTH / DW ==32) + ||(C_AXI_DATA_WIDTH / DW ==16) + ||(C_AXI_DATA_WIDTH / DW == 8) + ||(C_AXI_DATA_WIDTH / DW == 4) + ||(C_AXI_DATA_WIDTH / DW == 2) + ||(C_AXI_DATA_WIDTH == DW)); + // + initial assert( C_AXI_ADDR_WIDTH == AW + (LG_WB_DW-3)); + + + initial begin + assert(C_AXI_DATA_WIDTH >= DW); + assert((DW == 8) == (AW == C_AXI_ADDR_WIDTH)); + assert(C_AXI_ADDR_WIDTH == AW + $clog2(DW)-3); + end + // }}} + + //////////////////////////////////////////////////////////////////////// + // + // Setup / f_past_valid + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + initial f_past_valid = 1'b0; + always @(posedge i_clk) + f_past_valid <= 1'b1; + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Assumptions about the WISHBONE inputs + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + always @(*) + if (!f_past_valid) + assume(i_reset); + + fwb_slave #(.DW(DW),.AW(AW), + .F_MAX_STALL(0), + .F_MAX_ACK_DELAY(0), + .F_LGDEPTH(F_LGDEPTH), + .F_MAX_REQUESTS(0)) + f_wb(i_clk, i_reset, i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, + i_wb_data, i_wb_sel, + o_wb_ack, o_wb_stall, o_wb_data, o_wb_err, + f_wb_nreqs, f_wb_nacks, f_wb_outstanding); + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Assumptions about the AXI inputs + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + faxi_master #( + // {{{ + .C_AXI_ID_WIDTH(C_AXI_ID_WIDTH), + .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), + .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH) + // ... + // }}} + ) f_axi(.i_clk(i_clk), .i_axi_reset_n(!i_reset), + // {{{ + // Write address channel + .i_axi_awready(i_axi_awready), + .i_axi_awid( o_axi_awid), + .i_axi_awaddr( o_axi_awaddr), + .i_axi_awlen( o_axi_awlen), + .i_axi_awsize( o_axi_awsize), + .i_axi_awburst(o_axi_awburst), + .i_axi_awlock( o_axi_awlock), + .i_axi_awcache(o_axi_awcache), + .i_axi_awprot( o_axi_awprot), + .i_axi_awqos( o_axi_awqos), + .i_axi_awvalid(o_axi_awvalid), + // Write data channel + .i_axi_wready( i_axi_wready), + .i_axi_wdata( o_axi_wdata), + .i_axi_wstrb( o_axi_wstrb), + .i_axi_wlast( o_axi_wlast), + .i_axi_wvalid( o_axi_wvalid), + // Write response channel + .i_axi_bid( i_axi_bid), + .i_axi_bresp( i_axi_bresp), + .i_axi_bvalid( i_axi_bvalid), + .i_axi_bready( o_axi_bready), + // Read address channel + .i_axi_arready(i_axi_arready), + .i_axi_arid( o_axi_arid), + .i_axi_araddr( o_axi_araddr), + .i_axi_arlen( o_axi_arlen), + .i_axi_arsize( o_axi_arsize), + .i_axi_arburst(o_axi_arburst), + .i_axi_arlock( o_axi_arlock), + .i_axi_arcache(o_axi_arcache), + .i_axi_arprot( o_axi_arprot), + .i_axi_arqos( o_axi_arqos), + .i_axi_arvalid(o_axi_arvalid), + // Read data channel + .i_axi_rid( i_axi_rid), + .i_axi_rresp( i_axi_rresp), + .i_axi_rvalid( i_axi_rvalid), + .i_axi_rdata( i_axi_rdata), + .i_axi_rlast( i_axi_rlast), + .i_axi_rready( o_axi_rready), + // Counts + .f_axi_awr_nbursts(f_axi_awr_nbursts), + .f_axi_wr_pending(f_axi_wr_pending), + .f_axi_rd_nbursts(f_axi_rd_nbursts), + .f_axi_rd_outstanding(f_axi_rd_outstanding) + // + // ... + // + // }}} + ); + + always @(*) + if (!flushing && i_wb_cyc) + assert(f_wb_outstanding == npending + (r_stb ? 1:0) + + ( ((C_AXI_DATA_WIDTH != DW) + && (o_wb_ack|o_wb_err))? 1:0)); + else if (flushing && i_wb_cyc && !o_wb_err) + assert(f_wb_outstanding == (r_stb ? 1:0)); + + always @(*) + if (f_axi_awr_nbursts > 0) + begin + assert(direction); + assert(f_axi_rd_nbursts == 0); + assert(f_axi_awr_nbursts + (o_axi_awvalid ? 1:0) == npending); + assert(f_axi_wr_pending == (o_axi_wvalid&&!o_axi_awvalid ? 1:0)); + + // + // ... + // + end + always @(*) + if (o_axi_awvalid) + assert(o_axi_wvalid); + + // Some quick read checks + always @(*) + if (f_axi_rd_nbursts > 0) + begin + assert(!direction); + assert(f_axi_rd_nbursts+(o_axi_arvalid ? 1:0) + == npending); + assert(f_axi_awr_nbursts == 0); + + // + // ... + // + end + + always @(*) + if (direction) + begin + assert(npending == (o_axi_awvalid ? 1:0) + f_axi_awr_nbursts); + assert(!o_axi_arvalid); + assert(f_axi_rd_nbursts == 0); + assert(!i_axi_rvalid); + end else begin + assert(npending == (o_axi_arvalid ? 1:0) + f_axi_rd_nbursts); + assert(!o_axi_awvalid); + assert(!o_axi_wvalid); + assert(f_axi_awr_nbursts == 0); + end + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Pending counter properties + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + always @(*) + begin + assert(npending <= { 1'b1, {(LGFIFO){1'b0}} }); + assert(empty == (npending == 0)); + assert(full == (npending == {1'b1, {(LGFIFO){1'b0}} })); + assert(nearfull == (npending >= {1'b0, {(LGFIFO){1'b1}} })); + if (full) + assert(!m_ready); + end + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Assertions about the AXI4 ouputs + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // Write response channel + always @(posedge i_clk) + // We keep bready high, so the other condition doesn't + // need to be checked + assert(o_axi_bready); + + // AXI read data channel signals + always @(posedge i_clk) + // We keep o_axi_rready high, so the other condition's + // don't need to be checked here + assert(o_axi_rready); + + // + // AXI write address channel + // + // + always @(*) + begin + if (o_axi_awvalid || o_axi_wvalid || f_axi_awr_nbursts>0) + assert(direction); + // + // ... + // + end + // + // AXI read address channel + // + always @(*) + begin + if (o_axi_arvalid || i_axi_rvalid || f_axi_rd_nbursts > 0) + assert(!direction); + // + // ... + // + end + + // + // AXI write response channel + // + + + // + // AXI read data channel signals + // + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Formal contract check + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // Prove that a write to this address will change this value + // + + // Some extra register declarations + // {{{ + (* anyconst *) reg [C_AXI_ADDR_WIDTH-1:0] f_const_addr; + reg [C_AXI_DATA_WIDTH-1:0] f_data; + // }}} + + // + // Assume a basic bus response to the given data and address + // + integer iN; + + // f_data + // {{{ + initial f_data = 0; + always @(posedge i_clk) + if (o_axi_wvalid && i_axi_wready && o_axi_awaddr == f_const_addr) + begin + for(iN=0; iN 0) + f_wb_addr[0 +: SUBW] = ~f_wb_addr[0 +: SUBW]; + end + // }}} + + // Assume the address is Wishbone word aligned + // {{{ + generate if (DW > 8) + begin + always @(*) + assume(f_const_addr[$clog2(DW)-4:0] == 0); + end endgenerate + // }}} + + // f_axi_data -- Replicate f_wb_data across the whole word + // {{{ + always @(*) + f_axi_data = {(C_AXI_DATA_WIDTH/DW){f_wb_data}}; + // }}} + + // + // ... + // + + always @(*) + begin + f_valid_wb_response = 1; + for(iN=0; iN 8) + begin + always @(*) + if (o_axi_awvalid) + assert(o_axi_awaddr[$clog2(DW)-4:0] == 0); + + always @(*) + if (o_axi_arvalid) + assert(o_axi_araddr[$clog2(DW)-4:0] == 0); + + end endgenerate + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Cover checks + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + reg [F_LGDEPTH-1:0] r_hit_reads, r_hit_writes, + r_check_fault, check_fault, + cvr_nreads, cvr_nwrites; + reg cvr_flushed, cvr_read2write, cvr_write2read; + + initial r_hit_reads = 0; + always @(posedge i_clk) + if (i_reset) + r_hit_writes <= 0; + else if (f_axi_awr_nbursts > 3) + r_hit_writes <= 1; + + initial r_hit_reads = 0; + always @(posedge i_clk) + if (i_reset) + r_hit_reads <= 0; + else if (f_axi_rd_nbursts > 3) + r_hit_reads <= 1; + + always @(*) + begin + check_fault = 0; + if (!i_wb_cyc && o_axi_awvalid) + check_fault = 1; + if (!i_wb_cyc && o_axi_wvalid) + check_fault = 1; + if (!i_wb_cyc && f_axi_awr_nbursts > 0) + check_fault = 1; + if (!i_wb_cyc && i_axi_bvalid) + check_fault = 1; + // + if (!i_wb_cyc && o_axi_arvalid) + check_fault = 1; + if (!i_wb_cyc && f_axi_rd_outstanding > 0) + check_fault = 1; + if (!i_wb_cyc && i_axi_rvalid) + check_fault = 1; + if (!i_wb_cyc && (o_wb_ack | o_wb_err)) + check_fault = 1; + + if (flushing) + check_fault = 1; + end + + initial r_check_fault = 0; + always @(posedge i_clk) + if (i_reset) + r_check_fault <= 0; + else if (check_fault) + r_check_fault <= 1; + + always @(*) + cover(r_hit_writes && r_hit_reads && f_axi_rd_nbursts == 0 + && f_axi_awr_nbursts == 0 + && !o_axi_awvalid && !o_axi_arvalid && !o_axi_wvalid + && !i_axi_bvalid && !i_axi_rvalid + && !o_wb_ack && !o_wb_stall && !i_wb_stb + && !check_fault && !r_check_fault); + + // + // ... + // + + initial cvr_flushed = 1'b0; + always @(posedge i_clk) + if (i_reset) + cvr_flushed <= 1'b0; + else if (flushing) + cvr_flushed <= 1'b1; + + always @(*) + begin + cover(!i_reset && cvr_flushed && !flushing); + cover(!i_reset && cvr_flushed && !flushing && !o_wb_stall); + end + + // + // Let's cover our ability to turn around, from reads to writes or from + // writes to reads. + // + // Note that without the RMW option above, switching direction requires + // dropping i_wb_cyc. Let's just make certain here, that if we do so, + // we don't drop it until after all of the returns come back. + // + initial cvr_read2write = 0; + always @(posedge i_clk) + if (i_reset || (!i_wb_cyc && f_wb_nreqs != f_wb_nacks)) + cvr_read2write <= 0; + else if (!direction && !empty && m_we) + cvr_read2write <= 1; + + initial cvr_write2read = 0; + always @(posedge i_clk) + if (i_reset || (!i_wb_cyc && f_wb_nreqs != f_wb_nacks)) + cvr_write2read <= 0; + else if (direction && !empty && !m_we) + cvr_write2read <= 1; + + always @(*) + begin + cover(cvr_read2write && direction && o_wb_ack && f_wb_outstanding == 1); + cover(cvr_write2read && !direction && o_wb_ack && f_wb_outstanding == 1); + end + + reg [2:0] cvr_ack_after_abort; + + initial cvr_ack_after_abort = 0; + always @(posedge i_clk) + if (i_reset) + cvr_ack_after_abort <= 0; + else begin + if (!i_wb_cyc) + cvr_ack_after_abort[2:0] <= (empty) ? 0 : 3'b01; + if (cvr_ack_after_abort[0] && i_wb_cyc && r_stb && flushing) + cvr_ack_after_abort[1] <= 1; + if (o_wb_ack && &cvr_ack_after_abort[1:0]) + cvr_ack_after_abort[2] <= 1; + end + + always @(*) + cover(&cvr_ack_after_abort[1:0]); + always @(*) + cover(!flushing && (&cvr_ack_after_abort[1:0])); + always @(*) + cover(&cvr_ack_after_abort[2:0]); + always @(*) + cover(!i_wb_cyc && &cvr_ack_after_abort[2:0]); + + initial cvr_nwrites = 0; + always @(posedge i_clk) + if (i_reset || flushing || !i_wb_cyc || !i_wb_we || o_wb_err) + cvr_nwrites <= 0; + else if (i_axi_bvalid && o_axi_bready) + cvr_nwrites <= cvr_nwrites + 1; + + initial cvr_nreads = 0; + always @(posedge i_clk) + if (i_reset || flushing || !i_wb_cyc || i_wb_we || o_wb_err) + cvr_nreads <= 0; + else if (i_axi_rvalid && o_axi_rready) + cvr_nreads <= cvr_nreads + 1; + + always @(*) + cover(cvr_nwrites == 3 && !o_wb_ack && !o_wb_err && !i_wb_cyc); + + always @(*) + cover(cvr_nreads == 3 && !o_wb_ack && !o_wb_err && !i_wb_cyc); + + // + // Generate a cover that doesn't include an abort + // {{{ + (* anyconst *) reg f_never_abort; + + always @(*) + if (f_never_abort && f_wb_nacks != f_wb_nreqs) + assume(!i_reset && i_wb_cyc && !o_wb_err); + + always @(posedge i_clk) + if (f_never_abort && $past(o_wb_ack) && o_wb_ack) + assume($changed(o_wb_data)); + + always @(*) + cover(cvr_nreads == 3 && !o_wb_ack && !o_wb_err && !i_wb_cyc + && f_never_abort); + // }}} + + // }}} +`endif // FORMAL +// }}} +endmodule -- cgit v1.2.3