| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: axivfifo.v |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: A virtual FIFO, using an AXI based memory on the back end. Data |
| // written via the AXI stream interface is written to an external |
| // memory once enough is available to fill a burst. It's then copied from |
| // this external memory to a FIFO from which it can drive an outgoing |
| // stream. |
| // |
| // Registers: |
| // This core is simple--providing no control interface nor registers |
| // whereby it may be controlled. To place it in a particular region of |
| // SDRAM, limit the address width and fill the rest of the address with |
| // the region you want. Note: THIS CORE DEPENDS UPON ALIGNED MEMORY |
| // ACCESSES. Hence, it must be aligned to the memory to keep these |
| // accesses aligned. |
| // |
| // Performance goals: |
| // 100% throughput |
| // Stay off the bus until you can drive it hard |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // }}} |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Copyright (C) 2020, 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 axivfifo #( |
| // {{{ |
| parameter C_AXI_ID_WIDTH = 1, |
| parameter C_AXI_ADDR_WIDTH = 32, |
| parameter C_AXI_DATA_WIDTH = 32, |
| // |
| // This core requires that the stream data width be identical |
| // to the bus data width. Use an upstream core if you need to |
| // pack a smaller width into your bus's width, or a downstream |
| // core if you need to unpack it. |
| localparam C_AXIS_DATA_WIDTH = C_AXI_DATA_WIDTH, |
| // |
| // LGMAXBURST determines the size of the maximum AXI burst. |
| // In AXI4, the maximum burst size is 256 beats the log_2() |
| // of which is 8. In AXI3, it's a 16 beat burst of which the |
| // log_2() is 4. Smaller numbers are also permissible here, |
| // although not verified. I expect problems if LGMAXBURST is |
| // ever set to zero (no bursting). An upgrade should fix that. |
| // Lower LGMAXBURST values will decrease the latency in this |
| // core while possibly causing throughput to be decreased |
| // (in the rest of the system--this core can handle 100% |
| // throughput either way.) |
| // |
| // Beware of the AXI requirement that bursts cannot cross |
| // 4kB boundaries. If your bus is larger than 128 bits wide, |
| // you'll need to lower this maximum burst size to meet that |
| // requirement. |
| `ifdef AXI3 |
| parameter LGMAXBURST=4, // 16 beats max |
| `else |
| parameter LGMAXBURST=8, // 256 beats |
| `endif |
| // 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<<LGMAXBURST), |
| // |
| // 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--that is LGFIFO must be at least one more |
| // than LGMAXBURST. Larger sizes are possible as well. |
| parameter LGFIFO = LGMAXBURST+1, // 512 element FIFO |
| // |
| // 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, |
| // |
| localparam ADDRLSB= $clog2(C_AXI_DATA_WIDTH)-3 |
| // }}} |
| ) ( |
| // {{{ |
| input wire S_AXI_ACLK, |
| input wire S_AXI_ARESETN, |
| // |
| // The AXI4-stream interface |
| // {{{ |
| // This core does not support TLAST, TKEEP, or TSTRB. If you |
| // want to support these extra values, expand the width of |
| // TDATA, and unpack them on the output of the FIFO. |
| // |
| // The incoming stream |
| input wire S_AXIS_TVALID, |
| output wire S_AXIS_TREADY, |
| input wire [C_AXIS_DATA_WIDTH-1:0] S_AXIS_TDATA, |
| // |
| // The outgoing stream |
| output wire M_AXIS_TVALID, |
| input wire M_AXIS_TREADY, |
| output reg [C_AXIS_DATA_WIDTH-1:0] M_AXIS_TDATA, |
| // }}} |
| // |
| // The AXI Master (DMA) interface |
| // {{{ |
| // First to write data to the (external) AXI buffer |
| output wire M_AXI_AWVALID, |
| input wire M_AXI_AWREADY, |
| output wire [C_AXI_ID_WIDTH-1:0] M_AXI_AWID, |
| output wire [C_AXI_ADDR_WIDTH-1:0] M_AXI_AWADDR, |
| `ifdef AXI3 |
| output wire [3:0] M_AXI_AWLEN, |
| `else |
| output wire [7:0] M_AXI_AWLEN, |
| `endif |
| output wire [2:0] M_AXI_AWSIZE, |
| output wire [1:0] M_AXI_AWBURST, |
| `ifdef AXI3 |
| output wire [1:0] M_AXI_AWLOCK, |
| `else |
| output wire M_AXI_AWLOCK, |
| `endif |
| output wire [3:0] M_AXI_AWCACHE, |
| output wire [2:0] M_AXI_AWPROT, |
| output wire [3:0] M_AXI_AWQOS, |
| // |
| // |
| output wire M_AXI_WVALID, |
| input wire M_AXI_WREADY, |
| `ifdef AXI3 |
| output wire [C_AXI_ID_WIDTH-1:0] M_AXI_WID, |
| `endif |
| output wire [C_AXI_DATA_WIDTH-1:0] M_AXI_WDATA, |
| output wire [C_AXI_DATA_WIDTH/8-1:0] M_AXI_WSTRB, |
| output wire M_AXI_WLAST, |
| // |
| // |
| input wire M_AXI_BVALID, |
| output wire M_AXI_BREADY, |
| input wire [C_AXI_ID_WIDTH-1:0] M_AXI_BID, |
| input wire [1:0] M_AXI_BRESP, |
| // |
| // Then the read interface to read the data back |
| output wire M_AXI_ARVALID, |
| input wire M_AXI_ARREADY, |
| output wire [C_AXI_ID_WIDTH-1:0] M_AXI_ARID, |
| output wire [C_AXI_ADDR_WIDTH-1:0] M_AXI_ARADDR, |
| `ifdef AXI3 |
| output wire [3:0] M_AXI_ARLEN, |
| `else |
| output wire [7:0] M_AXI_ARLEN, |
| `endif |
| output wire [2:0] M_AXI_ARSIZE, |
| output wire [1:0] M_AXI_ARBURST, |
| `ifdef AXI3 |
| output wire [1:0] M_AXI_ARLOCK, |
| `else |
| output wire M_AXI_ARLOCK, |
| `endif |
| 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, |
| // }}} |
| // |
| // {{{ |
| // Request a soft-reset: reset the FIFO without resetting th bus |
| input wire i_reset, |
| // o_err is a hard error. If ever true, the core will come |
| // to a hard stop. |
| output reg o_err, |
| // o_overflow is an indication of data changing before it is |
| // accepted. |
| output reg o_overflow, |
| // o_mm2s_full is a reference to the last FIFO in our |
| // processing pipeline. It's true if a burst of (1<<LGMAXBURST) |
| // words of (1<<ADDRLSB) bytes may be read from the downstream |
| // FIFO without waiting on the external memory. |
| output reg o_mm2s_full, |
| // o_empty is true if nothing is in the core. |
| output reg o_empty, |
| // o_fill counts the number of items in the core. Just because |
| // the number of items is non-zero, however, doesn't mean you |
| // can read them out. In general, you will need to write at |
| // least a full (1<<LGMAXBURST) words to the core, those will |
| // need to be written to memory, read from memory, and then |
| // used to fill the downstream FIFO before you can read. This |
| // number is just available for your informational use. |
| output reg [C_AXI_ADDR_WIDTH-ADDRLSB:0] o_fill |
| // }}} |
| // }}} |
| ); |
| |
| // Register and signal definitions |
| // {{{ |
| localparam BURSTAW = C_AXI_ADDR_WIDTH-LGMAXBURST-ADDRLSB; |
| |
| reg soft_reset, vfifo_empty, vfifo_full; |
| wire reset_fifo; |
| reg [C_AXI_ADDR_WIDTH-ADDRLSB:0] vfifo_fill; |
| reg [BURSTAW:0] mem_data_available_w, |
| writes_outstanding; |
| reg [BURSTAW:0] mem_space_available_w, |
| reads_outstanding; |
| reg s_last_stalled; |
| reg [C_AXI_DATA_WIDTH-1:0] s_last_tdata; |
| wire read_from_fifo, ififo_full, ififo_empty; |
| wire [C_AXI_DATA_WIDTH-1:0] ififo_data; |
| wire [LGFIFO:0] ififo_fill; |
| |
| reg start_write, phantom_write, |
| axi_awvalid, axi_wvalid, axi_wlast, |
| writes_idle; |
| reg [C_AXI_ADDR_WIDTH-1:0] axi_awaddr; |
| reg [LGMAXBURST:0] writes_pending; |
| |
| reg start_read, phantom_read, reads_idle, |
| axi_arvalid; |
| reg [C_AXI_ADDR_WIDTH-1:0] axi_araddr; |
| |
| reg skd_valid; |
| reg [C_AXI_DATA_WIDTH-1:0] skd_data; |
| |
| reg [LGFIFO:0] ofifo_space_available; |
| wire write_to_fifo, ofifo_empty, ofifo_full; |
| wire [LGFIFO:0] ofifo_fill; |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Global FIFO signal handling |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // |
| // A soft reset |
| // {{{ |
| // This is how we reset the FIFO without resetting the rest of the AXI |
| // bus. On a reset request, we raise the soft_reset flag and reset all |
| // of our internal FIFOs. We also stop issuing bus commands. Once all |
| // outstanding bus commands come to a halt, then we release from reset |
| // and start operating as a FIFO. |
| initial soft_reset = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| soft_reset <= 0; |
| else if (i_reset) |
| soft_reset <= 1; |
| else if (writes_idle && reads_idle) |
| soft_reset <= 0; |
| |
| assign reset_fifo = soft_reset || !S_AXI_ARESETN; |
| // }}} |
| |
| // |
| // Calculating the fill of the virtual FIFO, and the associated |
| // full/empty flags that go with it |
| // {{{ |
| initial vfifo_fill = 0; |
| initial vfifo_empty = 1; |
| initial vfifo_full = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || soft_reset) |
| begin |
| vfifo_fill <= 0; |
| vfifo_empty <= 1; |
| vfifo_full <= 0; |
| end else case({ S_AXIS_TVALID && S_AXIS_TREADY, |
| M_AXIS_TVALID && M_AXIS_TREADY }) |
| 2'b10: begin |
| vfifo_fill <= vfifo_fill + 1; |
| vfifo_empty <= 0; |
| vfifo_full <= (&vfifo_fill[C_AXI_ADDR_WIDTH-ADDRLSB-1:0]); |
| end |
| 2'b01: begin |
| vfifo_fill <= vfifo_fill - 1; |
| vfifo_full <= 0; |
| vfifo_empty<= (vfifo_fill <= 1); |
| end |
| default: begin end |
| endcase |
| |
| always @(*) |
| o_fill = vfifo_fill; |
| |
| always @(*) |
| o_empty = vfifo_empty; |
| // }}} |
| |
| // Determining when the write half is idle |
| // {{{ |
| // This is required to know when to come out of soft reset. |
| // |
| // The first step is to count the number of bursts that remain |
| // outstanding |
| initial writes_outstanding = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| writes_outstanding <= 0; |
| else case({ phantom_write,M_AXI_BVALID && M_AXI_BREADY}) |
| 2'b01: writes_outstanding <= writes_outstanding - 1; |
| 2'b10: writes_outstanding <= writes_outstanding + 1; |
| default: begin end |
| endcase |
| |
| // The second step is to use this counter to determine if we are idle. |
| // If WVALID is ever high, or start_write goes high, then we are |
| // obviously not idle. Otherwise, we become idle when the number of |
| // writes outstanding transitions to (or equals) zero. |
| initial writes_idle = 1; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| writes_idle <= 1; |
| else if (start_write || M_AXI_WVALID) |
| writes_idle <= 0; |
| else |
| writes_idle <= (writes_outstanding |
| == ((M_AXI_BVALID && M_AXI_BREADY) ? 1:0)); |
| // }}} |
| |
| // Count how much space is used in the memory device |
| // {{{ |
| // Well, obviously, we can't fill our memory device or we have problems. |
| // To make sure we don't overflow, we count memory usage here. We'll |
| // count memory usage in units of bursts of (1<<LGMAXBURST) words of |
| // (1<<ADDRLSB) bytes each. So ... here we count the amount of device |
| // memory that hasn't (yet) been committed. This is different from the |
| // memory used (which we don't calculate), or the memory which may yet |
| // be read--which we'll calculate in a moment. |
| initial mem_space_available_w = (1<<BURSTAW); |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || soft_reset) |
| mem_space_available_w <= (1<<BURSTAW); |
| else case({ phantom_write,M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST }) |
| 2'b01: mem_space_available_w <= mem_space_available_w + 1; |
| 2'b10: mem_space_available_w <= mem_space_available_w - 1; |
| default: begin end |
| endcase |
| // }}} |
| |
| // Determining when the read half is idle |
| // {{{ |
| // Count the number of read bursts that we've committed to. This |
| // includes bursts that have ARVALID but haven't been accepted, as well |
| // as any the downstream device will yet return an RLAST for. |
| initial reads_outstanding = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| reads_outstanding <= 0; |
| else case({ phantom_read,M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST}) |
| 2'b01: reads_outstanding <= reads_outstanding - 1; |
| 2'b10: reads_outstanding <= reads_outstanding + 1; |
| default: begin end |
| endcase |
| |
| // Now, using the reads_outstanding counter, we can check whether or not |
| // we are idle (and can exit a reset) of if instead there are more |
| // bursts outstanding to wait for. |
| // |
| // By registering this counter, we can keep the soft_reset release |
| // simpler. At least this way, it doesn't need to check two counters |
| // for zero. |
| initial reads_idle = 1; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| reads_idle <= 1; |
| else if (start_read || M_AXI_ARVALID) |
| reads_idle <= 0; |
| else |
| reads_idle <= (reads_outstanding |
| == ((M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST) ? 1:0)); |
| // }}} |
| |
| // Count how much data is in the memory device that we can read out |
| // {{{ |
| // In AXI, after you issue a write, you can't depend upon that data |
| // being present on the device and available for a read until the |
| // associated BVALID is returned. Therefore we don't count any memory |
| // as available to be read until BVALID comes back. Once a read |
| // command is issued, the memory is again no longer available to be |
| // read. Note also that we are counting bursts here. A second |
| // conversion below converts this count to bytes. |
| initial mem_data_available_w = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || soft_reset) |
| mem_data_available_w <= 0; |
| else case({ M_AXI_BVALID, phantom_read }) |
| 2'b10: mem_data_available_w <= mem_data_available_w + 1; |
| 2'b01: mem_data_available_w <= mem_data_available_w - 1; |
| default: begin end |
| endcase |
| // }}} |
| |
| // |
| // Error detection |
| // {{{ |
| initial o_err = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| o_err <= 1'b0; |
| else begin |
| if (M_AXI_BVALID && M_AXI_BRESP[1]) |
| o_err <= 1'b1; |
| if (M_AXI_RVALID && M_AXI_RRESP[1]) |
| o_err <= 1'b1; |
| end |
| // }}} |
| |
| // |
| // Incoming stream overflow detection |
| // {{{ |
| // The overflow flag is set if ever an incoming value violates the |
| // stream protocol and changes while stalled. Internally, however, |
| // the overflow flag is ignored. It's provided for your information. |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| s_last_stalled <= 0; |
| else |
| s_last_stalled <= S_AXIS_TVALID && !S_AXIS_TREADY; |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXIS_TVALID) |
| s_last_tdata <= S_AXIS_TDATA; |
| |
| initial o_overflow = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || soft_reset) |
| o_overflow <= 0; |
| else if (s_last_stalled) |
| begin |
| if (!S_AXIS_TVALID) |
| o_overflow <= 1; |
| if (S_AXIS_TDATA != s_last_tdata) |
| o_overflow <= 1; |
| end |
| // }}} |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Incoming FIFO |
| // {{{ |
| // Incoming data stream info the FIFO |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| assign S_AXIS_TREADY = !reset_fifo && !ififo_full && !vfifo_full; |
| assign read_from_fifo= (!skd_valid || (M_AXI_WVALID && M_AXI_WREADY)); |
| |
| sfifo #(.BW(C_AXIS_DATA_WIDTH), .LGFLEN(LGFIFO)) |
| ififo(S_AXI_ACLK, reset_fifo, |
| S_AXIS_TVALID && S_AXIS_TREADY, |
| S_AXIS_TDATA, ififo_full, ififo_fill, |
| read_from_fifo, ififo_data, ififo_empty); |
| |
| // |
| // We need a quick 1-element buffer here in order to keep the soft |
| // reset, which resets the FIFO pointer, from adjusting any FIFO data. |
| // {{{ |
| // Here's the rule: we need to fill the buffer before it ever gets |
| // used. Then, once used, it should be able to maintain 100% |
| // throughput. |
| initial skd_valid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (reset_fifo) |
| skd_valid <= 0; |
| else if (!ififo_empty) |
| skd_valid <= 1; |
| else if (M_AXI_WVALID && M_AXI_WREADY) |
| skd_valid <= 0; |
| |
| always @(posedge S_AXI_ACLK) |
| if (!M_AXI_WVALID || M_AXI_WREADY) |
| begin |
| if (!skd_valid || M_AXI_WREADY) |
| skd_data <= ififo_data; |
| end |
| // }}} |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI write processing |
| // {{{ |
| // Write data from our FIFO onto the bus |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // start_write: determining when to issue a write burst |
| // {{{ |
| always @(*) |
| begin |
| start_write = 0; |
| |
| if (ififo_fill >= (1<<LGMAXBURST)) |
| start_write = 1; |
| if (vfifo_full || soft_reset || phantom_write) |
| start_write = 0; |
| if (mem_space_available_w == 0) |
| start_write = 0; |
| |
| if (M_AXI_WVALID && (!M_AXI_WREADY || !M_AXI_WLAST)) |
| start_write = 0; |
| if (M_AXI_AWVALID && !M_AXI_AWREADY) |
| start_write = 0; |
| if (o_err) |
| start_write = 0; |
| end |
| // }}} |
| |
| // Register the start write signal into AWVALID and phantom write |
| // {{{ |
| // phantom_write contains the start signal, but immediately clears |
| // on the next clock cycle. This allows us some time to calculate |
| // the data for the next burst which and if AWVALID remains high and |
| // not yet accepted. |
| initial phantom_write = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| phantom_write <= 0; |
| else |
| phantom_write <= start_write; |
| |
| // Set AWVALID to start_write if every the channel isn't stalled. |
| // Incidentally, start_write is guaranteed to be zero if the channel |
| // is stalled, since that signal is used by other things as well. |
| initial axi_awvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| axi_awvalid <= 0; |
| else if (!M_AXI_AWVALID || M_AXI_AWREADY) |
| axi_awvalid <= start_write; |
| // }}} |
| |
| // Write address |
| // {{{ |
| // We insist on alignment. On every accepted burst, we step forward by |
| // one burst length. On reset, we reset the address at our first |
| // opportunity. |
| initial axi_awaddr = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (M_AXI_AWVALID && M_AXI_AWREADY) |
| axi_awaddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB] |
| <= axi_awaddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB] +1; |
| |
| if ((!M_AXI_AWVALID || M_AXI_AWREADY) && soft_reset) |
| axi_awaddr <= 0; |
| |
| if (!S_AXI_ARESETN) |
| axi_awaddr <= 0; |
| |
| axi_awaddr[LGMAXBURST+ADDRLSB-1:0] <= 0; |
| end |
| // }}} |
| |
| // Write data channel valid |
| // {{{ |
| initial axi_wvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| axi_wvalid <= 0; |
| else if (start_write) |
| axi_wvalid <= 1; |
| else if (!M_AXI_WVALID || M_AXI_WREADY) |
| axi_wvalid <= M_AXI_WVALID && !M_AXI_WLAST; |
| // }}} |
| |
| // WLAST generation |
| // {{{ |
| // On the beginning of any burst, start a counter of the number of items |
| // in it. Once the counter gets to 1, set WLAST. |
| initial writes_pending = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| writes_pending <= 0; |
| else if (start_write) |
| writes_pending <= (1<<LGMAXBURST); |
| else if (M_AXI_WVALID && M_AXI_WREADY) |
| writes_pending <= writes_pending -1; |
| |
| always @(posedge S_AXI_ACLK) |
| if (start_write) |
| axi_wlast <= (LGMAXBURST == 0); |
| else if (!M_AXI_WVALID || M_AXI_WREADY) |
| axi_wlast <= (writes_pending == 1 + (M_AXI_WVALID ? 1:0)); |
| // }}} |
| |
| // Bus assignments based upon the above |
| // {{{ |
| assign M_AXI_AWVALID = axi_awvalid; |
| assign M_AXI_AWID = AXI_WRITE_ID; |
| assign M_AXI_AWADDR = axi_awaddr; |
| assign M_AXI_AWLEN = (1<<LGMAXBURST)-1; |
| assign M_AXI_AWSIZE = ADDRLSB[2:0]; |
| assign M_AXI_AWBURST = 2'b01; |
| assign M_AXI_AWLOCK = 0; |
| assign M_AXI_AWCACHE = 0; |
| assign M_AXI_AWPROT = 0; |
| assign M_AXI_AWQOS = 0; |
| |
| assign M_AXI_WVALID = axi_wvalid; |
| assign M_AXI_WDATA = skd_data; |
| `ifdef AXI3 |
| assign M_AXI_WID = AXI_WRITE_ID; |
| `endif |
| assign M_AXI_WLAST = axi_wlast; |
| assign M_AXI_WSTRB = -1; |
| |
| assign M_AXI_BREADY = 1; |
| // }}} |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI read processing |
| // {{{ |
| // Read data into our FIFO |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // How much FIFO space is available? |
| // {{{ |
| // One we issue a read command, the FIFO space isn't available any more. |
| // That way we can determine when a second read can be issued--even |
| // before the first has returned--while also guaranteeing that there's |
| // always room in the outgoing FIFO for anything that might return. |
| // Remember: NEVER generate backpressure in a bus master |
| initial ofifo_space_available = (1<<LGFIFO); |
| always @(posedge S_AXI_ACLK) |
| if (reset_fifo) |
| ofifo_space_available <= (1<<LGFIFO); |
| else case({phantom_read, M_AXIS_TVALID && M_AXIS_TREADY}) |
| 2'b10: ofifo_space_available <= ofifo_space_available - (1<<LGMAXBURST); |
| 2'b01: ofifo_space_available <= ofifo_space_available + 1; |
| 2'b11: ofifo_space_available <= ofifo_space_available - (1<<LGMAXBURST) + 1; |
| default: begin end |
| endcase |
| // }}} |
| |
| // Determine when to start a next read-from-memory-to-FIFO burst |
| // {{{ |
| always @(*) |
| begin |
| start_read = 1; |
| |
| // We can't read yet if we don't have space available. |
| // Note the comparison is carefully chosen to make certain |
| // it doesn't use all ofifo_space_available bits, but rather |
| // only the number of bits between LGFIFO and |
| // LGMAXBURST--nominally a single bit. |
| if (ofifo_space_available < (1<<LGMAXBURST)) // FIFO space ? |
| start_read = 0; |
| |
| // If there's no memory available for us to read from, then |
| // we can't start a read yet. |
| if (!M_AXI_BVALID && mem_data_available_w == 0) |
| start_read = 0; |
| |
| // Don't start anything while waiting on a reset. Likewise, |
| // insist on a minimum one clock between read burst issuances. |
| if (soft_reset || phantom_read) |
| start_read = 0; |
| |
| // We can't start a read request if the AR* channel is stalled |
| if (M_AXI_ARVALID && !M_AXI_ARREADY) |
| start_read = 0; |
| |
| // Following a bus error, we come to a complete halt. Such a |
| // bus error is an indication that something *SERIOUSLY* went |
| // wrong--perhaps we aren't accessing the memory we are supposed |
| // to. To prevent damage to external devices, we disable |
| // ourselves entirely. There is no fall back. We only |
| // restart on a full bus restart. |
| if (o_err) |
| start_read = 0; |
| end |
| // }}} |
| |
| // Set phantom_read and ARVALID |
| // {{{ |
| initial phantom_read = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| phantom_read <= 0; |
| else |
| phantom_read <= start_read; |
| |
| initial axi_arvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| axi_arvalid <= 0; |
| else if (!M_AXI_ARVALID || M_AXI_ARREADY) |
| axi_arvalid <= start_read; |
| // }}} |
| |
| // Calculate the next ARADDR |
| // {{{ |
| initial axi_araddr = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (M_AXI_ARVALID && M_AXI_ARREADY) |
| axi_araddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB] |
| <= axi_araddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB]+ 1; |
| |
| if ((!M_AXI_ARVALID || M_AXI_ARREADY) && soft_reset) |
| axi_araddr <= 0; |
| |
| if (!S_AXI_ARESETN) |
| axi_araddr <= 0; |
| |
| axi_araddr[LGMAXBURST+ADDRLSB-1:0] <= 0; |
| end |
| // }}} |
| |
| // Assign values to our bus wires |
| // {{{ |
| assign M_AXI_ARVALID = axi_arvalid; |
| assign M_AXI_ARID = AXI_READ_ID; |
| assign M_AXI_ARADDR = axi_araddr; |
| assign M_AXI_ARLEN = (1<<LGMAXBURST)-1; |
| assign M_AXI_ARSIZE = ADDRLSB[2:0]; |
| assign M_AXI_ARBURST = 2'b01; |
| assign M_AXI_ARLOCK = 0; |
| assign M_AXI_ARCACHE = 0; |
| assign M_AXI_ARPROT = 0; |
| assign M_AXI_ARQOS = 0; |
| |
| assign M_AXI_RREADY = 1; |
| // }}} |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Outgoing AXI stream processing |
| // {{{ |
| // Send data out from the MM2S FIFO |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // We basically just stuff the data read from memory back into our |
| // outgoing FIFO here. The logic is quite straightforward. |
| assign write_to_fifo = M_AXI_RVALID && M_AXI_RREADY; |
| assign M_AXIS_TVALID = !ofifo_empty; |
| |
| sfifo #(.BW(C_AXIS_DATA_WIDTH), .LGFLEN(LGFIFO)) |
| ofifo(S_AXI_ACLK, reset_fifo, |
| write_to_fifo, |
| M_AXI_RDATA, ofifo_full, ofifo_fill, |
| M_AXIS_TVALID && M_AXIS_TREADY, M_AXIS_TDATA, ofifo_empty); |
| |
| always @(*) |
| o_mm2s_full = |ofifo_fill[LGFIFO:LGMAXBURST]; |
| // }}} |
| |
| // Keep Verilator happy |
| // {{{ |
| // Verilator lint_off UNUSED |
| wire unused; |
| assign unused = &{ 1'b0, M_AXI_BID, M_AXI_RID, |
| M_AXI_BRESP[0], M_AXI_RRESP[0], |
| ififo_empty, ofifo_full, ofifo_fill |
| // fifo_full, fifo_fill, fifo_empty, |
| }; |
| |
| // Verilator lint_on UNUSED |
| // }}} |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal property section |
| // {{{ |
| // |
| // The following are a subset of the formal properties used to verify this |
| // core. The full set of formal properties, together with the formal |
| // property set itself, are available for purchase. |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| // FAXI_DEPTH controls the width of the counters in the bus property |
| // interface file. In order to support bursts of length 8 (or more), |
| // there's a minimum of 9. Otherwise, we'll just set this to the width |
| // of the AXI address bus. |
| localparam FAXI_DEPTH = (C_AXI_ADDR_WIDTH > 8) |
| ? (C_AXI_ADDR_WIDTH+1) : 9; |
| |
| reg f_past_valid; |
| |
| initial f_past_valid = 0; |
| always @(posedge S_AXI_ACLK) |
| f_past_valid <= 1; |
| |
| // |
| // Wires necessary for interacting with the formal property file |
| // {{{ |
| // ... |
| // }}} |
| |
| // Other registers to keep simplify keeping track of our progress |
| // {{{ |
| reg [C_AXI_ADDR_WIDTH-1:0] faxi_rd_cknext, faxi_wr_cknext, |
| f_read_beat_addr, f_write_beat_addr, |
| faxi_read_beat_addr; |
| reg [C_AXI_ADDR_WIDTH-1:0] f_read_ckbeat_addr; |
| reg [FAXI_DEPTH-1:0] f_rd_bursts_after_check; |
| |
| reg [C_AXI_ADDR_WIDTH:0] f_vfill; |
| reg [C_AXI_ADDR_WIDTH:0] f_space_available, |
| f_data_available; |
| |
| reg [C_AXI_ADDR_WIDTH-1:0] f_read_checksum; |
| reg [C_AXI_ADDR_WIDTH:0] mem_space_available, mem_data_available; |
| // }}} |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // The main AXI data interface bus property check |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| 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-1), |
| .OPT_NARROW_BURST(1'b0), |
| .OPT_ASYNC_RESET(1'b0), // We don't use asynchronous resets |
| .OPT_EXCLUSIVE(1'b0), // We don't use the LOCK signal |
| .F_OPT_ASSUME_RESET(1'b1), // We aren't generating the reset |
| .F_OPT_NO_RESET(1'b1), |
| .F_LGDEPTH(FAXI_DEPTH) // Width of the counters |
| // }}} |
| ) faxi( |
| // {{{ |
| .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), |
| // Write signals |
| // {{{ |
| .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), |
| // }}} |
| // Read signals |
| // {{{ |
| .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), |
| // }}} |
| // Induction signals |
| // {{{ |
| // ... |
| // }}} |
| // }}} |
| ); |
| |
| // Some quick sanity checks |
| // {{{ |
| always @(*) |
| begin |
| // |
| // ... |
| // |
| end |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Write sanity checking |
| // {{{ |
| always @(*) |
| mem_space_available = { mem_space_available_w, |
| {(LGMAXBURST+ADDRLSB){1'b0} } }; |
| |
| // Let's calculate the address of each write beat |
| // {{{ |
| initial f_write_beat_addr = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| f_write_beat_addr <= 0; |
| else if ((!M_AXI_WVALID || (M_AXI_WREADY && M_AXI_WLAST)) && soft_reset) |
| f_write_beat_addr <= 0; |
| else if (M_AXI_WVALID && M_AXI_WREADY) |
| f_write_beat_addr <= f_write_beat_addr + (1<<ADDRLSB); |
| // }}} |
| |
| // |
| // ... |
| // |
| |
| // Verify during any write burst that all the burst parameters are |
| // correct |
| // {{{ |
| // ... |
| // }}} |
| |
| always @(*) |
| if (M_AXI_AWVALID) |
| begin |
| assert(writes_pending == (1<<LGMAXBURST)); |
| // ... |
| end else |
| // ... |
| |
| always @(*) |
| assert(M_AXI_WVALID == (writes_pending != 0)); |
| |
| // |
| // ... |
| // |
| |
| // Check the writes-idle signal |
| // {{{ |
| // ... |
| // }}} |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Read sanity checking |
| // {{{ |
| |
| always @(*) |
| mem_data_available = { mem_data_available_w, |
| {(LGMAXBURST+ADDRLSB){1'b0} } }; |
| // |
| // ... |
| // Check the reads-idle signal |
| // {{{ |
| // ... |
| // }}} |
| |
| // Regenerate the read beat address |
| // {{{ |
| // This works because we are using a single AXI ID for all of our reads. |
| // Therefore we can guarantee that reads will come back in order, thus |
| // we can count the return address here. |
| initial f_read_beat_addr = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| f_read_beat_addr <= 0; |
| else if (soft_reset && reads_idle) |
| f_read_beat_addr <= 0; |
| else if (M_AXI_RVALID && M_AXI_RREADY) |
| f_read_beat_addr <= f_read_beat_addr + (1<<ADDRLSB); |
| // }}} |
| |
| // Read burst checking |
| // {{{ |
| |
| // |
| // ... |
| // |
| |
| // }}} |
| |
| |
| // Match our read beat address to ARADDR |
| // {{{ |
| // ... |
| // }}} |
| |
| // Insist that our burst counters are consistent with bursts of a full |
| // length only |
| // {{{ |
| // ... |
| // }}} |
| |
| // RLAST checking |
| // {{{ |
| // ... |
| // }}} |
| |
| // Match the read beat address to the number of items remaining in this |
| // burst |
| // {{{ |
| // ... |
| // }}} |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Internal assertions (Induction) |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // |
| // On either error, or while waiting for a soft reset to complete |
| // nothing new should issue |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (f_past_valid && ($past(soft_reset) || $past(o_err))) |
| begin |
| assert(!$rose(M_AXI_AWVALID)); |
| assert(!$rose(M_AXI_WVALID)); |
| assert(!$rose(M_AXI_ARVALID)); |
| assert(!phantom_write); |
| assert(!phantom_read); |
| end |
| // }}} |
| |
| // |
| // Writes and reads always have enough room |
| |
| // Bus writes aren't allowed to drain the incoming FIFO dry |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (!soft_reset && M_AXI_WVALID) |
| assert(ififo_fill + (skd_valid ? 1:0) >= writes_pending); |
| // }}} |
| |
| // Bus reads aren't allowed to overflow the return FIFO |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (!soft_reset && M_AXI_RVALID) |
| assert(!ofifo_full); |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Write checks |
| // |
| |
| // Make sure the skid buffer only reads when either there's nothing |
| // held in the buffer, or the write channel has accepted data. Indeed, |
| // the write channel should never be active unless the skid buffer is |
| // full. |
| // {{{ |
| always @(*) |
| if (!soft_reset && !skd_valid) |
| assert(!M_AXI_WVALID); |
| |
| always @(*) |
| if (M_AXI_WVALID && M_AXI_WREADY) |
| assert(read_from_fifo); |
| else if (!skd_valid && !ififo_empty) |
| assert(read_from_fifo); |
| // }}} |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Read checks |
| // {{{ |
| |
| // No read checks in addition to the ones above |
| |
| // }}} |
| |
| //////////////////////////////////////// |
| // |
| // Errors or resets -- do we properly end gracefully |
| // |
| // {{{ |
| // Set o_err on any bus error. Only clear it on reset |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (f_past_valid && $past(S_AXI_ARESETN)) |
| begin |
| if ($past(M_AXI_BVALID && M_AXI_BRESP[1])) |
| assert(o_err); |
| if ($past(M_AXI_RVALID && M_AXI_RRESP[1])) |
| assert(o_err); |
| if ($past(!M_AXI_BVALID || !M_AXI_BRESP[1]) |
| && $past(!M_AXI_RVALID || !M_AXI_RRESP[1])) |
| assert(!$rose(o_err)); |
| end |
| |
| // Only release soft_reset once the bus is idle |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (f_past_valid && $past(S_AXI_ARESETN) && $fell(soft_reset)) |
| begin |
| // |
| // ... |
| // |
| assert(!M_AXI_AWVALID); |
| assert(!M_AXI_WVALID); |
| assert(!M_AXI_ARVALID); |
| end |
| // }}} |
| // }}} |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // FIFO checks |
| // {{{ |
| |
| // Check the global fill/emtpy values |
| // {{{ |
| always @(*) |
| assert(vfifo_full == (vfifo_fill == (1<<(C_AXI_ADDR_WIDTH-ADDRLSB)))); |
| |
| always @(*) |
| assert(vfifo_fill <= (1<<(C_AXI_ADDR_WIDTH-ADDRLSB))); |
| |
| always @(*) |
| assert(vfifo_empty == (vfifo_fill == 0)); |
| // }}} |
| |
| // An equation for vfill based upon our property checker's counters |
| // {{{ |
| always @(*) |
| begin |
| f_vfill = M_AXI_AWADDR - M_AXI_ARADDR; |
| f_vfill[C_AXI_ADDR_WIDTH] = 0; |
| if (!M_AXI_AWVALID) |
| f_vfill = f_vfill - (writes_pending << ADDRLSB); |
| // ... |
| if (skd_valid) |
| f_vfill = f_vfill + (1<<ADDRLSB); |
| f_vfill = f_vfill + ((ififo_fill + ofifo_fill)<<ADDRLSB); |
| end |
| // }}} |
| |
| // Make sure the virtual FIFO's fill matches that counter |
| // {{{ |
| always @(*) |
| if (!soft_reset) |
| begin |
| assert(vfifo_fill == (f_vfill >> ADDRLSB)); |
| assert(f_vfill <= (1<<(C_AXI_ADDR_WIDTH))); |
| |
| // Before the equation check, double check that we |
| // don't overflow any of our arithmetic. Then check our |
| // virtual FIFO's fill counter against the various internal |
| // FIFO fills and read counters. |
| |
| // These are just inequality checks, however, so we'll still |
| // need a full equation check elsewhere |
| // |
| // ... |
| // |
| end |
| |
| // Make certain we aren't overflowing in our subtraction above |
| always @(*) |
| if (M_AXI_ARVALID && !soft_reset) |
| assert(M_AXI_ARADDR != M_AXI_AWADDR); |
| // }}} |
| |
| // Check mem_space_available |
| // {{{ |
| always @(*) |
| begin |
| f_space_available = (M_AXI_AWADDR - M_AXI_ARADDR); |
| f_space_available[C_AXI_ADDR_WIDTH] = 0; |
| f_space_available = (1<<C_AXI_ADDR_WIDTH) - f_space_available; |
| if (M_AXI_AWVALID && !phantom_write) |
| f_space_available = f_space_available |
| - (1 << (LGMAXBURST+ADDRLSB)); |
| // |
| // ... |
| end |
| |
| always @(*) |
| begin |
| assert({ mem_data_available_w, {(LGMAXBURST){1'b0}} } |
| <= vfifo_fill); |
| // ... |
| assert(mem_data_available <= (1<<C_AXI_ADDR_WIDTH)); |
| assert(mem_space_available <= (1<<C_AXI_ADDR_WIDTH)); |
| if (!soft_reset) |
| begin |
| assert(mem_space_available == f_space_available); |
| |
| if (mem_space_available[C_AXI_ADDR_WIDTH]) |
| begin |
| assert(M_AXI_ARADDR == M_AXI_AWADDR); |
| assert(!M_AXI_AWVALID || phantom_write); |
| // ... |
| end |
| end |
| end |
| // }}} |
| |
| // Check mem_data_available |
| // {{{ |
| // First, generate an equation to describe it |
| always @(*) |
| begin |
| f_data_available = M_AXI_AWADDR - M_AXI_ARADDR; |
| f_data_available[C_AXI_ADDR_WIDTH] = 0; |
| // ... |
| if (M_AXI_ARVALID && !phantom_read) |
| f_data_available = f_data_available |
| - (1 << (ADDRLSB + LGMAXBURST)); |
| end |
| |
| // Then compare it against that equation |
| always @(*) |
| if (!soft_reset) |
| begin |
| assert(mem_data_available == f_data_available); |
| if (mem_data_available[C_AXI_ADDR_WIDTH]) |
| begin |
| assert(vfifo_fill[C_AXI_ADDR_WIDTH]); |
| assert(ofifo_empty); |
| end |
| end |
| // }}} |
| |
| // ofifo_space_available |
| // {{{ |
| always @(*) |
| if (!reset_fifo) |
| begin |
| // ... |
| |
| // Make sure we don't overflow above |
| assert(ofifo_space_available <= (1<<LGFIFO)); |
| end |
| // }}} |
| |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Initial (only) constraints |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| always @(posedge S_AXI_ACLK) |
| if (!f_past_valid || $past(!S_AXI_ARESETN)) |
| begin |
| assert(!M_AXI_AWVALID); |
| assert(!M_AXI_WVALID); |
| assert(!M_AXI_ARVALID); |
| |
| assert(mem_space_available == (1<<C_AXI_ADDR_WIDTH)); |
| assert(mem_data_available == 0); |
| |
| assert(!phantom_read); |
| assert(!phantom_write); |
| |
| assert(vfifo_fill == 0); |
| end |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Formal contract checking |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // This core doesn't (yet) have any formal contract check |
| |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| reg [2:0] cvr_write_bursts, cvr_read_bursts; |
| (* anyconst *) reg cvr_high_speed; |
| |
| always @(posedge S_AXI_ACLK) |
| if (cvr_high_speed) |
| begin |
| assume(!$fell(S_AXIS_TVALID)); |
| // if (S_AXI_ARESETN && $past(S_AXIS_TVALID && !S_AXIS_TREADY)) |
| // assume(S_AXIS_TVALID && $stable(S_AXIS_TDATA)); |
| |
| assume(M_AXI_AWREADY || writes_pending > 0); |
| assume(M_AXIS_TREADY); |
| assume(M_AXI_WREADY); |
| assume(M_AXI_ARREADY); |
| end |
| |
| initial cvr_write_bursts = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || soft_reset || o_err || o_overflow) |
| cvr_write_bursts <= 0; |
| else if (M_AXI_BVALID && !cvr_write_bursts[2]) |
| cvr_write_bursts <= cvr_write_bursts + 1; |
| |
| initial cvr_read_bursts = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || soft_reset || o_err || o_overflow) |
| cvr_read_bursts <= 0; |
| else if (M_AXI_RVALID && M_AXI_RLAST && !cvr_read_bursts[2]) |
| cvr_read_bursts <= cvr_read_bursts + 1; |
| |
| // |
| // ... |
| // |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && !soft_reset) |
| cover(cvr_read_bursts > 1 && cvr_write_bursts > 1); |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && !soft_reset) |
| cover(cvr_read_bursts > 1 && cvr_write_bursts > 1 |
| && cvr_high_speed); |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Careless assumptions (i.e. constraints) |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // No careless assumptions. Indeed, no assumptions at all beyond |
| // what's in the bus property file, and some optional cover assumptions. |
| |
| // }}} |
| // }}} |
| `endif |
| endmodule |