rtl/wb2axip: add to version control

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