From 3038edc09a2eb15762f2e58533f429489107520b Mon Sep 17 00:00:00 2001
From: Alejandro Soto <alejandro@34project.org>
Date: Wed, 6 Mar 2024 02:38:24 -0600
Subject: rtl/wb2axip: add to version control

---
 rtl/wb2axip/axivfifo.v | 1405 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 1405 insertions(+)
 create mode 100644 rtl/wb2axip/axivfifo.v

(limited to 'rtl/wb2axip/axivfifo.v')

diff --git a/rtl/wb2axip/axivfifo.v b/rtl/wb2axip/axivfifo.v
new file mode 100644
index 0000000..2dc5369
--- /dev/null
+++ b/rtl/wb2axip/axivfifo.v
@@ -0,0 +1,1405 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: 	axivfifo.v
+// {{{
+// Project:	WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose:	A virtual FIFO, using an AXI based memory on the back end.  Data
+//		written via the AXI stream interface is written to an external
+//	memory once enough is available to fill a burst.  It's then copied from
+//	this external memory to a FIFO from which it can drive an outgoing
+//	stream.
+//
+// Registers:
+//	This core is simple--providing no control interface nor registers
+//	whereby it may be controlled.  To place it in a particular region of
+//	SDRAM, limit the address width and fill the rest of the address with
+//	the region you want.  Note: THIS CORE DEPENDS UPON ALIGNED MEMORY
+//	ACCESSES.  Hence, it must be aligned to the memory to keep these
+//	accesses aligned.
+//
+// Performance goals:
+//	100% throughput
+//	Stay off the bus until you can drive it hard
+//
+// 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
+//
+// `define			AXI3
+// }}}
+module	axivfifo #(
+		// {{{
+		parameter	C_AXI_ID_WIDTH = 1,
+		parameter	C_AXI_ADDR_WIDTH = 32,
+		parameter	C_AXI_DATA_WIDTH = 32,
+		//
+		// This core requires that the stream data width be identical
+		// to the bus data width.  Use an upstream core if you need to
+		// pack a smaller width into your bus's width, or a downstream
+		// core if you need to unpack it.
+		localparam	C_AXIS_DATA_WIDTH = C_AXI_DATA_WIDTH,
+		//
+		// LGMAXBURST determines the size of the maximum AXI burst.
+		// In AXI4, the maximum burst size is 256 beats the log_2()
+		// of which is 8.  In AXI3, it's a 16 beat burst of which the
+		// log_2() is 4.  Smaller numbers are also permissible here,
+		// although not verified.  I expect problems if LGMAXBURST is
+		// ever set to zero (no bursting).  An upgrade should fix that.
+		// Lower LGMAXBURST values will decrease the latency in this
+		// core while possibly causing throughput to be decreased
+		// (in the rest of the system--this core can handle 100%
+		// throughput either way.)
+		//
+		// Beware of the AXI requirement that bursts cannot cross
+		// 4kB boundaries.  If your bus is larger than 128 bits wide,
+		// you'll need to lower this maximum burst size to meet that
+		// requirement.
+`ifdef	AXI3
+		parameter	LGMAXBURST=4,	// 16 beats max
+`else
+		parameter	LGMAXBURST=8,	// 256 beats
+`endif
+		//
+		// LGFIFO: This is the (log-based-2) size of the internal FIFO.
+		// Hence if LGFIFO=8, the internal FIFO will have 256 elements
+		// (words) in it.  High throughput transfers are accomplished
+		// by first storing data into a FIFO, then once a full burst
+		// size is available bursting that data over the bus.  In
+		// order to be able to keep receiving data while bursting it
+		// out, the FIFO size must be at least twice the size of the
+		// maximum burst size--that is LGFIFO must be at least one more
+		// than LGMAXBURST.  Larger sizes are possible as well.
+		parameter	LGFIFO = LGMAXBURST+1,	// 512 element FIFO
+		//
+		// AXI uses ID's to transfer information.  This core rather
+		// ignores them.  Instead, it uses a constant ID for all
+		// transfers.  The following two parameters control that ID.
+		parameter	[C_AXI_ID_WIDTH-1:0]	AXI_READ_ID = 0,
+		parameter	[C_AXI_ID_WIDTH-1:0]	AXI_WRITE_ID = 0,
+		//
+		localparam	ADDRLSB= $clog2(C_AXI_DATA_WIDTH)-3
+		// }}}
+	) (
+		// {{{
+		input	wire	S_AXI_ACLK,
+		input	wire	S_AXI_ARESETN,
+		//
+		// The AXI4-stream interface
+		// {{{
+		// This core does not support TLAST, TKEEP, or TSTRB.  If you
+		// want to support these extra values, expand the width of
+		// TDATA, and unpack them on the output of the FIFO.
+		//
+		// The incoming stream
+		input	wire				S_AXIS_TVALID,
+		output	wire				S_AXIS_TREADY,
+		input	wire	[C_AXIS_DATA_WIDTH-1:0]	S_AXIS_TDATA,
+		//
+		// The outgoing stream
+		output	wire				M_AXIS_TVALID,
+		input	wire				M_AXIS_TREADY,
+		output	reg	[C_AXIS_DATA_WIDTH-1:0]	M_AXIS_TDATA,
+		// }}}
+		//
+		// The AXI Master (DMA) interface
+		// {{{
+		// First to write data to the (external) AXI buffer
+		output	wire				M_AXI_AWVALID,
+		input	wire				M_AXI_AWREADY,
+		output	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_AWID,
+		output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_AWADDR,
+`ifdef	AXI3
+		output	wire	[3:0]			M_AXI_AWLEN,
+`else
+		output	wire	[7:0]			M_AXI_AWLEN,
+`endif
+		output	wire	[2:0]			M_AXI_AWSIZE,
+		output	wire	[1:0]			M_AXI_AWBURST,
+`ifdef	AXI3
+		output	wire	[1:0]			M_AXI_AWLOCK,
+`else
+		output	wire				M_AXI_AWLOCK,
+`endif
+		output	wire	[3:0]			M_AXI_AWCACHE,
+		output	wire	[2:0]			M_AXI_AWPROT,
+		output	wire	[3:0]			M_AXI_AWQOS,
+		//
+		//
+		output	wire				M_AXI_WVALID,
+		input	wire				M_AXI_WREADY,
+`ifdef	AXI3
+		output	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_WID,
+`endif
+		output	wire	[C_AXI_DATA_WIDTH-1:0]	M_AXI_WDATA,
+		output	wire [C_AXI_DATA_WIDTH/8-1:0]	M_AXI_WSTRB,
+		output	wire				M_AXI_WLAST,
+		//
+		//
+		input	wire				M_AXI_BVALID,
+		output	wire				M_AXI_BREADY,
+		input	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_BID,
+		input	wire	[1:0]			M_AXI_BRESP,
+		//
+		// Then the read interface to read the data back
+		output	wire				M_AXI_ARVALID,
+		input	wire				M_AXI_ARREADY,
+		output	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_ARID,
+		output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_ARADDR,
+`ifdef	AXI3
+		output	wire	[3:0]			M_AXI_ARLEN,
+`else
+		output	wire	[7:0]			M_AXI_ARLEN,
+`endif
+		output	wire	[2:0]			M_AXI_ARSIZE,
+		output	wire	[1:0]			M_AXI_ARBURST,
+`ifdef	AXI3
+		output	wire	[1:0]			M_AXI_ARLOCK,
+`else
+		output	wire				M_AXI_ARLOCK,
+`endif
+		output	wire	[3:0]			M_AXI_ARCACHE,
+		output	wire	[2:0]			M_AXI_ARPROT,
+		output	wire	[3:0]			M_AXI_ARQOS,
+		//
+		input	wire				M_AXI_RVALID,
+		output	wire				M_AXI_RREADY,
+		input	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_RID,
+		input	wire	[C_AXI_DATA_WIDTH-1:0]	M_AXI_RDATA,
+		input	wire				M_AXI_RLAST,
+		input	wire	[1:0]			M_AXI_RRESP,
+		// }}}
+		//
+		// {{{
+		// Request a soft-reset: reset the FIFO without resetting th bus
+		input	wire				i_reset,
+		// o_err is a hard error.  If ever true, the core will come
+		// to a hard stop.
+		output	reg				o_err,
+		// o_overflow is an indication of data changing before it is
+		// accepted.
+		output	reg				o_overflow,
+		// o_mm2s_full is a reference to the last FIFO in our
+		// processing pipeline.  It's true if a burst of (1<<LGMAXBURST)
+		// words of (1<<ADDRLSB) bytes may be read from the downstream
+		// FIFO without waiting on the external memory.
+		output	reg				o_mm2s_full,
+		// o_empty is true if nothing is in the core.
+		output	reg				o_empty,
+		// o_fill counts the number of items in the core.  Just because
+		// the number of items is non-zero, however, doesn't mean you
+		// can read them out.  In general, you will need to write at
+		// least a full (1<<LGMAXBURST) words to the core, those will
+		// need to be written to memory, read from memory, and then
+		// used to fill the downstream FIFO before you can read.  This
+		// number is just available for your informational use.
+		output reg [C_AXI_ADDR_WIDTH-ADDRLSB:0]	o_fill
+		// }}}
+		// }}}
+	);
+
+	// Register and signal definitions
+	// {{{
+	// The number of beats in this maximum burst size is automatically
+	// determined from LGMAXBURST, and so its forced to be a power of
+	// two this way.
+	localparam	MAXBURST=(1<<LGMAXBURST);
+	localparam	BURSTAW = C_AXI_ADDR_WIDTH-LGMAXBURST-ADDRLSB;
+
+	reg				soft_reset, vfifo_empty, vfifo_full;
+	wire				reset_fifo;
+	reg	[C_AXI_ADDR_WIDTH-ADDRLSB:0]	vfifo_fill;
+	reg	[BURSTAW:0]		mem_data_available_w,
+					writes_outstanding;
+	reg	[BURSTAW:0]		mem_space_available_w,
+					reads_outstanding;
+	reg				s_last_stalled;
+	reg	[C_AXI_DATA_WIDTH-1:0]	s_last_tdata;
+	wire				read_from_fifo, ififo_full, ififo_empty;
+	wire	[C_AXI_DATA_WIDTH-1:0]	ififo_data;
+	wire	[LGFIFO:0]		ififo_fill;
+
+	reg				start_write, phantom_write,
+					axi_awvalid, axi_wvalid, axi_wlast,
+					writes_idle;
+	reg	[C_AXI_ADDR_WIDTH-1:0]	axi_awaddr;
+	reg	[LGMAXBURST:0]		writes_pending;
+
+	reg				start_read, phantom_read, reads_idle,
+					axi_arvalid;
+	reg	[C_AXI_ADDR_WIDTH-1:0]	axi_araddr;
+
+	reg				skd_valid;
+	reg	[C_AXI_DATA_WIDTH-1:0]	skd_data;
+
+	reg	[LGFIFO:0]	ofifo_space_available;
+	wire			write_to_fifo, ofifo_empty, ofifo_full;
+	wire	[LGFIFO:0]	ofifo_fill;
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Global FIFO signal handling
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	//
+	// A soft reset
+	// {{{
+	// This is how we reset the FIFO without resetting the rest of the AXI
+	// bus.  On a reset request, we raise the soft_reset flag and reset all
+	// of our internal FIFOs.  We also stop issuing bus commands.  Once all
+	// outstanding bus commands come to a halt, then we release from reset
+	// and start operating as a FIFO.
+	initial	soft_reset = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		soft_reset <= 0;
+	else if (i_reset)
+		soft_reset <= 1;
+	else if (writes_idle && reads_idle)
+		soft_reset <= 0;
+
+	assign	reset_fifo = soft_reset || !S_AXI_ARESETN;
+	// }}}
+
+	//
+	// Calculating the fill of the virtual FIFO, and the associated
+	// full/empty flags that go with it
+	// {{{
+	initial	vfifo_fill  = 0;
+	initial	vfifo_empty = 1;
+	initial	vfifo_full  = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || soft_reset)
+	begin
+		vfifo_fill  <= 0;
+		vfifo_empty <= 1;
+		vfifo_full  <= 0;
+	end else case({ S_AXIS_TVALID && S_AXIS_TREADY,
+			M_AXIS_TVALID && M_AXIS_TREADY })
+	2'b10:	begin
+		vfifo_fill  <= vfifo_fill + 1;
+		vfifo_empty <= 0;
+		vfifo_full  <= (&vfifo_fill[C_AXI_ADDR_WIDTH-ADDRLSB-1:0]);
+		end
+	2'b01:	begin
+		vfifo_fill <= vfifo_fill - 1;
+		vfifo_full <= 0;
+		vfifo_empty<= (vfifo_fill <= 1);
+		end
+	default: begin end
+	endcase
+
+	always @(*)
+		o_fill = vfifo_fill;
+
+	always @(*)
+		o_empty = vfifo_empty;
+	// }}}
+
+	// Determining when the write half is idle
+	// {{{
+	// This is required to know when to come out of soft reset.
+	//
+	// The first step is to count the number of bursts that remain
+	// outstanding
+	initial	writes_outstanding = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		writes_outstanding <= 0;
+	else case({ phantom_write,M_AXI_BVALID && M_AXI_BREADY})
+	2'b01: writes_outstanding <= writes_outstanding - 1;
+	2'b10: writes_outstanding <= writes_outstanding + 1;
+	default: begin end
+	endcase
+
+	// The second step is to use this counter to determine if we are idle.
+	// If WVALID is ever high, or start_write goes high, then we are
+	// obviously not idle.  Otherwise, we become idle when the number of
+	// writes outstanding transitions to (or equals) zero.
+	initial	writes_idle = 1;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		writes_idle <= 1;
+	else if (start_write || M_AXI_WVALID)
+		writes_idle <= 0;
+	else
+		writes_idle <= (writes_outstanding
+				== ((M_AXI_BVALID && M_AXI_BREADY) ? 1:0));
+	// }}}
+
+	// Count how much space is used in the memory device
+	// {{{
+	// Well, obviously, we can't fill our memory device or we have problems.
+	// To make sure we don't overflow, we count memory usage here.  We'll
+	// count memory usage in units of bursts of (1<<LGMAXBURST) words of
+	// (1<<ADDRLSB) bytes each.  So ... here we count the amount of device
+	// memory that hasn't (yet) been committed.  This is different from the
+	// memory used (which we don't calculate), or the memory which may yet
+	// be read--which we'll calculate in a moment.
+	initial	mem_space_available_w = (1<<BURSTAW);
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || soft_reset)
+		mem_space_available_w <= (1<<BURSTAW);
+	else case({ phantom_write,M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST })
+	2'b01: mem_space_available_w <= mem_space_available_w + 1;
+	2'b10: mem_space_available_w <= mem_space_available_w - 1;
+	default: begin end
+	endcase
+	// }}}
+
+	// Determining when the read half is idle
+	// {{{
+	// Count the number of read bursts that we've committed to.  This
+	// includes bursts that have ARVALID but haven't been accepted, as well
+	// as any the downstream device will yet return an RLAST for.
+	initial	reads_outstanding = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		reads_outstanding <= 0;
+	else case({ phantom_read,M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST})
+	2'b01: reads_outstanding <= reads_outstanding - 1;
+	2'b10: reads_outstanding <= reads_outstanding + 1;
+	default: begin end
+	endcase
+
+	// Now, using the reads_outstanding counter, we can check whether or not
+	// we are idle (and can exit a reset) of if instead there are more
+	// bursts outstanding to wait for.
+	//
+	// By registering this counter, we can keep the soft_reset release
+	// simpler.  At least this way, it doesn't need to check two counters
+	// for zero.
+	initial	reads_idle = 1;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		reads_idle <= 1;
+	else if (start_read || M_AXI_ARVALID)
+		reads_idle <= 0;
+	else
+		reads_idle <= (reads_outstanding
+		== ((M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST) ? 1:0));
+	// }}}
+
+	// Count how much data is in the memory device that we can read out
+	// {{{
+	// In AXI, after you issue a write, you can't depend upon that data
+	// being present on the device and available for a read until the
+	// associated BVALID is returned.  Therefore we don't count any memory
+	// as available to be read until BVALID comes back.  Once a read
+	// command is issued, the memory is again no longer available to be
+	// read.  Note also that we are counting bursts here.  A second
+	// conversion below converts this count to bytes.
+	initial	mem_data_available_w = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || soft_reset)
+		mem_data_available_w <= 0;
+	else case({ M_AXI_BVALID, phantom_read })
+	2'b10: mem_data_available_w <= mem_data_available_w + 1;
+	2'b01: mem_data_available_w <= mem_data_available_w - 1;
+	default: begin end
+	endcase
+	// }}}
+
+	//
+	// Error detection
+	// {{{
+	initial	o_err = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		o_err <= 1'b0;
+	else begin
+		if (M_AXI_BVALID && M_AXI_BRESP[1])
+			o_err <= 1'b1;
+		if (M_AXI_RVALID && M_AXI_RRESP[1])
+			o_err <= 1'b1;
+	end
+	// }}}
+
+	//
+	// Incoming stream overflow detection
+	// {{{
+	// The overflow flag is set if ever an incoming value violates the
+	// stream protocol and changes while stalled.  Internally, however,
+	// the overflow flag is ignored.  It's provided for your information.
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		s_last_stalled <= 0;
+	else
+		s_last_stalled <= S_AXIS_TVALID && !S_AXIS_TREADY;
+
+	always @(posedge S_AXI_ACLK)
+	if (S_AXIS_TVALID)
+		s_last_tdata <= S_AXIS_TDATA;
+
+	initial	o_overflow = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || soft_reset)
+		o_overflow <= 0;
+	else if (s_last_stalled)
+	begin
+		if (!S_AXIS_TVALID)
+			o_overflow <= 1;
+		if (S_AXIS_TDATA != s_last_tdata)
+			o_overflow <= 1;
+	end
+	// }}}
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Incoming FIFO
+	// {{{
+	// Incoming data stream info the FIFO
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	assign	S_AXIS_TREADY = !reset_fifo && !ififo_full && !vfifo_full;
+	assign	read_from_fifo= (!skd_valid || (M_AXI_WVALID && M_AXI_WREADY));
+
+	sfifo #(.BW(C_AXIS_DATA_WIDTH), .LGFLEN(LGFIFO))
+	ififo(S_AXI_ACLK, reset_fifo,
+		S_AXIS_TVALID && S_AXIS_TREADY,
+			S_AXIS_TDATA, ififo_full, ififo_fill,
+		read_from_fifo, ififo_data, ififo_empty);
+
+	//
+	// We need a quick 1-element buffer here in order to keep the soft
+	// reset, which resets the FIFO pointer, from adjusting any FIFO data.
+	// {{{
+	// Here's the rule: we need to fill the buffer before it ever gets
+	// used.  Then, once used, it should be able to maintain 100%
+	// throughput.
+	initial	skd_valid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (reset_fifo)
+		skd_valid <= 0;
+	else if (!ififo_empty)
+		skd_valid <= 1;
+	else if (M_AXI_WVALID && M_AXI_WREADY)
+		skd_valid <= 0;
+
+	always @(posedge S_AXI_ACLK)
+	if (!M_AXI_WVALID || M_AXI_WREADY)
+	begin
+		if (!skd_valid || M_AXI_WREADY)
+			skd_data <= ififo_data;
+	end
+	// }}}
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// AXI write processing
+	// {{{
+	// Write data from our FIFO onto the bus
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// start_write: determining when to issue a write burst
+	// {{{
+	always @(*)
+	begin
+		start_write = 0;
+
+		if (ififo_fill >= (1<<LGMAXBURST))
+			start_write = 1;
+		if (vfifo_full || soft_reset || phantom_write)
+			start_write = 0;
+		if (mem_space_available_w == 0)
+			start_write = 0;
+
+		if (M_AXI_WVALID && (!M_AXI_WREADY || !M_AXI_WLAST))
+			start_write = 0;
+		if (M_AXI_AWVALID && !M_AXI_AWREADY)
+			start_write = 0;
+		if (o_err)
+			start_write = 0;
+	end
+	// }}}
+
+	// Register the start write signal into AWVALID and phantom write
+	// {{{
+	// phantom_write contains the start signal, but immediately clears
+	// on the next clock cycle.  This allows us some time to calculate
+	// the data for the next burst which and if AWVALID remains high and
+	// not yet accepted.
+	initial	phantom_write = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		phantom_write <= 0;
+	else
+		phantom_write <= start_write;
+
+	// Set AWVALID to start_write if every the channel isn't stalled.
+	// Incidentally, start_write is guaranteed to be zero if the channel
+	// is stalled, since that signal is used by other things as well.
+	initial	axi_awvalid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		axi_awvalid <= 0;
+	else if (!M_AXI_AWVALID || M_AXI_AWREADY)
+		axi_awvalid <= start_write;
+	// }}}
+
+	// Write address
+	// {{{
+	// We insist on alignment.  On every accepted burst, we step forward by
+	// one burst length.  On reset, we reset the address at our first
+	// opportunity.
+	initial	axi_awaddr = 0;
+	always @(posedge S_AXI_ACLK)
+	begin
+		if (M_AXI_AWVALID && M_AXI_AWREADY)
+			axi_awaddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB]
+			<= axi_awaddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB] +1;
+
+		if ((!M_AXI_AWVALID || M_AXI_AWREADY) && soft_reset)
+			axi_awaddr <= 0;
+
+		if (!S_AXI_ARESETN)
+			axi_awaddr <= 0;
+
+		axi_awaddr[LGMAXBURST+ADDRLSB-1:0] <= 0;
+	end
+	// }}}
+
+	// Write data channel valid
+	// {{{
+	initial	axi_wvalid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		axi_wvalid <= 0;
+	else if (start_write)
+		axi_wvalid <= 1;
+	else if (!M_AXI_WVALID || M_AXI_WREADY)
+		axi_wvalid <= M_AXI_WVALID && !M_AXI_WLAST;
+	// }}}
+
+	// WLAST generation
+	// {{{
+	// On the beginning of any burst, start a counter of the number of items
+	// in it.  Once the counter gets to 1, set WLAST.
+	initial	writes_pending = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		writes_pending <= 0;
+	else if (start_write)
+		writes_pending <= MAXBURST;
+	else if (M_AXI_WVALID && M_AXI_WREADY)
+		writes_pending <= writes_pending -1;
+
+	always @(posedge S_AXI_ACLK)
+	if (start_write)
+		axi_wlast <= (LGMAXBURST == 0);
+	else if (!M_AXI_WVALID || M_AXI_WREADY)
+		axi_wlast <= (writes_pending == 1 + (M_AXI_WVALID ? 1:0));
+	// }}}
+
+	// Bus assignments based upon the above
+	// {{{
+	assign	M_AXI_AWVALID = axi_awvalid;
+	assign	M_AXI_AWID    = AXI_WRITE_ID;
+	assign	M_AXI_AWADDR  = axi_awaddr;
+	assign	M_AXI_AWLEN   = MAXBURST-1;
+	assign	M_AXI_AWSIZE  = ADDRLSB[2:0];
+	assign	M_AXI_AWBURST = 2'b01;
+	assign	M_AXI_AWLOCK  = 0;
+	assign	M_AXI_AWCACHE = 0;
+	assign	M_AXI_AWPROT  = 0;
+	assign	M_AXI_AWQOS   = 0;
+
+	assign	M_AXI_WVALID = axi_wvalid;
+	assign	M_AXI_WDATA  = skd_data;
+`ifdef	AXI3
+	assign	M_AXI_WID    = AXI_WRITE_ID;
+`endif
+	assign	M_AXI_WLAST  = axi_wlast;
+	assign	M_AXI_WSTRB  = -1;
+
+	assign	M_AXI_BREADY = 1;
+	// }}}
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// AXI read processing
+	// {{{
+	// Read data into our FIFO
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// How much FIFO space is available?
+	// {{{
+	// One we issue a read command, the FIFO space isn't available any more.
+	// That way we can determine when a second read can be issued--even
+	// before the first has returned--while also guaranteeing that there's
+	// always room in the outgoing FIFO for anything that might return.
+	// Remember: NEVER generate backpressure in a bus master
+	initial	ofifo_space_available = (1<<LGFIFO);
+	always @(posedge S_AXI_ACLK)
+	if (reset_fifo)
+		ofifo_space_available <= (1<<LGFIFO);
+	else case({phantom_read, M_AXIS_TVALID && M_AXIS_TREADY})
+	2'b10:	ofifo_space_available <= ofifo_space_available - MAXBURST;
+	2'b01:	ofifo_space_available <= ofifo_space_available + 1;
+	2'b11:	ofifo_space_available <= ofifo_space_available - MAXBURST + 1;
+	default: begin end
+	endcase
+	// }}}
+
+	// Determine when to start a next read-from-memory-to-FIFO burst
+	// {{{
+	always @(*)
+	begin
+		start_read = 1;
+
+		// We can't read yet if we don't have space available.
+		// Note the comparison is carefully chosen to make certain
+		// it doesn't use all ofifo_space_available bits, but rather
+		// only the number of bits between LGFIFO and
+		// LGMAXBURST--nominally a single bit.
+		if (ofifo_space_available < MAXBURST)	// FIFO space ?
+			start_read = 0;
+
+		// If there's no memory available for us to read from, then
+		// we can't start a read yet.
+		if (!M_AXI_BVALID && mem_data_available_w == 0)
+			start_read = 0;
+
+		// Don't start anything while waiting on a reset.  Likewise,
+		// insist on a minimum one clock between read burst issuances.
+		if (soft_reset || phantom_read)
+			start_read = 0;
+
+		// We can't start a read request if the AR* channel is stalled
+		if (M_AXI_ARVALID && !M_AXI_ARREADY)
+			start_read = 0;
+
+		// Following a bus error, we come to a complete halt.  Such a
+		// bus error is an indication that something *SERIOUSLY* went
+		// wrong--perhaps we aren't accessing the memory we are supposed
+		// to.  To prevent damage to external devices, we disable
+		// ourselves entirely.  There is no fall back.  We only
+		// restart on a full bus restart.
+		if (o_err)
+			start_read = 0;
+	end
+	// }}}
+
+	// Set phantom_read and ARVALID
+	// {{{
+	initial	phantom_read = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		phantom_read <= 0;
+	else
+		phantom_read <= start_read;
+
+	initial	axi_arvalid = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		axi_arvalid <= 0;
+	else if (!M_AXI_ARVALID || M_AXI_ARREADY)
+		axi_arvalid <= start_read;
+	// }}}
+
+	// Calculate the next ARADDR
+	// {{{
+	initial	axi_araddr = 0;
+	always @(posedge S_AXI_ACLK)
+	begin
+		if (M_AXI_ARVALID && M_AXI_ARREADY)
+			axi_araddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB]
+			<= axi_araddr[C_AXI_ADDR_WIDTH-1:LGMAXBURST+ADDRLSB]+ 1;
+
+		if ((!M_AXI_ARVALID || M_AXI_ARREADY) && soft_reset)
+			axi_araddr <= 0;
+
+		if (!S_AXI_ARESETN)
+			axi_araddr <= 0;
+
+		axi_araddr[LGMAXBURST+ADDRLSB-1:0] <= 0;
+	end
+	// }}}
+
+	// Assign values to our bus wires
+	// {{{
+	assign	M_AXI_ARVALID = axi_arvalid;
+	assign	M_AXI_ARID    = AXI_READ_ID;
+	assign	M_AXI_ARADDR  = axi_araddr;
+	assign	M_AXI_ARLEN   = MAXBURST-1;
+	assign	M_AXI_ARSIZE  = ADDRLSB[2:0];
+	assign	M_AXI_ARBURST = 2'b01;
+	assign	M_AXI_ARLOCK  = 0;
+	assign	M_AXI_ARCACHE = 0;
+	assign	M_AXI_ARPROT  = 0;
+	assign	M_AXI_ARQOS   = 0;
+
+	assign	M_AXI_RREADY = 1;
+	// }}}
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Outgoing AXI stream processing
+	// {{{
+	// Send data out from the MM2S FIFO
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// We basically just stuff the data read from memory back into our
+	// outgoing FIFO here.  The logic is quite straightforward.
+	assign	write_to_fifo = M_AXI_RVALID && M_AXI_RREADY;
+	assign	M_AXIS_TVALID = !ofifo_empty;
+
+	sfifo #(.BW(C_AXIS_DATA_WIDTH), .LGFLEN(LGFIFO))
+	ofifo(S_AXI_ACLK, reset_fifo,
+		write_to_fifo,
+			M_AXI_RDATA, ofifo_full, ofifo_fill,
+		M_AXIS_TVALID && M_AXIS_TREADY, M_AXIS_TDATA, ofifo_empty);
+
+	always @(*)
+		o_mm2s_full = |ofifo_fill[LGFIFO:LGMAXBURST];
+	// }}}
+
+	// Keep Verilator happy
+	// {{{
+	// Verilator lint_off UNUSED
+	wire	unused;
+	assign	unused = &{ 1'b0, M_AXI_BID, M_AXI_RID,
+			M_AXI_BRESP[0], M_AXI_RRESP[0],
+			ififo_empty, ofifo_full, ofifo_fill
+			// fifo_full, fifo_fill, fifo_empty,
+			};
+
+	// Verilator lint_on UNUSED
+	// }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal property section
+// {{{
+//
+// The following are a subset of the formal properties used to verify this
+// core.  The full set of formal properties, together with the formal
+// property set itself, are available for purchase.
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+	// FAXI_DEPTH controls the width of the counters in the bus property
+	// interface file.  In order to support bursts of length 8 (or more),
+	// there's a minimum of 9.  Otherwise, we'll just set this to the width
+	// of the AXI address bus.
+	localparam	FAXI_DEPTH = (C_AXI_ADDR_WIDTH > 8)
+					? (C_AXI_ADDR_WIDTH+1) : 9;
+
+	reg	f_past_valid;
+
+	initial	f_past_valid = 0;
+	always @(posedge S_AXI_ACLK)
+		f_past_valid <= 1;
+
+	//
+	// Wires necessary for interacting with the formal property file
+	// {{{
+	// ...
+	// }}}
+
+	// Other registers to keep simplify keeping track of our progress
+	// {{{
+	reg	[C_AXI_ADDR_WIDTH-1:0]	faxi_rd_cknext, faxi_wr_cknext,
+					f_read_beat_addr, f_write_beat_addr,
+					faxi_read_beat_addr;
+	reg	[C_AXI_ADDR_WIDTH-1:0]	f_read_ckbeat_addr;
+	reg	[FAXI_DEPTH-1:0]	f_rd_bursts_after_check;
+
+	reg	[C_AXI_ADDR_WIDTH:0]	f_vfill;
+	reg	[C_AXI_ADDR_WIDTH:0]	f_space_available,
+					f_data_available;
+
+	reg	[C_AXI_ADDR_WIDTH-1:0]	f_read_checksum;
+	reg	[C_AXI_ADDR_WIDTH:0]	mem_space_available, mem_data_available;
+	// }}}
+
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// The main AXI data interface bus property check
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// The number of beats in the maximum burst size is
+	// automatically determined from LGMAXBURST, and so its
+	// forced to be a power of two this way.
+	localparam	MAXBURST=(1<<LGMAXBURST);
+
+	faxi_master #(
+		// {{{
+		.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
+		.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
+		.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
+		.OPT_MAXBURST(MAXBURST-1),
+		.OPT_NARROW_BURST(1'b0),
+		.OPT_ASYNC_RESET(1'b0),	// We don't use asynchronous resets
+		.OPT_EXCLUSIVE(1'b0),	// We don't use the LOCK signal
+		.F_OPT_ASSUME_RESET(1'b1), // We aren't generating the reset
+		.F_OPT_NO_RESET(1'b1),
+		.F_LGDEPTH(FAXI_DEPTH)	// Width of the counters
+		// }}}
+	) faxi(
+		// {{{
+		.i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
+		// Write signals
+		// {{{
+		.i_axi_awvalid(M_AXI_AWVALID),
+		.i_axi_awready(M_AXI_AWREADY),
+		.i_axi_awid(   M_AXI_AWID),
+		.i_axi_awaddr( M_AXI_AWADDR),
+		.i_axi_awlen(  M_AXI_AWLEN),
+		.i_axi_awsize( M_AXI_AWSIZE),
+		.i_axi_awburst(M_AXI_AWBURST),
+		.i_axi_awlock( M_AXI_AWLOCK),
+		.i_axi_awcache(M_AXI_AWCACHE),
+		.i_axi_awprot( M_AXI_AWPROT),
+		.i_axi_awqos(  M_AXI_AWQOS),
+		//
+		.i_axi_wvalid(M_AXI_WVALID),
+		.i_axi_wready(M_AXI_WREADY),
+		.i_axi_wdata( M_AXI_WDATA),
+		.i_axi_wstrb( M_AXI_WSTRB),
+		.i_axi_wlast( M_AXI_WLAST),
+		//
+		.i_axi_bvalid(M_AXI_BVALID),
+		.i_axi_bready(M_AXI_BREADY),
+		.i_axi_bid(   M_AXI_BID),
+		.i_axi_bresp( M_AXI_BRESP),
+		// }}}
+		// Read signals
+		// {{{
+		.i_axi_arvalid(M_AXI_ARVALID),
+		.i_axi_arready(M_AXI_ARREADY),
+		.i_axi_arid(   M_AXI_ARID),
+		.i_axi_araddr( M_AXI_ARADDR),
+		.i_axi_arlen(  M_AXI_ARLEN),
+		.i_axi_arsize( M_AXI_ARSIZE),
+		.i_axi_arburst(M_AXI_ARBURST),
+		.i_axi_arlock( M_AXI_ARLOCK),
+		.i_axi_arcache(M_AXI_ARCACHE),
+		.i_axi_arprot( M_AXI_ARPROT),
+		.i_axi_arqos(  M_AXI_ARQOS),
+		//
+		//
+		.i_axi_rvalid(M_AXI_RVALID),
+		.i_axi_rready(M_AXI_RREADY),
+		.i_axi_rid(   M_AXI_RID),
+		.i_axi_rdata( M_AXI_RDATA),
+		.i_axi_rlast( M_AXI_RLAST),
+		.i_axi_rresp( M_AXI_RRESP),
+		// }}}
+		// Induction signals
+		// {{{
+		// ...
+		// }}}
+		// }}}
+	);
+
+	// Some quick sanity checks
+	// {{{
+	always @(*)
+	begin
+		//
+		// ...
+		//
+	end
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Write sanity checking
+	// {{{
+	always @(*)
+		mem_space_available = { mem_space_available_w,
+			{(LGMAXBURST+ADDRLSB){1'b0} } };
+
+	// Let's calculate the address of each write beat
+	// {{{
+	initial	f_write_beat_addr = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		f_write_beat_addr <= 0;
+	else if ((!M_AXI_WVALID || (M_AXI_WREADY && M_AXI_WLAST)) && soft_reset)
+		f_write_beat_addr <= 0;
+	else if (M_AXI_WVALID && M_AXI_WREADY)
+		f_write_beat_addr <= f_write_beat_addr + (1<<ADDRLSB);
+	// }}}
+
+	//
+	// ...
+	//
+
+	// Verify during any write burst that all the burst parameters are
+	// correct
+	// {{{
+	// ...
+	// }}}
+
+	always @(*)
+	if (M_AXI_AWVALID)
+	begin
+		assert(writes_pending == (1<<LGMAXBURST));
+		// ...
+	end else
+		// ...
+
+	always @(*)
+		assert(M_AXI_WVALID == (writes_pending != 0));
+
+	//
+	// ...
+	//
+
+	// Check the writes-idle signal
+	// {{{
+	// ...
+	// }}}
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Read sanity checking
+	// {{{
+
+	always @(*)
+		mem_data_available = { mem_data_available_w,
+			{(LGMAXBURST+ADDRLSB){1'b0} } };
+	//
+	// ...
+	// Check the reads-idle signal
+	// {{{
+	// ...
+	// }}}
+
+	// Regenerate the read beat address
+	// {{{
+	// This works because we are using a single AXI ID for all of our reads.
+	// Therefore we can guarantee that reads will come back in order, thus
+	// we can count the return address here.
+	initial	f_read_beat_addr = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		f_read_beat_addr <= 0;
+	else if (soft_reset && reads_idle)
+		f_read_beat_addr <= 0;
+	else if (M_AXI_RVALID && M_AXI_RREADY)
+		f_read_beat_addr <= f_read_beat_addr + (1<<ADDRLSB);
+	// }}}
+
+	// Read burst checking
+	// {{{
+
+	//
+	// ...
+	//
+
+	// }}}
+
+
+	// Match our read beat address to ARADDR
+	// {{{
+	// ...
+	// }}}
+
+	// Insist that our burst counters are consistent with bursts of a full
+	// length only
+	// {{{
+	// ...
+	// }}}
+
+	// RLAST checking
+	// {{{
+	// ...
+	// }}}
+
+	// Match the read beat address to the number of items remaining in this
+	// burst
+	// {{{
+	// ...
+	// }}}
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Internal assertions (Induction)
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	//
+	// On either error, or while waiting for a soft reset to complete
+	// nothing new should issue
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (f_past_valid && ($past(soft_reset) || $past(o_err)))
+	begin
+		assert(!$rose(M_AXI_AWVALID));
+		assert(!$rose(M_AXI_WVALID));
+		assert(!$rose(M_AXI_ARVALID));
+		assert(!phantom_write);
+		assert(!phantom_read);
+	end
+	// }}}
+
+	//
+	// Writes and reads always have enough room
+
+	// Bus writes aren't allowed to drain the incoming FIFO dry
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (!soft_reset && M_AXI_WVALID)
+		assert(ififo_fill + (skd_valid ? 1:0) >= writes_pending);
+	// }}}
+
+	// Bus reads aren't allowed to overflow the return FIFO
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (!soft_reset && M_AXI_RVALID)
+		assert(!ofifo_full);
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Write checks
+	//
+
+	// Make sure the skid buffer only reads when either there's nothing
+	// held in the buffer, or the write channel has accepted data.  Indeed,
+	// the write channel should never be active unless the skid buffer is
+	// full.
+	// {{{
+	always @(*)
+	if (!soft_reset && !skd_valid)
+		assert(!M_AXI_WVALID);
+
+	always @(*)
+	if (M_AXI_WVALID && M_AXI_WREADY)
+	begin
+		assert(read_from_fifo);
+	end else if (!skd_valid && !ififo_empty)
+		assert(read_from_fifo);
+	// }}}
+
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Read checks
+	// {{{
+
+	// No read checks in addition to the ones above
+
+	// }}}
+
+	////////////////////////////////////////
+	//
+	// Errors or resets -- do we properly end gracefully
+	//
+	// {{{
+	// Set o_err on any bus error.  Only clear it on reset
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (f_past_valid && $past(S_AXI_ARESETN))
+	begin
+		if ($past(M_AXI_BVALID && M_AXI_BRESP[1]))
+			assert(o_err);
+		if ($past(M_AXI_RVALID && M_AXI_RRESP[1]))
+			assert(o_err);
+		if ($past(!M_AXI_BVALID || !M_AXI_BRESP[1])
+			&& $past(!M_AXI_RVALID || !M_AXI_RRESP[1]))
+			assert(!$rose(o_err));
+	end
+
+	// Only release soft_reset once the bus is idle
+	// {{{
+	always @(posedge S_AXI_ACLK)
+	if (f_past_valid && $past(S_AXI_ARESETN) && $fell(soft_reset))
+	begin
+		//
+		// ...
+		//
+		assert(!M_AXI_AWVALID);
+		assert(!M_AXI_WVALID);
+		assert(!M_AXI_ARVALID);
+	end
+	// }}}
+	// }}}
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// FIFO checks
+	// {{{
+
+	// Check the global fill/emtpy values
+	// {{{
+	always @(*)
+		assert(vfifo_full == (vfifo_fill == (1<<(C_AXI_ADDR_WIDTH-ADDRLSB))));
+
+	always @(*)
+		assert(vfifo_fill <= (1<<(C_AXI_ADDR_WIDTH-ADDRLSB)));
+
+	always @(*)
+		assert(vfifo_empty == (vfifo_fill == 0));
+	// }}}
+
+	// An equation for vfill based upon our property checker's counters
+	// {{{
+	always @(*)
+	begin
+		f_vfill = M_AXI_AWADDR - M_AXI_ARADDR;
+		f_vfill[C_AXI_ADDR_WIDTH] = 0;
+		if (!M_AXI_AWVALID)
+			f_vfill = f_vfill - (writes_pending << ADDRLSB);
+		// ...
+		if (skd_valid)
+			f_vfill = f_vfill + (1<<ADDRLSB);
+		f_vfill = f_vfill + ((ififo_fill + ofifo_fill)<<ADDRLSB);
+	end
+	// }}}
+
+	// Make sure the virtual FIFO's fill matches that counter
+	// {{{
+	always @(*)
+	if (!soft_reset)
+	begin
+		assert(vfifo_fill == (f_vfill >> ADDRLSB));
+		assert(f_vfill <= (1<<(C_AXI_ADDR_WIDTH)));
+
+		// Before the equation check, double check that we
+		// don't overflow any of our arithmetic.  Then check our
+		// virtual FIFO's fill counter against the various internal
+		// FIFO fills and read counters.
+
+		// These are just inequality checks, however, so we'll still
+		// need a full equation check elsewhere
+		//
+		// ...
+		//
+	end
+
+	// Make certain we aren't overflowing in our subtraction above
+	always @(*)
+	if (M_AXI_ARVALID && !soft_reset)
+		assert(M_AXI_ARADDR != M_AXI_AWADDR);
+	// }}}
+
+	// Check mem_space_available
+	// {{{
+	always @(*)
+	begin
+		f_space_available = (M_AXI_AWADDR - M_AXI_ARADDR);
+		f_space_available[C_AXI_ADDR_WIDTH] = 0;
+		f_space_available = (1<<C_AXI_ADDR_WIDTH) - f_space_available;
+		if (M_AXI_AWVALID && !phantom_write)
+			f_space_available = f_space_available
+					- (1 << (LGMAXBURST+ADDRLSB));
+		//
+		// ...
+	end
+
+	always @(*)
+	begin
+		assert({ mem_data_available_w, {(LGMAXBURST){1'b0}} }
+			<= vfifo_fill);
+		// ...
+		assert(mem_data_available  <= (1<<C_AXI_ADDR_WIDTH));
+		assert(mem_space_available <= (1<<C_AXI_ADDR_WIDTH));
+		if (!soft_reset)
+		begin
+			assert(mem_space_available == f_space_available);
+
+			if (mem_space_available[C_AXI_ADDR_WIDTH])
+			begin
+				assert(M_AXI_ARADDR == M_AXI_AWADDR);
+				assert(!M_AXI_AWVALID || phantom_write);
+				// ...
+			end
+		end
+	end
+	// }}}
+
+	// Check mem_data_available
+	// {{{
+	// First, generate an equation to describe it
+	always @(*)
+	begin
+		f_data_available = M_AXI_AWADDR - M_AXI_ARADDR;
+		f_data_available[C_AXI_ADDR_WIDTH] = 0;
+		// ...
+		if (M_AXI_ARVALID && !phantom_read)
+			f_data_available = f_data_available
+				- (1 << (ADDRLSB + LGMAXBURST));
+	end
+
+	// Then compare it against that equation
+	always @(*)
+	if (!soft_reset)
+	begin
+		assert(mem_data_available == f_data_available);
+		if (mem_data_available[C_AXI_ADDR_WIDTH])
+		begin
+			assert(vfifo_fill[C_AXI_ADDR_WIDTH]);
+			assert(ofifo_empty);
+		end
+	end
+	// }}}
+
+	// ofifo_space_available
+	// {{{
+	always @(*)
+	if (!reset_fifo)
+	begin
+		// ...
+
+		// Make sure we don't overflow above
+		assert(ofifo_space_available <= (1<<LGFIFO));
+	end
+	// }}}
+
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Initial (only) constraints
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	always @(posedge S_AXI_ACLK)
+	if (!f_past_valid || $past(!S_AXI_ARESETN))
+	begin
+		assert(!M_AXI_AWVALID);
+		assert(!M_AXI_WVALID);
+		assert(!M_AXI_ARVALID);
+
+		assert(mem_space_available == (1<<C_AXI_ADDR_WIDTH));
+		assert(mem_data_available  == 0);
+
+		assert(!phantom_read);
+		assert(!phantom_write);
+
+		assert(vfifo_fill == 0);
+	end
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Formal contract checking
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// This core doesn't (yet) have any formal contract check
+
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Cover checks
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	reg	[2:0]		cvr_write_bursts, cvr_read_bursts;
+	(* anyconst *)	reg	cvr_high_speed;
+
+	always @(posedge S_AXI_ACLK)
+	if (cvr_high_speed)
+	begin
+		assume(!$fell(S_AXIS_TVALID));
+		// if (S_AXI_ARESETN && $past(S_AXIS_TVALID && !S_AXIS_TREADY))
+			// assume(S_AXIS_TVALID && $stable(S_AXIS_TDATA));
+
+		assume(M_AXI_AWREADY || writes_pending > 0);
+		assume(M_AXIS_TREADY);
+		assume(M_AXI_WREADY);
+		assume(M_AXI_ARREADY);
+	end
+
+	initial	cvr_write_bursts = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || soft_reset || o_err || o_overflow)
+		cvr_write_bursts <= 0;
+	else if (M_AXI_BVALID && !cvr_write_bursts[2])
+		cvr_write_bursts <= cvr_write_bursts + 1;
+
+	initial	cvr_read_bursts = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN || soft_reset || o_err || o_overflow)
+		cvr_read_bursts <= 0;
+	else if (M_AXI_RVALID && M_AXI_RLAST && !cvr_read_bursts[2])
+		cvr_read_bursts <= cvr_read_bursts + 1;
+
+	//
+	// ...
+	//
+
+	always @(posedge S_AXI_ACLK)
+	if (S_AXI_ARESETN && !soft_reset)
+		cover(cvr_read_bursts > 1 && cvr_write_bursts > 1);
+
+	always @(posedge S_AXI_ACLK)
+	if (S_AXI_ARESETN && !soft_reset)
+		cover(cvr_read_bursts > 1 && cvr_write_bursts > 1
+							&& cvr_high_speed);
+	// }}}
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Careless assumptions (i.e. constraints)
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// No careless assumptions.  Indeed, no assumptions at all beyond
+	// what's in the bus property file, and some optional cover assumptions.
+
+	// }}}
+	// }}}
+`endif
+endmodule
-- 
cgit v1.2.3