diff options
Diffstat (limited to 'rtl/wb2axip/axil2axis.v')
| -rw-r--r-- | rtl/wb2axip/axil2axis.v | 883 |
1 files changed, 883 insertions, 0 deletions
diff --git a/rtl/wb2axip/axil2axis.v b/rtl/wb2axip/axil2axis.v new file mode 100644 index 0000000..0e1d14f --- /dev/null +++ b/rtl/wb2axip/axil2axis.v @@ -0,0 +1,883 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// 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 |