diff options
Diffstat (limited to '')
| -rw-r--r-- | rtl/wb2axip/axil2axis.v | 883 |
1 files changed, 0 insertions, 883 deletions
diff --git a/rtl/wb2axip/axil2axis.v b/rtl/wb2axip/axil2axis.v deleted file mode 100644 index 0e1d14f..0000000 --- a/rtl/wb2axip/axil2axis.v +++ /dev/null @@ -1,883 +0,0 @@ -//////////////////////////////////////////////////////////////////////////////// -// -// 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-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 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, - // }}} - ) ( - // {{{ - 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 wire 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 wire 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 ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3; - 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; - - wire read_timeout; - reg axil_rerr; - reg [3:0] read_bursts_completed; - reg [11:0] reads_completed; - - wire [3:0] write_bursts_completed; - wire [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 : GEN_WRITE_TIMEOUT - reg r_write_timeout; - reg [$clog2(OPT_TIMEOUT)-1:0] write_timer; - - initial write_timer = OPT_TIMEOUT-1; - initial r_write_timeout = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - write_timer <= OPT_TIMEOUT-1; - r_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; - r_write_timeout<= 1'b0; - end else begin - if (write_timer > 0) - write_timer <= write_timer - 1; - r_write_timeout <= (write_timer <= 1); - end - - assign write_timeout = r_write_timeout; -`ifdef FORMAL - always @(*) - assert(write_timer <= OPT_TIMEOUT-1); - always @(*) - assert(write_timeout == (write_timer == 0)); -`endif - end else begin : NO_WRITE_TIMEOUT - - assign 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 : GEN_SOURCE_FIFO - - 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)); - - assign M_AXIS_TVALID = !wfifo_empty; - - end else begin : NO_SOURCE_FIFO - - assign M_AXIS_TVALID = 1'b0; - assign M_AXIS_TDATA = 0; - assign M_AXIS_TLAST = 0; - - 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 : GEN_SINK_FIFO - - 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)); - - assign S_AXIS_TREADY = !rfifo_full; - assign read_rfifo =(axil_read_ready && arskd_addr== ADDR_SINK) - && !rfifo_empty; - - end else begin : NO_SINK - - assign 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 : GEN_READ_TIMEOUT - reg [$clog2(OPT_TIMEOUT)-1:0] read_timer; - reg r_read_timeout; - - initial read_timer = OPT_TIMEOUT-1; - initial r_read_timeout = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - read_timer <= OPT_TIMEOUT-1; - r_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; - r_read_timeout<= 1'b0; - end else begin - if (read_timer > 0) - read_timer <= read_timer - 1; - r_read_timeout <= (read_timer <= 1); - end - - assign read_timeout = r_read_timeout; - -`ifdef FORMAL - always @(*) - assert(read_timer <= OPT_TIMEOUT-1); - always @(*) - assert(read_timeout == (read_timer == 0)); -`endif - end else begin : NO_READ_TIMEOUT - - assign 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 : reads_completed and read_bursts_completed - // {{{ - 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 : GEN_WRITES_COMPLETED - // {{{ - reg [3:0] r_write_bursts_completed; - reg [11:0] r_writes_completed; - - initial r_writes_completed = 0; - initial r_write_bursts_completed = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - r_writes_completed <= 0; - r_write_bursts_completed <= 0; - end else if (M_AXIS_TVALID && M_AXIS_TREADY) - begin - r_writes_completed <= writes_completed + 1; - r_write_bursts_completed <= write_bursts_completed - + (M_AXIS_TLAST ? 1:0); - end - - assign writes_completed = r_writes_completed; - assign write_bursts_completed = r_write_bursts_completed; - // }}} - end else begin : NO_COMPLETION_COUNTERS // No AXI-stream source logic - // {{{ - assign writes_completed = 0; - assign write_bursts_completed = 0; - // }}} - 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; - // }}} - - // Make Verilator happy - // {{{ - // 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 - // }}} - // }}} -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -// -// Formal properties used in verfiying this core -// {{{ -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -`ifdef FORMAL - // Register definitions - // {{{ - 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_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_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 |