diff options
Diffstat (limited to 'rtl/wb2axip/axisafety.v')
| -rw-r--r-- | rtl/wb2axip/axisafety.v | 2339 |
1 files changed, 0 insertions, 2339 deletions
diff --git a/rtl/wb2axip/axisafety.v b/rtl/wb2axip/axisafety.v deleted file mode 100644 index ff7e351..0000000 --- a/rtl/wb2axip/axisafety.v +++ /dev/null @@ -1,2339 +0,0 @@ -//////////////////////////////////////////////////////////////////////////////// -// -// 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. -// -// 5) OPT_EXCLUSIVE If clear, will prohibit the slave from ever -// receiving an exclusive access request. This saves the logic -// in the firewall necessary to check that an EXOKAY response -// to a write request was truly an allowed response. Since that -// logic can explode with the ID width, sparing it can be quite -// useful. If set, provides full exclusive access checking in -// addition to the normal bus fault checking. -// -// 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-2024, Gisselquist Technology, LLC -// {{{ -// This file is part of the WB2AXIP project. -// -// The WB2AXIP project contains free software and gateware, licensed under the -// Apache License, Version 2.0 (the "License"). You may not use this project, -// or this file, except in compliance with the License. You may obtain a copy -// of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT -// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the -// License for the specific language governing permissions and limitations -// under the License. -// -//////////////////////////////////////////////////////////////////////////////// -// -// -`default_nettype none -// }}} -module axisafety #( - // {{{ - parameter C_S_AXI_ID_WIDTH = 1, - parameter C_S_AXI_DATA_WIDTH = 32, - parameter C_S_AXI_ADDR_WIDTH = 16, - // OPT_SELF_RESET: Set to true if the downstream slave should be - // reset upon detecting an error and separate from the upstream reset - // domain - parameter [0:0] OPT_SELF_RESET = 1'b0, - // OPT_EXCLUSIVE: Set to true if the downstream slave might possibly - // offer an exclusive access capability - parameter [0:0] OPT_EXCLUSIVE = 1'b0, - // - // 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 [1:0] OKAY = 2'b00, 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 - wire [IW-1:0] wfifo_id; - wire 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; - wire waddr_valid, raddr_valid; - - wire lock_enabled, lock_failed; - wire [(1<<IW)-1:0] lock_active; - reg rfifo_first, exread; - // }}} - //////////////////////////////////////////////////////////////////////// - // - // 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_BVALID && S_AXI_BREADY; - // }}} - - generate if (OPT_EXCLUSIVE) - begin : GEN_LOCK_ENABLED - // {{{ - reg r_lock_enabled, r_lock_failed; - - // lock_enabled - // {{{ - initial r_lock_enabled = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !OPT_EXCLUSIVE) - r_lock_enabled <= 0; - else if (S_AXI_AWVALID && S_AXI_AWREADY) - r_lock_enabled <= S_AXI_AWLOCK && lock_active[S_AXI_AWID]; - else if (S_AXI_BVALID && S_AXI_BREADY) - r_lock_enabled <= 0; - // }}} - - // lock_failed - // {{{ - initial r_lock_failed = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !OPT_EXCLUSIVE) - r_lock_failed <= 0; - else if (S_AXI_AWVALID && S_AXI_AWREADY) - r_lock_failed <= S_AXI_AWLOCK && !lock_active[S_AXI_AWID]; - else if (S_AXI_BVALID && S_AXI_BREADY) - r_lock_failed <= 0; - // }}} - - assign lock_enabled = r_lock_enabled; - assign lock_failed = r_lock_failed; - // }}} - end else begin : NO_LOCK_ENABLE - // {{{ - assign lock_enabled = 0; - assign lock_failed = 0; - // }}} - end endgenerate - - // waddr_valid - // {{{ - generate if (OPT_SELF_RESET) - begin : GEN_LCL_RESET - reg r_waddr_valid; - - initial r_waddr_valid = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - r_waddr_valid <= 0; - else if (S_AXI_AWVALID && S_AXI_AWREADY) - r_waddr_valid <= 1; - else if (waddr_valid) - r_waddr_valid <= !S_AXI_BVALID || !S_AXI_BREADY; - - assign waddr_valid = r_waddr_valid; - end else begin : NO_LCL_RESET - assign 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) - begin - r_awvalid <= 0; - r_awlock <= 0; - end - - if (!OPT_EXCLUSIVE) - r_awlock <= 1'b0; - 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 && OPT_EXCLUSIVE; - 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 && lock_active[m_awid]; - M_AXI_AWCACHE <= m_awcache; - M_AXI_AWPROT <= m_awprot; - M_AXI_AWQOS <= m_awqos; - end - - if (!OPT_EXCLUSIVE) - M_AXI_AWLOCK <= 0; - 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. - - assign wfifo_id = r_awid; - assign wfifo_lock = r_awlock; - // }}} - - // 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; - if (OPT_EXCLUSIVE && lock_failed) - M_AXI_WSTRB <= 0; - 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 && (!OPT_EXCLUSIVE - || !lock_enabled)) - // An attempt to return a valid lock, without - // a prior request - 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 - // {{{ - generate if (OPT_SELF_RESET) - begin : GEN_READ_RESET - assign raddr_valid = !rfifo_empty; - end else begin : SIMPLE_RADDR_VALID - assign raddr_valid = !S_AXI_ARREADY; - end endgenerate - // }}} - - // 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 <= 0; // (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; - if (!OPT_EXCLUSIVE || !S_AXI_ARESETN) - r_arlock <= 1'b0; - 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 && OPT_EXCLUSIVE; - 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 && OPT_EXCLUSIVE; - 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 before the - // request has been accepted - 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 && (!OPT_EXCLUSIVE || !rfifo_lock)) - faulty_read_return = 1; - if (OPT_EXCLUSIVE && exread && M_AXI_RRESP == OKAY) - // Can't switch from EXOKAY to OKAY - faulty_read_return = 1; - if ((!OPT_EXCLUSIVE || (!rfifo_first && !exread)) - && M_AXI_RRESP == EXOKAY) - // Can't switch from OKAY to EXOKAY - 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 - // {{{ - - - // exread - // {{{ - always @(posedge S_AXI_ACLK) - if (!M_AXI_ARESETN || !OPT_EXCLUSIVE) - exread <= 0; - else if (M_AXI_RVALID && M_AXI_RREADY) - begin - if (!M_AXI_RRESP[1]) - exread <= (M_AXI_RRESP == EXOKAY); - end else if (S_AXI_RVALID && S_AXI_RREADY) - begin - if (S_AXI_RLAST) - exread <= 1'b0; - end - // }}} - - // 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 @(*) - rfifo_id = r_arid; - always @(*) - rfifo_lock = r_arlock; - // }}} - - // 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 - // }}} - - // lock_active - // {{{ - generate if (OPT_EXCLUSIVE) - begin : CALC_LOCK_ACTIVE - // {{{ - genvar gk; - - for(gk=0; gk<(1<<IW); gk=gk+1) - begin : LOCK_PER_ID - reg r_lock_active; - - initial r_lock_active = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN - || faulty_read_return || faulty_write_return) - r_lock_active <= 0; - else if (M_AXI_RVALID && M_AXI_RREADY && rfifo_lock - && !S_AXI_ARREADY - && r_arid == gk[IW-1:0] - &&(!faulty_read_return && !o_read_fault) - && M_AXI_RRESP == EXOKAY) - r_lock_active <= 1; - else if (M_AXI_BVALID && M_AXI_BREADY && wfifo_lock - && r_awid == gk[IW-1:0] - && (S_AXI_ARREADY - || r_arid != gk[IW-1:0] - || !r_arlock) - && M_AXI_BRESP == OKAY) - r_lock_active <= 0; - else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLOCK - && S_AXI_ARID == gk[IW-1:0]) - r_lock_active <= 0; - - assign lock_active[gk] = r_lock_active; - end - // }}} - end else begin : LOCK_NEVER_ACTIVE - // {{{ - assign lock_active = 0; - - // Keep Verilator happy - // Verilator lint_off UNUSED - wire unused_lock; - assign unused_lock = &{ 1'b0, wfifo_lock }; - // Verilator lint_on UNUSED - // }}} - end endgenerate - // }}} - - // rfifo_first - // {{{ - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !OPT_EXCLUSIVE) - rfifo_first <= 1'b0; - else if (S_AXI_ARVALID && S_AXI_ARREADY) - rfifo_first <= 1'b1; - else if (M_AXI_RVALID && M_AXI_RREADY) - rfifo_first <= 1'b0; - else if (o_read_fault) - rfifo_first <= 1'b0; - // }}} - - // 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 : GEN_SELFRESET - // {{{ - // Declarations - // {{{ - reg [4:0] reset_counter; - reg r_clear_fault, w_clear_fault; - wire reset_timeout; - // }}} - - // 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; - // }}} - - assign 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) - w_clear_fault = 0; - else if (raddr_valid || waddr_valid) - w_clear_fault = 0; - else - w_clear_fault = r_clear_fault; - - assign clear_fault = w_clear_fault; - // }}} - - // }}} - end else begin : NO_SELFRESET - // {{{ - always @(*) - M_AXI_ARESETN = S_AXI_ARESETN; - assign clear_fault = 0; - // }}} - end endgenerate - // }}} - - // Make Verilator happy - // {{{ - // Verilator lint_off UNUSED - wire unused; - assign unused = &{ 1'b0 }; - // Verilator lint_on UNUSED - // }}} -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -// -// 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 - // {{{ - .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), - // }}} - // Write response channel - // {{{ - .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_rvalid(S_AXI_RVALID), - .i_axi_rready(S_AXI_RREADY), - .i_axi_rid(S_AXI_RID), - .i_axi_rdata(S_AXI_RDATA), - .i_axi_rresp(S_AXI_RRESP), - .i_axi_rlast(S_AXI_RLAST), - // }}} - // Formal induction values - // {{{ - .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) - begin - assert(1 || S_AXI_AWREADY || !M_AXI_ARESETN || !S_AXI_ARESETN); - end 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)) - begin - assert(S_AXI_AWREADY == !OPT_SELF_RESET); - end else if (f_axi_wr_pending > 0) - begin - assert(!S_AXI_AWREADY); - end else if (s_wbursts) - begin - assert(!S_AXI_AWREADY); - end else if (!OPT_SELF_RESET) - begin - assert(S_AXI_AWREADY); - end else if (!o_write_fault && !o_read_fault) - assert(S_AXI_AWREADY || OPT_SELF_RESET); - - always @(*) - if (f_axi_wr_pending > 0) - begin - assert(s_wbursts == 0); - end else if (f_axi_awr_nbursts > 0) - begin - assert((s_wbursts ? 1:0) == f_axi_awr_nbursts); - end 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) - begin - assert(waddr_valid); - end else if (f_axi_wr_pending > 0) - begin - if (!o_write_fault) - assert(M_AXI_WVALID && r_wvalid); - end - - always @(*) - if (!OPT_SELF_RESET) - begin - assert(waddr_valid == !S_AXI_AWREADY); - end else begin - // ... - assert(waddr_valid == (f_axi_awr_nbursts > 0)); - end - - always @(*) - if (S_AXI_ARESETN && !o_write_fault && f_axi_wr_pending > 0 && !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) - begin - assert(f_axi_wr_pending + (M_AXI_WVALID ? 1:0) + (r_wvalid ? 1:0) == m_wpending); - end 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) - begin - assert(waddr_valid == !S_AXI_AWREADY); - end 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) - begin - assert(rfifo_id == f_axi_rd_checkid); - end 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) - begin - assert(raddr_valid == !S_AXI_ARREADY); - end 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 - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Exclusive access property checking - // {{{ - // - //////////////////////////////////////////////////////////////////////// - // - // ... - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Cover properties - // - //////////////////////////////////////////////////////////////////////// - // - // }}} - - //////////////////////////////////////////////////////////////////////// - // - // Good interface check - // - //////////////////////////////////////////////////////////////////////// - // - // - generate if (F_OPT_FAULTLESS) - begin : ASSUME_FAULTLESS - // {{{ - // - // ... - // - - 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 - // {{{ - .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), - // }}} - // Write response channel - // {{{ - .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 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_rvalid(M_AXI_RVALID), - .i_axi_rready(M_AXI_RREADY), - .i_axi_rid(M_AXI_RID), - .i_axi_rdata(M_AXI_RDATA), - .i_axi_rresp(M_AXI_RRESP), - .i_axi_rlast(M_AXI_RLAST), - // }}} - // 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) - // - // ... - // }}} - // }}} - ); - - //////////////////////////////////////////////////////////////// - // - // Contract: If the downstream has no faults, then we - // shouldn't detect any here. - // {{{ - //////////////////////////////////////////////////////////////// - // - // - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!o_write_fault || !M_AXI_ARESETN); - end else - assert(!o_write_fault); - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!o_read_fault || !M_AXI_ARESETN); - end else - assert(!o_read_fault); - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!read_timeout || !M_AXI_ARESETN); - end else - assert(!read_timeout); - - always @(*) - if (OPT_SELF_RESET) - begin - assert(!write_timeout || !M_AXI_ARESETN); - end 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 - // }}} - //////////////////////////////////////////////////////////////// - // - // Exclusive address checking - // {{{ - //////////////////////////////////////////////////////////////// - // - // - - // - // - // ... - // - - //////////////////////////////////////////////////////////////// - // - // Cover checks - // {{{ - //////////////////////////////////////////////////////////////// - // - // - - // }}} - //////////////////////////////////////////////////////////////// - // - // "Careless" assumptions - // {{{ - //////////////////////////////////////////////////////////////// - // - // - 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) - begin - if (lock_failed) - assert(M_AXI_WSTRB == 0); - else - assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data); - end - // }}} - - // 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; - reg [4:0] f_rd_count, f_wr_count; - - // f_wr_count - // {{{ - initial f_wr_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault) - f_wr_count <= 0; - else if (S_AXI_BVALID && S_AXI_BREADY) - begin - if (!(&f_wr_count)) - f_wr_count <= f_wr_count + 1; - end - // }}} - - // f_dbl_wr_count - // {{{ - initial f_dbl_wr_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault||(S_AXI_AWVALID && S_AXI_AWLEN < 3)) - f_dbl_wr_count <= 0; - else if (S_AXI_BVALID && S_AXI_BREADY) - begin - if (!(&f_dbl_wr_count)) - f_dbl_wr_count <= f_dbl_wr_count + 1; - end - // }}} - - // f_rd_count - // {{{ - initial f_rd_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_read_fault) - f_rd_count <= 0; - else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST) - begin - if (!(&f_rd_count)) - f_rd_count <= f_rd_count + 1; - end - // }}} - - // f_dbl_rd_count - // {{{ - initial f_dbl_rd_count = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_read_fault||(S_AXI_ARVALID && S_AXI_ARLEN < 3)) - f_dbl_rd_count <= 0; - else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST) - begin - if (!(&f_dbl_rd_count)) - f_dbl_rd_count <= f_dbl_rd_count + 1; - end - // }}} - - // Can we complete a single write burst without fault? - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_wr_count > 1) && (!o_write_fault)); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_wr_count > 1) && (!o_write_fault)); - // }}} - - // Can we complete four write bursts without fault? (and return to idle) - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_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 @(*) - if (S_AXI_ARESETN) - cover((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)); - // }}} - - // Can we complete a single read burst without fault? - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_rd_count > 1) && (!o_read_fault)); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_rd_count > 1) && (!o_read_fault)); - // }}} - - // Can we complete four read bursts without fault? - // {{{ - always @(*) - if (S_AXI_ARESETN) - cover((f_rd_count > 3) && (f_axi_rd_nbursts == 0) - && !S_AXI_ARVALID && !S_AXI_RVALID); - - always @(*) - if (S_AXI_ARESETN) - cover((f_dbl_rd_count > 3) && (f_axi_rd_nbursts == 0) - && !S_AXI_ARVALID && !S_AXI_RVALID); - // }}} -`endif -// }}} -endmodule -`ifndef YOSYS -`default_nettype wire -`endif |