//////////////////////////////////////////////////////////////////////////////// // // 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