////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	axildouble.v
// {{{
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	Create a special slave which can be used to reduce crossbar
//		logic for multiple simplified slaves.  This is a companion
//	core to the similar axilsingle core, but allowing the slave to
//	decode the clock between multiple possible addresses.
//
//	To use this, the slave must follow specific (simplified AXI) rules:
//
//	Write interface
//	1. The slave must guarantee that AWREADY == WREADY = 1
//		(This core doesn't have AWREADY or WREADY inputs)
//	2. The slave must also guarantee that BVALID == $past(AWVALID)
//		(This core internally generates BVALID)
//	3. The controller will guarantee that AWVALID == WVALID
//		(You can connect AWVALID to WVALID when connecting to your core)
//	4. The controller will also guarantee that BREADY = 1
//		(This core doesn't have a BVALID input)
//
//	Read interface
//	1. The slave must guarantee that ARREADY == 1
//		(This core doesn't have an ARREADY input)
//	2. The slave must also guarantee that RVALID == $past(ARVALID)
//		(This core doesn't have an RVALID input, trusting the slave
//			instead)
//	3. The controller will guarantee that RREADY = 1
//		(This core doesn't have an RREADY output)
//
//
//	Why?  This simplifies slave logic.  Slaves may interact with the bus
//	using only the logic below:
//
//		always @(posedge S_AXI_ACLK)
//		if (AWVALID) case(AWADDR)
//		R1:	slvreg_1 <= WDATA;
//		R2:	slvreg_2 <= WDATA;
//		R3:	slvreg_3 <= WDATA;
//		R4:	slvreg_4 <= WDATA;
//		endcase
//
//		always @(*)
//			BRESP = 2'b00;
//
//		always @(posedge S_AXI_ACLK)
//		if (ARVALID)
//		case(ARADDR)
//			R1: RDATA <= slvreg_1;
//			R2: RDATA <= slvreg_2;
//			R3: RDATA <= slvreg_3;
//			R4: RDATA <= slvreg_4;
//		endcase
//
//		always @(*)
//			RRESP = 2'b00;
//
//	This core will then keep track of the more complex bus logic,
//	simplifying both slaves and connection logic.  Slaves with the more
//	complicated (and proper/accurate) logic, that follow the rules above,
//	should have no problems with this additional logic.
//
// Performance:
//
//	This core can sustain one read/write per clock as long as the upstream
//	AXI master keeps S_AXI_[BR]READY high.  If S_AXI_[BR]READY ever drops,
//	there's some flexibility provided by the return FIFO, so the master
//	might not notice a drop in throughput until the FIFO fills.
//
//	The more practical performance measure is the latency of this core.
//	That I've measured at four clocks.
//
// 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
// `ifdef	VERILATOR
// `define	FORMAL
// `endif
// }}}
module	axildouble #(
		// {{{
		parameter integer C_AXI_DATA_WIDTH = 32,
		parameter integer C_AXI_ADDR_WIDTH = 32,
		//
		// NS is the number of slave interfaces
		parameter	NS = 8,
		//
		//
		parameter	[NS*C_AXI_ADDR_WIDTH-1:0]	SLAVE_ADDR = {
			{ 3'b111, {(C_AXI_ADDR_WIDTH-3){1'b0}} },
			{ 3'b110, {(C_AXI_ADDR_WIDTH-3){1'b0}} },
			{ 3'b101, {(C_AXI_ADDR_WIDTH-3){1'b0}} },
			{ 3'b100, {(C_AXI_ADDR_WIDTH-3){1'b0}} },
			{ 3'b011, {(C_AXI_ADDR_WIDTH-3){1'b0}} },
			{ 3'b010, {(C_AXI_ADDR_WIDTH-3){1'b0}} },
			{ 4'b0001,{(C_AXI_ADDR_WIDTH-4){1'b0}} },
			{ 4'b0000,{(C_AXI_ADDR_WIDTH-4){1'b0}} } },
		//
		//
		parameter	[NS*C_AXI_ADDR_WIDTH-1:0]	SLAVE_MASK =
			(NS <= 1) ? 0
			: {	{(NS-2){ 3'b111,{(C_AXI_ADDR_WIDTH-3){1'b0}} }},
				{(2){   4'b1111,{(C_AXI_ADDR_WIDTH-4){1'b0}} }}
			},
		//
		//
		// LGFLEN specifies the log (based two) of the number of
		// transactions that may need to be held outstanding internally.
		// If you really want high throughput, and if you expect any
		// back pressure at all, then increase LGFLEN.  Otherwise the
		// default value of 3 (FIFO size = 8) should be sufficient
		// to maintain full loading
		parameter	LGFLEN=3,
		//
		// 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 = 0
		// }}}
	) (
		// {{{
		input	wire				S_AXI_ACLK,
		input	wire				S_AXI_ARESETN,
		//
		input	wire				S_AXI_AWVALID,
		output	wire				S_AXI_AWREADY,
		input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_AWADDR,
		input	wire	[3-1:0]			S_AXI_AWPROT,
		//
		input	wire				S_AXI_WVALID,
		output	wire				S_AXI_WREADY,
		input	wire	[C_AXI_DATA_WIDTH-1:0]	S_AXI_WDATA,
		input	wire [C_AXI_DATA_WIDTH/8-1:0]	S_AXI_WSTRB,
		//
		output	wire	[2-1:0]			S_AXI_BRESP,
		output	wire				S_AXI_BVALID,
		input	wire				S_AXI_BREADY,
		//
		input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_ARADDR,
		input	wire	[3-1:0]			S_AXI_ARPROT,
		input	wire				S_AXI_ARVALID,
		output	wire				S_AXI_ARREADY,
		//
		output	wire	[C_AXI_DATA_WIDTH-1:0]	S_AXI_RDATA,
		output	wire	[2-1:0]			S_AXI_RRESP,
		output	wire				S_AXI_RVALID,
		input	wire				S_AXI_RREADY,
		//
		//
		//
		output	wire	[NS-1:0]		M_AXI_AWVALID,
		output	wire [C_AXI_ADDR_WIDTH-1:0]	M_AXI_AWADDR,
		output	wire	[3-1:0]			M_AXI_AWPROT,
		//
		output	wire	[C_AXI_DATA_WIDTH-1:0]	M_AXI_WDATA,
		output	wire [C_AXI_DATA_WIDTH/8-1:0]	M_AXI_WSTRB,
		//
		input	wire	[NS*2-1:0]		M_AXI_BRESP,
		//
		output	wire	[NS-1:0]		M_AXI_ARVALID,
		output	wire [C_AXI_ADDR_WIDTH-1:0]	M_AXI_ARADDR,
		output	wire	[3-1:0]			M_AXI_ARPROT,
		//
		input	wire [NS*C_AXI_DATA_WIDTH-1:0]	M_AXI_RDATA,
		input	wire	[NS*2-1:0]		M_AXI_RRESP
		// }}}
	);

	//
	// AW, and DW, are short-hand abbreviations used locally.
	localparam	AW = C_AXI_ADDR_WIDTH;
	localparam	DW = C_AXI_DATA_WIDTH;
	localparam	LGNS = $clog2(NS);
	//
	localparam	INTERCONNECT_ERROR = 2'b11;

	////////////////////////////////////////////////////////////////////////
	//
	// Write logic:
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	wire			awskid_valid, bffull, bempty, write_awskidready,
				dcd_awvalid;
	reg			write_bvalid, write_response;
	reg			bfull, write_wready, write_no_index;
	wire	[NS:0]		wdecode;
	wire	[AW-1:0]	awskid_addr;
	wire	[AW-1:0]	m_awaddr;
	reg	[LGNS-1:0]	write_windex, write_bindex;
	wire	[3-1:0]		awskid_prot, m_axi_awprot;
	wire	[LGFLEN:0]	bfill;
	reg	[LGFLEN:0]	write_count;
	reg	[1:0]		write_resp;
	integer			k;

	skidbuffer #(.OPT_LOWPOWER(OPT_LOWPOWER), .OPT_OUTREG(0),
			.DW(AW+3))
	awskid(	.i_clk(S_AXI_ACLK),
		.i_reset(!S_AXI_ARESETN),
		.i_valid(S_AXI_AWVALID),
			.o_ready(S_AXI_AWREADY),
			.i_data({ S_AXI_AWPROT, S_AXI_AWADDR }),
		.o_valid(awskid_valid), .i_ready(write_awskidready),
			.o_data({ awskid_prot, awskid_addr }));
	
	wire		awskd_stall;

	addrdecode #(.AW(AW), .DW(3), .NS(NS),
		.SLAVE_ADDR(SLAVE_ADDR),
		.SLAVE_MASK(SLAVE_MASK),
		.OPT_REGISTERED(1'b1))
	wraddr(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
		.i_valid(awskid_valid && write_awskidready), .o_stall(awskd_stall),
			.i_addr(awskid_addr),
			.i_data(awskid_prot),
		.o_valid(dcd_awvalid), .i_stall(!S_AXI_WVALID),
			.o_decode(wdecode), .o_addr(m_awaddr),
			.o_data(m_axi_awprot));

	always @(*)
		write_wready = dcd_awvalid;
	assign	S_AXI_WREADY  = write_wready;
	assign	M_AXI_AWVALID = (S_AXI_WVALID) ? wdecode[NS-1:0] : 0;
	assign	M_AXI_AWADDR  = m_awaddr;
	assign	M_AXI_AWPROT  = m_axi_awprot;
	assign	M_AXI_WDATA   = S_AXI_WDATA;
	assign	M_AXI_WSTRB   = S_AXI_WSTRB;
	assign	write_awskidready = (S_AXI_WVALID || !S_AXI_WREADY) && !bfull;

	always @(*)
	begin
		write_windex = 0;
		for(k=0; k<NS; k=k+1)
		if (wdecode[k])
			write_windex = write_windex | k[LGNS-1:0];
	end

	always @(posedge S_AXI_ACLK)
	begin
		write_bindex <= write_windex;
		write_no_index <= wdecode[NS];
	end

	initial	{ write_response, write_bvalid } = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		{ write_response, write_bvalid } <= 0;
	else
		{ write_response, write_bvalid }
			<= { write_bvalid, (S_AXI_WVALID && S_AXI_WREADY) };

	always @(posedge S_AXI_ACLK)
	if (write_no_index)
		write_resp <= INTERCONNECT_ERROR;
	else
		write_resp <= M_AXI_BRESP[2*write_bindex +: 2];

	initial	write_count = 0;
	initial	bfull = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	begin
		write_count <= 0;
		bfull <= 0;
	end else case({ (awskid_valid && write_awskidready),
			(S_AXI_BVALID & S_AXI_BREADY) })
	2'b01:	begin
		write_count <= write_count - 1;
		bfull <= 1'b0;
		end
	2'b10:	begin
		write_count <= write_count + 1;
		bfull <= (&write_count[LGFLEN-1:0]);
		end
	default: begin end
	endcase

`ifdef	FORMAL
	always @(*)
		assert(write_count <= { 1'b1, {(LGFLEN){1'b0}} });
	always @(*)
		assert(bfull == (write_count == { 1'b1, {(LGFLEN){1'b0}} }));
`endif

	sfifo #(.BW(2), .OPT_ASYNC_READ(0), .LGFLEN(LGFLEN))
	bfifo ( .i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
		.i_wr(write_response), .i_data(write_resp), .o_full(bffull),
			.o_fill(bfill),
		.i_rd(S_AXI_BVALID && S_AXI_BREADY), .o_data(S_AXI_BRESP),
			.o_empty(bempty));

`ifdef	FORMAL
	always @(*)
		assert(write_count == bfill
			+ (write_response ? 1:0)
			+ (write_bvalid ? 1:0)
			+ (write_wready ? 1:0));

`ifdef	VERIFIC
	always @(*)
	if (bfifo.f_first_in_fifo)
		assert(bfifo.f_first_data != 2'b01);
	always @(*)
	if (bfifo.f_second_in_fifo)
		assert(bfifo.f_second_data != 2'b01);
	always @(*)
	if (!bempty && (!bfifo.f_first_in_fifo
				|| bfifo.rd_addr != bfifo.f_first_addr)
			&&(!bfifo.f_second_in_fifo
				|| bfifo.rd_addr != bfifo.f_second_addr))
		assume(S_AXI_BRESP != 2'b01);
`else
	always @(*)
	if (!bempty)
		assume(S_AXI_BRESP != 2'b01);
`endif
`endif

	assign	S_AXI_BVALID = !bempty;

`ifdef	FORMAL
	always @(*)
		assert(!bffull || !write_bvalid);
`endif

	////////////////////////////////////////////////////////////////////////
	//
	// Read logic
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	wire				rempty, rdfull;
	wire	[LGFLEN:0]		rfill;
	reg	[LGNS-1:0]		read_index, last_read_index;
	reg	[1:0]			read_resp;
	reg	[DW-1:0]		read_rdata;
	wire				read_rwait, arskd_stall;
	reg				read_rvalid, read_result, read_no_index;
	wire	[AW-1:0]		m_araddr;
	wire	[3-1:0]			m_axi_arprot;
	wire	[NS:0]			rdecode;

	addrdecode #(.AW(AW), .DW(3), .NS(NS),
		.SLAVE_ADDR(SLAVE_ADDR),
		.SLAVE_MASK(SLAVE_MASK),
		.OPT_REGISTERED(1'b1))
	rdaddr(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
		.i_valid(S_AXI_ARVALID && S_AXI_ARREADY), .o_stall(arskd_stall),
			.i_addr(S_AXI_ARADDR), .i_data(S_AXI_ARPROT),
		.o_valid(read_rwait), .i_stall(1'b0),
			.o_decode(rdecode), .o_addr(m_araddr),
			.o_data(m_axi_arprot));

	assign	M_AXI_ARVALID = rdecode[NS-1:0];
	assign	M_AXI_ARADDR  = m_araddr;
	assign	M_AXI_ARPROT  = m_axi_arprot;

	initial	{ read_result, read_rvalid } = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		{ read_result, read_rvalid } <= 2'b00;
	else
		{ read_result, read_rvalid } <= { read_rvalid, read_rwait };

	always @(*)
	begin
		read_index = 0;

		for(k=0; k<NS; k=k+1)
		if (rdecode[k])
			read_index = read_index | k[LGNS-1:0];
	end

	always @(posedge S_AXI_ACLK)
		last_read_index <= read_index;

	always @(posedge S_AXI_ACLK)
		read_no_index <= rdecode[NS];

	always @(posedge S_AXI_ACLK)
		read_rdata <= M_AXI_RDATA[DW*last_read_index +: DW];

	always @(posedge S_AXI_ACLK)
	if (read_no_index)
		read_resp <= INTERCONNECT_ERROR;
	else
		read_resp <= M_AXI_RRESP[2*last_read_index +: 2];

	reg			read_full;
	reg	[LGFLEN:0]	read_count;

	initial	{ read_count, read_full } = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		{ read_count, read_full } <= 0;
	else case({ S_AXI_ARVALID & S_AXI_ARREADY, S_AXI_RVALID & S_AXI_RREADY})
	2'b10: begin
		read_count <= read_count + 1;
		read_full  <= &read_count[LGFLEN-1:0];
		end
	2'b01: begin
		read_count <= read_count - 1;
		read_full <= 1'b0;
		end
	default: begin end
	endcase

`ifdef	FORMAL
	always @(*)
		assert(read_count <= { 1'b1, {(LGFLEN){1'b0}} });
	always @(*)
		assert(read_full == (read_count == { 1'b1, {(LGFLEN){1'b0}} }));
`endif
	assign	S_AXI_ARREADY = !read_full;

	sfifo #(.BW(DW+2), .OPT_ASYNC_READ(0), .LGFLEN(LGFLEN))
	rfifo ( .i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
		.i_wr(read_result), .i_data({ read_rdata, read_resp }),
			.o_full(rdfull), .o_fill(rfill),
		.i_rd(S_AXI_RVALID && S_AXI_RREADY),
			.o_data({ S_AXI_RDATA, S_AXI_RRESP }),.o_empty(rempty));

`ifdef	FORMAL
	always @(*)
		assert(read_count == rfill + read_result + read_rvalid + read_rwait);
`ifdef	VERIFIC
	always @(*)
	if (rfifo.f_first_in_fifo)
		assert(rfifo.f_first_data[1:0] != 2'b01);
	always @(*)
	if (rfifo.f_second_in_fifo)
		assert(rfifo.f_second_data[1:0] != 2'b01);
	always @(*)
	if (!rempty && (!rfifo.f_first_in_fifo
				|| rfifo.rd_addr != rfifo.f_first_addr)
			&&(!rfifo.f_second_in_fifo
				|| rfifo.rd_addr != rfifo.f_second_addr))
		assume(S_AXI_RRESP != 2'b01);
`else
	always @(*)
	if (!rempty)
		assume(S_AXI_RRESP != 2'b01);
`endif
`endif

	assign	S_AXI_RVALID = !rempty;

	// verilator lint_off UNUSED
	wire	unused;
	assign	unused = &{ 1'b0,
			bffull, rdfull, bfill, rfill,
			awskd_stall, arskd_stall };
	// verilator lint_on  UNUSED
`ifdef	FORMAL
	localparam	F_LGDEPTH = LGFLEN+1;
	reg	f_past_valid;
	reg	[F_LGDEPTH-1:0]	count_awr_outstanding, count_wr_outstanding,
				count_rd_outstanding;


	wire	[(F_LGDEPTH-1):0]	f_axi_awr_outstanding,
					f_axi_wr_outstanding,
					f_axi_rd_outstanding;

	wire	[1:0]	fm_axi_awr_outstanding [0:NS-1];
	wire	[1:0]	fm_axi_wr_outstanding [0:NS-1];
	wire	[1:0]	fm_axi_rd_outstanding [0:NS-1];

	reg [NS-1:0]	m_axi_rvalid, m_axi_bvalid;

	faxil_slave #(// .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
			.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
			// .F_OPT_NO_READS(1'b0),
			// .F_OPT_NO_WRITES(1'b0),
			.F_OPT_XILINX(1),
			.F_LGDEPTH(F_LGDEPTH))
		properties (
		.i_clk(S_AXI_ACLK),
		.i_axi_reset_n(S_AXI_ARESETN),
		//
		.i_axi_awvalid(S_AXI_AWVALID),
		.i_axi_awready(S_AXI_AWREADY),
		.i_axi_awaddr(S_AXI_AWADDR),
		.i_axi_awprot(S_AXI_AWPROT),
		//
		.i_axi_wvalid(S_AXI_WVALID),
		.i_axi_wready(S_AXI_WREADY),
		.i_axi_wdata(S_AXI_WDATA),
		.i_axi_wstrb(S_AXI_WSTRB),
		//
		.i_axi_bvalid(S_AXI_BVALID),
		.i_axi_bready(S_AXI_BREADY),
		.i_axi_bresp(S_AXI_BRESP),
		//
		.i_axi_arvalid(S_AXI_ARVALID),
		.i_axi_arready(S_AXI_ARREADY),
		.i_axi_araddr(S_AXI_ARADDR),
		.i_axi_arprot(S_AXI_ARPROT),
		//
		.i_axi_rvalid(S_AXI_RVALID),
		.i_axi_rready(S_AXI_RREADY),
		.i_axi_rdata(S_AXI_RDATA),
		.i_axi_rresp(S_AXI_RRESP),
		//
		.f_axi_rd_outstanding(f_axi_rd_outstanding),
		.f_axi_wr_outstanding(f_axi_wr_outstanding),
		.f_axi_awr_outstanding(f_axi_awr_outstanding));

	initial	f_past_valid = 1'b0;
	always @(posedge S_AXI_ACLK)
		f_past_valid <= 1'b1;

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

		faxil_master #(// .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
				.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
				.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
				// .F_OPT_NO_READS(1'b0),
				// .F_OPT_NO_WRITES(1'b0),
				.F_OPT_NO_RESET(1'b1),
				.F_LGDEPTH(2))
			properties (
			.i_clk(S_AXI_ACLK),
			.i_axi_reset_n(S_AXI_ARESETN),
			//
			.i_axi_awvalid(M_AXI_AWVALID[M]),
			.i_axi_awready(1'b1),
			.i_axi_awaddr(M_AXI_AWADDR),
			.i_axi_awprot(M_AXI_AWPROT),
			//
			.i_axi_wvalid(M_AXI_AWVALID[M]),
			.i_axi_wready(1'b1),
			.i_axi_wdata(M_AXI_WDATA[C_AXI_DATA_WIDTH-1:0]),
			.i_axi_wstrb(M_AXI_WSTRB[C_AXI_DATA_WIDTH/8-1:0]),
			//
			.i_axi_bvalid(m_axi_bvalid[M]),
			.i_axi_bready(1'b1),
			.i_axi_bresp(M_AXI_BRESP[2*M +: 2]),
			//
			.i_axi_arvalid(M_AXI_ARVALID[M]),
			.i_axi_arready(1'b1),
			.i_axi_araddr(M_AXI_ARADDR),
			.i_axi_arprot(M_AXI_ARPROT),
			//
			.i_axi_rdata(M_AXI_RDATA[M*C_AXI_DATA_WIDTH +: C_AXI_DATA_WIDTH]),
			.i_axi_rresp(M_AXI_RRESP[2*M +: 2]),
			.i_axi_rvalid(m_axi_rvalid[M]),
			.i_axi_rready(1'b1),
			//
			.f_axi_rd_outstanding(fm_axi_rd_outstanding[M]),
			.f_axi_wr_outstanding(fm_axi_wr_outstanding[M]),
			.f_axi_awr_outstanding(fm_axi_awr_outstanding[M]));

		initial	m_axi_bvalid <= 0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN)
			m_axi_bvalid[M] <= 1'b0;
		else
			m_axi_bvalid[M] <= M_AXI_AWVALID[M];

		initial	m_axi_rvalid[M] <= 0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN)
			m_axi_rvalid[M] <= 1'b0;
		else
			m_axi_rvalid[M] <= M_AXI_ARVALID[M];

		always @(*)
			assert(fm_axi_awr_outstanding[M] == fm_axi_wr_outstanding[M]);

		always @(*)
			assert(fm_axi_wr_outstanding[M]== (m_axi_bvalid[M] ? 1:0));

		always @(*)
			assert(fm_axi_rd_outstanding[M]== (m_axi_rvalid[M] ? 1:0));
	end endgenerate

	////////////////////////////////////////////////////////////////////////
	//
	// Properties necessary to pass induction
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	always @(*)
		assert(S_AXI_WREADY == (wdecode != 0));
`ifdef	VERIFIC
	always @(*)
		assert($onehot0(M_AXI_AWVALID));

	always @(*)
		assert($onehot0(m_axi_bvalid));

	always @(*)
		assert($onehot0(m_axi_rvalid));
`endif
	always @(*)
	begin
		count_awr_outstanding = 0;
		if (!S_AXI_AWREADY)
			count_awr_outstanding = count_awr_outstanding + 1;
		if (write_wready)
			count_awr_outstanding = count_awr_outstanding + 1;
		if (write_bvalid)
			count_awr_outstanding = count_awr_outstanding + 1;
		if (write_response)
			count_awr_outstanding = count_awr_outstanding + 1;
		count_awr_outstanding = count_awr_outstanding + bfill;
	end

	always @(*)
	if (S_AXI_ARESETN)
		assert(f_axi_awr_outstanding == count_awr_outstanding);

	always @(*)
	begin
		count_wr_outstanding = 0;
		if (write_bvalid)
			count_wr_outstanding = count_wr_outstanding + 1;
		if (write_response)
			count_wr_outstanding = count_wr_outstanding + 1;
		count_wr_outstanding = count_wr_outstanding + bfill;
	end

	always @(*)
	if (S_AXI_ARESETN)
		assert(f_axi_wr_outstanding == count_wr_outstanding);

	//
	//
	//
	always @(*)
	begin
		count_rd_outstanding = 0;
		if (read_rwait)
			count_rd_outstanding = count_rd_outstanding + 1;
		if (read_rvalid)
			count_rd_outstanding = count_rd_outstanding + 1;
		if (read_result)
			count_rd_outstanding = count_rd_outstanding + 1;
		count_rd_outstanding = count_rd_outstanding + rfill;
	end

	always @(*)
	if (S_AXI_ARESETN)
		assert(f_axi_rd_outstanding == count_rd_outstanding);


	////////////////////////////////////////////////////////////////////////
	//
	// Cover properties
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	reg	[3:0]	cvr_arvalids, cvr_awvalids, cvr_reads, cvr_writes;

	initial	cvr_awvalids = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_awvalids <= 0;
	else if (S_AXI_AWVALID && S_AXI_AWREADY && !(&cvr_awvalids))
		cvr_awvalids <= cvr_awvalids + 1;

	initial	cvr_arvalids = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_arvalids <= 0;
	else if (S_AXI_ARVALID && S_AXI_ARREADY && !(&cvr_arvalids))
		cvr_arvalids <= cvr_arvalids + 1;

	initial	cvr_writes = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_writes <= 0;
	else if (S_AXI_BVALID && S_AXI_BREADY && !(&cvr_writes))
		cvr_writes <= cvr_writes + 1;

	initial	cvr_reads = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		cvr_reads <= 0;
	else if (S_AXI_RVALID && S_AXI_RREADY && !(&cvr_arvalids))
		cvr_reads <= cvr_reads + 1;

	always @(*)
		cover(cvr_awvalids > 4);

	always @(*)
		cover(cvr_arvalids > 4);

	always @(*)
		cover(cvr_reads > 4);

	always @(*)
		cover(cvr_writes > 4);

	always @(*)
		cover((cvr_writes > 4) && (cvr_reads > 4));
`endif
endmodule
// `ifndef	YOSYS
// `default_nettype wire
// `endif