From 3038edc09a2eb15762f2e58533f429489107520b Mon Sep 17 00:00:00 2001
From: Alejandro Soto <alejandro@34project.org>
Date: Wed, 6 Mar 2024 02:38:24 -0600
Subject: rtl/wb2axip: add to version control

---
 rtl/wb2axip/axildouble.v | 734 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 734 insertions(+)
 create mode 100644 rtl/wb2axip/axildouble.v

(limited to 'rtl/wb2axip/axildouble.v')

diff --git a/rtl/wb2axip/axildouble.v b/rtl/wb2axip/axildouble.v
new file mode 100644
index 0000000..ddaedb6
--- /dev/null
+++ b/rtl/wb2axip/axildouble.v
@@ -0,0 +1,734 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// 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
-- 
cgit v1.2.3