diff options
Diffstat (limited to 'rtl/wb2axip/aximm2s.v')
| -rw-r--r-- | rtl/wb2axip/aximm2s.v | 2158 |
1 files changed, 2158 insertions, 0 deletions
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<<TMP_LGMAXBURST)) + ? TMP_LGMAXBURST : $clog2(4096 * 8 / C_AXI_DATA_WIDTH); + localparam LGMAX_FIXED_BURST = (LGMAXBURST < 4) ? LGMAXBURST : 4, + MAX_FIXED_BURST = (1<<LGMAX_FIXED_BURST); + localparam LGLENW = LGLEN - ($clog2(C_AXI_DATA_WIDTH)-3), + LGLENWA = LGLENW + (OPT_UNALIGNED ? 1:0); + // localparam LGFIFOB = LGFIFO + ($clog2(C_AXI_DATA_WIDTH)-3); + // localparam [ADDRLSB-1:0] LSBZEROS = 0; + // }}} + + // Signal declarations + // {{{ + wire clk_active, gated_clk; + wire i_clk = gated_clk; + wire i_reset = !S_AXI_ARESETN; + + reg r_busy, r_err, r_complete, r_continuous, r_increment, + cmd_abort, zero_length, + w_cmd_start, w_complete, w_cmd_abort, r_pre_start; + // reg cmd_start; + reg axi_abort_pending; + + reg [LGLENWA-1:0] ar_requests_remaining, + ar_bursts_outstanding, + ar_next_remaining; + reg [LGMAXBURST:0] r_max_burst; + reg [C_AXI_ADDR_WIDTH-1:0] axi_raddr; + + reg [C_AXI_ADDR_WIDTH-1:0] cmd_addr; + reg [LGLENW-1:0] cmd_length_w; + reg [LGLENWA-1:0] cmd_length_aligned_w; + reg unaligned_cmd_addr; + + // FIFO signals + wire reset_fifo, write_to_fifo, + read_from_fifo; + wire [C_AXI_DATA_WIDTH-1:0] write_data; + wire [LGFIFO:0] fifo_fill; + wire fifo_full, fifo_empty; + + wire awskd_valid, axil_write_ready; + wire [C_AXIL_ADDR_WIDTH-AXILLSB-1:0] awskd_addr; + // + wire wskd_valid; + wire [C_AXIL_DATA_WIDTH-1:0] wskd_data; + wire [C_AXIL_DATA_WIDTH/8-1:0] wskd_strb; + reg axil_bvalid; + // + wire arskd_valid, axil_read_ready; + wire [C_AXIL_ADDR_WIDTH-AXILLSB-1:0] arskd_addr; + reg [C_AXIL_DATA_WIDTH-1:0] axil_read_data; + reg axil_read_valid; + reg [C_AXIL_DATA_WIDTH-1:0] w_status_word; + reg [2*C_AXIL_DATA_WIDTH-1:0] wide_address, wide_length, + new_wideaddr, new_widelen; + wire [C_AXIL_DATA_WIDTH-1:0] new_cmdaddrlo, new_cmdaddrhi, + new_lengthlo, new_lengthhi; + + + + reg axi_arvalid; + reg [C_AXI_ADDR_WIDTH-1:0] axi_araddr; + reg [7:0] axi_arlen; + + // Speed up checking for zeros + reg ar_none_remaining, + ar_none_outstanding, + phantom_start, start_burst; + reg ar_multiple_full_bursts, + ar_multiple_fixed_bursts, + ar_multiple_bursts_remaining, + ar_needs_alignment; + wire partial_burst_requested; + reg [LGMAXBURST-1:0] addralign; + reg [LGFIFO:0] rd_uncommitted; + reg [LGMAXBURST:0] initial_burstlen; + reg [LGLENWA-1:0] rd_reads_remaining; + reg rd_none_remaining, + rd_last_remaining; + + wire realign_last_valid; +/* + wr_none_pending, r_none_remaining; + + reg w_phantom_start, phantom_start; + reg [LGFIFO:0] next_fill; +*/ + + // }}} + + //////////////////////////////////////////////////////////////////////// + // + // AXI-lite signaling + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // This is mostly the skidbuffer logic, and handling of the VALID + // and READY signals for the AXI-lite control logic in the next + // section. + // + + // + // Write signaling + // + // {{{ + + skidbuffer #( + // {{{ + .OPT_OUTREG(0), + .OPT_LOWPOWER(OPT_LOWPOWER), + .DW(C_AXIL_ADDR_WIDTH-AXILLSB) + // }}} + ) axilawskid( + // {{{ + .i_clk(S_AXI_ACLK), .i_reset(i_reset), + .i_valid(S_AXIL_AWVALID), .o_ready(S_AXIL_AWREADY), + .i_data(S_AXIL_AWADDR[C_AXIL_ADDR_WIDTH-1:AXILLSB]), + .o_valid(awskd_valid), .i_ready(axil_write_ready), + .o_data(awskd_addr) + // }}} + ); + + skidbuffer #( + // {{{ + .OPT_OUTREG(0), + .OPT_LOWPOWER(OPT_LOWPOWER), + .DW(C_AXIL_DATA_WIDTH+C_AXIL_DATA_WIDTH/8) + // }}} + ) axilwskid( + // {{{ + .i_clk(S_AXI_ACLK), .i_reset(i_reset), + .i_valid(S_AXIL_WVALID), .o_ready(S_AXIL_WREADY), + .i_data({ S_AXIL_WDATA, S_AXIL_WSTRB }), + .o_valid(wskd_valid), .i_ready(axil_write_ready), + .o_data({ wskd_data, wskd_strb }) + // }}} + ); + + assign axil_write_ready = clk_active && awskd_valid && wskd_valid + && (!S_AXIL_BVALID || S_AXIL_BREADY); + + initial axil_bvalid = 0; + always @(posedge i_clk) + if (i_reset) + axil_bvalid <= 0; + else if (axil_write_ready) + axil_bvalid <= 1; + else if (S_AXIL_BREADY) + axil_bvalid <= 0; + + assign S_AXIL_BVALID = axil_bvalid; + assign S_AXIL_BRESP = 2'b00; + // }}} + + // + // Read signaling + // + // {{{ + + skidbuffer #( + // {{{ + .OPT_OUTREG(0), + .OPT_LOWPOWER(OPT_LOWPOWER), + .DW(C_AXIL_ADDR_WIDTH-AXILLSB) + // }}} + ) axilarskid( + // {{{ + .i_clk(S_AXI_ACLK), .i_reset(i_reset), + .i_valid(S_AXIL_ARVALID), .o_ready(S_AXIL_ARREADY), + .i_data(S_AXIL_ARADDR[C_AXIL_ADDR_WIDTH-1:AXILLSB]), + .o_valid(arskd_valid), .i_ready(axil_read_ready), + .o_data(arskd_addr) + // }}} + ); + + assign axil_read_ready = clk_active && arskd_valid + && (!axil_read_valid || S_AXIL_RREADY); + + initial axil_read_valid = 1'b0; + always @(posedge i_clk) + if (i_reset) + axil_read_valid <= 1'b0; + else if (axil_read_ready) + axil_read_valid <= 1'b1; + else if (S_AXIL_RREADY) + axil_read_valid <= 1'b0; + + assign S_AXIL_RVALID = axil_read_valid; + assign S_AXIL_RDATA = axil_read_data; + assign S_AXIL_RRESP = 2'b00; + // }}} + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // AXI-lite controlled logic + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // w_cmd_abort, cmd_abort : Abort transaction + // {{{ + always @(*) + begin + w_cmd_abort = 0; + w_cmd_abort = (axil_write_ready && awskd_addr == CMD_CONTROL) + && (wskd_strb[3] && wskd_data[31:24] == ABORT_KEY); + if (!r_busy) + w_cmd_abort = 0; + end + + initial cmd_abort = 0; + always @(posedge i_clk) + if (i_reset) + cmd_abort <= 0; + else + cmd_abort <= (cmd_abort && r_busy)||w_cmd_abort; + // }}} + + // w_cmd_start: Start command + // {{{ + always @(*) + if (r_busy) + w_cmd_start = 0; + else begin + w_cmd_start = 0; + if ((axil_write_ready && awskd_addr == CMD_CONTROL) + && (wskd_strb[3] && wskd_data[CBIT_BUSY])) + w_cmd_start = 1; + if (r_err && !wskd_data[CBIT_ERR]) + w_cmd_start = 0; + if (zero_length) + w_cmd_start = 0; + if (OPT_UNALIGNED && unaligned_cmd_addr + && wskd_data[CBIT_INCREMENT]) + w_cmd_start = 0; + end + // }}} + + // r_busy, r_complete: Calculate busy or complete flags + // {{{ + initial r_busy = 0; + initial r_complete = 0; + always @(posedge i_clk) + if (i_reset) + begin + r_busy <= 0; + r_complete <= 0; + end else if (!r_busy) + begin + if (w_cmd_start) + r_busy <= 1'b1; + if (axil_write_ready && awskd_addr == CMD_CONTROL) + // Any write to the control register will clear the + // completion flag + r_complete <= 1'b0; + end else if (r_busy) + begin + if (w_complete) + begin + r_complete <= 1; + r_busy <= 1'b0; + end + end + // }}} + + // o_int: Interrupts + // {{{ + initial o_int = 0; + always @(posedge i_clk) + if (i_reset) + o_int <= 0; + else + o_int <= (r_busy && w_complete); + // }}} + + // r_err : Error conditions + // {{{ + always @(posedge i_clk) + if (i_reset) + r_err <= 0; + else if (!r_busy) + begin + if (axil_write_ready && awskd_addr == CMD_CONTROL) + begin + if (!w_cmd_abort) + r_err <= r_err && (!wskd_strb[3] || !wskd_data[CBIT_ERR]); + // On any request to start a transfer with an unaligned + // address, that's not incrementing--declare an + // immediate error + if (wskd_strb[3] && wskd_data[CBIT_BUSY] + && wskd_data[CBIT_INCREMENT] + && (OPT_UNALIGNED && unaligned_cmd_addr)) + r_err <= 1'b1; + end + end else // if (r_busy) + begin + if (M_AXI_RVALID && M_AXI_RREADY && M_AXI_RRESP[1]) + r_err <= 1'b1; + end + // }}} + + // r_continuous + // {{{ + initial r_continuous = 0; + always @(posedge i_clk) + if (i_reset) + r_continuous <= 0; + else begin + if (!r_busy && axil_write_ready && awskd_addr == CMD_CONTROL + && !w_cmd_abort) + r_continuous <= wskd_strb[3] && wskd_data[CBIT_CONTINUOUS]; + end + // }}} + + // wide_address, wide_length + // {{{ + always @(*) + begin + wide_address = 0; + wide_address[C_AXI_ADDR_WIDTH-1:0] = cmd_addr; + if (!OPT_UNALIGNED) + wide_address[ADDRLSB-1:0] = 0; + + wide_length = 0; + wide_length[ADDRLSB +: LGLENW] = cmd_length_w; + end + // }}} + + // new_cmdaddr* + // {{{ + assign new_cmdaddrlo = apply_wstrb( + wide_address[C_AXIL_DATA_WIDTH-1:0], + wskd_data, wskd_strb); + + assign new_cmdaddrhi = apply_wstrb( + wide_address[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH], + wskd_data, wskd_strb); + // }}} + + // new_length* + // {{{ + assign new_lengthlo = apply_wstrb( + wide_length[C_AXIL_DATA_WIDTH-1:0], + wskd_data, wskd_strb); + + assign new_lengthhi = apply_wstrb( + wide_length[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH], + wskd_data, wskd_strb); + // }}} + + always @(*) + begin + new_wideaddr = wide_address; + + if (awskd_addr == CMD_ADDRLO) + new_wideaddr[C_AXIL_DATA_WIDTH-1:0] = new_cmdaddrlo; + if (awskd_addr == CMD_ADDRHI) + new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH] = new_cmdaddrhi; + if (!OPT_UNALIGNED) + new_wideaddr[ADDRLSB-1:0] = 0; + new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH] = 0; + + + new_widelen = wide_length; + if (awskd_addr == CMD_LENLO) + new_widelen[C_AXIL_DATA_WIDTH-1:0] = new_lengthlo; + if (awskd_addr == CMD_LENHI) + new_widelen[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH] = new_lengthhi; + new_widelen[ADDRLSB-1:0] = 0; + new_widelen[2*C_AXIL_DATA_WIDTH-1:ADDRLSB+LGLENW] = 0; + end + + + initial r_increment = 1'b1; + initial cmd_addr = 0; + initial cmd_length_w = 0; // Counts in bytes + initial zero_length = 1; + initial cmd_length_aligned_w = 0; + initial unaligned_cmd_addr = 1'b0; + initial ar_multiple_full_bursts = 0; + initial ar_multiple_fixed_bursts = 0; + always @(posedge i_clk) + begin + if (axil_write_ready && !r_busy) + begin + case(awskd_addr) + CMD_CONTROL: + r_increment <= !wskd_data[CBIT_INCREMENT]; + CMD_ADDRLO: begin + cmd_addr <= new_wideaddr[C_AXI_ADDR_WIDTH-1:0]; + unaligned_cmd_addr <= |new_wideaddr[ADDRLSB-1:0]; + if (OPT_UNALIGNED) + cmd_length_aligned_w <= cmd_length_w + + (|new_wideaddr[ADDRLSB-1:0] ? 1:0); + // ERR: What if !r_increment? In that case, we can't + // support unaligned addressing + end + CMD_ADDRHI: if (C_AXI_ADDR_WIDTH > 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<<ADDRLSB) : 0); + + if (i_reset) + begin + r_increment <= 1'b1; + cmd_addr <= 0; + cmd_length_w <= 0; + zero_length <= 1; + unaligned_cmd_addr <= 0; + cmd_length_aligned_w <= 0; + ar_multiple_full_bursts <= 0; + ar_multiple_fixed_bursts <= 0; + end + + if (!OPT_UNALIGNED) + unaligned_cmd_addr <= 0; + end + + // w_status_word + // {{{ + always @(*) + begin + w_status_word = 0; + w_status_word[CBIT_BUSY] = r_busy; + w_status_word[CBIT_ERR] = r_err; + w_status_word[CBIT_COMPLETE] = r_complete; + w_status_word[CBIT_CONTINUOUS] = r_continuous; + w_status_word[CBIT_INCREMENT] = !r_increment; + w_status_word[20:16] = LGFIFO; + end + // }}} + + // axil_read_data + // {{{ + always @(posedge i_clk) + if (!axil_read_valid || S_AXIL_RREADY) + begin + axil_read_data <= 0; + case(arskd_addr) + CMD_CONTROL: axil_read_data <= w_status_word; + CMD_ADDRLO: axil_read_data <= wide_address[C_AXIL_DATA_WIDTH-1:0]; + CMD_ADDRHI: axil_read_data <= wide_address[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH]; + CMD_LENLO: axil_read_data <= wide_length[C_AXIL_DATA_WIDTH-1:0]; + CMD_LENHI: axil_read_data <= wide_length[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH]; + default axil_read_data <= 0; + endcase + + if (OPT_LOWPOWER && !axil_read_ready) + axil_read_data <= 0; + end + // }}} + + function [C_AXIL_DATA_WIDTH-1:0] apply_wstrb; + // {{{ + input [C_AXIL_DATA_WIDTH-1:0] prior_data; + input [C_AXIL_DATA_WIDTH-1:0] new_data; + input [C_AXIL_DATA_WIDTH/8-1:0] wstrb; + + integer k; + for(k=0; k<C_AXIL_DATA_WIDTH/8; k=k+1) + begin + apply_wstrb[k*8 +: 8] + = wstrb[k] ? new_data[k*8 +: 8] : prior_data[k*8 +: 8]; + end + endfunction + // }}} + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // The data FIFO section + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + assign reset_fifo = i_reset || (!r_busy && (!r_continuous || r_err)); + + // Realign the data (if OPT_UNALIGN) before sending it to the FIFO + // {{{ + // This allows us to handle unaligned addresses. + generate if (OPT_UNALIGNED) + begin : REALIGN_DATA + + reg r_write_to_fifo; + reg [C_AXI_DATA_WIDTH-1:0] last_data, + r_write_data; + reg [ADDRLSB-1:0] corollary_shift; + reg last_valid; + reg [ADDRLSB-1:0] realignment; + + always @(*) + realignment = cmd_addr[ADDRLSB-1:0]; + + initial last_data = 0; + always @(posedge i_clk) + if (reset_fifo || !unaligned_cmd_addr) + last_data <= 0; + else if (M_AXI_RVALID && M_AXI_RREADY) + last_data <= M_AXI_RDATA >> (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<<LGMAXBURST); + if (!r_increment) + begin + initial_burstlen = MAX_FIXED_BURST; + if (!ar_multiple_fixed_bursts + && !cmd_length_aligned_w[LGMAX_FIXED_BURST]) + begin + initial_burstlen = 0; + initial_burstlen[LGMAX_FIXED_BURST-1:0] + = cmd_length_aligned_w[ + LGMAX_FIXED_BURST-1:0]; + end + end else if (ar_needs_alignment) + initial_burstlen = { 1'b0, addralign }; + else if (!ar_multiple_full_bursts + && !cmd_length_aligned_w[LGMAXBURST]) + initial_burstlen = { 1'b0, cmd_length_aligned_w[ + LGMAXBURST-1:0] }; + end + + initial r_max_burst = 0; + always @(posedge i_clk) + if (!r_busy || r_pre_start) + begin + // Force us to align ourself early + // That way we don't need to check for + // alignment (again) later + r_max_burst <= initial_burstlen; + end else if (phantom_start) + begin + // Verilator lint_off WIDTH + if (r_increment || LGMAXBURST <= LGMAX_FIXED_BURST) + begin : LIMIT_BY_LGMAXBURST + r_max_burst <= (1<<LGMAXBURST); + + if (!ar_multiple_bursts_remaining + && ar_next_remaining[LGMAXBURST:0] < (1<<LGMAXBURST)) + r_max_burst <= { 1'b0, ar_next_remaining[8:0] }; + end else begin : LIMIT_BY_SIXTEEN + r_max_burst <= MAX_FIXED_BURST; + + if (!ar_multiple_bursts_remaining + && ar_next_remaining[LGMAXBURST:0] < MAX_FIXED_BURST) + r_max_burst <= { 1'b0, ar_next_remaining[LGMAXBURST:0] }; + end + // Verilator lint_on WIDTH + end + // }}} + + // Count the number of bursts outstanding--these are the number of + // ARVALIDs that have been accepted, but for which the RVALID && RLAST + // has not (yet) been returned. + // {{{ + initial ar_none_outstanding = 1; + initial ar_bursts_outstanding = 0; + always @(posedge i_clk) + if (i_reset) + begin + ar_bursts_outstanding <= 0; + ar_none_outstanding <= 1; + end else case ({ phantom_start, + M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST }) + 2'b01: begin + ar_bursts_outstanding <= ar_bursts_outstanding - 1; + ar_none_outstanding <= (ar_bursts_outstanding == 1); + end + 2'b10: begin + ar_bursts_outstanding <= ar_bursts_outstanding + 1; + ar_none_outstanding <= 0; + end + default: begin end + endcase + // }}} + + // Are we there yet? + // {{{ + initial rd_reads_remaining = 0; + initial rd_none_remaining = 1; + initial rd_last_remaining = 0; + always @(posedge i_clk) + if (!r_busy) + begin + rd_reads_remaining <= cmd_length_aligned_w; + rd_last_remaining <= (cmd_length_aligned_w == 1); + rd_none_remaining <= (cmd_length_aligned_w == 0); + end else if (M_AXI_RVALID && M_AXI_RREADY) + begin + rd_reads_remaining <= rd_reads_remaining - 1; + rd_last_remaining <= (rd_reads_remaining == 2); + rd_none_remaining <= (rd_reads_remaining == 1); + end + + always @(*) + if (!r_busy) + w_complete = 0; + else if (axi_abort_pending && ar_none_outstanding && !M_AXI_ARVALID) + w_complete = 1; + else if (r_continuous) + w_complete = (rd_none_remaining)||((rd_last_remaining) && M_AXI_RVALID && M_AXI_RREADY); + else // if !r_continuous + w_complete = (rd_none_remaining && fifo_empty); + + // }}} + + // Are we stopping early? Aborting something ongoing? + // {{{ + initial axi_abort_pending = 0; + always @(posedge i_clk) + if (i_reset || !r_busy) + axi_abort_pending <= 0; + else begin + if (M_AXI_RVALID && M_AXI_RREADY && M_AXI_RRESP[1]) + axi_abort_pending <= 1; + if (cmd_abort) + axi_abort_pending <= 1; + end + // }}} + + // Count the number of uncommited spaces in the FIFO + // {{{ + generate if (OPT_UNALIGNED) + begin : GEN_UNALIGNED_BREQ_COUNT + reg r_partial_burst_requested; + + initial r_partial_burst_requested = 1'b1; + always @(posedge i_clk) + if (!r_busy) + r_partial_burst_requested <= !unaligned_cmd_addr; + else if (phantom_start) + r_partial_burst_requested <= 1'b1; + + assign partial_burst_requested = r_partial_burst_requested; + end else begin : NO_UNALIGNED_BREQ_COUNT + + assign partial_burst_requested = 1'b1; + end endgenerate + + initial rd_uncommitted = (1<<LGFIFO); + always @(posedge i_clk) + if (reset_fifo) + begin + rd_uncommitted <= (1<<LGFIFO); + end else case ({ phantom_start, + M_AXIS_TVALID && M_AXIS_TREADY }) + 2'b00: begin end + 2'b01: begin + rd_uncommitted <= rd_uncommitted + 1; + end + 2'b10: begin + // Verilator lint_off WIDTH + rd_uncommitted <= rd_uncommitted - (M_AXI_ARLEN + 1) + + (partial_burst_requested ? 0 :1); + end + 2'b11: begin + rd_uncommitted <= rd_uncommitted - (M_AXI_ARLEN) + + (partial_burst_requested ? 0 :1); + // Verilator lint_on WIDTH + end + endcase + // }}} + + // So that we can monitor where we are at, and perhaps restart it + // later, keep track of the current address used by the R-channel + // {{{ + + initial axi_raddr = 0; + always @(posedge i_clk) + begin + if (!r_busy) + axi_raddr <= cmd_addr; + else if (axi_abort_pending || !r_increment) + // Stop incrementing tthe address following an abort + axi_raddr <= axi_raddr; + else begin + if (M_AXI_RVALID && M_AXI_RREADY && !M_AXI_RRESP[1] + && (!unaligned_cmd_addr || realign_last_valid)) + axi_raddr <= axi_raddr + (1<<ADDRLSB); + end + + if (!OPT_UNALIGNED) + axi_raddr[ADDRLSB-1:0] <= 0; + end + + // }}} + + // + // }}} + + // start_burst, phantom_start + // {{{ + always @(*) + begin + start_burst = !ar_none_remaining; + if ((rd_uncommitted[LGFIFO:LGMAXBURST] == 0) + && ({ 1'b0, rd_uncommitted[LGMAXBURST-1:0] } + < r_max_burst)) + start_burst = 0; + if (phantom_start || r_pre_start) + // Insist on a minimum of one clock between burst + // starts, so we can get our lengths right + start_burst = 0; + if (M_AXI_ARVALID && !M_AXI_ARREADY) + start_burst = 0; + if (!r_busy || cmd_abort || axi_abort_pending) + start_burst = 0; + end + + initial phantom_start = 0; + always @(posedge i_clk) + if (i_reset) + phantom_start <= 0; + else + phantom_start <= start_burst; + // }}} + + + // Calculate ARLEN and ARADDR for the next ARVALID + // {{{ + generate if (LGMAXBURST >= 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<<LGFIFO)); + if (!r_continuous) + assert(fifo_fill == 0 || reset_fifo); + end + + // + // ... + // + + always @(*) + if (r_busy) + begin + if (!OPT_UNALIGNED) + begin + assert(M_AXI_ARADDR[ADDRLSB-1:0] == 0); + end else + assert((M_AXI_ARADDR[ADDRLSB-1:0] == 0) + ||(M_AXI_ARADDR == fv_start_addr)); + end + + always @(*) + if (!OPT_UNALIGNED || (r_busy && !r_increment)) + begin + assert(cmd_addr[ADDRLSB-1:0] == 0); + assert(fv_start_addr[ADDRLSB-1:0] == 0); + assert(axi_araddr[ADDRLSB-1:0] == 0); + assert(axi_raddr[ADDRLSB-1:0] == 0); + end + + // + // f_last_addr is the (aligned) address one following the last valid + // address read. Once all reading is done, all (aligned) address + // pointers should point there. + always @(*) + begin + f_last_addr = { fv_start_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB], + {(ADDRLSB){1'b0}} }; + + if (r_increment) + f_last_addr = f_last_addr + cmd_length_b; + if (unaligned_cmd_addr) // Only true if r_increment as well + f_last_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB] + = f_last_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB]+1; + + f_last_addr[ADDRLSB-1:0] = 0; + + f_next_start = fv_start_addr; + if (r_increment) + f_next_start = f_next_start + cmd_length_b; + if (!OPT_UNALIGNED) + assert(f_next_start == f_last_addr); + end + + + // + // ... + // + + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Other formal properties + // {{{ + //////////////////////////////////////////////////////////////////////// + // + // + + // + // Define some helper metrics + // + initial fv_start_addr = 0; + always @(posedge i_clk) + if (!r_busy) + fv_start_addr <= cmd_addr; + + always @(*) + begin + // Metrics defining M_AXI_ARADDR + f_araddr_is_aligned = (M_AXI_ARADDR[ADDRLSB+LGMAXBURST-1:0]==0); + f_araddr_is_initial = (M_AXI_ARADDR == fv_start_addr); + f_araddr_is_final = (M_AXI_ARADDR == f_last_addr); + + // + // Metrics to check ARADDR, assuming it had been accepted + // + + // + // ... + // + end + + // + // fv_ar_requests_remaining ... shadows ar_requests_remaining + // + // Since ar_requests_remaining drops to zero suddenly on any + // axi_abort_pending, we need another counter that we can use + // which doesn't have this feature, but which can also be used + // to check assertions and intermediate logic against until the + // abort takes effect. + initial fv_ar_requests_remaining = 0; + always @(posedge i_clk) + if (!r_busy) + begin + fv_ar_requests_remaining <= cmd_length_aligned_w; + end else if (phantom_start) + begin + // Verilator lint_off WIDTH + fv_ar_requests_remaining + <= fv_ar_requests_remaining - (M_AXI_ARLEN + 1); + // Verilator lint_on WIDTH + end + + always @(*) + if (r_busy) + begin + if (!axi_abort_pending) + begin + assert(fv_ar_requests_remaining == ar_requests_remaining); + end else + assert((ar_requests_remaining == 0) + ||(fv_ar_requests_remaining + == ar_requests_remaining)); + end + + always @(*) + if(r_busy) + begin + assert(fv_ar_requests_remaining <= cmd_length_aligned_w); + // + // ... + // + end + + // + // fv_axi_raddr ... shadows axi_raddr + // + // The low order bits will match the low order bits of the initial + // cmd_addr + // + initial fv_axi_raddr = 0; + always @(posedge i_clk) + if (!r_busy) + fv_axi_raddr <= cmd_addr; + else if (!r_increment) + fv_axi_raddr <= fv_start_addr; + else begin + if (M_AXI_RVALID && M_AXI_RREADY + && (!unaligned_cmd_addr || realign_last_valid)) + fv_axi_raddr <= fv_axi_raddr + (1<<ADDRLSB); + if (!OPT_UNALIGNED) + fv_axi_raddr[ADDRLSB-1:0] <= 0; + end + + // Constrain start <= axi_raddr <= fv_axi_raddr <= f_last_addr + // in spite of any address wrapping + always @(*) + if (r_busy) + begin + assert(axi_raddr[ADDRLSB-1:0] == cmd_addr[ADDRLSB-1:0]); + assert(axi_abort_pending || fv_axi_raddr == axi_raddr); + if (!r_increment) + begin + assert(fv_axi_raddr == fv_start_addr); + assert(axi_raddr == fv_start_addr); + end if (!axi_abort_pending) + begin + if (fv_start_addr <= f_last_addr) + begin + // Natural order: start < f_raddr < last + assert(fv_axi_raddr <= f_last_addr); + assert(fv_axi_raddr >= 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<<LGFIFO) minus the current + // fifo fill. This does not include what's in the pre-FIFO + // logic when OPT_UNALIGNED is true. + always @(*) + f_fifo_availability = rd_uncommitted; + + always @(*) + assert(f_fifo_committed <= (1<<LGFIFO)); + + always @(*) + assert(f_fifo_availability <= (1<<LGFIFO)); + + // + // ... + // + + always @(*) + if (!reset_fifo) + assert(f_fifo_committed + f_fifo_availability + fifo_fill + == (1<<LGFIFO)); + + // + // ... + // + + always @(*) + if (r_busy) + assert(r_max_burst <= (1<<LGMAXBURST)); + + always @(*) + if (r_busy && !r_pre_start) + assert((r_max_burst > 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<<LGMAXBURST)); + // + // ... + // + end + + // + // Constrain the length + // + // ... + // + + // Constrain rd_reads_remaining + // + // ... + // + always @(*) + if (r_busy) + begin + assert(rd_reads_remaining <= cmd_length_w); + // + // ... + // + assert(ar_bursts_outstanding <= rd_reads_remaining); + // + // ... + // + end + + // + // Constrain the number of requests remaining + // + // ... + // + + // + // Make sure our aw_bursts_outstanding counter never overflows + // (Given that the counter is as long as the length register, it cannot) + // + always @(*) + begin + if (&ar_bursts_outstanding[LGLENWA-1:1]) + assert(!M_AXI_ARVALID); + // + // ... + // + end + + // }}} + + // + // Some (fairly) random/unsorted properties + // {{{ + + always @(*) + begin + assert(ar_multiple_full_bursts + == |cmd_length_w[LGLENW-1:LGMAXBURST]); + assert(ar_multiple_fixed_bursts + == |cmd_length_w[LGLENW-1:LGMAX_FIXED_BURST]); + end + // + // Match axi_raddr to the faxi_ values + // + // ... + // + + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Contract checks + // + //////////////////////////////////////////////////////////////////////// + // + // {{{ + + // 1. All data values must get read and placed into the FIFO, with + // none skipped + // Captured in logic above(?) + // + // 2. No addresses skipped. Check the write address against the + // write address we are expecting + // + // ... + // + + // 3. If we aren't incrementing addresses, then our current address + // should always be the axi address + // + // ... + + // + // 4. Whenever we go from busy to idle, we should raise o_int for one + // (and only one) cycle + always @(posedge i_clk) + if (!f_past_valid || $past(!S_AXI_ARESETN)) + begin + assert(!o_int); + end else + assert(o_int == $fell(r_busy)); + + // + // ... + // + + + // 5. Pick an incoming data value. Choose whether or not to restrict + // incoming data not to be that value. If the incoming data is so + // restricted then assert that the stream output will never contain that + // value. + (* anyconst *) reg f_restrict_data; + (* anyconst *) reg [C_AXI_DATA_WIDTH-1:0] f_restricted; + + always @(*) + if (f_restrict_data && M_AXI_RVALID + && (!OPT_UNALIGNED || !unaligned_cmd_addr)) + assume(M_AXI_RDATA != f_restricted); + + always @(*) + if (f_restrict_data && M_AXIS_TVALID + && (!OPT_UNALIGNED || !unaligned_cmd_addr)) + assert(M_AXIS_TDATA != f_restricted); + + // + // ... + // + // }}} + //////////////////////////////////////////////////////////////////////// + // + // Cover checks + // + //////////////////////////////////////////////////////////////////////// + // + // {{{ + reg cvr_aborted, cvr_buserr; + reg [2:0] cvr_continued; + + initial { cvr_aborted, cvr_buserr } = 0; + always @(posedge i_clk) + if (i_reset || !r_busy) + { cvr_aborted, cvr_buserr } <= 0; + else if (r_busy && !axi_abort_pending) + begin + if (cmd_abort && ar_requests_remaining > 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 |