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/axiempty.v | 490 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 490 insertions(+) create mode 100644 rtl/wb2axip/axiempty.v (limited to 'rtl/wb2axip/axiempty.v') diff --git a/rtl/wb2axip/axiempty.v b/rtl/wb2axip/axiempty.v new file mode 100644 index 0000000..d0ec896 --- /dev/null +++ b/rtl/wb2axip/axiempty.v @@ -0,0 +1,490 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: axiempty.v +// {{{ +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: A basic AXI core to provide a response to an AXI master when +// no other slaves are connected to the bus. All results are +// bus errors. +// +// Creator: Dan Gisselquist, Ph.D. +// Gisselquist Technology, LLC +// +//////////////////////////////////////////////////////////////////////////////// +// }}} +// Copyright (C) 2019-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 axiempty #( + // {{{ + parameter integer C_AXI_ID_WIDTH = 2, + parameter integer C_AXI_DATA_WIDTH = 32, + // Verilator lint_off UNUSED + parameter integer C_AXI_ADDR_WIDTH = 6, + // Verilator lint_on UNUSED + parameter [0:0] OPT_LOWPOWER = 0 + // Some useful short-hand definitions + // localparam AW = C_AXI_ADDR_WIDTH, + // localparam DW = C_AXI_DATA_WIDTH + // }}} + ) ( + // {{{ + input wire S_AXI_ACLK, + input wire S_AXI_ARESETN, + // + input wire S_AXI_AWVALID, + output wire S_AXI_AWREADY, + input wire [C_AXI_ID_WIDTH-1:0] S_AXI_AWID, + // + input wire S_AXI_WVALID, + output wire S_AXI_WREADY, + input wire S_AXI_WLAST, + // + output wire S_AXI_BVALID, + input wire S_AXI_BREADY, + output wire [C_AXI_ID_WIDTH-1:0] S_AXI_BID, + output wire [1:0] S_AXI_BRESP, + // + input wire S_AXI_ARVALID, + output wire S_AXI_ARREADY, + input wire [C_AXI_ID_WIDTH-1:0] S_AXI_ARID, + input wire [7:0] S_AXI_ARLEN, + // + output wire S_AXI_RVALID, + input wire S_AXI_RREADY, + output wire [C_AXI_ID_WIDTH-1:0] S_AXI_RID, + output wire [C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA, + output wire S_AXI_RLAST, + output wire [1:0] S_AXI_RRESP + // }}} + ); + + localparam IW = C_AXI_ID_WIDTH; + // Double buffer the write response channel only + reg [IW-1 : 0] axi_bid; + reg axi_bvalid; + + //////////////////////////////////////////////////////////////////////// + // + // Write logic + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // + // Start with the two skid buffers + // {{{ + wire m_awvalid, m_wvalid; + wire m_awready, m_wready, m_wlast; + wire [IW-1:0] m_awid; + // + skidbuffer #(.DW(IW), .OPT_OUTREG(1'b0)) + awskd(S_AXI_ACLK, !S_AXI_ARESETN, + S_AXI_AWVALID, S_AXI_AWREADY, S_AXI_AWID, + m_awvalid, m_awready, m_awid ); + + skidbuffer #(.DW(1), .OPT_OUTREG(1'b0)) + wskd(S_AXI_ACLK, !S_AXI_ARESETN, + S_AXI_WVALID, S_AXI_WREADY, S_AXI_WLAST, + m_wvalid, m_wready, m_wlast ); + // }}} + + // m_awready, m_wready + // {{{ + // The logic here is pretty simple--accept a write address burst + // into the skid buffer, then leave it there while the write data comes + // on. Once we get to the last write data element, accept both it and + // the address. This spares us the trouble of counting out the elements + // in the write burst. + // + assign m_awready= (m_awvalid && m_wvalid && m_wlast) + && (!S_AXI_BVALID || S_AXI_BREADY); + assign m_wready = !m_wlast || m_awready; + // }}} + + // bvalid + // {{{ + // As soon as m_awready above, a packet has come through successfully. + // Acknowledge it with a bus error. + // + initial axi_bvalid = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + axi_bvalid <= 1'b0; + else if (m_awready) + axi_bvalid <= 1'b1; + else if (S_AXI_BREADY) + axi_bvalid <= 1'b0; + // }}} + + // bid + // {{{ + always @(posedge S_AXI_ACLK) + if (m_awready) + axi_bid <= m_awid; + // }}} + + assign S_AXI_BVALID = axi_bvalid; + assign S_AXI_BID = axi_bid; + assign S_AXI_BRESP = 2'b11; // An interconnect bus error + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Read half + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + reg [IW-1:0] rid, axi_rid; + reg axi_arready, axi_rlast, axi_rvalid; + reg [8:0] axi_rlen; + + // axi_arready + // {{{ + initial axi_arready = 1; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + axi_arready <= 1; + else if (S_AXI_ARVALID && S_AXI_ARREADY) + axi_arready <= (S_AXI_ARLEN==0)&&(!S_AXI_RVALID|| S_AXI_RREADY); + else if (!S_AXI_RVALID || S_AXI_RREADY) + begin + if ((!axi_arready)&&(S_AXI_RVALID)) + axi_arready <= (axi_rlen <= 2); + end + // }}} + + // axi_rlen + // {{{ + initial axi_rlen = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + axi_rlen <= 0; + else if (S_AXI_ARVALID && S_AXI_ARREADY) + axi_rlen <= (S_AXI_ARLEN+1) + + ((S_AXI_RVALID && !S_AXI_RREADY) ? 1:0); + else if (S_AXI_RREADY && S_AXI_RVALID) + axi_rlen <= axi_rlen - 1; + // }}} + + // rid + // {{{ + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN && OPT_LOWPOWER) + rid <= 0; + else if (S_AXI_ARREADY && (!OPT_LOWPOWER || S_AXI_ARVALID)) + rid <= S_AXI_ARID; + else if (OPT_LOWPOWER && S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST) + rid <= 0; + // }}} + + // axi_rvalid + // {{{ + initial axi_rvalid = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + axi_rvalid <= 0; + else if (S_AXI_ARVALID || (axi_rlen > 1)) + axi_rvalid <= 1; + else if (S_AXI_RREADY) + axi_rvalid <= 0; + // }}} + + // axi_rid + // {{{ + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN && OPT_LOWPOWER) + axi_rid <= 0; + else if (!S_AXI_RVALID || S_AXI_RREADY) + begin + if (S_AXI_ARVALID && S_AXI_ARREADY) + axi_rid <= S_AXI_ARID; + else if (OPT_LOWPOWER && S_AXI_RVALID && S_AXI_RREADY + && S_AXI_RLAST) + axi_rid <= 0; + else + axi_rid <= rid; + end + // }}} + + // axi_rlast + // {{{ + initial axi_rlast = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN && OPT_LOWPOWER) + axi_rlast <= 0; + else if (!S_AXI_RVALID || S_AXI_RREADY) + begin + if (S_AXI_ARVALID && S_AXI_ARREADY) + axi_rlast <= (S_AXI_ARLEN == 0); + else if (S_AXI_RVALID) + axi_rlast <= (axi_rlen == 2); + else + axi_rlast <= (axi_rlen == 1); + end + // }}} + + // + assign S_AXI_ARREADY = axi_arready; + assign S_AXI_RVALID = axi_rvalid; + assign S_AXI_RID = axi_rid; + assign S_AXI_RDATA = 0; + assign S_AXI_RRESP = 2'b11; + assign S_AXI_RLAST = axi_rlast; + // }}} + + // Make Verilator happy + // {{{ + // Verilator lint_off UNUSED + wire unused; + assign unused = &{ 1'b0 }; + // Verilator lint_on UNUSED + // }}} +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +// +// Formal properties +// {{{ +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +`ifdef FORMAL + // + // The following properties are only some of the properties used + // to verify this core + // + reg f_past_valid; + initial f_past_valid = 0; + always @(posedge S_AXI_ACLK) + f_past_valid <= 1; + + always @(*) + if (!f_past_valid) + assume(!S_AXI_ARESETN); + + faxi_slave #( + // {{{ + .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_slave( + // {{{ + .i_clk(S_AXI_ACLK), + .i_axi_reset_n(S_AXI_ARESETN), + // + // Address write channel + // {{{ + .i_axi_awvalid(S_AXI_AWVALID), + .i_axi_awready(S_AXI_AWREADY), + .i_axi_awid( S_AXI_AWID), + .i_axi_awaddr( {(C_AXI_ADDR_WIDTH){1'b0}}), + .i_axi_awlen( S_AXI_AWLEN), + .i_axi_awsize( LSB[2:0]), + .i_axi_awburst(2'b0), + .i_axi_awlock( 1'b0), + .i_axi_awcache(4'h0), + .i_axi_awprot( 3'h0), + .i_axi_awqos( 4'h0), + // }}} + // Write Data Channel + // {{{ + // Write Data + .i_axi_wdata({(C_AXI_DATA_WIDTH){1'b0}}), + .i_axi_wstrb({(C_AXI_DATA_WIDTH/8){1'b0}}), + .i_axi_wlast(S_AXI_WLAST), + .i_axi_wvalid(S_AXI_WVALID), + .i_axi_wready(S_AXI_WREADY), + // }}} + // Write response + // {{{ + .i_axi_bvalid(S_AXI_BVALID), + .i_axi_bready(S_AXI_BREADY), + .i_axi_bid( S_AXI_BID), + .i_axi_bresp( S_AXI_BRESP), + // }}} + // Read address channel + // {{{ + .i_axi_arvalid(S_AXI_ARVALID), + .i_axi_arready(S_AXI_ARREADY), + .i_axi_arid( S_AXI_ARID), + .i_axi_araddr( {(C_AXI_ADDR_WIDTH){1'b0}}), + .i_axi_arlen( S_AXI_ARLEN), + .i_axi_arsize( LSB[2:0]), + .i_axi_arburst(2'b00), + .i_axi_arlock( 1'b0), + .i_axi_arcache(4'h0), + .i_axi_arprot( 3'h0), + .i_axi_arqos( 4'h0), + // }}} + // Read data return channel + // {{{ + .i_axi_rvalid(S_AXI_RVALID), + .i_axi_rready(S_AXI_RREADY), + .i_axi_rid(S_AXI_RID), + .i_axi_rdata(S_AXI_RDATA), + .i_axi_rresp(S_AXI_RRESP), + .i_axi_rlast(S_AXI_RLAST), + // + // ... + // }}} + ); + + // + + //////////////////////////////////////////////////////////////////////// + // + // Write induction properties + // + //////////////////////////////////////////////////////////////////////// + // + // {{{ + + + // + // ... + // + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Read induction properties + // + //////////////////////////////////////////////////////////////////////// + // + // {{{ + + // + // ... + // + + always @(posedge S_AXI_ACLK) + if (f_past_valid && $rose(S_AXI_RLAST)) + assert(S_AXI_ARREADY); + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Contract checking + // + //////////////////////////////////////////////////////////////////////// + // + // {{{ + + // + // ... + // + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Cover properties + // + //////////////////////////////////////////////////////////////////////// + // + // {{{ + reg f_wr_cvr_valid, f_rd_cvr_valid; + + initial f_wr_cvr_valid = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + f_wr_cvr_valid <= 0; + else if (S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN > 4) + f_wr_cvr_valid <= 1; + + always @(*) + cover(!S_AXI_BVALID && axi_awready && !m_awvalid + && f_wr_cvr_valid /* && ... */)); + + initial f_rd_cvr_valid = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + f_rd_cvr_valid <= 0; + else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN > 4) + f_rd_cvr_valid <= 1; + + always @(*) + cover(S_AXI_ARREADY && f_rd_cvr_valid /* && ... */); + + // + // Generate cover statements associated with multiple successive bursts + // + // These will be useful for demonstrating the throughput of the core. + // + reg [4:0] f_dbl_rd_count, f_dbl_wr_count; + + initial f_dbl_wr_count = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + f_dbl_wr_count = 0; + else if (S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN == 3) + begin + if (!(&f_dbl_wr_count)) + f_dbl_wr_count <= f_dbl_wr_count + 1; + end + + always @(*) + cover(S_AXI_ARESETN && (f_dbl_wr_count > 1)); //! + + always @(*) + cover(S_AXI_ARESETN && (f_dbl_wr_count > 3)); //! + + always @(*) + cover(S_AXI_ARESETN && (f_dbl_wr_count > 3) && !m_awvalid + &&(!S_AXI_AWVALID && !S_AXI_WVALID && !S_AXI_BVALID) + && (f_axi_awr_nbursts == 0) + && (f_axi_wr_pending == 0)); //!! + + initial f_dbl_rd_count = 0; + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + f_dbl_rd_count = 0; + else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN == 3) + begin + if (!(&f_dbl_rd_count)) + f_dbl_rd_count <= f_dbl_rd_count + 1; + end + + always @(*) + cover(!S_AXI_ARESETN && (f_dbl_rd_count > 3) + /* && ... */ + && !S_AXI_ARVALID && !S_AXI_RVALID); + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Assumptions necessary to pass a formal check + // + //////////////////////////////////////////////////////////////////////// + // + // + + // + // No limiting assumptions at present, check is currently full and + // complete + // +`endif +// }}} +endmodule -- cgit v1.2.3