////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	aximm2s
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	Converts an AXI (full) memory port to an AXI-stream
//		interface.
// // {{{
//	While I am aware that other vendors sell similar components, if you
//	look under the hood you'll find no relation to anything but my own
//	work here.
//
// Registers:
//
//  0:	CMD_CONTROL
//		Controls the transaction via either starting or aborting an
//		ongoing transaction, provides feedback regarding the current
//		status.
//
//	[31]	r_busy
//		True if the core is in the middle of a transaction
//
//	[30]	r_err
//		True if the core has detected an error, a bus error
//		while the FIFO is reading.
//
//		Writing a '1' to this bit while the core is idle will clear it.
//		New transfers will not start until this bit is cleared.
//
//	[29]	r_complete
//		True if the transaction has completed, whether normally or
//		abnormally (error or abort).
//
//		Any write to the CMD_CONTROL register will clear this flag.
//
//	[28]	r_continuous
//		Normally the FIFO gets cleared and reset between operations.
//		However, if you set r_continuous, the core will then expect
//		a second operation to take place following the first one.
//		In this case, the operation will complete but the FIFO won't
//		get cleared.  During this time, the FIFO will not fill further.
//
//		Any write to the CMD_CONTROL register while the core is not
//		busy will adjust this bit.
//
//	[27]	!r_increment
//
//		If clear, the core reads from subsequent and incrementing
//		addresses.  If set, the core reads from the same address
//		throughout a transaction.
//
//		Writes to CMD_CONTROL while the core is idle will adjust this
//		bit.
//
//	[20:16]	LGFIFO
//		These are read-only bits, returning the size of the FIFO.
//
//	ABORT
//		If the core is busy, and ABORT_KEY (currently set to 8'h6d
//		below) is written to the top 8-bits of this register,
//		the current transfer will be aborted.  Any pending reads
//		will be completed, but nothing more will be written to the
//		stream.
//
//		Alternatively, the core will enter into an abort state
//		following any returned bus error indications.
//
//  4:	(Unused and reserved)
//
//  8-c:	CMD_ADDRLO, CMD_ADDR_HI
//	[C_AXI_ADDR_WIDTH-1:($clog2(C_AXI_DATA_WIDTH)-3)]
//		If idle, the address the core will read from when it starts.
//		If busy, the address the core is currently reading from.
//		Upon completion, the address either returns to the starting
//		address (if r_continuous is clear), or otherwise becomes the
//		address where the core left off.  In the case of an abort or an
//		error, this will be (near) the address that was last read.
//
//		Why "near"?  Because this address records the reads that have
//		been issued while no error is pending.  If a bus error return
//		comes back, there may have been several more reads issued before
//		that error address.
//
//  10-14:	(Unused and reserved)
//
//  18-1c:  CMD_LENLO, CMD_LENHI
//	[LGLEN-1:0]
//		The size of the transfer in bytes.  Only accepts aligned
//		addresses, therefore bits [($clog2(C_AXI_DATA_WIDTH)-3):0]
//		will always be forced to zero.  To find out what size bus
//		this core is conencted to, or the maximum transfer length,
//		write a -1 to this value and read the returning result.
//		Only the active bits will be set.
//
//		While the core is busy, reads from this address will return
//		the number of items still to be read from the bus.
//
//		I hope to eventually add support for unaligned bursts.  Such
//		support is not currently part of this core.
//
// }}}
//
// Status:
// {{{
//	1. The core passes both cover checks and formal property (assertion)
//		based checks.  It has not (yet) been tested in real hardware.
//
//	2. I'd like to support unaligned addresses and lengths.  This will
//		require aligning the data coming out of the FIFO as well.
//		As written, the core doesn't yet support these.
//
// }}}
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2019-2020, Gisselquist Technology, LLC
// {{{
// This file is part of the WB2AXIP project.
//
// The WB2AXIP project contains free software and gateware, licensed under the
// Apache License, Version 2.0 (the "License").  You may not use this project,
// or this file, except in compliance with the License.  You may obtain a copy
// of the License at
//
//	http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  See the
// License for the specific language governing permissions and limitations
// under the License.
//
////////////////////////////////////////////////////////////////////////////////
// }}}
//
`default_nettype none
//
module	aximm2s #(
		// {{{
		parameter	C_AXI_ADDR_WIDTH = 32,
		parameter	C_AXI_DATA_WIDTH = 32,
		parameter	C_AXI_ID_WIDTH = 1,
		//
		// We support five 32-bit AXI-lite registers, requiring 5-bits
		// of AXI-lite addressing
		localparam	C_AXIL_ADDR_WIDTH = 5,
		localparam	C_AXIL_DATA_WIDTH = 32,
		//
		// The bottom ADDRLSB bits of any AXI address are subword bits
		localparam	ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3,
		localparam	AXILLSB = $clog2(C_AXIL_DATA_WIDTH)-3,
		//
		// OPT_UNALIGNED: Allow unaligned accesses, address requests
		// and sizes which may or may not match the underlying data
		// width.  If set, the core will quietly align these requests.
		parameter [0:0]	OPT_UNALIGNED = 1'b0,
		//
		// OPT_TKEEP [Future]: If set, will also add TKEEP signals to
		// the outgoing slave interface.  This is necessary if ever you
		// wish to output partial stream words, such as might happen if
		// the length were ever something other than a full number of
		// words.  (Not yet implemented)
		// parameter [0:0]	OPT_TKEEP = 1'b0,
		//
		// OPT_TLAST: If enabled, will embed TLAST=1 at the end of every
		// commanded burst.  If  disabled, TLAST will be set to a
		// constant 1'b1.
		parameter [0:0]	OPT_TLAST = 1'b0,
		//
		// ABORT_KEY is the value that, when written to the top 8-bits
		// of the control word, will abort any ongoing operation.
		parameter [7:0]	ABORT_KEY = 8'h6d,
		//
		// The size of the FIFO
		parameter	LGFIFO = 9,
		//
		// Maximum number of bytes that can ever be transferred, in
		// log-base 2
		parameter	LGLEN  = 20,
		//
		// AXI_ID is the ID we will use for all of our AXI transactions
		parameter	AXI_ID = 0
		// }}}
	) (
		// {{{
		input	wire					S_AXI_ACLK,
		input	wire					S_AXI_ARESETN,
		//
		// The stream interface
		// {{{
		output	wire					M_AXIS_TVALID,
		input	wire					M_AXIS_TREADY,
		output	wire	[C_AXI_DATA_WIDTH-1:0]		M_AXIS_TDATA,
		output	wire					M_AXIS_TLAST,
		// }}}
		//
		// The control interface
		// {{{
		input	wire					S_AXIL_AWVALID,
		output	wire					S_AXIL_AWREADY,
		input	wire	[C_AXIL_ADDR_WIDTH-1:0]		S_AXIL_AWADDR,
		input	wire	[2:0]				S_AXIL_AWPROT,
		//
		input	wire					S_AXIL_WVALID,
		output	wire					S_AXIL_WREADY,
		input	wire	[C_AXIL_DATA_WIDTH-1:0]		S_AXIL_WDATA,
		input	wire	[C_AXIL_DATA_WIDTH/8-1:0]	S_AXIL_WSTRB,
		//
		output	wire					S_AXIL_BVALID,
		input	wire					S_AXIL_BREADY,
		output	wire	[1:0]				S_AXIL_BRESP,
		//
		input	wire					S_AXIL_ARVALID,
		output	wire					S_AXIL_ARREADY,
		input	wire	[C_AXIL_ADDR_WIDTH-1:0]		S_AXIL_ARADDR,
		input	wire	[2:0]				S_AXIL_ARPROT,
		//
		output	wire					S_AXIL_RVALID,
		input	wire					S_AXIL_RREADY,
		output	wire	[C_AXIL_DATA_WIDTH-1:0]		S_AXIL_RDATA,
		output	wire	[1:0]				S_AXIL_RRESP,
		// }}}
		//

		//
		// The AXI (full) read interface
		// {{{
		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,
		output	wire	[7:0]			M_AXI_ARLEN,
		output	wire	[2:0]			M_AXI_ARSIZE,
		output	wire	[1:0]			M_AXI_ARBURST,
		output	wire				M_AXI_ARLOCK,
		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_DATA_WIDTH-1:0]	M_AXI_RDATA,
		input	wire				M_AXI_RLAST,
		input	wire	[C_AXI_ID_WIDTH-1:0]	M_AXI_RID,
		input	wire	[1:0]			M_AXI_RRESP,
		// }}}
		//
		//
		// Create an output signal to indicate that we've finished
		output	reg				o_int
		// }}}
	);
	// Local parameter declarations
	// {{{
	localparam [2:0]	CMD_CONTROL   = 3'b000,
				CMD_UNUSED_1  = 3'b001,
				CMD_ADDRLO    = 3'b010,
				CMD_ADDRHI    = 3'b011,
				CMD_UNUSED_2  = 3'b100,
				CMD_UNUSED_3  = 3'b101,
				CMD_LENLO     = 3'b110,
				CMD_LENHI     = 3'b111;
	localparam		CBIT_BUSY	= 31,
				CBIT_ERR	= 30,
				CBIT_COMPLETE	= 29,
				CBIT_CONTINUOUS	= 28,
				CBIT_INCREMENT	= 27;
	localparam	LGMAXBURST=(LGFIFO > 8) ? 8 : LGFIFO-1;
	localparam	LGMAX_FIXED_BURST = 4,
			MAX_FIXED_BURST = 16;
	localparam	LGLENW  = LGLEN  - ($clog2(C_AXI_DATA_WIDTH)-3),
			LGLENWA = LGLENW + (OPT_UNALIGNED ? 1:0);
	localparam	LGFIFOB = LGFIFO + ($clog2(C_AXI_DATA_WIDTH)-3);
	localparam [ADDRLSB-1:0] LSBZEROS = 0;
	// }}}

	wire	i_clk   =  S_AXI_ACLK;
	wire	i_reset = !S_AXI_ARESETN;

	// Signal declarations
	// {{{
	reg	r_busy, r_err, r_complete, r_continuous, r_increment,
		cmd_abort, zero_length,
		w_cmd_start, w_complete, w_cmd_abort;
	// reg	cmd_start;
	reg				axi_abort_pending;

	reg	[LGLENWA-1:0]		ar_requests_remaining,
					ar_bursts_outstanding;
	reg	[LGMAXBURST:0]		r_max_burst;
	reg	[C_AXI_ADDR_WIDTH-1:0]	axi_raddr;

	reg	[C_AXI_ADDR_WIDTH-1:0]	cmd_addr;
	reg	[LGLENW-1:0]		cmd_length_w;
	reg	[LGLENWA-1:0]		cmd_length_aligned_w;
	reg				unaligned_cmd_addr;

	// FIFO signals
	wire				reset_fifo, write_to_fifo,
					read_from_fifo;
	wire	[C_AXI_DATA_WIDTH-1:0]	write_data;
	wire	[LGFIFO:0]		fifo_fill;
	wire				fifo_full, fifo_empty;

	wire				awskd_valid, axil_write_ready;
	wire	[C_AXIL_ADDR_WIDTH-AXILLSB-1:0]	awskd_addr;
	//
	wire				wskd_valid;
	wire	[C_AXIL_DATA_WIDTH-1:0]	wskd_data;
	wire [C_AXIL_DATA_WIDTH/8-1:0]	wskd_strb;
	reg				axil_bvalid;
	//
	wire				arskd_valid, axil_read_ready;
	wire	[C_AXIL_ADDR_WIDTH-AXILLSB-1:0]	arskd_addr;
	reg	[C_AXIL_DATA_WIDTH-1:0]	axil_read_data;
	reg				axil_read_valid;
	reg	[C_AXIL_DATA_WIDTH-1:0]	w_status_word;
	reg	[2*C_AXIL_DATA_WIDTH-1:0]	wide_address, wide_length,
					new_wideaddr, new_widelen;
	wire	[C_AXIL_DATA_WIDTH-1:0]	new_cmdaddrlo, new_cmdaddrhi,
					new_lengthlo, new_lengthhi;


	reg				axi_arvalid;
	reg	[C_AXI_ADDR_WIDTH-1:0]	axi_araddr;
	reg	[7:0]			axi_arlen;
	reg	[1:0]			axi_arburst;

	// Speed up checking for zeros
	reg				ar_none_remaining,
					ar_none_outstanding,
					phantom_start, start_burst;
	reg				partial_burst_requested;
	reg	[LGMAXBURST-1:0]	addralign;
	reg	[LGFIFO:0]		rd_uncommitted;
	reg				w_increment;
	reg	[LGMAXBURST:0]		initial_burstlen;
	reg	[LGLENWA-1:0]		rd_reads_remaining;
	reg				rd_none_remaining,
					rd_last_remaining;

	wire				realign_last_valid;
/*
					wr_none_pending, r_none_remaining;

	reg				w_phantom_start, phantom_start;
	reg	[LGFIFO:0]	next_fill;
*/

	// }}}

	////////////////////////////////////////////////////////////////////////
	//
	// AXI-lite signaling
	//
	////////////////////////////////////////////////////////////////////////
	//
	// This is mostly the skidbuffer logic, and handling of the VALID
	// and READY signals for the AXI-lite control logic in the next
	// section.
	// {{{

	//
	// Write signaling
	//
	// {{{

	skidbuffer #(.OPT_OUTREG(0), .DW(C_AXIL_ADDR_WIDTH-AXILLSB))
	axilawskid(//
		.i_clk(S_AXI_ACLK), .i_reset(i_reset),
		.i_valid(S_AXIL_AWVALID), .o_ready(S_AXIL_AWREADY),
		.i_data(S_AXIL_AWADDR[C_AXIL_ADDR_WIDTH-1:AXILLSB]),
		.o_valid(awskd_valid), .i_ready(axil_write_ready),
		.o_data(awskd_addr));

	skidbuffer #(.OPT_OUTREG(0), .DW(C_AXIL_DATA_WIDTH+C_AXIL_DATA_WIDTH/8))
	axilwskid(//
		.i_clk(S_AXI_ACLK), .i_reset(i_reset),
		.i_valid(S_AXIL_WVALID), .o_ready(S_AXIL_WREADY),
		.i_data({ S_AXIL_WDATA, S_AXIL_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_AXIL_BVALID || S_AXIL_BREADY);

	initial	axil_bvalid = 0;
	always @(posedge i_clk)
	if (i_reset)
		axil_bvalid <= 0;
	else if (axil_write_ready)
		axil_bvalid <= 1;
	else if (S_AXIL_BREADY)
		axil_bvalid <= 0;

	assign	S_AXIL_BVALID = axil_bvalid;
	assign	S_AXIL_BRESP = 2'b00;
	// }}}

	//
	// Read signaling
	//
	// {{{

	skidbuffer #(.OPT_OUTREG(0), .DW(C_AXIL_ADDR_WIDTH-AXILLSB))
	axilarskid(//
		.i_clk(S_AXI_ACLK), .i_reset(i_reset),
		.i_valid(S_AXIL_ARVALID), .o_ready(S_AXIL_ARREADY),
		.i_data(S_AXIL_ARADDR[C_AXIL_ADDR_WIDTH-1:AXILLSB]),
		.o_valid(arskd_valid), .i_ready(axil_read_ready),
		.o_data(arskd_addr));

	assign	axil_read_ready = arskd_valid
				&& (!axil_read_valid || S_AXIL_RREADY);

	initial	axil_read_valid = 1'b0;
	always @(posedge i_clk)
	if (i_reset)
		axil_read_valid <= 1'b0;
	else if (axil_read_ready)
		axil_read_valid <= 1'b1;
	else if (S_AXIL_RREADY)
		axil_read_valid <= 1'b0;

	assign	S_AXIL_RVALID = axil_read_valid;
	assign	S_AXIL_RDATA  = axil_read_data;
	assign	S_AXIL_RRESP = 2'b00;
	// }}}

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// AXI-lite controlled logic
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{

	//
	// Abort transaction
	//
	always @(*)
	begin
		w_cmd_abort = 0;
		w_cmd_abort = (axil_write_ready && awskd_addr == CMD_CONTROL)
			&& (wskd_strb[3] && wskd_data[31:24] == ABORT_KEY);
		if (!r_busy)
			w_cmd_abort = 0;
	end

	initial	cmd_abort = 0;
	always @(posedge i_clk)
	if (i_reset)
		cmd_abort <= 0;
	else
		cmd_abort <= (cmd_abort && r_busy)||w_cmd_abort;

	//
	// Start command
	//
	always @(*)
	if (r_busy)
		w_cmd_start = 0;
	else begin
		w_cmd_start = 0;
		if ((axil_write_ready && awskd_addr == CMD_CONTROL)
			&& (wskd_strb[3] && wskd_data[CBIT_BUSY]))
			w_cmd_start = 1;
		if (r_err && !wskd_data[CBIT_ERR])
			w_cmd_start = 0;
		if (zero_length)
			w_cmd_start = 0;
		if (OPT_UNALIGNED && unaligned_cmd_addr
				&& wskd_data[CBIT_INCREMENT])
			w_cmd_start = 0;
	end

	//
	// Calculate busy or complete flags
	//
	initial	r_busy     = 0;
	initial	r_complete = 0;
	always @(posedge i_clk)
	if (i_reset)
	begin
		r_busy     <= 0;
		r_complete <= 0;
	end else if (!r_busy)
	begin
		if (w_cmd_start)
			r_busy <= 1'b1;
		if (axil_write_ready && awskd_addr == CMD_CONTROL)
			// Any write to the control register will clear the
			// completion flag
			r_complete <= 1'b0;
	end else if (r_busy)
	begin
		if (w_complete)
		begin
			r_complete <= 1;
			r_busy <= 1'b0;
		end
	end

	//
	// Interrupts
	//
	initial	o_int = 0;
	always @(posedge i_clk)
	if (i_reset)
		o_int <= 0;
	else
		o_int <= (r_busy && w_complete);

	//
	// Error conditions
	//
	always @(posedge i_clk)
	if (i_reset)
		r_err <= 0;
	else if (!r_busy)
	begin
		if (axil_write_ready && awskd_addr == CMD_CONTROL)
		begin
			if (!w_cmd_abort)
				r_err <= r_err && (!wskd_strb[3] || !wskd_data[CBIT_ERR]);
			// On any request to start a transfer with an unaligned
			// address, that's not incrementing--declare an
			// immediate error
			if (wskd_strb[3] && wskd_data[CBIT_BUSY]
				&& wskd_data[CBIT_INCREMENT]
				&& (OPT_UNALIGNED && unaligned_cmd_addr))
				r_err <= 1'b1;
		end
	end else // if (r_busy)
	begin
		if (M_AXI_RVALID && M_AXI_RREADY && M_AXI_RRESP[1])
			r_err <= 1'b1;
	end

	initial	r_continuous = 0;
	always @(posedge i_clk)
	if (i_reset)
		r_continuous <= 0;
	else begin
		if (!r_busy && axil_write_ready && awskd_addr == CMD_CONTROL
			&& !w_cmd_abort)
			r_continuous <= wskd_strb[3] && wskd_data[CBIT_CONTINUOUS];
	end

	always @(*)
	begin
		wide_address = 0;
		wide_address[C_AXI_ADDR_WIDTH-1:0] = cmd_addr;
		if (!OPT_UNALIGNED)
			wide_address[ADDRLSB-1:0] = 0;

		wide_length  = 0;
		wide_length[ADDRLSB +: LGLENW] = cmd_length_w;
	end

	assign	new_cmdaddrlo = apply_wstrb(
			wide_address[C_AXIL_DATA_WIDTH-1:0],
			wskd_data, wskd_strb);

	assign	new_cmdaddrhi = apply_wstrb(
			wide_address[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH],
			wskd_data, wskd_strb);

	assign	new_lengthlo = apply_wstrb(
			wide_length[C_AXIL_DATA_WIDTH-1:0],
			wskd_data, wskd_strb);

	assign	new_lengthhi = apply_wstrb(
			wide_length[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH],
			wskd_data, wskd_strb);

	always @(*)
	begin
		new_wideaddr = wide_address;

		if (awskd_addr == CMD_ADDRLO)
			new_wideaddr[C_AXIL_DATA_WIDTH-1:0] = new_cmdaddrlo;
		if (awskd_addr == CMD_ADDRHI)
			new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH] = new_cmdaddrhi;
		if (!OPT_UNALIGNED)
			new_wideaddr[ADDRLSB-1:0] = 0;
		new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH] = 0;


		new_widelen = wide_length;
		if (awskd_addr == CMD_LENLO)
			new_widelen[C_AXIL_DATA_WIDTH-1:0] = new_lengthlo;
		if (awskd_addr == CMD_LENHI)
			new_widelen[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH] = new_lengthhi;
		new_widelen[ADDRLSB-1:0] = 0;
		new_widelen[2*C_AXIL_DATA_WIDTH-1:ADDRLSB+LGLENW] = 0;
	end


	initial	r_increment   = 1'b1;
	initial	cmd_addr      = 0;
	initial	cmd_length_w  = 0;	// Counts in bytes
	initial	zero_length   = 1;
	initial	cmd_length_aligned_w = 0;
	initial	unaligned_cmd_addr = 1'b0;
	always @(posedge i_clk)
	if (i_reset)
	begin
		r_increment <= 1'b1;
		cmd_addr      <= 0;
		cmd_length_w  <= 0;
		cmd_length_aligned_w  <= 0;
		zero_length   <= 1;
		unaligned_cmd_addr <= 1'b0;
	end else if (axil_write_ready && !r_busy)
	begin
		case(awskd_addr)
		CMD_CONTROL:
			r_increment <= !wskd_data[CBIT_INCREMENT];
		CMD_ADDRLO: begin
			cmd_addr <= new_wideaddr[C_AXI_ADDR_WIDTH-1:0];
			unaligned_cmd_addr <= |new_wideaddr[ADDRLSB-1:0];
			if (!OPT_UNALIGNED)
				unaligned_cmd_addr <= 1'b0;
			else
				cmd_length_aligned_w <= cmd_length_w
					+ (|new_wideaddr[ADDRLSB-1:0] ? 1:0);
			// ERR: What if !r_increment?  In that case, we can't
			//   support unaligned addressing
			end
		CMD_ADDRHI: if (C_AXI_ADDR_WIDTH > C_AXIL_DATA_WIDTH)
			begin
			cmd_addr <= new_wideaddr[C_AXI_ADDR_WIDTH-1:0];
			end
		CMD_LENLO: begin
			cmd_length_w <= new_widelen[ADDRLSB +: LGLENW];
			zero_length <= (new_widelen[ADDRLSB +: LGLENW] == 0);
			cmd_length_aligned_w <= new_widelen[ADDRLSB +: LGLENW]
				+ (unaligned_cmd_addr ? 1:0);
			end
		CMD_LENHI: begin
			cmd_length_w <= new_widelen[ADDRLSB +: LGLENW];
			zero_length <= (new_widelen[ADDRLSB +: LGLENW] == 0);
			cmd_length_aligned_w <= new_widelen[ADDRLSB +: LGLENW]
				+ (unaligned_cmd_addr ? 1:0);
			end
		default: begin end
		endcase
	end else if(r_busy && r_continuous && !axi_abort_pending && r_increment)
		cmd_addr <= axi_raddr
			+ ((M_AXI_RVALID && !M_AXI_RRESP[1]
				&& (!unaligned_cmd_addr || realign_last_valid))
				? (1<<ADDRLSB) : 0);

	always @(*)
	begin
		w_status_word = 0;
		w_status_word[CBIT_BUSY]	= r_busy;
		w_status_word[CBIT_ERR]		= r_err;
		w_status_word[CBIT_COMPLETE]	= r_complete;
		w_status_word[CBIT_CONTINUOUS]	= r_continuous;
		w_status_word[CBIT_INCREMENT]	= !r_increment;
		w_status_word[20:16] = LGFIFO;
	end

	always @(posedge i_clk)
	if (!axil_read_valid || S_AXIL_RREADY)
	begin
		axil_read_data <= 0;
		case(arskd_addr)
		CMD_CONTROL:	axil_read_data <= w_status_word;
		CMD_ADDRLO:	axil_read_data <= wide_address[C_AXIL_DATA_WIDTH-1:0];
		CMD_ADDRHI:	axil_read_data <= wide_address[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH];
		CMD_LENLO:	axil_read_data <= wide_length[C_AXIL_DATA_WIDTH-1:0];
		CMD_LENHI:	axil_read_data <= wide_length[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH];
		default		axil_read_data <= 0;
		endcase
	end

	function [C_AXIL_DATA_WIDTH-1:0]	apply_wstrb;
		input	[C_AXIL_DATA_WIDTH-1:0]		prior_data;
		input	[C_AXIL_DATA_WIDTH-1:0]		new_data;
		input	[C_AXIL_DATA_WIDTH/8-1:0]	wstrb;

		integer	k;
		for(k=0; k<C_AXIL_DATA_WIDTH/8; k=k+1)
		begin
			apply_wstrb[k*8 +: 8]
				= wstrb[k] ? new_data[k*8 +: 8] : prior_data[k*8 +: 8];
		end
	endfunction

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// The data FIFO section
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{
	assign	reset_fifo = i_reset || (!r_busy && (!r_continuous || r_err));

	// Realign the data (if OPT_UNALIGN) before sending it to the FIFO
	// {{{
	// This allows us to handle unaligned addresses.
	generate if (OPT_UNALIGNED)
	begin : REALIGN_DATA

		reg				r_write_to_fifo;
		reg	[C_AXI_DATA_WIDTH-1:0]	last_data,
						r_write_data;
		reg	[ADDRLSB-1:0]		corollary_shift;
		reg				last_valid;
		reg	[ADDRLSB-1:0]		realignment;

		always @(*)
			realignment = cmd_addr[ADDRLSB-1:0];

		initial	last_data = 0;
		always @(posedge S_AXI_ACLK)
		if (reset_fifo || !unaligned_cmd_addr)
			last_data <= 0;
		else if (M_AXI_RVALID && M_AXI_RREADY)
			last_data <= M_AXI_RDATA >> (realignment * 8);

		initial	last_valid = 1'b0;
		always @(posedge S_AXI_ACLK)
		if (reset_fifo)
			last_valid <= 0;
		else if (M_AXI_RVALID && M_AXI_RREADY)
			last_valid <= 1'b1;
		else if (!r_busy)
			last_valid <= 1'b0;

		assign	realign_last_valid = last_valid;

		always @(*)
			corollary_shift = -realignment*8;

		always @(posedge S_AXI_ACLK)
		if (M_AXI_RVALID && M_AXI_RREADY)
			r_write_data <= (M_AXI_RDATA << corollary_shift)
					| last_data;
		else if (!fifo_full)
			r_write_data <= last_data;

		initial	r_write_to_fifo = 1'b0;
		always @(posedge S_AXI_ACLK)
		if (reset_fifo)
			r_write_to_fifo <= 1'b0;
		else if (M_AXI_RVALID && M_AXI_RREADY)
			r_write_to_fifo <= last_valid || !unaligned_cmd_addr;
		else if (!fifo_full)
			r_write_to_fifo <= 1'b0;

		assign	write_to_fifo = r_write_to_fifo;
		assign	write_data = r_write_data;

	end else begin : ALIGNED_DATA

		assign	write_to_fifo  = M_AXI_RVALID && M_AXI_RREADY;
		assign	write_data = M_AXI_RDATA;
		assign	realign_last_valid = 0;

	end endgenerate
	// }}}

	assign	read_from_fifo = M_AXIS_TVALID && M_AXIS_TREADY;
	assign	M_AXIS_TVALID  = !fifo_empty;

	// Write the results to the FIFO
	// {{{
	generate if (OPT_TLAST)
	begin : FIFO_W_TLAST
		// FIFO section--used if we have to add a TLAST signal to the
		// data stream
		// {{{
		reg	pre_tlast;
		wire	tlast;

		// tlast will be set on the last data word of any commanded
		// burst.

		// Appropriately, pre_tlast = (something) && M_AXI_RVALID
		//			&& M_AXI_RREADY && M_AXI_RLAST
		// We can simplify this greatly, since any time M_AXI_RVALID is
		// true, we also know that M_AXI_RREADY will be true.  This
		// allows us to get rid of the RREADY condition.  Next, we can
		// simplify the RVALID condition since we'll never write to the
		// FIFO if RVALID isn't also true.  Finally, we can get rid of
		// M_AXI_RLAST since this is captured by rd_last_remaining.
		always @(*)
			pre_tlast = rd_last_remaining;

		if (OPT_UNALIGNED)
		begin
			reg	r_tlast;

			// REALIGN delays the data by one clock period.  We'll
			// also need to delay the last as well.
			// Note that no one cares what tlast is if write_to_fifo
			// is zero, allowing us to massively simplify this.
			always @(posedge i_clk)
				r_tlast <= pre_tlast;

			assign	tlast = r_tlast;

		end else begin

			assign	tlast = pre_tlast;
		end


		sfifo #(.BW(C_AXI_DATA_WIDTH+1), .LGFLEN(LGFIFO))
		sfifo(i_clk, reset_fifo,
			write_to_fifo, { tlast, write_data }, fifo_full, fifo_fill,
			read_from_fifo, { M_AXIS_TLAST, M_AXIS_TDATA }, fifo_empty);
		// }}}
	end else begin : NO_TLAST_FIFO

		// FIFO section, where TLAST is held at 1'b1
		// {{{
		sfifo #(.BW(C_AXI_DATA_WIDTH), .LGFLEN(LGFIFO))
		sfifo(i_clk, reset_fifo,
			write_to_fifo, write_data, fifo_full, fifo_fill,
			read_from_fifo, M_AXIS_TDATA, fifo_empty);

		assign	M_AXIS_TLAST = 1'b1;
		// }}}
	end endgenerate
	// }}}


	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// The incoming AXI (full) protocol section
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	// {{{

	// Some counters to keep track of our state
	// {{{


	// Count the number of word writes left to be requested, starting
	// with the overall command length and then reduced by M_AWLEN on
	// each address write
	// {{{
	initial	ar_none_remaining = 1;
	initial	ar_requests_remaining = 0;
	always @(posedge i_clk)
	if (!r_busy)
	begin
		ar_requests_remaining <= cmd_length_aligned_w;
		ar_none_remaining     <= zero_length;
	end else if (cmd_abort || axi_abort_pending)
	begin
		ar_requests_remaining <= 0;
		ar_none_remaining <= 1;
	end else if (phantom_start)
	begin
		// Verilator lint_off WIDTH
		ar_requests_remaining
			<= ar_requests_remaining - (M_AXI_ARLEN + 1);
		ar_none_remaining <= (ar_requests_remaining == (M_AXI_ARLEN+1));
		// Verilator lint_on WIDTH
	end
	// }}}

	// Calculate the maximum possible burst length, ignoring 4kB boundaries
	// {{{
	always @(*)
		addralign = 1+(~cmd_addr[ADDRLSB +: LGMAXBURST]);
	always @(*)
		w_increment = !wskd_data[CBIT_INCREMENT];

	always @(*)
	begin
		initial_burstlen = (1<<LGMAXBURST);
		if (!w_increment)
		begin
			if (LGMAXBURST <= LGMAX_FIXED_BURST)
				initial_burstlen = (1<<LGMAXBURST);
			else
				initial_burstlen = MAX_FIXED_BURST;
			if (cmd_length_aligned_w < { {(LGLENWA-LGMAXBURST-1){1'b0}},
						initial_burstlen })
				initial_burstlen = cmd_length_aligned_w[LGMAXBURST:0];
		end else if (cmd_length_aligned_w >= (1<<LGMAXBURST))
		begin
			if (|cmd_addr[ADDRLSB +: LGMAXBURST])
				initial_burstlen = { 1'b0, addralign };
		end else begin
			initial_burstlen = cmd_length_aligned_w[LGMAXBURST:0];
			if ((|cmd_addr[ADDRLSB +: LGMAXBURST])
				&&({{(LGLENW-LGMAXBURST){1'b0}}, addralign } < cmd_length_aligned_w))
				initial_burstlen = { 1'b0, addralign };
		end
	end

	initial	r_max_burst = 0;
	always @(posedge i_clk)
	if (!r_busy)
	begin
		// Force us to align ourself early
		//   That way we don't need to check for
		//   alignment (again) later
		r_max_burst <= initial_burstlen;
	end else if (phantom_start)
	begin
		// Verilator lint_off WIDTH
		if (r_increment || LGMAXBURST <= LGMAX_FIXED_BURST)
		begin : LIMIT_BY_LGMAXBURST
			if (ar_requests_remaining < (1<<LGMAXBURST) + (M_AXI_ARLEN+1))
				r_max_burst <= ar_requests_remaining[8:0] - (M_AXI_ARLEN+1);
			else
				r_max_burst <= (1<<LGMAXBURST);
		end else begin : LIMIT_BY_SIXTEEN
			if (ar_requests_remaining < MAX_FIXED_BURST + (M_AXI_ARLEN+1))
				r_max_burst <= ar_requests_remaining[8:0] - (M_AXI_ARLEN+1);
			else
				r_max_burst <= MAX_FIXED_BURST;
		end
		// Verilator lint_on WIDTH
	end
	// }}}

	// Count the number of bursts outstanding--these are the number of
	// ARVALIDs that have been accepted, but for which the RVALID && RLAST
	// has not (yet) been returned.
	// {{{
	initial	ar_none_outstanding   = 1;
	initial	ar_bursts_outstanding = 0;
	always @(posedge i_clk)
	if (i_reset)
	begin
		ar_bursts_outstanding <= 0;
		ar_none_outstanding <= 1;
	end else case ({ phantom_start,
				M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST })
	2'b01:	begin
			ar_bursts_outstanding <=  ar_bursts_outstanding - 1;
			ar_none_outstanding   <= (ar_bursts_outstanding == 1);
		end
	2'b10:	begin
		ar_bursts_outstanding <= ar_bursts_outstanding + 1;
		ar_none_outstanding <= 0;
		end
	default: begin end
	endcase
	// }}}

	// Are we there yet?
	// {{{
	initial	rd_reads_remaining = 0;
	initial	rd_none_remaining = 1;
	initial	rd_last_remaining = 0;
	always @(posedge  i_clk)
	if (!r_busy)
	begin
		rd_reads_remaining <= cmd_length_aligned_w;
		rd_last_remaining  <= (cmd_length_aligned_w == 1);
		rd_none_remaining  <= (cmd_length_aligned_w == 0);
	end else if (M_AXI_RVALID && M_AXI_RREADY)
	begin
		rd_reads_remaining <= rd_reads_remaining - 1;
		rd_last_remaining  <= (rd_reads_remaining == 2);
		rd_none_remaining  <= (rd_reads_remaining == 1);
	end

	always @(*)
	if (!r_busy)
		w_complete = 0;
	else if (axi_abort_pending && ar_none_outstanding && !M_AXI_ARVALID)
		w_complete = 1;
	else if (r_continuous)
		w_complete = (rd_none_remaining)||((rd_last_remaining) && M_AXI_RVALID && M_AXI_RREADY);
	else // if !r_continuous
		w_complete = (rd_none_remaining && fifo_empty);

	// }}}

	// Are we stopping early?  Aborting something ongoing?
	// {{{
	initial	axi_abort_pending = 0;
	always @(posedge i_clk)
	if (i_reset || !r_busy)
		axi_abort_pending <= 0;
	else begin
		if (M_AXI_RVALID && M_AXI_RREADY && M_AXI_RRESP[1])
			axi_abort_pending <= 1;
		if (cmd_abort)
			axi_abort_pending <= 1;
	end
	// }}}

	// Count the number of uncommited spaces in the FIFO
	// {{{
	generate if (OPT_UNALIGNED)
	begin
		initial	partial_burst_requested <= 1'b1;
		always @(posedge i_clk)
		if (!r_busy)
			partial_burst_requested <= !unaligned_cmd_addr;
		else if (phantom_start)
			partial_burst_requested <= 1'b1;
	end else begin

		always @(*)
			partial_burst_requested = 1'b1;
	end endgenerate

	initial	rd_uncommitted = (1<<LGFIFO);
	always @(posedge i_clk)
	if (reset_fifo)
	begin
		rd_uncommitted <= (1<<LGFIFO);
	end else case ({ phantom_start,
			M_AXIS_TVALID && M_AXIS_TREADY })
	2'b00: begin end
	2'b01: begin
		rd_uncommitted <= rd_uncommitted + 1;
		end
	2'b10: begin
		// Verilator lint_off WIDTH
		rd_uncommitted <= rd_uncommitted - (M_AXI_ARLEN + 1)
			+ (partial_burst_requested ? 0 :1);
		end
	2'b11: begin
		rd_uncommitted <= rd_uncommitted - (M_AXI_ARLEN)
			+ (partial_burst_requested ? 0 :1);
		// Verilator lint_on WIDTH
		end
	endcase
	// }}}

	// So that we can monitor where we are at, and perhaps restart it
	// later, keep track of the current address used by the R-channel
	// {{{

	initial	axi_raddr = 0;
	always @(posedge i_clk)
	begin
		if (!r_busy)
			axi_raddr <= cmd_addr;
		else if (axi_abort_pending || !r_increment)
			// Stop incrementing tthe address following an abort
			axi_raddr <= axi_raddr;
		else begin
			if (M_AXI_RVALID && M_AXI_RREADY && !M_AXI_RRESP[1]
				&& (!unaligned_cmd_addr || realign_last_valid))
				axi_raddr <= axi_raddr + (1<<ADDRLSB);
		end

		if (!OPT_UNALIGNED)
			axi_raddr[ADDRLSB-1:0] <= 0;
	end

	// }}}

	//
	// }}}

	always @(*)
	begin
		start_burst = !ar_none_remaining;
		if (rd_uncommitted< {{(LGFIFO-LGMAXBURST){1'b0}}, r_max_burst})
			start_burst = 0;
		if (phantom_start)
			// Insist on a minimum of one clock between burst
			// starts, so we can get our lengths right
			start_burst = 0;
		if (M_AXI_ARVALID && !M_AXI_ARREADY)
			start_burst = 0;
		if (!r_busy || cmd_abort || axi_abort_pending)
			start_burst  = 0;
	end

	initial	phantom_start = 0;
	always @(posedge i_clk)
	if (i_reset)
		phantom_start <= 0;
	else
		phantom_start <= start_burst;
	// }}}


	// Calculate ARLEN and ARADDR for the next ARVALID
	// {{{
	initial	axi_araddr = 0;
	always @(posedge i_clk)
	if (!M_AXI_ARVALID || M_AXI_ARREADY)
	begin
		if (!r_busy)
			axi_araddr <= cmd_addr;
		else if (M_AXI_ARVALID && r_increment)
		begin
			// Verilator lint_off WIDTH
			axi_araddr[C_AXI_ADDR_WIDTH-1:ADDRLSB]
				<= axi_araddr[C_AXI_ADDR_WIDTH-1:ADDRLSB]
					+ (M_AXI_ARLEN + 1);
			// Verilator lint_on  WIDTH
			axi_araddr[ADDRLSB-1:0] <= 0;
		end
		axi_arlen  <= r_max_burst[7:0] - 8'd1;

		if (!OPT_UNALIGNED)
			axi_araddr[ADDRLSB-1:0] <= 0;
	end
	// }}}

	// ARVALID
	// {{{
	initial	axi_arvalid = 0;
	always @(posedge i_clk)
	if (i_reset)
		axi_arvalid <= 0;
	else if (!M_AXI_ARVALID || M_AXI_ARREADY)
		axi_arvalid <= start_burst;
	// }}}

	always @(posedge i_clk)
	if (!r_busy)
		axi_arburst <= (w_increment) ? 2'b01 : 2'b00;

	// Set the constant M_AXI_* signals
	// {{{
	assign	M_AXI_ARVALID= axi_arvalid;
	assign	M_AXI_ARID   = AXI_ID;
	assign	M_AXI_ARADDR = axi_araddr;
	assign	M_AXI_ARLEN  = axi_arlen;
	// Verilator lint_off WIDTH
	assign	M_AXI_ARSIZE = $clog2(C_AXI_DATA_WIDTH)-3;
	// Verilator lint_on  WIDTH
	assign	M_AXI_ARBURST= axi_arburst;
	assign	M_AXI_ARLOCK = 0;
	assign	M_AXI_ARCACHE= 4'b0011;
	assign	M_AXI_ARPROT = 0;
	assign	M_AXI_ARQOS  = 0;

	assign	M_AXI_RREADY = 1;

	// Verilator lint_off UNUSED
	wire	unused;
	assign	unused = &{ 1'b0, S_AXIL_AWPROT, S_AXIL_ARPROT, M_AXI_RID,
			M_AXI_RRESP[0], fifo_full, wskd_strb[2:0], fifo_fill,
			ar_none_outstanding, S_AXIL_AWADDR[AXILLSB-1:0],
			S_AXIL_ARADDR[AXILLSB-1:0],
			new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH],
			new_widelen[2*C_AXIL_DATA_WIDTH-1:LGLEN],
			new_widelen[AXILLSB-1:0]
			 };
	// Verilator lint_on  UNUSED
	// }}}
`ifdef	FORMAL
	//
	// The formal properties for this unit are maintained elsewhere.
	// This core does, however, pass a full prove (w/ induction) for all
	// bus properties.
	//
	// ...
	//

	////////////////////////////////////////////////////////////////////////
	//
	// Properties of the AXI-stream data interface
	// {{{
	//
	////////////////////////////////////////////////////////////////////////
	//
	//

	// (These are captured by the FIFO within)

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// The AXI-lite control interface
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{
	faxil_slave #(
		// {{{
		.C_AXI_DATA_WIDTH(C_AXIL_DATA_WIDTH),
		.C_AXI_ADDR_WIDTH(C_AXIL_ADDR_WIDTH),
		//
		// ...
		// }}}
	) faxil(
		// {{{
		.i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
		//
		.i_axi_awvalid(S_AXIL_AWVALID),
		.i_axi_awready(S_AXIL_AWREADY),
		.i_axi_awaddr( S_AXIL_AWADDR),
		.i_axi_awcache(4'h0),
		.i_axi_awprot( S_AXIL_AWPROT),
		//
		.i_axi_wvalid(S_AXIL_WVALID),
		.i_axi_wready(S_AXIL_WREADY),
		.i_axi_wdata( S_AXIL_WDATA),
		.i_axi_wstrb( S_AXIL_WSTRB),
		//
		.i_axi_bvalid(S_AXIL_BVALID),
		.i_axi_bready(S_AXIL_BREADY),
		.i_axi_bresp( S_AXIL_BRESP),
		//
		.i_axi_arvalid(S_AXIL_ARVALID),
		.i_axi_arready(S_AXIL_ARREADY),
		.i_axi_araddr( S_AXIL_ARADDR),
		.i_axi_arcache(4'h0),
		.i_axi_arprot( S_AXIL_ARPROT),
		//
		.i_axi_rvalid(S_AXIL_RVALID),
		.i_axi_rready(S_AXIL_RREADY),
		.i_axi_rdata( S_AXIL_RDATA),
		.i_axi_rresp( S_AXIL_RRESP));
		//
		// ...
		// }}}
		);

	//
	// ...
	//

	always @(posedge i_clk)
	if (f_past_valid && $past(S_AXI_ARESETN))
	begin
		if ($past(r_busy)||$past(w_cmd_start))
		begin
			assert($stable(cmd_length_b));
			assert($stable(cmd_length_w));
			assert($stable(cmd_length_aligned_w));
		end
		if ($past(r_busy))
		begin
			assert($stable(r_increment));
			assert($stable(r_continuous));
		end
		if ($past(r_busy) && $past(r_busy,2))
			assert($stable(fv_start_addr));
	end

	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// The AXI master memory interface
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{

	//
	// ...
	//

	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_EXCLUSIVE(1'b0),
		.OPT_NARROW_BURST(1'b0),
		//
		// ...
		// }}}
	) faxi(
		// {{{
		.i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
		//
		.i_axi_awvalid(1'b0),
		.i_axi_awready(1'b0),
		.i_axi_awid(   AXI_ID),
		.i_axi_awaddr( 0),
		.i_axi_awlen(  0),
		.i_axi_awsize( 0),
		.i_axi_awburst(0),
		.i_axi_awlock( 0),
		.i_axi_awcache(0),
		.i_axi_awprot( 0),
		.i_axi_awqos(  0),
		//
		.i_axi_wvalid(0),
		.i_axi_wready(0),
		.i_axi_wdata( 0),
		.i_axi_wstrb( 0),
		.i_axi_wlast( 0),
		//
		.i_axi_bvalid(1'b0),
		.i_axi_bready(1'b0),
		.i_axi_bid(   AXI_ID),
		.i_axi_bresp( 2'b00),
		//
		.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_rdata( M_AXI_RDATA),
		.i_axi_rlast( M_AXI_RLAST),
		.i_axi_rresp( M_AXI_RRESP));
		//
		// ...
		//
		// }}}
	);


	//
	// ...
	//

	always @(*)
	if (r_busy)
		assert(axi_arburst == (r_increment ? 2'b01 : 2'b00));

	//
	// ...
	//

	always @(*)
	if (r_busy)
	begin
		//
		// ...
		//
	end else begin
		//
		// ...
		//

		assert(rd_uncommitted
			+ ((OPT_UNALIGNED && write_to_fifo) ? 1:0)
			+ fifo_fill == (1<<LGFIFO));
		if (!r_continuous)
			assert(fifo_fill == 0 || reset_fifo);
	end

	//
	// ...
	//

	always @(*)
	if (r_busy)
	begin
		if (!OPT_UNALIGNED)
			assert(M_AXI_ARADDR[ADDRLSB-1:0] == 0);
		else
			assert((M_AXI_ARADDR[ADDRLSB-1:0] == 0)
				||(M_AXI_ARADDR == fv_start_addr));
	end

	always @(*)
	if (!OPT_UNALIGNED || (r_busy && !r_increment))
	begin
		assert(cmd_addr[ADDRLSB-1:0] == 0);
		assert(fv_start_addr[ADDRLSB-1:0] == 0);
		assert(axi_araddr[ADDRLSB-1:0] == 0);
		assert(axi_raddr[ADDRLSB-1:0] == 0);
	end

	//
	// f_last_addr is the (aligned) address one following the last valid
	// address read.  Once all reading is done, all (aligned) address
	// pointers should point there.
	always @(*)
	begin
		f_last_addr = { fv_start_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB],
				{(ADDRLSB){1'b0}} };

		if (r_increment)
			f_last_addr = f_last_addr + cmd_length_b;
		if (unaligned_cmd_addr)	// Only true if r_increment as well
			f_last_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB]
				= f_last_addr[C_AXI_ADDR_WIDTH-1:ADDRLSB]+1;

		f_last_addr[ADDRLSB-1:0] = 0;

		f_next_start = fv_start_addr;
		if (r_increment)
			f_next_start = f_next_start + cmd_length_b;
		if (!OPT_UNALIGNED)
			assert(f_next_start == f_last_addr);
	end


	//
	// ...
	//


	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Other formal properties
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{

	//
	// Define some helper metrics
	//
	initial	fv_start_addr = 0;
	always @(posedge i_clk)
	if (!r_busy)
		fv_start_addr <= cmd_addr;

	always @(*)
	begin
		// Metrics defining M_AXI_ARADDR
		f_araddr_is_aligned = (M_AXI_ARADDR[ADDRLSB+LGMAXBURST-1:0]==0);
		f_araddr_is_initial = (M_AXI_ARADDR == fv_start_addr);
		f_araddr_is_final   = (M_AXI_ARADDR == f_last_addr);

		//
		// Metrics to check ARADDR, assuming it had been accepted
		//

		//
		// ...
		//
	end

	//
	// fv_ar_requests_remaining ... shadows ar_requests_remaining
	//
	// Since ar_requests_remaining drops to zero suddenly on any
	// axi_abort_pending, we need another counter that we can use
	// which doesn't have this feature, but which can also be used
	// to check assertions and intermediate logic against until the
	// abort takes effect.
	initial	fv_ar_requests_remaining = 0;
	always @(posedge i_clk)
	if (!r_busy)
	begin
		fv_ar_requests_remaining <= cmd_length_aligned_w;
	end else if (phantom_start)
	begin
		// Verilator lint_off WIDTH
		fv_ar_requests_remaining
			<= fv_ar_requests_remaining - (M_AXI_ARLEN + 1);
		// Verilator lint_on WIDTH
	end

	always @(*)
	if (r_busy)
	begin
		if (!axi_abort_pending)
			assert(fv_ar_requests_remaining == ar_requests_remaining);
		else
			assert((ar_requests_remaining == 0)
				||(fv_ar_requests_remaining
					== ar_requests_remaining));
	end

	always @(*)
	if(r_busy)
	begin
		assert(fv_ar_requests_remaining <= cmd_length_aligned_w);
		//
		// ...
		//
	end

	//
	// fv_axi_raddr ... shadows axi_raddr
	//
	// The low order bits will match the low order bits of the initial
	// cmd_addr
	//
	initial	fv_axi_raddr = 0;
	always @(posedge i_clk)
	if (!r_busy)
		fv_axi_raddr <= cmd_addr;
	else if (!r_increment)
		fv_axi_raddr <= fv_start_addr;
	else begin
		if (M_AXI_RVALID && M_AXI_RREADY
				&& (!unaligned_cmd_addr || realign_last_valid))
			fv_axi_raddr <= fv_axi_raddr + (1<<ADDRLSB);
		if (!OPT_UNALIGNED)
			fv_axi_raddr[ADDRLSB-1:0] <= 0;
	end

	// Constrain start <= axi_raddr <= fv_axi_raddr <= f_last_addr
	//	in spite of any address wrapping
	always @(*)
	if (r_busy)
	begin
		assert(axi_raddr[ADDRLSB-1:0] == cmd_addr[ADDRLSB-1:0]);
		assert(axi_abort_pending || fv_axi_raddr == axi_raddr);
		if (!r_increment)
		begin
			assert(fv_axi_raddr == fv_start_addr);
			assert(axi_raddr == fv_start_addr);
		end if (!axi_abort_pending)
		begin
			if (fv_start_addr <= f_last_addr)
			begin
				// Natural order: start < f_raddr < last
				assert(fv_axi_raddr <= f_last_addr);
				assert(fv_axi_raddr >= fv_start_addr);
			end else begin
				// Reverse order
				//	Either: last < start <= f_raddr
				//	    or: f_raddr < last < start
				assert((fv_axi_raddr >= fv_start_addr)
					||(fv_axi_raddr <= f_last_addr));
			end

			if (fv_start_addr <= fv_axi_raddr)
			begin
				// Natural order: start < rad < f_rad < last
				//   or even: last < start < rad < f_rad
				assert(axi_raddr <= fv_axi_raddr);
				assert(fv_start_addr <= axi_raddr);
			end else if (fv_axi_raddr <= f_last_addr)
			begin
				// Reverse order: f_raddr < last < start
				//   so either: last < start < raddr
				//          or: raddr < f_raddr < last < start
				//
				assert((axi_raddr >= fv_start_addr)
					|| (axi_raddr <= fv_axi_raddr));
			end
		end
	end

	always @(*)
	if (!r_busy)
	begin
		assert(!M_AXI_ARVALID);
		assert(!M_AXI_RVALID);
		//
		// ...
		//
	end

	always @(*)
		assert(zero_length == (cmd_length_w == 0));

	always @(*)
	if (phantom_start)
		assert(rd_uncommitted >= (M_AXI_ARLEN + 1));

	always @(*)
	if (zero_length)
		assert(!r_busy);
	always @(*)
	if (r_busy)
		assert(ar_none_remaining   == (ar_requests_remaining == 0));
	always @(*)
		assert(ar_none_outstanding == (ar_bursts_outstanding == 0));
	always @(*)
		assert(rd_none_remaining   == (rd_reads_remaining == 0));
	always @(*)
		assert(rd_last_remaining   == (rd_reads_remaining == 1));

	always @(*)
	if (r_complete)
		assert(!r_busy);

	//
	// ...
	//

	//
	// fifo_availability is a measure of (1<<LGFIFO) minus the current
	// fifo fill.  This does not include what's in the pre-FIFO
	// logic when OPT_UNALIGNED is true.
	always @(*)
		f_fifo_availability = rd_uncommitted;

	always @(*)
		assert(f_fifo_committed <= (1<<LGFIFO));

	always @(*)
		assert(f_fifo_availability <= (1<<LGFIFO));

	//
	// ...
	//

	always @(*)
	if (!reset_fifo)
		assert(f_fifo_committed + f_fifo_availability + fifo_fill
			== (1<<LGFIFO));

	//
	// ...
	//

	always @(*)
	if (r_busy)
		assert(r_max_burst <= (1<<LGMAXBURST));

	always @(*)
	if (r_busy)
		assert((r_max_burst > 0) || (ar_requests_remaining == 0));


	always @(*)
	if (phantom_start)
		assert(M_AXI_ARVALID);

	always @(posedge i_clk)
	if (phantom_start)
	begin
		assert(r_max_burst > 0);
		assert(M_AXI_ARLEN == $past(r_max_burst)-1);
	end

	always @(*)
	if (r_busy)
		assert(initial_burstlen > 0);


	//
	// Address checking
	//

	// Check cmd_addr
	always @(*)
	if (r_busy)
	begin
		if (r_increment && r_continuous)
			assert(cmd_addr == axi_raddr);
		else
			assert(cmd_addr == fv_start_addr);
	end

	// Check M_AXI_ARADDR
	//
	// ...
	//

	//
	// Check M_AXI_ARLEN
	//
	// ...
	//

	//
	// Constrain the r_maxburst
	//
	// ...
	//

	always @(*)
	if (r_busy)
	begin
		assert(r_max_burst <= (1<<LGMAXBURST));
		//
		// ...
		//
	end

	//
	// Constrain the length
	//
	// ...
	//

	always @(posedge i_clk)
	if (phantom_start)
	begin
		assert(axi_arlen == $past(r_max_burst[7:0]) - 8'd1);
		if (!r_increment)
			assert(M_AXI_ARADDR == fv_start_addr);
	end

	// Constrain rd_reads_remaining
	//
	// ...
	//
	always @(*)
	if (r_busy)
	begin
		assert(rd_reads_remaining <= cmd_length_w);
		//
		// ...
		//
		assert(ar_bursts_outstanding <= rd_reads_remaining);
		//
		// ...
		//
	end

	//
	// Constrain the number of requests remaining
	//
	// ...
	//

	//
	// Make sure our aw_bursts_outstanding counter never overflows
	// (Given that the counter is as long as the length register, it cannot)
	//
	always @(*)
	begin
		if (&ar_bursts_outstanding[LGLENWA-1:1])
			assert(!M_AXI_ARVALID);
		//
		// ...
		//
	end

	// }}}

	//
	// Match axi_raddr to the faxi_ values
	//
	// ...
	//

	////////////////////////////////////////////////////////////////////////
	//
	// Contract checks
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{

	// 1. All data values must get read and placed into the FIFO, with
	//	none skipped
	//	Captured in logic above(?)
	//
	// 2. No addresses skipped.  Check the write address against the 
	//	write address we are expecting
	//
	// ...
	//

	// 3. If we aren't incrementing addresses, then our current address
	//	should always be the axi address
	//
	// ...

	//
	// 4. Whenever we go from busy to idle, we should raise o_int for one
	// (and only one) cycle
	always @(posedge i_clk)
	if (!f_past_valid || $past(!S_AXI_ARESETN))
		assert(!o_int);
	else
		assert(o_int == $fell(r_busy));

	//
	// ...
	//


	// 5. Pick an incoming data value.  Choose whether or not to restrict
	// incoming data not to be that value.  If the incoming data is so restricted
	// then assert that the stream output will contain that value.
	(* anyconst *)	reg	f_restrict_data;
	(* anyconst *)	reg	[C_AXI_DATA_WIDTH-1:0]	f_restricted;

	always @(*)
	if (f_restrict_data && M_AXI_RVALID
			&& (!OPT_UNALIGNED || !unaligned_cmd_addr))
		assume(M_AXI_RDATA != f_restricted);

	always @(*)
	if (f_restrict_data && M_AXIS_TVALID
			&& (!OPT_UNALIGNED || !unaligned_cmd_addr))
		assert(M_AXIS_TDATA != f_restricted);

	//
	// ...
	//
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Cover checks
	//
	////////////////////////////////////////////////////////////////////////
	//
	// {{{
	reg		cvr_aborted, cvr_buserr;
	reg	[2:0]	cvr_continued;

	initial	{ cvr_aborted, cvr_buserr } = 0;
	always @(posedge i_clk)
	if (i_reset || !r_busy)
		{ cvr_aborted, cvr_buserr } <= 0;
	else if (r_busy && !axi_abort_pending)
	begin
		if (cmd_abort && ar_requests_remaining > 0)
			cvr_aborted <= 1;
		if (M_AXI_RVALID && M_AXI_RRESP[1] && M_AXI_RLAST)
			cvr_buserr <= 1;
	end

	initial	cvr_continued = 0;
	always @(posedge i_clk)
	if (i_reset || r_err || cmd_abort)
		cvr_continued <= 0;
	else begin
		// Cover a continued transaction across two separate bursts
		if (r_busy && r_continuous)
			cvr_continued[0] <= 1;
		if (!r_busy && cvr_continued[0])
			cvr_continued[1] <= 1;
		if (r_busy && cvr_continued[1])
			cvr_continued[2] <= 1;
	end

	always @(posedge i_clk)
	if (f_past_valid && !$past(i_reset) && !i_reset && $fell(r_busy))
	begin
		cover( r_err && cvr_aborted);
		cover( r_err && cvr_buserr);
		cover(!r_err);
		if (!r_err && !axi_abort_pending && !cvr_aborted && !cvr_buserr)
		begin
			cover(cmd_length_w > 5);
			cover(cmd_length_w > 8);
			//
			// ...
			//
			cover(&cvr_continued);
			cover(&cvr_continued && (cmd_length_w > 2));
			cover(&cvr_continued && (cmd_length_w > 5));
		end
	end

	always @(*)
	if (!i_reset)
		cover(!r_err && fifo_fill > 8 && !r_busy);

	always @(*)
		cover(r_busy);

	always @(*)
		cover(start_burst);

	always @(*)
		cover(M_AXI_ARVALID && M_AXI_ARREADY);

	always @(*)
		cover(M_AXI_RVALID);

	always @(*)
		cover(M_AXI_RVALID & M_AXI_RLAST);
	always @(*)
	if (r_busy)
	begin
		cover(!ar_none_remaining);
		if(!ar_none_remaining)
		begin
			cover(1);
			cover(rd_uncommitted>= {{(LGFIFO-LGMAXBURST){1'b0}}, r_max_burst});
			if(rd_uncommitted>= {{(LGFIFO-LGMAXBURST){1'b0}}, r_max_burst})
			begin
				cover(!phantom_start);
				cover(phantom_start);
			end
		end
	end

	//
	// Unaligned cover properties
	generate if (OPT_TLAST)
	begin
		reg	[3:0]	cvr_lastcount;
		always @(posedge i_clk)
		if (i_reset || (r_busy && cmd_length_w <= 2))
			cvr_lastcount <= 0;
		else if (M_AXIS_TVALID && M_AXIS_TREADY && M_AXIS_TLAST
				&& !cvr_lastcount[3])
			cvr_lastcount <= cvr_lastcount + 1;

		always @(*)
			cover(M_AXIS_TVALID && M_AXIS_TREADY && M_AXIS_TLAST);

		always @(posedge i_clk)
			cover(o_int && cvr_lastcount > 2);

	end endgenerate

	generate if (OPT_UNALIGNED)
	begin
		//
		// ...
		//
		always @(posedge i_clk)
		if (f_past_valid && !$past(i_reset) && !i_reset &&$fell(r_busy))
		begin
			cover(r_err);
			cover(!r_err);
			cover(axi_abort_pending);
			cover(!axi_abort_pending);
			cover(cvr_aborted);
			cover(!cvr_aborted);
			cover(cvr_buserr);
			cover(!cvr_buserr);
			cover(!cvr_buserr && !axi_abort_pending);
			cover(!cvr_buserr && !axi_abort_pending
				&& (cmd_length_w > 2));
			cover(!r_err && !cvr_aborted && !cvr_buserr
				&& !axi_abort_pending
				&& (cmd_length_w > 2));
		end
	end endgenerate


	// }}}
	// }}}
`endif
endmodule
`ifndef	YOSYS
`default_nettype wire
`endif