//////////////////////////////////////////////////////////////////////////////// // // Filename: axidma.v // {{{ // Project: WB2AXIPSP: bus bridges and other odds and ends // // Purpose: To move memory from one location to another, at high speed. // This is not a memory to stream, nor a stream to memory core, // but rather a memory to memory core. // // // Registers: // // 0. Control // 8b KEY // 3'b PROT // 4'b QOS // 1b Abort: Either aborting or aborted // 1b Err: Ended on an error // 1b Busy // 1b Interrupt Enable // 1b Interrupt Clear // 1b Start // 1. Unused // 2-3. Source address, low and then high 64-bit words // (Last value read address) // 4-5. Destination address, low and then high 64-bit words // (Next value to write address) // 6-7. Length, low and then high words // (Total number minus successful writes) // // Performance goals: // 100% throughput // Stay off the bus until you can drive it hard // Other goals: // Be both AXI3 and AXI4 capable // // Creator: Dan Gisselquist, Ph.D. // Gisselquist Technology, LLC // //////////////////////////////////////////////////////////////////////////////// // }}} // Copyright (C) 2020-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 // `define AXI3 // }}} module axidma #( // {{{ parameter C_AXI_ID_WIDTH = 1, parameter C_AXI_ADDR_WIDTH = 32, parameter C_AXI_DATA_WIDTH = 32, // // These two "parameters" really aren't things that can be // changed externally. They control the size of the AXI4-lite // port. Internally, it's defined to have 8, 32-bit registers. // The registers are configured wide enough to support 64-bit // AXI addressing. Similarly, the AXI-lite data width is fixed // at 32-bits. /*local*/parameter C_AXIL_ADDR_WIDTH = 5, /*local*/parameter C_AXIL_DATA_WIDTH = 32, // // OPT_UNALIGNED turns on support for unaligned addresses, // whether source, destination, or length parameters. parameter [0:0] OPT_UNALIGNED = 1'b1, // // OPT_WRAPMEM controls what happens if the transfer runs off // of the end of memory. If set, the transfer will continue // again from the beginning of memory. If clear, the transfer // will be aborted with an error if either read or write // address ever get this far. parameter [0:0] OPT_WRAPMEM = 1'b1, // // LGMAXBURST controls the size of the maximum burst produced // by this core. Specifically, its the log (based 2) of that // maximum size. Hence, for AXI4, this size must be 8 // (i.e. 2^8 or 256 beats) or less. For AXI3, the size must // be 4 or less. Tests have verified performance for // LGMAXBURST as low as 2. While I expect it to fail at // LGMAXBURST=0, I haven't verified at what value this burst // parameter is too small. `ifdef AXI3 parameter LGMAXBURST=4, // 16 beats max `else parameter LGMAXBURST=8, // 256 beats `endif // LGFIFO: This is the (log-based-2) size of the internal FIFO. // Hence if LGFIFO=8, the internal FIFO will have 256 elements // (words) in it. High throughput transfers are accomplished // by first storing data into a FIFO, then once a full burst // size is available bursting that data over the bus. In // order to be able to keep receiving data while bursting it // out, the FIFO size must be at least twice the size of the // maximum burst size. Larger sizes are possible as well. parameter LGFIFO = LGMAXBURST+1, // 512 element FIFO // // LGLEN: specifies the number of bits in the transfer length // register. If a transfer cannot be specified in LGLEN bits, // it won't happen. LGLEN must be less than or equal to the // address width. parameter LGLEN = C_AXI_ADDR_WIDTH, // // OPT_LOWPOWER: parameter [0:0] OPT_LOWPOWER = 1'b0, // // OPT_CLKGATE: parameter [0:0] OPT_CLKGATE = OPT_LOWPOWER, // // AXI uses ID's to transfer information. This core rather // ignores them. Instead, it uses a constant ID for all // transfers. The following two parameters control that ID. parameter [C_AXI_ID_WIDTH-1:0] AXI_READ_ID = 0, parameter [C_AXI_ID_WIDTH-1:0] AXI_WRITE_ID = 0, // // The "ABORT_KEY" is a byte that, if written to the control // word while the core is running, will cause the data transfer // to be aborted. parameter [7:0] ABORT_KEY = 8'h6d, // /*local*/parameter ADDRLSB= $clog2(C_AXI_DATA_WIDTH)-3, /*local*/parameter AXILLSB= $clog2(C_AXIL_DATA_WIDTH)-3, /*local*/parameter LGLENW= LGLEN-ADDRLSB // }}} ) ( // {{{ input wire S_AXI_ACLK, input wire S_AXI_ARESETN, // AXI low-power interface // {{{ // This has been removed, due to a lack of definition from the // AXI standard for these wires. // }}} // // The AXI4-lite 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 reg 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 reg S_AXIL_RVALID, input wire S_AXIL_RREADY, output reg [C_AXIL_DATA_WIDTH-1:0] S_AXIL_RDATA, output wire [1:0] S_AXIL_RRESP, // }}} // The AXI Master (DMA) interface // {{{ output reg M_AXI_AWVALID, input wire M_AXI_AWREADY, output reg [C_AXI_ID_WIDTH-1:0] M_AXI_AWID, output reg [C_AXI_ADDR_WIDTH-1:0] M_AXI_AWADDR, `ifdef AXI3 output reg [3:0] M_AXI_AWLEN, `else output reg [7:0] M_AXI_AWLEN, `endif output reg [2:0] M_AXI_AWSIZE, output reg [1:0] M_AXI_AWBURST, output reg M_AXI_AWLOCK, output reg [3:0] M_AXI_AWCACHE, output reg [2:0] M_AXI_AWPROT, output reg [3:0] M_AXI_AWQOS, // // output reg M_AXI_WVALID, input wire M_AXI_WREADY, `ifdef AXI3 output reg [C_AXI_ID_WIDTH-1:0] M_AXI_WID, `endif output wire [C_AXI_DATA_WIDTH-1:0] M_AXI_WDATA, output reg [C_AXI_DATA_WIDTH/8-1:0] M_AXI_WSTRB, output reg M_AXI_WLAST, // // input wire M_AXI_BVALID, output reg M_AXI_BREADY, input wire [C_AXI_ID_WIDTH-1:0] M_AXI_BID, input wire [1:0] M_AXI_BRESP, // // output reg M_AXI_ARVALID, input wire M_AXI_ARREADY, output wire [C_AXI_ID_WIDTH-1:0] M_AXI_ARID, output reg [C_AXI_ADDR_WIDTH-1:0] M_AXI_ARADDR, `ifdef AXI3 output reg [3:0] M_AXI_ARLEN, `else output reg [7:0] M_AXI_ARLEN, `endif 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_ID_WIDTH-1:0] M_AXI_RID, input wire [C_AXI_DATA_WIDTH-1:0] M_AXI_RDATA, input wire M_AXI_RLAST, input wire [1:0] M_AXI_RRESP, // }}} output reg o_int // }}} ); // Local declarations // {{{ // The number of beats in this maximum burst size is // automatically determined from LGMAXBURST, and so its // forced to be a power of two this way. localparam MAXBURST=(1< C_AXIL_DATA_WIDTH) begin r_src_addr <= new_widesrc[C_AXI_ADDR_WIDTH-1:0]; end DSTLO_ADDR: begin r_dst_addr <= new_widedst[C_AXI_ADDR_WIDTH-1:0]; end DSTHI_ADDR: if (C_AXI_ADDR_WIDTH > C_AXIL_DATA_WIDTH) begin r_dst_addr <= new_widedst[C_AXI_ADDR_WIDTH-1:0]; end LENLO_ADDR: begin r_len <= new_widelen[LGLEN-1:0]; zero_len <= (new_widelen == 0); end LENHI_ADDR: if (LGLEN > C_AXIL_DATA_WIDTH) begin r_len <= new_widelen[LGLEN-1:0]; zero_len <= (new_widelen == 0); end default: begin end endcase // }}} end else if (r_busy) begin // {{{ r_dst_addr <= write_address[C_AXI_ADDR_WIDTH-1:0]; if (writes_remaining_w[LGLENW]) r_len <= -1; else r_len <= { writes_remaining_w[LGLENW-1:0], {(ADDRLSB){1'b0}} }; if (OPT_UNALIGNED) r_len[ADDRLSB-1:0] <= 0; zero_len <= (writes_remaining_w == 0); if (M_AXI_RVALID && M_AXI_RREADY && !M_AXI_RRESP[1]) begin r_src_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB] <= r_src_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB]+1; r_src_addr[ADDRLSB-1:0] <= 0; end // }}} 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 readlen_b[LGLEN:ADDRLSB]) initial_readlen_w[LGMAXBURST:0] = { 1'b0, readlen_b[ADDRLSB +: LGMAXBURST] }; initial_readlen_w[LGLENW-1:LGMAXBURST+1] = 0; end // }}} // readlen_w // {{{ // Verilator lint_off WIDTH always @(posedge i_clk) if (!r_busy) begin readlen_w <= initial_readlen_w; end else if (phantom_read) begin readlen_w <= reads_remaining_w - (M_AXI_ARLEN+1); if (reads_remaining_w - (M_AXI_ARLEN+1) > MAXBURST) readlen_w <= MAXBURST; end // Verilator lint_on WIDTH // }}} // w_start_read // {{{ always @(*) begin w_start_read = r_busy && reads_remaining_nonzero; if (phantom_read) w_start_read = 0; if (!OPT_WRAPMEM && read_address[C_AXI_ADDR_WIDTH]) w_start_read = 0; if (fifo_space_available < MAXBURST) w_start_read = 0; if (M_AXI_ARVALID && !M_AXI_ARREADY) w_start_read = 0; if (r_err || r_abort) w_start_read = 0; end // }}} // M_AXI_ARVALID, phantom_read // {{{ initial M_AXI_ARVALID = 1'b0; initial phantom_read = 1'b0; always @(posedge i_clk) if (i_reset || !r_busy) begin M_AXI_ARVALID <= 0; phantom_read <= 0; end else if (!M_AXI_ARVALID || M_AXI_ARREADY) begin M_AXI_ARVALID <= w_start_read; phantom_read <= w_start_read; end else phantom_read <= 0; // }}} // M_AXI_ARLEN // {{{ always @(posedge i_clk) if (i_reset || !r_busy) M_AXI_ARLEN <= 0; else if (!M_AXI_ARVALID || M_AXI_ARREADY) begin `ifdef AXI3 M_AXI_ARLEN <= readlen_w[3:0] - 4'h1; `else M_AXI_ARLEN <= readlen_w[7:0] - 8'h1; `endif if (OPT_LOWPOWER && !w_start_read) M_AXI_ARLEN <= 0; end // }}} assign M_AXI_ARID = AXI_READ_ID; assign M_AXI_ARBURST = AXI_INCR; assign M_AXI_ARSIZE = ADDRLSB[2:0]; assign M_AXI_ARLOCK = 1'b0; assign M_AXI_ARCACHE = 4'b0011; assign M_AXI_ARPROT = r_prot; assign M_AXI_ARQOS = r_qos; // assign M_AXI_RREADY = !no_read_bursts_outstanding; // }}} //////////////////////////////////////////////////////////////////////// // // The intermediate FIFO // {{{ //////////////////////////////////////////////////////////////////////// // // always @(*) fifo_reset = i_reset || !r_busy || r_done; generate if (OPT_UNALIGNED) begin : REALIGNMENT_FIFO reg extra_realignment_read; // {{{ reg [ADDRLSB-1:0] inbyte_shift, outbyte_shift, remaining_read_realignment; reg [ADDRLSB+3-1:0] inshift_down, outshift_down, inshift_up, outshift_up; reg [C_AXI_DATA_WIDTH-1:0] r_partial_inword, r_outword, r_partial_outword, r_realigned_incoming; wire [C_AXI_DATA_WIDTH-1:0] fifo_data; reg [ADDRLSB-1:0] r_last_write_addr; reg r_oneword, r_firstword; /////////////////// always @(posedge i_clk) if (!r_busy) begin inbyte_shift <= r_src_addr[ADDRLSB-1:0]; inshift_up <= 0; inshift_up[3 +: ADDRLSB] <= -r_src_addr[ADDRLSB-1:0]; end always @(*) inshift_down = { inbyte_shift, 3'b000 }; always @(*) remaining_read_realignment = -r_src_addr[ADDRLSB-1:0]; // extra_realignment_read will be true if we need to flush // the read processor after the last word has been read in an // extra write to the FIFO that isn't associated with any reads. // In other words, if the number of writes to the FIFO is // greater than the number of read beats // - (src_addr unaligned?1:0) always @(posedge i_clk) if (!r_busy) begin extra_realignment_read <= (remaining_read_realignment >= r_len[ADDRLSB-1:0]) ? 1:0; if (r_len[ADDRLSB-1:0] == 0) extra_realignment_read <= 1'b0; if (r_src_addr[ADDRLSB-1:0] == 0) extra_realignment_read <= 1'b0; end else if ((!r_write_fifo || !fifo_full) && clear_read_pipeline) extra_realignment_read <= 1'b0; always @(posedge i_clk) if (!r_busy || !extra_realignment_read || clear_read_pipeline) clear_read_pipeline <= 0; else if (!r_write_fifo || !fifo_full) clear_read_pipeline <= (read_beats_remaining_w == (M_AXI_RVALID ? 1:0)); `ifdef FORMAL always @(*) if (r_busy) begin if (!extra_realignment_read) begin assert(!clear_read_pipeline); end else if (read_beats_remaining_w > 0) begin assert(!clear_read_pipeline); end else if (!no_read_bursts_outstanding) begin assert(!clear_read_pipeline); end end `endif always @(posedge i_clk) if (fifo_reset) r_partial_in_valid <= (r_src_addr[ADDRLSB-1:0] == 0); else if (M_AXI_RVALID) r_partial_in_valid <= 1; else if ((!r_write_fifo || !fifo_full) && clear_read_pipeline) // If we have to flush the final partial valid signal, // the do it when writing to the FIFO with clear_read // pipelin set. Actually, this is one clock before // that ... r_partial_in_valid <= 0; always @(posedge i_clk) if (fifo_reset || (inbyte_shift == 0)) r_partial_inword <= 0; else if (M_AXI_RVALID) r_partial_inword <= M_AXI_RDATA >> inshift_down; initial r_write_fifo = 0; always @(posedge i_clk) if (fifo_reset) r_write_fifo <= 0; else if (M_AXI_RVALID || clear_read_pipeline) r_write_fifo <= r_partial_in_valid; else if (!fifo_full) r_write_fifo <= 0; always @(posedge i_clk) if (fifo_reset) r_realigned_incoming <= 0; else if (M_AXI_RVALID) r_realigned_incoming <= r_partial_inword | (M_AXI_RDATA << inshift_up); else if (!r_write_fifo || !fifo_full) r_realigned_incoming <= r_partial_inword; sfifo #( // {{{ .BW(C_AXI_DATA_WIDTH), .LGFLEN(LGFIFO), .OPT_ASYNC_READ(1'b1) // }}} ) middata( // {{{ i_clk, fifo_reset, r_write_fifo, r_realigned_incoming, fifo_full, fifo_fill, r_read_fifo, fifo_data, fifo_empty // }}} ); always @(posedge i_clk) if (!r_busy) begin outbyte_shift <= r_dst_addr[ADDRLSB-1:0]; outshift_down <= 0; outshift_down[3 +: ADDRLSB] <= -r_dst_addr[ADDRLSB-1:0]; end always @(*) outshift_up = { outbyte_shift, 3'b000 }; always @(posedge i_clk) if (fifo_reset) r_partial_outword <= 0; else if (r_read_fifo && outshift_up != 0) r_partial_outword <= (fifo_data >> outshift_down); else if (M_AXI_WVALID && M_AXI_WREADY) r_partial_outword <= 0; always @(posedge i_clk) if (fifo_reset) r_partial_outvalid <= 0; else if (r_read_fifo && !fifo_empty) r_partial_outvalid <= 1; else if (fifo_empty && M_AXI_WVALID && M_AXI_WREADY) r_partial_outvalid <= extra_realignment_write; always @(posedge i_clk) if (fifo_reset) r_outword <= 0; else if (!r_partial_outvalid || (M_AXI_WVALID && M_AXI_WREADY)) begin if (!fifo_empty) r_outword <= r_partial_outword | (fifo_data << outshift_up); else r_outword <= r_partial_outword; end /*always @(*)*/ assign M_AXI_WDATA = r_outword; always @(*) begin r_read_fifo = 0; if (!r_partial_outvalid) r_read_fifo = 1; if (M_AXI_WVALID && M_AXI_WREADY) r_read_fifo = 1; if (fifo_empty) r_read_fifo = 0; end //////////////////////////////////////////////////////////////// // // Write strobe logic for the unaligned case // //////////////////////////////////////////////////////////////// // // always @(posedge i_clk) if (!r_busy) begin if (r_len[(LGLEN-1):(ADDRLSB+1)] != 0) r_oneword <= 0; else r_oneword <= (({ 2'b0, r_dst_addr[ADDRLSB-1:0]} + r_len[ADDRLSB+1:0]) <= { 2'b01, {(ADDRLSB){1'b0}} } ? 1:0); end initial r_first_wstrb = 0; always @(posedge i_clk) if (!r_busy) begin if (r_len[LGLEN-1:ADDRLSB] != 0) r_first_wstrb <= -1 << r_dst_addr[ADDRLSB-1:0]; else r_first_wstrb <= ((1< 2) M_AXI_WSTRB <= -1; else M_AXI_WSTRB <= r_last_wstrb; end else if (r_firstword) M_AXI_WSTRB <= r_first_wstrb; if (r_err || r_abort) M_AXI_WSTRB <= 0; end // }}} end else begin : ALIGNED_FIFO // {{{ always @(*) begin r_first_wstrb = -1; r_last_wstrb = -1; r_partial_in_valid = 1; r_partial_outvalid = !fifo_empty; r_write_fifo = M_AXI_RVALID; r_read_fifo = M_AXI_WVALID && M_AXI_WREADY; clear_read_pipeline = 1'b0; end sfifo #( // {{{ .BW(C_AXI_DATA_WIDTH), .LGFLEN(LGFIFO), .OPT_ASYNC_READ(1'b1) // }}} ) middata( // {{{ i_clk, fifo_reset, r_write_fifo, M_AXI_RDATA, fifo_full, fifo_fill, r_read_fifo, M_AXI_WDATA, fifo_empty // }}} ); initial M_AXI_WSTRB = -1; always @(posedge i_clk) if (!S_AXI_ARESETN || !r_busy) M_AXI_WSTRB <= -1; else if (!M_AXI_WVALID || M_AXI_WREADY) M_AXI_WSTRB <= (r_err || r_abort) ? 0 : -1; wire extra_realignment_read; //always @(*) assign extra_realignment_read /*<*/= 0; // }}} end endgenerate // fifo_space_available // {{{ always @(posedge i_clk) if (fifo_reset) fifo_space_available <= (1< ((phantom_write) ? (M_AXI_AWLEN+1) : 0)) last_write_ack <= 0; else last_write_ack <= (write_bursts_outstanding == (phantom_write ? 0:1) + (M_AXI_BVALID ? 1:0)); // Verilator lint_on WIDTH // }}} // r_done // {{{ always @(posedge i_clk) if (!r_busy || M_AXI_ARVALID || M_AXI_AWVALID) r_done <= 0; else if (read_bursts_outstanding > 0) r_done <= 0; else if (write_bursts_outstanding > (M_AXI_BVALID ? 1:0)) r_done <= 0; else if (r_abort || r_err) r_done <= 1; else if (writes_remaining_w > 0) r_done <= 0; else r_done <= 1; // }}} // writelen_b // {{{ always @(*) if (OPT_UNALIGNED) writelen_b = { 1'b0, r_len } + { {(LGLEN+1-ADDRLSB){1'b0}}, r_dst_addr[ADDRLSB-1:0] } + { {(LGLEN+1-ADDRLSB){1'b0}}, {(ADDRLSB){1'b1}} }; // was + (1< initial_write_distance_to_boundary_w) first_write_len_w<=initial_write_distance_to_boundary_w; end // }}} // write_burst_length // {{{ // Verilator lint_off WIDTH always @(*) if (first_write_burst) write_burst_length = first_write_len_w; else begin write_burst_length = MAXBURST; if (!multiple_write_bursts_remaining && (write_burst_length[ADDRLSB +: LGMAXBURST] > writes_remaining_w[ADDRLSB +: LGMAXBURST])) write_burst_length = writes_remaining_w; end // Verilator lint_on WIDTH // }}} // write_count // {{{ initial write_count = 0; always @(posedge i_clk) if (i_reset || !r_busy) write_count <= 0; else if (w_write_start) begin write_count <= 0; write_count[LGMAXBURST:0] <= write_burst_length[LGMAXBURST:0]; end else if (M_AXI_WVALID && M_AXI_WREADY) write_count <= write_count - 1; // }}} // M_AXI_WLAST // {{{ initial M_AXI_WLAST = 0; always @(posedge i_clk) if (i_reset || !r_busy) begin M_AXI_WLAST <= 0; end else if (!M_AXI_WVALID || M_AXI_WREADY) begin M_AXI_WLAST <= 1; if (write_count > 2) M_AXI_WLAST <= 0; if (w_write_start) `ifdef AXI3 M_AXI_WLAST <= (write_burst_length[3:0] == 1); `else M_AXI_WLAST <= (write_burst_length[7:0] == 1); `endif end // }}} // w_write_start // {{{ always @(*) last_write_burst = (write_burst_length == writes_remaining_w); always @(*) begin // Verilator lint_off WIDTH if (!last_write_burst && OPT_UNALIGNED) w_write_start = (fifo_data_available > 1) &&(fifo_data_available > write_burst_length); else w_write_start = (fifo_data_available >= write_burst_length); // Verilator lint_on WIDTH if (!write_requests_remaining) w_write_start = 0; if (!OPT_WRAPMEM && write_address[C_AXI_ADDR_WIDTH]) w_write_start = 0; if (phantom_write) w_write_start = 0; if (M_AXI_AWVALID && !M_AXI_AWREADY) w_write_start = 0; if (M_AXI_WVALID && (!M_AXI_WLAST || !M_AXI_WREADY)) w_write_start = 0; if (i_reset || r_err || r_abort || !r_busy) w_write_start = 0; end // }}} // M_AXI_AWVALID, phantom_write // {{{ initial M_AXI_AWVALID = 0; initial phantom_write = 0; always @(posedge i_clk) if (i_reset) begin M_AXI_AWVALID <= 0; phantom_write <= 0; end else if (!M_AXI_AWVALID || M_AXI_AWREADY) begin M_AXI_AWVALID <= w_write_start; phantom_write <= w_write_start; end else phantom_write <= 0; // }}} // M_AXI_WVALID // {{{ initial M_AXI_WVALID = 1'b0; always @(posedge i_clk) if (i_reset) M_AXI_WVALID <= 0; else if (!M_AXI_WVALID || M_AXI_WREADY) begin M_AXI_WVALID <= 0; if (M_AXI_WVALID && !M_AXI_WLAST) M_AXI_WVALID <= 1; if (w_write_start) M_AXI_WVALID <= 1; end // }}} // M_AXI_AWLEN // {{{ initial M_AXI_AWLEN = 0; always @(posedge i_clk) if (i_reset || !r_busy) M_AXI_AWLEN <= 0; else if (!M_AXI_AWVALID || M_AXI_AWREADY) begin M_AXI_AWLEN <= 0; if (w_write_start) `ifdef AXI3 M_AXI_AWLEN <= write_burst_length[3:0]-1; `else M_AXI_AWLEN <= write_burst_length[7:0]-1; `endif end // }}} // M_AXI_AWADDR // {{{ always @(posedge i_clk) if (!r_busy) M_AXI_AWADDR <= r_dst_addr; else if (!M_AXI_AWVALID || M_AXI_AWREADY) M_AXI_AWADDR <= write_address[C_AXI_ADDR_WIDTH-1:0]; // }}} always @(*) begin M_AXI_AWID = AXI_WRITE_ID; M_AXI_AWBURST = AXI_INCR; M_AXI_AWSIZE = ADDRLSB[2:0]; M_AXI_AWLOCK = 1'b0; M_AXI_AWCACHE = 4'b0011; M_AXI_AWPROT = r_prot; M_AXI_AWQOS = r_qos; // `ifdef AXI3 M_AXI_WID = AXI_WRITE_ID; `endif M_AXI_BREADY = !r_done; end // }}} //////////////////////////////////////////////////////////////////////// // // (Optional) Clock gating // {{{ //////////////////////////////////////////////////////////////////////// // // generate if (OPT_CLKGATE) begin : CLK_GATING // {{{ reg 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; end assign clk_active = r_clk_active; // }}} // Gate the clock here locally // {{{ always @(negedge S_AXI_ACLK) if (!S_AXI_ARESETN) gaten <= 1'b1; else gaten <= r_clk_active; 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 lint_off UNUSED // Verilator coverage_off wire unused; assign unused = &{ 1'b0, S_AXIL_AWPROT, S_AXIL_ARPROT, M_AXI_BID, M_AXI_RID, M_AXI_BRESP[0], M_AXI_RRESP[0], S_AXIL_AWADDR[AXILLSB-1:0], S_AXIL_ARADDR[AXILLSB-1:0], fifo_full, fifo_fill, fifo_empty, `ifdef AXI3 readlen_w[LGLENW:4], `else readlen_w[LGLENW:8], `endif writelen_b[ADDRLSB-1:0], readlen_b[ADDRLSB-1:0], read_distance_to_boundary_b }; generate if (C_AXI_ADDR_WIDTH < 2*C_AXIL_DATA_WIDTH) begin : NEW_UNUSED wire genunused; assign genunused = &{ 1'b0, new_widesrc[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH], new_widedst[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH] }; end endgenerate // Verilator coverage_on // Verilator lint_on UNUSED // }}} //////////////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////// // // Formal property section // {{{ //////////////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////// `ifdef FORMAL //////////////////////////////////////////////////////////////////////// // // The following formal properties are only a subset of those used // to verify the full core. Do not be surprised to find syntax errors // here, or registers that are not defined. These are correct in the // full version. // //////////////////////////////////////////////////////////////////////// // reg f_past_valid; initial f_past_valid = 0; always @(posedge S_AXI_ACLK) f_past_valid <= 1; // // ... // reg [C_AXI_ADDR_WIDTH:0] f_next_wraddr, f_next_rdaddr; reg [C_AXI_ADDR_WIDTH:0] f_src_addr, f_dst_addr, f_read_address, f_write_address, f_read_check_addr, f_write_beat_addr, f_read_beat_addr; reg [LGLEN:0] f_length, f_rdlength, f_wrlength, f_writes_complete, f_reads_complete; //////////////////////////////////////////////////////////////////////// // // The 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) // // ... // ); // // ... // // // Verify the AXI-lite result registers // always @(*) if (!r_busy) assert((r_done && (r_err || r_abort)) || (zero_len == (r_len == 0))); else assert(zero_len == (r_len == 0 && writes_remaining_w == 0)); always @(*) if (!i_reset && !OPT_UNALIGNED) assert(r_src_addr[ADDRLSB-1:0] == 0); always @(*) if (!i_reset && !OPT_UNALIGNED) assert(r_dst_addr[ADDRLSB-1:0] == 0); // }}} //////////////////////////////////////////////////////////////////////// // // The main AXI data 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_MAXBURST(MAXBURST) // // ... // ) faxi( .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), // .i_axi_awvalid(M_AXI_AWVALID), .i_axi_awready(M_AXI_AWREADY), .i_axi_awid( M_AXI_AWID), .i_axi_awaddr( M_AXI_AWADDR), .i_axi_awlen( M_AXI_AWLEN), .i_axi_awsize( M_AXI_AWSIZE), .i_axi_awburst(M_AXI_AWBURST), .i_axi_awlock( M_AXI_AWLOCK), .i_axi_awcache(M_AXI_AWCACHE), .i_axi_awprot( M_AXI_AWPROT), .i_axi_awqos( M_AXI_AWQOS), // .i_axi_wvalid(M_AXI_WVALID), .i_axi_wready(M_AXI_WREADY), .i_axi_wdata( M_AXI_WDATA), .i_axi_wstrb( M_AXI_WSTRB), .i_axi_wlast( M_AXI_WLAST), // .i_axi_bvalid(M_AXI_BVALID), .i_axi_bready(M_AXI_BREADY), .i_axi_bid( M_AXI_BID), .i_axi_bresp( M_AXI_BRESP), // .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_rid( M_AXI_RID), .i_axi_rdata( M_AXI_RDATA), .i_axi_rlast( M_AXI_RLAST), .i_axi_rresp( M_AXI_RRESP) // // ... // ); always @(*) begin // // ... // if (r_done) begin // // ... // assert(!M_AXI_AWVALID); assert(!M_AXI_WVALID); assert(!M_AXI_ARVALID); end end // }}} //////////////////////////////////////////////////////////////////////// // // Internal assertions (Induction) // {{{ //////////////////////////////////////////////////////////////////////// // // always @(posedge S_AXI_ACLK) if (w_start) begin f_src_addr <= { 1'b0, r_src_addr }; f_dst_addr <= { 1'b0, r_dst_addr }; f_length <= r_len; end else if (r_busy) begin assert(f_length != 0); assert(f_length[LGLEN] == 0); assert(f_src_addr[C_AXI_ADDR_WIDTH] == 1'b0); assert(f_dst_addr[C_AXI_ADDR_WIDTH] == 1'b0); end always @(*) begin f_rdlength = f_length + f_src_addr[ADDRLSB-1:0] + (1<= f_length[ADDRLSB-1:0]) ? 1:0; if (f_length[ADDRLSB-1:0] == 0) f_extra_realignment_read = 0; end else f_extra_realignment_read = 1'b0; // // f_extra_realignment_preread // will be true anytime we need to read a first word before // writing anything to the buffer. if (OPT_UNALIGNED && f_src_addr[ADDRLSB-1:0] != 0) f_extra_realignment_preread = 1'b1; else f_extra_realignment_preread = 1'b0; // // f_extra_realignment_write // true if following the last read from the FIFO there's a // partial word that will need to be flushed through the // system. if (OPT_UNALIGNED && f_raw_length[LGLEN:ADDRLSB] != f_wrlength[LGLEN:ADDRLSB]) f_extra_realignment_write = 1'b1; else f_extra_realignment_write = 1'b0; f_extra_write_in_fifo = (f_extra_realignment_write) && (read_beats_remaining_w == 0)&&(!last_read_beat); end always @(*) if (r_busy && !OPT_UNALIGNED) begin assert(f_src_addr[ADDRLSB-1:0] == 0); assert(f_dst_addr[ADDRLSB-1:0] == 0); assert(f_length[ADDRLSB-1:0] == 0); end always @(*) if (r_busy) begin if (!f_extra_realignment_write) assert(!extra_realignment_write); else if (f_writes_complete >= f_wrlength[LGLEN:ADDRLSB]-1) assert(!extra_realignment_write); else assert(extra_realignment_write); if ((f_writes_complete > 0 || M_AXI_WVALID) && extra_realignment_write) assert(r_partial_outvalid); end always @(*) if (r_busy) begin if (extra_realignment_read) assert(f_extra_realignment_read); else if (read_beats_remaining_w > 0) assert(f_extra_realignment_read == extra_realignment_read); end // // ... // always @(*) if (fifo_full) assert(no_read_bursts_outstanding); always @(*) if (r_busy) assert(!r_int); //////////////////////////////////////////////////////////////////////// // // Write checks // // // ... // always @(*) begin f_write_address = 0; f_write_address[C_AXI_ADDR_WIDTH:ADDRLSB] = f_dst_addr[C_AXI_ADDR_WIDTH:ADDRLSB] + (f_wrlength[LGLEN:ADDRLSB] - writes_remaining_w); end always @(*) begin f_next_wraddr = { 1'b0, M_AXI_AWADDR } + ((M_AXI_AWLEN+1)< 0)) assert(write_address[LGMAXBURST+ADDRLSB-1:0] == 0); if (writes_remaining_w != f_wrlength[LGLEN:ADDRLSB] && writes_remaining_w != 0) assert((write_burst_length == (1<= (M_AXI_AWLEN+1)); else if (M_AXI_AWVALID) assert(write_address[C_AXI_ADDR_WIDTH-1:0] == f_next_wraddr[C_AXI_ADDR_WIDTH-1:0]); // // ... // always @(*) if (M_AXI_WVALID) begin if (OPT_UNALIGNED) assert(r_partial_outvalid); else assert(!fifo_empty || r_abort || r_err); // // ... // end always @(*) begin f_write_beat_addr = 0; f_write_beat_addr[C_AXI_ADDR_WIDTH:ADDRLSB] = f_dst_addr[C_AXI_ADDR_WIDTH:ADDRLSB] + (f_wrlength[LGLEN:ADDRLSB]-write_beats_remaining); // // ... // end always @(*) if (r_busy) begin // // ... // if (write_beats_remaining == 0) assert(!M_AXI_WVALID); end always @(*) if (writes_remaining_w < f_wrlength[LGLEN:ADDRLSB]) begin if (writes_remaining_w == 0) assert(fifo_data_available == 0); // else ... end //////////////////////////////////////////////////////////////////////// // // Read checks // always @(*) begin f_reads_complete = f_rdlength[LGLEN:ADDRLSB] - reads_remaining_w - // ... // // ... // end always @(*) begin if (reads_remaining_w == f_rdlength[LGLEN:ADDRLSB]) f_read_address = f_src_addr; else begin f_read_address = 0; f_read_address[C_AXI_ADDR_WIDTH:ADDRLSB] = f_src_addr[C_AXI_ADDR_WIDTH:ADDRLSB] + (f_rdlength[LGLEN:ADDRLSB] - reads_remaining_w); end f_araddr = f_read_address; if (M_AXI_ARVALID && !phantom_read) f_araddr[C_AXI_ADDR_WIDTH:ADDRLSB] = f_araddr[C_AXI_ADDR_WIDTH:ADDRLSB] - (M_AXI_ARLEN+1); if (f_araddr[C_AXI_ADDR_WIDTH:ADDRLSB] == f_src_addr[C_AXI_ADDR_WIDTH:ADDRLSB]) f_araddr[ADDRLSB-1:0] = f_src_addr[ADDRLSB-1:0]; // // Match the read check address to our source address // f_read_check_addr = 0; f_read_check_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB] = f_src_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB] + f_reads_complete + // ... // // Match the RVALID address to our source address // f_read_beat_addr = 0; if (f_reads_complete == 0) f_read_beat_addr = f_src_addr; else f_read_beat_addr[C_AXI_ADDR_WIDTH:ADDRLSB] = f_src_addr[C_AXI_ADDR_WIDTH:ADDRLSB] + f_reads_complete; f_end_of_read_burst = M_AXI_ARADDR; f_end_of_read_burst[ADDRLSB-1:0] = 0; f_end_of_read_burst[C_AXI_ADDR_WIDTH:ADDRLSB] = f_end_of_read_burst[C_AXI_ADDR_WIDTH:ADDRLSB] + (M_AXI_ARLEN + 1); // // ... // end always @(*) begin f_next_rdaddr = { 1'b0, M_AXI_ARADDR } + ((M_AXI_ARLEN+1)< 0) assert(M_AXI_ARADDR[0 +: LGMAXBURST + ADDRLSB] == 0); end else if (phantom_read) assert(reads_remaining_w == f_rdlength[LGLEN:ADDRLSB]); else if (M_AXI_ARVALID) assert(reads_remaining_w == f_rdlength[LGLEN:ADDRLSB] - (M_AXI_ARLEN+1)); // All but the first burst should be aligned if (!OPT_UNALIGNED || M_AXI_ARADDR != f_src_addr) assert(M_AXI_ARADDR[ADDRLSB-1:0] == 0); if (phantom_read) assert(M_AXI_ARADDR == read_address[C_AXI_ADDR_WIDTH-1:0]); else if (M_AXI_ARVALID) assert(read_address[C_AXI_ADDR_WIDTH-1:0] == f_next_rdaddr[C_AXI_ADDR_WIDTH-1:0]); end // else ... // // ... // // Constrain read_address--our pointer to the next bursts address always @(*) if (r_busy) begin assert((read_address == f_src_addr) || (read_address[LGMAXBURST+ADDRLSB-1:0] == 0) || (reads_remaining_w == 0)); assert(read_address == f_read_address); if (!OPT_UNALIGNED) assert(read_address[ADDRLSB-1:0] == 0); if ((reads_remaining_w != f_rdlength[LGLEN:ADDRLSB]) &&(reads_remaining_w > 0)) assert(read_address[LGMAXBURST+ADDRLSB-1:0] == 0); if ((read_address[C_AXI_ADDR_WIDTH:ADDRLSB] != f_src_addr[C_AXI_ADDR_WIDTH:ADDRLSB]) &&(reads_remaining_w > 0)) assert(read_address[LGMAXBURST+ADDRLSB-1:0] == 0); end ///////// // // Constrain the read length // always @(*) if (M_AXI_ARVALID) begin assert(M_AXI_ARLEN < (1< (M_AXI_ARLEN+1)) assert(f_end_of_read_burst[ADDRLSB+LGMAXBURST-1:0]==0); ///////// // // Constrain RLAST // always @(*) if (M_AXI_RVALID) begin if (M_AXI_RLAST) begin if (f_read_beat_addr[C_AXI_ADDR_WIDTH:ADDRLSB] != f_last_src_beat[C_AXI_ADDR_WIDTH:ADDRLSB]) assert(&f_read_beat_addr[ADDRLSB+LGMAXBURST-1:ADDRLSB]); end else assert(f_read_beat_addr[ADDRLSB+LGMAXBURST-1:ADDRLSB] != {(LGMAXBURST){1'b1}}); end always @(*) if (f_read_beat_addr == f_last_src_beat) assert(!M_AXI_RVALID || M_AXI_RLAST); else assert(!M_AXI_RVALID || M_AXI_RLAST == (&f_read_beat_addr[LGMAXBURST+ADDRLSB-1:ADDRLSB])); ///////// // // // always @(*) assert(no_read_bursts_outstanding == (read_bursts_outstanding == 0)); always @(*) if (r_busy && !r_err) assert(f_read_beat_addr[C_AXI_ADDR_WIDTH-1:0] == r_src_addr); always @(*) if (r_busy) begin // Some quick checks to make sure the subsequent checks // don't overflow anything assert(reads_remaining_w <= f_rdlength[LGLEN:ADDRLSB]); assert(f_reads_complete <= f_rdlength[LGLEN:ADDRLSB]); // ... assert(fifo_fill <= f_raw_length[LGLEN:ADDRLSB]); assert(fifo_space_available<= (1< 0) assert(readlen_w != 0); if (readlen_w != (1< 0) assert(!r_done); // // If no returns are outstanding, and following an error, then // r_done should be set if ($past(r_busy && (r_err || r_abort)) &&($past(!M_AXI_ARVALID && read_bursts_outstanding==0)) &&($past(!M_AXI_AWVALID && write_bursts_outstanding==0))) assert(r_done); if ($past(r_err || r_abort)) begin // // Just double check that we aren't starting anything // new following either an abort or an error // assert(!$rose(M_AXI_ARVALID)); assert(!$rose(M_AXI_AWVALID)); if ($past(!M_AXI_WVALID || M_AXI_WREADY)) assert(M_AXI_WSTRB == 0); end end // // ... // //////////////////////////////////////// // // ... // always @(*) if (r_busy) begin if (readlen_w == 0) assert(reads_remaining_w == 0); else begin assert(reads_remaining_w > 0); if (!w_start_read) begin assert(readlen_w <= reads_remaining_w); assert(readlen_w <= (1< 0) assert(M_AXI_WVALID); // // ... // end always @(*) if (r_busy) assert(last_write_ack == ((write_bursts_outstanding <= 1) &&(writes_remaining_w == 0))); //////////////////////////////////////////////////////////////////////// // // Initial (only) constraints // {{{ //////////////////////////////////////////////////////////////////////// // // always @(posedge S_AXI_ACLK) if (!f_past_valid || $past(!S_AXI_ARESETN)) begin assert(!S_AXIL_BVALID); assert(!S_AXIL_RVALID); assert(!M_AXI_AWVALID); assert(!M_AXI_WVALID); assert(!M_AXI_ARVALID); assert(write_bursts_outstanding == 0); assert(write_requests_remaining == 0); assert(!phantom_read); assert(!phantom_write); assert(!r_busy); assert(read_bursts_outstanding == 0); assert(no_read_bursts_outstanding); assert(r_len == 0); assert(zero_len); assert(write_count == 0); assert(!M_AXI_WLAST); assert(M_AXI_AWLEN == 0); assert(!r_write_fifo); assert(r_src_addr == 0); assert(r_dst_addr == 0); end always @(*) assert(ADDRLSB + LGMAXBURST <= 12); // }}} //////////////////////////////////////////////////////////////////////// // // Formal contract checking // {{{ // Given an arbitrary address within the source address range, and an // arbitrary piece of data at that source address, prove that said // piece of data will get properly written to the destination address // range // //////////////////////////////////////////////////////////////////////// // // // We'll pick the byte read from const_addr_src, and then written to // const_addr_dst. // generate if (OPT_UNALIGNED) begin : F_UNALIGNED_SAMPLE_CHECK (* anyconst *) reg [C_AXI_ADDR_WIDTH-1:0] f_const_posn; reg [C_AXI_ADDR_WIDTH:0] f_const_addr_src, f_const_addr_dst; reg [8-1:0] f_const_byte; reg [C_AXI_ADDR_WIDTH:0] f_write_fifo_addr, f_read_fifo_addr, f_partial_out_addr; reg [C_AXI_DATA_WIDTH-1:0] f_shifted_read, f_shifted_write; reg [C_AXI_DATA_WIDTH/8-1:0] f_shifted_wstrb; reg [C_AXI_DATA_WIDTH-1:0] f_shifted_to_fifo, f_shifted_partial_to_fifo, f_shifted_partial_from_fifo; reg [C_AXI_DATA_WIDTH-1:0] f_shifted_from_fifo, f_shifted_from_partial_out; reg [ADDRLSB-1:0] subshift; always @(*) begin assume(f_const_posn < f_length); f_const_addr_src = f_src_addr + f_const_posn; f_const_addr_dst = f_dst_addr + f_const_posn; f_shifted_read =(M_AXI_RDATA >> (8*f_const_addr_src[ADDRLSB-1:0])); f_shifted_write=(M_AXI_WDATA >> (8*f_const_addr_dst[ADDRLSB-1:0])); f_shifted_wstrb=(M_AXI_WSTRB >> (f_const_addr_dst[ADDRLSB-1:0])); end //////////////////////////////////////////////////////////////// // // Step 1: Assume a known input // Actually, we'll copy it when it comes in // always @(posedge S_AXI_ACLK) if (M_AXI_RVALID && f_read_beat_addr[C_AXI_ADDR_WIDTH:ADDRLSB] == f_const_addr_src[C_AXI_ADDR_WIDTH:ADDRLSB]) begin // Record our byte to be read f_const_byte <= f_shifted_read[7:0]; end //////////////////////////////////////////////////////////////// // // Step 2: Assert that value gets written on the way out // always @(*) if (M_AXI_WVALID && f_write_beat_addr[C_AXI_ADDR_WIDTH:ADDRLSB] == f_const_addr_dst[C_AXI_ADDR_WIDTH:ADDRLSB]) begin // Assert that we have the right byte in the end if (!r_err && !r_abort) begin // Although it only really matters if we are // actually writing it to the bus assert(f_shifted_wstrb[0]); assert(f_shifted_write[7:0] == f_const_byte); end else assert(f_shifted_wstrb[0] || M_AXI_WSTRB==0); end //////////////////////////////////////////////////////////////// // // Assert the write side of the realignment FIFO // always @(*) begin // // ... // subshift = f_const_posn[ADDRLSB-1:0]; end always @(*) f_shifted_to_fifo = REALIGNMENT_FIFO.r_realigned_incoming >> (8*subshift); always @(*) f_shifted_partial_to_fifo = REALIGNMENT_FIFO.r_partial_inword >> (8*subshift); // // ... // always @(*) if (S_AXI_ARESETN && r_write_fifo && f_write_fifo_addr <= f_const_addr_src && f_write_fifo_addr + (1< f_const_addr_src) begin // Assert that our special byte gets written to the FIFO assert(f_const_byte == f_shifted_to_fifo[7:0]); end //////////////////////////////////////////////////////////////// // // Assert the read side of the realignment FIFO // always @(*) begin f_read_fifo_addr =f_dst_addr; f_read_fifo_addr[C_AXI_ADDR_WIDTH:ADDRLSB] = f_dst_addr[C_AXI_ADDR_WIDTH:ADDRLSB] + (r_partial_outvalid ? 1:0) + f_writes_complete; f_partial_out_addr = f_read_fifo_addr; f_partial_out_addr[ADDRLSB-1:0] = 0; end always @(*) f_shifted_from_fifo = REALIGNMENT_FIFO.fifo_data >> (8*subshift); always @(*) f_shifted_from_partial_out = REALIGNMENT_FIFO.r_partial_outword >> (8*f_const_addr_dst[ADDRLSB-1:0]); always @(*) if (!fifo_empty && f_read_fifo_addr <= f_const_addr_dst && f_read_fifo_addr + (1< f_const_addr_dst) begin // Assume that our special byte gets read from the FIFO // That way we don't have to verify every element of the // FIFO. We'll instead rely upon the FIFO working from // here. assume(f_const_byte == f_shifted_from_fifo[7:0]); end // // ... // end endgenerate // }}} //////////////////////////////////////////////////////////////////////// // // Cover checks // {{{ //////////////////////////////////////////////////////////////////////// // // reg [3:0] f_cvr_rd_bursts, f_cvr_wr_bursts; reg f_cvr_complete; always @(posedge S_AXI_ACLK) if (i_reset) f_cvr_wr_bursts <= 0; else if (w_start) f_cvr_wr_bursts <= 0; else if (M_AXI_AWVALID && M_AXI_AWREADY && !f_cvr_wr_bursts[3]) f_cvr_wr_bursts <= f_cvr_wr_bursts + 1; always @(posedge S_AXI_ACLK) if (i_reset) f_cvr_rd_bursts <= 0; else if (w_start) f_cvr_rd_bursts <= 0; else if (M_AXI_ARVALID && M_AXI_ARREADY && !f_cvr_rd_bursts[3]) f_cvr_rd_bursts <= f_cvr_rd_bursts + 1; always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy)) cover(!r_busy && !r_err && !r_abort && f_cvr_wr_bursts[0] && f_cvr_rd_bursts[0]); always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy)) cover(r_done && !r_err && !r_abort && f_cvr_wr_bursts[0] && f_cvr_rd_bursts[0]); always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy)) cover(!r_busy && !r_err && !r_abort && &f_cvr_wr_bursts[1] && f_cvr_rd_bursts[1]); always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy)) cover(!r_busy && !r_err && !r_abort && (&f_cvr_wr_bursts[1:0]) && (&f_cvr_rd_bursts[1:0])); always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy)) cover(!r_busy && !r_err && !r_abort && f_cvr_wr_bursts[2] && f_cvr_rd_bursts[2]); always @(*) cover(f_past_valid && S_AXI_ARESETN && r_busy && r_err); always @(*) cover(f_past_valid && S_AXI_ARESETN && r_busy && M_AXI_RVALID && M_AXI_RRESP[1]); always @(*) cover(f_past_valid && S_AXI_ARESETN && r_busy && M_AXI_RVALID && M_AXI_BRESP[1]); always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy && r_err)) cover(!r_busy && r_err); always @(posedge S_AXI_ACLK) if (f_past_valid && $past(S_AXI_ARESETN && r_busy && r_abort)) cover(!r_busy && r_abort); always @(posedge S_AXI_ACLK) if (f_past_valid && r_busy && !r_abort && !r_err) cover(reads_remaining_w == 0); always @(posedge S_AXI_ACLK) if (f_past_valid && r_busy && !r_abort && !r_err) cover(reads_remaining_w == 0 && fifo_empty); generate if (OPT_UNALIGNED) begin : COVER_MISALIGNED_COPYING reg [2:0] cvr_opt_checks; integer ik; always @(*) begin cvr_opt_checks[0] = (f_src_addr[ADDRLSB-1:0] == 0); cvr_opt_checks[1] = (f_dst_addr[ADDRLSB-1:0] == 0); cvr_opt_checks[2] = (f_length[ ADDRLSB-1:0] == 0); end always @(posedge S_AXI_ACLK) if (f_past_valid && S_AXI_ARESETN && o_int) begin for(ik=0; ik<8; ik=ik+1) begin cover(cvr_opt_checks == ik[2:0] && !r_busy && r_err && !r_abort && f_cvr_wr_bursts[0] && f_cvr_rd_bursts[0]); cover(cvr_opt_checks == ik[2:0] && !r_busy && !r_err && r_abort && f_cvr_wr_bursts[0] && f_cvr_rd_bursts[0]); cover(cvr_opt_checks == ik[2:0] && !r_busy && !r_err && !r_abort && f_cvr_wr_bursts[0] && f_cvr_rd_bursts[0]); cover(cvr_opt_checks == ik[2:0] && !r_busy && !r_err && !r_abort && f_cvr_wr_bursts[2] && f_cvr_rd_bursts[2]); end end always @(posedge S_AXI_ACLK) if (f_past_valid && S_AXI_ARESETN && o_int) begin cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && f_extra_realignment_read && f_extra_realignment_write); // // Will never happen--since f_extra_realignment_read // can only be true if f_extra_realignment_preread // is also true // // cover(!r_busy && !r_err && !r_abort // && !f_extra_realignment_preread // && f_extra_realignment_read // && f_extra_realignment_write); cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && !f_extra_realignment_read && f_extra_realignment_write); cover(!r_busy && !r_err && !r_abort && !f_extra_realignment_preread && !f_extra_realignment_read && f_extra_realignment_write); cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && f_extra_realignment_read && !f_extra_realignment_write); // !preread && read will never happen cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && !f_extra_realignment_read && !f_extra_realignment_write); cover(!r_busy && !r_err && !r_abort && !f_extra_realignment_preread && !f_extra_realignment_read && !f_extra_realignment_write); cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && f_extra_realignment_read && f_extra_realignment_write && f_length[LGLEN-1:ADDRLSB] > 2); // !preread && read will never happen cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && !f_extra_realignment_read && f_extra_realignment_write && f_length[LGLEN-1:ADDRLSB] > 2); cover(!r_busy && !r_err && !r_abort && !f_extra_realignment_preread && !f_extra_realignment_read && f_extra_realignment_write && f_length[LGLEN-1:ADDRLSB] > 2); cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && f_extra_realignment_read && !f_extra_realignment_write && f_length[LGLEN-1:ADDRLSB] > 2); // !preread && read will never happen cover(!r_busy && !r_err && !r_abort && f_extra_realignment_preread && !f_extra_realignment_read && !f_extra_realignment_write && f_length[LGLEN-1:ADDRLSB] > 2); cover(!r_busy && !r_err && !r_abort && !f_extra_realignment_preread && !f_extra_realignment_read && !f_extra_realignment_write && f_length[LGLEN-1:ADDRLSB] > 2); end end endgenerate // }}} //////////////////////////////////////////////////////////////////////// // // Careless assumptions (i.e. constraints) // //////////////////////////////////////////////////////////////////////// // // // None (currently) `endif // }}} endmodule