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/aximm2s.v | 2158 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2158 insertions(+) create mode 100644 rtl/wb2axip/aximm2s.v (limited to 'rtl/wb2axip/aximm2s.v') diff --git a/rtl/wb2axip/aximm2s.v b/rtl/wb2axip/aximm2s.v new file mode 100644 index 0000000..b4c1056 --- /dev/null +++ b/rtl/wb2axip/aximm2s.v @@ -0,0 +1,2158 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: aximm2s +// {{{ +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: Converts an AXI (full) memory port to an AXI-stream +// interface. +// // {{{ +// While I am aware that other vendors sell similar components, if you +// look under the hood you'll find no relation to anything but my own +// work here. +// +// Registers: +// +// 0: CMD_CONTROL +// Controls the transaction via either starting or aborting an +// ongoing transaction, provides feedback regarding the current +// status. +// +// [31] r_busy +// True if the core is in the middle of a transaction +// +// [30] r_err +// True if the core has detected an error, a bus error +// while the FIFO is reading. +// +// Writing a '1' to this bit while the core is idle will clear it. +// New transfers will not start until this bit is cleared. +// +// [29] r_complete +// True if the transaction has completed, whether normally or +// abnormally (error or abort). +// +// Any write to the CMD_CONTROL register will clear this flag. +// +// [28] r_continuous +// Normally the FIFO gets cleared and reset between operations. +// However, if you set r_continuous, the core will then expect +// a second operation to take place following the first one. +// In this case, the operation will complete but the FIFO won't +// get cleared. During this time, the FIFO will not fill further. +// +// Any write to the CMD_CONTROL register while the core is not +// busy will adjust this bit. +// +// [27] !r_increment +// +// If clear, the core reads from subsequent and incrementing +// addresses. If set, the core reads from the same address +// throughout a transaction. +// +// Writes to CMD_CONTROL while the core is idle will adjust this +// bit. +// +// [20:16] LGFIFO +// These are read-only bits, returning the size of the FIFO. +// +// ABORT +// If the core is busy, and ABORT_KEY (currently set to 8'h6d +// below) is written to the top 8-bits of this register, +// the current transfer will be aborted. Any pending reads +// will be completed, but nothing more will be written to the +// stream. +// +// Alternatively, the core will enter into an abort state +// following any returned bus error indications. +// +// 4: (Unused and reserved) +// +// 8-c: CMD_ADDRLO, CMD_ADDR_HI +// [C_AXI_ADDR_WIDTH-1:($clog2(C_AXI_DATA_WIDTH)-3)] +// If idle, the address the core will read from when it starts. +// If busy, the address the core is currently reading from. +// Upon completion, the address either returns to the starting +// address (if r_continuous is clear), or otherwise becomes the +// address where the core left off. In the case of an abort or an +// error, this will be (near) the address that was last read. +// +// Why "near"? Because this address records the reads that have +// been issued while no error is pending. If a bus error return +// comes back, there may have been several more reads issued before +// that error address. +// +// 10-14: (Unused and reserved) +// +// 18-1c: CMD_LENLO, CMD_LENHI +// [LGLEN-1:0] +// The size of the transfer in bytes. Only accepts aligned +// addresses, therefore bits [($clog2(C_AXI_DATA_WIDTH)-3):0] +// will always be forced to zero. To find out what size bus +// this core is conencted to, or the maximum transfer length, +// write a -1 to this value and read the returning result. +// Only the active bits will be set. +// +// While the core is busy, reads from this address will return +// the number of items still to be read from the bus. +// +// I hope to eventually add support for unaligned bursts. Such +// support is not currently part of this core. +// +// }}} +// +// Status: +// {{{ +// 1. The core passes both cover checks and formal property (assertion) +// based checks. It has not (yet) been tested in real hardware. +// +// 2. I'd like to support unaligned addresses and lengths. This will +// require aligning the data coming out of the FIFO as well. +// As written, the core doesn't yet support these. +// +// }}} +// 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 aximm2s #( + // {{{ + parameter C_AXI_ADDR_WIDTH = 32, + parameter C_AXI_DATA_WIDTH = 32, + parameter C_AXI_ID_WIDTH = 1, + // + // We support five 32-bit AXI-lite registers, requiring 5-bits + // of AXI-lite addressing + localparam C_AXIL_ADDR_WIDTH = 5, + localparam C_AXIL_DATA_WIDTH = 32, + // + // The bottom ADDRLSB bits of any AXI address are subword bits + localparam ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3, + localparam AXILLSB = $clog2(C_AXIL_DATA_WIDTH)-3, + // + // OPT_UNALIGNED: Allow unaligned accesses, address requests + // and sizes which may or may not match the underlying data + // width. If set, the core will quietly align these requests. + parameter [0:0] OPT_UNALIGNED = 1'b0, + // + // OPT_TKEEP [Future]: If set, will also add TKEEP signals to + // the outgoing slave interface. This is necessary if ever you + // wish to output partial stream words, such as might happen if + // the length were ever something other than a full number of + // words. (Not yet implemented) + // parameter [0:0] OPT_TKEEP = 1'b0, + // + // OPT_TLAST: If enabled, will embed TLAST=1 at the end of every + // commanded burst. If disabled, TLAST will be set to a + // constant 1'b1. + parameter [0:0] OPT_TLAST = 1'b0, + // + parameter [0:0] OPT_LOWPOWER = 1'b0, + parameter [0:0] OPT_CLKGATE = OPT_LOWPOWER, + // + // ABORT_KEY is the value that, when written to the top 8-bits + // of the control word, will abort any ongoing operation. + parameter [7:0] ABORT_KEY = 8'h6d, + // + // The size of the FIFO + parameter LGFIFO = 9, + // + // Maximum number of bytes that can ever be transferred, in + // log-base 2 + parameter LGLEN = 20, + // + // AXI_ID is the ID we will use for all of our AXI transactions + parameter AXI_ID = 0 + // }}} + ) ( + // {{{ + input wire S_AXI_ACLK, + input wire S_AXI_ARESETN, + // + // The stream interface + // {{{ + output wire M_AXIS_TVALID, + input wire M_AXIS_TREADY, + output wire [C_AXI_DATA_WIDTH-1:0] M_AXIS_TDATA, + output wire M_AXIS_TLAST, + // }}} + // + // The control interface + // {{{ + input wire S_AXIL_AWVALID, + output wire S_AXIL_AWREADY, + input wire [C_AXIL_ADDR_WIDTH-1:0] S_AXIL_AWADDR, + input wire [2:0] S_AXIL_AWPROT, + // + input wire S_AXIL_WVALID, + output wire S_AXIL_WREADY, + input wire [C_AXIL_DATA_WIDTH-1:0] S_AXIL_WDATA, + input wire [C_AXIL_DATA_WIDTH/8-1:0] S_AXIL_WSTRB, + // + output wire S_AXIL_BVALID, + input wire S_AXIL_BREADY, + output wire [1:0] S_AXIL_BRESP, + // + input wire S_AXIL_ARVALID, + output wire S_AXIL_ARREADY, + input wire [C_AXIL_ADDR_WIDTH-1:0] S_AXIL_ARADDR, + input wire [2:0] S_AXIL_ARPROT, + // + output wire S_AXIL_RVALID, + input wire S_AXIL_RREADY, + output wire [C_AXIL_DATA_WIDTH-1:0] S_AXIL_RDATA, + output wire [1:0] S_AXIL_RRESP, + // }}} + // + + // + // The AXI (full) read interface + // {{{ + output wire M_AXI_ARVALID, + input wire M_AXI_ARREADY, + output wire [C_AXI_ID_WIDTH-1:0] M_AXI_ARID, + output wire [C_AXI_ADDR_WIDTH-1:0] M_AXI_ARADDR, + output wire [7:0] M_AXI_ARLEN, + output wire [2:0] M_AXI_ARSIZE, + output wire [1:0] M_AXI_ARBURST, + output wire M_AXI_ARLOCK, + output wire [3:0] M_AXI_ARCACHE, + output wire [2:0] M_AXI_ARPROT, + output wire [3:0] M_AXI_ARQOS, + // + input wire M_AXI_RVALID, + output wire M_AXI_RREADY, + input wire [C_AXI_DATA_WIDTH-1:0] M_AXI_RDATA, + input wire M_AXI_RLAST, + input wire [C_AXI_ID_WIDTH-1:0] M_AXI_RID, + input wire [1:0] M_AXI_RRESP, + // }}} + // + // + // Create an output signal to indicate that we've finished + output reg o_int + // }}} + ); + + // Local parameter declarations + // {{{ + localparam [2:0] CMD_CONTROL = 3'b000, + // CMD_UNUSED_1 = 3'b001, + CMD_ADDRLO = 3'b010, + CMD_ADDRHI = 3'b011, + // CMD_UNUSED_2 = 3'b100, + // CMD_UNUSED_3 = 3'b101, + CMD_LENLO = 3'b110, + CMD_LENHI = 3'b111; + localparam CBIT_BUSY = 31, + CBIT_ERR = 30, + CBIT_COMPLETE = 29, + CBIT_CONTINUOUS = 28, + CBIT_INCREMENT = 27; + localparam TMP_LGMAXBURST=(LGFIFO > 8) ? 8 : LGFIFO-1; + localparam LGMAXBURST = ((4096/(C_AXI_DATA_WIDTH/8)) + > (1< C_AXIL_DATA_WIDTH) + begin + cmd_addr <= new_wideaddr[C_AXI_ADDR_WIDTH-1:0]; + end + CMD_LENLO: begin + cmd_length_w <= new_widelen[ADDRLSB +: LGLENW]; + zero_length <= (new_widelen[ADDRLSB +: LGLENW] == 0); + cmd_length_aligned_w <= new_widelen[ADDRLSB +: LGLENW] + + (unaligned_cmd_addr ? 1:0); + ar_multiple_full_bursts <= |new_widelen[LGLEN-1:(ADDRLSB+LGMAXBURST)]; + ar_multiple_fixed_bursts <= |new_widelen[LGLEN-1:(ADDRLSB+LGMAX_FIXED_BURST)]; + end + CMD_LENHI: begin + cmd_length_w <= new_widelen[ADDRLSB +: LGLENW]; + zero_length <= (new_widelen[ADDRLSB +: LGLENW] == 0); + cmd_length_aligned_w <= new_widelen[ADDRLSB +: LGLENW] + + (unaligned_cmd_addr ? 1:0); + ar_multiple_full_bursts <= |new_widelen[LGLEN-1:(ADDRLSB+LGMAXBURST)]; + ar_multiple_fixed_bursts <= |new_widelen[LGLEN-1:(ADDRLSB+LGMAX_FIXED_BURST)]; + end + default: begin end + endcase + end else if(r_busy && r_continuous && !axi_abort_pending + && r_increment) + cmd_addr <= axi_raddr + + ((M_AXI_RVALID && !M_AXI_RRESP[1] + && (!unaligned_cmd_addr || realign_last_valid)) + ? (1<> (realignment * 8); + + initial last_valid = 1'b0; + always @(posedge i_clk) + if (reset_fifo) + last_valid <= 0; + else if (M_AXI_RVALID && M_AXI_RREADY) + last_valid <= 1'b1; + else if (!r_busy) + last_valid <= 1'b0; + + assign realign_last_valid = last_valid; + + always @(*) + corollary_shift = -realignment; + + always @(posedge i_clk) + if (M_AXI_RVALID && M_AXI_RREADY) + r_write_data <= (M_AXI_RDATA << (corollary_shift*8)) + | last_data; + else if (!fifo_full) + r_write_data <= last_data; + + initial r_write_to_fifo = 1'b0; + always @(posedge i_clk) + if (reset_fifo) + r_write_to_fifo <= 1'b0; + else if (M_AXI_RVALID && M_AXI_RREADY) + r_write_to_fifo <= last_valid || !unaligned_cmd_addr; + else if (!fifo_full) + r_write_to_fifo <= 1'b0; + + assign write_to_fifo = r_write_to_fifo; + assign write_data = r_write_data; + + end else begin : ALIGNED_DATA + + assign write_to_fifo = M_AXI_RVALID && M_AXI_RREADY; + assign write_data = M_AXI_RDATA; + assign realign_last_valid = 0; + + end endgenerate + // }}} + + assign read_from_fifo = M_AXIS_TVALID && M_AXIS_TREADY; + assign M_AXIS_TVALID = !fifo_empty; + + // Write the results to the FIFO + // {{{ + generate if (OPT_TLAST) + begin : FIFO_W_TLAST + // FIFO section--used if we have to add a TLAST signal to the + // data stream + // {{{ + reg pre_tlast; + wire tlast; + + // tlast will be set on the last data word of any commanded + // burst. + + // Appropriately, pre_tlast = (something) && M_AXI_RVALID + // && M_AXI_RREADY && M_AXI_RLAST + // We can simplify this greatly, since any time M_AXI_RVALID is + // true, we also know that M_AXI_RREADY will be true. This + // allows us to get rid of the RREADY condition. Next, we can + // simplify the RVALID condition since we'll never write to the + // FIFO if RVALID isn't also true. Finally, we can get rid of + // M_AXI_RLAST since this is captured by rd_last_remaining. + always @(*) + pre_tlast = rd_last_remaining; + + if (OPT_UNALIGNED) + begin : GEN_UNALIGNED_TLAST + reg r_tlast; + + // REALIGN delays the data by one clock period. We'll + // also need to delay the last as well. + // Note that no one cares what tlast is if write_to_fifo + // is zero, allowing us to massively simplify this. + always @(posedge i_clk) + r_tlast <= pre_tlast; + + assign tlast = r_tlast; + + end else begin : NO_UNALIGNED_TLAST + + assign tlast = pre_tlast; + end + + + sfifo #( + // {{{ + .BW(C_AXI_DATA_WIDTH+1), .LGFLEN(LGFIFO) + // }}} + ) sfifo( + // {{{ + i_clk, reset_fifo, + write_to_fifo, { tlast, write_data }, fifo_full, fifo_fill, + read_from_fifo, { M_AXIS_TLAST, M_AXIS_TDATA }, fifo_empty + // }}} + ); + // }}} + end else begin : NO_TLAST_FIFO + + // FIFO section, where TLAST is held at 1'b1 + // {{{ + sfifo #( + // {{{ + .BW(C_AXI_DATA_WIDTH), .LGFLEN(LGFIFO) + // }}} + ) sfifo( + // {{{ + i_clk, reset_fifo, + write_to_fifo, write_data, fifo_full, fifo_fill, + read_from_fifo, M_AXIS_TDATA, fifo_empty + // }}} + ); + + assign M_AXIS_TLAST = 1'b1; + // }}} + end endgenerate + // }}} + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // The incoming AXI (full) protocol section + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + // + + // Some counters to keep track of our state + // {{{ + + + // Count the number of word writes left to be requested, starting + // with the overall command length and then reduced by M_AWLEN on + // each address write + // {{{ + always @(*) + begin + ar_next_remaining = ar_requests_remaining; + ar_next_remaining = ar_requests_remaining + + { {(LGLENWA-8){phantom_start}}, + (phantom_start) ? ~M_AXI_ARLEN : 8'h00}; + end + + always @(posedge i_clk) + if (!r_busy) + r_pre_start <= 1; + else + r_pre_start <= 0; + + always @(posedge i_clk) + if (!r_busy) + begin + ar_needs_alignment <= 0; + + if (|new_wideaddr[ADDRLSB +: LGMAXBURST]) + begin + if (|new_widelen[LGLEN-1:(LGMAXBURST+ADDRLSB)]) + ar_needs_alignment <= 1; + if (~new_wideaddr[ADDRLSB +: LGMAXBURST] + < new_widelen[ADDRLSB +: LGMAXBURST]) + ar_needs_alignment <= 1; + end + end + + initial ar_none_remaining = 1; + initial ar_requests_remaining = 0; + always @(posedge i_clk) + if (!r_busy) + begin + ar_requests_remaining <= cmd_length_aligned_w; + ar_none_remaining <= zero_length; + ar_multiple_bursts_remaining + <= |cmd_length_aligned_w[LGLENWA-1:LGMAXBURST+1]; + end else if (cmd_abort || axi_abort_pending) + begin + ar_requests_remaining <= 0; + ar_none_remaining <= 1; + ar_multiple_bursts_remaining <= 0; + + end else if (phantom_start) + begin + // Verilator lint_off WIDTH + ar_requests_remaining + <= ar_next_remaining; + ar_none_remaining <= (ar_next_remaining == 0); + ar_multiple_bursts_remaining + <= |ar_next_remaining[LGLENWA-1:LGMAXBURST+1]; + // Verilator lint_on WIDTH + end + // }}} + + // Calculate the maximum possible burst length, ignoring 4kB boundaries + // {{{ + always @(*) + addralign = 1+(~cmd_addr[ADDRLSB +: LGMAXBURST]); + + always @(*) + begin + initial_burstlen = (1<= 8) + begin : GEN_BIG_AWLEN + // Verilator lint_off WIDTH + + always @(posedge i_clk) + if (!r_busy) + axi_arlen <= initial_burstlen - 1; + else if (!M_AXI_ARVALID || M_AXI_ARREADY) + axi_arlen <= r_max_burst - 1; + + // Verilator lint_on WIDTH + end else begin : GEN_SHORT_AWLEN + + always @(posedge i_clk) + begin + axi_arlen[7:LGMAXBURST] <= 0; + if (!r_busy) + axi_arlen[LGMAXBURST:0] <= initial_burstlen - 1; + else if (!M_AXI_ARVALID || M_AXI_ARREADY) + axi_arlen[LGMAXBURST:0] <= r_max_burst - 1; + end + + end endgenerate + // }}} + + // Calculate ARADDR for the next ARVALID + // {{{ + initial axi_araddr = 0; + always @(posedge i_clk) + begin + if (M_AXI_ARVALID && M_AXI_ARREADY) + begin + if (r_increment) + // Verilator lint_off WIDTH + axi_araddr[C_AXI_ADDR_WIDTH-1:ADDRLSB] + <= axi_araddr[C_AXI_ADDR_WIDTH-1:ADDRLSB] + + (M_AXI_ARLEN + 1); + // Verilator lint_on WIDTH + + axi_araddr[ADDRLSB-1:0] <= 0; + end + + if (!r_busy) + begin + axi_araddr <= cmd_addr; + end + + if (!OPT_UNALIGNED) + axi_araddr[ADDRLSB-1:0] <= 0; + end + // }}} + + // ARVALID + // {{{ + initial axi_arvalid = 0; + always @(posedge i_clk) + if (i_reset) + axi_arvalid <= 0; + else if (!M_AXI_ARVALID || M_AXI_ARREADY) + axi_arvalid <= start_burst; + // }}} + + // Set the constant M_AXI_* signals + // {{{ + assign M_AXI_ARVALID= axi_arvalid; + assign M_AXI_ARID = AXI_ID; + assign M_AXI_ARADDR = axi_araddr; + assign M_AXI_ARLEN = axi_arlen; + // Verilator lint_off WIDTH + assign M_AXI_ARSIZE = $clog2(C_AXI_DATA_WIDTH)-3; + // Verilator lint_on WIDTH + assign M_AXI_ARBURST= { 1'b0, r_increment }; + assign M_AXI_ARLOCK = 0; + assign M_AXI_ARCACHE= 4'b0011; + assign M_AXI_ARPROT = 0; + assign M_AXI_ARQOS = 0; + + assign M_AXI_RREADY = 1; + // }}} + // }}} + //////////////////////////////////////////////////////////////////////// + // + // (Optional) clock gating + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + generate if (OPT_CLKGATE) + begin : CLK_GATING + // {{{ + reg gatep, r_clk_active; + reg gaten /* verilator clock_enable */; + + // clk_active + // {{{ + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + r_clk_active <= 1'b1; + else begin + r_clk_active <= 1'b0; + + if (r_busy) + r_clk_active <= 1'b1; + if (awskd_valid || wskd_valid || arskd_valid) + r_clk_active <= 1'b1; + if (S_AXIL_BVALID || S_AXIL_RVALID) + r_clk_active <= 1'b1; + + if (M_AXIS_TVALID) + r_clk_active <= 1'b1; + end + + assign clk_active = r_clk_active; + // }}} + // Gate the clock here locally + // {{{ + always @(posedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + gatep <= 1'b1; + else + gatep <= clk_active; + + always @(negedge S_AXI_ACLK) + if (!S_AXI_ARESETN) + gaten <= 1'b1; + else + gaten <= gatep; + + assign gated_clk = S_AXI_ACLK && gaten; + + assign clk_active = r_clk_active; + // }}} + // }}} + end else begin : NO_CLK_GATING + // {{{ + // Always active + assign clk_active = 1'b1; + assign gated_clk = S_AXI_ACLK; + // }}} + end endgenerate + // }}} + + // Keep Verilator happy + // {{{ + // Verilator coverage_off + // Verilator lint_off UNUSED + wire unused; + assign unused = &{ 1'b0, S_AXIL_AWPROT, S_AXIL_ARPROT, M_AXI_RID, + M_AXI_RRESP[0], fifo_full, wskd_strb[2:0], fifo_fill, + ar_none_outstanding, S_AXIL_AWADDR[AXILLSB-1:0], + S_AXIL_ARADDR[AXILLSB-1:0], + new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH], + new_widelen + }; + // Verilator coverage_on + // Verilator lint_on UNUSED + // }}} +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +// +// Formal properties +// {{{ +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +//////////////////////////////////////////////////////////////////////////////// +`ifdef FORMAL + // + // The formal properties for this unit are maintained elsewhere. + // This core does, however, pass a full prove (w/ induction) for all + // bus properties. + // + // ... + // + + + initial f_past_valid = 0; + always @(posedge i_clk) + f_past_valid <= 1; + //////////////////////////////////////////////////////////////////////// + // + // Properties of the AXI-stream data interface + // {{{ + // + //////////////////////////////////////////////////////////////////////// + // + // + + // (These are captured by the FIFO within) + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // The AXI-lite control interface + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + faxil_slave #( + // {{{ + .C_AXI_DATA_WIDTH(C_AXIL_DATA_WIDTH), + .C_AXI_ADDR_WIDTH(C_AXIL_ADDR_WIDTH), + // + // ... + // }}} + ) faxil( + // {{{ + .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), + // + .i_axi_awvalid(S_AXIL_AWVALID), + .i_axi_awready(S_AXIL_AWREADY), + .i_axi_awaddr( S_AXIL_AWADDR), + .i_axi_awprot( S_AXIL_AWPROT), + // + .i_axi_wvalid(S_AXIL_WVALID), + .i_axi_wready(S_AXIL_WREADY), + .i_axi_wdata( S_AXIL_WDATA), + .i_axi_wstrb( S_AXIL_WSTRB), + // + .i_axi_bvalid(S_AXIL_BVALID), + .i_axi_bready(S_AXIL_BREADY), + .i_axi_bresp( S_AXIL_BRESP), + // + .i_axi_arvalid(S_AXIL_ARVALID), + .i_axi_arready(S_AXIL_ARREADY), + .i_axi_araddr( S_AXIL_ARADDR), + .i_axi_arprot( S_AXIL_ARPROT), + // + .i_axi_rvalid(S_AXIL_RVALID), + .i_axi_rready(S_AXIL_RREADY), + .i_axi_rdata( S_AXIL_RDATA), + .i_axi_rresp( S_AXIL_RRESP), + // + // ... + // }}} + ); + + // + // ... + // + + always @(posedge i_clk) + if (f_past_valid && $past(S_AXI_ARESETN)) + begin + if ($past(r_busy)||$past(w_cmd_start)) + begin + assert($stable(cmd_length_b)); + assert($stable(cmd_length_w)); + assert($stable(cmd_length_aligned_w)); + end + if ($past(r_busy)) + begin + assert($stable(r_increment)); + assert($stable(r_continuous)); + end + if ($past(r_busy) && $past(r_busy,2)) + assert($stable(fv_start_addr)); + end + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // The AXI master memory interface + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // + // ... + // + + faxi_master #( + // {{{ + .C_AXI_ID_WIDTH(C_AXI_ID_WIDTH), + .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), + .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), + // + .OPT_EXCLUSIVE(1'b0), + .OPT_NARROW_BURST(1'b0), + // + // ... + // }}} + ) faxi( + // {{{ + .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), + // + .i_axi_awvalid(1'b0), + .i_axi_awready(1'b0), + .i_axi_awid( AXI_ID), + .i_axi_awaddr( 0), + .i_axi_awlen( 0), + .i_axi_awsize( 0), + .i_axi_awburst(0), + .i_axi_awlock( 0), + .i_axi_awcache(0), + .i_axi_awprot( 0), + .i_axi_awqos( 0), + // + .i_axi_wvalid(0), + .i_axi_wready(0), + .i_axi_wdata( 0), + .i_axi_wstrb( 0), + .i_axi_wlast( 0), + // + .i_axi_bvalid(1'b0), + .i_axi_bready(1'b0), + .i_axi_bid( AXI_ID), + .i_axi_bresp( 2'b00), + // + .i_axi_arvalid(M_AXI_ARVALID), + .i_axi_arready(M_AXI_ARREADY), + .i_axi_arid( M_AXI_ARID), + .i_axi_araddr( M_AXI_ARADDR), + .i_axi_arlen( M_AXI_ARLEN), + .i_axi_arsize( M_AXI_ARSIZE), + .i_axi_arburst(M_AXI_ARBURST), + .i_axi_arlock( M_AXI_ARLOCK), + .i_axi_arcache(M_AXI_ARCACHE), + .i_axi_arprot( M_AXI_ARPROT), + .i_axi_arqos( M_AXI_ARQOS), + // + .i_axi_rvalid(M_AXI_RVALID), + .i_axi_rready(M_AXI_RREADY), + .i_axi_rdata( M_AXI_RDATA), + .i_axi_rlast( M_AXI_RLAST), + .i_axi_rresp( M_AXI_RRESP), + // + // ... + // + // }}} + ); + + + // + // ... + // + + always @(*) + if (r_busy) + begin + // + // ... + // + end else begin + // + // ... + // + + assert(rd_uncommitted + + ((OPT_UNALIGNED && write_to_fifo) ? 1:0) + + fifo_fill == (1<= fv_start_addr); + end else begin + // Reverse order + // Either: last < start <= f_raddr + // or: f_raddr < last < start + assert((fv_axi_raddr >= fv_start_addr) + ||(fv_axi_raddr <= f_last_addr)); + end + + if (fv_start_addr <= fv_axi_raddr) + begin + // Natural order: start < rad < f_rad < last + // or even: last < start < rad < f_rad + assert(axi_raddr <= fv_axi_raddr); + assert(fv_start_addr <= axi_raddr); + end else if (fv_axi_raddr <= f_last_addr) + begin + // Reverse order: f_raddr < last < start + // so either: last < start < raddr + // or: raddr < f_raddr < last < start + // + assert((axi_raddr >= fv_start_addr) + || (axi_raddr <= fv_axi_raddr)); + end + end + end + + always @(*) + if (!r_busy) + begin + assert(!M_AXI_ARVALID); + assert(!M_AXI_RVALID); + // + // ... + // + end + + always @(*) + assert(zero_length == (cmd_length_w == 0)); + + always @(*) + if (phantom_start) + assert(rd_uncommitted >= (M_AXI_ARLEN + 1)); + + always @(*) + if (zero_length) + assert(!r_busy); + always @(*) + if (r_busy) + assert(ar_none_remaining == (ar_requests_remaining == 0)); + always @(*) + assert(ar_none_outstanding == (ar_bursts_outstanding == 0)); + always @(*) + assert(rd_none_remaining == (rd_reads_remaining == 0)); + always @(*) + assert(rd_last_remaining == (rd_reads_remaining == 1)); + + always @(*) + if (r_complete) + assert(!r_busy); + + // + // ... + // + + // + // fifo_availability is a measure of (1< 0) || (ar_requests_remaining == 0)); + + + always @(*) + if (phantom_start) + assert(M_AXI_ARVALID); + + always @(posedge i_clk) + if (phantom_start) + begin + assert(r_max_burst > 0); + assert(M_AXI_ARLEN == $past(r_max_burst)-1); + end + + + + // + // Address checking + // + + // Check cmd_addr + always @(*) + if (r_busy) + begin + if (r_increment && r_continuous) + begin + assert(cmd_addr == axi_raddr); + end else + assert(cmd_addr == fv_start_addr); + end + + // Check M_AXI_ARADDR + // + // ... + // + + // + // Check M_AXI_ARLEN + // + // ... + // + + // + // Constrain the r_maxburst + // + // ... + // + + always @(*) + if (r_busy) + begin + assert(r_max_burst <= (1< 0) + cvr_aborted <= 1; + if (M_AXI_RVALID && M_AXI_RRESP[1] && M_AXI_RLAST) + cvr_buserr <= 1; + end + + initial cvr_continued = 0; + always @(posedge i_clk) + if (i_reset || r_err || cmd_abort) + cvr_continued <= 0; + else begin + // Cover a continued transaction across two separate bursts + if (r_busy && r_continuous) + cvr_continued[0] <= 1; + if (!r_busy && cvr_continued[0]) + cvr_continued[1] <= 1; + if (r_busy && cvr_continued[1]) + cvr_continued[2] <= 1; + end + + always @(posedge i_clk) + if (f_past_valid && !$past(i_reset) && !i_reset && $fell(r_busy)) + begin + cover( r_err && cvr_aborted); + cover( r_err && cvr_buserr); + cover(!r_err); + if (!r_err && !axi_abort_pending && !cvr_aborted && !cvr_buserr) + begin + cover(cmd_length_w > 5); + cover(cmd_length_w > 8); + // + // ... + // + cover(&cvr_continued); + cover(&cvr_continued && (cmd_length_w > 2)); + cover(&cvr_continued && (cmd_length_w > 5)); + end + end + + always @(*) + if (!i_reset) + cover(!r_err && fifo_fill > 8 && !r_busy); + + always @(*) + cover(r_busy); + + always @(*) + cover(start_burst); + + always @(*) + cover(M_AXI_ARVALID && M_AXI_ARREADY); + + always @(*) + cover(M_AXI_RVALID); + + always @(*) + cover(M_AXI_RVALID & M_AXI_RLAST); + always @(*) + if (r_busy) + begin + cover(!ar_none_remaining); + if(!ar_none_remaining) + begin + cover(1); + cover(rd_uncommitted>= {{(LGFIFO-LGMAXBURST){1'b0}}, r_max_burst}); + if(rd_uncommitted>= {{(LGFIFO-LGMAXBURST){1'b0}}, r_max_burst}) + begin + cover(!phantom_start); + cover(phantom_start); + end + end + end + + // + // Unaligned cover properties + generate if (OPT_TLAST) + begin + reg [3:0] cvr_lastcount; + always @(posedge i_clk) + if (i_reset || (r_busy && cmd_length_w <= 2)) + cvr_lastcount <= 0; + else if (M_AXIS_TVALID && M_AXIS_TREADY && M_AXIS_TLAST + && !cvr_lastcount[3]) + cvr_lastcount <= cvr_lastcount + 1; + + always @(*) + cover(M_AXIS_TVALID && M_AXIS_TREADY && M_AXIS_TLAST); + + always @(posedge i_clk) + cover(o_int && cvr_lastcount > 2); + + end endgenerate + + generate if (OPT_UNALIGNED) + begin + // + // ... + // + always @(posedge i_clk) + if (f_past_valid && !$past(i_reset) && !i_reset &&$fell(r_busy)) + begin + cover(r_err); + cover(!r_err); + cover(axi_abort_pending); + cover(!axi_abort_pending); + cover(cvr_aborted); + cover(!cvr_aborted); + cover(cvr_buserr); + cover(!cvr_buserr); + cover(!cvr_buserr && !axi_abort_pending); + cover(!cvr_buserr && !axi_abort_pending + && (cmd_length_w > 2)); + cover(!r_err && !cvr_aborted && !cvr_buserr + && !axi_abort_pending + && (cmd_length_w > 2)); + end + end endgenerate + + + // }}} +`endif +// }}} +endmodule -- cgit v1.2.3