From 3038edc09a2eb15762f2e58533f429489107520b Mon Sep 17 00:00:00 2001 From: Alejandro Soto Date: Wed, 6 Mar 2024 02:38:24 -0600 Subject: rtl/wb2axip: add to version control --- rtl/wb2axip/axidma.v | 2977 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2977 insertions(+) create mode 100644 rtl/wb2axip/axidma.v (limited to 'rtl/wb2axip/axidma.v') diff --git a/rtl/wb2axip/axidma.v b/rtl/wb2axip/axidma.v new file mode 100644 index 0000000..46b1e69 --- /dev/null +++ b/rtl/wb2axip/axidma.v @@ -0,0 +1,2977 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// 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. + localparam C_AXIL_ADDR_WIDTH = 5, + localparam 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, + // + localparam ADDRLSB= $clog2(C_AXI_DATA_WIDTH)-3, + localparam AXILLSB= $clog2(C_AXIL_DATA_WIDTH)-3, + localparam 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 reg [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 [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 @(*) + 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; + + always @(*) + 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 -- cgit v1.2.3