rtl/wb2axip: add to version control

1 files changed, 2421 insertions, 0 deletions

diff --git a/rtl/wb2axip/axilxbar.v b/rtl/wb2axip/axilxbar.v
new file mode 100644
index 0000000..4a1ed43
--- /dev/null
+++ b/rtl/wb2axip/axilxbar.v
@@ -0,0 +1,2421 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: 	axilxbar.v
+// {{{
+// Project:	WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose:	Create a full crossbar between NM AXI-lite sources (masters),
+//		and NS AXI-lite slaves.  Every master can talk to any slave,
+//	provided it isn't already busy.
+//
+// Performance:	This core has been designed with the goal of being able to push
+//		one transaction through the interconnect, from any master to
+//	any slave, per clock cycle.  This may perhaps be its most unique
+//	feature.  While throughput is good, latency is something else.
+//
+//	The arbiter requires a clock to switch, then another clock to send data
+//	downstream.  This creates a minimum two clock latency up front.  The
+//	return path suffers another clock of latency as well, placing the
+//	minimum latency at four clocks.  The minimum write latency is at
+//	least one clock longer, since the write data must wait for the write
+//	address before proceeeding.
+//
+// Usage:	To use, you must first set NM and NS to the number of masters
+//	and the number of slaves you wish to connect to.  You then need to
+//	adjust the addresses of the slaves, found SLAVE_ADDR array.  Those
+//	bits that are relevant in SLAVE_ADDR to then also be set in SLAVE_MASK.
+//	Adjusting the data and address widths go without saying.
+//
+//	Lower numbered masters are given priority in any "fight".
+//
+//	Channel grants are given on the condition that 1) they are requested,
+//	2) no other channel has a grant, 3) all of the responses have been
+//	received from the current channel, and 4) the internal counters are
+//	not overflowing.
+//
+//	The core limits the number of outstanding transactions on any channel to
+//	1<<LGMAXBURST-1.
+//
+//	Channel grants are lost 1) after OPT_LINGER clocks of being idle, or
+//	2) when another master requests an idle (but still lingering) channel
+//	assignment, or 3) once all the responses have been returned to the
+//	current channel, and the current master is requesting another channel.
+//
+//	A special slave is allocated for the case of no valid address.
+//
+//	Since the write channel has no address information, the write data
+//	channel always be delayed by at least one clock from the write address
+//	channel.
+//
+//	If OPT_LOWPOWER is set, then unused values will be set to zero.
+//	This can also be used to help identify relevant values within any
+//	trace.
+//
+//
+// Creator:	Dan Gisselquist, Ph.D.
+//		Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2019-2024, Gisselquist Technology, LLC
+// {{{
+// This file is part of the WB2AXIP project.
+//
+// The WB2AXIP project contains free software and gateware, licensed under the
+// Apache License, Version 2.0 (the "License").  You may not use this project,
+// or this file, except in compliance with the License.  You may obtain a copy
+// of the License at
+//
+//	http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  See the
+// License for the specific language governing permissions and limitations
+// under the License.
+//
+////////////////////////////////////////////////////////////////////////////////
+//
+`default_nettype none
+// }}}
+module	axilxbar #(
+		// {{{
+		parameter integer C_AXI_DATA_WIDTH = 32,
+		parameter integer C_AXI_ADDR_WIDTH = 32,
+		//
+		// NM is the number of master interfaces this core supports
+		parameter	NM = 4,
+		//
+		// NS is the number of slave interfaces
+		parameter	NS = 8,
+		//
+		// AW, and DW, are short-hand abbreviations used locally.
+		localparam	AW = C_AXI_ADDR_WIDTH,
+		localparam	DW = C_AXI_DATA_WIDTH,
+		// SLAVE_ADDR is a bit vector containing AW bits for each of the
+		// slaves indicating the base address of the slave.  This
+		// goes with SLAVE_MASK below.
+		parameter	[NS*AW-1:0]	SLAVE_ADDR = {
+			3'b111,  {(AW-3){1'b0}},
+			3'b110,  {(AW-3){1'b0}},
+			3'b101,  {(AW-3){1'b0}},
+			3'b100,  {(AW-3){1'b0}},
+			3'b011,  {(AW-3){1'b0}},
+			3'b010,  {(AW-3){1'b0}},
+			4'b0001, {(AW-4){1'b0}},
+			4'b0000, {(AW-4){1'b0}} },
+		//
+		// SLAVE_MASK indicates which bits in the SLAVE_ADDR bit vector
+		// need to be checked to determine if a given address request
+		// maps to the given slave or not
+		// Verilator lint_off WIDTH
+		parameter	[NS*AW-1:0]	SLAVE_MASK =
+			(NS <= 1) ? { 4'b1111, {(AW-4){1'b0}} }
+			: { {(NS-2){ 3'b111, {(AW-3){1'b0}} }},
+				{(2){ 4'b1111, {(AW-4){1'b0}} }} },
+		// Verilator lint_on WIDTH
+		//
+		// If set, OPT_LOWPOWER will set all unused registers, both
+		// internal and external, to zero anytime their corresponding
+		// *VALID bit is clear
+		parameter [0:0]	OPT_LOWPOWER = 1,
+		//
+		// OPT_LINGER is the number of cycles to wait, following a
+		// transaction, before tearing down the bus grant.
+		parameter	OPT_LINGER = 4,
+		//
+		// LGMAXBURST is the log (base two) of the maximum number of
+		// requests that can be outstanding on any given channel at any
+		// given time.  It is used within this core to control the
+		// counters that are used to determine if a particular channel
+		// grant must stay open, or if it may be closed.
+		parameter	LGMAXBURST = 5
+		// }}}
+	) (
+		// {{{
+		input	wire	S_AXI_ACLK,
+		input	wire	S_AXI_ARESETN,
+		// Incoming AXI4-lite slave port(s)
+		// {{{
+		input	wire	[NM-1:0]			S_AXI_AWVALID,
+		output	wire	[NM-1:0]			S_AXI_AWREADY,
+		input	wire	[NM*C_AXI_ADDR_WIDTH-1:0]	S_AXI_AWADDR,
+		// Verilator coverage_off
+		input	wire	[NM*3-1:0]			S_AXI_AWPROT,
+		// Verilator coverage_on
+		//
+		input	wire	[NM-1:0]			S_AXI_WVALID,
+		output	wire	[NM-1:0]			S_AXI_WREADY,
+		input	wire	[NM*C_AXI_DATA_WIDTH-1:0]	S_AXI_WDATA,
+		input	wire	[NM*C_AXI_DATA_WIDTH/8-1:0]	S_AXI_WSTRB,
+		//
+		output	wire	[NM-1:0]			S_AXI_BVALID,
+		input	wire	[NM-1:0]			S_AXI_BREADY,
+		output	wire	[NM*2-1:0]			S_AXI_BRESP,
+		//
+		input	wire	[NM-1:0]			S_AXI_ARVALID,
+		output	wire	[NM-1:0]			S_AXI_ARREADY,
+		input	wire	[NM*C_AXI_ADDR_WIDTH-1:0]	S_AXI_ARADDR,
+		// Verilator coverage_off
+		input	wire	[NM*3-1:0]			S_AXI_ARPROT,
+		// Verilator coverage_on
+		//
+		output	wire	[NM-1:0]			S_AXI_RVALID,
+		input	wire	[NM-1:0]			S_AXI_RREADY,
+		output	wire	[NM*C_AXI_DATA_WIDTH-1:0]	S_AXI_RDATA,
+		output	wire	[NM*2-1:0]			S_AXI_RRESP,
+		// }}}
+		// Outgoing AXI4-lite master port(s)
+		// {{{
+		output	wire	[NS*C_AXI_ADDR_WIDTH-1:0]	M_AXI_AWADDR,
+		output	wire	[NS*3-1:0]			M_AXI_AWPROT,
+		output	wire	[NS-1:0]			M_AXI_AWVALID,
+		input	wire	[NS-1:0]			M_AXI_AWREADY,
+		//
+		output	wire	[NS*C_AXI_DATA_WIDTH-1:0]	M_AXI_WDATA,
+		output	wire	[NS*C_AXI_DATA_WIDTH/8-1:0]	M_AXI_WSTRB,
+		output	wire	[NS-1:0]			M_AXI_WVALID,
+		input	wire	[NS-1:0]			M_AXI_WREADY,
+		//
+		input	wire	[NS*2-1:0]			M_AXI_BRESP,
+		input	wire	[NS-1:0]			M_AXI_BVALID,
+		output	wire	[NS-1:0]			M_AXI_BREADY,
+		//
+		output	wire	[NS*C_AXI_ADDR_WIDTH-1:0]	M_AXI_ARADDR,
+		output	wire	[NS*3-1:0]			M_AXI_ARPROT,
+		output	wire	[NS-1:0]			M_AXI_ARVALID,
+		input	wire	[NS-1:0]			M_AXI_ARREADY,
+		//
+		input	wire	[NS*C_AXI_DATA_WIDTH-1:0]	M_AXI_RDATA,
+		input	wire	[NS*2-1:0]			M_AXI_RRESP,
+		input	wire	[NS-1:0]			M_AXI_RVALID,
+		output	wire	[NS-1:0]			M_AXI_RREADY
+		// }}}
+		// }}}
+	);
+	//
+	// Local parameters, derived from those above
+	// {{{
+	localparam	LGLINGER = (OPT_LINGER>1) ? $clog2(OPT_LINGER+1) : 1;
+	//
+	localparam	LGNM = (NM>1) ? $clog2(NM) : 1;
+	localparam	LGNS = (NS>1) ? $clog2(NS+1) : 1;
+	//
+	// In order to use indexes, and hence fully balanced mux trees, it helps
+	// to make certain that we have a power of two based lookup.  NMFULL
+	// is the number of masters in this lookup, with potentially some
+	// unused extra ones.  NSFULL is defined similarly.
+	localparam	NMFULL = (NM>1) ? (1<<LGNM) : 1;
+	localparam	NSFULL = (NS>1) ? (1<<LGNS) : 2;
+	//
+	localparam [1:0] INTERCONNECT_ERROR = 2'b11;
+	localparam [0:0]	OPT_SKID_INPUT = 0;
+	localparam [0:0]	OPT_BUFFER_DECODER = 1;
+
+	genvar	N,M;
+	integer	iN, iM;
+	// }}}
+
+	// {{{
+	reg	[NSFULL-1:0]	wrequest		[0:NM-1];
+	reg	[NSFULL-1:0]	rrequest		[0:NM-1];
+	reg	[NSFULL-1:0]	wrequested		[0:NM];
+	reg	[NSFULL-1:0]	rrequested		[0:NM];
+	reg	[NS:0]		wgrant			[0:NM-1];
+	reg	[NS:0]		rgrant			[0:NM-1];
+	reg	[NM-1:0]	swgrant;
+	reg	[NM-1:0]	srgrant;
+	reg	[NS-1:0]	mwgrant;
+	reg	[NS-1:0]	mrgrant;
+
+	// verilator lint_off UNUSED
+	wire	[LGMAXBURST-1:0]	w_sawpending	[0:NM-1];
+`ifdef	FORMAL
+	wire	[LGMAXBURST-1:0]	w_swpending	[0:NM-1];
+`endif
+	wire	[LGMAXBURST-1:0]	w_srpending	[0:NM-1];
+	// verilator lint_on  UNUSED
+	reg	[NM-1:0]		swfull;
+	reg	[NM-1:0]		srfull;
+	reg	[NM-1:0]		swempty;
+	reg	[NM-1:0]		srempty;
+	//
+	wire	[LGNS-1:0]		swindex	[0:NMFULL-1];
+	wire	[LGNS-1:0]		srindex	[0:NMFULL-1];
+	wire	[LGNM-1:0]		mwindex	[0:NSFULL-1];
+	wire	[LGNM-1:0]		mrindex	[0:NSFULL-1];
+
+	wire	[NM-1:0]		wdata_expected;
+
+	// The shadow buffers
+	wire	[NMFULL-1:0]	m_awvalid, m_wvalid, m_arvalid;
+	wire	[NM-1:0]	dcd_awvalid, dcd_arvalid;
+
+	wire	[C_AXI_ADDR_WIDTH-1:0]		m_awaddr	[0:NMFULL-1];
+	wire	[2:0]				m_awprot	[0:NMFULL-1];
+	wire	[C_AXI_DATA_WIDTH-1:0]		m_wdata		[0:NMFULL-1];
+	wire	[C_AXI_DATA_WIDTH/8-1:0]	m_wstrb		[0:NMFULL-1];
+
+	wire	[C_AXI_ADDR_WIDTH-1:0]		m_araddr	[0:NMFULL-1];
+	wire	[2:0]				m_arprot	[0:NMFULL-1];
+	//
+
+	wire	[NM-1:0]	skd_awvalid, skd_awstall, skd_wvalid;
+	wire	[NM-1:0]	skd_arvalid, skd_arstall;
+	wire	[AW-1:0]	skd_awaddr			[0:NM-1];
+	wire	[3-1:0]		skd_awprot			[0:NM-1];
+	wire	[AW-1:0]	skd_araddr			[0:NM-1];
+	wire	[3-1:0]		skd_arprot			[0:NM-1];
+
+	reg	[NM-1:0]	r_bvalid;
+	reg	[1:0]		r_bresp		[0:NM-1];
+
+	reg	[NSFULL-1:0]	m_axi_awvalid;
+	reg	[NSFULL-1:0]	m_axi_awready;
+	reg	[NSFULL-1:0]	m_axi_wvalid;
+	reg	[NSFULL-1:0]	m_axi_wready;
+	reg	[NSFULL-1:0]	m_axi_bvalid;
+`ifdef	FORMAL
+	reg	[NSFULL-1:0]	m_axi_bready;
+`endif
+	reg	[1:0]		m_axi_bresp	[0:NSFULL-1];
+
+	reg	[NSFULL-1:0]	m_axi_arvalid;
+	// Verilator lint_off UNUSED
+	reg	[NSFULL-1:0]	m_axi_arready;
+	// Verilator lint_on  UNUSED
+	reg	[NSFULL-1:0]	m_axi_rvalid;
+	// Verilator lint_off UNUSED
+	reg	[NSFULL-1:0]	m_axi_rready;
+	// Verilator lint_on  UNUSED
+
+	reg	[NM-1:0]	r_rvalid;
+	reg	[1:0]		r_rresp		[0:NM-1];
+	reg	[DW-1:0]	r_rdata		[0:NM-1];
+
+	reg	[DW-1:0]	m_axi_rdata	[0:NSFULL-1];
+	reg	[1:0]		m_axi_rresp	[0:NSFULL-1];
+
+	reg	[NM-1:0]	slave_awaccepts;
+	reg	[NM-1:0]	slave_waccepts;
+	reg	[NM-1:0]	slave_raccepts;
+	// }}}
+
+	// m_axi_[aw|w|b]*
+	// {{{
+	always @(*)
+	begin
+		m_axi_awvalid = -1;
+		m_axi_awready = -1;
+		m_axi_wvalid = -1;
+		m_axi_wready = -1;
+		m_axi_bvalid = 0;
+
+		m_axi_awvalid[NS-1:0] = M_AXI_AWVALID;
+		m_axi_awready[NS-1:0] = M_AXI_AWREADY;
+		m_axi_wvalid[NS-1:0]  = M_AXI_WVALID;
+		m_axi_wready[NS-1:0]  = M_AXI_WREADY;
+		m_axi_bvalid[NS-1:0]  = M_AXI_BVALID;
+
+		for(iM=0; iM<NS; iM=iM+1)
+		begin
+			m_axi_bresp[iM] = M_AXI_BRESP[iM* 2 +:  2];
+
+			m_axi_rdata[iM] = M_AXI_RDATA[iM*DW +: DW];
+			m_axi_rresp[iM] = M_AXI_RRESP[iM* 2 +:  2];
+		end
+		for(iM=NS; iM<NSFULL; iM=iM+1)
+		begin
+			m_axi_bresp[iM] = INTERCONNECT_ERROR;
+
+			m_axi_rdata[iM] = 0;
+			m_axi_rresp[iM] = INTERCONNECT_ERROR;
+		end
+
+`ifdef	FORMAL
+		m_axi_bready = -1;
+		m_axi_bready[NS-1:0]  = M_AXI_BREADY;
+`endif
+	end
+	// }}}
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : DECODE_WRITE_REQUEST
+		// {{{
+		wire	[NS:0]		wdecode;
+		reg	r_mawvalid, r_mwvalid;
+
+		// awskid
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(AW+3), .OPT_OUTREG(OPT_SKID_INPUT)
+			// }}}
+		) awskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(S_AXI_AWVALID[N]), .o_ready(S_AXI_AWREADY[N]),
+			.i_data({ S_AXI_AWADDR[N*AW +: AW], S_AXI_AWPROT[N*3 +: 3] }),
+			.o_valid(skd_awvalid[N]), .i_ready(!skd_awstall[N]),
+				.o_data({ skd_awaddr[N], skd_awprot[N] })
+			// }}}
+		);
+		// }}}
+
+		// write address decoding
+		// {{{
+		addrdecode #(
+			// {{{
+			.AW(AW), .DW(3), .NS(NS),
+			.SLAVE_ADDR(SLAVE_ADDR),
+			.SLAVE_MASK(SLAVE_MASK),
+			.OPT_REGISTERED(OPT_BUFFER_DECODER)
+			// }}}
+		) wraddr(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(skd_awvalid[N]), .o_stall(skd_awstall[N]),
+				.i_addr(skd_awaddr[N]), .i_data(skd_awprot[N]),
+			.o_valid(dcd_awvalid[N]),
+				.i_stall(!dcd_awvalid[N]||!slave_awaccepts[N]),
+				.o_decode(wdecode), .o_addr(m_awaddr[N]),
+				.o_data(m_awprot[N])
+			// }}}
+		);
+		// }}}
+
+		// wskid
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(DW+DW/8), .OPT_OUTREG(OPT_SKID_INPUT)
+			// }}}
+		) wskid (
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(S_AXI_WVALID[N]), .o_ready(S_AXI_WREADY[N]),
+				.i_data({ S_AXI_WDATA[N*DW +: DW],
+						S_AXI_WSTRB[N*DW/8 +: DW/8]}),
+			.o_valid(skd_wvalid[N]),
+				.i_ready(m_wvalid[N] && slave_waccepts[N]),
+				.o_data({ m_wdata[N], m_wstrb[N] })
+			// }}}
+		);
+		// }}}
+
+		// slave_awaccepts
+		// {{{
+		always @(*)
+		begin
+			slave_awaccepts[N] = 1'b1;
+			if (!swgrant[N])
+				slave_awaccepts[N] = 1'b0;
+			if (swfull[N])
+				slave_awaccepts[N] = 1'b0;
+			if (!wrequest[N][swindex[N]])
+				slave_awaccepts[N] = 1'b0;
+			if (!wgrant[N][NS]&&(m_axi_awvalid[swindex[N]] && !m_axi_awready[swindex[N]]))
+				slave_awaccepts[N] = 1'b0;
+			// ERRORs are always accepted
+			//	back pressure is handled in the write side
+		end
+		// }}}
+
+		// slave_waccepts
+		// {{{
+		always @(*)
+		begin
+			slave_waccepts[N] = 1'b1;
+			if (!swgrant[N])
+				slave_waccepts[N] = 1'b0;
+			if (!wdata_expected[N])
+				slave_waccepts[N] = 1'b0;
+			if (!wgrant[N][NS] &&(m_axi_wvalid[swindex[N]]
+						&& !m_axi_wready[swindex[N]]))
+				slave_waccepts[N] = 1'b0;
+			if (wgrant[N][NS]&&(S_AXI_BVALID[N]&& !S_AXI_BREADY[N]))
+				slave_waccepts[N] = 1'b0;
+		end
+		// }}}
+
+		// r_mawvalid, r_mwvalid
+		// {{{
+		always @(*)
+		begin
+			r_mawvalid= dcd_awvalid[N] && !swfull[N];
+			r_mwvalid = skd_wvalid[N];
+			wrequest[N]= 0;
+			if (!swfull[N])
+				wrequest[N][NS:0] = wdecode;
+		end
+
+		assign	m_awvalid[N] = r_mawvalid;
+		assign	m_wvalid[N] = r_mwvalid;
+		// }}}
+
+		// }}}
+	end for (N=NM; N<NMFULL; N=N+1)
+	begin : UNUSED_WSKID_BUFFERS
+		// {{{
+		assign	m_awvalid[N] = 0;
+		assign	m_awaddr[N] = 0;
+		assign	m_awprot[N] = 0;
+		assign	m_wdata[N] = 0;
+		assign	m_wstrb[N] = 0;
+		// }}}
+	end endgenerate
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : DECODE_READ_REQUEST
+		// {{{
+		wire	[NS:0]		rdecode;
+		reg	r_marvalid;
+
+		// arskid
+		// {{{
+		skidbuffer #(
+			// {{{
+			.DW(AW+3), .OPT_OUTREG(OPT_SKID_INPUT)
+			// }}}
+		) arskid(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(S_AXI_ARVALID[N]), .o_ready(S_AXI_ARREADY[N]),
+			.i_data({ S_AXI_ARADDR[N*AW +: AW], S_AXI_ARPROT[N*3 +: 3] }),
+			.o_valid(skd_arvalid[N]), .i_ready(!skd_arstall[N]),
+				.o_data({ skd_araddr[N], skd_arprot[N] })
+			// }}}
+		);
+		// }}}
+
+		// Read address decoding
+		// {{{
+		addrdecode #(
+			// {{{
+			.AW(AW), .DW(3), .NS(NS),
+			.SLAVE_ADDR(SLAVE_ADDR), .SLAVE_MASK(SLAVE_MASK),
+			.OPT_REGISTERED(OPT_BUFFER_DECODER)
+			// }}}
+		) rdaddr(
+			// {{{
+			.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
+			.i_valid(skd_arvalid[N]), .o_stall(skd_arstall[N]),
+				.i_addr(skd_araddr[N]), .i_data(skd_arprot[N]),
+			.o_valid(dcd_arvalid[N]),
+				.i_stall(!m_arvalid[N] || !slave_raccepts[N]),
+				.o_decode(rdecode), .o_addr(m_araddr[N]),
+				.o_data(m_arprot[N])
+			// }}}
+		);
+		// }}}
+
+		// r_marvalid -> m_arvalid[N]
+		// {{{
+		always @(*)
+		begin
+			r_marvalid = dcd_arvalid[N] && !srfull[N];
+			rrequest[N] = 0;
+			if (!srfull[N])
+				rrequest[N][NS:0] = rdecode;
+		end
+
+		assign	m_arvalid[N] = r_marvalid;
+		// }}}
+
+		// slave_raccepts
+		// {{{
+		always @(*)
+		begin
+			slave_raccepts[N] = 1'b1;
+			if (!srgrant[N])
+				slave_raccepts[N] = 1'b0;
+			if (srfull[N])
+				slave_raccepts[N] = 1'b0;
+			// verilator lint_off  WIDTH
+			if (!rrequest[N][srindex[N]])
+				slave_raccepts[N] = 1'b0;
+			// verilator lint_on  WIDTH
+			if (!rgrant[N][NS])
+			begin
+				if (m_axi_arvalid[srindex[N]] && !m_axi_arready[srindex[N]])
+					slave_raccepts[N] = 1'b0;
+			end else if (S_AXI_RVALID[N] && !S_AXI_RREADY[N])
+				slave_raccepts[N] = 1'b0;
+		end
+		// }}}
+
+		// }}}
+	end for (N=NM; N<NMFULL; N=N+1)
+	begin : UNUSED_RSKID_BUFFERS
+		// {{{
+		assign	m_arvalid[N] = 0;
+		assign	m_araddr[N] = 0;
+		assign	m_arprot[N] = 0;
+		// }}}
+	end endgenerate
+
+	// wrequested
+	// {{{
+	always @(*)
+	begin : DECONFLICT_WRITE_REQUESTS
+
+		for(iN=1; iN<NM ; iN=iN+1)
+			wrequested[iN] = 0;
+
+		// Vivado may complain about too many bits for wrequested.
+		// This is (currrently) expected.  swindex is used to index
+		// into wrequested, and swindex has LGNS bits, where LGNS
+		// is $clog2(NS+1) rather than $clog2(NS).  The extra bits
+		// are defined to be zeros, but the point is there are defined.
+		// Therefore, no matter what swindex is, it will always
+		// reference something valid.
+		wrequested[NM] = 0;
+
+		for(iM=0; iM<NS; iM=iM+1)
+		begin
+			wrequested[0][iM] = 1'b0;
+			for(iN=1; iN<NM ; iN=iN+1)
+			begin
+				// Continue to request any channel with
+				// a grant and pending operations
+				if (wrequest[iN-1][iM] && wgrant[iN-1][iM])
+					wrequested[iN][iM] = 1;
+				if (wrequest[iN-1][iM] && (!swgrant[iN-1]||swempty[iN-1]))
+					wrequested[iN][iM] = 1;
+				// Otherwise, if it's already claimed, then
+				// it can't be claimed again
+				if (wrequested[iN-1][iM])
+					wrequested[iN][iM] = 1;
+			end
+			wrequested[NM][iM] = wrequest[NM-1][iM] || wrequested[NM-1][iM];
+		end
+	end
+	// }}}
+
+	// rrequested
+	// {{{
+	always @(*)
+	begin : DECONFLICT_READ_REQUESTS
+
+		for(iN=0; iN<NM ; iN=iN+1)
+			rrequested[iN] = 0;
+
+		// See the note above for wrequested.  This applies to
+		// rrequested as well.
+		rrequested[NM] = 0;
+
+		for(iM=0; iM<NS; iM=iM+1)
+		begin
+			rrequested[0][iM] = 0;
+			for(iN=1; iN<NM ; iN=iN+1)
+			begin
+				// Continue to request any channel with
+				// a grant and pending operations
+				if (rrequest[iN-1][iM] && rgrant[iN-1][iM])
+					rrequested[iN][iM] = 1;
+				if (rrequest[iN-1][iM] && (!srgrant[iN-1] || srempty[iN-1]))
+					rrequested[iN][iM] = 1;
+				// Otherwise, if it's already claimed, then
+				// it can't be claimed again
+				if (rrequested[iN-1][iM])
+					rrequested[iN][iM] = 1;
+			end
+			rrequested[NM][iM] = rrequest[NM-1][iM] || rrequested[NM-1][iM];
+		end
+	end
+	// }}}
+
+	// mwgrant, mrgrant
+	// {{{
+	generate for(M=0; M<NS; M=M+1)
+	begin : GEN_GRANT
+		// {{{
+		initial	mwgrant[M] = 0;
+		always @(*)
+		begin
+			mwgrant[M] = 0;
+			for(iN=0; iN<NM; iN=iN+1)
+			if (wgrant[iN][M])
+				mwgrant[M] = 1;
+		end
+
+		always @(*)
+		begin
+			mrgrant[M] = 0;
+			for(iN=0; iN<NM; iN=iN+1)
+			if (rgrant[iN][M])
+				mrgrant[M] = 1;
+		end
+		// }}}
+	end endgenerate
+	// }}}
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : ARBITRATE_WRITE_REQUESTS
+		// {{{
+		// Declarations
+		// {{{
+		reg			stay_on_channel;
+		reg			requested_channel_is_available;
+		reg			leave_channel;
+		reg	[LGNS-1:0]	requested_index;
+		wire			linger;
+		// }}}
+
+		// stay_on_channel
+		// {{{
+		always @(*)
+		begin
+			stay_on_channel = |(wrequest[N][NS:0] & wgrant[N]);
+
+			if (swgrant[N] && !swempty[N])
+				stay_on_channel = 1;
+		end
+		// }}}
+
+		// requested_channel_is_available
+		// {{{
+		always @(*)
+		begin
+			requested_channel_is_available =
+				|(wrequest[N][NS-1:0] & ~mwgrant
+						& ~wrequested[N][NS-1:0]);
+			if (wrequest[N][NS])
+				requested_channel_is_available = 1;
+
+			if (NM < 2)
+				requested_channel_is_available = m_awvalid[N];
+		end
+		// }}}
+
+		if (OPT_LINGER == 0)
+		begin : NO_LINGER
+			// {{{
+			assign	linger = 0;
+			// }}}
+		end else begin : WRITE_LINGER
+			// {{{
+			reg [LGLINGER-1:0]	linger_counter;
+			reg			r_linger;
+
+			initial	r_linger = 0;
+			initial	linger_counter = 0;
+			always @(posedge S_AXI_ACLK)
+			if (!S_AXI_ARESETN || wgrant[N][NS])
+			begin
+				r_linger <= 0;
+				linger_counter <= 0;
+			end else if (!swempty[N] || S_AXI_BVALID[N])
+			begin
+				linger_counter <= OPT_LINGER;
+				r_linger <= 1;
+			end else if (linger_counter > 0)
+			begin
+				r_linger <= (linger_counter > 1);
+				linger_counter <= linger_counter - 1;
+			end else
+				r_linger <= 0;
+
+			assign	linger = r_linger;
+
+`ifdef	FORMAL
+		// {{{
+			always @(*)
+				assert(linger == (linger_counter != 0));
+		// }}}
+`endif
+			// }}}
+		end
+
+		// leave_channel
+		// {{{
+		always @(*)
+		begin
+			leave_channel = 0;
+			if (!m_awvalid[N]
+				&& (!linger || wrequested[NM][swindex[N]]))
+				// Leave the channel after OPT_LINGER counts
+				// of the channel being idle, or when someone
+				// else asks for the channel
+				leave_channel = 1;
+			if (m_awvalid[N] && !wrequest[N][swindex[N]])
+				// Need to leave this channel to connect
+				// to any other channel
+				leave_channel = 1;
+		end
+		// }}}
+
+		// wgrant, swgrant
+		// {{{
+		initial	wgrant[N]  = 0;
+		initial	swgrant[N] = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+		begin
+			wgrant[N]  <= 0;
+			swgrant[N] <= 0;
+		end else if (!stay_on_channel)
+		begin
+			if (requested_channel_is_available)
+			begin
+				// Switching channels
+				swgrant[N] <= 1'b1;
+				wgrant[N]  <= wrequest[N][NS:0];
+			end else if (leave_channel)
+			begin
+				swgrant[N] <= 1'b0;
+				wgrant[N]  <= 0;
+			end
+		end
+		// }}}
+
+		// requested_index
+		// {{{
+		always @(wrequest[N])
+		begin
+			requested_index = 0;
+			for(iM=0; iM<=NS; iM=iM+1)
+			if (wrequest[N][iM])
+				requested_index= requested_index | iM[LGNS-1:0];
+		end
+		// }}}
+
+		// Now for swindex
+		// {{{
+		reg	[LGNS-1:0]	r_swindex;
+
+		initial	r_swindex = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!stay_on_channel && requested_channel_is_available)
+			r_swindex <= requested_index;
+
+		assign	swindex[N] = r_swindex;
+		// }}}
+		// }}}
+	end for (N=NM; N<NMFULL; N=N+1)
+	begin : EMPTY_WRITE_REQUEST
+		// {{{
+		assign	swindex[N] = 0;
+		// }}}
+	end endgenerate
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : ARBITRATE_READ_REQUESTS
+		// {{{
+		// Declarations
+		// {{{
+		reg			stay_on_channel;
+		reg			requested_channel_is_available;
+		reg			leave_channel;
+		reg	[LGNS-1:0]	requested_index;
+		wire			linger;
+		// }}}
+
+		// stay_on_channel
+		// {{{
+		always @(*)
+		begin
+			stay_on_channel = |(rrequest[N][NS:0] & rgrant[N]);
+
+			if (srgrant[N] && !srempty[N])
+				stay_on_channel = 1;
+		end
+		// }}}
+
+		// requested_channel_is_available
+		// {{{
+		always @(*)
+		begin
+			requested_channel_is_available =
+				|(rrequest[N][NS-1:0] & ~mrgrant
+						& ~rrequested[N][NS-1:0]);
+			if (rrequest[N][NS])
+				requested_channel_is_available = 1;
+
+			if (NM < 2)
+				requested_channel_is_available = m_arvalid[N];
+		end
+		// }}}
+
+		if (OPT_LINGER == 0)
+		begin : NO_LINGER
+			// {{{
+			assign	linger = 0;
+			// }}}
+		end else begin : READ_LINGER
+			// {{{
+			reg [LGLINGER-1:0]	linger_counter;
+			reg			r_linger;
+
+			initial	r_linger = 0;
+			initial	linger_counter = 0;
+			always @(posedge S_AXI_ACLK)
+			if (!S_AXI_ARESETN || rgrant[N][NS])
+			begin
+				r_linger <= 0;
+				linger_counter <= 0;
+			end else if (!srempty[N] || S_AXI_RVALID[N])
+			begin
+				linger_counter <= OPT_LINGER;
+				r_linger <= 1;
+			end else if (linger_counter > 0)
+			begin
+				r_linger <= (linger_counter > 1);
+				linger_counter <= linger_counter - 1;
+			end else
+				r_linger <= 0;
+
+			assign	linger = r_linger;
+`ifdef	FORMAL
+			// {{{
+			always @(*)
+				assert(linger == (linger_counter != 0));
+			// }}}
+`endif
+			// }}}
+		end
+
+		// leave_channel
+		// {{{
+		always @(*)
+		begin
+			leave_channel = 0;
+			if (!m_arvalid[N]
+				&& (!linger || rrequested[NM][srindex[N]]))
+				// Leave the channel after OPT_LINGER counts
+				// of the channel being idle, or when someone
+				// else asks for the channel
+				leave_channel = 1;
+			if (m_arvalid[N] && !rrequest[N][srindex[N]])
+				// Need to leave this channel to connect
+				// to any other channel
+				leave_channel = 1;
+		end
+		// }}}
+
+		// rgrant, srgrant
+		// {{{
+		initial	rgrant[N]  = 0;
+		initial	srgrant[N] = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+		begin
+			rgrant[N]  <= 0;
+			srgrant[N] <= 0;
+		end else if (!stay_on_channel)
+		begin
+			if (requested_channel_is_available)
+			begin
+				// Switching channels
+				srgrant[N] <= 1'b1;
+				rgrant[N] <= rrequest[N][NS:0];
+			end else if (leave_channel)
+			begin
+				srgrant[N] <= 1'b0;
+				rgrant[N]  <= 0;
+			end
+		end
+		// }}}
+
+		// requested_index
+		// {{{
+		always @(rrequest[N])
+		begin
+			requested_index = 0;
+			for(iM=0; iM<=NS; iM=iM+1)
+			if (rrequest[N][iM])
+				requested_index = requested_index|iM[LGNS-1:0];
+		end
+		// }}}
+
+		// Now for srindex
+		// {{{
+		reg	[LGNS-1:0]	r_srindex;
+
+		initial	r_srindex = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!stay_on_channel && requested_channel_is_available)
+			r_srindex <= requested_index;
+
+		assign	srindex[N] = r_srindex;
+		// }}}
+		// }}}
+	end for (N=NM; N<NMFULL; N=N+1)
+	begin : EMPTY_READ_REQUEST
+		// {{{
+		assign	srindex[N] = 0;
+		// }}}
+	end endgenerate
+
+	// Calculate mwindex
+	generate for (M=0; M<NS; M=M+1)
+	begin : SLAVE_WRITE_INDEX
+		// {{{
+		if (NM <= 1)
+		begin : ONE_MASTER
+			// {{{
+			assign mwindex[M] = 0;
+			// }}}
+		end else begin : MULTIPLE_MASTERS
+			// {{{
+			reg [LGNM-1:0]		reswindex;
+			reg	[LGNM-1:0]	r_mwindex;
+
+			always @(*)
+			begin
+				reswindex = 0;
+			for(iN=0; iN<NM; iN=iN+1)
+			if ((!swgrant[iN] || swempty[iN])
+				&&(wrequest[iN][M] && !wrequested[iN][M]))
+					reswindex = reswindex | iN[LGNM-1:0];
+			end
+
+			always @(posedge S_AXI_ACLK)
+			if (!mwgrant[M])
+				r_mwindex <= reswindex;
+
+			assign	mwindex[M] = r_mwindex;
+			// }}}
+		end
+		// }}}
+	end for (M=NS; M<NSFULL; M=M+1)
+	begin : NO_WRITE_INDEX
+		// {{{
+		assign	mwindex[M] = 0;
+		// }}}
+	end endgenerate
+
+	// Calculate mrindex
+	generate for (M=0; M<NS; M=M+1)
+	begin : SLAVE_READ_INDEX
+		// {{{
+		if (NM <= 1)
+		begin : ONE_MASTER
+			// {{{
+			assign mrindex[M] = 0;
+			// }}}
+		end else begin : MULTIPLE_MASTERS
+			// {{{
+			reg [LGNM-1:0]	resrindex;
+			reg [LGNM-1:0]	r_mrindex;
+
+			always @(*)
+			begin
+				resrindex = 0;
+			for(iN=0; iN<NM; iN=iN+1)
+			if ((!srgrant[iN] || srempty[iN])
+				&&(rrequest[iN][M] && !rrequested[iN][M]))
+					resrindex = resrindex | iN[LGNM-1:0];
+			end
+
+			always @(posedge S_AXI_ACLK)
+			if (!mrgrant[M])
+				r_mrindex <= resrindex;
+
+			assign	mrindex[M] = r_mrindex;
+			// }}}
+		end
+		// }}}
+	end for (M=NS; M<NSFULL; M=M+1)
+	begin : NO_READ_INDEX
+		// {{{
+		assign	mrindex[M] = 0;
+		// }}}
+	end endgenerate
+
+	// Assign outputs to the various slaves
+	generate for(M=0; M<NS; M=M+1)
+	begin : WRITE_SLAVE_OUTPUTS
+		// {{{
+
+		// Declarations
+		// {{{
+		reg			axi_awvalid;
+		reg	[AW-1:0]	axi_awaddr;
+		reg	[2:0]		axi_awprot;
+
+		reg			axi_wvalid;
+		reg	[DW-1:0]	axi_wdata;
+		reg	[DW/8-1:0]	axi_wstrb;
+		//
+		reg			axi_bready;
+
+		wire	sawstall, swstall, mbstall;
+		// }}}
+		assign	sawstall= (M_AXI_AWVALID[M]&& !M_AXI_AWREADY[M]);
+		assign	swstall = (M_AXI_WVALID[M] && !M_AXI_WREADY[M]);
+		assign	mbstall = (S_AXI_BVALID[mwindex[M]] && !S_AXI_BREADY[mwindex[M]]);
+
+		// axi_awvalid
+		// {{{
+		initial	axi_awvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN || !mwgrant[M])
+			axi_awvalid <= 0;
+		else if (!sawstall)
+		begin
+			axi_awvalid <= m_awvalid[mwindex[M]]
+				&&(slave_awaccepts[mwindex[M]]);
+		end
+		// }}}
+
+		// axi_awaddr, axi_awprot
+		// {{{
+		initial	axi_awaddr  = 0;
+		initial	axi_awprot  = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+		begin
+			axi_awaddr  <= 0;
+			axi_awprot  <= 0;
+		end else if (OPT_LOWPOWER && !mwgrant[M])
+		begin
+			axi_awaddr  <= 0;
+			axi_awprot  <= 0;
+		end else if (!sawstall)
+		begin
+			if (!OPT_LOWPOWER||(m_awvalid[mwindex[M]]&&slave_awaccepts[mwindex[M]]))
+			begin
+				axi_awaddr  <= m_awaddr[mwindex[M]];
+				axi_awprot  <= m_awprot[mwindex[M]];
+			end else begin
+				axi_awaddr  <= 0;
+				axi_awprot  <= 0;
+			end
+		end
+		// }}}
+
+		// axi_wvalid
+		// {{{
+		initial	axi_wvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN || !mwgrant[M])
+			axi_wvalid <= 0;
+		else if (!swstall)
+		begin
+			axi_wvalid <= (m_wvalid[mwindex[M]])
+					&&(slave_waccepts[mwindex[M]]);
+		end
+		// }}}
+
+		// axi_wdata, axi_wstrb
+		// {{{
+		initial axi_wdata  = 0;
+		initial axi_wstrb  = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+		begin
+			axi_wdata  <= 0;
+			axi_wstrb  <= 0;
+		end else if (OPT_LOWPOWER && !mwgrant[M])
+		begin
+			axi_wdata  <= 0;
+			axi_wstrb  <= 0;
+		end else if (!swstall)
+		begin
+			if (!OPT_LOWPOWER || (m_wvalid[mwindex[M]]&&slave_waccepts[mwindex[M]]))
+			begin
+				axi_wdata  <= m_wdata[mwindex[M]];
+				axi_wstrb  <= m_wstrb[mwindex[M]];
+			end else begin
+				axi_wdata  <= 0;
+				axi_wstrb  <= 0;
+			end
+		end
+		// }}}
+
+		// axi_bready
+		// {{{
+		initial	axi_bready = 1;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN || !mwgrant[M])
+			axi_bready <= 1;
+		else if (!mbstall)
+			axi_bready <= 1;
+		else if (M_AXI_BVALID[M]) // && mbstall
+			axi_bready <= 0;
+		// }}}
+
+		//
+		assign	M_AXI_AWVALID[M]         = axi_awvalid;
+		assign	M_AXI_AWADDR[M*AW +: AW] = axi_awaddr;
+		assign	M_AXI_AWPROT[M*3 +: 3]   = axi_awprot;
+		//
+		//
+		assign	M_AXI_WVALID[M]             = axi_wvalid;
+		assign	M_AXI_WDATA[M*DW +: DW]     = axi_wdata;
+		assign	M_AXI_WSTRB[M*DW/8 +: DW/8] = axi_wstrb;
+		//
+		//
+		assign	M_AXI_BREADY[M]             = axi_bready;
+		//
+`ifdef	FORMAL
+		// {{{
+		if (OPT_LOWPOWER)
+		begin
+			always @(*)
+			if (!axi_awvalid)
+			begin
+				assert(axi_awaddr == 0);
+				assert(axi_awprot == 0);
+			end
+
+			always @(*)
+			if (!axi_wvalid)
+			begin
+				assert(axi_wdata == 0);
+				assert(axi_wstrb == 0);
+			end
+		end
+		// }}}
+`endif
+		// }}}
+	end endgenerate
+
+
+	generate for(M=0; M<NS; M=M+1)
+	begin : READ_SLAVE_OUTPUTS
+		// {{{
+		// Declarations
+		// {{{
+		reg				axi_arvalid;
+		reg	[C_AXI_ADDR_WIDTH-1:0]	axi_araddr;
+		reg	[2:0]			axi_arprot;
+		//
+		reg				axi_rready;
+
+		wire	arstall, srstall;
+		// }}}
+		assign	arstall= (M_AXI_ARVALID[M]&& !M_AXI_ARREADY[M]);
+		assign	srstall = (S_AXI_RVALID[mrindex[M]]
+						&& !S_AXI_RREADY[mrindex[M]]);
+
+		// axi_arvalid
+		// {{{
+		initial	axi_arvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN || !mrgrant[M])
+			axi_arvalid <= 0;
+		else if (!arstall)
+		begin
+			axi_arvalid <= m_arvalid[mrindex[M]] && slave_raccepts[mrindex[M]];
+		end
+		// }}}
+
+		// axi_araddr, axi_arprot
+		// {{{
+		initial	axi_araddr  = 0;
+		initial	axi_arprot  = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+		begin
+			axi_araddr  <= 0;
+			axi_arprot  <= 0;
+		end else if (OPT_LOWPOWER && !mrgrant[M])
+		begin
+			axi_araddr  <= 0;
+			axi_arprot  <= 0;
+		end else if (!arstall)
+		begin
+			if (!OPT_LOWPOWER || (m_arvalid[mrindex[M]] && slave_raccepts[mrindex[M]]))
+			begin
+				if (NM == 1)
+				begin
+					axi_araddr  <= m_araddr[0];
+					axi_arprot  <= m_arprot[0];
+				end else begin
+					axi_araddr  <= m_araddr[mrindex[M]];
+					axi_arprot  <= m_arprot[mrindex[M]];
+				end
+			end else begin
+				axi_araddr  <= 0;
+				axi_arprot  <= 0;
+			end
+		end
+		// }}}
+
+		// axi_rready
+		// {{{
+		initial	axi_rready = 1;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN || !mrgrant[M])
+			axi_rready <= 1;
+		else if (!srstall)
+			axi_rready <= 1;
+		else if (M_AXI_RVALID[M] && M_AXI_RREADY[M]) // && srstall
+			axi_rready <= 0;
+		// }}}
+
+		//
+		assign	M_AXI_ARVALID[M]         = axi_arvalid;
+		assign	M_AXI_ARADDR[M*AW +: AW] = axi_araddr;
+		assign	M_AXI_ARPROT[M*3 +: 3]   = axi_arprot;
+		//
+		assign	M_AXI_RREADY[M]          = axi_rready;
+		//
+`ifdef	FORMAL
+		// {{{
+		if (OPT_LOWPOWER)
+		begin
+			always @(*)
+			if (!axi_arvalid)
+			begin
+				assert(axi_araddr == 0);
+				assert(axi_arprot == 0);
+			end
+		end
+		// }}}
+`endif
+	// }}}
+	end endgenerate
+
+	// Return values
+	generate for (N=0; N<NM; N=N+1)
+	begin : WRITE_RETURN_CHANNEL
+		// {{{
+		reg		axi_bvalid;
+		reg	[1:0]	axi_bresp;
+		reg		i_axi_bvalid;
+		wire	[1:0]	i_axi_bresp;
+		wire		mbstall;
+
+		initial	i_axi_bvalid = 1'b0;
+		always @(*)
+		if (wgrant[N][NS])
+			i_axi_bvalid = m_wvalid[N] && slave_waccepts[N];
+		else
+			i_axi_bvalid = m_axi_bvalid[swindex[N]];
+
+		assign	i_axi_bresp = m_axi_bresp[swindex[N]];
+
+		assign	mbstall = S_AXI_BVALID[N] && !S_AXI_BREADY[N];
+
+		// r_bvalid
+		// {{{
+		initial	r_bvalid[N] = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			r_bvalid[N] <= 0;
+		else if (mbstall && !r_bvalid[N] && !wgrant[N][NS])
+			r_bvalid[N] <= swgrant[N] && i_axi_bvalid;
+		else if (!mbstall)
+			r_bvalid[N] <= 1'b0;
+		// }}}
+
+		// r_bresp
+		// {{{
+		initial	r_bresp[N] = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+			r_bresp[N] <= 0;
+		else if (OPT_LOWPOWER && (!swgrant[N] || S_AXI_BREADY[N]))
+			r_bresp[N] <= 0;
+		else if (!r_bvalid[N])
+		begin
+			if (!OPT_LOWPOWER ||(i_axi_bvalid && !wgrant[N][NS] && mbstall))
+			begin
+				r_bresp[N] <= i_axi_bresp;
+			end else
+				r_bresp[N] <= 0;
+		end
+		// }}}
+
+		// axi_bvalid
+		// {{{
+		initial	axi_bvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			axi_bvalid <= 0;
+		else if (!mbstall)
+			axi_bvalid <= swgrant[N] && (r_bvalid[N] || i_axi_bvalid);
+		// }}}
+
+		// axi_bresp
+		// {{{
+		initial	axi_bresp = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+			axi_bresp <= 0;
+		else if (OPT_LOWPOWER && !swgrant[N])
+			axi_bresp <= 0;
+		else if (!mbstall)
+		begin
+			if (r_bvalid[N])
+				axi_bresp <= r_bresp[N];
+			else if (!OPT_LOWPOWER || i_axi_bvalid)
+				axi_bresp <= i_axi_bresp;
+			else
+				axi_bresp <= 0;
+
+			if (wgrant[N][NS] && (!OPT_LOWPOWER || i_axi_bvalid))
+				axi_bresp <= INTERCONNECT_ERROR;
+		end
+		// }}}
+
+		//
+		assign	S_AXI_BVALID[N]       = axi_bvalid;
+		assign	S_AXI_BRESP[N*2 +: 2] = axi_bresp;
+`ifdef	FORMAL
+		// {{{
+		always @(*)
+		if (r_bvalid[N])
+			assert(r_bresp[N] != 2'b01);
+		always @(*)
+		if (swgrant[N])
+			assert(m_axi_bready[swindex[N]] == !r_bvalid[N]);
+		else
+			assert(!r_bvalid[N]);
+		always @(*)
+		if (OPT_LOWPOWER && !r_bvalid[N])
+			assert(r_bresp[N]  == 0);
+
+		always @(*)
+		if (OPT_LOWPOWER && !axi_bvalid)
+			assert(axi_bresp  == 0);
+		// }}}
+`endif
+		// }}}
+	end endgenerate
+
+	// m_axi_?r* values
+	// {{{
+	always @(*)
+	begin
+		m_axi_arvalid = 0;
+		m_axi_arready = 0;
+		m_axi_rvalid = 0;
+		m_axi_rready = 0;
+
+		m_axi_arvalid[NS-1:0] = M_AXI_ARVALID;
+		m_axi_arready[NS-1:0] = M_AXI_ARREADY;
+		m_axi_rvalid[NS-1:0]  = M_AXI_RVALID;
+		m_axi_rready[NS-1:0]  = M_AXI_RREADY;
+	end
+	// }}}
+
+	// Return values
+	generate for (N=0; N<NM; N=N+1)
+	begin : READ_RETURN_CHANNEL
+		// {{{
+		reg			axi_rvalid;
+		reg	[1:0]		axi_rresp;
+		reg	[DW-1:0]	axi_rdata;
+		wire			srstall;
+		reg			i_axi_rvalid;
+
+		initial	i_axi_rvalid = 1'b0;
+		always @(*)
+		if (rgrant[N][NS])
+			i_axi_rvalid = m_arvalid[N] && slave_raccepts[N];
+		else
+			i_axi_rvalid = m_axi_rvalid[srindex[N]];
+
+		assign	srstall = S_AXI_RVALID[N] && !S_AXI_RREADY[N];
+
+		initial	r_rvalid[N] = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			r_rvalid[N] <= 0;
+		else if (srstall && !r_rvalid[N])
+			r_rvalid[N] <= srgrant[N] && !rgrant[N][NS]&&i_axi_rvalid;
+		else if (!srstall)
+			r_rvalid[N] <= 0;
+
+		initial	r_rresp[N] = 0;
+		initial	r_rdata[N] = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+		begin
+			r_rresp[N] <= 0;
+			r_rdata[N] <= 0;
+		end else if (OPT_LOWPOWER && (!srgrant[N] || S_AXI_RREADY[N]))
+		begin
+			r_rresp[N] <= 0;
+			r_rdata[N] <= 0;
+		end else if (!r_rvalid[N])
+		begin
+			if (!OPT_LOWPOWER || (i_axi_rvalid && !rgrant[N][NS] && srstall))
+			begin
+				if (NS == 1)
+				begin
+					r_rresp[N] <= m_axi_rresp[0];
+					r_rdata[N] <= m_axi_rdata[0];
+				end else begin
+					r_rresp[N] <= m_axi_rresp[srindex[N]];
+					r_rdata[N] <= m_axi_rdata[srindex[N]];
+				end
+			end else begin
+				r_rresp[N] <= 0;
+				r_rdata[N] <= 0;
+			end
+		end
+
+		initial	axi_rvalid = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			axi_rvalid <= 0;
+		else if (!srstall)
+			axi_rvalid <= srgrant[N] && (r_rvalid[N] || i_axi_rvalid);
+
+		initial	axi_rresp = 0;
+		initial	axi_rdata = 0;
+		always @(posedge S_AXI_ACLK)
+		if (OPT_LOWPOWER && !S_AXI_ARESETN)
+		begin
+			axi_rresp <= 0;
+			axi_rdata <= 0;
+		end else if (OPT_LOWPOWER && !srgrant[N])
+		begin
+			axi_rresp <= 0;
+			axi_rdata <= 0;
+		end else if (!srstall)
+		begin
+			if (r_rvalid[N])
+			begin
+				axi_rresp <= r_rresp[N];
+				axi_rdata <= r_rdata[N];
+			end else if (!OPT_LOWPOWER || i_axi_rvalid)
+			begin
+				if (NS == 1)
+				begin
+					axi_rresp <= m_axi_rresp[0];
+					axi_rdata <= m_axi_rdata[0];
+				end else begin
+					axi_rresp <= m_axi_rresp[srindex[N]];
+					axi_rdata <= m_axi_rdata[srindex[N]];
+				end
+
+				if (rgrant[N][NS])
+					axi_rresp <= INTERCONNECT_ERROR;
+			end else begin
+				axi_rresp <= 0;
+				axi_rdata <= 0;
+			end
+		end
+
+		assign	S_AXI_RVALID[N]        = axi_rvalid;
+		assign	S_AXI_RRESP[N*2  +: 2] = axi_rresp;
+		assign	S_AXI_RDATA[N*DW +: DW]= axi_rdata;
+`ifdef	FORMAL
+		// {{{
+		always @(*)
+		if (r_rvalid[N])
+			assert(r_rresp[N] != 2'b01);
+		always @(*)
+		if (srgrant[N] && !rgrant[N][NS])
+			assert(m_axi_rready[srindex[N]] == !r_rvalid[N]);
+		else
+			assert(!r_rvalid[N]);
+		always @(*)
+		if (OPT_LOWPOWER && !r_rvalid[N])
+		begin
+			assert(r_rresp[N] == 0);
+			assert(r_rdata[N] == 0);
+		end
+
+		always @(*)
+		if (OPT_LOWPOWER && !axi_rvalid)
+		begin
+			assert(axi_rresp == 0);
+			assert(axi_rdata == 0);
+		end
+		// }}}
+`endif
+		// }}}
+	end endgenerate
+
+	// Count pending transactions
+	generate for (N=0; N<NM; N=N+1)
+	begin : COUNT_PENDING
+		// {{{
+		reg	[LGMAXBURST-1:0]	awpending, rpending,
+						missing_wdata;
+		//reg				rempty, awempty; // wempty;
+		reg	r_wdata_expected;
+
+		initial	awpending    = 0;
+		initial	swempty[N]   = 1;
+		initial	swfull[N]    = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+		begin
+			awpending     <= 0;
+			swempty[N]    <= 1;
+			swfull[N]     <= 0;
+		end else case ({(m_awvalid[N] && slave_awaccepts[N]),
+				(S_AXI_BVALID[N] && S_AXI_BREADY[N])})
+		2'b01: begin
+			awpending     <= awpending - 1;
+			swempty[N]    <= (awpending <= 1);
+			swfull[N]     <= 0;
+			end
+		2'b10: begin
+			awpending <= awpending + 1;
+			swempty[N] <= 0;
+			swfull[N]     <= &awpending[LGMAXBURST-1:1];
+			end
+		default: begin end
+		endcase
+
+		initial	missing_wdata = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			missing_wdata <= 0;
+		else begin
+			missing_wdata <= missing_wdata
+				+((m_awvalid[N] && slave_awaccepts[N])? 1:0)
+				-((m_wvalid[N] && slave_waccepts[N])? 1:0);
+		end
+
+		initial	r_wdata_expected = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			r_wdata_expected <= 0;
+		else case({ m_awvalid[N] && slave_awaccepts[N],
+				m_wvalid[N] && slave_waccepts[N] })
+		2'b10: r_wdata_expected <= 1;
+		2'b01: r_wdata_expected <= (missing_wdata > 1);
+		default: begin end
+		endcase
+
+
+		initial	rpending     = 0;
+		initial	srempty[N]   = 1;
+		initial	srfull[N]    = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+		begin
+			rpending  <= 0;
+			srempty[N]<= 1;
+			srfull[N] <= 0;
+		end else case ({(m_arvalid[N] && slave_raccepts[N]),
+				(S_AXI_RVALID[N] && S_AXI_RREADY[N])})
+		2'b01: begin
+			rpending      <= rpending - 1;
+			srempty[N]    <= (rpending == 1);
+			srfull[N]     <= 0;
+			end
+		2'b10: begin
+			rpending      <= rpending + 1;
+			srfull[N]     <= &rpending[LGMAXBURST-1:1];
+			srempty[N]    <= 0;
+			end
+		default: begin end
+		endcase
+
+		assign	w_sawpending[N] = awpending;
+		assign	w_srpending[N]  = rpending;
+
+		assign	wdata_expected[N] = r_wdata_expected;
+
+`ifdef	FORMAL
+		// {{{
+		reg	[LGMAXBURST-1:0]	wpending;
+		reg	[LGMAXBURST-1:0]	f_missing_wdata;
+
+		initial	wpending = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			wpending <= 0;
+		else case ({(m_wvalid[N] && slave_waccepts[N]),
+				(S_AXI_BVALID[N] && S_AXI_BREADY[N])})
+		2'b01: wpending <= wpending - 1;
+		2'b10: wpending <= wpending + 1;
+		default: begin end
+		endcase
+
+		assign	w_swpending[N]  = wpending;
+
+		always @(*)
+			assert(missing_wdata == awpending - wpending);
+		always @(*)
+			assert(r_wdata_expected == (missing_wdata > 0));
+		always @(*)
+			assert(awpending >= wpending);
+		// }}}
+`endif
+		// }}}
+	end endgenerate
+
+	// Property validation
+	// {{{
+	initial begin
+		if (NM == 0) begin
+                        $display("At least one master must be defined");
+                        $stop;
+                end
+
+		if (NS == 0) begin
+                        $display("At least one slave must be defined");
+                        $stop;
+                end
+        end
+	// }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal properties used to verify this core
+// {{{
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+	// Local declarations
+	// {{{
+	localparam	F_LGDEPTH = LGMAXBURST+1;
+	wire	[F_LGDEPTH-1:0]	fm_rd_outstanding	[0:NM-1];
+	wire	[F_LGDEPTH-1:0]	fm_wr_outstanding	[0:NM-1];
+	wire	[F_LGDEPTH-1:0]	fm_awr_outstanding	[0:NM-1];
+
+	wire	[F_LGDEPTH-1:0]	fs_rd_outstanding	[0:NS-1];
+	wire	[F_LGDEPTH-1:0]	fs_wr_outstanding	[0:NS-1];
+	wire	[F_LGDEPTH-1:0]	fs_awr_outstanding	[0:NS-1];
+
+	initial	assert(NS >= 1);
+	initial	assert(NM >= 1);
+	// }}}
+
+`ifdef	VERIFIC
+	reg	f_past_valid;
+
+	initial	f_past_valid = 0;
+	always @(posedge S_AXI_ACLK)
+		f_past_valid <= 1;
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Initial value checks
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+`ifdef	VERIFIC
+`define	INITIAL_CHECK	assume
+`else
+`define	INITIAL_CHECK	assert
+`endif // VERIFIC
+	always @(*)
+	if (!f_past_valid)
+	begin
+		`INITIAL_CHECK(!S_AXI_ARESETN);
+		`INITIAL_CHECK(S_AXI_BVALID == 0);
+		`INITIAL_CHECK(S_AXI_RVALID == 0);
+		`INITIAL_CHECK(swgrant == 0);
+		`INITIAL_CHECK(srgrant == 0);
+		`INITIAL_CHECK(swfull == 0);
+		`INITIAL_CHECK(srfull == 0);
+		`INITIAL_CHECK(&swempty);
+		`INITIAL_CHECK(&srempty);
+		for(iN=0; iN<NM; iN=iN+1)
+		begin
+			`INITIAL_CHECK(wgrant[iN] == 0);
+			assume(swindex[iN] == 0);
+
+			`INITIAL_CHECK(rgrant[iN] == 0);
+			assume(srindex[iN] == 0);
+
+			`INITIAL_CHECK(r_bvalid[iN] == 0);
+			`INITIAL_CHECK(r_rvalid[iN] == 0);
+			//
+			`INITIAL_CHECK(r_bresp[iN]  == 0);
+			//
+			`INITIAL_CHECK(r_rresp[iN]  == 0);
+			`INITIAL_CHECK(r_rdata[iN]  == 0);
+		end
+
+		`INITIAL_CHECK(M_AXI_AWVALID == 0);
+		`INITIAL_CHECK(M_AXI_WVALID == 0);
+		`INITIAL_CHECK(M_AXI_RVALID == 0);
+	end
+`endif
+	// }}}
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : CHECK_MASTER_GRANTS
+		// {{{
+
+		////////////////////////////////////////////////////////////////
+		// Write grant checks
+		// {{{
+		always @(*)
+		for(iM=0; iM<=NS; iM=iM+1)
+		begin
+			if (wgrant[N][iM])
+			begin
+				assert((wgrant[N] ^ (1<<iM))==0);
+				assert(swgrant[N]);
+				assert(swindex[N] == iM);
+				if (iM < NS)
+				begin
+					assert(mwgrant[iM]);
+					assert(mwindex[iM] == N);
+				end
+			end
+		end
+
+		always @(*)
+		if (swgrant[N])
+			assert(wgrant[N] != 0);
+
+		always @(*)
+		if (wrequest[N][NS])
+			assert(wrequest[N][NS-1:0] == 0);
+
+		// }}}
+		////////////////////////////////////////////////////////////////
+		//
+		// Read grant checking
+		// {{{
+		always @(*)
+		for(iM=0; iM<=NS; iM=iM+1)
+		begin
+			if (rgrant[N][iM])
+			begin
+				assert((rgrant[N] ^ (1<<iM))==0);
+				assert(srgrant[N]);
+				assert(srindex[N] == iM);
+				if (iM < NS)
+				begin
+					assert(mrgrant[iM]);
+					assert(mrindex[iM] == N);
+				end
+			end
+		end
+
+		always @(*)
+		if (srgrant[N])
+			assert(rgrant[N] != 0);
+
+		always @(*)
+		if (rrequest[N][NS])
+			assert(rrequest[N][NS-1:0] == 0);
+		// }}}
+		// }}}
+	end endgenerate
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : CHECK_MASTERS
+		// {{{
+		faxil_slave #(
+			.C_AXI_DATA_WIDTH(DW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.F_OPT_ASSUME_RESET(1'b1),
+			.F_AXI_MAXWAIT(0),
+			.F_AXI_MAXDELAY(0),
+			.F_LGDEPTH(F_LGDEPTH))
+		  mstri(.i_clk(S_AXI_ACLK),
+			.i_axi_reset_n(S_AXI_ARESETN),
+			//
+			.i_axi_awvalid(S_AXI_AWVALID[N]),
+			.i_axi_awready(S_AXI_AWREADY[N]),
+			.i_axi_awaddr(S_AXI_AWADDR[N*AW +: AW]),
+			.i_axi_awprot(S_AXI_AWPROT[N*3 +: 3]),
+			//
+			.i_axi_wvalid(S_AXI_WVALID[N]),
+			.i_axi_wready(S_AXI_WREADY[N]),
+			.i_axi_wdata( S_AXI_WDATA[N*DW +: DW]),
+			.i_axi_wstrb( S_AXI_WSTRB[N*DW/8 +: DW/8]),
+			//
+			.i_axi_bvalid(S_AXI_BVALID[N]),
+			.i_axi_bready(S_AXI_BREADY[N]),
+			.i_axi_bresp( S_AXI_BRESP[N*2 +: 2]),
+			//
+			.i_axi_arvalid(S_AXI_ARVALID[N]),
+			.i_axi_arready(S_AXI_ARREADY[N]),
+			.i_axi_araddr( S_AXI_ARADDR[N*AW +: AW]),
+			.i_axi_arprot( S_AXI_ARPROT[N*3 +: 3]),
+			//
+			//
+			.i_axi_rvalid(S_AXI_RVALID[N]),
+			.i_axi_rready(S_AXI_RREADY[N]),
+			.i_axi_rdata( S_AXI_RDATA[N*DW +: DW]),
+			.i_axi_rresp( S_AXI_RRESP[N*2 +: 2]),
+			//
+			.f_axi_rd_outstanding( fm_rd_outstanding[N]),
+			.f_axi_wr_outstanding( fm_wr_outstanding[N]),
+			.f_axi_awr_outstanding(fm_awr_outstanding[N]));
+
+		//
+		// Check write counters
+		//
+		always @(*)
+		if (S_AXI_ARESETN)
+		assert(fm_awr_outstanding[N] == { 1'b0, w_sawpending[N] }
+				+((OPT_BUFFER_DECODER & dcd_awvalid[N]) ? 1:0)
+				+ (S_AXI_AWREADY[N] ? 0:1));
+
+		always @(*)
+		if (S_AXI_ARESETN)
+		assert(fm_wr_outstanding[N] == { 1'b0, w_swpending[N] }
+				+ (S_AXI_WREADY[N] ? 0:1));
+
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(fm_awr_outstanding[N] >=
+				(S_AXI_AWREADY[N] ? 0:1)
+				+((OPT_BUFFER_DECODER & dcd_awvalid[N]) ? 1:0)
+				+ (S_AXI_BVALID[N]  ? 1:0));
+
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(fm_wr_outstanding[N] >=
+				(S_AXI_WREADY[N] ? 0:1)
+				+ (S_AXI_BVALID[N]? 1:0));
+
+		always @(*)
+		if (S_AXI_ARESETN)
+		assert(fm_wr_outstanding[N]-(S_AXI_WREADY[N] ? 0:1)
+			<= fm_awr_outstanding[N]-(S_AXI_AWREADY[N] ? 0:1));
+
+		always @(*)
+		if (S_AXI_ARESETN && wgrant[N][NS])
+			assert(fm_wr_outstanding[N] == (S_AXI_WREADY[N] ? 0:1)
+				+ (S_AXI_BVALID[N] ? 1:0));
+
+		always @(*)
+		if (S_AXI_ARESETN && !swgrant[N])
+		begin
+			assert(!S_AXI_BVALID[N]);
+
+			assert(fm_awr_outstanding[N]==(S_AXI_AWREADY[N] ? 0:1)
+				+((OPT_BUFFER_DECODER & dcd_awvalid[N]) ? 1:0));
+			assert(fm_wr_outstanding[N] == (S_AXI_WREADY[N] ? 0:1));
+			assert(w_sawpending[N] == 0);
+			assert(w_swpending[N] == 0);
+		end
+
+
+		//
+		// Check read counters
+		//
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(fm_rd_outstanding[N] >=
+				(S_AXI_ARREADY[N] ? 0:1)
+				+(S_AXI_RVALID[N] ? 1:0));
+
+		always @(*)
+		if (S_AXI_ARESETN && (!srgrant[N] || rgrant[N][NS]))
+			assert(fm_rd_outstanding[N] ==
+				(S_AXI_ARREADY[N] ? 0:1)
+				+((OPT_BUFFER_DECODER & dcd_arvalid[N]) ? 1:0)
+				+(S_AXI_RVALID[N] ? 1:0));
+
+		always @(*)
+		if (S_AXI_ARESETN)
+			assert(fm_rd_outstanding[N] == { 1'b0, w_srpending[N] }
+				+((OPT_BUFFER_DECODER & dcd_arvalid[N]) ? 1:0)
+				+ (S_AXI_ARREADY[N] ? 0:1));
+
+		always @(*)
+		if (S_AXI_ARESETN && rgrant[N][NS])
+			assert(fm_rd_outstanding[N] == (S_AXI_ARREADY[N] ? 0:1)
+				+((OPT_BUFFER_DECODER & dcd_arvalid[N]) ? 1:0)
+				+(S_AXI_RVALID[N] ? 1:0));
+
+		always @(*)
+		if (S_AXI_ARESETN && !srgrant[N])
+		begin
+			assert(!S_AXI_RVALID[N]);
+			assert(fm_rd_outstanding[N]== (S_AXI_ARREADY[N] ? 0:1)
+				+((OPT_BUFFER_DECODER && dcd_arvalid[N])? 1:0));
+			assert(w_srpending[N] == 0);
+		end
+
+		//
+		// Check full/empty flags
+		//
+		localparam	[LGMAXBURST-1:0] NEAR_THRESHOLD = -2;
+
+		always @(*)
+		begin
+			assert(swfull[N] == &w_sawpending[N]);
+			assert(swempty[N] == (w_sawpending[N] == 0));
+		end
+
+		always @(*)
+		begin
+			assert(srfull[N] == &w_srpending[N]);
+			assert(srempty[N] == (w_srpending[N] == 0));
+		end
+		// }}}
+	end endgenerate
+
+	generate for(M=0; M<NS; M=M+1)
+	begin : CHECK_SLAVES
+		// {{{
+		faxil_master #(
+			.C_AXI_DATA_WIDTH(DW),
+			.C_AXI_ADDR_WIDTH(AW),
+			.F_OPT_ASSUME_RESET(1'b1),
+			.F_AXI_MAXRSTALL(0),
+			.F_LGDEPTH(F_LGDEPTH))
+		  slvi(.i_clk(S_AXI_ACLK),
+			.i_axi_reset_n(S_AXI_ARESETN),
+			//
+			.i_axi_awvalid(M_AXI_AWVALID[M]),
+			.i_axi_awready(M_AXI_AWREADY[M]),
+			.i_axi_awaddr(M_AXI_AWADDR[M*AW +: AW]),
+			.i_axi_awprot(M_AXI_AWPROT[M*3 +: 3]),
+			//
+			.i_axi_wvalid(M_AXI_WVALID[M]),
+			.i_axi_wready(M_AXI_WREADY[M]),
+			.i_axi_wdata( M_AXI_WDATA[M*DW +: DW]),
+			.i_axi_wstrb( M_AXI_WSTRB[M*DW/8 +: DW/8]),
+			//
+			.i_axi_bvalid(M_AXI_BVALID[M]),
+			.i_axi_bready(M_AXI_BREADY[M]),
+			.i_axi_bresp( M_AXI_BRESP[M*2 +: 2]),
+			//
+			.i_axi_arvalid(M_AXI_ARVALID[M]),
+			.i_axi_arready(M_AXI_ARREADY[M]),
+			.i_axi_araddr( M_AXI_ARADDR[M*AW +: AW]),
+			.i_axi_arprot( M_AXI_ARPROT[M*3 +: 3]),
+			//
+			//
+			.i_axi_rvalid(M_AXI_RVALID[M]),
+			.i_axi_rready(M_AXI_RREADY[M]),
+			.i_axi_rdata( M_AXI_RDATA[M*DW +: DW]),
+			.i_axi_rresp( M_AXI_RRESP[M*2 +: 2]),
+			//
+			.f_axi_rd_outstanding( fs_rd_outstanding[M]),
+			.f_axi_wr_outstanding( fs_wr_outstanding[M]),
+			.f_axi_awr_outstanding(fs_awr_outstanding[M]));
+
+		always @(*)
+		assert(fs_wr_outstanding[M] + (M_AXI_WVALID[M] ? 1:0)
+			<= fs_awr_outstanding[M] + (M_AXI_AWVALID[M]? 1:0));
+
+		always @(*)
+		if (!mwgrant[M])
+		begin
+			assert(fs_awr_outstanding[M] == 0);
+			assert(fs_wr_outstanding[M] == 0);
+		end
+
+		always @(*)
+		if (!mrgrant[M])
+			assert(fs_rd_outstanding[M] == 0);
+
+		always @(*)
+			assert(fs_awr_outstanding[M] < { 1'b1, {(F_LGDEPTH-1){1'b0}} });
+		always @(*)
+			assert(fs_wr_outstanding[M] < { 1'b1, {(F_LGDEPTH-1){1'b0}} });
+		always @(*)
+			assert(fs_rd_outstanding[M] < { 1'b1, {(F_LGDEPTH-1){1'b0}} });
+
+		always @(*)
+		if (M_AXI_AWVALID[M])
+			assert(((M_AXI_AWADDR[M*AW +: AW]
+				^ SLAVE_ADDR[M*AW +: AW])
+				& SLAVE_MASK[M*AW +: AW]) == 0);
+
+		always @(*)
+		if (M_AXI_ARVALID[M])
+			assert(((M_AXI_ARADDR[M*AW +: AW]
+				^ SLAVE_ADDR[M*AW +: AW])
+				& SLAVE_MASK[M*AW +: AW]) == 0);
+		// }}}
+	end endgenerate
+
+	generate for(N=0; N<NM; N=N+1)
+	begin : CORRELATE_OUTSTANDING
+		// {{{
+		always @(*)
+		if (S_AXI_ARESETN && (swgrant[N] && (swindex[N] < NS)))
+		begin
+			assert((fm_awr_outstanding[N]
+				- (S_AXI_AWREADY[N] ? 0:1)
+				-((OPT_BUFFER_DECODER && dcd_awvalid[N]) ? 1:0)
+				- (S_AXI_BVALID[N]  ? 1:0))
+				== (fs_awr_outstanding[swindex[N]]
+					+ (m_axi_awvalid[swindex[N]] ? 1:0)
+					+ (m_axi_bready[swindex[N]] ? 0:1)));
+
+			assert((fm_wr_outstanding[N]
+				- (S_AXI_WREADY[N] ? 0:1)
+				- (S_AXI_BVALID[N] ? 1:0))
+				== (fs_wr_outstanding[swindex[N]]
+					+ (m_axi_wvalid[swindex[N]] ? 1:0)
+					+ (m_axi_bready[swindex[N]] ? 0:1)));
+
+		end else if (S_AXI_ARESETN && (!swgrant[N] || (swindex[N]==NS)))
+		begin
+			if (!swgrant[N])
+				assert(fm_awr_outstanding[N] ==
+					(S_AXI_AWREADY[N] ? 0:1)
+					+((OPT_BUFFER_DECODER && dcd_awvalid[N]) ? 1:0)
+					+(S_AXI_BVALID[N]  ? 1:0));
+			else
+				assert(fm_awr_outstanding[N] >=
+					(S_AXI_AWREADY[N] ? 0:1)
+					+((OPT_BUFFER_DECODER && dcd_awvalid[N]) ? 1:0)
+					+(S_AXI_BVALID[N]  ? 1:0));
+
+			assert(fm_wr_outstanding[N]  ==
+					(S_AXI_WREADY[N]  ? 0:1)
+					+(S_AXI_BVALID[N]  ? 1:0));
+		end
+
+		always @(*)
+		if (srgrant[N] && (srindex[N] < NS))
+		begin
+			assert((fm_rd_outstanding[N]//17
+				- (S_AXI_ARREADY[N] ? 0:1)//1
+				-((OPT_BUFFER_DECODER && dcd_arvalid[N]) ? 1:0)
+				- (S_AXI_RVALID[N] ? 1:0))//0
+				== (fs_rd_outstanding[srindex[N]]//16
+					+ (m_axi_arvalid[srindex[N]] ? 1:0)//0
+					+ (m_axi_rready[srindex[N]] ? 0:1)));//0
+		end
+		// }}}
+	end endgenerate
+
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Cover properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	// Can every master reach every slave?
+	// Can things transition without dropping the request line(s)?
+	generate for(N=0; N<NM; N=N+1)
+	begin : COVER_CONNECTIVITY_FROM_MASTER
+		reg [3:0]	cvr_w_returns, cvr_r_returns;
+		reg		err_wr_return, err_rd_return;
+		reg [NS-1:0]	cvr_w_every, cvr_r_every;
+		reg		cvr_was_wevery, cvr_was_revery,
+				cvr_whsreturn, cvr_rhsreturn;
+
+		// cvr_w_returns is a speed check: Can we return one write
+		// acknowledgement per clock cycle?
+		initial	cvr_w_returns = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_w_returns = 0;
+		else begin
+			cvr_w_returns <= { cvr_w_returns[2:0], 1'b0 };
+			if (S_AXI_BVALID[N] && S_AXI_BREADY[N] && !wgrant[N][NS])
+				cvr_w_returns[0] <= 1'b1;
+		end
+
+		initial	cvr_whsreturn = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_whsreturn <= 0;
+		else
+			cvr_whsreturn <= cvr_whsreturn || (&cvr_w_returns);
+
+		// w_every is a connectivity test: Can we get a return from
+		// every slave?
+		initial	cvr_w_every = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_w_every <= 0;
+		else if (!S_AXI_AWVALID[N])
+			cvr_w_every <= 0;
+		else begin
+			if (S_AXI_BVALID[N] && S_AXI_BREADY[N] && !wgrant[N][NS])
+				cvr_w_every[swindex[N]] <= 1'b1;
+		end
+
+		always @(posedge S_AXI_ACLK)
+		if (S_AXI_BVALID[N])
+			assert($stable(swindex[N]));
+
+		initial	cvr_was_wevery = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_was_wevery <= 0;
+		else
+			cvr_was_wevery <= cvr_was_wevery || (&cvr_w_every);
+
+		// err_wr_return is a test to make certain we can return a
+		// bus error on the write channel.
+		initial	err_wr_return = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			err_wr_return = 0;
+		else if (wgrant[N][NS] && S_AXI_BVALID[N]
+				&& (S_AXI_BRESP[2*N+:2]==INTERCONNECT_ERROR))
+			err_wr_return = 1;
+
+`ifndef	VERILATOR
+		always @(*)
+			cover(!swgrant[N] && cvr_whsreturn);
+		always @(*)
+			cover(!swgrant[N] && cvr_was_wevery);
+
+		always @(*)
+			cover(S_AXI_ARESETN && wrequest[N][NS]);
+		always @(*)
+			cover(S_AXI_ARESETN && wrequest[N][NS] && slave_awaccepts[N]);
+		always @(*)
+			cover(err_wr_return);
+		always @(*)
+			cover(!swgrant[N] && err_wr_return);
+`endif
+
+		always @(*)
+		if (S_AXI_BVALID[N])
+			assert(swgrant[N]);
+
+		// cvr_r_returns is a speed check: Can we return one read
+		// acknowledgment per clock cycle?
+		initial	cvr_r_returns = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_r_returns = 0;
+		else begin
+			cvr_r_returns <= { cvr_r_returns[2:0], 1'b0 };
+			if (S_AXI_RVALID[N] && S_AXI_RREADY[N])
+				cvr_r_returns[0] <= 1'b1;
+		end
+
+		initial	cvr_rhsreturn = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_rhsreturn <= 0;
+		else
+			cvr_rhsreturn <= cvr_rhsreturn || (&cvr_r_returns);
+
+
+		// r_every is a connectivity test: Can we get a read return from
+		// every slave?
+		initial	cvr_r_every = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_r_every = 0;
+		else if (!S_AXI_ARVALID[N])
+			cvr_r_every = 0;
+		else begin
+			if (S_AXI_RVALID[N] && S_AXI_RREADY[N])
+				cvr_r_every[srindex[N]] <= 1'b1;
+		end
+
+		// cvr_was_revery is a return to idle check following the
+		// connectivity test.  Since the connectivity test is cleared
+		// if there's ever a drop in the valid line, we need a separate
+		// wire to check that this master can return to idle again.
+		initial	cvr_was_revery = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			cvr_was_revery <= 0;
+		else
+			cvr_was_revery <= cvr_was_revery || (&cvr_r_every);
+
+		always @(posedge S_AXI_ACLK)
+		if (S_AXI_RVALID[N])
+			assert($stable(srindex[N]));
+
+		initial	err_rd_return = 0;
+		always @(posedge S_AXI_ACLK)
+		if (!S_AXI_ARESETN)
+			err_rd_return = 0;
+		else if (rgrant[N][NS] && S_AXI_RVALID[N]
+				&& (S_AXI_RRESP[2*N+:2]==INTERCONNECT_ERROR))
+			err_rd_return = 1;
+
+`ifndef	VERILATOR
+		always @(*)
+			cover(!srgrant[N] && cvr_rhsreturn);	// @26
+		always @(*)
+			cover(!srgrant[N] && cvr_was_revery);	// @26
+
+		always @(*)
+			cover(S_AXI_ARVALID[N] && rrequest[N][NS]);
+		always @(*)
+			cover(rgrant[N][NS]);
+		always @(*)
+			cover(err_rd_return);
+		always @(*)
+			cover(!srgrant[N] && err_rd_return); //@!
+`endif
+
+		always @(*)
+		if (S_AXI_BVALID[N] && wgrant[N][NS])
+			assert(S_AXI_BRESP[2*N+:2]==INTERCONNECT_ERROR);
+		always @(*)
+		if (S_AXI_RVALID[N] && rgrant[N][NS])
+			assert(S_AXI_RRESP[2*N+:2]==INTERCONNECT_ERROR);
+	end endgenerate
+
+	reg	cvr_multi_write_hit, cvr_multi_read_hit;
+
+	initial	cvr_multi_write_hit = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		cvr_multi_write_hit <= 0;
+	else if (fm_awr_outstanding[0] > 2 && !wgrant[0][NS])
+		cvr_multi_write_hit <= 1;
+
+	initial	cvr_multi_read_hit = 0;
+	always @(posedge S_AXI_ACLK)
+	if (!S_AXI_ARESETN)
+		cvr_multi_read_hit <= 0;
+	else if (fm_rd_outstanding[0] > 2 && !rgrant[0][NS])
+		cvr_multi_read_hit <= 1;
+
+	always @(*)
+		cover(cvr_multi_write_hit);
+
+	always @(*)
+		cover(cvr_multi_read_hit);
+
+	always @(*)
+		cover(S_AXI_ARESETN && cvr_multi_write_hit & mwgrant == 0 && M_AXI_BVALID == 0);
+
+	always @(*)
+		cover(S_AXI_ARESETN && cvr_multi_read_hit & mrgrant == 0 && M_AXI_RVALID == 0);
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Negation check
+	// {{{
+	// Pick a particular value.  Assume the value doesn't show up on the
+	// input.  Prove it doesn't show up on the output.  This will check for
+	// ...
+	// 1. Stuck bits on the output channel
+	// 2. Cross-talk between channels
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	(* anyconst *)	reg	[LGNM-1:0]	f_const_source;
+	(* anyconst *)	reg	[AW-1:0]	f_const_addr;
+	(* anyconst *)	reg	[AW-1:0]	f_const_addr_n;
+	(* anyconst *)	reg	[DW-1:0]	f_const_data_n;
+	(* anyconst *)	reg	[DW/8-1:0]	f_const_strb_n;
+	(* anyconst *)	reg	[3-1:0]		f_const_prot_n;
+	(* anyconst *)	reg	[2-1:0]		f_const_resp_n;
+			reg	[LGNS-1:0]	f_const_slave;
+
+	always @(*)
+		assume(f_const_source < NM);
+	always @(*)
+	begin
+		f_const_slave = NS;
+		for(iM=0; iM<NS; iM=iM+1)
+		begin
+			if (((f_const_addr ^ SLAVE_ADDR[iM*AW+:AW])
+					&SLAVE_MASK[iM*AW+:AW])==0)
+				f_const_slave = iM;
+		end
+
+		assume(f_const_slave < NS);
+	end
+
+	reg	[AW-1:0]	f_awaddr;
+	reg	[AW-1:0]	f_araddr;
+	always @(*)
+		f_awaddr = S_AXI_AWADDR[f_const_source * AW +: AW];
+	always @(*)
+		f_araddr = S_AXI_ARADDR[f_const_source * AW +: AW];
+
+	// The assumption check: assume our negated values are not found on
+	// the inputs
+	always @(*)
+	begin
+		if (S_AXI_AWVALID[f_const_source])
+		begin
+			assume(f_awaddr != f_const_addr_n);
+			assume(S_AXI_AWPROT[f_const_source*3+:3] != f_const_prot_n);
+		end
+		if (m_wvalid)
+		begin
+			assume(m_wdata[f_const_source] != f_const_data_n);
+			assume(m_wstrb[f_const_source] != f_const_strb_n);
+		end
+		if (S_AXI_ARVALID[f_const_source])
+		begin
+			assume(f_araddr != f_const_addr_n);
+			assume(S_AXI_ARPROT[f_const_source*3+:3] != f_const_prot_n);
+		end
+
+		if (M_AXI_BVALID[f_const_slave] && wgrant[f_const_source][f_const_slave])
+		begin
+			assume(m_axi_bresp[f_const_slave] != f_const_resp_n);
+		end
+
+		if (M_AXI_RVALID[f_const_slave] && rgrant[f_const_source][f_const_slave])
+		begin
+			assume(m_axi_rdata[f_const_slave] != f_const_data_n);
+			assume(m_axi_rresp[f_const_slave] != f_const_resp_n);
+		end
+	end
+
+	// Proof check: Prove these values are not found on our outputs
+	always @(*)
+	begin
+		if (skd_awvalid[f_const_source])
+		begin
+			assert(skd_awaddr[f_const_source] != f_const_addr_n);
+			assert(skd_awprot[f_const_source] != f_const_prot_n);
+		end
+		if (dcd_awvalid[f_const_source])
+		begin
+			assert(m_awaddr[f_const_source] != f_const_addr_n);
+			assert(m_awprot[f_const_source] != f_const_prot_n);
+		end
+		if (M_AXI_AWVALID[f_const_slave] && wgrant[f_const_source][f_const_slave])
+		begin
+			assert(M_AXI_AWADDR[f_const_slave*AW+:AW] != f_const_addr_n);
+			assert(M_AXI_AWPROT[f_const_slave*3+:3] != f_const_prot_n);
+		end
+		if (M_AXI_WVALID[f_const_slave] && wgrant[f_const_source][f_const_slave])
+		begin
+			assert(M_AXI_WDATA[f_const_slave*DW+:DW] != f_const_data_n);
+			assert(M_AXI_WSTRB[f_const_slave*(DW/8)+:(DW/8)] != f_const_strb_n);
+		end
+		if (skd_arvalid[f_const_source])
+		begin
+			assert(skd_araddr[f_const_source] != f_const_addr_n);
+			assert(skd_arprot[f_const_source] != f_const_prot_n);
+		end
+		if (dcd_arvalid[f_const_source])
+		begin
+			assert(m_araddr[f_const_source] != f_const_addr_n);
+			assert(m_arprot[f_const_source] != f_const_prot_n);
+		end
+		if (M_AXI_ARVALID[f_const_slave] && rgrant[f_const_source][f_const_slave])
+		begin
+			assert(M_AXI_ARADDR[f_const_slave*AW+:AW] != f_const_addr_n);
+			assert(M_AXI_ARPROT[f_const_slave*3+:3] != f_const_prot_n);
+		end
+		//
+		if (r_bvalid[f_const_source] && wgrant[f_const_source][f_const_slave])
+			assert(r_bresp[f_const_source] != f_const_resp_n);
+		if (S_AXI_BVALID[f_const_source] && wgrant[f_const_source][f_const_slave])
+			assert(S_AXI_BRESP[f_const_source*2+:2] != f_const_resp_n);
+		if (r_rvalid[f_const_source] && rgrant[f_const_source][f_const_slave])
+		begin
+			assert(r_rresp[f_const_source] != f_const_resp_n);
+			assert(r_rdata[f_const_source] != f_const_data_n);
+		end
+		if (S_AXI_RVALID[f_const_source] && rgrant[f_const_source][f_const_slave])
+		begin
+			assert(S_AXI_RRESP[f_const_source*2+:2]!=f_const_resp_n);
+			assert(S_AXI_RDATA[f_const_source*DW+:DW]!=f_const_data_n);
+		end
+	end
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// (Careless) constraining assumptions
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	generate for(N=0; N<NM; N=N+1)
+	begin
+
+	end endgenerate
+	// }}}
+`endif
+// }}}
+endmodule
+`ifndef	YOSYS
+`default_nettype wire
+`endif