| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: axisafety.v |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: Given that 1) AXI interfaces can be difficult to write and to |
| // get right, 2) my experiences with the AXI infrastructure of an |
| // ARM+FPGA is that the device needs a power cycle following a bus fault, |
| // and given that I've now found multiple interfaces that had some bug |
| // or other within them, the following is a bus fault isolator. It acts |
| // as a bump in the log between the interconnect and the user core. As |
| // such, it has two interfaces: The first is the slave interface, |
| // coming from the interconnect. The second interface is the master |
| // interface, proceeding to a slave that might be faulty. |
| // |
| // INTERCONNECT --> (S) AXISAFETY (M) --> POTENTIALLY FAULTY CORE |
| // |
| // The slave interface has been formally verified to be a valid AXI |
| // slave, independent of whatever the potentially faulty core might do. |
| // If the user core (i.e. the potentially faulty one) responds validly |
| // to the requests of a master, then this core will turn into a simple |
| // delay on the bus. If, on the other hand, the user core suffers from |
| // a protocol error, then this core will set one of two output |
| // flags--either o_write_fault or o_read_fault indicating whether a write |
| // or a read fault was detected. Further attempts to access the user |
| // core will result in bus errors, generated by the AXISAFETY core. |
| // |
| // Assuming the bus master can properly detect and deal with a bus error, |
| // this should then make it possible to properly recover from a bus |
| // protocol error without later needing to cycle power. |
| // |
| // The core does have a couple of limitations. For example, it can only |
| // handle one burst transaction, and one ID at a time. This matches the |
| // performances of Xilinx's example AXI full core, from which many user |
| // cores have have been copied/modified from. Therefore, there will be |
| // no performance loss for such a core. |
| // |
| // Because of this, it is still possible that the user core might have an |
| // undetected fault when using this core. For example, if the interconnect |
| // issues more than one bus request before receiving the response from the |
| // first request, this safety core will stall the second request, |
| // preventing the downstream core from seeing this second request. If the |
| // downstream core would suffer from an error while handling the second |
| // request, by preventing the user core from seeing the second request this |
| // core eliminates that potential for error. |
| // |
| // Usage: The important part of using this core is to connect the slave |
| // side to the interconnect, and the master side to the user core. |
| // |
| // Some options are available: |
| // |
| // 1) C_S_AXI_ADDR_WIDTH The number of address bits in the AXI channel |
| // 1) C_S_AXI_DATA_WIDTH The number of data bits in the AXI channel |
| // 3) C_S_AXI_ID_WIDTH The number of bits in an AXI ID. As currently |
| // written, this number cannot be zero. You can, however, set it |
| // to '1' and connect all of the relevant ID inputs to zero. |
| // |
| // These three parameters have currently been abbreviated with AW, DW, and |
| // IW. I anticipate returning them to their original meanings, I just |
| // haven't done so (yet). |
| // |
| // 4) OPT_TIMEOUT This is the number of clock periods, from |
| // interconnect request to interconnect response, that the |
| // slave needs to respond within. (The actual timeout from the |
| // user slave's perspective will be shorter than this.) |
| // |
| // This timeout is part of the check that a slave core will |
| // always return a response. From the standpoint of this core, |
| // it can be set arbitrarily large. (From the standpoint of |
| // formal verification, it needs to be kept short ...) |
| // Feel free to set this even as large as 1ms if you would like. |
| // |
| // 5) OPT_SELF_RESET If set, will send a reset signal to the slave |
| // following any write or read fault. This will cause the other |
| // side of the link (write or read) to fault as well. Once the |
| // channel then becomes inactive, the slave will be released from |
| // reset and will be able to interact with the rest of the bus |
| // again. |
| // |
| // Performance: As mentioned above, this core can handle one read burst and one |
| // write burst at a time, no more. Further, the core will delay |
| // an input path by one clock and the output path by another clock, so that |
| // the latency involved with using this core is a minimum of two extra |
| // clocks beyond the latency user slave core. |
| // |
| // Maximum write latency: N+3 clocks for a burst of N values |
| // Maximum read latency: N+3 clocks for a burst of N values |
| // |
| // Faults detected: |
| // |
| // Write channel: |
| // 1. Raising BVALID prior to the last write value being sent |
| // to the user/slave core. |
| // 2. Raising BVALID prior to accepting the write address |
| // 3. A BID return ID that doesn't match the request AWID |
| // 4. Sending too many returns, such as not dropping BVALID |
| // or raising it when there is no outstanding write |
| // request |
| // |
| // While the following technically isn't a violation of the |
| // AXI protocol, it is treated as such by this fault isolator. |
| // |
| // 5. Accepting write data prior to the write address |
| // |
| // The fault isolator will guarantee that AWVALID is raised before |
| // WVALID, so this shouldn't be a problem. |
| // |
| // Read channel: |
| // |
| // 1. Raising RVALID before accepting the read address, ARVALID |
| // 2. A return ID that doesn't match the ID that was sent. |
| // 3. Raising RVALID after the last return value, and so returning |
| // too many response values |
| // 4. Setting the RLAST value on anything but the last value from |
| // the bus. |
| // |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // Copyright (C) 2019-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 |
| // }}} |
| module axisafety #( |
| // {{{ |
| parameter C_S_AXI_ID_WIDTH = 1, |
| parameter C_S_AXI_DATA_WIDTH = 32, |
| parameter C_S_AXI_ADDR_WIDTH = 16, |
| parameter [0:0] OPT_SELF_RESET = 0, |
| // |
| // I use the following abbreviations, IW, DW, and AW, to simplify |
| // the code below (and to help it fit within an 80 col terminal) |
| localparam IW = C_S_AXI_ID_WIDTH, |
| localparam DW = C_S_AXI_DATA_WIDTH, |
| localparam AW = C_S_AXI_ADDR_WIDTH, |
| // |
| // OPT_TIMEOUT references the number of clock cycles to wait |
| // between raising the *VALID signal and when the respective |
| // *VALID return signal must be high. You might wish to set this |
| // to a very high number, to allow your core to work its magic. |
| parameter OPT_TIMEOUT = 20 |
| // }}} |
| ) ( |
| // {{{ |
| output reg o_read_fault, |
| output reg o_write_fault, |
| // User ports ends |
| // Do not modify the ports beyond this line |
| |
| // Global Clock Signal |
| input wire S_AXI_ACLK, |
| // Global Reset Signal. This Signal is Active LOW |
| input wire S_AXI_ARESETN, |
| output reg M_AXI_ARESETN, |
| // |
| // The input side. This is where slave requests come into |
| // the core. |
| // {{{ |
| // |
| // Write address |
| input wire [IW-1 : 0] S_AXI_AWID, |
| input wire [AW-1 : 0] S_AXI_AWADDR, |
| input wire [7 : 0] S_AXI_AWLEN, |
| input wire [2 : 0] S_AXI_AWSIZE, |
| input wire [1 : 0] S_AXI_AWBURST, |
| input wire S_AXI_AWLOCK, |
| input wire [3 : 0] S_AXI_AWCACHE, |
| input wire [2 : 0] S_AXI_AWPROT, |
| input wire [3 : 0] S_AXI_AWQOS, |
| input wire S_AXI_AWVALID, |
| output reg S_AXI_AWREADY, |
| // Write data |
| input wire [DW-1 : 0] S_AXI_WDATA, |
| input wire [(DW/8)-1 : 0] S_AXI_WSTRB, |
| input wire S_AXI_WLAST, |
| input wire S_AXI_WVALID, |
| output reg S_AXI_WREADY, |
| // Write return |
| output reg [IW-1 : 0] S_AXI_BID, |
| output reg [1 : 0] S_AXI_BRESP, |
| output reg S_AXI_BVALID, |
| input wire S_AXI_BREADY, |
| // Read address |
| input wire [IW-1 : 0] S_AXI_ARID, |
| input wire [AW-1 : 0] S_AXI_ARADDR, |
| input wire [7 : 0] S_AXI_ARLEN, |
| input wire [2 : 0] S_AXI_ARSIZE, |
| input wire [1 : 0] S_AXI_ARBURST, |
| input wire S_AXI_ARLOCK, |
| input wire [3 : 0] S_AXI_ARCACHE, |
| input wire [2 : 0] S_AXI_ARPROT, |
| input wire [3 : 0] S_AXI_ARQOS, |
| input wire S_AXI_ARVALID, |
| output reg S_AXI_ARREADY, |
| // Read data |
| output reg [IW-1 : 0] S_AXI_RID, |
| output reg [DW-1 : 0] S_AXI_RDATA, |
| output reg [1 : 0] S_AXI_RRESP, |
| output reg S_AXI_RLAST, |
| output reg S_AXI_RVALID, |
| input wire S_AXI_RREADY, |
| // }}} |
| // |
| // The output side, where slave requests are forwarded to the |
| // actual slave |
| // {{{ |
| // Write address |
| // {{{ |
| output reg [IW-1 : 0] M_AXI_AWID, |
| output reg [AW-1 : 0] M_AXI_AWADDR, |
| output reg [7 : 0] M_AXI_AWLEN, |
| 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_AWVALID, |
| input wire M_AXI_AWREADY, |
| // Write data |
| output reg [DW-1 : 0] M_AXI_WDATA, |
| output reg [(DW/8)-1 : 0] M_AXI_WSTRB, |
| output reg M_AXI_WLAST, |
| output reg M_AXI_WVALID, |
| input wire M_AXI_WREADY, |
| // Write return |
| input wire [IW-1 : 0] M_AXI_BID, |
| input wire [1 : 0] M_AXI_BRESP, |
| input wire M_AXI_BVALID, |
| output wire M_AXI_BREADY, |
| // }}} |
| // Read address |
| // {{{ |
| output reg [IW-1 : 0] M_AXI_ARID, |
| output reg [AW-1 : 0] M_AXI_ARADDR, |
| output reg [7 : 0] M_AXI_ARLEN, |
| output reg [2 : 0] M_AXI_ARSIZE, |
| output reg [1 : 0] M_AXI_ARBURST, |
| output reg M_AXI_ARLOCK, |
| output reg [3 : 0] M_AXI_ARCACHE, |
| output reg [2 : 0] M_AXI_ARPROT, |
| output reg [3 : 0] M_AXI_ARQOS, |
| output reg M_AXI_ARVALID, |
| input wire M_AXI_ARREADY, |
| // Read data |
| input wire [IW-1 : 0] M_AXI_RID, |
| input wire [DW-1 : 0] M_AXI_RDATA, |
| input wire [1 : 0] M_AXI_RRESP, |
| input wire M_AXI_RLAST, |
| input wire M_AXI_RVALID, |
| output wire M_AXI_RREADY |
| // }}} |
| // }}} |
| // }}} |
| ); |
| |
| localparam LGTIMEOUT = $clog2(OPT_TIMEOUT+1); |
| localparam LSB = $clog2(DW)-3; |
| localparam EXOKAY = 2'b01; |
| localparam SLAVE_ERROR = 2'b10; |
| // |
| // |
| // Register declarations |
| // {{{ |
| reg faulty_write_return, faulty_read_return; |
| reg clear_fault; |
| // |
| // Timer/timeout variables |
| reg [LGTIMEOUT-1:0] write_timer, read_timer; |
| reg write_timeout, read_timeout; |
| |
| // |
| // Double buffer the write address channel |
| reg r_awvalid, m_awvalid; |
| reg [IW-1:0] r_awid, m_awid; |
| reg [AW-1:0] r_awaddr, m_awaddr; |
| reg [7:0] r_awlen, m_awlen; |
| reg [2:0] r_awsize, m_awsize; |
| reg [1:0] r_awburst, m_awburst; |
| reg r_awlock, m_awlock; |
| reg [3:0] r_awcache, m_awcache; |
| reg [2:0] r_awprot, m_awprot; |
| reg [3:0] r_awqos, m_awqos; |
| |
| // |
| // Double buffer for the write channel |
| reg r_wvalid,m_wvalid; |
| reg [DW-1:0] r_wdata, m_wdata; |
| reg [DW/8-1:0] r_wstrb, m_wstrb; |
| reg r_wlast, m_wlast; |
| |
| // |
| // Double buffer the write response channel |
| reg m_bvalid; // r_bvalid == 0 |
| reg [IW-1:0] m_bid; |
| reg [1:0] m_bresp; |
| |
| // |
| // Double buffer the read address channel |
| reg r_arvalid, m_arvalid; |
| reg [IW-1:0] r_arid, m_arid; |
| reg [AW-1:0] r_araddr, m_araddr; |
| reg [7:0] r_arlen, m_arlen; |
| reg [2:0] r_arsize, m_arsize; |
| reg [1:0] r_arburst, m_arburst; |
| reg r_arlock, m_arlock; |
| reg [3:0] r_arcache, m_arcache; |
| reg [2:0] r_arprot, m_arprot; |
| reg [3:0] r_arqos, m_arqos; |
| |
| // |
| // Double buffer the read data response channel |
| reg r_rvalid,m_rvalid; |
| reg [IW-1:0] m_rid; |
| reg [1:0] r_rresp, m_rresp; |
| reg m_rlast; |
| reg [DW-1:0] r_rdata, m_rdata; |
| |
| // |
| // Write FIFO data |
| reg [IW-1:0] wfifo_id; |
| reg wfifo_lock; |
| |
| // |
| // Read FIFO data |
| reg [IW-1:0] rfifo_id; |
| reg rfifo_lock; |
| reg [8:0] rfifo_counter; |
| reg rfifo_empty, rfifo_last, rfifo_penultimate; |
| |
| // |
| // |
| reg [0:0] s_wbursts; |
| reg [8:0] m_wpending; |
| reg m_wempty, m_wlastctr; |
| reg waddr_valid, raddr_valid; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Write channel processing |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Write address processing |
| // {{{ |
| // S_AXI_AWREADY |
| // {{{ |
| initial S_AXI_AWREADY = (OPT_SELF_RESET) ? 0:1; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_AWREADY <= !OPT_SELF_RESET; |
| else if (S_AXI_AWVALID && S_AXI_AWREADY) |
| S_AXI_AWREADY <= 0; |
| else if (clear_fault) |
| S_AXI_AWREADY <= 1; |
| else if (!S_AXI_AWREADY) |
| S_AXI_AWREADY <= !S_AXI_AWREADY && S_AXI_BVALID && S_AXI_BREADY; |
| // }}} |
| |
| // waddr_valid |
| // {{{ |
| generate if (OPT_SELF_RESET) |
| begin |
| initial waddr_valid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| waddr_valid <= 0; |
| else if (S_AXI_AWVALID && S_AXI_AWREADY) |
| waddr_valid <= 1; |
| else if (waddr_valid) |
| waddr_valid <= !S_AXI_BVALID || !S_AXI_BREADY; |
| end else begin |
| always @(*) |
| waddr_valid = !S_AXI_AWREADY; |
| end endgenerate |
| // }}} |
| |
| // r_aw* |
| // {{{ |
| // Double buffer for the AW* channel |
| // |
| initial r_awvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (S_AXI_AWVALID && S_AXI_AWREADY) |
| begin |
| r_awvalid <= 1'b0; |
| r_awid <= S_AXI_AWID; |
| r_awaddr <= S_AXI_AWADDR; |
| r_awlen <= S_AXI_AWLEN; |
| r_awsize <= S_AXI_AWSIZE; |
| r_awburst <= S_AXI_AWBURST; |
| r_awlock <= S_AXI_AWLOCK; |
| r_awcache <= S_AXI_AWCACHE; |
| r_awprot <= S_AXI_AWPROT; |
| r_awqos <= S_AXI_AWQOS; |
| end else if (M_AXI_AWREADY) |
| r_awvalid <= 0; |
| |
| if (!S_AXI_ARESETN) |
| r_awvalid <= 0; |
| end |
| // }}} |
| |
| // m_aw* |
| // {{{ |
| // Second half of the AW* double-buffer. The m_* terms reference |
| // either the value in the double buffer (assuming one is in there), |
| // or the incoming value (if the double buffer is empty) |
| // |
| always @(*) |
| if (r_awvalid) |
| begin |
| m_awvalid = r_awvalid; |
| m_awid = r_awid; |
| m_awaddr = r_awaddr; |
| m_awlen = r_awlen; |
| m_awsize = r_awsize; |
| m_awburst = r_awburst; |
| m_awlock = r_awlock; |
| m_awcache = r_awcache; |
| m_awprot = r_awprot; |
| m_awqos = r_awqos; |
| end else begin |
| m_awvalid = S_AXI_AWVALID && S_AXI_AWREADY; |
| m_awid = S_AXI_AWID; |
| m_awaddr = S_AXI_AWADDR; |
| m_awlen = S_AXI_AWLEN; |
| m_awsize = S_AXI_AWSIZE; |
| m_awburst = S_AXI_AWBURST; |
| m_awlock = S_AXI_AWLOCK; |
| m_awcache = S_AXI_AWCACHE; |
| m_awprot = S_AXI_AWPROT; |
| m_awqos = S_AXI_AWQOS; |
| end |
| // }}} |
| |
| // M_AXI_AW* |
| // {{{ |
| // Set the output AW* channel outputs--but only on no fault |
| // |
| initial M_AXI_AWVALID = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (!M_AXI_AWVALID || M_AXI_AWREADY) |
| begin |
| |
| if (o_write_fault) |
| M_AXI_AWVALID <= 0; |
| else |
| M_AXI_AWVALID <= m_awvalid; |
| |
| M_AXI_AWID <= m_awid; |
| M_AXI_AWADDR <= m_awaddr; |
| M_AXI_AWLEN <= m_awlen; |
| M_AXI_AWSIZE <= m_awsize; |
| M_AXI_AWBURST <= m_awburst; |
| M_AXI_AWLOCK <= m_awlock; |
| M_AXI_AWCACHE <= m_awcache; |
| M_AXI_AWPROT <= m_awprot; |
| M_AXI_AWQOS <= m_awqos; |
| end |
| |
| if (!M_AXI_ARESETN) |
| M_AXI_AWVALID <= 0; |
| end |
| // }}} |
| // }}} |
| |
| // s_wbursts |
| // {{{ |
| // Count write bursts outstanding from the standpoint of |
| // the incoming (slave) channel |
| // |
| // Notice that, as currently built, the count can only ever be one |
| // or zero. |
| // |
| // We'll use this count in a moment to determine if a response |
| // has taken too long, or if a response is returned when there's |
| // no outstanding request |
| initial s_wbursts = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| s_wbursts <= 0; |
| else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST) |
| s_wbursts <= 1; |
| else if (S_AXI_BVALID && S_AXI_BREADY) |
| s_wbursts <= 0; |
| // }}} |
| |
| // wfifo_id, wfifo_lock |
| // {{{ |
| // Keep track of the ID of the last transaction. Since we only |
| // ever have one write transaction outstanding, this will need to be |
| // the ID of the returned value. |
| // |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_AWREADY && S_AXI_AWVALID) |
| begin |
| // {{{ |
| wfifo_id <= S_AXI_AWID; |
| wfifo_lock <= S_AXI_AWLOCK; |
| // }}} |
| end |
| // }}} |
| |
| // m_wpending, m_wempty, m_wlastctr |
| // {{{ |
| // m_wpending counts the number of (remaining) write data values that |
| // need to be sent to the slave. It counts this number with respect |
| // to the *SLAVE*, not the master. When m_wpending == 1, WLAST shall |
| // be true. To make comparisons of (m_wpending == 0) or (m_wpending>0), |
| // m_wempty is assigned to (m_wpending). Similarly, m_wlastctr is |
| // assigned to (m_wpending == 1). |
| // |
| initial m_wpending = 0; |
| initial m_wempty = 1; |
| initial m_wlastctr = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || o_write_fault) |
| begin |
| // {{{ |
| m_wpending <= 0; |
| m_wempty <= 1; |
| m_wlastctr <= 0; |
| // }}} |
| end else if (M_AXI_AWVALID && M_AXI_AWREADY) |
| begin |
| // {{{ |
| if (M_AXI_WVALID && M_AXI_WREADY) |
| begin |
| // {{{ |
| // Accepting AW* and W* packets on the same |
| // clock |
| if (m_wpending == 0) |
| begin |
| // The AW* and W* packets go together |
| m_wpending <= {1'b0, M_AXI_AWLEN}; |
| m_wempty <= (M_AXI_AWLEN == 0); |
| m_wlastctr <= (M_AXI_AWLEN == 1); |
| end else begin |
| // The W* packet goes with the last |
| // AW* command, the AW* packet with a |
| // new one |
| m_wpending <= M_AXI_AWLEN+1; |
| m_wempty <= 0; |
| m_wlastctr <= (M_AXI_AWLEN == 0); |
| end |
| // }}} |
| end else begin |
| // {{{ |
| m_wpending <= M_AXI_AWLEN+1; |
| m_wempty <= 0; |
| m_wlastctr <= (M_AXI_AWLEN == 0); |
| // }}} |
| end |
| // }}} |
| end else if (M_AXI_WVALID && M_AXI_WREADY && (!m_wempty)) |
| begin |
| // {{{ |
| // The AW* channel is idle, and we just accepted a value |
| // on the W* channel |
| m_wpending <= m_wpending - 1; |
| m_wempty <= (m_wpending <= 1); |
| m_wlastctr <= (m_wpending == 2); |
| // }}} |
| end |
| // }}} |
| |
| // Write data processing |
| // {{{ |
| // S_AXI_WREADY |
| // {{{ |
| // The S_AXI_WREADY or write channel stall signal |
| // |
| // For this core, we idle at zero (stalled) until an AW* packet |
| // comes through |
| // |
| initial S_AXI_WREADY = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_WREADY <= 0; |
| else if (S_AXI_WVALID && S_AXI_WREADY) |
| begin |
| // {{{ |
| if (S_AXI_WLAST) |
| S_AXI_WREADY <= 0; |
| else if (o_write_fault) |
| S_AXI_WREADY <= 1; |
| else if (!M_AXI_WVALID || M_AXI_WREADY) |
| S_AXI_WREADY <= 1; |
| else |
| S_AXI_WREADY <= 0; |
| // }}} |
| end else if ((s_wbursts == 0)&&(waddr_valid) |
| &&(o_write_fault || M_AXI_WREADY)) |
| S_AXI_WREADY <= 1; |
| else if (S_AXI_AWVALID && S_AXI_AWREADY) |
| S_AXI_WREADY <= 1; |
| // }}} |
| |
| // r_w* |
| // {{{ |
| // Double buffer for the write channel |
| // |
| // As before, the r_* values contain the values in the double |
| // buffer itself |
| // |
| initial r_wvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| r_wvalid <= 0; |
| else if (!r_wvalid) |
| begin |
| // {{{ |
| r_wvalid <= (S_AXI_WVALID && S_AXI_WREADY |
| && M_AXI_WVALID && !M_AXI_WREADY); |
| r_wdata <= S_AXI_WDATA; |
| r_wstrb <= S_AXI_WSTRB; |
| r_wlast <= S_AXI_WLAST; |
| // }}} |
| end else if (o_write_fault || M_AXI_WREADY || !M_AXI_ARESETN) |
| r_wvalid <= 0; |
| // }}} |
| |
| // m_w* |
| // {{{ |
| // Here's the result of our double buffer |
| // |
| // m_* references the value within the double buffer in the case that |
| // something is in the double buffer. Otherwise, it is the values |
| // directly from the inputs. In the case of a fault, neither is true. |
| // Write faults override. |
| // |
| always @(*) |
| if (o_write_fault) |
| begin |
| // {{{ |
| m_wvalid = !m_wempty; |
| m_wlast = m_wlastctr; |
| m_wstrb = 0; |
| // }}} |
| end else if (r_wvalid) |
| begin |
| // {{{ |
| m_wvalid = 1; |
| m_wstrb = r_wstrb; |
| m_wlast = r_wlast; |
| // }}} |
| end else begin |
| // {{{ |
| m_wvalid = S_AXI_WVALID && S_AXI_WREADY; |
| m_wstrb = S_AXI_WSTRB; |
| m_wlast = S_AXI_WLAST; |
| // }}} |
| end |
| // }}} |
| |
| // m_wdata |
| // {{{ |
| // The logic for the DATA output of the double buffer doesn't |
| // matter so much in the case of o_write_fault |
| always @(*) |
| if (r_wvalid) |
| m_wdata = r_wdata; |
| else |
| m_wdata = S_AXI_WDATA; |
| // }}} |
| |
| // M_AXI_W* |
| // {{{ |
| // Set the downstream write channel values |
| // |
| // As per AXI spec, these values *must* be registered. Note that our |
| // source here is the m_* double buffer/incoming write data switch. |
| initial M_AXI_WVALID = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (!M_AXI_WVALID || M_AXI_WREADY) |
| begin |
| M_AXI_WVALID <= m_wvalid; |
| M_AXI_WDATA <= m_wdata; |
| M_AXI_WSTRB <= m_wstrb; |
| M_AXI_WLAST <= m_wlast; |
| end |
| |
| // Override the WVALID signal (only) on reset, voiding any |
| // output we might otherwise send. |
| if (!M_AXI_ARESETN) |
| M_AXI_WVALID <= 0; |
| end |
| // }}} |
| // }}} |
| |
| // Write fault detection |
| // {{{ |
| // write_timer |
| // {{{ |
| // The write timer |
| // |
| // The counter counts up to saturation. It is reset any time |
| // the write channel is either clear, or a value is accepted |
| // at the *MASTER* (not slave) side. Why the master side? Simply |
| // because it makes the proof below easier. (At one time I checked |
| // both, but then couldn't prove that the faults wouldn't get hit |
| // if the slave responded in time.) |
| initial write_timer = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || !waddr_valid) |
| write_timer <= 0; |
| else if (!o_write_fault && M_AXI_BVALID) |
| write_timer <= 0; |
| else if (S_AXI_WREADY) |
| write_timer <= 0; |
| else if (!(&write_timer)) |
| write_timer <= write_timer + 1; |
| // }}} |
| |
| // write_timeout |
| // {{{ |
| // Write timeout detector |
| // |
| // If the write_timer reaches the OPT_TIMEOUT, then the write_timeout |
| // will get set true. This will force a fault, taking the write |
| // channel off line. |
| initial write_timeout = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || clear_fault) |
| write_timeout <= 0; |
| else if (M_AXI_BVALID) |
| write_timeout <= write_timeout; |
| else if (S_AXI_WVALID && S_AXI_WREADY) |
| write_timeout <= write_timeout; |
| else if (write_timer >= OPT_TIMEOUT) |
| write_timeout <= 1; |
| // }}} |
| |
| // faulty_write_return |
| // {{{ |
| // fault_write_return |
| // |
| // This combinational logic is used to catch an invalid return, and |
| // so take the slave off-line before the return can corrupt the master |
| // channel. Reasons for taking the write return off line are listed |
| // below. |
| always @(*) |
| begin |
| faulty_write_return = 0; |
| if (M_AXI_WVALID && M_AXI_WREADY |
| && M_AXI_AWVALID && !M_AXI_AWREADY) |
| // Accepting the write *data* prior to the write |
| // *address* is a fault |
| faulty_write_return = 1; |
| if (M_AXI_BVALID) |
| begin |
| if (M_AXI_AWVALID || M_AXI_WVALID) |
| // Returning a B* acknowledgement while the |
| // request remains outstanding is also a fault |
| faulty_write_return = 1; |
| if (!m_wempty) |
| // Same as above, but this time the write |
| // channel is neither complete, nor is *WVALID |
| // active. Values remain to be written, |
| // and so a return is a fault. |
| faulty_write_return = 1; |
| if (s_wbursts <= (S_AXI_BVALID ? 1:0)) |
| // Too many acknowledgments |
| // |
| // Returning more than one BVALID&BREADY for |
| // every AWVALID & AWREADY is a fault. |
| faulty_write_return = 1; |
| if (M_AXI_BID != wfifo_id) |
| // An attempt to return the wrong ID |
| faulty_write_return = 1; |
| if (M_AXI_BRESP == EXOKAY && !wfifo_lock) |
| // An attempt to return the wrong ID |
| faulty_write_return = 1; |
| end |
| end |
| // }}} |
| |
| // o_write_fault |
| // {{{ |
| // On a write fault, we're going to disconnect the write port from |
| // the slave, and return errors on each write connect. o_write_fault |
| // is our signal determining if the write channel is disconnected. |
| // |
| // Most of this work is determined within faulty_write_return above. |
| // Here we do just a bit more: |
| initial o_write_fault = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || clear_fault) |
| o_write_fault <= 0; |
| else if ((!M_AXI_ARESETN&&o_read_fault) || write_timeout) |
| o_write_fault <= 1; |
| else if (M_AXI_BVALID && M_AXI_BREADY) |
| o_write_fault <= (o_write_fault) || faulty_write_return; |
| else if (M_AXI_WVALID && M_AXI_WREADY |
| && M_AXI_AWVALID && !M_AXI_AWREADY) |
| // Accepting the write data prior to the write address |
| // is a fault |
| o_write_fault <= 1; |
| // }}} |
| // }}} |
| |
| // Write return generation |
| // {{{ |
| // m_b* |
| // {{{ |
| // Since we only ever allow a single write burst at a time, we don't |
| // need to double buffer the return channel. Hence, we'll set our |
| // return channel based upon the incoming values alone. Note that |
| // we're overriding the M_AXI_BID below, in order to make certain that |
| // the return goes to the right source. |
| // |
| always @(*) |
| if (o_write_fault) |
| begin |
| m_bvalid = (s_wbursts > (S_AXI_BVALID ? 1:0)); |
| m_bid = wfifo_id; |
| m_bresp = SLAVE_ERROR; |
| end else begin |
| m_bvalid = M_AXI_BVALID; |
| if (faulty_write_return) |
| m_bvalid = 0; |
| m_bid = wfifo_id; |
| m_bresp = M_AXI_BRESP; |
| end |
| // }}} |
| |
| // S_AXI_B* |
| // {{{ |
| // We'll *never* stall the slaves BREADY channel |
| // |
| // If the slave returns the response we are expecting, then S_AXI_BVALID |
| // will be low and it can go directly into the S_AXI_BVALID slot. If |
| // on the other hand the slave returns M_AXI_BVALID at the wrong time, |
| // then we'll quietly accept it and send the write interface into |
| // fault detected mode, setting o_write_fault. |
| // |
| // Sadly, this will create a warning in Vivado. If/when you see it, |
| // see this note and then just ignore it. |
| assign M_AXI_BREADY = 1; |
| |
| // |
| // Return a write acknowlegement at the end of every write |
| // burst--regardless of whether or not the slave does so |
| // |
| initial S_AXI_BVALID = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_BVALID <= 0; |
| else if (!S_AXI_BVALID || S_AXI_BREADY) |
| S_AXI_BVALID <= m_bvalid; |
| |
| // |
| // Set the values associated with the response |
| // |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_BVALID || S_AXI_BREADY) |
| begin |
| S_AXI_BID <= m_bid; |
| S_AXI_BRESP <= m_bresp; |
| end |
| // }}} |
| |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Read channel processing |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // |
| // Read address channel |
| // {{{ |
| |
| // S_AXI_ARREADY |
| // {{{ |
| initial S_AXI_ARREADY = (OPT_SELF_RESET) ? 0:1; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_ARREADY <= !OPT_SELF_RESET; |
| else if (S_AXI_ARVALID && S_AXI_ARREADY) |
| S_AXI_ARREADY <= 0; |
| else if (clear_fault) |
| S_AXI_ARREADY <= 1; |
| else if (!S_AXI_ARREADY) |
| S_AXI_ARREADY <= (S_AXI_RVALID && S_AXI_RLAST && S_AXI_RREADY); |
| // }}} |
| |
| // raddr_valid |
| // {{{ |
| always @(*) |
| if (OPT_SELF_RESET) |
| raddr_valid = !rfifo_empty; |
| else |
| raddr_valid = !S_AXI_ARREADY; |
| // }}} |
| |
| // r_ar* |
| // {{{ |
| // Double buffer the values associated with any read address request |
| // |
| initial r_arvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (S_AXI_ARVALID && S_AXI_ARREADY) |
| begin |
| r_arvalid <= (M_AXI_ARVALID && !M_AXI_ARREADY); |
| r_arid <= S_AXI_ARID; |
| r_araddr <= S_AXI_ARADDR; |
| r_arlen <= S_AXI_ARLEN; |
| r_arsize <= S_AXI_ARSIZE; |
| r_arburst <= S_AXI_ARBURST; |
| r_arlock <= S_AXI_ARLOCK; |
| r_arcache <= S_AXI_ARCACHE; |
| r_arprot <= S_AXI_ARPROT; |
| r_arqos <= S_AXI_ARQOS; |
| end else if (M_AXI_ARREADY) |
| r_arvalid <= 0; |
| |
| if (!M_AXI_ARESETN) |
| r_arvalid <= 0; |
| end |
| // }}} |
| |
| // m_ar* |
| // {{{ |
| always @(*) |
| if (r_arvalid) |
| begin |
| m_arvalid = r_arvalid; |
| m_arid = r_arid; |
| m_araddr = r_araddr; |
| m_arlen = r_arlen; |
| m_arsize = r_arsize; |
| m_arburst = r_arburst; |
| m_arlock = r_arlock; |
| m_arcache = r_arcache; |
| m_arprot = r_arprot; |
| m_arqos = r_arqos; |
| end else begin |
| m_arvalid = S_AXI_ARVALID && S_AXI_ARREADY; |
| m_arid = S_AXI_ARID; |
| m_araddr = S_AXI_ARADDR; |
| m_arlen = S_AXI_ARLEN; |
| m_arsize = S_AXI_ARSIZE; |
| m_arburst = S_AXI_ARBURST; |
| m_arlock = S_AXI_ARLOCK; |
| m_arcache = S_AXI_ARCACHE; |
| m_arprot = S_AXI_ARPROT; |
| m_arqos = S_AXI_ARQOS; |
| end |
| // }}} |
| |
| // M_AXI_AR* |
| // {{{ |
| // Set the downstream values according to the transaction we've just |
| // received. |
| // |
| initial M_AXI_ARVALID = 0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (!M_AXI_ARVALID || M_AXI_ARREADY) |
| begin |
| |
| if (o_read_fault) |
| M_AXI_ARVALID <= 0; |
| else |
| M_AXI_ARVALID <= m_arvalid; |
| |
| M_AXI_ARID <= m_arid; |
| M_AXI_ARADDR <= m_araddr; |
| M_AXI_ARLEN <= m_arlen; |
| M_AXI_ARSIZE <= m_arsize; |
| M_AXI_ARBURST <= m_arburst; |
| M_AXI_ARLOCK <= m_arlock; |
| M_AXI_ARCACHE <= m_arcache; |
| M_AXI_ARPROT <= m_arprot; |
| M_AXI_ARQOS <= m_arqos; |
| end |
| |
| if (!M_AXI_ARESETN) |
| M_AXI_ARVALID <= 0; |
| end |
| // }}} |
| |
| // }}} |
| |
| // |
| // Read fault detection |
| // {{{ |
| |
| // read_timer |
| // {{{ |
| // First step: a timer. The timer starts as soon as the S_AXI_ARVALID |
| // is accepted. Once that happens, rfifo_empty will no longer be true. |
| // The count is reset any time the slave produces a value for us to |
| // read. Once the count saturates, it stops counting. |
| initial read_timer = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || clear_fault) |
| read_timer <= 0; |
| else if (rfifo_empty||(S_AXI_RVALID)) |
| read_timer <= 0; |
| else if (M_AXI_RVALID) |
| read_timer <= 0; |
| else if (!(&read_timer)) |
| read_timer <= read_timer + 1; |
| // }}} |
| |
| // read_timeout |
| // {{{ |
| // Once the counter > OPT_TIMEOUT, we have a timeout condition. |
| // We'll detect this one clock earlier below. If we ever enter |
| // a read time out condition, we'll set the read fault. The read |
| // timeout condition can only be cleared by a reset. |
| initial read_timeout = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || clear_fault) |
| read_timeout <= 0; |
| else if (rfifo_empty||S_AXI_RVALID) |
| read_timeout <= read_timeout; |
| else if (M_AXI_RVALID) |
| read_timeout <= read_timeout; |
| else if (read_timer == OPT_TIMEOUT) |
| read_timeout <= 1; |
| // }}} |
| |
| // |
| // faulty_read_return |
| // {{{ |
| // To avoid returning a fault from the slave, it is important to |
| // determine within a single clock period whether or not the slaves |
| // return value is at fault or not. That's the purpose of the code |
| // below. |
| always @(*) |
| begin |
| faulty_read_return = 0; |
| if (M_AXI_RVALID) |
| begin |
| if (M_AXI_ARVALID) |
| // It is a fault to return data apart from a |
| // request. |
| faulty_read_return = 1; |
| if (M_AXI_RID != rfifo_id) |
| // It is a fault to return data from a |
| // different ID |
| faulty_read_return = 1; |
| if (rfifo_last && (S_AXI_RVALID || !M_AXI_RLAST)) |
| faulty_read_return = 1; |
| if (rfifo_penultimate && S_AXI_RVALID && (r_rvalid || !M_AXI_RLAST)) |
| faulty_read_return = 1; |
| if (M_AXI_RRESP == EXOKAY && !rfifo_lock) |
| // An attempt to return the wrong ID |
| faulty_read_return = 1; |
| end |
| end |
| // }}} |
| |
| // o_read_fault |
| // {{{ |
| initial o_read_fault = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || clear_fault) |
| o_read_fault <= 0; |
| else if ((!M_AXI_ARESETN && o_write_fault) || read_timeout) |
| o_read_fault <= 1; |
| else if (M_AXI_RVALID) |
| begin |
| if (faulty_read_return) |
| o_read_fault <= 1; |
| if (!raddr_valid) |
| // It is a fault if we haven't issued an AR* request |
| // yet, and a value is returned |
| o_read_fault <= 1; |
| end |
| // }}} |
| |
| // }}} |
| |
| // |
| // Read return/acknowledgment processing |
| // {{{ |
| |
| // r_rvalid |
| // {{{ |
| // Step one, set/create the read return double buffer. If r_rvalid |
| // is true, there's a valid value in the double buffer location. |
| // |
| initial r_rvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || o_read_fault) |
| r_rvalid <= 0; |
| else if (!r_rvalid) |
| begin |
| // {{{ |
| // Refuse to set the double-buffer valid on any fault. |
| // That will also keep (below) M_AXI_RREADY high--so that |
| // following the fault the slave might still (pretend) to |
| // respond properly |
| if (faulty_read_return) |
| r_rvalid <= 0; |
| else if (o_read_fault) |
| r_rvalid <= 0; |
| // If there's nothing in the double buffer, then we might |
| // place something in there. The double buffer only gets |
| // filled under two conditions: 1) something is pending to be |
| // returned, and 2) there's another return that we can't |
| // stall and so need to accept here. |
| r_rvalid <= M_AXI_RVALID && M_AXI_RREADY |
| && (S_AXI_RVALID && !S_AXI_RREADY); |
| // }}} |
| end else if (S_AXI_RREADY) |
| // Once the up-stream read-channel clears, we can always |
| // clear the double buffer |
| r_rvalid <= 0; |
| // }}} |
| |
| // r_rresp, r_rdata |
| // {{{ |
| // Here's the actual values kept whenever r_rvalid is true. This is |
| // the double buffer. Notice that r_rid and r_last are generated |
| // locally, so not recorded here. |
| // |
| always @(posedge S_AXI_ACLK) |
| if (!r_rvalid) |
| begin |
| r_rresp <= M_AXI_RRESP; |
| r_rdata <= M_AXI_RDATA; |
| end |
| // }}} |
| |
| // M_AXI_RREADY |
| // {{{ |
| // Stall the downstream channel any time there's something in the |
| // double buffer. In spite of the ! here, this is a registered value. |
| assign M_AXI_RREADY = !r_rvalid; |
| // }}} |
| |
| // rfifo_id, rfifo_lock |
| // {{{ |
| // Copy the ID for later comparisons on the return |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARVALID && S_AXI_ARREADY) |
| begin |
| rfifo_id <= S_AXI_ARID; |
| rfifo_lock <= S_AXI_ARLOCK; |
| end |
| // }}} |
| |
| // rfifo_[counter|empty|last|penultimate |
| // {{{ |
| // Count the number of outstanding read elements. This is the number |
| // of read returns we still expect--from the upstream perspective. The |
| // downstream perspective will be off by both what's waiting for |
| // S_AXI_RREADY and what's in the double buffer |
| // |
| initial rfifo_counter = 0; |
| initial rfifo_empty = 1; |
| initial rfifo_last = 0; |
| initial rfifo_penultimate= 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| rfifo_counter <= 0; |
| rfifo_empty <= 1; |
| rfifo_last <= 0; |
| rfifo_penultimate<= 0; |
| end else if (S_AXI_ARVALID && S_AXI_ARREADY) |
| begin |
| rfifo_counter <= S_AXI_ARLEN+1; |
| rfifo_empty <= 0; |
| rfifo_last <= (S_AXI_ARLEN == 0); |
| rfifo_penultimate <= (S_AXI_ARLEN == 1); |
| end else if (!rfifo_empty) |
| begin |
| if (S_AXI_RVALID && S_AXI_RREADY) |
| begin |
| rfifo_counter <= rfifo_counter - 1; |
| rfifo_empty <= (rfifo_counter <= 1); |
| rfifo_last <= (rfifo_counter == 2); |
| rfifo_penultimate <= (rfifo_counter == 3); |
| end |
| end |
| // }}} |
| |
| // m_rvalid, m_rresp |
| // {{{ |
| // Determine values to send back and return |
| // |
| // This data set includes all the return values, even though only |
| // RRESP and RVALID are set in this block. |
| always @(*) |
| if (o_read_fault || (!M_AXI_ARESETN && OPT_SELF_RESET)) |
| begin |
| m_rvalid = !rfifo_empty; |
| if (S_AXI_RVALID && rfifo_last) |
| m_rvalid = 0; |
| m_rresp = SLAVE_ERROR; |
| end else if (r_rvalid) |
| begin |
| m_rvalid = r_rvalid; |
| m_rresp = r_rresp; |
| end else begin |
| m_rvalid = M_AXI_RVALID && raddr_valid && !faulty_read_return; |
| m_rresp = M_AXI_RRESP; |
| end |
| // }}} |
| |
| // m_rid |
| // {{{ |
| // We've stored the ID locally, so that our response will never be in |
| // error |
| always @(*) |
| m_rid = rfifo_id; |
| // }}} |
| |
| // m_rlast |
| // {{{ |
| // Ideally, we'd want to say m_rlast = rfifo_last. However, we might |
| // have a value in S_AXI_RVALID already. In that case, the last |
| // value can only be true if we are one further away from the end. |
| // (Remember, rfifo_last and rfifo_penultimate are both dependent upon |
| // the *upstream* number of read values outstanding, not the downstream |
| // number which we can't trust in all cases) |
| always @(*) |
| if (S_AXI_RVALID) |
| m_rlast = rfifo_penultimate; |
| else |
| m_rlast = (rfifo_last); |
| // }}} |
| |
| // m_rdata |
| // {{{ |
| // In the case of a fault, rdata is a don't care. Therefore we can |
| // always set it based upon the values returned from the slave. |
| always @(*) |
| if (r_rvalid) |
| m_rdata = r_rdata; |
| else |
| m_rdata = M_AXI_RDATA; |
| // }}} |
| |
| // S_AXI_R* |
| // {{{ |
| // Record our return data values |
| // |
| // These are the values from either the slave, the double buffer, |
| // or an error value bypassing either as determined by the m_* values. |
| // Per spec, all of these values must be registered. First the valid |
| // signal |
| initial S_AXI_RVALID = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_RVALID <= 0; |
| else if (!S_AXI_RVALID || S_AXI_RREADY) |
| S_AXI_RVALID <= m_rvalid; |
| |
| // Then the various slave data channels |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_RVALID || S_AXI_RREADY) |
| begin |
| S_AXI_RID <= m_rid; |
| S_AXI_RRESP <= m_rresp; |
| S_AXI_RLAST <= m_rlast; |
| S_AXI_RDATA <= m_rdata; |
| end |
| // }}} |
| |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Self-reset |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| generate if (OPT_SELF_RESET) |
| begin |
| // {{{ |
| // Declarations |
| // {{{ |
| reg [4:0] reset_counter; |
| reg reset_timeout, r_clear_fault; |
| // }}} |
| |
| // M_AXI_ARESETN |
| // {{{ |
| initial M_AXI_ARESETN = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| M_AXI_ARESETN <= 0; |
| else if (clear_fault) |
| M_AXI_ARESETN <= 1; |
| else if (o_read_fault || o_write_fault) |
| M_AXI_ARESETN <= 0; |
| // }}} |
| |
| // reset_counter |
| // {{{ |
| initial reset_counter = 0; |
| always @(posedge S_AXI_ACLK) |
| if (M_AXI_ARESETN) |
| reset_counter <= 0; |
| else if (!reset_timeout) |
| reset_counter <= reset_counter+1; |
| // }}} |
| |
| always @(*) |
| reset_timeout <= reset_counter[4]; |
| |
| // r_clear_fault |
| // {{{ |
| initial r_clear_fault <= 1; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| r_clear_fault <= 1; |
| else if (!M_AXI_ARESETN && !reset_timeout) |
| r_clear_fault <= 0; |
| else if (!o_read_fault && !o_write_fault) |
| r_clear_fault <= 0; |
| else if (raddr_valid || waddr_valid) |
| r_clear_fault <= 0; |
| else |
| r_clear_fault <= 1; |
| // }}} |
| |
| // clear_fault |
| // {{{ |
| always @(*) |
| if (S_AXI_AWVALID || S_AXI_ARVALID) |
| clear_fault = 0; |
| else if (raddr_valid || waddr_valid) |
| clear_fault = 0; |
| else |
| clear_fault = r_clear_fault; |
| // }}} |
| |
| // }}} |
| end else begin |
| // {{{ |
| always @(*) |
| M_AXI_ARESETN = S_AXI_ARESETN; |
| always @(*) |
| clear_fault = 0; |
| // }}} |
| end endgenerate |
| // }}} |
| |
| // Make Verilator happy |
| // {{{ |
| // Verilator lint_off UNUSED |
| wire unused; |
| assign unused = &{ 1'b0 }; |
| // Verilator lint_on UNUSED |
| // }}} |
| // Add user logic here |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| // {{{ |
| // Below are just some of the formal properties used to verify |
| // this core. The full property set is maintained elsewhere. |
| // |
| parameter [0:0] F_OPT_FAULTLESS = 1; |
| |
| // |
| // ... |
| // }}} |
| |
| faxi_slave #( |
| // {{{ |
| .C_AXI_ID_WIDTH(C_S_AXI_ID_WIDTH), |
| .C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH), |
| .C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH) |
| // ... |
| // }}} |
| ) |
| f_slave( |
| .i_clk(S_AXI_ACLK), |
| .i_axi_reset_n(S_AXI_ARESETN), |
| // {{{ |
| // |
| // Address write channel |
| // |
| .i_axi_awid(S_AXI_AWID), |
| .i_axi_awaddr(S_AXI_AWADDR), |
| .i_axi_awlen(S_AXI_AWLEN), |
| .i_axi_awsize(S_AXI_AWSIZE), |
| .i_axi_awburst(S_AXI_AWBURST), |
| .i_axi_awlock(S_AXI_AWLOCK), |
| .i_axi_awcache(S_AXI_AWCACHE), |
| .i_axi_awprot(S_AXI_AWPROT), |
| .i_axi_awqos(S_AXI_AWQOS), |
| .i_axi_awvalid(S_AXI_AWVALID), |
| .i_axi_awready(S_AXI_AWREADY), |
| // |
| // |
| // |
| // Write Data Channel |
| // |
| // Write Data |
| .i_axi_wdata(S_AXI_WDATA), |
| .i_axi_wstrb(S_AXI_WSTRB), |
| .i_axi_wlast(S_AXI_WLAST), |
| .i_axi_wvalid(S_AXI_WVALID), |
| .i_axi_wready(S_AXI_WREADY), |
| // |
| // |
| // Response ID tag. This signal is the ID tag of the |
| // write response. |
| .i_axi_bid(S_AXI_BID), |
| .i_axi_bresp(S_AXI_BRESP), |
| .i_axi_bvalid(S_AXI_BVALID), |
| .i_axi_bready(S_AXI_BREADY), |
| // |
| // |
| // |
| // Read address channel |
| // |
| .i_axi_arid(S_AXI_ARID), |
| .i_axi_araddr(S_AXI_ARADDR), |
| .i_axi_arlen(S_AXI_ARLEN), |
| .i_axi_arsize(S_AXI_ARSIZE), |
| .i_axi_arburst(S_AXI_ARBURST), |
| .i_axi_arlock(S_AXI_ARLOCK), |
| .i_axi_arcache(S_AXI_ARCACHE), |
| .i_axi_arprot(S_AXI_ARPROT), |
| .i_axi_arqos(S_AXI_ARQOS), |
| .i_axi_arvalid(S_AXI_ARVALID), |
| .i_axi_arready(S_AXI_ARREADY), |
| // |
| // |
| // |
| // Read data return channel |
| // |
| .i_axi_rid(S_AXI_RID), |
| .i_axi_rdata(S_AXI_RDATA), |
| .i_axi_rresp(S_AXI_RRESP), |
| .i_axi_rlast(S_AXI_RLAST), |
| .i_axi_rvalid(S_AXI_RVALID), |
| // Read ready. This signal indicates that the master can |
| // accept the read data and response information. |
| .i_axi_rready(S_AXI_RREADY), |
| // |
| // Formal outputs |
| // |
| .f_axi_awr_nbursts(f_axi_awr_nbursts), |
| .f_axi_wr_pending(f_axi_wr_pending), |
| .f_axi_rd_nbursts(f_axi_rd_nbursts), |
| .f_axi_rd_outstanding(f_axi_rd_outstanding) |
| // |
| // ... |
| // }}} |
| ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Write induction properties |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| // {{{ |
| |
| // 1. We will only ever handle a single burst--never any more |
| always @(*) |
| assert(f_axi_awr_nbursts <= 1); |
| |
| always @(*) |
| if (f_axi_awr_nbursts == 1) |
| begin |
| assert(!S_AXI_AWREADY); |
| if (S_AXI_BVALID) |
| assert(f_axi_wr_pending == 0); |
| if (!o_write_fault && M_AXI_AWVALID) |
| assert(f_axi_wr_pending == M_AXI_AWLEN + 1 |
| - (M_AXI_WVALID ? 1:0) |
| - (r_wvalid ? 1 : 0)); |
| if (!o_write_fault && f_axi_wr_pending > 0) |
| assert((!M_AXI_WVALID || !M_AXI_WLAST) |
| &&(!r_wvalid || !r_wlast)); |
| if (!o_write_fault && M_AXI_WVALID && M_AXI_WLAST) |
| assert(!r_wvalid || !r_wlast); |
| end else begin |
| assert(s_wbursts == 0); |
| assert(!S_AXI_WREADY); |
| if (OPT_SELF_RESET) |
| assert(1 || S_AXI_AWREADY || !M_AXI_ARESETN || !S_AXI_ARESETN); |
| else |
| assert(S_AXI_AWREADY); |
| end |
| |
| // |
| // ... |
| // |
| |
| // |
| // AWREADY will always be low mid-burst |
| always @(posedge S_AXI_ACLK) |
| if (!f_past_valid || $past(!S_AXI_ARESETN)) |
| assert(S_AXI_AWREADY == !OPT_SELF_RESET); |
| else if (f_axi_wr_pending > 0) |
| assert(!S_AXI_AWREADY); |
| else if (s_wbursts) |
| assert(!S_AXI_AWREADY); |
| else if (!OPT_SELF_RESET) |
| assert(S_AXI_AWREADY); |
| else if (!o_write_fault && !o_read_fault) |
| assert(S_AXI_AWREADY || OPT_SELF_RESET); |
| |
| always @(*) |
| if (f_axi_wr_pending > 0) |
| assert(s_wbursts == 0); |
| else if (f_axi_awr_nbursts > 0) |
| assert(s_wbursts == f_axi_awr_nbursts); |
| else |
| assert(s_wbursts == 0); |
| |
| always @(*) |
| if (!o_write_fault && S_AXI_AWREADY) |
| assert(!M_AXI_AWVALID); |
| |
| always @(*) |
| if (M_AXI_ARESETN && (f_axi_awr_nbursts == 0)) |
| begin |
| assert(o_write_fault || !M_AXI_AWVALID); |
| assert(!S_AXI_BVALID); |
| assert(s_wbursts == 0); |
| end else if (M_AXI_ARESETN && s_wbursts == 0) |
| assert(f_axi_wr_pending > 0); |
| |
| always @(*) |
| if (S_AXI_WREADY) |
| assert(waddr_valid); |
| else if (f_axi_wr_pending > 0) |
| begin |
| if (!o_write_fault) |
| assert(M_AXI_WVALID && r_wvalid); |
| end |
| |
| always @(*) |
| if (!OPT_SELF_RESET) |
| assert(waddr_valid == !S_AXI_AWREADY); |
| else begin |
| // ... |
| assert(waddr_valid == (f_axi_awr_nbursts > 0)); |
| end |
| |
| always @(*) |
| if (S_AXI_ARESETN && !o_write_fault && f_axi_wr_pending && !S_AXI_WREADY) |
| assert(M_AXI_WVALID); |
| |
| always @(*) |
| if (S_AXI_ARESETN && !o_write_fault && m_wempty) |
| begin |
| assert(M_AXI_AWVALID || !M_AXI_WVALID); |
| assert(M_AXI_AWVALID || f_axi_wr_pending == 0); |
| end |
| |
| always @(*) |
| if (S_AXI_ARESETN && M_AXI_AWVALID) |
| begin |
| if (!o_write_fault && !M_AXI_AWVALID) |
| assert(f_axi_wr_pending + (M_AXI_WVALID ? 1:0) + (r_wvalid ? 1:0) == m_wpending); |
| else if (!o_write_fault) |
| begin |
| assert(f_axi_wr_pending == M_AXI_AWLEN + 1 - (M_AXI_WVALID ? 1:0) - (r_wvalid ? 1:0)); |
| assert(m_wpending == 0); |
| end |
| end |
| |
| always @(*) |
| assert(m_wpending <= 9'h100); |
| |
| always @(*) |
| if (M_AXI_ARESETN && (!o_write_fault)&&(f_axi_awr_nbursts == 0)) |
| assert(!M_AXI_AWVALID); |
| |
| always @(*) |
| if (S_AXI_ARESETN && !o_write_fault) |
| begin |
| if (f_axi_awr_nbursts == 0) |
| begin |
| assert(!M_AXI_AWVALID); |
| assert(!M_AXI_WVALID); |
| end |
| |
| if (!M_AXI_AWVALID) |
| assert(f_axi_wr_pending |
| +(M_AXI_WVALID ? 1:0) |
| + (r_wvalid ? 1:0) |
| == m_wpending); |
| if (f_axi_awr_nbursts == (S_AXI_BVALID ? 1:0)) |
| begin |
| assert(!M_AXI_AWVALID); |
| assert(!M_AXI_WVALID); |
| end |
| |
| if (S_AXI_BVALID) |
| assert(f_axi_awr_nbursts == 1); |
| |
| if (M_AXI_AWVALID) |
| assert(m_wpending == 0); |
| |
| if (S_AXI_AWREADY) |
| assert(!M_AXI_AWVALID); |
| end |
| |
| always @(*) |
| assert(!r_awvalid); |
| |
| always @(*) |
| assert(m_wempty == (m_wpending == 0)); |
| always @(*) |
| assert(m_wlastctr == (m_wpending == 1)); |
| |
| // |
| // Verify the contents of the skid buffers |
| // |
| |
| // |
| // ... |
| // |
| |
| always @(*) |
| if (write_timer > OPT_TIMEOUT) |
| assert(o_write_fault || write_timeout); |
| |
| always @(*) |
| if (!OPT_SELF_RESET) |
| assert(waddr_valid == !S_AXI_AWREADY); |
| else if (waddr_valid) |
| assert(!S_AXI_AWREADY); |
| |
| always @(*) |
| if (!o_write_fault && M_AXI_ARESETN) |
| assert(waddr_valid == !S_AXI_AWREADY); |
| |
| always @(*) |
| if (f_axi_wr_pending == 0) |
| assert(!S_AXI_WREADY); |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Read induction properties |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| // |
| |
| always @(*) |
| assert(f_axi_rd_nbursts <= 1); |
| always @(*) |
| assert(raddr_valid == (f_axi_rd_nbursts>0)); |
| always @(*) |
| if (f_axi_rdid_nbursts > 0) |
| assert(rfifo_id == f_axi_rd_checkid); |
| else if (f_axi_rd_nbursts > 0) |
| assert(rfifo_id != f_axi_rd_checkid); |
| |
| always @(*) |
| if (f_axi_rd_nbursts > 0) |
| assert(raddr_valid); |
| |
| always @(*) |
| if (raddr_valid) |
| assert(!S_AXI_ARREADY); |
| |
| always @(*) |
| if (!OPT_SELF_RESET) |
| assert(raddr_valid == !S_AXI_ARREADY); |
| else begin |
| // ... |
| assert(raddr_valid == (f_axi_rd_nbursts > 0)); |
| end |
| |
| // |
| // ... |
| // |
| |
| always @(*) |
| if (f_axi_rd_outstanding == 0) |
| assert(!raddr_valid || OPT_SELF_RESET); |
| |
| always @(*) |
| if (!o_read_fault && S_AXI_ARREADY) |
| assert(!M_AXI_ARVALID); |
| |
| // Our "FIFO" counter |
| always @(*) |
| assert(rfifo_counter == f_axi_rd_outstanding); |
| |
| always @(*) |
| begin |
| assert(rfifo_empty == (rfifo_counter == 0)); |
| assert(rfifo_last == (rfifo_counter == 1)); |
| assert(rfifo_penultimate == (rfifo_counter == 2)); |
| end |
| |
| // |
| // ... |
| // |
| |
| always @(*) |
| if (r_arvalid) |
| assert(skid_arvalid); |
| |
| always @(*) |
| if (read_timer > OPT_TIMEOUT) |
| assert(read_timeout); |
| |
| |
| always @(posedge S_AXI_ACLK) |
| if (OPT_SELF_RESET && (!f_past_valid || !$past(M_AXI_ARESETN))) |
| begin |
| assume(!M_AXI_BVALID); |
| assume(!M_AXI_RVALID); |
| end |
| |
| always @(*) |
| if (!o_read_fault && M_AXI_ARESETN) |
| assert(raddr_valid == !S_AXI_ARREADY); |
| |
| always @(*) |
| if (f_axi_rd_nbursts > 0) |
| assert(raddr_valid); |
| |
| always @(*) |
| if (S_AXI_ARESETN && OPT_SELF_RESET) |
| begin |
| if (!M_AXI_ARESETN) |
| assert(o_read_fault || o_write_fault /* ... */ ); |
| end |
| // }}} |
| |
| |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover properties |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Good interface check |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| generate if (F_OPT_FAULTLESS) |
| begin |
| // |
| // ... |
| // |
| |
| faxi_master #( |
| // {{{ |
| .C_AXI_ID_WIDTH(C_S_AXI_ID_WIDTH), |
| .C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH), |
| .C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH)) |
| // ... |
| // }}} |
| f_master( |
| .i_clk(S_AXI_ACLK), |
| .i_axi_reset_n(M_AXI_ARESETN), |
| // {{{ |
| // |
| // Address write channel |
| // |
| .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_awvalid(M_AXI_AWVALID), |
| .i_axi_awready(M_AXI_AWREADY), |
| // |
| // |
| // |
| // Write Data Channel |
| // |
| // Write Data |
| .i_axi_wdata(M_AXI_WDATA), |
| .i_axi_wstrb(M_AXI_WSTRB), |
| .i_axi_wlast(M_AXI_WLAST), |
| .i_axi_wvalid(M_AXI_WVALID), |
| .i_axi_wready(M_AXI_WREADY), |
| // |
| // |
| // Response ID tag. This signal is the ID tag of the |
| // write response. |
| .i_axi_bid(M_AXI_BID), |
| .i_axi_bresp(M_AXI_BRESP), |
| .i_axi_bvalid(M_AXI_BVALID), |
| .i_axi_bready(M_AXI_BREADY), |
| // |
| // |
| // |
| // Read address channel |
| // |
| .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_arvalid(M_AXI_ARVALID), |
| .i_axi_arready(M_AXI_ARREADY), |
| // |
| // |
| // |
| // Read data return channel |
| // |
| .i_axi_rid(M_AXI_RID), |
| .i_axi_rdata(M_AXI_RDATA), |
| .i_axi_rresp(M_AXI_RRESP), |
| .i_axi_rlast(M_AXI_RLAST), |
| .i_axi_rvalid(M_AXI_RVALID), |
| .i_axi_rready(M_AXI_RREADY), |
| // |
| // Formal outputs |
| // |
| .f_axi_awr_nbursts(fm_axi_awr_nbursts), |
| .f_axi_wr_pending(fm_axi_wr_pending), |
| .f_axi_rd_nbursts(fm_axi_rd_nbursts), |
| .f_axi_rd_outstanding(fm_axi_rd_outstanding) |
| // |
| // ... |
| // |
| // }}} |
| ); |
| |
| // {{{ |
| always @(*) |
| if (OPT_SELF_RESET) |
| assert(!o_write_fault || !M_AXI_ARESETN); |
| else |
| assert(!o_write_fault); |
| |
| always @(*) |
| if (OPT_SELF_RESET) |
| assert(!o_read_fault || !M_AXI_ARESETN); |
| else |
| assert(!o_read_fault); |
| |
| always @(*) |
| if (OPT_SELF_RESET) |
| assert(!read_timeout || !M_AXI_ARESETN); |
| else |
| assert(!read_timeout); |
| |
| always @(*) |
| if (OPT_SELF_RESET) |
| assert(!write_timeout || !M_AXI_ARESETN); |
| else |
| assert(!write_timeout); |
| |
| always @(*) |
| if (S_AXI_AWREADY) |
| assert(!M_AXI_AWVALID); |
| |
| // |
| // ... |
| // |
| |
| always @(*) |
| if (M_AXI_ARESETN && f_axi_rd_nbursts > 0) |
| assert(f_axi_rd_nbursts == fm_axi_rd_nbursts |
| + (M_AXI_ARVALID ? 1 : 0) |
| + (r_rvalid&&m_rlast ? 1 : 0) |
| + (S_AXI_RVALID&&S_AXI_RLAST ? 1 : 0)); |
| |
| always @(*) |
| if (M_AXI_ARESETN && f_axi_rd_outstanding > 0) |
| assert(f_axi_rd_outstanding == fm_axi_rd_outstanding |
| + (M_AXI_ARVALID ? M_AXI_ARLEN+1 : 0) |
| + (r_rvalid ? 1 : 0) |
| + (S_AXI_RVALID ? 1 : 0)); |
| |
| // |
| // ... |
| // |
| always @(*) |
| if (M_AXI_RVALID) |
| assert(!M_AXI_ARVALID); |
| |
| always @(*) |
| if (S_AXI_ARESETN) |
| assert(m_wpending == fm_axi_wr_pending); |
| |
| always @(*) |
| if (S_AXI_ARESETN && fm_axi_awr_nbursts > 0) |
| begin |
| assert(fm_axi_awr_nbursts== f_axi_awr_nbursts); |
| assert(fm_axi_awr_nbursts == 1); |
| // |
| // ... |
| // |
| end |
| |
| // |
| // ... |
| // |
| |
| end endgenerate |
| |
| // |
| // ... |
| // |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Never path check |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| (* anyconst *) reg [C_S_AXI_ADDR_WIDTH-1:0] fc_never_write_addr, |
| fc_never_read_addr; |
| (* anyconst *) reg [C_S_AXI_DATA_WIDTH + C_S_AXI_DATA_WIDTH/8-1:0] |
| fc_never_write_data; |
| (* anyconst *) reg [C_S_AXI_DATA_WIDTH-1:0] fc_never_read_data; |
| |
| // Write address |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && S_AXI_AWVALID) |
| assume(S_AXI_AWADDR != fc_never_write_addr); |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && !o_write_fault && M_AXI_ARESETN && M_AXI_AWVALID) |
| assert(M_AXI_AWADDR != fc_never_write_addr); |
| // }}} |
| |
| // Write data |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && S_AXI_WVALID) |
| assume({ S_AXI_WDATA, S_AXI_WSTRB } != fc_never_write_data); |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && !o_write_fault && M_AXI_ARESETN && M_AXI_WVALID) |
| assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data); |
| // }}} |
| |
| // Read address |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && S_AXI_ARVALID) |
| assume(S_AXI_ARADDR != fc_never_read_addr); |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && r_arvalid) |
| assume(r_araddr != fc_never_read_addr); |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && !o_read_fault && M_AXI_ARESETN && M_AXI_ARVALID) |
| assert(M_AXI_ARADDR != fc_never_read_addr); |
| // }}} |
| |
| // Read data |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && M_AXI_ARESETN && M_AXI_RVALID) |
| assume(M_AXI_RDATA != fc_never_read_data); |
| |
| always @(posedge S_AXI_ACLK) |
| if (S_AXI_ARESETN && S_AXI_RVALID && S_AXI_RRESP != SLAVE_ERROR) |
| assert(S_AXI_RDATA != fc_never_read_data); |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // We'll use these to determine the best performance this core |
| // can achieve |
| // |
| reg [4:0] f_dbl_rd_count, f_dbl_wr_count; |
| |
| initial f_dbl_wr_count = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || o_write_fault) |
| f_dbl_wr_count = 0; |
| else if (S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN == 3) |
| begin |
| if (!(&f_dbl_wr_count)) |
| f_dbl_wr_count <= f_dbl_wr_count + 1; |
| end |
| |
| always @(*) |
| cover(!S_AXI_ARESETN && (f_dbl_wr_count > 3) |
| && (!o_write_fault) |
| &&(!S_AXI_AWVALID && !S_AXI_WVALID |
| && !S_AXI_BVALID) |
| && (f_axi_awr_nbursts == 0) |
| && (f_axi_wr_pending == 0)); |
| |
| always @(*) |
| cover(!S_AXI_ARESETN && (f_dbl_wr_count > 1) |
| && (!o_write_fault) |
| ); |
| |
| always @(*) |
| cover(S_AXI_AWVALID && S_AXI_AWREADY); |
| |
| always @(*) |
| cover(S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN == 3); |
| |
| initial f_dbl_rd_count = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN || o_read_fault) |
| f_dbl_rd_count = 0; |
| else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN == 3) |
| begin |
| if (!(&f_dbl_rd_count)) |
| f_dbl_rd_count <= f_dbl_rd_count + 1; |
| end |
| |
| always @(*) |
| cover(!S_AXI_ARESETN && (f_dbl_rd_count > 3) |
| && (f_axi_rd_nbursts == 0) |
| && !S_AXI_ARVALID && !S_AXI_RVALID); |
| // }}} |
| `endif |
| // }}} |
| endmodule |
| `ifndef YOSYS |
| `default_nettype wire |
| `endif |