rtl/wb2axip: add to version control

1 files changed, 2157 insertions, 0 deletions

diff --git a/rtl/wb2axip/axi2axilsub.v b/rtl/wb2axip/axi2axilsub.v
new file mode 100644
index 0000000..694dc58
--- /dev/null
+++ b/rtl/wb2axip/axi2axilsub.v
@@ -0,0 +1,2157 @@
+///////////////////////////////////////////////////////////////////////////////
+//
+// Filename: 	axi2axilsub.v
+// {{{
+// Project:	WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose:	Convert from AXI to AXI-lite with no performance loss, and to
+//		a potentially smaller bus width.
+//
+// Performance:	The goal of this converter is to convert from AXI to an AXI-lite
+//		bus of a smaller width, while still maintaining the one-clock
+//	per transaction speed of AXI.  It currently achieves this goal.  The
+//	design needs very little configuration to be useful, but you might
+//	wish to resize the FIFOs within depending upon the length of your
+//	slave's data path.  The current FIFO length, LGFIFO=4, is sufficient to
+//	maintain full speed.  If the slave, however, can maintain full speed but
+//	requires a longer processing cycle, then you may need longer FIFOs.
+//
+//	The AXI specification does require an additional 2 clocks per
+//	transaction when using this core, so your latency will go up.
+//
+// Creator:	Dan Gisselquist, Ph.D.
+//		Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2019-2024, Gisselquist Technology, LLC
+// {{{
+// This digital logic component is the proprietary property of Gisselquist
+// Technology, LLC.  It may only be distributed and/or re-distributed by the
+// express permission of Gisselquist Technology.
+//
+// Permission has been granted to the Patreon sponsors of the ZipCPU blog
+// to use this logic component as they see fit, but not to redistribute it
+// beyond their individual personal or commercial use.
+//
+// This component is distributed in the hope that it will be useful, but
+// WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.
+//
+// Please feel free to contact me should you have any questions, or even if you
+// just want to ask about what you find within here.
+//
+// Yours,
+//
+// Dan Gisselquist
+// Owner
+// Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+`default_nettype	none
+//
+`ifdef	FORMAL
+`ifdef	BMC
+`define	BMC_ASSERT	assert
+`else
+`define	BMC_ASSERT	assume
+`endif
+`endif
+//
+// }}}
+module axi2axilsub #(
+		// {{{
+		parameter integer C_AXI_ID_WIDTH	= 2,
+		parameter integer C_S_AXI_DATA_WIDTH	= 64,
+		parameter integer C_M_AXI_DATA_WIDTH	= 32,
+		parameter integer C_AXI_ADDR_WIDTH	= 6,
+		parameter	 [0:0]	OPT_LOWPOWER	= 1,
+		parameter	 [0:0]	OPT_WRITES	= 1,
+		parameter	 [0:0]	OPT_READS	= 1,
+		parameter		SLVSZ = $clog2(C_S_AXI_DATA_WIDTH/8),
+		parameter		MSTSZ = $clog2(C_M_AXI_DATA_WIDTH/8),
+		// Log (based two) of the maximum number of outstanding AXI
+		// (not AXI-lite) transactions.  If you multiply 2^LGFIFO * 256,
+		// you'll get the maximum number of outstanding AXI-lite
+		// transactions
+		parameter	LGFIFO			= 4
+		// }}}
+	) (
+		// {{{
+		input	wire	S_AXI_ACLK,
+		input	wire	S_AXI_ARESETN,
+		// AXI4 slave interface
+		// {{{
+		// Write address channel
+		// {{{
+		input	wire				S_AXI_AWVALID,
+		output	wire				S_AXI_AWREADY,
+		input	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_AWID,
+		input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_AWADDR,
+		input	wire	[7:0]			S_AXI_AWLEN,
+		input	wire	[2:0]			S_AXI_AWSIZE,
+		input	wire	[1:0]			S_AXI_AWBURST,
+		input	wire				S_AXI_AWLOCK,
+		input	wire	[3:0]			S_AXI_AWCACHE,
+		input	wire	[2:0]			S_AXI_AWPROT,
+		input	wire	[3:0]			S_AXI_AWQOS,
+		// }}}
+		// Write data channel
+		// {{{
+		input	wire				S_AXI_WVALID,
+		output	wire				S_AXI_WREADY,
+		input	wire [C_S_AXI_DATA_WIDTH-1:0]	S_AXI_WDATA,
+		input	wire [(C_S_AXI_DATA_WIDTH/8)-1:0] S_AXI_WSTRB,
+		input	wire				S_AXI_WLAST,
+		// }}}
+		// Write return channel
+		// {{{
+		output	wire				S_AXI_BVALID,
+		input	wire				S_AXI_BREADY,
+		output	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_BID,
+		output	wire	[1:0]			S_AXI_BRESP,
+		// }}}
+		// Read address channel
+		// {{{
+		input	wire				S_AXI_ARVALID,
+		output	wire				S_AXI_ARREADY,
+		input	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_ARID,
+		input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_ARADDR,
+		input	wire	[7:0]			S_AXI_ARLEN,
+		input	wire	[2:0]			S_AXI_ARSIZE,
+		input	wire	[1:0]			S_AXI_ARBURST,
+		input	wire				S_AXI_ARLOCK,
+		input	wire	[3:0]			S_AXI_ARCACHE,
+		input	wire	[2:0]			S_AXI_ARPROT,
+		input	wire	[3:0]			S_AXI_ARQOS,
+		// }}}
+		// Read data channel
+		// {{{
+		output	wire				S_AXI_RVALID,
+		input	wire				S_AXI_RREADY,
+		output	wire [C_AXI_ID_WIDTH-1:0]	S_AXI_RID,
+		output	wire [C_S_AXI_DATA_WIDTH-1:0]	S_AXI_RDATA,
+		output	wire	[1:0]			S_AXI_RRESP,
+		output	wire				S_AXI_RLAST,
+		// }}}
+		// }}}
+		// AXI-lite master interface
+		// {{{
+		// AXI-lite Write interface
+		// {{{
+		output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_AWADDR,
+		output	wire	[2 : 0]			M_AXI_AWPROT,
+		output	wire				M_AXI_AWVALID,
+		input	wire				M_AXI_AWREADY,
+		output	wire [C_M_AXI_DATA_WIDTH-1:0]	M_AXI_WDATA,
+		output	wire [(C_M_AXI_DATA_WIDTH/8)-1:0] M_AXI_WSTRB,
+		output	wire				M_AXI_WVALID,
+		input	wire				M_AXI_WREADY,
+		input	wire	[1 : 0]			M_AXI_BRESP,
+		input	wire				M_AXI_BVALID,
+		output	wire				M_AXI_BREADY,
+		// }}}
+		// AXI-lite read interface
+		// {{{
+		output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_ARADDR,
+		output	wire	[2:0]			M_AXI_ARPROT,
+		output	wire				M_AXI_ARVALID,
+		input	wire				M_AXI_ARREADY,
+		//
+		input	wire				M_AXI_RVALID,
+		output	wire				M_AXI_RREADY,
+		input	wire	[C_M_AXI_DATA_WIDTH-1 : 0] M_AXI_RDATA,
+		input	wire	[1 : 0]			M_AXI_RRESP
+		// }}}
+		// }}}
+		// }}}
+	);
+
+	// Local parameters, register, and net declarations
+	// {{{
+	// Verilator lint_off UNUSED
+	localparam [1:0]	OKAY   = 2'b00,
+				EXOKAY = 2'b01,
+				SLVERR = 2'b10;
+	// localparam [1:0]	DECERR = 2'b10;
+
+	// Verilator lint_on UNUSED
+	localparam	AW = C_AXI_ADDR_WIDTH;
+	localparam	SLVDW = C_S_AXI_DATA_WIDTH;
+	localparam	MSTDW = C_M_AXI_DATA_WIDTH;
+	localparam	IW = C_AXI_ID_WIDTH;
+	// localparam	LSB = $clog2(C_AXI_DATA_WIDTH)-3;
+	// }}}
+	// Register declarations
+	// {{{
+	//
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Write logic
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	generate if (OPT_WRITES && SLVDW == MSTDW)
+	begin : IMPLEMENT_AXI2AXILITE_WRITES
+		// {{{
+
+		// (Unused) signal declarations
+		// {{{
+		// Verilator lint_off UNUSED
+		wire				ign_arready, ign_rvalid,
+						ign_rlast,
+						ign_arvalid, ign_rready;
+		wire	[IW-1:0]		ign_rid;
+		wire [SLVDW-1:0]	ign_rdata;
+		wire	[1:0]			ign_rresp;
+		wire	[AW-1:0]	ign_araddr;
+		wire	[2:0]			ign_arprot;
+		// Verilator lint_on  UNUSED
+		// }}}
+
+		axi2axilite #(
+			// {{{
+			.C_AXI_ID_WIDTH(IW),
+			.C_AXI_DATA_WIDTH(SLVDW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.OPT_WRITES(1),
+			.OPT_READS(0),
+			.LGFIFO(LGFIFO)
+			// }}}
+		) axilwrite (
+			// {{{
+			.S_AXI_ACLK(S_AXI_ACLK),
+			.S_AXI_ARESETN(S_AXI_ARESETN),
+			// AXI4 slave interface
+			// {{{
+			// Write address channel
+			// {{{
+			.S_AXI_AWVALID(S_AXI_AWVALID),
+			.S_AXI_AWREADY(S_AXI_AWREADY),
+			.S_AXI_AWID(   S_AXI_AWID),
+			.S_AXI_AWADDR( S_AXI_AWADDR),
+			.S_AXI_AWLEN(  S_AXI_AWLEN),
+			.S_AXI_AWSIZE( S_AXI_AWSIZE),
+			.S_AXI_AWBURST(S_AXI_AWBURST),
+			.S_AXI_AWLOCK( S_AXI_AWLOCK),
+			.S_AXI_AWCACHE(S_AXI_AWCACHE),
+			.S_AXI_AWPROT( S_AXI_AWPROT),
+			.S_AXI_AWQOS(  S_AXI_AWQOS),
+			// }}}
+			// Write data channel
+			// {{{
+			.S_AXI_WVALID(S_AXI_WVALID),
+			.S_AXI_WREADY(S_AXI_WREADY),
+			.S_AXI_WDATA( S_AXI_WDATA),
+			.S_AXI_WSTRB( S_AXI_WSTRB),
+			.S_AXI_WLAST( S_AXI_WLAST),
+			// }}}
+			// Write return channel
+			// {{{
+			.S_AXI_BVALID(S_AXI_BVALID),
+			.S_AXI_BREADY(S_AXI_BREADY),
+			.S_AXI_BID(   S_AXI_BID),
+			.S_AXI_BRESP( S_AXI_BRESP),
+			// }}}
+			// Read address channel
+			// {{{
+			.S_AXI_ARVALID(1'b0),
+			.S_AXI_ARREADY(ign_arready),
+			.S_AXI_ARID(   {(IW){1'b0}}),
+			.S_AXI_ARADDR( {(AW){1'b0}}),
+			.S_AXI_ARLEN(  8'h0),
+			.S_AXI_ARSIZE( 3'h0),
+			.S_AXI_ARBURST(2'h0),
+			.S_AXI_ARLOCK( 1'b0),
+			.S_AXI_ARCACHE(4'h0),
+			.S_AXI_ARPROT( 3'h0),
+			.S_AXI_ARQOS(  4'h0),
+			// }}}
+			// Read data channel
+			// {{{
+			.S_AXI_RVALID(ign_rvalid),
+			.S_AXI_RREADY(1'b1),
+			.S_AXI_RID(   ign_rid),
+			.S_AXI_RDATA( ign_rdata),
+			.S_AXI_RRESP( ign_rresp),
+			.S_AXI_RLAST( ign_rlast),
+			// }}}
+			// }}}
+			// AXI-lite master interface
+			// {{{
+			// AXI-lite Write interface
+			// {{{
+			.M_AXI_AWVALID(M_AXI_AWVALID),
+			.M_AXI_AWREADY(M_AXI_AWREADY),
+			.M_AXI_AWADDR(M_AXI_AWADDR),
+			.M_AXI_AWPROT(M_AXI_AWPROT),
+			//
+			.M_AXI_WVALID(M_AXI_WVALID),
+			.M_AXI_WREADY(M_AXI_WREADY),
+			.M_AXI_WDATA(M_AXI_WDATA),
+			.M_AXI_WSTRB(M_AXI_WSTRB),
+			//
+			.M_AXI_BVALID(M_AXI_BVALID),
+			.M_AXI_BREADY(M_AXI_BREADY),
+			.M_AXI_BRESP(M_AXI_BRESP),
+			// }}}
+			// AXI-lite read interface
+			// {{{
+			.M_AXI_ARVALID(ign_arvalid),
+			.M_AXI_ARREADY(1'b1),
+			.M_AXI_ARADDR(ign_araddr),
+			.M_AXI_ARPROT(ign_arprot),
+			//
+			.M_AXI_RVALID(1'b0),
+			.M_AXI_RREADY(ign_rready),
+			.M_AXI_RDATA({(MSTDW){1'b0}}),
+			.M_AXI_RRESP(2'b00)
+			// }}}
+			// }}}
+			// }}}
+		);
+
+		// }}}
+	end else begin : WDN
+	if (OPT_WRITES)
+	begin : IMPLEMENT_WRITES
+		// {{{
+
+		// Register declarations
+		// {{{
+		localparam	BIDFIFOBW = IW+1+(SLVSZ-MSTSZ+1);
+
+		//
+		// S_AXI_AW* skid buffer
+		wire			skids_awvalid;
+		wire			skids_awready;
+		wire	[IW-1:0]	skids_awid;
+		wire	[AW-1:0]	skids_awaddr;
+		wire	[7:0]		skids_awlen;
+		wire	[2:0]		skids_awsize;
+		wire	[1:0]		skids_awburst;
+		wire	[2:0]		skids_awprot;
+		//
+		// S_AXI_W* skid buffer
+		wire			skids_wvalid, skids_wready;
+		wire	[SLVDW-1:0]	skids_wdata;
+		wire	[SLVDW/8-1:0]	skids_wstrb;
+
+		wire			slv_awready, slv_wready;
+		reg	[SLVDW-1:0]	slv_wdata;
+		reg	[SLVDW/8-1:0]	slv_wstrb;
+
+		reg	[IW-1:0]			slv_awid;
+		reg	[AW-1:0]			slv_awaddr;
+		wire	[AW-1:0]			slv_next_awaddr;
+		reg	[2:0]				slv_awsize;
+		reg	[1:0]				slv_awburst;
+		reg	[7:0]				slv_awlen;
+		reg	[8:0]				slv_wlen;
+		reg					slv_awlast;
+
+		// Write registers
+		reg				m_awvalid;
+		reg				bfifo_write;
+		wire				wfifo_wlast;
+		reg	[IW+1+SLVSZ-MSTSZ:0]	bfifo_wdata;
+		wire	[LGFIFO:0]		wfifo_count;
+		wire				wfifo_full;
+		wire				wfifo_empty;
+		wire	[SLVSZ-MSTSZ:0]		wfifo_subcount;
+		wire	[IW-1:0]		wfifo_bid;
+		reg	[SLVSZ-MSTSZ:0]		bcounts;
+		reg	[IW-1:0]	s_axi_bid, bid;
+		reg				blast;
+		reg	[1:0]			s_axi_bresp, bresp;
+		reg				s_axi_bvalid;
+		reg				b_return_stall;
+		wire				read_from_wrfifo;
+		//
+		// S_AXI_B* skid buffer isn't needed
+		//
+		// M_AXI_AW* skid buffer isn't needed
+		//
+		// M_AXI_W* skid buffer isn't needed
+		//
+		// M_AXI_B* skid buffer
+		wire			skidm_bvalid, skidm_bready;
+		wire	[1:0]		skidm_bresp;
+
+		reg				m_wvalid;
+		reg	[AW-1:0]		mst_awaddr;
+		reg	[2:0]			mst_awprot;
+		reg	[SLVSZ-MSTSZ:0]		mst_awbeats,
+						mst_wbeats, next_slv_beats;
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// Incoming write address / data handling
+		// {{{
+		////////////////////////////////////////////////////////////////
+		//
+		//
+
+		////////////////////////////////////////
+		//
+		// Clock #1: The skid buffer
+		// {{{
+
+		// The write address channel's skid buffer
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(IW+AW+8+3+2+3),
+			.OPT_LOWPOWER(OPT_LOWPOWER),
+			.OPT_OUTREG(0)
+			// }}}
+		) awskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(S_AXI_AWVALID), .o_ready(S_AXI_AWREADY),
+			.i_data({ S_AXI_AWID, S_AXI_AWADDR, S_AXI_AWLEN,
+				S_AXI_AWSIZE, S_AXI_AWBURST, S_AXI_AWPROT }),
+			.o_valid(skids_awvalid), .i_ready(skids_awready),
+			.o_data({ skids_awid, skids_awaddr, skids_awlen,
+				skids_awsize, skids_awburst, skids_awprot })
+			// }}}
+		);
+		// }}}
+		//
+		// The write data channel's skid buffer (S_AXI_W*)
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(SLVDW+SLVDW/8),
+			.OPT_LOWPOWER(OPT_LOWPOWER),
+			.OPT_OUTREG(0)
+			// }}}
+		) wskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(S_AXI_WVALID), .o_ready(S_AXI_WREADY),
+			.i_data({ S_AXI_WDATA, S_AXI_WSTRB }),
+			.o_valid(skids_wvalid), .i_ready(skids_wready),
+			.o_data({ skids_wdata, skids_wstrb })
+			// }}}
+		);
+		// }}}
+
+		assign	skids_awready = skids_wvalid && skids_wready
+					&& slv_awlast;
+
+		assign	skids_wready = slv_wready;
+		// }}}
+		////////////////////////////////////////
+		//
+		// Clock 2: slv_* clock
+		// {{{
+
+		// When are we ready for a next SLAVE beat?
+		assign	slv_awready = (skids_wvalid && skids_wready);
+
+		// slv_aw*
+		// {{{
+		// slv_awaddr is the address of the value *CURRENTLY* in the
+		// buffer, *NOT* the next address.
+		initial	slv_awlast = 1;
+		always @(posedge S_AXI_ACLK)
+		if (skids_awvalid && skids_awready)
+		begin
+			slv_awid    <= skids_awid;
+			slv_awaddr  <= skids_awaddr;
+			slv_awlen   <= skids_awlen;
+			slv_awsize  <= skids_awsize;
+			slv_awburst <= skids_awburst;
+		end else if (slv_awready && slv_wlen > 0)
+		begin
+			// Step forward a full beat -- but only when we have
+			// the data to do so
+			slv_awaddr <= slv_next_awaddr;
+		end
+		// }}}
+
+		// slv_awlast
+		// {{{
+		initial	slv_awlast = 1;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			slv_awlast <= 1;
+		else if (skids_awvalid && skids_awready)
+			slv_awlast  <= (skids_awlen == 0);
+		else if (skids_wvalid && skids_wready)
+			slv_awlast <= (slv_wlen <= 2);
+
+`ifdef	FORMAL
+		always @(*)
+			assert(slv_awlast == (slv_wlen <= 1));
+`endif
+		// }}}
+
+		// slv_wlen = Number of beats remaining
+		// {{{
+		// ... in the slave's data space, to include the one we've
+		// just ingested.  Therefore, this is a 1-up counter.  If
+		// slv_wlen == 0, then we are idle.
+		initial	slv_wlen = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			slv_wlen <= 0;
+		else if (skids_awvalid && skids_awready)
+		begin
+			slv_wlen <= skids_awlen + 1;
+		end else if (skids_wvalid && skids_wready) // (slv_awready && slv_wlen > 0)
+		begin
+			slv_wlen <= slv_wlen - 1;
+`ifdef	FORMAL
+			assert(slv_wlen > 0);
+`endif
+		end else if (slv_wlen == 1 && slv_wready)
+			slv_wlen <= 0;
+		// }}}
+
+		// next_slv_beats
+		// {{{
+		always @(*)
+		begin
+			// Verilator lint_off WIDTH
+			next_slv_beats = (1<<(skids_awsize-MSTSZ[2:0]))
+				  - (skids_awaddr[SLVSZ-1:0] >> skids_awsize);
+			if (skids_awsize <= MSTSZ[2:0])
+				next_slv_beats = 1;
+			// Verilator lint_on  WIDTH
+		end
+		// }}}
+
+		// slv_next_awaddr
+		// {{{
+		axi_addr #(
+			// {{{
+			.AW(AW),
+			.DW(SLVDW)
+			// }}}
+		) get_next_slave_addr (
+			// {{{
+			.i_last_addr(slv_awaddr),
+			.i_size(slv_awsize),
+			.i_burst(slv_awburst),
+			.i_len(slv_awlen),
+			.o_next_addr(slv_next_awaddr)
+			// }}}
+		);
+		// }}}
+
+		assign	slv_wready = (mst_awbeats <= (M_AXI_AWREADY ? 1:0))
+					&& (mst_wbeats <= (M_AXI_WREADY ? 1:0))
+					&& (!bfifo_write || !wfifo_full);
+
+		// slv_wstrb, slv_wdata
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+			{ slv_wstrb, slv_wdata } <= 0;
+		else if (skids_awready)
+		begin
+			slv_wstrb <= skids_wstrb >> (skids_awaddr[SLVSZ-1:MSTSZ]*MSTDW/8);
+			slv_wdata <= skids_wdata >> (skids_awaddr[SLVSZ-1:MSTSZ]*MSTDW);
+			if (OPT_LOWPOWER && !skids_awvalid)
+			begin
+				slv_wstrb <= 0;
+				slv_wdata <= 0;
+			end
+		end else if (skids_wready)
+		begin
+			slv_wstrb <= skids_wstrb >> (slv_next_awaddr[SLVSZ-1:MSTSZ]*MSTDW/8);
+			slv_wdata <= skids_wdata >> (slv_next_awaddr[SLVSZ-1:MSTSZ]*MSTDW);
+			if (OPT_LOWPOWER && !skids_wvalid)
+			begin
+				slv_wstrb <= 0;
+				slv_wdata <= 0;
+			end
+		end else if (M_AXI_WVALID && M_AXI_WREADY)
+		begin
+			slv_wstrb <= slv_wstrb >> (MSTDW/8);
+			slv_wdata <= slv_wdata >> (MSTDW);
+		end
+		// }}}
+
+		// }}}
+		////////////////////////////////////////
+		//
+		// Clock 2 (continued): mst_* = M_AXI_*
+		// {{{
+
+		// mst_awaddr, mst_awprot, mst_awbeats
+		// {{{
+		initial	mst_awaddr = 0;
+		initial	mst_awprot = 0;
+		always @(posedge S_AXI_ACLK)
+		begin
+			if (!M_AXI_AWVALID || M_AXI_AWREADY)
+			begin
+				if (skids_awvalid && skids_awready)
+				begin
+					mst_awaddr <= skids_awaddr;
+					mst_awprot <= skids_awprot;
+					mst_awbeats<= next_slv_beats;
+				end else if (skids_wvalid && skids_wready)
+				begin
+					mst_awaddr <= slv_next_awaddr;
+					mst_awbeats<= 1;
+					if (slv_awsize >= MSTSZ[2:0])
+						mst_awbeats <= (1<<(slv_awsize - MSTSZ[2:0]));
+				end else begin
+					if (mst_awbeats > 1)
+					begin
+						mst_awaddr <= mst_awaddr + (1<<MSTSZ);
+						mst_awaddr[MSTSZ-1:0] <= 0;
+					end else if (OPT_LOWPOWER)
+					begin
+						mst_awaddr <= 0;
+					end
+
+					if (mst_awbeats > 0)
+						mst_awbeats <= mst_awbeats - 1;
+				end
+			end
+
+			if (!S_AXI_ARESETN)
+			begin
+				// {{{
+				mst_awbeats <= 0;
+				if (OPT_LOWPOWER)
+				begin
+					mst_awaddr  <= 0;
+					mst_awprot  <= 0;
+				end
+				// }}}
+			end
+		end
+`ifdef	FORMAL
+		always @(*)
+		if(S_AXI_ARESETN && OPT_LOWPOWER && mst_awbeats == 0)
+		begin
+			assert(mst_awaddr == 0);
+		end
+
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(m_axi_awvalid == (mst_awbeats > 0));
+`endif
+		// }}}
+
+		// m_awvalid
+		// {{{
+		initial	m_axi_awvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			m_awvalid <= 0;
+		else if (!M_AXI_AWVALID || M_AXI_AWREADY)
+		begin
+			if (skids_wvalid && skids_wready)
+				m_awvalid <= 1'b1;
+			else if (mst_awbeats == 1)
+				m_awvalid <= 1'b0;
+		end
+		// }}}
+
+		assign	M_AXI_AWVALID = m_awvalid;
+		assign	M_AXI_AWADDR  = mst_awaddr;
+		assign	M_AXI_AWPROT  = mst_awprot;
+
+		// M_AXI_WVALID, mst_wbeats
+		// {{{
+		initial	m_wvalid = 0;
+		initial	mst_wbeats   = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+		begin
+			m_wvalid <= 0;
+			mst_wbeats   <= 0;
+		end else if (!M_AXI_WVALID || M_AXI_WREADY)
+		begin
+			if (skids_wvalid && skids_wready)
+			begin
+				m_wvalid <= 1'b1;
+				if (skids_awvalid && skids_awready)
+					mst_wbeats   <= next_slv_beats;
+				else if (slv_awsize <= MSTSZ[2:0])
+					mst_wbeats <= 1;
+				else
+					mst_wbeats <= (1<<(slv_awsize - MSTSZ[2:0]));
+			end else begin
+				if (mst_wbeats <= 1)
+					m_wvalid <= 1'b0;
+				if (mst_wbeats > 0)
+					mst_wbeats   <= mst_wbeats - 1;
+			end
+		end
+`ifdef	FORMAL
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(M_AXI_WVALID == (mst_wbeats > 0));
+`endif
+		// }}}
+
+		// M_AXI_W*
+		// {{{
+		assign	M_AXI_WVALID = m_wvalid;
+		assign	M_AXI_WDATA  = slv_wdata[MSTDW-1:0];
+		assign	M_AXI_WSTRB  = slv_wstrb[MSTDW/8-1:0];
+		// }}}
+		// }}}
+		////////////////////////////////////////
+		//
+		// Clock 3: The B FIFO
+		// {{{
+
+		// bfifo_write
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			bfifo_write <= 0;
+		else if (!bfifo_write || !wfifo_full)
+			bfifo_write <= skids_wvalid && skids_wready;
+		// }}}
+
+		// bfifo_wdata
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			bfifo_wdata <= 0;
+		else if (skids_awvalid && skids_awready)
+		begin
+			bfifo_wdata[SLVSZ-MSTSZ:0] <= next_slv_beats;
+			bfifo_wdata[SLVSZ-MSTSZ+1] <= (skids_awlen == 0);
+			bfifo_wdata[SLVSZ-MSTSZ+2 +: IW] <= skids_awid;
+`ifdef	FORMAL
+			assert(skids_wvalid && skids_wready);
+`endif
+		end else if (skids_wvalid && skids_wready)
+		begin
+			bfifo_wdata[SLVSZ-MSTSZ+2 +: IW] <= slv_awid;
+			bfifo_wdata[SLVSZ-MSTSZ+1] <= (slv_wlen <= 2)
+						? 1'b1 : 1'b0;
+
+			if (slv_awsize <= MSTSZ[2:0])
+				bfifo_wdata[SLVSZ-MSTSZ:0] <= 1;
+			else
+				bfifo_wdata[SLVSZ-MSTSZ:0]
+					<= (1<<(slv_awsize - MSTSZ[2:0]));
+		end
+		// }}}
+
+		// BFIFO
+		// {{{
+		sfifo	#(
+			// {{{
+			.BW(BIDFIFOBW), .LGFLEN(LGFIFO)
+			// }}}
+		) bidlnfifo(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_wr(bfifo_write), .i_data(bfifo_wdata),
+				.o_full(wfifo_full), .o_fill(wfifo_count),
+			.i_rd(read_from_wrfifo),
+			.o_data({ wfifo_bid, wfifo_wlast,wfifo_subcount }),
+			.o_empty(wfifo_empty)
+			// }}}
+		);
+		// }}}
+
+		// read_from_wrfifo
+		// {{{
+		assign	read_from_wrfifo = (bcounts <= 1)&&(!wfifo_empty)
+			    &&(skidm_bvalid && skidm_bready);
+		// }}}
+		// }}}
+		////////////////////////////////////////
+		//
+		// Return clock 1: the skid buffer
+		// {{{
+
+		//
+		// The downstream AXI-lite response (M_AXI_B*) skid buffer
+		skidbuffer #(
+			// {{{
+			.DW(2),
+			.OPT_LOWPOWER(OPT_LOWPOWER),
+			.OPT_OUTREG(0)
+			// }}}
+		) bskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(M_AXI_BVALID), .o_ready(M_AXI_BREADY),
+				.i_data({ M_AXI_BRESP }),
+			.o_valid(skidm_bvalid), .i_ready(skidm_bready),
+				.o_data({ skidm_bresp })
+			// }}}
+		);
+
+		assign	skidm_bready = ((bcounts > 0)||(!wfifo_empty))
+				&& !b_return_stall;
+		// }}}
+		////////////////////////////////////////
+		//
+		// Return staging: Counting returns
+		// {{{
+
+		// bcounts
+		// {{{
+		// Return counts
+		initial	bcounts = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			bcounts <= 0;
+		else if (skidm_bvalid && skidm_bready)
+		begin
+			if (read_from_wrfifo)
+			begin
+				/*
+				if (bcounts == 0 && wfifo_subcount <= 1
+						&& wfifo_wlast)
+					// Go straight to S_AXI_BVALID, no
+					// more bursts to count here
+					bcounts <= 0;
+				else
+				*/
+					bcounts <= wfifo_subcount + bcounts - 1;
+			end else
+				bcounts <= bcounts - 1;
+		end
+		// }}}
+
+		// blast
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (read_from_wrfifo)
+			blast <= wfifo_wlast;
+		// }}}
+
+		// bid
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (read_from_wrfifo)
+			bid <= wfifo_bid;
+		// }}}
+
+		// bresp
+		// {{{
+		initial	bresp = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			bresp <= OKAY;
+		else if (!S_AXI_BVALID || S_AXI_BREADY)
+			bresp <= OKAY;
+		else if (skidm_bvalid && skidm_bready)
+		begin
+			// Let SLVERR take priority over DECERR
+			casez({ bresp, skidm_bresp })
+			4'b??0?: bresp <= bresp;
+			4'b0?1?: bresp <= skidm_bresp;
+			4'b1?10: bresp <= SLVERR;
+			4'b1011: bresp <= SLVERR;
+			4'b1111: bresp <= skidm_bresp;
+			endcase
+
+			if (blast)
+				bresp <= OKAY;
+		end
+		// }}}
+		// }}}
+		////////////////////////////////////////
+		//
+		// Return clock 2: S_AXI_* returns
+		// {{{
+
+		// s_axi_bid
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_BVALID || S_AXI_BREADY)
+		begin
+			if (bcounts > 0 && blast)
+				s_axi_bid <= bid;
+			else if (read_from_wrfifo)
+				s_axi_bid <= wfifo_bid;
+			else
+				s_axi_bid <= bid;
+		end
+		// }}}
+
+		// s_axi_bvalid, b_return_stall
+		// {{{
+		always @(*)
+		begin
+			// Force simulation evaluation on reset
+			if (!S_AXI_ARESETN)
+				b_return_stall = 0;
+
+			// Default: stalled if the output is stalled
+			b_return_stall = S_AXI_BVALID && !S_AXI_BREADY;
+
+			if (bcounts > 1)
+				b_return_stall = 0;
+			else if (bcounts == 1 && !blast)
+				b_return_stall = 0;
+			else if (bcounts == 0
+				&& (wfifo_subcount > 1 || !wfifo_wlast))
+				b_return_stall = 0;
+		end
+
+		initial	s_axi_bvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			s_axi_bvalid <= 0;
+		else if (!S_AXI_BVALID || S_AXI_BREADY)
+		begin
+			s_axi_bvalid <= 0;
+			if (skidm_bvalid && skidm_bready)
+				s_axi_bvalid <= ((bcounts == 1)&& blast)
+					||((bcounts == 0) && (!wfifo_empty)
+						&& (wfifo_subcount <= 1)&& wfifo_wlast);
+		end
+		// }}}
+
+		// s_axi_bresp
+		// {{{
+		initial	s_axi_bresp = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			s_axi_bresp <= OKAY;
+		else if (!S_AXI_BVALID || S_AXI_BREADY)
+		begin
+			if (skidm_bvalid && skidm_bready)
+			begin
+				// Let SLVERR take priority over DECERR
+				casez({ bresp, skidm_bresp[1] })
+				3'b??0: s_axi_bresp <= s_axi_bresp;
+				3'b0?1: s_axi_bresp <= skidm_bresp;
+				3'b101: s_axi_bresp <= SLVERR;
+				3'b111: s_axi_bresp <= skidm_bresp;
+				endcase
+			end else
+				s_axi_bresp <= bresp;
+		end
+		// }}}
+
+		// S_AXI_B* assignments
+		// {{{
+		assign	S_AXI_BID    = s_axi_bid;
+		assign	S_AXI_BRESP  = s_axi_bresp;
+		assign	S_AXI_BVALID = s_axi_bvalid;
+		// }}}
+		// }}}
+		// }}}
+		// Make Verilator happy
+		// {{{
+		// Verilator lint_off UNUSED
+		wire	unused_write;
+		assign	unused_write = &{ 1'b0, wfifo_count, S_AXI_WLAST };
+		// Verilator lint_on  UNUSED
+		// }}}
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+		//
+		// Formal properties, write half
+		// {{{
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+		// These are only a subset of the formal properties used to
+		// verify this design.  While I will warrant that the full
+		// property set will work, I don't really expect the below
+		// properties to be sufficient or for that matter even
+		// syntactically correct.
+		//
+		// Register declarations
+		// {{{
+		localparam	F_LGDEPTH = LGFIFO+1+8;
+
+		wire	[F_LGDEPTH-1:0]		faxi_awr_nbursts;
+		wire	[9-1:0]			faxi_wr_pending;
+		wire	[F_LGDEPTH-1:0]		faxi_rd_nbursts;
+		wire	[F_LGDEPTH-1:0]		faxi_rd_outstanding;
+
+		//
+		// ...
+		//
+
+		localparam	F_AXIL_LGDEPTH = F_LGDEPTH;
+		wire	[F_AXIL_LGDEPTH-1:0]	faxil_rd_outstanding,
+						faxil_wr_outstanding,
+						faxil_awr_outstanding;
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// AXI channel properties
+		// {{{
+		////////////////////////////////////////////////////////////////
+		//
+		//
+		faxi_slave #(
+			// {{{
+			.C_AXI_ID_WIDTH(IW),
+			.C_AXI_DATA_WIDTH(SLVDW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.F_LGDEPTH(F_AXIL_LGDEPTH),
+			.OPT_EXCLUSIVE(0)
+			// ...
+			// }}}
+		) faxi(
+			// {{{
+			.i_clk(S_AXI_ACLK),
+			.i_axi_reset_n(S_AXI_ARESETN),
+			// Write address
+			// {{{
+			.i_axi_awvalid(skids_awvalid),
+			.i_axi_awready(skids_awready),
+			.i_axi_awid(   skids_awid),
+			.i_axi_awaddr( skids_awaddr),
+			.i_axi_awlen(  skids_awlen),
+			.i_axi_awsize( skids_awsize),
+			.i_axi_awburst(skids_awburst),
+			.i_axi_awlock( 0),
+			.i_axi_awcache(0),
+			.i_axi_awprot( skids_awprot),
+			.i_axi_awqos(  0),
+			// }}}
+			// Write data
+			// {{{
+			.i_axi_wvalid( skids_wvalid),
+			.i_axi_wready( skids_wready),
+			.i_axi_wdata(  skids_wdata),
+			.i_axi_wstrb(  skids_wstrb),
+			.i_axi_wlast(  S_AXI_WLAST),
+			// }}}
+			// Write return response
+			// {{{
+			.i_axi_bvalid( S_AXI_BVALID),
+			.i_axi_bready( S_AXI_BREADY),
+			.i_axi_bid(    S_AXI_BID),
+			.i_axi_bresp(  S_AXI_BRESP),
+			// }}}
+			// Read address
+			// {{{
+			.i_axi_arvalid(1'b0),
+			.i_axi_arready(1'b0),
+			.i_axi_arid(   skids_awid),
+			.i_axi_araddr( skids_awaddr),
+			.i_axi_arlen(  skids_awlen),
+			.i_axi_arsize( skids_awsize),
+			.i_axi_arburst(skids_awburst),
+			.i_axi_arlock( 0),
+			.i_axi_arcache(0),
+			.i_axi_arprot( 0),
+			.i_axi_arqos(  0),
+			// }}}
+			// Read response
+			// {{{
+			.i_axi_rvalid( 1'b0),
+			.i_axi_rready( 1'b0),
+			.i_axi_rid(    S_AXI_RID),
+			.i_axi_rdata(  S_AXI_RDATA),
+			.i_axi_rlast(  S_AXI_RLAST),
+			.i_axi_rresp(  S_AXI_RRESP),
+			// }}}
+			// Formal property data
+			// {{{
+			.f_axi_awr_nbursts(   faxi_awr_nbursts),
+			.f_axi_wr_pending(    faxi_wr_pending),
+			.f_axi_rd_nbursts(    faxi_rd_nbursts),
+			.f_axi_rd_outstanding(faxi_rd_outstanding)
+			//
+			// ...
+			//
+			// }}}
+			// }}}
+		);
+
+		always @(*)
+		begin
+			// ...
+			assert(faxi_rd_nbursts == 0);
+		end
+
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// AXI-lite properties
+		// {{{
+		////////////////////////////////////////////////////////////////
+		//
+		//
+
+		faxil_master #(
+			// {{{
+			.C_AXI_DATA_WIDTH(MSTDW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.F_OPT_NO_RESET(1),
+			.F_AXI_MAXWAIT(5),
+			.F_AXI_MAXDELAY(4),
+			.F_AXI_MAXRSTALL(0),
+			.F_OPT_WRITE_ONLY(1),
+			.F_OPT_READ_ONLY(1'b0),
+			.F_LGDEPTH(F_AXIL_LGDEPTH)
+			// }}}
+		) faxil(
+			// {{{
+			.i_clk(S_AXI_ACLK),
+			.i_axi_reset_n(S_AXI_ARESETN),
+			// Write address channel
+			// {{{
+			.i_axi_awvalid(M_AXI_AWVALID),
+			.i_axi_awready(M_AXI_AWREADY),
+			.i_axi_awaddr( M_AXI_AWADDR),
+			.i_axi_awprot( M_AXI_AWPROT),
+			// }}}
+			// Write data
+			// {{{
+			.i_axi_wvalid( M_AXI_WVALID),
+			.i_axi_wready( M_AXI_WREADY),
+			.i_axi_wdata(  M_AXI_WDATA),
+			.i_axi_wstrb(  M_AXI_WSTRB),
+			// }}}
+			// Write response
+			// {{{
+			.i_axi_bvalid( skidm_bvalid),
+			.i_axi_bready( skidm_bready),
+			.i_axi_bresp(  skidm_bresp),
+			// }}}
+			// Read address
+			// {{{
+			.i_axi_arvalid(M_AXI_ARVALID),
+			.i_axi_arready(M_AXI_ARREADY),
+			.i_axi_araddr( M_AXI_ARADDR),
+			.i_axi_arprot( M_AXI_ARPROT),
+			// }}}
+			// Read data return
+			// {{{
+			.i_axi_rvalid( 1'b0),
+			.i_axi_rready( 1'b1),
+			.i_axi_rdata(  {(C_M_AXI_DATA_WIDTH){1'b0}}),
+			.i_axi_rresp(  2'b00),
+			// }}}
+			// Formal check variables
+			// {{{
+			.f_axi_rd_outstanding(faxil_rd_outstanding),
+			.f_axi_wr_outstanding(faxil_wr_outstanding),
+			.f_axi_awr_outstanding(faxil_awr_outstanding)
+			// }}}
+			// }}}
+		);
+
+		always @(*)
+		if (S_AXI_ARESETN)
+		begin
+			assert(faxil_rd_outstanding == 0);
+
+			assert(faxil_awr_outstanding
+				+ ((mst_awbeats > 0) ? mst_awbeats : 0)
+				== f_wfifo_beats
+				+ (bfifo_write ? bfifo_wdata[SLVSZ-MSTSZ:0] : 0)
+				+ bcounts);
+
+			assert(faxil_wr_outstanding
+				+ ((mst_wbeats > 0) ? mst_wbeats : 0)
+				== f_wfifo_beats
+				+ (bfifo_write ? bfifo_wdata[SLVSZ-MSTSZ:0] : 0)
+				+ bcounts);
+		end
+
+
+		always @(*)
+			assert(faxil_awr_outstanding <= { 1'b1, {(LGFIFO+8){1'b0}} } + bcounts);
+		always @(*)
+			assert(faxil_wr_outstanding  <= { 1'b1, {(LGFIFO+8){1'b0}} } + bcounts);
+
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// BFIFO property checking
+		// {{{
+		////////////////////////////////////////////////////////////////
+		//
+		//
+
+		//
+		// ...
+		//
+
+		always @(posedge S_AXI_ACLK)
+		if (S_AXI_ARESETN)
+		begin
+			assert(faxi_awr_nbursts == f_bfifo_packets
+				+ (slv_awvalid ? 1:0));
+			assert(f_bfifo_packets <= wfifo_count);
+
+			// ...
+		end
+
+		//
+		// ...
+		//
+
+		// }}}
+`endif
+		// }}}
+		// }}}
+	end else begin : NO_WRITE_SUPPORT
+		// {{{
+		assign	S_AXI_AWREADY = 0;
+		assign	S_AXI_WREADY  = 0;
+		assign	S_AXI_BID     = 0;
+		assign	S_AXI_BRESP   = 2'b11;
+		assign	S_AXI_BVALID  = 0;
+		assign	S_AXI_BID     = 0;
+
+		//
+		assign	M_AXI_AWVALID = 0;
+		assign	M_AXI_AWADDR  = 0;
+		assign	M_AXI_AWPROT  = 0;
+		//
+		assign	M_AXI_WVALID  = 0;
+		assign	M_AXI_WDATA   = 0;
+		assign	M_AXI_WSTRB   = 0;
+		//
+		assign	M_AXI_BREADY  = 0;
+		// }}}
+	end end endgenerate
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Read logic
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	generate if (OPT_READS && SLVDW == MSTDW)
+	begin : IMPLEMENT_AXI2AXILITE_READS
+		// {{{
+
+		// (Unused) signal declarations
+		// {{{
+		// Verilator lint_off UNUSED
+		wire				ign_awready, ign_wready,
+						ign_bvalid;
+		wire	[IW-1:0]	ign_bid;
+		wire	[1:0]			ign_bresp;
+
+		wire				ign_awvalid, ign_wvalid,
+						ign_bready;
+		wire	[AW-1:0]	ign_awaddr;
+		wire	[2:0]			ign_awprot;
+		wire	[MSTDW-1:0]	ign_wdata;
+		wire	[MSTDW/8-1:0]	ign_wstrb;
+		// Verilator lint_on  UNUSED
+		// }}}
+
+		axi2axilite #(
+			// {{{
+			.C_AXI_ID_WIDTH(IW),
+			.C_AXI_DATA_WIDTH(SLVDW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.OPT_WRITES(0),
+			.OPT_READS(1),
+			.LGFIFO(LGFIFO)
+			// }}}
+		) axilread (
+		// {{{
+			.S_AXI_ACLK(S_AXI_ACLK),
+			.S_AXI_ARESETN(S_AXI_ARESETN),
+			// AXI4 slave interface
+			// {{{
+			// Write address channel
+			// {{{
+			.S_AXI_AWVALID(1'b0),
+			.S_AXI_AWREADY(ign_awready),
+			.S_AXI_AWID(   {(IW){1'b0}} ),
+			.S_AXI_AWADDR( {(AW){1'b0}} ),
+			.S_AXI_AWLEN(  8'h0),
+			.S_AXI_AWSIZE( 3'h0),
+			.S_AXI_AWBURST(2'h0),
+			.S_AXI_AWLOCK( 1'b0),
+			.S_AXI_AWCACHE(4'h0),
+			.S_AXI_AWPROT( 3'h0),
+			.S_AXI_AWQOS(  4'h0),
+			// }}}
+			// Write data channel
+			// {{{
+			.S_AXI_WVALID(1'b0),
+			.S_AXI_WREADY(ign_wready),
+			.S_AXI_WDATA( {(SLVDW){1'b0}}),
+			.S_AXI_WSTRB( {(SLVDW/8){1'b0}}),
+			.S_AXI_WLAST( 1'b0),
+			// }}}
+			// Write return channel
+			// {{{
+			.S_AXI_BVALID(ign_bvalid),
+			.S_AXI_BREADY(1'b1),
+			.S_AXI_BID(   ign_bid),
+			.S_AXI_BRESP( ign_bresp),
+			// }}}
+			// Read address channel
+			// {{{
+			.S_AXI_ARVALID(S_AXI_ARVALID),
+			.S_AXI_ARREADY(S_AXI_ARREADY),
+			.S_AXI_ARID(   S_AXI_ARID),
+			.S_AXI_ARADDR( S_AXI_ARADDR),
+			.S_AXI_ARLEN(  S_AXI_ARLEN),
+			.S_AXI_ARSIZE( S_AXI_ARSIZE),
+			.S_AXI_ARBURST(S_AXI_ARBURST),
+			.S_AXI_ARLOCK( S_AXI_ARLOCK),
+			.S_AXI_ARCACHE(S_AXI_ARCACHE),
+			.S_AXI_ARPROT( S_AXI_ARPROT),
+			.S_AXI_ARQOS(  S_AXI_ARQOS),
+			// }}}
+			// Read data channel
+			// {{{
+			.S_AXI_RVALID(S_AXI_RVALID),
+			.S_AXI_RREADY(S_AXI_RREADY),
+			.S_AXI_RID(   S_AXI_RID),
+			.S_AXI_RDATA( S_AXI_RDATA),
+			.S_AXI_RRESP( S_AXI_RRESP),
+			.S_AXI_RLAST( S_AXI_RLAST),
+			// }}}
+			// }}}
+			// AXI-lite master interface
+			// {{{
+			// AXI-lite Write interface
+			// {{{
+			.M_AXI_AWVALID(ign_awvalid),
+			.M_AXI_AWREADY(1'b1),
+			.M_AXI_AWADDR(ign_awaddr),
+			.M_AXI_AWPROT(ign_awprot),
+			//
+			.M_AXI_WVALID(ign_wvalid),
+			.M_AXI_WREADY(1'b1),
+			.M_AXI_WDATA(ign_wdata),
+			.M_AXI_WSTRB(ign_wstrb),
+			//
+			.M_AXI_BVALID(1'b0),
+			.M_AXI_BREADY(ign_bready),
+			.M_AXI_BRESP(2'b00),
+			// }}}
+			// AXI-lite read interface
+			// {{{
+			.M_AXI_ARVALID(M_AXI_ARVALID),
+			.M_AXI_ARREADY(M_AXI_ARREADY),
+			.M_AXI_ARADDR(M_AXI_ARADDR),
+			.M_AXI_ARPROT(M_AXI_ARPROT),
+			//
+			.M_AXI_RVALID(M_AXI_RVALID),
+			.M_AXI_RREADY(M_AXI_RREADY),
+			.M_AXI_RDATA(M_AXI_RDATA),
+			.M_AXI_RRESP(M_AXI_RRESP)
+			// }}}
+			// }}}
+			// }}}
+		);
+
+		// }}}
+	end else begin : RDN
+	if (OPT_READS)
+	begin : IMPLEMENT_READS
+		// {{{
+
+		// Declarations
+		// {{{
+		wire				slv_arvalid, slv_arready;
+		reg	[IW-1:0]		slv_arid, mst_arid;
+		reg	[AW-1:0]		slv_araddr, mst_araddr;
+		wire	[AW-1:0]		slv_next_araddr;
+		reg	[7:0]			slv_arlen;
+		reg				slv_arlast, mst_arlast,
+						mst_arsublast;
+		reg	[2:0]			slv_arprot, mst_arprot;
+		reg	[2:0]			slv_arsize;
+		reg	[1:0]			slv_arburst;
+		reg	[SLVSZ-MSTSZ:0]		slv_arbeats, mst_arbeats;
+		reg	[8:0]			slv_rlen;
+
+		wire	[SLVSZ-MSTSZ-1:0]	rfifo_addr;
+		wire				rfifo_end_of_beat,
+						rfifo_rlast;
+		wire	[4:0]			rfifo_count;
+		//
+		reg				m_arvalid;
+		wire				rfifo_full;
+		wire				rfifo_empty;
+		reg				s_axi_rvalid;
+		reg	[1:0]			s_axi_rresp;
+		reg	[IW-1:0]		s_axi_rid;
+		wire	[IW-1:0]		rfifo_rid;
+		reg	[SLVDW-1:0]		s_axi_rdata, next_rdata;
+		reg				s_axi_rlast;
+		reg	[IW-1:0]		rid;
+		wire				read_from_rdfifo;
+
+		//
+		//
+		// S_AXI_AR* skid buffer
+		wire			skids_arvalid, skids_arready;
+		wire	[IW-1:0]	skids_arid;
+		wire	[AW-1:0]	skids_araddr;
+		wire	[7:0]		skids_arlen;
+		wire	[2:0]		skids_arsize, skids_arprot;
+		wire	[1:0]		skids_arburst;
+		//
+		// S_AXI_R* skid buffer isn't needed
+		//
+		// M_AXI_AR* skid buffer isn't needed
+		// M_AXI_R* skid buffer
+		wire			skidm_rvalid, skidm_rready;
+		wire	[MSTDW-1:0]	skidm_rdata;
+		wire	[1:0]		skidm_rresp;
+		// }}}
+
+		// S_AXI_AR* skid buffer
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(IW+AW+8+3+2+3),
+			.OPT_LOWPOWER(OPT_LOWPOWER),
+			.OPT_OUTREG(0)
+			// }}}
+		) arskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(S_AXI_ARVALID), .o_ready(S_AXI_ARREADY),
+			.i_data({ S_AXI_ARID, S_AXI_ARADDR, S_AXI_ARLEN,
+				S_AXI_ARSIZE, S_AXI_ARBURST, S_AXI_ARPROT }),
+			.o_valid(skids_arvalid), .i_ready(skids_arready),
+			.o_data({ skids_arid, skids_araddr, skids_arlen,
+				skids_arsize, skids_arburst, skids_arprot })
+			// }}}
+		);
+		// }}}
+		// M_AXI_R* skid buffer
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(MSTDW+2),
+			.OPT_LOWPOWER(OPT_LOWPOWER),
+			.OPT_OUTREG(0)
+			// }}}
+		) rskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(M_AXI_RVALID), .o_ready(M_AXI_RREADY),
+				.i_data({ M_AXI_RDATA, M_AXI_RRESP }),
+			.o_valid(skidm_rvalid), .i_ready(skidm_rready),
+				.o_data({ skidm_rdata, skidm_rresp })
+			// }}}
+		);
+		// }}}
+
+		assign	skids_arready = (slv_rlen <= (slv_arready ? 1:0))
+					&&(mst_arbeats <=(M_AXI_ARREADY ? 1:0));
+
+		// slv_*
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		begin
+			if (OPT_LOWPOWER && (slv_rlen <= (slv_arready ? 1:0)))
+			begin
+				// {{{
+				slv_arid    <= 0;
+				slv_araddr  <= 0;
+				slv_arlen   <= 0;
+				slv_arsize  <= 0;
+				slv_arburst <= 0;
+				slv_arprot  <= 0;
+
+				slv_rlen    <= 0;
+				// }}}
+			end
+
+			if (skids_arvalid && skids_arready)
+			begin
+				// {{{
+				slv_arid    <= skids_arid;
+				slv_araddr  <= skids_araddr;
+				slv_arlen   <= skids_arlen;
+				slv_arsize  <= skids_arsize;
+				slv_arburst <= skids_arburst;
+				slv_arlast  <= (skids_arlen == 0);
+				slv_arprot  <= skids_arprot;
+
+				slv_rlen    <= skids_arlen+1;
+				// }}}
+			end else if (slv_arready && slv_rlen > 0)
+			begin
+				// {{{
+				slv_araddr  <= (!OPT_LOWPOWER || slv_rlen > 1)
+							? slv_next_araddr : 0;
+				slv_rlen    <= slv_rlen - 1;
+				slv_arlast  <= (slv_rlen <= 2);
+				// }}}
+			end
+
+			if (OPT_LOWPOWER && !S_AXI_ARESETN)
+			begin
+				// {{{
+				slv_arid    <= 0;
+				slv_araddr  <= 0;
+				slv_arlen   <= 0;
+				slv_arsize  <= 0;
+				slv_arburst <= 0;
+				slv_arprot  <= 0;
+
+				slv_arlast  <= 1;
+				// }}}
+			end
+
+			if (!S_AXI_ARESETN)
+				slv_rlen <= 0;
+		end
+
+		assign	slv_arvalid = (slv_rlen > 0);
+`ifdef	FORMAL
+		always @(*)
+		if (S_AXI_ARESETN)
+		begin
+			assert(slv_arlast == (slv_rlen <= 1));
+			assert(slv_rlen <= (slv_arlen + 1));
+		end
+`endif
+		// }}}
+
+		// slv_next_araddr
+		// {{{
+		axi_addr #(
+			// {{{
+			.AW(AW),
+			.DW(SLVDW)
+			// }}}
+		) get_next_slave_addr (
+			// {{{
+			.i_last_addr(slv_araddr),
+			.i_size(slv_arsize),
+			.i_burst(slv_arburst),
+			.i_len(slv_arlen),
+			.o_next_addr(slv_next_araddr)
+			// }}}
+		);
+		// }}}
+
+		// slv_arbeats
+		// {{{
+		always @(*)
+		if (slv_rlen > 0)
+		begin
+			// Master beats to turn this slave beat into
+			if (slv_arsize >= MSTSZ[2:0])
+				slv_arbeats = (1<<(slv_arsize-MSTSZ[2:0]))
+					- (slv_araddr[MSTSZ-1:0] >> slv_arsize);
+			else
+				slv_arbeats = 1;
+		end else
+			slv_arbeats = 0;
+		// }}}
+
+		// mst_araddr, mst_arprot, mst_arbeats
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		begin
+			if (slv_arready)
+			begin
+				// {{{
+				mst_arid    <= slv_arid;
+				mst_araddr  <= slv_araddr;
+				mst_arprot  <= slv_arprot;
+
+				// Beats to turn this beat into
+				mst_arbeats <= slv_arbeats;
+				mst_arlast  <= slv_arlast;
+				mst_arsublast <= (slv_arbeats <= 1);
+
+				if (OPT_LOWPOWER && slv_rlen == 0)
+				begin
+					mst_arid   <= 0;
+					mst_araddr <= 0;
+					mst_arprot <= 0;
+				end
+				// }}}
+			end else if ((mst_arbeats > 0)
+					&&(M_AXI_ARVALID && M_AXI_ARREADY))
+			begin
+				// {{{
+				mst_araddr <= mst_araddr + (1<<MSTSZ);
+				mst_araddr[MSTSZ-1:0] <= 0;
+				mst_arbeats <= mst_arbeats - 1;
+
+				mst_arsublast <= (mst_arbeats <= 2);
+				// }}}
+			end
+
+			if (!S_AXI_ARESETN)
+			begin
+				// {{{
+				mst_arbeats <= 0;
+				if (OPT_LOWPOWER)
+				begin
+					mst_arid    <= 0;
+					mst_araddr  <= 0;
+					mst_arprot  <= 0;
+				end
+				// }}}
+			end
+		end
+`ifdef	FORMAL
+		always @(*)
+		if(OPT_LOWPOWER && S_AXI_ARESETN && mst_arbeats == 0)
+		begin
+			assert(mst_arid   == 0);
+			assert(mst_araddr == 0);
+			assert(mst_arprot == 0);
+		end
+`endif
+		// }}}
+
+		// m_arvalid
+		// {{{
+		initial	m_arvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			m_arvalid <= 0;
+		else if (slv_arvalid && slv_arready)
+			m_arvalid <= 1;
+		else if (M_AXI_ARVALID && M_AXI_ARREADY)
+			m_arvalid <= (mst_arbeats > 1);
+`ifdef	FORMAL
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(M_AXI_ARVALID == (mst_arbeats > 0));
+`endif
+		// }}}
+
+		assign	slv_arready = (mst_arbeats <= (M_AXI_ARREADY ? 1:0));
+		assign	read_from_rdfifo = skidm_rvalid && skidm_rready
+					&&(!S_AXI_RVALID || S_AXI_RREADY);
+
+		// Read ID FIFO
+		// {{{
+		sfifo	#(
+			// {{{
+			.BW(IW+2+SLVSZ-MSTSZ),
+			.LGFLEN(LGFIFO)
+			// }}}
+		) ridlnfifo(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			//
+			.i_wr(M_AXI_ARVALID && M_AXI_ARREADY),
+			.i_data({ mst_arid, mst_arlast, mst_arsublast,
+				M_AXI_ARADDR[SLVSZ-1:MSTSZ] }),
+			.o_full(rfifo_full), .o_fill(rfifo_count),
+			//
+			.i_rd(read_from_rdfifo),
+			.o_data({ rfifo_rid, rfifo_rlast, rfifo_end_of_beat,
+				rfifo_addr }),
+			.o_empty(rfifo_empty)
+			// }}}
+		);
+		// }}}
+
+		assign	skidm_rready = (!S_AXI_RVALID || S_AXI_RREADY)
+				&& !rfifo_empty;
+
+		// s_axi_rvalid
+		// {{{
+		initial	s_axi_rvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			s_axi_rvalid <= 0;
+		else if (skidm_rvalid && skidm_rready && rfifo_end_of_beat)
+			s_axi_rvalid <= 1'b1;
+		else if (S_AXI_RREADY)
+			s_axi_rvalid <= 0;
+		// }}}
+
+		// s_axi_rdata
+		// {{{
+		always @(*)
+		begin
+			next_rdata = s_axi_rdata;
+			if (S_AXI_RVALID)
+				next_rdata = 0;
+			if (skidm_rvalid)
+				next_rdata = next_rdata | ({ {(SLVDW-MSTDW){1'b0}}, skidm_rdata } << (rfifo_addr * MSTDW));
+		end
+
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+			s_axi_rdata <= 0;
+		else if (!S_AXI_RVALID || S_AXI_RREADY)
+			s_axi_rdata <= next_rdata;
+		// }}}
+
+		// s_axi_rresp
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			s_axi_rresp <= OKAY;
+		else if (!S_AXI_RVALID || S_AXI_RREADY)
+		begin
+			if (S_AXI_RVALID)
+				s_axi_rresp <= (skidm_rvalid) ? skidm_rresp : OKAY;
+			else if (skidm_rvalid)
+			casez({ s_axi_rresp, skidm_rresp[1] })
+			// Let SLVERR take priority over DECERR
+			3'b??0: s_axi_rresp <= s_axi_rresp;
+			3'b0?1: s_axi_rresp <= skidm_rresp;
+			3'b101: s_axi_rresp <= SLVERR;
+			3'b111: s_axi_rresp <= skidm_rresp;
+			endcase
+		end
+		// }}}
+
+		// rid
+		// {{{
+		initial	rid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (read_from_rdfifo)
+			rid <= rfifo_rid;
+		// }}}
+
+		// s_axi_rlast
+		// {{{
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_RVALID || S_AXI_RREADY)
+		begin
+			if (read_from_rdfifo)
+				s_axi_rlast <= rfifo_rlast;
+			else
+				s_axi_rlast <= 0;
+		end
+		// }}}
+
+		// s_axi_rid
+		// {{{
+		initial	s_axi_rid = 0;
+		always @(posedge S_AXI_ACLK)
+		if ((S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST)
+				||(!S_AXI_RVALID && rfifo_end_of_beat))
+			s_axi_rid <= (read_from_rdfifo && rfifo_end_of_beat)?rfifo_rid : rid;
+		// }}}
+
+		// M_AXI_AR*
+		// {{{
+		assign	M_AXI_ARVALID= m_arvalid;
+		assign	M_AXI_ARADDR = mst_araddr;
+		assign	M_AXI_ARPROT = mst_arprot;
+		// }}}
+		// S_AXI_R*
+		// {{{
+		assign	S_AXI_RVALID = s_axi_rvalid;
+		assign	S_AXI_RDATA  = s_axi_rdata;
+		assign	S_AXI_RRESP  = s_axi_rresp;
+		assign	S_AXI_RLAST  = s_axi_rlast;
+		assign	S_AXI_RID    = s_axi_rid;
+		// }}}
+		// Make Verilator happy
+		// {{{
+		// Verilator lint_off UNUSED
+		wire	unused_read;
+		assign	unused_read = &{ 1'b0,
+				/*
+				S_AXI_AWID, S_AXI_AWVALID,
+				S_AXI_AWLEN, S_AXI_AWBURST, S_AXI_AWSIZE,
+				S_AXI_AWADDR,
+				S_AXI_WVALID, S_AXI_WDATA, S_AXI_WSTRB,
+				S_AXI_WLAST, S_AXI_BREADY,
+				M_AXI_AWREADY, M_AXI_WREADY,
+				M_AXI_BRESP, M_AXI_BVALID,
+				*/
+				rfifo_count, rfifo_full
+				};
+		// Verilator lint_on  UNUSED
+		// }}}
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+		//
+		// Formal properties, read half
+		// {{{
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+		////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+		// As with the write half, the following is a subset of the
+		// formal properties used to verify this section of the core.
+		// It may, or may not, be syntactically correct.  I don't
+		// warrant this version of the design.
+		//
+		// Register declarations
+		// {{{
+		localparam	F_LGDEPTH = LGFIFO+1+8;
+
+		wire	[F_LGDEPTH-1:0]		faxi_awr_nbursts;
+		wire	[9-1:0]			faxi_wr_pending;
+		wire	[F_LGDEPTH-1:0]		faxi_rd_nbursts;
+		wire	[F_LGDEPTH-1:0]		faxi_rd_outstanding;
+
+		//
+		// ...
+		//
+
+		localparam	F_AXIL_LGDEPTH = F_LGDEPTH;
+		wire	[F_AXIL_LGDEPTH-1:0]	faxil_rd_outstanding,
+						faxil_wr_outstanding,
+						faxil_awr_outstanding;
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// AXI channel properties
+		// {{{
+		////////////////////////////////////////////////////////////////
+		//
+		//
+		faxi_slave #(
+			// {{{
+			.C_AXI_ID_WIDTH(IW),
+			.C_AXI_DATA_WIDTH(SLVDW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.OPT_EXCLUSIVE(0)
+			// ...
+			// }}}
+		) faxi(
+			// {{{
+			.i_clk(S_AXI_ACLK),
+			.i_axi_reset_n(S_AXI_ARESETN),
+			// Write address
+			// {{{
+			.i_axi_awvalid(1'b0),
+			.i_axi_awready(1'b0),
+			.i_axi_awid(   skids_arid),
+			.i_axi_awaddr( skids_araddr),
+			.i_axi_awlen(  8'h0),
+			.i_axi_awsize( 3'h0),
+			.i_axi_awburst(2'h0),
+			.i_axi_awlock( 0),
+			.i_axi_awcache(0),
+			.i_axi_awprot( 0),
+			.i_axi_awqos(  0),
+			// }}}
+			// Write data
+			// {{{
+			.i_axi_wvalid( 1'b0),
+			.i_axi_wready( 1'b0),
+			.i_axi_wdata(  {(C_S_AXI_DATA_WIDTH  ){1'b0}}),
+			.i_axi_wstrb(  {(C_S_AXI_DATA_WIDTH/8){1'b0}}),
+			.i_axi_wlast(  1'b0),
+			// }}}
+			// Write return response
+			// {{{
+			.i_axi_bvalid( 1'b0),
+			.i_axi_bready( 1'b0),
+			.i_axi_bid(    S_AXI_BID),
+			.i_axi_bresp(  2'b00),
+			// }}}
+			// Read address
+			// {{{
+			.i_axi_arready(skids_arready),
+			.i_axi_arid(   skids_arid),
+			.i_axi_araddr( skids_araddr),
+			.i_axi_arlen(  skids_arlen),
+			.i_axi_arsize( skids_arsize),
+			.i_axi_arburst(skids_arburst),
+			.i_axi_arlock( 0),
+			.i_axi_arcache(0),
+			.i_axi_arprot( 0),
+			.i_axi_arqos(  0),
+			.i_axi_arvalid(skids_arvalid),
+			// }}}
+			// Read response
+			// {{{
+			.i_axi_rid(    S_AXI_RID),
+			.i_axi_rresp(  S_AXI_RRESP),
+			.i_axi_rvalid( S_AXI_RVALID),
+			.i_axi_rdata(  S_AXI_RDATA),
+			.i_axi_rlast(  S_AXI_RLAST),
+			.i_axi_rready( S_AXI_RREADY),
+			// }}}
+			// Formal property data
+			// {{{
+			.f_axi_awr_nbursts(   faxi_awr_nbursts),
+			.f_axi_wr_pending(    faxi_wr_pending),
+			.f_axi_rd_nbursts(    faxi_rd_nbursts),
+			.f_axi_rd_outstanding(faxi_rd_outstanding),
+			//
+			// ...
+			//
+			// }}}
+			// }}}
+		);
+
+		always @(*)
+		begin
+			assert(faxi_awr_nbursts == 0);
+			assert(faxi_wr_pending == 0);
+			assert(faxi_wr_ckvalid == 0);
+		end
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// AXI-lite properties
+		// {{{
+		////////////////////////////////////////////////////////////////
+		//
+		//
+		faxil_master #(
+			// {{{
+			.C_AXI_DATA_WIDTH(MSTDW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.F_OPT_NO_RESET(1),
+			.F_AXI_MAXWAIT(5),
+			.F_AXI_MAXDELAY(4),
+			.F_AXI_MAXRSTALL(0),
+			.F_OPT_WRITE_ONLY(1'b0),
+			.F_OPT_READ_ONLY(1'b1),
+			.F_LGDEPTH(F_AXIL_LGDEPTH)
+			// }}}
+		) faxil(
+			// {{{
+			.i_clk(S_AXI_ACLK),
+			.i_axi_reset_n(S_AXI_ARESETN),
+			// Write address channel
+			// {{{
+			.i_axi_awvalid(1'b0),
+			.i_axi_awready(1'b0),
+			.i_axi_awaddr( M_AXI_AWADDR),
+			.i_axi_awprot( 3'h0),
+			// }}}
+			// Write data
+			// {{{
+			.i_axi_wvalid( 1'b0),
+			.i_axi_wready( 1'b0),
+			.i_axi_wdata(  {(C_M_AXI_DATA_WIDTH  ){1'b0}}),
+			.i_axi_wstrb(  {(C_M_AXI_DATA_WIDTH/8){1'b0}}),
+			// }}}
+			// Write response
+			// {{{
+			.i_axi_bvalid( 1'b0),
+			.i_axi_bready( 1'b0),
+			.i_axi_bresp(  2'b00),
+			// }}}
+			// Read address
+			// {{{
+			.i_axi_arvalid(M_AXI_ARVALID),
+			.i_axi_arready(M_AXI_ARREADY),
+			.i_axi_araddr( M_AXI_ARADDR),
+			.i_axi_arprot( M_AXI_ARPROT),
+			// }}}
+			// Read data return
+			// {{{
+			.i_axi_rvalid( skidm_rvalid),
+			.i_axi_rready( skidm_rready),
+			.i_axi_rdata(  skidm_rdata),
+			.i_axi_rresp(  skidm_rresp),
+			// }}}
+			// Formal check variables
+			// {{{
+			.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 == 0);
+			assert(faxil_wr_outstanding == 0);
+		end
+		// }}}
+`endif
+		// }}}
+		// }}}
+	end else begin : NO_READ_SUPPORT // if (!OPT_READS)
+		// {{{
+		assign	M_AXI_ARVALID= 0;
+		assign	M_AXI_ARADDR = 0;
+		assign	M_AXI_ARPROT = 0;
+		assign	M_AXI_RREADY = 0;
+		//
+		assign	S_AXI_ARREADY= 0;
+		assign	S_AXI_RVALID = 0;
+		assign	S_AXI_RDATA  = 0;
+		assign	S_AXI_RRESP  = 0;
+		assign	S_AXI_RLAST  = 0;
+		assign	S_AXI_RID    = 0;
+
+		// Make Verilator happy
+		// Verilator lint_off UNUSED
+		wire	unused_read;
+		assign	unused_read = &{ 1'b0, M_AXI_ARREADY, M_AXI_RVALID,
+				M_AXI_RDATA, M_AXI_RRESP, S_AXI_RREADY,
+				S_AXI_ARLEN, S_AXI_ARSIZE, S_AXI_ARBURST,
+				S_AXI_ARADDR, S_AXI_ARVALID, S_AXI_ARID
+				};
+		// Verilator lint_on  UNUSED
+		// }}}
+	end end endgenerate
+	// }}}
+	// Minimal parameter validation
+	// {{{
+	initial begin
+		if (SLVDW < MSTDW)
+		begin
+			$fatal;		// Fatal elaboration error
+			$stop;		// Stop any simulation
+		end
+	end
+	// }}}
+	// Make Verilator happy
+	// {{{
+	// Verilator lint_off UNUSED
+	wire	unused;
+	assign	unused = &{ 1'b0,
+		S_AXI_AWLOCK, S_AXI_AWCACHE, S_AXI_AWPROT, S_AXI_AWQOS,
+		// skids_wlast, wfifo_count, rfifo_count
+		S_AXI_ARLOCK, S_AXI_ARCACHE, S_AXI_ARPROT, S_AXI_ARQOS
+		};
+	// Verilator lint_on  UNUSED
+	// }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal properties
+// {{{
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Assume that the two write channels stay within an appropriate
+	// distance of each other.  This is to make certain that the property
+	// file features are not violated, although not necessary true for
+	// actual operation
+	//
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Select only write or only read operation
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	generate if (!OPT_WRITES)
+	begin
+		always @(*)
+		begin
+			assume(!S_AXI_AWVALID);
+			assume(!S_AXI_WVALID);
+			assert(!M_AXI_AWVALID);
+			assert(!M_AXI_WVALID);
+			assume(!M_AXI_BVALID);
+			assert(!S_AXI_BVALID);
+		end
+	end endgenerate
+
+	generate if (!OPT_READS)
+	begin
+
+		always @(*)
+		begin
+			assume(!S_AXI_ARVALID);
+			assert(!M_AXI_ARVALID);
+		end
+
+	end endgenerate
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Lowpower assertions
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	generate if (OPT_LOWPOWER)
+	begin : F_LOWPOWER
+
+		always @(*)
+		if (S_AXI_ARESETN)
+		begin
+			if (!M_AXI_AWVALID)
+			begin
+				// Not supported.
+				// assert(M_AXI_AWADDR == 0);
+				// assert(M_AXI_AWPROT == 0);
+			end
+
+			if (!M_AXI_WVALID)
+			begin
+				// assert(M_AXI_WDATA == 0);
+				// assert(M_AXI_WSTRB == 0);
+			end
+
+			if (!M_AXI_ARVALID)
+			begin
+				assert(M_AXI_ARADDR == 0);
+				assert(M_AXI_ARPROT == 0);
+			end
+
+			if (!S_AXI_RVALID)
+			begin
+				// These items build over the course of a
+				// returned burst, so they might not be
+				// zero when RVALID is zero.
+				//
+				// assert(S_AXI_RLAST == 0);
+				// assert(S_AXI_RDATA == 0);
+				// assert(S_AXI_RID == 0);
+			end
+		end
+
+	end endgenerate
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Cover statements, to show performance
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	generate if (OPT_READS)
+	begin
+		// {{{
+		reg	[3:0]	cvr_read_count, cvr_read_count_simple;
+
+		initial	cvr_read_count_simple = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_read_count_simple <= 0;
+		else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN == 0)
+			cvr_read_count_simple <= cvr_read_count_simple + 1;
+
+		initial	cvr_read_count = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_read_count <= 0;
+		else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN > 2)
+			cvr_read_count <= cvr_read_count + 1;
+
+		// }}}
+	end endgenerate
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// "Careless" assumptions
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+
+	// }}}
+`undef	BMC_ASSERT
+`endif
+// }}}
+endmodule