| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: axil2axis |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: Demonstrates a simple AXI-Lite interface to drive an AXI-Stream |
| // channel. This can then be used to debug DSP processing. |
| // |
| // Registers: This AXI-lite to AXI-Stream core supports four word-sized |
| // addresses. Byte enables are ignored. |
| // |
| // 2'b00, ADDR_SINK |
| // Writes to this register will send data to the stream master, |
| // with TLAST clear. Data goes first through a FIFO. If the |
| // FIFO is full, the write will stall. If it stalls OPT_TIMEOUT |
| // cycles, the write will fail and return a bus error. |
| // |
| // Reads from this register will return data from the stream slave, |
| // but without consuming it. Values read here may still be read |
| // from the ADDR_SOURCE register later. |
| // |
| // 2'b01, ADDR_SOURCE |
| // Writes to this register will send data downstream to the stream |
| // master as well, but this time with TLAST set. |
| // |
| // Reads from this register will accept a value from the stream |
| // slave interface. The read value contains TDATA. TLAST is |
| // ignored in this read. If you want access to TLAST, you can get |
| // it from the ADDR_FIFO register. |
| // |
| // If there is no data to be read, the read will not and does not |
| // stall. It will instead return a bus error. |
| // |
| // 2'b10, ADDR_STATS |
| // Since we can, we'll handle some statistics here. The top half |
| // word contains two counters: a 4-bit counter of TLAST's issued |
| // from the stream master, and a 12-bit counter of TDATA values |
| // issued. Neither counter includes data still contained in the |
| // FIFO. If the OPT_SOURCE option is clear, these values will |
| // always be zero. |
| // |
| // The second (bottom, or least-significant) halfword contains the |
| // same regarding the stream slave. If OPT_SINK is set, these |
| // counters count values read from the core. If OPT_SINK is clear, |
| // so that the stream sink is not truly implemented, then TREADY |
| // will be held high and the counter will just count values coming |
| // into the core never going into the FIFO. |
| // |
| // 2'b11, ADDR_FIFO |
| // Working with the core can be a challenge. You want to make |
| // certain that writing to the core doesn't hang the design, and |
| // that reading from the core doesn't cause a bus error. |
| // |
| // Bits 31:16 contain the number of items in the write FIFO, and |
| // bits 14:0 contain the number of items in the read FIFO. |
| // |
| // Bit 15 contains whether or not the next item to be read is |
| // the last item in a packet, i.e. with TLAST set. |
| // |
| // |
| // 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 axil2axis #( |
| // {{{ |
| // |
| // Size of the AXI-lite bus. These are fixed, since 1) AXI-lite |
| // is fixed at a width of 32-bits by Xilinx def'n, and 2) since |
| // we only ever have 4 configuration words. |
| parameter C_AXI_ADDR_WIDTH = 4, |
| localparam C_AXI_DATA_WIDTH = 32, |
| parameter C_AXIS_DATA_WIDTH = 16, |
| // |
| // OPT_SOURCE enables the AXI stream master logic. If not |
| // enabled, M_AXI_TVALID will be held at zero, and the stream |
| // master logic may be ignored. |
| parameter [0:0] OPT_SOURCE = 1'b1, |
| // |
| // OPT_SINK enables the AXI stream slave logic. If not enabled, |
| // reads will always return zero, and S_AXIS_TREADY will be |
| // held high. |
| parameter [0:0] OPT_SINK = 1'b1, |
| // |
| // If OPT_SIGN_EXTEND is set, values received will be sign |
| // extended to fill the full data width on read. Otherwise |
| // the most significant of any unused bits will remain clear. |
| parameter [0:0] OPT_SIGN_EXTEND = 1'b0, |
| // |
| // Data written to this core will be placed into a FIFO before |
| // entering the AXI stream master. LGFIFO is the log, based |
| // two, of the number of words in this FIFO. Similarly, data |
| // consumed by AXI stream slave contained in this core will go |
| // first into a read FIFO. Reads from the core will then return |
| // data from this FIFO, or a bus error if none is available. |
| parameter LGFIFO = 5, |
| // |
| // OPT_TIMEOUT, if non-zero, will allow writes to the stream |
| // master, or reads from the stream slave, to stall the core |
| // for OPT_TIMEOUT cycles for the stream to be ready. If the |
| // stream isn't ready at this time (i.e. if the write FIFO is |
| // still full, or the read FIFO still empty), the result will |
| // be returned as a bus error. Likewise, if OPT_TIMEOUT==0, |
| // the core will always return a bus error if ever the write |
| // FIFO is full or the read FIFO empty. |
| parameter OPT_TIMEOUT = 5, |
| // |
| // OPT_LOWPOWER sets outputs to zero if not valid. This applies |
| // to the AXI-lite bus, however, and not the AXI stream FIFOs, |
| // since those don't have LOWPOWER support (currently). |
| parameter [0:0] OPT_LOWPOWER = 0, |
| // |
| // This design currently ignores WSTRB, beyond checking that it |
| // is not zero. I see no easy way to add it. (I'll leave that |
| // to you to implement, if you wish.) |
| // parameter [0:0] OPT_WSTRB = 0, |
| // |
| localparam ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3 |
| // }}} |
| ) ( |
| // {{{ |
| input wire S_AXI_ACLK, |
| input wire S_AXI_ARESETN, |
| // AXI-lite signals |
| // {{{ |
| input wire S_AXI_AWVALID, |
| output wire S_AXI_AWREADY, |
| input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_AWADDR, |
| input wire [2:0] S_AXI_AWPROT, |
| // |
| input wire S_AXI_WVALID, |
| output wire S_AXI_WREADY, |
| input wire [C_AXI_DATA_WIDTH-1:0] S_AXI_WDATA, |
| input wire [C_AXI_DATA_WIDTH/8-1:0] S_AXI_WSTRB, |
| // |
| output wire S_AXI_BVALID, |
| input wire S_AXI_BREADY, |
| output wire [1:0] S_AXI_BRESP, |
| // |
| input wire S_AXI_ARVALID, |
| output wire S_AXI_ARREADY, |
| input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_ARADDR, |
| input wire [2:0] S_AXI_ARPROT, |
| // |
| output wire S_AXI_RVALID, |
| input wire S_AXI_RREADY, |
| output wire [C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA, |
| output wire [1:0] S_AXI_RRESP, |
| // }}} |
| // AXI stream slave (sink) signals |
| // {{{ |
| input wire S_AXIS_TVALID, |
| output reg S_AXIS_TREADY, |
| input wire [C_AXIS_DATA_WIDTH-1:0] S_AXIS_TDATA, |
| input wire S_AXIS_TLAST, |
| // }}} |
| // AXI stream master (source) signals |
| // {{{ |
| output reg M_AXIS_TVALID, |
| input wire M_AXIS_TREADY, |
| output reg [C_AXIS_DATA_WIDTH-1:0] M_AXIS_TDATA, |
| output reg M_AXIS_TLAST |
| // }}} |
| // }}} |
| ); |
| |
| localparam [1:0] ADDR_SINK = 2'b00, // Read from stream |
| ADDR_SOURCE = 2'b01, // Write, also sets TLAST |
| ADDR_STATS = 2'b10, |
| ADDR_FIFO = 2'b11; |
| localparam SW = C_AXIS_DATA_WIDTH; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Register/wire signal declarations |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| wire i_reset = !S_AXI_ARESETN; |
| |
| wire axil_write_ready; |
| wire [C_AXI_ADDR_WIDTH-ADDRLSB-1:0] awskd_addr; |
| // |
| wire [C_AXI_DATA_WIDTH-1:0] wskd_data; |
| wire [C_AXI_DATA_WIDTH/8-1:0] wskd_strb; |
| reg axil_bvalid, axil_berr; |
| // |
| wire axil_read_ready; |
| wire [C_AXI_ADDR_WIDTH-ADDRLSB-1:0] arskd_addr; |
| reg [C_AXI_DATA_WIDTH-1:0] axil_read_data; |
| reg axil_read_valid; |
| |
| wire awskd_valid, wskd_valid; |
| wire wfifo_full, wfifo_write, wfifo_empty; |
| wire [LGFIFO:0] wfifo_fill; |
| reg write_timeout; |
| |
| reg read_timeout; |
| reg axil_rerr; |
| reg [3:0] read_bursts_completed; |
| reg [11:0] reads_completed; |
| |
| reg [3:0] write_bursts_completed; |
| reg [11:0] writes_completed; |
| |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI-lite signaling |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| |
| // |
| // Write signaling |
| // |
| // {{{ |
| skidbuffer #(.OPT_OUTREG(0), |
| .OPT_LOWPOWER(OPT_LOWPOWER), |
| .DW(C_AXI_ADDR_WIDTH-ADDRLSB)) |
| axilawskid(// |
| .i_clk(S_AXI_ACLK), .i_reset(i_reset), |
| .i_valid(S_AXI_AWVALID), .o_ready(S_AXI_AWREADY), |
| .i_data(S_AXI_AWADDR[C_AXI_ADDR_WIDTH-1:ADDRLSB]), |
| .o_valid(awskd_valid), .i_ready(axil_write_ready), |
| .o_data(awskd_addr)); |
| |
| skidbuffer #(.OPT_OUTREG(0), |
| .OPT_LOWPOWER(OPT_LOWPOWER), |
| .DW(C_AXI_DATA_WIDTH+C_AXI_DATA_WIDTH/8)) |
| axilwskid(// |
| .i_clk(S_AXI_ACLK), .i_reset(i_reset), |
| .i_valid(S_AXI_WVALID), .o_ready(S_AXI_WREADY), |
| .i_data({ S_AXI_WDATA, S_AXI_WSTRB }), |
| .o_valid(wskd_valid), .i_ready(axil_write_ready), |
| .o_data({ wskd_data, wskd_strb })); |
| |
| assign axil_write_ready = awskd_valid && wskd_valid |
| && (!S_AXI_BVALID || S_AXI_BREADY) |
| && ((awskd_addr[1] != ADDR_SOURCE[1]) |
| || (!wfifo_full || write_timeout)); |
| |
| // |
| // Write timeout generation |
| // |
| // {{{ |
| generate if ((OPT_TIMEOUT > 1) && OPT_SOURCE) |
| begin |
| |
| reg [$clog2(OPT_TIMEOUT)-1:0] write_timer; |
| |
| initial write_timer = OPT_TIMEOUT-1; |
| initial write_timeout = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| write_timer <= OPT_TIMEOUT-1; |
| write_timeout<= 1'b0; |
| end else if (!awskd_valid || !wfifo_full || !wskd_valid |
| || (awskd_addr[1] != ADDR_SOURCE[1]) |
| || (S_AXI_BVALID && !S_AXI_BREADY)) |
| begin |
| write_timer <= OPT_TIMEOUT-1; |
| write_timeout<= 1'b0; |
| end else begin |
| if (write_timer > 0) |
| write_timer <= write_timer - 1; |
| write_timeout <= (write_timer <= 1); |
| end |
| |
| `ifdef FORMAL |
| always @(*) |
| assert(write_timer <= OPT_TIMEOUT-1); |
| always @(*) |
| assert(write_timeout == (write_timer == 0)); |
| `endif |
| end else begin |
| |
| always @(*) |
| write_timeout<= 1'b1; |
| |
| end endgenerate |
| // }}} |
| |
| |
| initial axil_bvalid = 0; |
| always @(posedge S_AXI_ACLK) |
| if (i_reset) |
| axil_bvalid <= 0; |
| else if (axil_write_ready) |
| axil_bvalid <= 1; |
| else if (S_AXI_BREADY) |
| axil_bvalid <= 0; |
| |
| assign S_AXI_BVALID = axil_bvalid; |
| |
| initial axil_berr = 0; |
| always @(posedge S_AXI_ACLK) |
| if (OPT_LOWPOWER && i_reset) |
| axil_berr <= 0; |
| else if (axil_write_ready) |
| axil_berr <= (wfifo_full)&&(awskd_addr[1]==ADDR_SOURCE[1]); |
| else if (OPT_LOWPOWER && S_AXI_BREADY) |
| axil_berr <= 1'b0; |
| |
| assign S_AXI_BRESP = { axil_berr, 1'b0 }; |
| // }}} |
| |
| // |
| // AXI-stream source (Write) FIFO |
| // |
| // {{{ |
| assign wfifo_write = axil_write_ready && awskd_addr[1]==ADDR_SOURCE[1] |
| && wskd_strb != 0 && !wfifo_full; |
| |
| generate if (OPT_SOURCE) |
| begin |
| |
| sfifo #(.BW(SW+1), .LGFLEN(LGFIFO)) |
| source(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), |
| .i_wr(wfifo_write), |
| .i_data({awskd_addr[0]==ADDR_SOURCE[0], |
| wskd_data[SW-1:0]}), |
| .o_full(wfifo_full), .o_fill(wfifo_fill), |
| .i_rd(M_AXIS_TREADY), |
| .o_data({ M_AXIS_TLAST, M_AXIS_TDATA }), |
| .o_empty(wfifo_empty)); |
| |
| always @(*) |
| M_AXIS_TVALID = !wfifo_empty; |
| |
| end else begin |
| |
| always @(*) |
| begin |
| M_AXIS_TVALID = 1'b0; |
| M_AXIS_TDATA = 0; |
| M_AXIS_TLAST = 0; |
| end |
| |
| assign wfifo_full = 1'b0; |
| assign wfifo_fill = 0; |
| |
| end endgenerate |
| // }}} |
| |
| // |
| // AXI-stream consumer/sink (Read) FIFO |
| // |
| // {{{ |
| wire rfifo_empty, rfifo_full, rfifo_last, read_rfifo; |
| wire [LGFIFO:0] rfifo_fill; |
| wire [SW-1:0] rfifo_data; |
| |
| generate if (OPT_SINK) |
| begin |
| |
| sfifo #(.BW(SW+1), .LGFLEN(LGFIFO)) |
| sink(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), |
| .i_wr(S_AXIS_TVALID && S_AXIS_TREADY), |
| .i_data({S_AXIS_TLAST, S_AXIS_TDATA}), |
| .o_full(rfifo_full), .o_fill(rfifo_fill), |
| .i_rd(read_rfifo), |
| .o_data({ rfifo_last, rfifo_data }), |
| .o_empty(rfifo_empty)); |
| |
| always @(*) |
| S_AXIS_TREADY = !rfifo_full; |
| assign read_rfifo =(axil_read_ready && arskd_addr== ADDR_SINK) |
| && !rfifo_empty; |
| |
| end else begin |
| |
| always @(*) |
| S_AXIS_TREADY = 1'b1; |
| |
| assign rfifo_empty = 1'b1; |
| assign rfifo_data = 0; |
| assign rfifo_last = 1'b1; |
| assign rfifo_fill = 0; |
| |
| end endgenerate |
| // }}} |
| |
| // |
| // Read timeout generation |
| // |
| // {{{ |
| generate if (OPT_SINK && OPT_TIMEOUT > 1) |
| begin |
| reg [$clog2(OPT_TIMEOUT)-1:0] read_timer; |
| |
| initial read_timer = OPT_TIMEOUT-1; |
| initial read_timeout = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| read_timer <= OPT_TIMEOUT-1; |
| read_timeout<= 1'b0; |
| end else if (!arskd_valid || (S_AXI_RVALID && !S_AXI_RREADY) |
| ||!rfifo_empty |
| ||(arskd_addr[1] != ADDR_SINK[1])) |
| begin |
| read_timer <= OPT_TIMEOUT-1; |
| read_timeout<= 1'b0; |
| end else begin |
| if (read_timer > 0) |
| read_timer <= read_timer - 1; |
| read_timeout <= (read_timer <= 1); |
| end |
| |
| `ifdef FORMAL |
| always @(*) |
| assert(read_timer <= OPT_TIMEOUT-1); |
| always @(*) |
| assert(read_timeout == (read_timer == 0)); |
| `endif |
| end else begin |
| |
| always @(*) |
| read_timeout = 1'b1; |
| |
| end endgenerate |
| // }}} |
| |
| // |
| // Read signaling |
| // |
| // {{{ |
| wire arskd_valid; |
| |
| skidbuffer #(.OPT_OUTREG(0), |
| .OPT_LOWPOWER(OPT_LOWPOWER), |
| .DW(C_AXI_ADDR_WIDTH-ADDRLSB)) |
| axilarskid(// |
| .i_clk(S_AXI_ACLK), .i_reset(i_reset), |
| .i_valid(S_AXI_ARVALID), .o_ready(S_AXI_ARREADY), |
| .i_data(S_AXI_ARADDR[C_AXI_ADDR_WIDTH-1:ADDRLSB]), |
| .o_valid(arskd_valid), .i_ready(axil_read_ready), |
| .o_data(arskd_addr)); |
| |
| assign axil_read_ready = arskd_valid |
| && (!S_AXI_RVALID || S_AXI_RREADY) |
| && ((arskd_addr[1] != ADDR_SINK[1]) |
| || (!rfifo_empty || read_timeout)); |
| |
| initial axil_read_valid = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| if (i_reset) |
| axil_read_valid <= 1'b0; |
| else if (axil_read_ready) |
| axil_read_valid <= 1'b1; |
| else if (S_AXI_RREADY) |
| axil_read_valid <= 1'b0; |
| |
| assign S_AXI_RVALID = axil_read_valid; |
| |
| always @(posedge S_AXI_ACLK) |
| if (OPT_LOWPOWER && !S_AXI_ARESETN) |
| axil_rerr <= 1'b0; |
| else if (axil_read_ready) |
| axil_rerr <= rfifo_empty && (arskd_addr[1] == ADDR_SINK[1]); |
| else if (OPT_LOWPOWER && S_AXI_RREADY) |
| axil_rerr <= 1'b0; |
| |
| assign S_AXI_RRESP = { axil_rerr, 1'b0 }; |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI-lite register logic |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| |
| |
| // |
| // Read data counting |
| // {{{ |
| initial reads_completed = 0; |
| initial read_bursts_completed = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| reads_completed <= 0; |
| read_bursts_completed <= 0; |
| end else if (!OPT_SINK) |
| begin |
| reads_completed <= reads_completed + (S_AXIS_TVALID ? 1:0); |
| read_bursts_completed <= read_bursts_completed |
| + ((S_AXIS_TVALID && S_AXIS_TLAST) ? 1:0); |
| end else if (read_rfifo && !rfifo_empty) |
| begin |
| reads_completed <= reads_completed + 1; |
| read_bursts_completed <= read_bursts_completed + (rfifo_last ? 1:0); |
| end |
| // }}} |
| |
| // |
| // Write data counting |
| // {{{ |
| generate if (OPT_SOURCE) |
| begin |
| |
| initial writes_completed = 0; |
| initial write_bursts_completed = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| writes_completed <= 0; |
| write_bursts_completed <= 0; |
| end else if (M_AXIS_TVALID && M_AXIS_TREADY) |
| begin |
| writes_completed <= writes_completed + 1; |
| write_bursts_completed <= write_bursts_completed |
| + (M_AXIS_TLAST ? 1:0); |
| end |
| |
| end else begin |
| |
| always @(*) |
| begin |
| writes_completed = 0; |
| write_bursts_completed = 0; |
| end |
| |
| end endgenerate |
| // }}} |
| |
| // |
| // Read data register |
| // {{{ |
| initial axil_read_data = 0; |
| always @(posedge S_AXI_ACLK) |
| if (OPT_LOWPOWER && !S_AXI_ARESETN) |
| axil_read_data <= 0; |
| else if (!S_AXI_RVALID || S_AXI_RREADY) |
| begin |
| axil_read_data <= 0; |
| casez(arskd_addr) |
| { ADDR_SINK[1], 1'b? }: begin |
| if (OPT_SIGN_EXTEND && rfifo_data[SW-1]) |
| axil_read_data <= -1; |
| axil_read_data[SW-1:0] <= rfifo_data; |
| end |
| ADDR_STATS: begin |
| axil_read_data[31:28] <= write_bursts_completed; |
| axil_read_data[27:16] <= writes_completed; |
| axil_read_data[15:12] <= read_bursts_completed; |
| axil_read_data[11:0] <= reads_completed; |
| end |
| ADDR_FIFO: begin |
| // FIFO information |
| axil_read_data[16 +: LGFIFO+1] <= wfifo_fill; |
| axil_read_data[15] <= rfifo_last; |
| axil_read_data[LGFIFO:0] <= rfifo_fill; |
| end |
| endcase |
| |
| if (OPT_LOWPOWER && !axil_read_ready) |
| axil_read_data <= 0; |
| end |
| |
| assign S_AXI_RDATA = axil_read_data; |
| // }}} |
| |
| // Verilator lint_off UNUSED |
| wire unused; |
| assign unused = &{ 1'b0, S_AXI_AWPROT, S_AXI_ARPROT, |
| S_AXI_ARADDR[ADDRLSB-1:0], |
| S_AXI_AWADDR[ADDRLSB-1:0], |
| wskd_data[C_AXI_DATA_WIDTH-1:SW] }; |
| // Verilator lint_on UNUSED |
| // }}} |
| `ifdef FORMAL |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties used in verfiying this core |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| // {{{ |
| reg f_past_valid; |
| initial f_past_valid = 0; |
| always @(posedge S_AXI_ACLK) |
| f_past_valid <= 1; |
| |
| always @(*) |
| if (!f_past_valid) |
| assume(!S_AXI_ARESETN); |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // The AXI-lite control interface |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| localparam F_AXIL_LGDEPTH = 4; |
| wire [F_AXIL_LGDEPTH-1:0] faxil_rd_outstanding, |
| faxil_wr_outstanding, |
| faxil_awr_outstanding; |
| |
| faxil_slave #( |
| // {{{ |
| .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), |
| .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), |
| .F_LGDEPTH(F_AXIL_LGDEPTH), |
| .F_AXI_MAXWAIT(OPT_TIMEOUT + 2), |
| .F_AXI_MAXDELAY(OPT_TIMEOUT + 2), |
| .F_AXI_MAXRSTALL(2), |
| .F_OPT_COVER_BURST(4) |
| // }}} |
| ) faxil( |
| // {{{ |
| .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), |
| // |
| .i_axi_awvalid(S_AXI_AWVALID), |
| .i_axi_awready(S_AXI_AWREADY), |
| .i_axi_awaddr( S_AXI_AWADDR), |
| .i_axi_awcache(4'h0), |
| .i_axi_awprot( S_AXI_AWPROT), |
| // |
| .i_axi_wvalid(S_AXI_WVALID), |
| .i_axi_wready(S_AXI_WREADY), |
| .i_axi_wdata( S_AXI_WDATA), |
| .i_axi_wstrb( S_AXI_WSTRB), |
| // |
| .i_axi_bvalid(S_AXI_BVALID), |
| .i_axi_bready(S_AXI_BREADY), |
| .i_axi_bresp( S_AXI_BRESP), |
| // |
| .i_axi_arvalid(S_AXI_ARVALID), |
| .i_axi_arready(S_AXI_ARREADY), |
| .i_axi_araddr( S_AXI_ARADDR), |
| .i_axi_arcache(4'h0), |
| .i_axi_arprot( S_AXI_ARPROT), |
| // |
| .i_axi_rvalid(S_AXI_RVALID), |
| .i_axi_rready(S_AXI_RREADY), |
| .i_axi_rdata( S_AXI_RDATA), |
| .i_axi_rresp( S_AXI_RRESP), |
| // |
| .f_axi_rd_outstanding(faxil_rd_outstanding), |
| .f_axi_wr_outstanding(faxil_wr_outstanding), |
| .f_axi_awr_outstanding(faxil_awr_outstanding) |
| // }}} |
| ); |
| |
| always @(*) |
| begin |
| assert(faxil_awr_outstanding== (S_AXI_BVALID ? 1:0) |
| +(S_AXI_AWREADY ? 0:1)); |
| |
| assert(faxil_wr_outstanding == (S_AXI_BVALID ? 1:0) |
| +(S_AXI_WREADY ? 0:1)); |
| |
| assert(faxil_rd_outstanding == (S_AXI_RVALID ? 1:0) |
| +(S_AXI_ARREADY ? 0:1)); |
| end |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Verifying the packet counters |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| reg [11:0] f_reads, f_writes; |
| reg [3:0] f_read_pkts, f_write_pkts; |
| |
| // |
| // Mirror the read counter |
| // |
| initial f_reads = 0; |
| initial f_read_pkts = 0; |
| |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| f_reads <= 0; |
| f_read_pkts <= 0; |
| end else if (OPT_SINK && (axil_read_ready |
| && arskd_addr == ADDR_SINK && !rfifo_empty)) |
| begin |
| f_reads <= f_reads + 1; |
| f_read_pkts <= f_read_pkts + (rfifo_last ? 1:0); |
| end else if (!OPT_SINK && S_AXIS_TVALID) |
| begin |
| f_reads <= f_reads + 1; |
| f_read_pkts <= f_read_pkts + (S_AXIS_TLAST ? 1:0); |
| end |
| |
| always @(*) |
| assert(f_reads == reads_completed); |
| always @(*) |
| assert(f_read_pkts == read_bursts_completed); |
| |
| always @(*) |
| if (!OPT_SINK) |
| assert(S_AXIS_TREADY); |
| |
| // |
| // Mirror the write counter |
| // |
| initial f_writes = 0; |
| initial f_write_pkts = 0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| begin |
| f_writes <= 0; |
| f_write_pkts <= 0; |
| end else if (OPT_SOURCE && M_AXIS_TVALID && M_AXIS_TREADY) |
| begin |
| f_writes <= f_writes + 1; |
| f_write_pkts <= f_write_pkts + (M_AXIS_TLAST ? 1:0); |
| end |
| |
| always @(*) |
| if (!OPT_SOURCE) |
| begin |
| assert(f_writes == 0); |
| assert(f_write_pkts == 0); |
| end |
| |
| always @(*) |
| begin |
| assert(f_writes == writes_completed); |
| assert(f_write_pkts == write_bursts_completed); |
| end |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Verify the read result |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (f_past_valid && $past(S_AXI_ARESETN && axil_read_ready)) |
| begin |
| assert(S_AXI_RVALID); |
| case($past(arskd_addr)) |
| ADDR_SINK: begin |
| assert(S_AXI_RDATA[SW-1:0] == $past(rfifo_data)); |
| if (SW < C_AXI_DATA_WIDTH) |
| begin |
| if (OPT_SIGN_EXTEND && $past(rfifo_data[SW-1])) |
| assert(&S_AXI_RDATA[C_AXI_DATA_WIDTH-1:SW]); |
| else |
| assert(S_AXI_RDATA[C_AXI_DATA_WIDTH-1:SW] == 0); |
| end end |
| // 1: assert(S_AXI_RDATA == $past(r1)); |
| ADDR_STATS: begin |
| assert(S_AXI_RRESP == 2'b00); |
| assert(S_AXI_RDATA[31:28] |
| == $past(write_bursts_completed)); |
| assert(S_AXI_RDATA[27:16] == $past(writes_completed)); |
| |
| assert(S_AXI_RDATA[15:12] |
| == $past(read_bursts_completed)); |
| assert(S_AXI_RDATA[11:0] == $past(reads_completed)); |
| end |
| ADDR_FIFO: begin |
| assert(S_AXI_RRESP == 2'b00); |
| if (LGFIFO < 16) |
| assert(S_AXI_RDATA[31:16+LGFIFO+1] == 0); |
| assert(S_AXI_RDATA[16+: LGFIFO+1]==$past(wfifo_fill)); |
| assert(S_AXI_RDATA[15] == $past(rfifo_last)); |
| if (LGFIFO < 15) |
| assert(S_AXI_RDATA[14:LGFIFO+1] == 0); |
| assert(S_AXI_RDATA[ 0+: LGFIFO+1]==$past(rfifo_fill)); |
| end |
| default: begin end |
| endcase |
| end |
| |
| // |
| // Check that our low-power only logic works by verifying that anytime |
| // S_AXI_RVALID is inactive, then the outgoing data is also zero. |
| // |
| always @(*) |
| if (OPT_LOWPOWER && !S_AXI_RVALID) |
| assert(S_AXI_RDATA == 0); |
| |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // The AXI-stream interfaces |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| |
| // Slave/consumer properties |
| always @(posedge S_AXI_ACLK) |
| if (!f_past_valid || !$past(S_AXI_ARESETN)) |
| begin |
| assume(!S_AXIS_TVALID); |
| end else if ($past(S_AXIS_TVALID && !S_AXIS_TREADY)) |
| begin |
| assume(S_AXIS_TVALID); |
| assume($stable(S_AXIS_TDATA)); |
| assume($stable(S_AXIS_TLAST)); |
| end |
| |
| // Master/producer/source properties |
| always @(posedge S_AXI_ACLK) |
| if (!f_past_valid || !$past(S_AXI_ARESETN)) |
| begin |
| assert(!M_AXIS_TVALID); |
| end else if ($past(M_AXIS_TVALID && !M_AXIS_TREADY)) |
| begin |
| assert(M_AXIS_TVALID); |
| assert($stable(M_AXIS_TDATA)); |
| assert($stable(M_AXIS_TLAST)); |
| end |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover checks |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| |
| always @(*) |
| cover(S_AXI_ARESETN && writes_completed == 16); |
| |
| always @(*) |
| cover(S_AXI_ARESETN && reads_completed == 16); |
| |
| always @(*) |
| cover(S_AXI_ARESETN && writes_completed == 16 |
| && reads_completed == 16); |
| |
| always @(*) |
| cover(S_AXI_BVALID && S_AXI_BRESP != 2'b00); |
| |
| always @(*) |
| cover(S_AXI_RVALID && S_AXI_RRESP != 2'b00); |
| |
| // }}} |
| // }}} |
| `endif |
| endmodule |