////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	wbxbar.v
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	A Configurable wishbone cross-bar interconnect, conforming
//		to the WB-B4 pipeline specification, as described on the
//	ZipCPU blog.
//
// Performance:
//	Throughput: One transaction per clock
//	Latency: One clock to get access to an unused channel, another to
//	place the results on the slave bus, and another to return, or a minimum
//	of three clocks.
//
// Usage: To use, you'll need to set NM and NS to the number of masters
//	(input ports) and the number of slaves respectively.  You'll then
//	want to set the addresses for the slaves in the SLAVE_ADDR array,
//	together with the SLAVE_MASK array indicating which SLAVE_ADDRs
//	are valid.  Address and data widths should be adjusted at the same
//	time.
//
//	Voila, you are now set up!
//
//	Now let's fine tune this:
//
//	LGMAXBURST can be set to control the maximum number of outstanding
//	transactions.  An LGMAXBURST of 6 will allow 63 outstanding
//	transactions.
//
//	OPT_TIMEOUT, if set to a non-zero value, is a number of clock periods
//	to wait for a slave to respond.  Should the timeout expire and the
//	slave not respond, a bus error will be returned and the slave will
//	be issued a bus abort signal (CYC will be dropped).
//
//	OPT_STARVATION_TIMEOUT, if set, applies the OPT_TIMEOUT counter to
//	how long a particular master waits for arbitration.  If the master is
//	"starved", a bus error will be returned.
//
//	OPT_DBLBUFFER is used to increase clock speed by registering all
//	outputs.
//
//	OPT_LOWPOWER is an experimental feature that, if set, will cause any
//	unused FFs to be set to zero rather than flopping in the electronic
//	wind, in an effort to minimize transitions over bus wires.  This will
//	cost some extra logic, for ... an uncertain power savings.
//
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2019-2020, Gisselquist Technology, LLC
//
// This file is part of the WB2AXIP project.
//
// The WB2AXIP project contains free software and gateware, licensed under the
// Apache License, Version 2.0 (the "License").  You may not use this project,
// or this file, except in compliance with the License.  You may obtain a copy
// of the License at
//
//	http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.  See the
// License for the specific language governing permissions and limitations
// under the License.
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
//
module	wbxbar(i_clk, i_reset,
	i_mcyc, i_mstb, i_mwe, i_maddr, i_mdata, i_msel,
		o_mstall, o_mack, o_mdata, o_merr,
	o_scyc, o_sstb, o_swe, o_saddr, o_sdata, o_ssel,
		i_sstall, i_sack, i_sdata, i_serr);
	parameter	NM = 4, NS=8;
	parameter	AW = 32, DW=32;
	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'b0010, {(AW-4){1'b0}}},
				{ 4'b0000, {(AW-4){1'b0}}} };
	parameter	[NS*AW-1:0]	SLAVE_MASK = (NS <= 1) ? 0
		: { {(NS-2){ 3'b111, {(AW-3){1'b0}}}},
			{(2){ 4'b1111, {(AW-4){1'b0}} }} };
	//
	// LGMAXBURST is the log_2 of the length of the longest burst that
	// might be seen.  It's used to set the size of the internal
	// counters that are used to make certain that the cross bar doesn't
	// switch while still waiting on a response.
	parameter	LGMAXBURST=6;
	//
	// OPT_TIMEOUT is used to help recover from a misbehaving slave.  If
	// set, this value will determine the number of clock cycles to wait
	// for a misbehaving slave before returning a bus error.  Alternatively,
	// if set to zero, this functionality will be removed.
	parameter	OPT_TIMEOUT = 0; // 1023;
	//
	// If OPT_TIMEOUT is set, then OPT_STARVATION_TIMEOUT may also be set.
	// The starvation timeout adds to the bus error timeout generation
	// the possibility that a master will wait OPT_TIMEOUT counts without
	// receiving the bus.  This may be the case, for example, if one
	// bus master is consuming a peripheral to such an extent that there's
	// no time/room for another bus master to use it.  In that case, when
	// the timeout runs out, the waiting bus master will be given a bus
	// error.
	parameter [0:0]	OPT_STARVATION_TIMEOUT = 1'b0 && (OPT_TIMEOUT > 0);
	//
	// TIMEOUT_WIDTH is the number of bits in counter used to check on a
	// timeout.
	localparam	TIMEOUT_WIDTH = $clog2(OPT_TIMEOUT);
	//
	// OPT_DBLBUFFER is used to register all of the outputs, and thus
	// avoid adding additional combinational latency through the core
	// that might require a slower clock speed.
	parameter [0:0]	OPT_DBLBUFFER = 1'b0;
	//
	// OPT_LOWPOWER adds logic to try to force unused values to zero,
	// rather than to allow a variety of logic optimizations that could
	// be used to reduce the logic count of the device.  Hence, OPT_LOWPOWER
	// will use more logic, but it won't drive bus wires unless there's a
	// value to drive onto them.
	parameter [0:0]	OPT_LOWPOWER = 1'b1;
	//
	// LGNM is the log (base two) of the number of bus masters connecting
	// to this crossbar
	localparam	LGNM = (NM>1) ? $clog2(NM) : 1;
	//
	// LGNM is the log (base two) of the number of slaves plus one come
	// out of the system.  The extra "plus one" is used for a pseudo slave
	// representing the case where the given address doesn't connect to
	// any of the slaves.  This address will generate a bus error.
	localparam	LGNS = $clog2(NS+1);
	//
	//
	input	wire			i_clk, i_reset;
	//
	// Here are the bus inputs from each of the WB bus masters
	input	wire	[NM-1:0]	i_mcyc, i_mstb, i_mwe;
	input	wire	[NM*AW-1:0]	i_maddr;
	input	wire	[NM*DW-1:0]	i_mdata;
	input	wire	[NM*DW/8-1:0]	i_msel;
	//
	// .... and their return data
	output	reg	[NM-1:0]	o_mstall, o_mack, o_merr;
	output	reg	[NM*DW-1:0]	o_mdata;
	//
	//
	// Here are the output ports, used to control each of the various
	// slave ports that we are connected to
	output	reg	[NS-1:0]	o_scyc, o_sstb, o_swe;
	output	reg	[NS*AW-1:0]	o_saddr;
	output	reg	[NS*DW-1:0]	o_sdata;
	output	reg	[NS*DW/8-1:0]	o_ssel;
	//
	// ... and their return data back to us.
	input	wire	[NS-1:0]	i_sstall, i_sack, i_serr;
	input	wire	[NS*DW-1:0]	i_sdata;
	//
	//

	// At one time I used o_macc and o_sacc to put into the outgoing
	// trace file, just enough logic to tell me if a transaction was
	// taking place on the given clock.
	//
	// assign	o_macc = (i_mstb & ~o_mstall);
	// assign	o_sacc = (o_sstb & ~i_sstall);
	//
	// These definitions work with Veri1ator, just not with Yosys
	// reg	[NM-1:0][NS:0]		request;
	// reg	[NM-1:0][NS-1:0]	requested;
	// reg	[NM-1:0][NS:0]		grant;
	//
	// These definitions work with both
	wire	[NS:0]			request		[0:NM-1];
	reg	[NS-1:0]		requested	[0:NM-1];
	reg	[NS:0]			grant		[0:NM-1];
	reg	[NM-1:0]		mgrant;
	reg	[NS-1:0]		sgrant;

	// Verilator lint_off UNUSED
	wire	[LGMAXBURST-1:0]	w_mpending [0:NM-1];
	// Verilator lint_on  UNUSED
	reg	[NM-1:0]		mfull, mnearfull, mempty, timed_out;

	localparam	NMFULL = (NM > 1) ? (1<<LGNM) : 1;
	localparam	NSFULL = (1<<LGNS);

	reg	[LGNS-1:0]	mindex		[0:NMFULL-1];
	reg	[LGNM-1:0]	sindex		[0:NSFULL-1];

	reg	[NMFULL-1:0]	m_cyc;
	reg	[NMFULL-1:0]	m_stb;
	wire	[NMFULL-1:0]	m_we;
	wire	[AW-1:0]	m_addr		[0:NMFULL-1];
	wire	[DW-1:0]	m_data		[0:NMFULL-1];
	wire	[DW/8-1:0]	m_sel		[0:NMFULL-1];
	reg	[NM-1:0]	m_stall;
	//
	reg	[NSFULL-1:0]	s_stall;
	reg	[DW-1:0]	s_data		[0:NSFULL-1];
	reg	[NSFULL-1:0]	s_ack;
	reg	[NSFULL-1:0]	s_err;
	wire	[NM-1:0]	dcd_stb;

	localparam [0:0]	OPT_BUFFER_DECODER = (NS != 1 || SLAVE_MASK != 0);

	genvar	N, M;
	integer	iN, iM;
	generate for(N=0; N<NM; N=N+1)
	begin : DECODE_REQUEST
		wire			skd_stb, skd_stall;
		wire			skd_we;
		wire	[AW-1:0]	skd_addr;
		wire	[DW-1:0]	skd_data;
		wire	[DW/8-1:0]	skd_sel;
		wire	[NS:0]		decoded;
		wire			iskd_ready;

		skidbuffer #(
			//
			// Can't run OPT_LOWPOWER here, less we mess up the
			// consistency in skd_we following
			//
			// .OPT_LOWPOWER(OPT_LOWPOWER),
			.DW(1+AW+DW+DW/8),
`ifdef	FORMAL
			.OPT_PASSTHROUGH(1),
`endif
			.OPT_OUTREG(0))
		iskid(i_clk, i_reset || !i_mcyc[N], i_mstb[N], iskd_ready,
			{ i_mwe[N], i_maddr[N*AW +: AW], i_mdata[N*DW +: DW],
					i_msel[N*DW/8 +: DW/8] },
			skd_stb, !skd_stall,
				{ skd_we, skd_addr, skd_data, skd_sel });

		always @(*)
			o_mstall[N] = !iskd_ready;

		addrdecode #(
			//
			// Can't run OPT_LOWPOWER here, less we mess up the
			// consistency in m_we following
			//
			// .OPT_LOWPOWER(OPT_LOWPOWER),
			.NS(NS), .AW(AW), .DW(DW+DW/8+1),
			.SLAVE_ADDR(SLAVE_ADDR),
			.SLAVE_MASK(SLAVE_MASK),
			.OPT_REGISTERED(OPT_BUFFER_DECODER)
		) adcd(i_clk, i_reset, skd_stb && i_mcyc[N], skd_stall,
			skd_addr, { skd_we, skd_data, skd_sel },
			dcd_stb[N], (m_stall[N]&&i_mcyc[N]),decoded, m_addr[N],
				{ m_we[N], m_data[N], m_sel[N] });

		assign	request[N] = (m_cyc[N] && dcd_stb[N]) ? decoded : 0;

		always @(*)
			m_cyc[N] = i_mcyc[N];
		always @(*)
		if (mfull[N])
			m_stb[N] = 1'b0;
		else
			m_stb[N] = i_mcyc[N] && dcd_stb[N];

	end for(N=NM; N<NMFULL; N=N+1)
	begin
		// in case NM isn't one less than a power of two, complete
		// the set
		always @(*)
		begin
			m_cyc[N]  = 0;
			m_stb[N]  = 0;
		end


		assign	m_we[N]   = 0;
		assign	m_addr[N] = 0;
		assign	m_data[N] = 0;
		assign	m_sel[N]  = 0;

	end endgenerate

	always @(*)
	begin
		for(iM=0; iM<NS; iM=iM+1)
		begin
			// For each slave
			requested[0][iM] = 0;
			for(iN=1; iN<NM; iN=iN+1)
			begin
				// This slave has been requested if a prior
				// master has requested it
				//
				// This includes any master before the last one
				requested[iN][iM] = requested[iN-1][iM];
				//
				// As well as if the last master has requested
				// this slave.  Only count this request, though,
				// if this master could act upon it.
				if (request[iN-1][iM] &&
					(grant[iN-1][iM]
					|| (!mgrant[iN-1]||mempty[iN-1])))
					requested[iN][iM] = 1;
			end
		end
	end

	generate for(M=0; M<NS; M=M+1)
	begin : SLAVE_GRANT

`define	REGISTERED_SGRANT
`ifdef	REGISTERED_SGRANT
		reg	drop_sgrant;
		always @(*)
		begin
			drop_sgrant = !m_cyc[sindex[M]];
			if (!request[sindex[M]][M] && m_stb[sindex[M]]
				&& mempty[sindex[M]])
				drop_sgrant = 1;
			if (!sgrant[M])
				drop_sgrant = 0;
			if (i_reset)
				drop_sgrant = 1;
		end

		initial	sgrant[M] = 0;
		always @(posedge i_clk)
		begin
			sgrant[M] <= sgrant[M];
			for(iN=0; iN<NM; iN=iN+1)
			if (request[iN][M] && (!mgrant[iN] || mempty[iN]))
				sgrant[M] <= 1;
			if (drop_sgrant)
				sgrant[M] <= 0;
		end
`else
		always @(*)
		begin
			sgrant[M] = 0;
			for(iN=0; iN<NM; iN=iN+1)
				if (grant[iN][M])
					sgrant[M] = 1;
		end
`endif

		always @(*)
			s_data[M]  = i_sdata[M*DW +: DW];
		always @(*)
			s_stall[M] = o_sstb[M] && i_sstall[M];
		always @(*)
			s_ack[M]   = o_scyc[M] && i_sack[M];
		always @(*)
			s_err[M]   = o_scyc[M] && i_serr[M];
	end for(M=NS; M<NSFULL; M=M+1)
	begin

		always @(*)
			s_data[M]  = 0;
		always @(*)
			s_stall[M] = 1;
		always @(*)
			s_ack[M]   = 0;
		always @(*)
			s_err[M]   = 1;
		// always @(*) sgrant[M]  = 0;

	end endgenerate

	//
	// Arbitrate among masters to determine who gets to access a given
	// channel
	generate for(N=0; N<NM; N=N+1)
	begin : ARBITRATE_REQUESTS
		reg	[NS:0]		regrant;
		reg	[LGNS-1:0]	reindex;

		// This is done using a couple of variables.
		//
		// request[N][M]
		//	This is true if master N is requesting to access slave
		//	M.  It is combinatorial, so it will be true if the
		//	request is being made on the current clock.
		//
		// requested[N][M]
		//	True if some other master, prior to N, has requested
		//	channel M.  This creates a basic priority arbiter,
		//	such that lower numbered masters have access before
		//	a greater numbered master
		//
		// grant[N][M]
		//	True if a grant has been made for master N to access
		//	slave channel M
		//
		// mgrant[N]
		//	True if master N has been granted access to some slave
		//	channel, any channel.
		//
		// mindex[N]
		//	This is the number of the slave channel that master
		//	N has been given access to
		//
		// sgrant[M]
		//	True if there exists some master, N, that has been
		// 	granted access to this slave, hence grant[N][M] must
		//	also be true
		//
		// sindex[M]
		//	This is the index of the master that has access to
		//	slave M, assuming sgrant[M].  Hence, if sgrant[M]
		//	then grant[sindex[M]][M] must be true
		//
		reg	stay_on_channel;
		reg	requested_channel_is_available;

		always @(*)
		begin
			stay_on_channel = |(request[N] & grant[N]);

			if (mgrant[N] && !mempty[N])
				stay_on_channel = 1;
		end

		always @(*)
		begin
			requested_channel_is_available =
			|(request[N][NS-1:0] & ~sgrant & ~requested[N][NS-1:0]);

			if (request[N][NS])
				requested_channel_is_available = 1;

			if (NM < 2)
				requested_channel_is_available = m_stb[N];
		end

		initial	grant[N] = 0;
		initial	mgrant[N] = 0;
		always @(posedge i_clk)
		if (i_reset || !i_mcyc[N])
		begin
			grant[N] <= 0;
			mgrant[N] <= 0;
		end else if (!stay_on_channel)
		begin
			if (requested_channel_is_available)
			begin
				mgrant[N] <= 1'b1;
				grant[N] <= request[N];
			end else if (m_stb[N])
			begin
				mgrant[N] <= 1'b0;
				grant[N]  <= 0;
			end
		end

		if (NS == 1)
		begin

			always @(*)
				mindex[N] = 0;

			always @(*)
				regrant = 0;

			always @(*)
				reindex = 0;

		end else begin
`define	NEW_MINDEX_CODE
`ifdef	NEW_MINDEX_CODE

			always @(*)
			begin
				regrant = 0;
				for(iM=0; iM<NS; iM=iM+1)
				begin
					if (grant[N][iM])
						// Maintain any open channels
						regrant[iM] = 1'b1;
					else if (!sgrant[iM]&&!requested[N][iM])
						regrant[iM] = 1'b1;

					if (!request[N][iM])
						regrant[iM] = 1'b0;
				end

				if (grant[N][NS])
					regrant[NS] = 1;
				if (!request[N][NS])
					regrant[NS] = 0;

				if (mgrant[N] && !mempty[N])
					regrant = 0;
			end

			always @(*)
			begin
				reindex = 0;
				for(iM=0; iM<=NS; iM=iM+1)
				if (regrant[iM])
					reindex = reindex | iM[LGNS-1:0];
				if (regrant == 0)
					reindex = mindex[N];
			end

			always @(posedge i_clk)
				mindex[N] <= reindex;
`else
			always @(posedge i_clk)
			if (!mgrant[N] || mempty[N])
			begin

				for(iM=0; iM<NS; iM=iM+1)
				begin
					if (request[N][iM] && grant[N][iM])
					begin
						// Maintain any open channels
						mindex[N] <= iM;
					end else if (request[N][iM]
							&& !sgrant[iM]
							&& !requested[N][iM])
					begin
						// Open a new channel
						// if necessary
						mindex[N] <= iM;
					end
				end
			end
`endif // NEW_MINDEX_CODE
		end

	end for (N=NM; N<NMFULL; N=N+1)
	begin

		always @(*)
			mindex[N] = 0;

	end endgenerate

	// Calculate sindex.  sindex[M] (indexed by slave ID)
	// references the master controlling this slave.  This makes for
	// faster/cheaper logic on the return path, since we can now use
	// a fully populated LUT rather than a priority based return scheme
	generate for(M=0; M<NS; M=M+1)
	begin

		if (NM <= 1)
		begin

			// If there will only ever be one master, then we
			// can assume all slave indexes point to that master
			always @(*)
				sindex[M] = 0;

		end else begin : SINDEX_MORE_THAN_ONE_MASTER

`define	NEW_SINDEX_CODE
`ifdef	NEW_SINDEX_CODE
			reg	[NM-1:0]	regrant;
			reg	[LGNM-1:0]	reindex;

			always @(*)
			begin
				regrant = 0;
				for (iN=0; iN<NM; iN=iN+1)
				begin
					// Each bit depends upon 6 inputs, so
					// one 6-LUT should be sufficient
					if (grant[iN][M])
						regrant[iN] = 1;
					else if (!sgrant[M]&& !requested[iN][M])
						regrant[iN] = 1;

					if (!request[iN][M])
						regrant[iN] = 0;
					if (mgrant[iN] && !mempty[iN])
						regrant[iN] = 0;
				end
			end

			always @(*)
			begin
				reindex = 0;
				// Each bit in reindex depends upon all of the
				// bits in regrant--should still be one LUT
				// per bit though
				if (regrant == 0)
					reindex = sindex[M];
				else for(iN=0; iN<NM; iN=iN+1)
					if (regrant[iN])
						reindex = reindex | iN[LGNM-1:0];
			end

			always @(posedge i_clk)
				sindex[M] <= reindex;
`else
			always @(posedge i_clk)
			for (iN=0; iN<NM; iN=iN+1)
			begin
				if (!mgrant[iN] || mempty[iN])
				begin
					if (request[iN][M] && grant[iN][M])
						sindex[M] <= iN;
					else if (request[iN][M] && !sgrant[M]
							&& !requested[iN][M])
						sindex[M] <= iN;
				end
			end
`endif
		end

	end for(M=NS; M<NSFULL; M=M+1)
	begin
		// Assign the unused slave indexes to zero
		//
		// Remember, to full out a full 2^something set of slaves,
		// we may have more slave indexes than we actually have slaves

		always @(*)
			sindex[M] = 0;

	end endgenerate


	//
	// Assign outputs to the slaves, part one
	//
	// In this part, we assign the difficult outputs: o_scyc and o_sstb
	generate for(M=0; M<NS; M=M+1)
	begin

		initial	o_scyc[M] = 0;
		initial	o_sstb[M] = 0;
		always @(posedge i_clk)
		begin
			if (sgrant[M])
			begin

				if (!i_mcyc[sindex[M]])
				begin
					o_scyc[M] <= 1'b0;
					o_sstb[M] <= 1'b0;
				end else begin
					o_scyc[M] <= 1'b1;

					if (!o_sstb[M] || !s_stall[M])
						o_sstb[M]<=request[sindex[M]][M]
						  && !mfull[sindex[M]];
				end
			end else begin
				o_scyc[M]  <= 1'b0;
				o_sstb[M]  <= 1'b0;
			end

			if (i_reset || s_err[M])
			begin
				o_scyc[M] <= 1'b0;
				o_sstb[M] <= 1'b0;
			end
		end
	end endgenerate

	//
	// Assign outputs to the slaves, part two
	//
	// These are the easy(er) outputs, since there are fewer properties
	// riding on them
	generate if ((NM == 1) && (!OPT_LOWPOWER))
	begin
		reg			r_swe;
		reg	[AW-1:0]	r_saddr;
		reg	[DW-1:0]	r_sdata;
		reg	[DW/8-1:0]	r_ssel;

		//
		// This is the low logic version of our bus data outputs.
		// It only works if we only have one master.
		//
		// The basic idea here is that we share all of our bus outputs
		// between all of the various slaves.  Since we only have one
		// bus master, this works.
		//
		always @(posedge i_clk)
		begin
			r_swe   <= o_swe[0];
			r_saddr <= o_saddr[0+:AW];
			r_sdata <= o_sdata[0+:DW];
			r_ssel  <=o_ssel[0+:DW/8];

			// Verilator lint_off WIDTH
			if (sgrant[mindex[0]] && !s_stall[mindex[0]])
			// Verilator lint_on  WIDTH
			begin
				r_swe   <= m_we[0];
				r_saddr <= m_addr[0];
				r_sdata <= m_data[0];
				r_ssel  <= m_sel[0];
			end
		end

		//
		// The original version set o_s*[0] above, and then
		// combinatorially the rest of o_s* here below.  That broke
		// Veri1ator.  Hence, we're using r_s* and setting all of o_s*
		// here.
		for(M=0; M<NS; M=M+1)
		always @(*)
		begin
			o_swe[M]            = r_swe;
			o_saddr[M*AW +: AW] = r_saddr[AW-1:0];
			o_sdata[M*DW +: DW] = r_sdata[DW-1:0];
			o_ssel[M*DW/8+:DW/8]= r_ssel[DW/8-1:0];
		end

	end else for(M=0; M<NS; M=M+1)
	begin
		always @(posedge i_clk)
		begin
			if (OPT_LOWPOWER && !sgrant[M])
			begin
				o_swe[M]              <= 1'b0;
				o_saddr[M*AW   +: AW] <= 0;
				o_sdata[M*DW   +: DW] <= 0;
				o_ssel[M*(DW/8)+:DW/8]<= 0;
			end else if (!s_stall[M]) begin
				o_swe[M]              <= m_we[sindex[M]];
				o_saddr[M*AW   +: AW] <= m_addr[sindex[M]];
				if (OPT_LOWPOWER && !m_we[sindex[M]])
					o_sdata[M*DW   +: DW] <= 0;
				else
					o_sdata[M*DW   +: DW] <= m_data[sindex[M]];
				o_ssel[M*(DW/8)+:DW/8]<= m_sel[sindex[M]];
			end

		end
	end endgenerate

	//
	// Assign return values to the masters
	generate if (OPT_DBLBUFFER)
	begin : DOUBLE_BUFFERRED_STALL

		reg	[NM-1:0]	r_mack, r_merr;

		for(N=0; N<NM; N=N+1)
		begin
			// m_stall isn't buffered, since it depends upon
			// the already existing buffer within the address
			// decoder
			always @(*)
			begin
				if (grant[N][NS])
					m_stall[N] = 1;
				else if (mgrant[N] && request[N][mindex[N]])
					m_stall[N] = mfull[N] || s_stall[mindex[N]];
				else
					m_stall[N] = m_stb[N];

				if (o_merr[N])
					m_stall[N] = 0;
			end

			initial	r_mack[N]   = 0;
			initial	r_merr[N]   = 0;
			always @(posedge i_clk)
			begin
				// Verilator lint_off WIDTH
				iM = mindex[N];
				// Verilator lint_on  WIDTH
				r_mack[N]   <= mgrant[N] && s_ack[mindex[N]];
				r_merr[N]   <= mgrant[N] && s_err[mindex[N]];
				if (OPT_LOWPOWER && !mgrant[N])
					o_mdata[N*DW +: DW] <= 0;
				else
					o_mdata[N*DW +: DW] <= s_data[mindex[N]];

				if (grant[N][NS]||(timed_out[N] && !o_mack[N]))
				begin
					r_mack[N]   <= 1'b0;
					r_merr[N]   <= !o_merr[N];
				end

				if (i_reset || !i_mcyc[N] || o_merr[N])
				begin
					r_mack[N]   <= 1'b0;
					r_merr[N]   <= 1'b0;
				end
			end

			always @(*)
				o_mack[N] = r_mack[N];

			always @(*)
			if (!OPT_STARVATION_TIMEOUT || i_mcyc[N])
				o_merr[N] = r_merr[N];
			else
				o_merr[N] = 1'b0;

		end

	end else if (NS == 1) // && !OPT_DBLBUFFER
	begin : SINGLE_SLAVE

		for(N=0; N<NM; N=N+1)
		begin
			always @(*)
			begin
				m_stall[N] = !mgrant[N] || s_stall[0]
					|| (m_stb[N] && !request[N][0]);
				o_mack[N]   =  mgrant[N] && i_sack[0];
				o_merr[N]   =  mgrant[N] && i_serr[0];
				o_mdata[N*DW +: DW]  = (!mgrant[N] && OPT_LOWPOWER)
					? 0 : i_sdata;

				if (mfull[N])
					m_stall[N] = 1'b1;

				if (timed_out[N]&&!o_mack[N])
				begin
					m_stall[N] = 1'b0;
					o_mack[N]   = 1'b0;
					o_merr[N]   = 1'b1;
				end

				if (grant[N][NS] && m_stb[N])
				begin
					m_stall[N] = 1'b0;
					o_mack[N]   = 1'b0;
					o_merr[N]   = 1'b1;
				end

				if (!m_cyc[N])
				begin
					o_mack[N] = 1'b0;
					o_merr[N] = 1'b0;
				end
			end
		end

	end else begin : SINGLE_BUFFER_STALL
		for(N=0; N<NM; N=N+1)
		begin
			// initial	o_mstall[N] = 0;
			// initial	o_mack[N]   = 0;
			always @(*)
			begin
				m_stall[N] = 1;
				o_mack[N]   = mgrant[N] && s_ack[mindex[N]];
				o_merr[N]   = mgrant[N] && s_err[mindex[N]];
				if (OPT_LOWPOWER && !mgrant[N])
					o_mdata[N*DW +: DW] = 0;
				else
					o_mdata[N*DW +: DW] = s_data[mindex[N]];

				if (mgrant[N])
					// Possibly lower the stall signal
					m_stall[N] = s_stall[mindex[N]]
					    || !request[N][mindex[N]];

				if (mfull[N])
					m_stall[N] = 1'b1;

				if (grant[N][NS] ||(timed_out[N]&&!o_mack[N]))
				begin
					m_stall[N] = 1'b0;
					o_mack[N]   = 1'b0;
					o_merr[N]   = 1'b1;
				end

				if (!m_cyc[N])
				begin
					o_mack[N] = 1'b0;
					o_merr[N] = 1'b0;
				end
			end
		end

	end endgenerate

	//
	// Count the pending transactions per master
	generate for(N=0; N<NM; N=N+1)
	begin : COUNT_PENDING_TRANSACTIONS

		reg	[LGMAXBURST-1:0]	lclpending;
		initial	lclpending  = 0;
		initial	mempty[N]    = 1;
		initial	mnearfull[N] = 0;
		initial	mfull[N]     = 0;
		always @(posedge i_clk)
		if (i_reset || !i_mcyc[N] || o_merr[N])
		begin
			lclpending <= 0;
			mfull[N]    <= 0;
			mempty[N]   <= 1'b1;
			mnearfull[N]<= 0;
		end else case({ (m_stb[N] && !m_stall[N]), o_mack[N] })
		2'b01: begin
			lclpending <= lclpending - 1'b1;
			mnearfull[N]<= mfull[N];
			mfull[N]    <= 1'b0;
			mempty[N]   <= (lclpending == 1);
			end
		2'b10: begin
			lclpending <= lclpending + 1'b1;
			mnearfull[N]<= (&lclpending[LGMAXBURST-1:2])&&(lclpending[1:0] != 0);
			mfull[N]    <= mnearfull[N];
			mempty[N]   <= 1'b0;
			end
		default: begin end
		endcase

		assign w_mpending[N] = lclpending;

	end endgenerate

	generate if (OPT_TIMEOUT > 0)
	begin : CHECK_TIMEOUT

		for(N=0; N<NM; N=N+1)
		begin

			reg	[TIMEOUT_WIDTH-1:0]	deadlock_timer;

			initial	deadlock_timer = OPT_TIMEOUT;
			initial	timed_out[N] = 0;
			always @(posedge i_clk)
			if (i_reset || !i_mcyc[N]
					||((w_mpending[N] == 0) && !m_stb[N])
					||(m_stb[N] && !m_stall[N])
					||(o_mack[N] || o_merr[N])
					||(!OPT_STARVATION_TIMEOUT&&!mgrant[N]))
			begin
				deadlock_timer <= OPT_TIMEOUT;
				timed_out[N] <= 0;
			end else if (deadlock_timer > 0)
			begin
				deadlock_timer <= deadlock_timer - 1;
				timed_out[N] <= (deadlock_timer <= 1);
			end
		end

	end else begin

		always @(*)
			timed_out = 0;

	end endgenerate

	initial	begin
		if (NM == 0)
		begin
			$display("ERROR: At least one master must be defined");
			$stop;
		end

		if (NS == 0)
		begin
			$display("ERROR: At least one slave must be defined");
			$stop;
		end

		if (OPT_STARVATION_TIMEOUT != 0 && OPT_TIMEOUT == 0)
		begin
			$display("ERROR: The starvation timeout is implemented as part of the regular timeout");
			$display("  Without a timeout, the starvation timeout will not work");
			$stop;
		end
	end

`ifdef	FORMAL
	localparam	F_MAX_DELAY = 4;
	localparam	F_LGDEPTH = LGMAXBURST;
	//
	reg			f_past_valid;
	//
	// Our bus checker keeps track of the number of requests,
	// acknowledgments, and the number of outstanding transactions on
	// every channel, both the masters driving us
	wire	[F_LGDEPTH-1:0]	f_mreqs		[0:NM-1];
	wire	[F_LGDEPTH-1:0]	f_macks		[0:NM-1];
	wire	[F_LGDEPTH-1:0]	f_moutstanding	[0:NM-1];
	//
	// as well as the slaves that we drive ourselves
	wire	[F_LGDEPTH-1:0]	f_sreqs		[0:NS-1];
	wire	[F_LGDEPTH-1:0]	f_sacks		[0:NS-1];
	wire	[F_LGDEPTH-1:0]	f_soutstanding	[0:NS-1];


	initial	assert(!OPT_STARVATION_TIMEOUT || OPT_TIMEOUT > 0);

	initial	f_past_valid = 0;
	always @(posedge i_clk)
		f_past_valid = 1'b1;

	always @(*)
	if (!f_past_valid)
		assume(i_reset);

	generate for(N=0; N<NM; N=N+1)
	begin
		always @(*)
		if (f_past_valid)
		for(iN=N+1; iN<NM; iN=iN+1)
			// Can't grant the same channel to two separate
			// masters.  This applies to all but the error or
			// no-slave-selected channel
			assert((grant[N][NS-1:0] & grant[iN][NS-1:0])==0);

		for(M=1; M<=NS; M=M+1)
		begin
			// Can't grant two channels to the same master
			always @(*)
			if (f_past_valid && grant[N][M])
				assert(grant[N][M-1:0] == 0);
		end


		always @(*)
		if (&w_mpending[N])
			assert(o_merr[N] || m_stall[N]);

		reg	checkgrant;
		always @(*)
		if (f_past_valid)
		begin
			checkgrant = 0;
			for(iM=0; iM<NS; iM=iM+1)
				if (grant[N][iM])
					checkgrant = 1;
			if (grant[N][NS])
				checkgrant = 1;

			assert(checkgrant == mgrant[N]);
		end

	end endgenerate

	// Double check the grant mechanism and its dependent variables
	generate for(N=0; N<NM; N=N+1)
	begin : CHECK_GRANTS

		for(M=0; M<NS; M=M+1)
		begin
			always @(*)
			if ((f_past_valid)&&grant[N][M])
			begin
				assert(mgrant[N]);
				assert(mindex[N] == M);
				assert(sgrant[M]);
				assert(sindex[M] == N);
			end
		end
	end endgenerate

	generate for(M=0; M<NS; M=M+1)
	begin : CHECK_SGRANT
		reg	f_sgrant;

		always @(*)
		if (sgrant[M])
			assert(grant[sindex[M]][M]);

		always @(*)
		begin
			f_sgrant = 0;
			for(iN=0; iN<NM; iN=iN+1)
			if (grant[iN][M])
				f_sgrant = 1;
		end

		always @(*)
			assert(sgrant[M] == f_sgrant);
	end endgenerate

	// Double check the timeout flags for consistency
	generate for(N=0; N<NM; N=N+1)
	begin
		always @(*)
		if (f_past_valid)
		begin
			assert(mempty[N] == (w_mpending[N] == 0));
			assert(mnearfull[N]==(&w_mpending[N][LGMAXBURST-1:1]));
			assert(mfull[N] == (&w_mpending[N]));
		end
	end endgenerate

`ifdef	VERIFIC
	//
	// The Verific parser is currently broken, and doesn't allow
	// initial assumes or asserts.  The following lines get us around that
	//
	always @(*)
	if (!f_past_valid)
		assume(sgrant == 0);

	generate for(M=0; M<NS; M=M+1)
	begin
		always @(*)
		if (!f_past_valid)
		begin
			assume(o_scyc[M] == 0);
			assume(o_sstb[M] == 0);
			assume(sgrant[M] == 0);
		end
	end endgenerate

	generate for(N=0; N<NM; N=N+1)
	begin
		always @(*)
		if (!f_past_valid)
		begin
			assume(grant[N] == 0);
			assume(mgrant[N] == 0);
		end
	end endgenerate
`endif

	////////////////////////////////////////////////////////////////////////
	//
	//	BUS CHECK
	//
	// Verify that every channel, whether master or slave, follows the rules
	// of the WB road.
	//
	////////////////////////////////////////////////////////////////////////
	generate for(N=0; N<NM; N=N+1)
	begin : WB_SLAVE_CHECK

		fwb_slave #(
			.AW(AW), .DW(DW),
			.F_LGDEPTH(LGMAXBURST),
			.F_MAX_ACK_DELAY(0),
			.F_MAX_STALL(0)
			) slvi(i_clk, i_reset,
				i_mcyc[N], i_mstb[N], i_mwe[N],
				i_maddr[N*AW +: AW], i_mdata[N*DW +: DW],
				i_msel[N*(DW/8) +: (DW/8)],
			o_mack[N], o_mstall[N], o_mdata[N*DW +: DW], o_merr[N],
			f_mreqs[N], f_macks[N], f_moutstanding[N]);

		always @(*)
		if ((f_past_valid)&&(grant[N][NS]))
			assert(f_moutstanding[N] <= 1);

		always @(*)
		if (f_past_valid && grant[N][NS] && i_mcyc[N])
			assert(m_stall[N] || o_merr[N]);

		always @(posedge i_clk)
		if (f_past_valid && $past(!i_reset && i_mstb[N] && o_mstall[N]))
			assume($stable(i_mdata[N*DW +: DW]));
	end endgenerate

	generate for(M=0; M<NS; M=M+1)
	begin : WB_MASTER_CHECK
		fwb_master #(
			.AW(AW), .DW(DW),
			.F_LGDEPTH(LGMAXBURST),
			.F_MAX_ACK_DELAY(F_MAX_DELAY),
			.F_MAX_STALL(2)
			) mstri(i_clk, i_reset,
				o_scyc[M], o_sstb[M], o_swe[M],
				o_saddr[M*AW +: AW], o_sdata[M*DW +: DW],
				o_ssel[M*(DW/8) +: (DW/8)],
			i_sack[M], i_sstall[M], s_data[M], i_serr[M],
			f_sreqs[M], f_sacks[M], f_soutstanding[M]);
	end endgenerate

	////////////////////////////////////////////////////////////////////////
	//
	////////////////////////////////////////////////////////////////////////
	generate for(N=0; N<NM; N=N+1)
	begin : CHECK_OUTSTANDING

		always @(*)
		if (mfull[N])
			assert(m_stall[N]);

		always @(posedge i_clk)
		if (i_mcyc[N])
			assert(f_moutstanding[N] == w_mpending[N]
				+((OPT_BUFFER_DECODER & dcd_stb[N]) ? 1:0));

		reg	[LGMAXBURST:0]	n_outstanding;
		always @(*)
		if (i_mcyc[N])
			assert(f_moutstanding[N] >=
				((OPT_BUFFER_DECODER && dcd_stb[N]) ? 1:0)
				+ (o_mack[N] && OPT_DBLBUFFER) ? 1:0);

		always @(*)
			n_outstanding = f_moutstanding[N]
				- ((OPT_BUFFER_DECODER && dcd_stb[N]) ? 1:0)
				- ((o_mack[N] && OPT_DBLBUFFER) ? 1:0);

		always @(posedge i_clk)
		if (i_mcyc[N] && !mgrant[N] && !o_merr[N])
			assert(f_moutstanding[N]
				== ((OPT_BUFFER_DECODER & dcd_stb[N]) ? 1:0));

		else if (i_mcyc[N] && mgrant[N] && !i_reset)
		for(iM=0; iM<NS; iM=iM+1)
		if (grant[N][iM] && o_scyc[iM] && !i_serr[iM] && !o_merr[N])
			assert(n_outstanding
				== {1'b0,f_soutstanding[iM]}
					+(o_sstb[iM] ? 1:0));

		always @(*)
		if (!i_reset)
		begin
			for(iM=0; iM<NS; iM=iM+1)
			if (grant[N][iM] && i_mcyc[N])
			begin
				if (f_soutstanding[iM] > 0)
					assert(i_mwe[N] == o_swe[iM]);
				if (o_sstb[iM])
					assert(i_mwe[N] == o_swe[iM]);
				if (o_mack[N])
					assert(i_mwe[N] == o_swe[iM]);
				if (o_scyc[iM] && i_sack[iM])
					assert(i_mwe[N] == o_swe[iM]);
				if (o_merr[N] && !timed_out[N])
					assert(i_mwe[N] == o_swe[iM]);
				if (o_scyc[iM] && i_serr[iM])
					assert(i_mwe[N] == o_swe[iM]);
			end
		end

		always @(*)
		if (!i_reset && OPT_BUFFER_DECODER && i_mcyc[N])
		begin
			if (dcd_stb[N])
				assert(i_mwe[N] == m_we[N]);
		end

	end endgenerate

	generate for(M=0; M<NS; M=M+1)
	begin
		always @(posedge i_clk)
		if (!$past(sgrant[M]))
			assert(!o_scyc[M]);
	end endgenerate

	////////////////////////////////////////////////////////////////////////
	//
	//	CONTRACT SECTION
	//
	// Here's the contract, in two parts:
	//
	//	1. Should ever a master (any master) wish to read from a slave
	//		(any slave), he should be able to read a known value
	//		from that slave (any value) from any arbitrary address
	//		he might wish to read from (any address)
	//
	//	2. Should ever a master (any master) wish to write to a slave
	//		(any slave), he should be able to write the exact
	//		value he wants (any value) to the exact address he wants
	//		(any address)
	//
	//	special_master	is an arbitrary constant chosen by the solver,
	//		which can reference *any* possible master
	//	special_address	is an arbitrary constant chosen by the solver,
	//		which can reference *any* possible address the master
	//		might wish to access
	//	special_value	is an arbitrary value (at least during
	//		induction) representing the current value within the
	//		slave at the given address
	//
	//
	////////////////////////////////////////////////////////////////////////
	//
	// Now let's pay attention to a special bus master and a special
	// address referencing a special bus slave.  We'd like to assert
	// that we can access the values of every slave from every master.
	(* anyconst *) reg	[(NM<=1)?0:(LGNM-1):0]	special_master;
			reg	[(NS<=1)?0:(LGNS-1):0]	special_slave;
	(* anyconst *) reg	[AW-1:0]	special_address;
			reg	[DW-1:0]	special_value;

	always @(*)
	if (NM <= 1)
		assume(special_master == 0);
	always @(*)
	if (NS <= 1)
		assume(special_slave == 0);

	//
	// Decode the special address to discover the slave associated with it
	always @(*)
	begin
		special_slave = NS;
		for(iM=0; iM<NS; iM = iM+1)
		begin
			if (((special_address ^ SLAVE_ADDR[iM*AW +: AW])
					&SLAVE_MASK[iM*AW +: AW]) == 0)
				special_slave = iM;
		end
	end

	generate if (NS > 1)
	begin : DOUBLE_ADDRESS_CHECK
		//
		// Check that no slave address has been assigned twice.
		// This check only needs to be done once at the beginning
		// of the run, during the BMC section.
		reg	address_found;

		always @(*)
		if (!f_past_valid)
		begin
			address_found = 0;
			for(iM=0; iM<NS; iM = iM+1)
			begin
				if (((special_address ^ SLAVE_ADDR[iM*AW +: AW])
						&SLAVE_MASK[iM*AW +: AW]) == 0)
				begin
					assert(address_found == 0);
					address_found = 1;
				end
			end
		end

	end endgenerate
	//
	// Let's assume this slave will acknowledge any request on the next
	// bus cycle after the stall goes low.  Further, lets assume that
	// it never creates an error, and that it always responds to our special
	// address with the special data value given above.  To do this, we'll
	// also need to make certain that the special value will change
	// following any write.
	//
	// These are the "assumptions" associated with our fictitious slave.
`ifdef	VERIFIC
	always @(*)
	if (!f_past_valid)
		assume(special_value == 0);
`else
	initial	assume(special_value == 0);
`endif
	always @(posedge i_clk)
	if (special_slave < NS)
	begin
		if ($past(o_sstb[special_slave] && !i_sstall[special_slave]))
		begin
			assume(i_sack[special_slave]);

			if ($past(!o_swe[special_slave])
					&&($past(o_saddr[special_slave*AW +: AW]) == special_address))
				assume(i_sdata[special_slave*DW+: DW]
						== special_value);
		end else
			assume(!i_sack[special_slave]);
		assume(!i_serr[special_slave]);

		if (o_scyc[special_slave])
			assert(f_soutstanding[special_slave]
				== i_sack[special_slave]);

		if (o_sstb[special_slave] && !i_sstall[special_slave]
			&& o_swe[special_slave])
		begin
			for(iM=0; iM < DW/8; iM=iM+1)
			if (o_ssel[special_slave * DW/8 + iM])
				special_value[iM*8 +: 8] <= o_sdata[special_slave * DW + iM*8 +: 8];
		end
	end

	//
	// Now its time to make some assertions.  Specifically, we want to
	// assert that any time we read from this special slave, the special
	// value is returned.
	reg	[2:0]	f_read_seq;
	reg		f_read_ack, f_read_sstall;

	initial	f_read_sstall = 0;
	always @(posedge i_clk)
		f_read_sstall <= s_stall[special_slave];

	always @(*)
		f_read_ack = (f_read_seq[2] || ((!OPT_DBLBUFFER)&&f_read_seq[1]
					&& !f_read_sstall));
	initial	f_read_seq = 0;
	always @(posedge i_clk)
	if ((special_master < NM)&&(special_slave < NS)
			&&(i_mcyc[special_master])
			&&(!timed_out[special_master]))
	begin
		f_read_seq <= 0;
		if ((grant[special_master][special_slave])
			&&(m_stb[special_master])
			&&(m_addr[special_master] == special_address)
			&&(!m_we[special_master])
			)
		begin
			f_read_seq[0] <= 1;
		end

		if (|f_read_seq)
		begin
			assert(grant[special_master][special_slave]);
			assert(mgrant[special_master]);
			assert(sgrant[special_slave]);
			assert(mindex[special_master] == special_slave);
			assert(sindex[special_slave] == special_master);
			assert(!o_merr[special_master]);
		end

		if (f_read_seq[0] && !$past(s_stall[special_slave]))
		begin
			assert(o_scyc[special_slave]);
			assert(o_sstb[special_slave]);
			assert(!o_swe[special_slave]);
			assert(o_saddr[special_slave*AW +: AW] == special_address);

			f_read_seq[1] <= 1;

		end else if (f_read_seq[0] && $past(s_stall[special_slave]))
		begin
			assert($stable(m_stb[special_master]));
			assert(!m_we[special_master]);
			assert(m_addr[special_master] == special_address);

			f_read_seq[0] <= 1;
		end

		if (f_read_seq[1] && $past(s_stall[special_slave]))
		begin
			assert(o_scyc[special_slave]);
			assert(o_sstb[special_slave]);
			assert(!o_swe[special_slave]);
			assert(o_saddr[special_slave*AW +: AW] == special_address);
			f_read_seq[1] <= 1;
		end else if (f_read_seq[1] && !$past(s_stall[special_slave]))
		begin
			assert(i_sack[special_slave]);
			assert(i_sdata[special_slave*DW +: DW] == $past(special_value));
			if (OPT_DBLBUFFER)
				f_read_seq[2] <= 1;
		end

		if (f_read_ack)
		begin
			assert(o_mack[special_master]);
			assert(o_mdata[special_master * DW +: DW]
				== $past(special_value,2));
		end
	end else
		f_read_seq <= 0;

	always @(*)
		cover(i_mcyc[special_master] && f_read_ack);


	//
	// Let's try a write assertion now.  Specifically, on any request to
	// write to our special address, we want to assert that the special
	// value at that address can be written.
	reg	[2:0]	f_write_seq;
	reg		f_write_ack, f_write_sstall;

	initial	f_write_sstall = 0;
	always @(posedge i_clk)
		f_write_sstall = s_stall[special_slave];

	always @(*)
		f_write_ack = (f_write_seq[2]
				|| ((!OPT_DBLBUFFER)&&f_write_seq[1]
					&& !f_write_sstall));
	initial	f_write_seq = 0;
	always @(posedge i_clk)
	if ((special_master < NM)&&(special_slave < NS)
			&&(i_mcyc[special_master])
			&&(!timed_out[special_master]))
	begin
		f_write_seq <= 0;
		if ((grant[special_master][special_slave])
			&&(m_stb[special_master])
			&&(m_addr[special_master] == special_address)
			&&(m_we[special_master]))
		begin
			// Our write sequence begins when our special master
			// has access to the bus, *and* he is trying to write
			// to our special address.
			f_write_seq[0] <= 1;
		end

		if (|f_write_seq)
		begin
			assert(grant[special_master][special_slave]);
			assert(mgrant[special_master]);
			assert(sgrant[special_slave]);
			assert(mindex[special_master] == special_slave);
			assert(sindex[special_slave] == special_master);
			assert(!o_merr[special_master]);
		end

		if (f_write_seq[0] && !$past(s_stall[special_slave]))
		begin
			assert(o_scyc[special_slave]);
			assert(o_sstb[special_slave]);
			assert(o_swe[special_slave]);
			assert(o_saddr[special_slave*AW +: AW] == special_address);
			assert(o_sdata[special_slave*DW +: DW]
				== $past(m_data[special_master]));
			assert(o_ssel[special_slave*DW/8 +: DW/8]
				== $past(m_sel[special_master]));

			f_write_seq[1] <= 1;

		end else if (f_write_seq[0] && $past(s_stall[special_slave]))
		begin
			assert($stable(m_stb[special_master]));
			assert(m_we[special_master]);
			assert(m_addr[special_master] == special_address);
			assert($stable(m_data[special_master]));
			assert($stable(m_sel[special_master]));

			f_write_seq[0] <= 1;
		end

		if (f_write_seq[1] && $past(s_stall[special_slave]))
		begin
			assert(o_scyc[special_slave]);
			assert(o_sstb[special_slave]);
			assert(o_swe[special_slave]);
			assert(o_saddr[special_slave*AW +: AW] == special_address);
			assert($stable(o_sdata[special_slave*DW +: DW]));
			assert($stable(o_ssel[special_slave*DW/8 +: DW/8]));
			f_write_seq[1] <= 1;
		end else if (f_write_seq[1] && !$past(s_stall[special_slave]))
		begin
			for(iM=0; iM<DW/8; iM=iM+1)
			begin
				if ($past(o_ssel[special_slave * DW/8 + iM]))
					assert(special_value[iM*8 +: 8]
						== $past(o_sdata[special_slave*DW+iM*8 +: 8]));
			end

			assert(i_sack[special_slave]);
			if (OPT_DBLBUFFER)
				f_write_seq[2] <= 1;
		end

		if (f_write_seq[2] || ((!OPT_DBLBUFFER) && f_write_seq[1]
					&& !$past(s_stall[special_slave])))
			assert(o_mack[special_master]);
	end else
		f_write_seq <= 0;

	always @(*)
		cover(i_mcyc[special_master] && f_write_ack);

	////////////////////////////////////////////////////////////////////////
	//
	// (draft) full connectivity check
	//
	////////////////////////////////////////////////////////////////////////
	reg	[NM-1:0]	f_m_ackd;
	reg	[NS-1:0]	f_s_ackd;
	reg			f_cvr_aborted;

	initial	f_cvr_aborted = 0;
	always @(posedge i_clk)
	if (!f_past_valid || i_reset)
		f_cvr_aborted <= 0;
	else for(iN=0; iN<NM; iN=iN+1)
	begin
		if (request[iN][NS])
			f_cvr_aborted = 1;
		if ($fell(i_mcyc[iN]))
		begin
			if (f_macks[iN] != f_mreqs[iN])
				f_cvr_aborted = 1;
		end
	end

	initial	f_m_ackd = 0;
	generate for (N=0; N<NM; N=N+1)
	begin

		always @(posedge i_clk)
		if (i_reset)
			f_m_ackd[N] <= 0;
		else if (o_mack[N])
			f_m_ackd[N] <= 1'b1;

	end endgenerate

	always @(posedge i_clk)
		cover(!f_cvr_aborted && (&f_m_ackd));

	generate if (NM > 1)
	begin

		always @(posedge i_clk)
			cover(!f_cvr_aborted && (&f_m_ackd[1:0]));

	end endgenerate

	initial	f_s_ackd = 0;
	generate for (M=0; M<NS; M=M+1)
	begin

		always @(posedge i_clk)
		if (i_reset)
			f_s_ackd[M] <= 1'b0;
		else if (sgrant[M] && o_mack[sindex[M]])
			f_s_ackd[M] <= 1'b1;

	end endgenerate

	always @(posedge i_clk)
		cover(!f_cvr_aborted && (&f_s_ackd[NS-1:0]));

	generate if (NS > 1)
	begin

		always @(posedge i_clk)
			cover(!f_cvr_aborted && (&f_s_ackd[NS-1:0]));

	end endgenerate

`endif
endmodule
`ifndef	YOSYS
`default_nettype wire
`endif