| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: saxi_slave.v (Simulation properties of an AXI4 (full) slave) |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: This file contains a set of SVA properties designed to help |
| // verify whether or not an AXI4 core complies with the |
| // specification within a given simulation. As written, the properties are |
| // not designed for formal verification and may (or may not) work in a |
| // formal context. |
| // |
| // My intent is to base a set of formal properties, useful for verifying |
| // a design using induction, off of these properties. |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // Copyright (C) 2020, Gisselquist Technology, LLC |
| // {{{ |
| // This file is part of the WB2AXIP project. |
| // |
| // The WB2AXIP project contains free software and gateware, licensed under the |
| // Apache License, Version 2.0 (the "License"). You may not use this project, |
| // or this file, except in compliance with the License. You may obtain a copy |
| // of the License at |
| // |
| // http://www.apache.org/licenses/LICENSE-2.0 |
| // |
| // Unless required by applicable law or agreed to in writing, software |
| // distributed under the License is distributed on an "AS IS" BASIS, WITHOUT |
| // WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the |
| // License for the specific language governing permissions and limitations |
| // under the License. |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // |
| `default_nettype none |
| // }}} |
| module saxi_slave #( |
| // {{{ |
| // AXI ID width |
| parameter C_AXI_ID_WIDTH = 3, |
| // Data width |
| parameter C_AXI_DATA_WIDTH = 128, |
| parameter C_AXI_ADDR_WIDTH = 28, |
| // OPT_MAXBURST - Maximum burst length, minus 1 |
| parameter [7:0] OPT_MAXBURST = 8'hff, |
| // Exclusive access allowed |
| parameter [0:0] OPT_EXCLUSIVE = 1, |
| // User design uses async resets -- not the default |
| parameter [0:0] OPT_ASYNC_RESET = 0, |
| // F_OPT_ASSUME_RESET, if set, will cause the design to |
| // *assume* the existence of a correct reset, rather than |
| // asserting it. (No difference under simulation.) It is |
| // appropriate anytime the reset logic is outside of the |
| /// circuit being examined |
| parameter [0:0] F_OPT_ASSUME_RESET = 1'b1, |
| // F_OPT_RESET_WIDTH -- insist on a minimum reset width. |
| // (Xilinx recommends a minimum width of 16 clocks. The |
| // AXI specification isn't that specific.) |
| parameter [0:0] F_OPT_RESET_WIDTH = 1'b1, |
| // F_LGDEPTH is the number of bits necessary to count the |
| // maximum number of items in flight. |
| parameter F_LGDEPTH = 10, |
| // MAXSTALL -- the maximum number of stall cycles the slave can |
| // make the master wait. |
| parameter [(F_LGDEPTH-1):0] F_AXI_MAXSTALL = 3, |
| // MAXRSTALL (reverse stall) -- the maximum number of stall |
| // cycles the master can make the slave wait |
| parameter [(F_LGDEPTH-1):0] F_AXI_MAXRSTALL= 3, |
| // MAXDELAY -- maximum number of clock cycles to wait for an |
| // accepted packet to be returned. |
| parameter [(F_LGDEPTH-1):0] F_AXI_MAXDELAY = 3, |
| // F_OPT_BURSTS -- true if the maximum burst length is longer |
| // than a single beat |
| localparam [0:0] F_OPT_BURSTS = (OPT_MAXBURST != 0), |
| // IW, DW, AW, and NUM_IDS are just short-hand notations |
| localparam IW = C_AXI_ID_WIDTH, |
| localparam DW = C_AXI_DATA_WIDTH, |
| localparam AW = C_AXI_ADDR_WIDTH, |
| localparam NUM_IDS = (1<<C_AXI_ID_WIDTH) |
| // }}} |
| ) ( |
| // {{{ |
| input wire i_clk, // System clock |
| input wire i_axi_aresetn, |
| |
| // AXI write address channel signals |
| // {{{ |
| input wire i_axi_awvalid, |
| input wire i_axi_awready, |
| input wire [IW-1:0] i_axi_awid, |
| input wire [AW-1:0] i_axi_awaddr, |
| input wire [7:0] i_axi_awlen, |
| input wire [2:0] i_axi_awsize, |
| input wire [1:0] i_axi_awburst, |
| input wire i_axi_awlock, |
| input wire [3:0] i_axi_awcache, |
| input wire [2:0] i_axi_awprot, |
| input wire [3:0] i_axi_awqos, |
| // }}} |
| // AXI write data channel signals |
| // {{{ |
| input wire i_axi_wvalid, |
| input wire i_axi_wready, |
| input wire [DW-1:0] i_axi_wdata, |
| input wire [DW/8-1:0] i_axi_wstrb, |
| input wire i_axi_wlast, |
| // }}} |
| // AXI write response channel signals |
| // {{{ |
| input wire i_axi_bvalid, |
| input wire i_axi_bready, |
| input wire [IW-1:0] i_axi_bid, |
| input wire [1:0] i_axi_bresp, |
| // }}} |
| // AXI read address channel signals |
| // {{{ |
| input wire i_axi_arvalid, |
| input wire i_axi_arready, |
| input wire [IW-1:0] i_axi_arid, |
| input wire [AW-1:0] i_axi_araddr, |
| input wire [7:0] i_axi_arlen, |
| input wire [2:0] i_axi_arsize, |
| input wire [1:0] i_axi_arburst, |
| input wire [0:0] i_axi_arlock, |
| input wire [3:0] i_axi_arcache, |
| input wire [2:0] i_axi_arprot, |
| input wire [3:0] i_axi_arqos, |
| // }}} |
| // AXI read data channel signals |
| // {{{ |
| input wire i_axi_rvalid, |
| input wire i_axi_rready, |
| input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, |
| input wire [DW-1:0] i_axi_rdata, |
| input wire i_axi_rlast, |
| input wire [1:0] i_axi_rresp |
| // }}} |
| // }}} |
| ); |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Parameter declarations |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| localparam [1:0] EXOKAY = 2'b01; |
| localparam F_AXI_MAXWAIT = F_AXI_MAXSTALL; |
| |
| // Because of the nature and size of bursts, which can be up to |
| // 256 in length (AxLEN), the F_LGDEPTH parameter necessary to capture |
| // this *must* be at least 8 bits wide |
| always @(*) |
| assert(F_LGDEPTH > 8); |
| |
| // Only power of two data sizes are supported from 8-bits on up to |
| // 1024 |
| always @(*) |
| assert((DW == 8) |
| ||(DW == 16) |
| ||(DW == 32) |
| ||(DW == 64) |
| ||(DW == 128) |
| ||(DW == 256) |
| ||(DW == 512) |
| ||(DW == 1024)); |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Internal register and wire declarations |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req, |
| axi_rd_err, axi_wr_err; |
| // |
| assign axi_ard_req = (i_axi_arvalid)&&(i_axi_arready); |
| assign axi_awr_req = (i_axi_awvalid)&&(i_axi_awready); |
| assign axi_wr_req = (i_axi_wvalid )&&(i_axi_wready); |
| // |
| assign axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready); |
| assign axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready); |
| assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]); |
| assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]); |
| |
| // |
| reg [F_LGDEPTH-1:0] f_axi_awr_nbursts; |
| reg [9-1:0] f_axi_wr_pending; |
| reg [F_LGDEPTH-1:0] f_axi_rd_nbursts; |
| reg [F_LGDEPTH-1:0] f_axi_rd_outstanding; |
| // |
| reg awfifo_read; |
| wire awfifo_full, awfifo_empty; |
| wire [F_LGDEPTH:0] awfifo_fill; |
| wire [C_AXI_ID_WIDTH-1:0] awfifo_id; |
| wire [C_AXI_ADDR_WIDTH-1:0] awfifo_addr; |
| wire [7:0] awfifo_len; |
| wire [1:0] awfifo_burst; |
| wire [2:0] awfifo_size; |
| wire awfifo_lock; |
| wire [3:0] awfifo_cache; |
| wire [2:0] awfifo_prot; |
| wire [3:0] awfifo_qos; |
| |
| reg [C_AXI_ID_WIDTH-1:0] f_axi_wr_this_id; |
| reg [C_AXI_ADDR_WIDTH-1:0] f_axi_wr_this_addr; |
| reg [7:0] f_axi_wr_this_len; |
| reg [1:0] f_axi_wr_this_burst; |
| reg [2:0] f_axi_wr_this_size; |
| reg f_axi_wr_this_lock; |
| reg [3:0] f_axi_wr_this_cache; |
| reg [2:0] f_axi_wr_this_prot; |
| reg [3:0] f_axi_wr_this_qos; |
| |
| reg [C_AXI_ID_WIDTH-1:0] r_axi_wr_id; |
| reg [C_AXI_ADDR_WIDTH-1:0] r_axi_wr_addr; |
| reg [7:0] r_axi_wr_len; |
| reg [1:0] r_axi_wr_burst; |
| reg [2:0] r_axi_wr_size; |
| reg r_axi_wr_lock; |
| reg [3:0] r_axi_wr_cache; |
| reg [2:0] r_axi_wr_prot; |
| reg [3:0] r_axi_wr_qos; |
| wire [C_AXI_ADDR_WIDTH-1:0] next_write_addr; |
| wire [7:0] f_axi_wr_this_incr; |
| |
| reg [8:0] r_wr_pending; |
| |
| reg wfifo_read; |
| wire wfifo_full, wfifo_empty; |
| wire [F_LGDEPTH:0] wfifo_fill; |
| wire [C_AXI_DATA_WIDTH-1:0] wfifo_data; |
| wire [C_AXI_DATA_WIDTH/8-1:0] wfifo_strb; |
| wire wfifo_last; |
| wire valid_iwaddr, // Incoming write address |
| valid_iraddr; |
| reg f_past_valid; |
| reg awr_aligned, |
| ard_aligned; |
| wire [AW-1:0] next_rd_addr; |
| |
| reg wstb_valid; |
| |
| genvar gk; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Pre-setup |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Within the slave core, we will *assume* properties from the master, |
| // and *assert* properties of signals coming from the slave and |
| // returning to the master. This order will be reversed within the |
| // master, and the following two definitions help us do that. |
| `define ASSUME assume |
| `define SLAVE_ASSUME assume |
| `define SLAVE_ASSERT assert |
| |
| // f_past_valid |
| // {{{ |
| initial f_past_valid = 1'b0; |
| always @(posedge i_clk) |
| f_past_valid <= 1'b1; |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Reset properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Insist that the reset signal start out asserted (negative), and |
| // remain so for 16 clocks. |
| // |
| |
| // The reset should be active initially |
| // {{{ |
| generate if (F_OPT_ASSUME_RESET) |
| begin : ASSUME_INITIAL_RESET |
| |
| `ASSUME property (@(posedge i_clk) |
| !f_past_valid |-> !i_axi_aresetn); |
| |
| end else begin : ASSERT_INITIAL_RESET |
| |
| assert property (@(posedge i_clk) |
| !f_past_valid |-> !i_axi_aresetn); |
| |
| end endgenerate |
| // }}} |
| |
| // If !F_OPT_NO_RESET, insist on a minimum 16-clock reset |
| // {{{ |
| generate if (F_OPT_ASSUME_RESET && F_OPT_RESET_WIDTH > 1) |
| begin |
| `ASSUME property (@(posedge i_clk) |
| (!f_past_valid || $fell(i_axi_aresetn)) |
| |-> !i_axi_aresetn [*F_OPT_RESET_WIDTH]); |
| |
| end else if (F_OPT_RESET_WIDTH > 1) |
| begin |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| (!f_past_valid || $fell(i_axi_aresetn)) |
| |-> !i_axi_aresetn [*F_OPT_RESET_WIDTH]); |
| |
| end endgenerate |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Clear everything on a reset |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| !i_axi_aresetn |=> !i_axi_awvalid && !i_axi_wvalid |
| && !i_axi_arvalid); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| !i_axi_aresetn |=> !i_axi_bvalid && !i_axi_rvalid); |
| |
| generate if (OPT_ASYNC_RESET) |
| begin : ASYNC_RESET_CHECKING |
| // {{{ |
| property ASYNC_CLEAR_REQUEST_ON_RESET; |
| @(posedge i_clk) |
| !i_axi_aresetn |-> !i_axi_awvalid && !i_axi_wvalid |
| && !i_axi_arvalid; |
| endproperty |
| |
| property ASYNC_CLEAR_RETURN_ON_RESET; |
| @(posedge i_clk) |
| !i_axi_aresetn |-> !i_axi_bvalid && !i_axi_rvalid; |
| endproperty |
| |
| `SLAVE_ASSUME property(ASYNC_CLEAR_REQUEST_ON_RESET); |
| `SLAVE_ASSERT property(ASYNC_CLEAR_RETURN_ON_RESET); |
| // }}} |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Stability properties--what happens if valid and not ready |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Assume any response from the bus will not change prior to that |
| // response being accepted |
| |
| // Write address channel |
| // {{{ |
| property STABLE_AW; |
| @(posedge i_clk) |
| i_axi_aresetn && i_axi_awvalid && !i_axi_awready |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_awvalid |
| && $stable({ i_axi_awid, i_axi_awaddr, i_axi_awlen, |
| i_axi_awsize, i_axi_awburst, i_axi_awlock, |
| i_axi_awcache, i_axi_awprot, i_axi_awqos }); |
| endproperty |
| // }}} |
| |
| // Write data channel |
| // {{{ |
| property STABLE_W; |
| @(posedge i_clk) |
| i_axi_aresetn && i_axi_wvalid && !i_axi_wready |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_wvalid |
| && $stable({ i_axi_wdata, i_axi_wstrb, i_axi_wlast }); |
| endproperty |
| // }}} |
| |
| // Write return channel |
| // {{{ |
| property STABLE_B; |
| @(posedge i_clk) |
| i_axi_aresetn && i_axi_bvalid && !i_axi_bready |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_bvalid |
| && $stable({ i_axi_bid, i_axi_bresp }); |
| endproperty |
| // }}} |
| |
| // Read address channel |
| // {{{ |
| property STABLE_AR; |
| @(posedge i_clk) |
| i_axi_aresetn && i_axi_arvalid && !i_axi_arready |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_arvalid |
| && $stable({ i_axi_arid, i_axi_araddr, i_axi_arlen, |
| i_axi_arsize, i_axi_arburst, i_axi_arlock, |
| i_axi_arcache, i_axi_arprot, i_axi_arqos }); |
| endproperty |
| // }}} |
| |
| // Read return channel |
| // {{{ |
| property STABLE_R; |
| @(posedge i_clk) |
| i_axi_aresetn && i_axi_rvalid && !i_axi_rready |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_rvalid |
| && $stable({ i_axi_rid, i_axi_rdata, i_axi_rlast, |
| i_axi_rresp }); |
| endproperty |
| // }}} |
| |
| `SLAVE_ASSUME property(STABLE_AW); |
| `SLAVE_ASSUME property(STABLE_W); |
| `SLAVE_ASSUME property(STABLE_AR); |
| |
| `SLAVE_ASSERT property(STABLE_B); |
| `SLAVE_ASSERT property(STABLE_R); |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Insist upon a maximum number of stalls before a request is accepted |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| generate if (F_AXI_MAXWAIT > 0) |
| begin : CHECK_STALL_COUNT |
| |
| // AXI write address channel |
| // {{{ |
| // Insist that AW channel can stall no more than F_AXI_MAXWAIT |
| // cycles before AWREADY is raised. However, if |
| // BVALID && !BREADY, then the slave has a reason why it might |
| // not want to accepting any more transactions. Similarly, |
| // many cores will only ever accept one request at a time, |
| // hence we won't count things as stalls if we are still |
| // waiting on write data--that's handled in another assertion |
| // below. |
| |
| property MAX_AW_STALLS; |
| @(posedge i_clk) |
| disable iff (!i_axi_aresetn || f_axi_wr_pending > 0) |
| i_axi_awvalid && !i_axi_awready [*F_AXI_MAXWAIT] |
| |=> i_axi_awready; |
| endproperty |
| |
| `SLAVE_ASSERT property(MAX_AW_STALLS); |
| // }}} |
| |
| // AXI write data channel |
| // {{{ |
| // Insist that the write data channel be stalled no more than |
| // F_AXI_MAXWAIT cycles. Since things can back up if |
| // BVALID & !BREADY, we avoid counting clock cycles in that |
| // circumstance |
| |
| property MAX_WREADY_STALLS; |
| @(posedge i_clk) |
| disable iff (!i_axi_aresetn || f_axi_wr_pending == 0 |
| || (i_axi_bvalid && !i_axi_bready)) |
| i_axi_wvalid && !i_axi_wready [*F_AXI_MAXWAIT] |
| |=> i_axi_wready; |
| endproperty |
| |
| `SLAVE_ASSERT property(MAX_WREADY_STALLS); |
| // }}} |
| |
| // AXI read address channel |
| // {{{ |
| // Similar to the first two above, once the master raises |
| // ARVALID, insist that the slave accept the read address |
| // request within a minimum number of clock cycles. |
| // Exceptions include any time RVALID is true, since that can |
| // back up the whole system, and any time the number of bursts |
| // is greater than zero, since many slaves can only accept one |
| // request at a time. |
| |
| property MAX_AR_STALLS; |
| @(posedge i_clk) |
| disable iff (!i_axi_aresetn || f_axi_rd_nbursts > 0) |
| i_axi_arvalid && !i_axi_arready [*F_AXI_MAXWAIT] |
| |=> i_axi_arready; |
| endproperty |
| |
| `SLAVE_ASSERT property(MAX_AR_STALLS); |
| // }}} |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Insist upon a maximum delay before any response is accepted |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Note that this is a *response* channel property, so it is separate |
| // from the earlier properties in case you wish to control it |
| // separately. For example, an interconnect might be forced to let a |
| // channel wait indefinitely for access, but it might not be |
| // appropriate to require the response to be able to wait indefinitely |
| // as well. So, here we check the response time. |
| // |
| // |
| |
| generate if (F_AXI_MAXRSTALL > 0) |
| begin : CHECK_RESPONSE_STALLS |
| // AXI write channel valid |
| // {{{ |
| // The first master stall check: guarantee that the master |
| // provides the required write data in fairly short order, |
| // and without much delay. That is, once AWVALID && AWREADY |
| // are true, the slave needs to provide the W* values. |
| // This is the only "forward" property check among our response |
| // channel checks, since it's a master and not a slave property. |
| |
| property MAX_WDATA_STALLS; |
| @(posedge i_clk) |
| i_axi_aresetn |
| && (!i_axi_bvalid || i_axi_bready) |
| && (f_axi_wr_pending > 0) |
| && (!i_axi_wvalid) [*F_AXI_MAXRSTALL] |
| |=> i_axi_wvalid; |
| endproperty |
| |
| `SLAVE_ASSUME property(MAX_WDATA_STALLS); |
| // }}} |
| |
| // AXI write response channel |
| // {{{ |
| // Insist on a maximum number of clocks that BVALID can be |
| // high while BREADY is low |
| property MAX_B_STALLS; |
| @(posedge i_clk) |
| i_axi_bvalid && !i_axi_bready [*F_AXI_MAXRSTALL] |
| |=> i_axi_bready; |
| endproperty |
| |
| `SLAVE_ASSUME property(MAX_B_STALLS); |
| // /}}} |
| |
| // AXI read response channel |
| // {{{ |
| // Insist on a maximum number of clocks that RVALID can be |
| // high while RREADY is low |
| property MAX_R_STALLS; |
| @(posedge i_clk) |
| i_axi_rvalid && !i_axi_rready [*F_AXI_MAXRSTALL] |
| |=> i_axi_rready; |
| endproperty |
| |
| `SLAVE_ASSUME property(MAX_R_STALLS); |
| // }}} |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Write property checking |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Validate the incoming address channel packet |
| // {{{ |
| faxi_valaddr #(.C_AXI_DATA_WIDTH(DW), .C_AXI_ADDR_WIDTH(AW), |
| .OPT_MAXBURST(OPT_MAXBURST), |
| .OPT_EXCLUSIVE(OPT_EXCLUSIVE), |
| .OPT_NARROW_BURST(1'b1)) |
| f_wraddr_validate(i_axi_awaddr, i_axi_awlen, i_axi_awsize, |
| i_axi_awburst, i_axi_awlock, |
| 1'b1, awr_aligned, valid_iwaddr); |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| i_axi_awvalid |-> valid_iwaddr); |
| // }}} |
| |
| // Write address request FIFO |
| // {{{ |
| // Queue write address requests so we can process them one packet |
| // at a time. |
| sfifo #( |
| // {{{ |
| .BW(C_AXI_ID_WIDTH + C_AXI_ADDR_WIDTH + 8 + 2 + 3+1+4+3+4), |
| .LGFLEN(F_LGDEPTH), |
| .OPT_ASYNC_READ(1'b0), |
| .OPT_WRITE_ON_FULL(1'b1), |
| .OPT_READ_ON_EMPTY(1'b1) |
| // }}} |
| ) awrequests ( |
| // {{{ |
| .i_clk(i_clk), .i_reset(!i_axi_aresetn), |
| .i_wr(i_axi_awvalid && i_axi_awready), |
| .i_data({ i_axi_awid, i_axi_awaddr, i_axi_awlen, |
| i_axi_awburst, i_axi_awsize, i_axi_awlock, |
| i_axi_awcache, i_axi_awprot, i_axi_awqos }), |
| .o_full(awfifo_full), .o_fill(awfifo_fill), |
| .i_rd(awfifo_read), |
| .o_data({ awfifo_id, awfifo_addr, awfifo_len, |
| awfifo_burst, awfifo_size, awfifo_lock, |
| awfifo_cache, awfifo_prot, awfifo_qos }), |
| .o_empty(awfifo_empty) |
| // }}} |
| ); |
| |
| always @(*) |
| awfifo_read = (r_wr_pending == 0); |
| // }}} |
| |
| // Write data FIFO |
| // {{{ |
| // In AXI, the write data can come before the address. In such |
| // circumstances, you need to hold on to that data in a queue (FIFO) |
| // until the address is available so that you can compare the two |
| // against each other for validity. |
| sfifo #( |
| // {{{ |
| .BW(C_AXI_DATA_WIDTH + (C_AXI_DATA_WIDTH/8) + 1), |
| .LGFLEN(F_LGDEPTH), |
| .OPT_ASYNC_READ(1'b0), |
| .OPT_WRITE_ON_FULL(1'b1), |
| .OPT_READ_ON_EMPTY(1'b1) |
| // }}} |
| ) wrequests ( |
| // {{{ |
| .i_clk(i_clk), .i_reset(!i_axi_aresetn), |
| .i_wr(i_axi_wvalid && i_axi_wready), |
| .i_data({ i_axi_wdata, i_axi_wstrb, i_axi_wlast }), |
| .o_full(wfifo_full), .o_fill(wfifo_fill), |
| .i_rd(wfifo_read), |
| .o_data({ wfifo_data, wfifo_strb, wfifo_last }), |
| .o_empty(wfifo_empty) |
| // }}} |
| ); |
| |
| always @(*) |
| wfifo_read = (r_wr_pending > 0)||(awfifo_read && !awfifo_empty); |
| // }}} |
| |
| // Make sure AWLOCK is low if !OPT_EXCLUSIVE |
| // {{{ |
| generate if (!OPT_EXCLUSIVE) |
| begin |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| (!i_axi_awvalid || !i_axi_awlock)); |
| |
| end endgenerate |
| // }}} |
| |
| // Build f_axi_wr_this_* |
| // {{{ |
| always @(*) |
| if (r_wr_pending == 0) |
| begin |
| f_axi_wr_this_id = awfifo_id; |
| f_axi_wr_this_addr = awfifo_addr; |
| f_axi_wr_this_len = awfifo_len; |
| f_axi_wr_this_burst = awfifo_burst; |
| f_axi_wr_this_size = awfifo_size; |
| f_axi_wr_this_lock = awfifo_lock; |
| f_axi_wr_this_cache = awfifo_cache; |
| f_axi_wr_this_prot = awfifo_prot; |
| f_axi_wr_this_qos = awfifo_qos; |
| end else begin |
| f_axi_wr_this_id = r_axi_wr_id; |
| f_axi_wr_this_addr = r_axi_wr_addr; |
| f_axi_wr_this_len = r_axi_wr_len; |
| f_axi_wr_this_burst = r_axi_wr_burst; |
| f_axi_wr_this_size = r_axi_wr_size; |
| f_axi_wr_this_lock = r_axi_wr_lock; |
| f_axi_wr_this_cache = r_axi_wr_cache; |
| f_axi_wr_this_prot = r_axi_wr_prot; |
| f_axi_wr_this_qos = r_axi_wr_qos; |
| end |
| // }}} |
| |
| // r_axi_wr_* |
| // {{{ |
| initial r_wr_pending = 0; |
| always @(posedge i_clk) |
| begin |
| if (awfifo_read && !awfifo_empty) |
| begin |
| r_axi_wr_id <= awfifo_id; |
| r_axi_wr_addr <= awfifo_addr; |
| r_axi_wr_len <= awfifo_len; |
| r_axi_wr_burst<= awfifo_burst; |
| r_axi_wr_size <= awfifo_size; |
| r_axi_wr_lock <= awfifo_lock; |
| r_axi_wr_cache<= awfifo_cache; |
| r_axi_wr_prot <= awfifo_prot; |
| r_axi_wr_qos <= awfifo_qos; |
| |
| r_wr_pending <= awfifo_len + 1; |
| if (wfifo_read && !wfifo_empty) |
| begin |
| r_axi_wr_addr <= next_write_addr; |
| r_wr_pending <= awfifo_len; |
| end |
| end else if (wfifo_read && !wfifo_empty) |
| begin |
| r_axi_wr_addr <= next_write_addr; |
| r_wr_pending <= r_wr_pending - 1; |
| end |
| |
| if (!i_axi_aresetn) |
| r_wr_pending <= 0; |
| end |
| // }}} |
| |
| // f_axi_wr_pending |
| // {{{ |
| always @(*) |
| if (r_wr_pending == 0) |
| begin |
| f_axi_wr_pending = awfifo_len + 1; |
| if (awfifo_empty || !awfifo_read) |
| f_axi_wr_pending = 0; |
| end else |
| f_axi_wr_pending = r_wr_pending; |
| // }}} |
| |
| // next_write_addr |
| // {{{ |
| faxi_addr #(.AW(AW)) |
| get_next_write_addr( |
| f_axi_wr_this_addr, f_axi_wr_this_size, f_axi_wr_this_burst, |
| f_axi_wr_this_len, |
| f_axi_wr_this_incr, next_write_addr); |
| // }}} |
| |
| // Check WSTRB |
| // {{{ |
| faxi_wstrb #(.C_AXI_DATA_WIDTH(DW)) |
| f_wstrbck (f_axi_wr_this_addr, f_axi_wr_this_size, |
| wfifo_strb, wstb_valid); |
| |
| // Insist the only the appropriate bits be valid |
| // For example, if the lower address bit is one, then the |
| // strobe LSB cannot be 1, but must be zero. This is just |
| // enforcing the rules of the sub-address which must match |
| // the write strobe. An STRB of 0 is always allowed. |
| // |
| always @(*) |
| if (!wfifo_empty) |
| `SLAVE_ASSUME(wstb_valid); |
| // }}} |
| |
| // Check WLAST |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| !wfifo_empty && r_wr_pending > 0 |
| |-> ((r_wr_pending == 1) == wfifo_last)); |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| !wfifo_empty && r_wr_pending == 0 && !awfifo_empty |
| |-> ((awfifo_len == 0) == wfifo_last)); |
| |
| // Check BID and BRESP |
| // {{{ |
| generate for(gk=0; gk<NUM_IDS; gk=gk+1) |
| begin : CHECK_BID |
| // {{{ |
| |
| // Register/net declarations |
| // {{{ |
| wire [F_LGDEPTH:0] bid_count; |
| reg block_fifo_write, block_fifo_check, |
| block_fifo_read; |
| wire block_possible; |
| wire block_fifo_empty; |
| // }}} |
| |
| always @(*) |
| block_fifo_write = (wfifo_read && !wfifo_empty |
| && wfifo_last && f_axi_wr_this_id == gk); |
| |
| always @(*) |
| block_fifo_check = (i_axi_bvalid && i_axi_bid == gk); |
| |
| always @(*) |
| block_fifo_read = block_fifo_check && i_axi_bready; |
| |
| if (OPT_EXCLUSIVE) |
| begin : EXCLUSIVE_WRITE_RETURN_CHECK |
| // {{{ |
| wire block_fifo_full; |
| |
| sfifo #( |
| // {{{ |
| .BW(1), |
| .LGFLEN(F_LGDEPTH), |
| .OPT_ASYNC_READ(1'b0), |
| .OPT_WRITE_ON_FULL(1'b1), |
| .OPT_READ_ON_EMPTY(1'b0) |
| // }}} |
| ) block_fifo ( |
| // {{{ |
| .i_clk(i_clk), .i_reset(!i_axi_aresetn), |
| .i_wr(block_fifo_write), |
| .i_data(f_axi_wr_this_lock), |
| .o_full(block_fifo_full), .o_fill(bid_count), |
| .i_rd(block_fifo_read), |
| .o_data(block_possible), |
| .o_empty(block_fifo_empty) |
| // }}} |
| ); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| !block_possible |
| |-> !block_fifo_check || i_axi_bresp != EXOKAY); |
| // }}} |
| end else begin : NO_EXCLUSIVE_WRITE_RETURNS |
| // {{{ |
| reg [F_LGDEPTH-1:0] r_bid_count; |
| |
| initial r_bid_count = 0; |
| always @(posedge i_clk) |
| if (!i_axi_aresetn) |
| r_bid_count = 0; |
| else case ({ block_fifo_write, block_fifo_read }) |
| 2'b10: r_bid_count <= r_bid_count + 1; |
| 2'b01: r_bid_count <= r_bid_count - 1; |
| default: begin end |
| endcase |
| |
| assign block_fifo_empty = (r_bid_count == 0); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| !block_fifo_check || i_axi_bresp != EXOKAY); |
| // }}} |
| end |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| block_fifo_write && !block_fifo_read |
| |-> (bid_count != {(F_LGDEPTH){1'b1}})); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| block_fifo_check |-> !block_fifo_empty); |
| |
| // }}} |
| end endgenerate |
| // }}} |
| |
| // f_axi_awr_nbursts |
| // {{{ |
| // Count the number of outstanding BVALID's to expect |
| initial f_axi_awr_nbursts = 0; |
| always @(posedge i_clk) |
| if (!i_axi_aresetn) |
| f_axi_awr_nbursts <= 0; |
| else case({ (axi_awr_req), (axi_wr_ack) }) |
| 2'b10: f_axi_awr_nbursts <= f_axi_awr_nbursts + 1'b1; |
| 2'b01: f_axi_awr_nbursts <= f_axi_awr_nbursts - 1'b1; |
| default: begin end |
| endcase |
| // }}} |
| |
| // f_axi_rd_nbursts |
| // {{{ |
| // Count the number of reads bursts outstanding. This defines the |
| // number of RDVALID && RLAST's we expect to see before becoming idle |
| // |
| initial f_axi_rd_nbursts = 0; |
| always @(posedge i_clk) |
| if (!i_axi_aresetn) |
| f_axi_rd_nbursts <= 0; |
| else case({ (axi_ard_req), (axi_rd_ack)&&(i_axi_rlast) }) |
| 2'b01: f_axi_rd_nbursts <= f_axi_rd_nbursts - 1'b1; |
| 2'b10: f_axi_rd_nbursts <= f_axi_rd_nbursts + 1'b1; |
| endcase |
| // }}} |
| |
| // f_axi_rd_outstanding |
| // {{{ |
| // f_axi_rd_outstanding counts the number of RDVALID's we expect to |
| // see before becoming idle. This must always be greater than or |
| // equal to the number of RVALID & RLAST's counted above |
| // |
| initial f_axi_rd_outstanding = 0; |
| always @(posedge i_clk) |
| if (!i_axi_aresetn) |
| f_axi_rd_outstanding <= 0; |
| else case({ (axi_ard_req), (axi_rd_ack) }) |
| 2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1; |
| 2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + i_axi_arlen+1; |
| 2'b11: f_axi_rd_outstanding <= f_axi_rd_outstanding + i_axi_arlen; |
| endcase |
| // }}} |
| |
| // |
| // Do not let the number of outstanding requests overflow. |
| // {{{ |
| // This is a responsibility of both the master and the slave to never |
| // allow 2^F_LGDEPTH-1 requests (or more) to be outstanding. |
| // |
| assert property (@(posedge i_clk) |
| !i_axi_aresetn || f_axi_awr_nbursts < {(F_LGDEPTH){1'b1}}); |
| assert property (@(posedge i_clk) |
| !i_axi_aresetn || f_axi_wr_pending <= 256); |
| assert property (@(posedge i_clk) |
| !i_axi_aresetn || f_axi_rd_nbursts < {(F_LGDEPTH){1'b1}}); |
| assert property (@(posedge i_clk) |
| !i_axi_aresetn || f_axi_rd_outstanding < {(F_LGDEPTH){1'b1}}); |
| // }}} |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Read property checking |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| generate if (!OPT_EXCLUSIVE) |
| begin : NO_EXCLUSIVE_READS |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| (!i_axi_arvalid || !i_axi_arlock)); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| (!i_axi_rvalid || i_axi_rresp != EXOKAY)); |
| |
| end endgenerate |
| |
| // Validate the read address packet |
| // {{{ |
| faxi_valaddr #(.C_AXI_DATA_WIDTH(DW), .C_AXI_ADDR_WIDTH(AW), |
| .OPT_MAXBURST(OPT_MAXBURST), |
| .OPT_EXCLUSIVE(OPT_EXCLUSIVE), |
| .OPT_NARROW_BURST(1'b1)) |
| f_rdaddr_validate(i_axi_araddr, i_axi_arlen, |
| i_axi_arsize, i_axi_arburst, i_axi_arlock, |
| 1'b1, ard_aligned, valid_iraddr); |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| i_axi_arvalid |-> valid_iraddr); |
| // }}} |
| |
| // Read return handling must be done on a per-ID basis |
| generate for(gk=0; gk<NUM_IDS; gk=gk+1) |
| begin : PER_READ_ID_PROCESSING |
| // {{{ |
| |
| // Register/wire declarations |
| // {{{ |
| wire arfifo_empty, arfifo_full; |
| wire [F_LGDEPTH:0] arfifo_fill; |
| reg arfifo_write, arfifo_read; |
| |
| wire [C_AXI_ADDR_WIDTH-1:0] arfifo_addr; |
| wire [7:0] arfifo_len; |
| wire [1:0] arfifo_burst; |
| wire [2:0] arfifo_size; |
| wire arfifo_lock; |
| wire [3:0] arfifo_cache; |
| wire [2:0] arfifo_prot; |
| wire [3:0] arfifo_qos; |
| |
| reg [C_AXI_ADDR_WIDTH-1:0] f_axi_rd_this_addr; |
| reg [7:0] f_axi_rd_this_len; |
| reg [1:0] f_axi_rd_this_burst; |
| reg [2:0] f_axi_rd_this_size; |
| reg f_axi_rd_this_lock; |
| reg [3:0] f_axi_rd_this_cache; |
| reg [2:0] f_axi_rd_this_prot; |
| reg [3:0] f_axi_rd_this_qos; |
| |
| reg [C_AXI_ID_WIDTH-1:0] r_axi_rd_id; |
| reg [C_AXI_ADDR_WIDTH-1:0] r_axi_rd_addr; |
| reg [7:0] r_axi_rd_len; |
| reg [1:0] r_axi_rd_burst; |
| reg [2:0] r_axi_rd_size; |
| reg r_axi_rd_lock; |
| reg [3:0] r_axi_rd_cache; |
| reg [2:0] r_axi_rd_prot; |
| reg [3:0] r_axi_rd_qos; |
| wire [C_AXI_ADDR_WIDTH-1:0] next_read_addr; |
| wire [7:0] f_axi_rd_this_incr; |
| reg [8:0] r_rd_pending; |
| // }}} |
| |
| // Read address FIFO |
| // {{{ |
| // Record any read address request for comparing against the |
| // subsequent response |
| |
| // arfifo_write - Write on any address request |
| // {{{ |
| always @(*) |
| arfifo_write = i_axi_arvalid && i_axi_arready |
| && i_axi_arid == gk; |
| // }}} |
| |
| // arfifo_read |
| // {{{ |
| // Read if nothing we know of is pending, or if we just |
| // read the last value from the last burst. |
| always @(*) |
| arfifo_read = (r_rd_pending == 0) |
| || (i_axi_rvalid && i_axi_rready && i_axi_rlast |
| && i_axi_rid == gk); |
| // }}} |
| |
| sfifo #( |
| // {{{ |
| .BW(C_AXI_ADDR_WIDTH+8+2+3+1+4+3+4), |
| .LGFLEN(F_LGDEPTH), |
| .OPT_ASYNC_READ(1'b0), |
| .OPT_WRITE_ON_FULL(1'b1), |
| .OPT_READ_ON_EMPTY(1'b1) |
| // }}} |
| ) arrequests ( |
| // {{{ |
| .i_clk(i_clk), .i_reset(!i_axi_aresetn), |
| .i_wr(arfifo_write), |
| .i_data({ i_axi_araddr, i_axi_arlen, |
| i_axi_arburst, i_axi_arsize, i_axi_arlock, |
| i_axi_arcache, i_axi_arprot, i_axi_arqos }), |
| .o_full(arfifo_full), .o_fill(arfifo_fill), |
| .i_rd(arfifo_read), |
| .o_data({ arfifo_addr, arfifo_len, |
| arfifo_burst, arfifo_size, arfifo_lock, |
| arfifo_cache, arfifo_prot, arfifo_qos }), |
| .o_empty(arfifo_empty) |
| // }}} |
| ); |
| // }}} |
| |
| // f_axi_rd_this_* |
| // {{{ |
| // These record the current burst that is being returned by |
| // this ID (if any). The current burst might still be in the |
| // FIFO, so this is combinatorial. |
| always @(*) |
| if (r_rd_pending == 0) |
| begin |
| f_axi_rd_this_addr = arfifo_addr; |
| f_axi_rd_this_len = arfifo_len; |
| f_axi_rd_this_burst = arfifo_burst; |
| f_axi_rd_this_size = arfifo_size; |
| f_axi_rd_this_lock = arfifo_lock; |
| f_axi_rd_this_cache = arfifo_cache; |
| f_axi_rd_this_prot = arfifo_prot; |
| f_axi_rd_this_qos = arfifo_qos; |
| end else begin |
| f_axi_rd_this_addr = r_axi_rd_addr; |
| f_axi_rd_this_len = r_axi_rd_len; |
| f_axi_rd_this_burst = r_axi_rd_burst; |
| f_axi_rd_this_size = r_axi_rd_size; |
| f_axi_rd_this_lock = r_axi_rd_lock; |
| f_axi_rd_this_cache = r_axi_rd_cache; |
| f_axi_rd_this_prot = r_axi_rd_prot; |
| f_axi_rd_this_qos = r_axi_rd_qos; |
| end |
| // }}} |
| |
| // r_axi_rd_* |
| // {{{ |
| // Register the details of the next read burst to be returned. |
| // We'll adjust the pending value and the address along the |
| // way. Hence, the address should always point to the address |
| // of the next value to be read, and the r_rd_pending to the |
| // next item to be read. |
| |
| initial r_rd_pending = 0; |
| always @(posedge i_clk) |
| if (!i_axi_aresetn) |
| r_rd_pending <= 0; |
| else if (arfifo_read) |
| begin |
| r_rd_pending = arfifo_len + 1; |
| if (arfifo_empty) |
| r_rd_pending = 0; |
| end else if (i_axi_rvalid && i_axi_rready && i_axi_rid == gk |
| && r_rd_pending > 0) |
| r_rd_pending = r_rd_pending - 1; |
| |
| always @(posedge i_clk) |
| if (arfifo_read) |
| begin |
| r_axi_rd_addr = arfifo_addr; |
| r_axi_rd_len = arfifo_len; |
| r_axi_rd_burst = arfifo_burst; |
| r_axi_rd_size = arfifo_size; |
| r_axi_rd_lock = arfifo_lock; |
| r_axi_rd_cache = arfifo_cache; |
| r_axi_rd_prot = arfifo_prot; |
| r_axi_rd_qos = arfifo_qos; |
| end else if (i_axi_rvalid && i_axi_rready && i_axi_rid == gk |
| && r_rd_pending > 0) |
| r_axi_rd_addr= next_read_addr; |
| // }}} |
| |
| // next_read_addr |
| // {{{ |
| // Compute the next read address, after the current one, using |
| // the current burst values. |
| faxi_addr #(.AW(AW)) |
| get_next_read_addr( |
| f_axi_rd_this_addr, f_axi_rd_this_size, |
| f_axi_rd_this_burst, f_axi_rd_this_len, |
| f_axi_rd_this_incr, next_read_addr); |
| // }}} |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| i_axi_aresetn && i_axi_rvalid && i_axi_rid == gk |
| |-> (r_rd_pending > 0)); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| i_axi_aresetn && i_axi_rvalid && i_axi_rid == gk |
| |-> (i_axi_rlast == (r_rd_pending == 1))); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| i_axi_aresetn && i_axi_rvalid && i_axi_rid == gk |
| && !f_axi_rd_this_lock |-> i_axi_rresp != EXOKAY); |
| |
| // }}} |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Maximum response time delay |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Insist that all responses are returned in less than a maximum delay |
| // |
| // A unique feature to the backpressure mechanism within AXI is that |
| // we have to reset our delay count in the case of any push back, since |
| // the response can't move forward if the master isn't (yet) ready for |
| // it. |
| // |
| |
| generate if (F_AXI_MAXDELAY > 0) |
| begin : CHECK_MAX_DELAY |
| // {{{ |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| i_axi_aresetn && !i_axi_bvalid |
| && f_axi_awr_nbursts > awrfifo_fill |
| + ((f_axi_wr_pending>0) ? 1:0) |
| [*F_AXI_MAXDELAY-1] |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_bvalid); |
| |
| `SLAVE_ASSERT property (@(posedge i_clk) |
| i_axi_aresetn && !i_axi_rvalid |
| && (f_axi_rd_outstanding > 0) [*F_AXI_MAXDELAY-1] |
| ##1 (!OPT_ASYNC_RESET || i_axi_aresetn) |
| |-> i_axi_rvalid); |
| // }}} |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Exclusive properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| generate if (!OPT_EXCLUSIVE) |
| begin : EXCLUSIVE_DISALLOWED |
| // {{{ |
| // These properties are captured above |
| // }}} |
| end else begin : EXCLUSIVE_ACCESS_CHECKER |
| // {{{ |
| |
| // |
| // 1. Exclusive access burst lengths max out at 16 |
| // (Checked within valaddr) |
| // 2. Exclusive access bursts must be aligned |
| // (NOT CHECKED) |
| // 3. Write must take place when the read channel is idle (on |
| // this ID) -- (NOT CHECKED) |
| // (4. Further read accesses on this ID are not allowed) |
| // (NOT CHECKED) |
| // |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| i_axi_aresetn && i_axi_awvalid && i_axi_awlock |
| |-> !i_axi_awcache[0]); |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| i_axi_aresetn && i_axi_arvalid && i_axi_arlock |
| |-> !i_axi_arcache[0]); |
| |
| // }}} |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AxCACHE properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Table A4-5 ?? |
| // |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| i_axi_awvalid && !i_axi_awcache[1] |
| |-> i_axi_awcache[3:2] == 2'b00); |
| |
| `SLAVE_ASSUME property (@(posedge i_clk) |
| i_axi_arvalid && !i_axi_arcache[1] |
| |-> i_axi_arcache[3:2] == 2'b00); |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Option for no bursts, only single transactions |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| generate if (!F_OPT_BURSTS) |
| begin |
| |
| `SLAVE_ASSUME property(@(posedge i_clk) |
| i_axi_awvalid |-> i_axi_awlen == 0); |
| |
| `SLAVE_ASSUME property(@(posedge i_clk) |
| i_axi_wvalid |-> i_axi_wlast); |
| |
| `SLAVE_ASSUME property(@(posedge i_clk) |
| i_axi_arvalid |-> i_axi_arlen == 0); |
| |
| `SLAVE_ASSERT property(@(posedge i_clk) |
| i_axi_rvalid |-> i_axi_rlast); |
| |
| end endgenerate |
| // }}} |
| `undef SLAVE_ASSUME |
| `undef SLAVE_ASSERT |
| endmodule |