rtl: fix quartus errors: parser, synthesis, fitter

1 files changed, 0 insertions, 1406 deletions

diff --git a/rtl/wb2axip/axidouble.v b/rtl/wb2axip/axidouble.v
deleted file mode 100644
index 6842e71..0000000
--- a/rtl/wb2axip/axidouble.v
+++ /dev/null
@@ -1,1406 +0,0 @@
-////////////////////////////////////////////////////////////////////////////////
-//
-// Filename: 	axidouble.v
-// {{{
-// Project:	WB2AXIPSP: bus bridges and other odds and ends
-//
-// Purpose:	Create a special AXI slave which can be used to reduce crossbar
-//		logic for multiple simplified AXI slaves.  This is a companion
-//	core to the similar axisingle 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 controller will guarantee that AWVALID == WVALID
-//		(You can connect AWVALID to WVALID when connecting to your core)
-//	2. The controller will guarantee that AWID == 0 for the slave
-//		All ID logic will be handled internally
-//	3. The controller will guarantee that AWLEN == 0 and WLAST == 1
-//		Instead, the controller will handle all burst addressing
-//		internally
-//	4. This makes AWBURST irrelevant
-//	5. Other wires are simplified as well: AWLOCK=0, AWCACHE=3, AWQOS=0
-//	6. If OPT_EXCLUSIVE_ACCESS is set, the controller will handle lock
-//		logic internally
-//	7. The slave must guarantee that AWREADY == WREADY = 1
-//		(This core doesn't have AWREADY or WREADY inputs)
-//	8. The slave must also guarantee that BVALID == $past(AWVALID)
-//		(This core internally generates BVALID, and so the slave's
-//		BVALID return is actually ignored.)
-//	9. The controller will also guarantee that BREADY = 1
-//		(This core doesn't have a BVALID input)
-//
-//	The controller will maintain AWPROT in case the slave wants to
-//	disallow particular writes, and AWSIZE so the slave can know how many
-//	bytes are being accessed.
-//
-//	Read interface
-//	--------------------
-//	1. The controller will guarantee that RREADY = 1
-//		(This core doesn't have an RREADY output)
-//	2. The controller will guarantee that ARID = 0
-//		All IDs are handled internally
-//	3. The controller will guarantee that ARLEN == 0
-//		All burst logic is handled internally
-//	4. As before, this makes ARBURST irrelevant
-//	5. Other wires are simplified: ARLOCK=0, ARCACHE = 3, ARQOS=0, etc
-//	6. The slave must guarantee that RVALID == $past(ARVALID)
-//		The controller actually ignores RVALID--but to be a valid slave,
-//		this must be assumed.
-//	7. The slave must also guarantee that RLAST == 1 anytime RVALID
-//
-//	As with the write side, the controller will fill in ARSIZE and ARPROT.
-//	They may be used or ignored by the slave.
-//
-//	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; // OKAY
-//
-//		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; // OKAY
-//
-//	This core will then keep track of the more complex bus logic, locking,
-//	burst length, burst ID's, etc, 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:
-//
-//	Throughput: The slave can sustain one read/write per clock as long as
-//	the upstream 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.
-//
-//	Latency: This core will create a four clock latency on all requests.
-//
-//	Logic: Actual logic depends upon how this is set up and built.  As
-//	parameterized below, this core can fit within 639 Xilinx 6-LUTs and
-//	39 M-LUTs.
-//
-//	Narrow bursts: This core supports narrow bursts by nature.  Whether the
-//	subcores pay attention to WSTRB, AWSIZE, and ARSIZE is up to the
-//	subcore itself.
-//
-// 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	axidouble #(
-		// {{{
-		parameter integer C_AXI_DATA_WIDTH = 32,
-		parameter integer C_AXI_ADDR_WIDTH = 32,
-		parameter integer C_AXI_ID_WIDTH = 1,
-		//
-		// NS is the number of slave interfaces.  If you are interested
-		// in a single slave interface, checkout the demofull.v core
-		// in this same repository.
-		parameter	NS = 8,
-		//
-		// OPT_LOWPOWER is generated by the interconnect, so we need
-		// to define it here.
-		parameter [0:0]	OPT_LOWPOWER = 1'b0,
-		//
-		// Shorthand for address width, data width, and id width
-		// AW, and DW, are short-hand abbreviations used locally.
-		localparam AW = C_AXI_ADDR_WIDTH,
-		//
-		// Each of the slave interfaces has an address range.  The
-		// base address for each slave is given by AW bits of SLAVE_ADDR
-		// 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}} } },
-		//
-		//
-		// The relevant bits of the slave address are given in
-		// SLAVE_MASK below, at AW bits per slave.  To be valid,
-		// SLAVE_ADDR & ~SLAVE_MASK must be zero.  Only the masked
-		// bits will be used in any compare.
-		//
-		// Also, while not technically required, it is strongly
-		// recommended that the bottom 12-bits of each AW bits of
-		// the SLAVE_MASK bust be zero.
-		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}} }}
-			},
-		//
-		// 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,
-		//
-		// This core will handle exclusive access if
-		// OPT_EXCLUSIVE_ACCESS is set to one.  If set to 1, all
-		// subcores will have exclusive access applied.  There is no
-		// core-by-core means of enabling exclusive access at this time.
-		parameter [0:0]	OPT_EXCLUSIVE_ACCESS = 1'b1
-		// }}}
-	) (
-		// {{{
-		input	wire				S_AXI_ACLK,
-		input	wire				S_AXI_ARESETN,
-		//
-		// Write address channel coming from upstream
-		input	wire				S_AXI_AWVALID,
-		output	wire				S_AXI_AWREADY,
-		input	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_AWID,
-		input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_AWADDR,
-		input	wire	[8-1:0]			S_AXI_AWLEN,
-		input	wire	[3-1:0]			S_AXI_AWSIZE,
-		input	wire	[2-1:0]			S_AXI_AWBURST,
-		input	wire				S_AXI_AWLOCK,
-		input	wire	[4-1:0]			S_AXI_AWCACHE,
-		input	wire	[3-1:0]			S_AXI_AWPROT,
-		input	wire	[4-1:0]			S_AXI_AWQOS,
-		//
-		// Write data channel coming from upstream
-		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,
-		input	wire 				S_AXI_WLAST,
-		//
-		// Write responses sent back
-		output	wire				S_AXI_BVALID,
-		input	wire				S_AXI_BREADY,
-		output	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_BID,
-		output	wire	[2-1:0]			S_AXI_BRESP,
-		//
-		// Read address request channel from upstream
-		input	wire				S_AXI_ARVALID,
-		output	wire				S_AXI_ARREADY,
-		input	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_ARID,
-		input	wire	[C_AXI_ADDR_WIDTH-1:0]	S_AXI_ARADDR,
-		input	wire	[8-1:0]			S_AXI_ARLEN,
-		input	wire	[3-1:0]			S_AXI_ARSIZE,
-		input	wire	[2-1:0]			S_AXI_ARBURST,
-		input	wire				S_AXI_ARLOCK,
-		input	wire	[4-1:0]			S_AXI_ARCACHE,
-		input	wire	[3-1:0]			S_AXI_ARPROT,
-		input	wire	[4-1:0]			S_AXI_ARQOS,
-		//
-		// Read data return channel back upstream
-		output	wire				S_AXI_RVALID,
-		input	wire				S_AXI_RREADY,
-		output	wire	[C_AXI_ID_WIDTH-1:0]	S_AXI_RID,
-		output	wire	[C_AXI_DATA_WIDTH-1:0]	S_AXI_RDATA,
-		output	wire				S_AXI_RLAST,
-		output	wire	[2-1:0]			S_AXI_RRESP,
-		//
-		//
-		// Now for the simplified downstream interface to a series
-		// of downstream slaves.  All outgoing wires are shared between
-		// the slaves save the AWVALID and ARVALID signals.  Slave
-		// returns are not shared.
-		//
-		//
-		// Simplified Write address channel.
-		output	wire	[NS-1:0]		M_AXI_AWVALID,
-		// input wire M_AXI_AWREADY is assumed to be 1
-		output	wire	[0:0]			M_AXI_AWID,//    = 0
-		output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_AWADDR,
-		output	wire	[8-1:0]			M_AXI_AWLEN,//   = 0
-		output	wire	[3-1:0]			M_AXI_AWSIZE,
-		output	wire	[2-1:0]			M_AXI_AWBURST,//=INC
-		output	wire				M_AXI_AWLOCK,//  = 0
-		output	wire	[4-1:0]			M_AXI_AWCACHE,// = 0
-		output	wire	[3-1:0]			M_AXI_AWPROT,//  = 0
-		output	wire	[4-1:0]			M_AXI_AWQOS,//   = 0
-		//
-		// Simplified write data channel
-		output	wire	[NS-1:0]		M_AXI_WVALID,//=AWVALID
-		// input wire M_AXI_WVALID is *assumed* to be 1
-		output	wire	[C_AXI_DATA_WIDTH-1:0]	M_AXI_WDATA,
-		output	wire [C_AXI_DATA_WIDTH/8-1:0]	M_AXI_WSTRB,
-		output	wire				M_AXI_WLAST,//   = 1
-		//
-		// Simplified write response channel
-		// input wire M_AXI_BVALID is *assumed* to be
-		//	$past(M_AXI_AWVALID), and so ignored
-		output	wire				M_AXI_BREADY,//  = 1
-		input	wire	[NS*2-1:0]		M_AXI_BRESP,
-		// The controller handles BID, so this can be ignored as well
-		//
-		// Simplified read address channel
-		output	wire	[NS-1:0]		M_AXI_ARVALID,
-		// input wire M_AXI_ARREADY is assumed to be 1
-		output	wire	[0:0]			M_AXI_ARID,//    = 0
-		output	wire	[C_AXI_ADDR_WIDTH-1:0]	M_AXI_ARADDR,
-		output	wire	[8-1:0]			M_AXI_ARLEN,//   = 0
-		output	wire	[3-1:0]			M_AXI_ARSIZE,
-		output	wire	[2-1:0]			M_AXI_ARBURST,//=INC
-		output	wire				M_AXI_ARLOCK,//  = 0
-		output	wire	[4-1:0]			M_AXI_ARCACHE,// = 0
-		output	wire	[3-1:0]			M_AXI_ARPROT,//  = 0
-		output	wire	[4-1:0]			M_AXI_ARQOS,//   = 0
-		//
-		// Simplified read data return channel
-		// input wire M_AXI_RVALID is assumed to be $past(ARVALID,1)
-		output	wire				M_AXI_RREADY,//  = 1
-		input	wire [NS*C_AXI_DATA_WIDTH-1:0]	M_AXI_RDATA,
-		input	wire	[NS*2-1:0]		M_AXI_RRESP
-		// input wire M_AXI_RLAST is assumed to be 1
-		// }}}
-	);
-
-	// Signal declarations
-	// {{{
-	localparam DW = C_AXI_DATA_WIDTH;
-	localparam IW = C_AXI_ID_WIDTH;
-	// LGNS is the number of bits required in a slave index
-	localparam	LGNS = (NS <= 1) ? 1 : $clog2(NS);
-	//
-	localparam [1:0]	OKAY = 2'b00,
-				EXOKAY = 2'b01,
-				SLVERR = 2'b10,
-				INTERCONNECT_ERROR = 2'b11;
-	// localparam	ADDR_LSBS = $clog2(DW)-3;
-	//
-	reg	locked_burst, locked_write, lock_valid;
-
-	// Write signals
-	// {{{
-	wire			awskd_stall;
-	wire			awskid_valid, bffull, bempty, write_awskidready,
-				dcd_awvalid;
-	reg			write_bvalid, write_response;
-	reg			bfull, write_no_index;
-	wire	[NS:0]		raw_wdecode;
-	reg	[NS:0]		last_wdecode, wdecode;
-	wire	[AW-1:0]	m_awaddr;
-	wire	[LGNS-1:0]	write_windex;
-	reg	[LGNS-1:0]	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;
-	//
-	reg	[C_AXI_ID_WIDTH-1:0]	write_id, write_bid, write_retid;
-	reg	[C_AXI_ADDR_WIDTH-1:0]	write_addr;
-	wire	[C_AXI_ID_WIDTH-1:0]	awskid_awid;
-	wire	[C_AXI_ADDR_WIDTH-1:0]	awskid_awaddr, next_waddr;
-	reg			write_request, write_topofburst,
-				write_beat_bvalid;
-	reg	[3-1:0]		write_size;
-	reg	[2-1:0]		write_burst;
-	reg	[8-1:0]		write_len, write_awlen;
-	wire	[8-1:0]		awskid_awlen;
-	wire	[2-1:0]		awskid_awburst;
-	wire	[3-1:0]		awskid_awsize;
-	wire			awskid_awlock;
-	//
-	reg			write_top_beat;
-	// }}}
-
-	// Read signals
-	// {{{
-	wire				rempty, rdfull;
-	wire	[LGFLEN:0]		rfill;
-	wire	[LGNS-1:0]		read_index;
-	reg	[LGNS-1:0]		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;
-	reg	[AW-1:0]		araddr;
-	reg	[3-1:0]			arprot;
-	wire	[NS:0]			raw_rdecode;
-
-	reg	[C_AXI_ID_WIDTH-1:0]	arid, read_rvid, read_retid;
-	reg	[3-1:0]			arsize;
-	reg	[2-1:0]			arburst;
-	reg				arlock, read_rvlock;
-	reg				read_rvlast, read_retlast;
-	reg	[8-1:0]			arlen, rlen;
-	wire	[C_AXI_ADDR_WIDTH-1:0]	next_araddr;
-	wire				issue_read;
-	reg			read_full;
-	reg	[LGFLEN:0]	read_count;
-	reg			arvalid;
-	reg	[NS:0]		last_rdecode, rdecode;
-
-	wire	[0:0]	unused_pin;
-	// }}}
-
-	// }}}
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Unused wire assignments
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	assign	M_AXI_AWID  = 0;
-	assign	M_AXI_AWLEN = 0;
-	assign	M_AXI_AWBURST = 2'b00;
-	assign	M_AXI_AWLOCK  = 1'b0;
-	assign	M_AXI_AWCACHE = 4'h3;
-	// assign	M_AXI_AWPROT  = 3'h0;
-	assign	M_AXI_AWQOS   = 4'h0;
-	//
-	assign	M_AXI_WVALID  = M_AXI_AWVALID;
-	assign	M_AXI_WLAST   = 1'b1;
-	//
-	assign	M_AXI_BREADY  = 1'b1;
-	//
-	assign	M_AXI_ARID	= 1'b0;
-	assign	M_AXI_ARLEN	= 8'h0; // Burst of one beat
-	assign	M_AXI_ARBURST	= 2'b00; // INC
-	assign	M_AXI_ARLOCK	= 1'b0;
-	assign	M_AXI_ARCACHE	= 4'h3;
-	// assign	M_AXI_ARPROT	= 3'h0;
-	assign	M_AXI_ARQOS	= 4'h0;
-	//
-	assign	M_AXI_RREADY	= -1;
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Write logic:
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	//
-	// Incoming write address requests must go through a skidbuffer.  By
-	// keeping OPT_OUTREG == 0, this shouldn't cost us any time, but should
-	// instead buy us the ability to keep AWREADY high even if for reasons
-	// we can't act on AWVALID & AWREADY on the same cycle
-	skidbuffer #(
-		// {{{
-		.OPT_OUTREG(0),
-		.DW(C_AXI_ID_WIDTH+AW+8+3+2+1+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_AWID, S_AXI_AWADDR, S_AXI_AWLEN,
-				S_AXI_AWSIZE, S_AXI_AWBURST,
-				S_AXI_AWLOCK, S_AXI_AWPROT }),
-		.o_valid(awskid_valid), .i_ready(write_awskidready),
-			.o_data({ awskid_awid, awskid_awaddr, awskid_awlen,
-				awskid_awsize, awskid_awburst, awskid_awlock,
-				awskid_prot })
-		// }}}
-	);
-
-	// write_addr and other write_*
-	// {{{
-	// On any write address request (post-skidbuffer), copy down the details
-	// of that request.  Once these details are valid (i.e. on the next
-	// clock), S_AXI_WREADY will be true.
-	always @(posedge S_AXI_ACLK)
-	if (awskid_valid && write_awskidready)
-	begin
-		write_id    <= awskid_awid;
-		write_addr  <= awskid_awaddr;
-		write_size  <= awskid_awsize;
-		write_awlen <= awskid_awlen;
-		write_burst <= awskid_awburst;
-		// write_lock  <= awskid_awlock;
-
-		if (OPT_LOWPOWER && !awskid_valid)
-		begin
-			write_id    <= {(C_AXI_ID_WIDTH){1'b0}};
-			write_addr  <= {(C_AXI_ADDR_WIDTH){1'b0}};
-			write_size  <= 3'h0;
-			write_awlen <= 8'h0;
-			write_burst <= 2'b00;
-		end
-	end else if (S_AXI_WVALID && S_AXI_WREADY)
-		// Following each write beat, we need to update our address
-		write_addr <= next_waddr;
-	// }}}
-
-	// next_waddr from get_next_write_address
-	// {{{
-	// Given the details of the address request, get the next address to
-	// write to.
-	axi_addr #(
-		// {{{
-		.AW(C_AXI_ADDR_WIDTH), .DW(C_AXI_DATA_WIDTH)
-		// }}}
-	) get_next_write_address(
-		// {{{
-		write_addr,
-			write_size, write_burst, write_awlen, next_waddr
-		// }}}
-	);
-	// }}}
-
-
-	// write_request, write_topofburst, write_len
-	// {{{
-	// Count through the beats of the burst in write_len.  write_topofburst
-	// indicates the first beat in any new burst, but will be zero for all
-	// subsequent burst beats.  write_request is true anytime we are trying
-	// to write.
-	initial	write_request    = 1'b0;
-	initial	write_topofburst = 1'b1;
-	initial	write_len        = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-	begin
-		// {{{
-		write_request    <= 1'b0;
-		write_topofburst <= 1'b1;
-		write_len        <= 0;
-		// }}}
-	end else if (write_awskidready)
-	begin
-		// {{{
-		write_request    <= awskid_valid;
-		write_topofburst <= awskid_valid;
-		write_len        <= (awskid_valid) ? awskid_awlen : 8'h00;
-		// }}}
-	end else if (S_AXI_WVALID && S_AXI_WREADY)
-	begin
-		// {{{
-		write_topofburst <= 1'b0;
-		if (S_AXI_WLAST)
-			write_request <= 1'b0;
-		if (write_len > 0)
-			write_len <= write_len - 1;
-		// }}}
-	end
-	// }}}
-
-	// Slave address decoding
-	// {{{
-	// Decode our incoming address in order to determine the next
-	// slave the address addresses
-	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_valid && write_awskidready
-			//	? awskid_awaddr : next_waddr),
-			.i_addr(awskid_awaddr),
-			.i_data(awskid_prot),
-		.o_valid(dcd_awvalid), .i_stall(!S_AXI_WVALID),
-			.o_decode(raw_wdecode), .o_addr(m_awaddr),
-			.o_data(m_axi_awprot)
-		// }}}
-	);
-	// }}}
-
-	// last_wdecode
-	// {{{
-	// We only do our decode on the address request.  We need the decoded
-	// values long after the top of the burst.  Therefore, let's use
-	// dcd_awvalid to know we have a valid output from the decoder and
-	// then we'll latch that (register it really) for the rest of the burst
-	always @(posedge S_AXI_ACLK)
-	if (dcd_awvalid)
-		last_wdecode <= raw_wdecode;
-	// }}}
-
-	// wdecode
-	// {{{
-	always @(*)
-	begin
-		if (dcd_awvalid)
-			wdecode = raw_wdecode;
-		else
-			wdecode = last_wdecode;
-	end
-	// }}}
-
-	// Downstream slave (write) signals
-	// {{{
-	// It's now time to create our write request for the slave.  Slave
-	// writes take place on the clock after address valid is true as long
-	// as S_AXI_WVALID is true.  This places combinatorial logic onto the
-	// outgoing AWVALID.  The sign that we are in the middle of a burst
-	// will specifically be that WREADY is true.
-	//
-
-	//
-	// If there were any part of this algorithm I disliked it would be the
-	// AWVALID logic here.  It shouldn't nearly be this loaded.
-	assign	S_AXI_WREADY  = write_request;
-	assign	M_AXI_AWVALID = (S_AXI_WVALID && write_request
-			&& (!locked_burst || locked_write)) ? wdecode[NS-1:0] : 0;
-	assign	M_AXI_AWADDR  = write_addr;
-	assign	M_AXI_AWPROT  = m_axi_awprot;
-	assign	M_AXI_AWSIZE  = write_size;
-	assign	M_AXI_WDATA   = S_AXI_WDATA;
-	assign	M_AXI_WSTRB   = S_AXI_WSTRB;
-	// }}}
-
-	// write_awskidready
-	// {{{
-	// We can accept a new value from the skid buffer as soon as the last
-	// write value comes in, or equivalently if we are not in the middle
-	// of a write.  This is all subject, of course, to our backpressure
-	// FIFO not being full.
-	assign	write_awskidready = ((S_AXI_WVALID&&S_AXI_WLAST)
-						|| !S_AXI_WREADY) && !bfull;
-	// }}}
-
-	// write_windex
-	// {{{
-	// Back out an index from our decoded slave value
-	generate if (NS <= 1)
-	begin : WR_ONE_SLAVE
-
-		assign	write_windex = 0;
-
-	end else begin : WR_INDEX
-		reg	[LGNS-1:0]	r_write_windex;
-		integer			k;
-
-		always @(*)
-		begin
-			r_write_windex = 0;
-			for(k=0; k<NS; k=k+1)
-			if (wdecode[k])
-				r_write_windex = r_write_windex | k[LGNS-1:0];
-		end
-
-		assign	write_windex = r_write_windex;
-	end endgenerate
-	// }}}
-
-	always @(posedge S_AXI_ACLK)
-	begin
-		write_bindex <= write_windex;
-		write_no_index <= wdecode[NS];
-	end
-
-	always @(posedge S_AXI_ACLK)
-	// if (write_top_of_burst) // -- not necessary
-		write_bid <= write_id;
-
-	// write_response, write_bvalid
-	// {{{
-	// write_bvalid will be true one clock after the last write is accepted.
-	// This is the internal signal that would've come from a subordinate
-	// slave's BVALID, save that we are generating it internally.
-	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&& S_AXI_WLAST) };
-	// }}}
-
-	// write_top_beat, write_beat_bvalid
-	// {{{
-	// Examine write beats, not just write bursts
-	always @(posedge S_AXI_ACLK)
-	begin
-		write_top_beat    <= write_topofburst;
-		write_beat_bvalid <= S_AXI_WVALID && S_AXI_WREADY;
-	end
-	// }}}
-
-	// write_resp
-	// {{{
-	// The response from any burst should be an DECERR (interconnect
-	// error) if ever the addressed slave doesn't exist in our address map.
-	// This is sticky: any attempt to generate a request to a non-existent
-	// slave will generate an interconnect error.  Likewise, if the slave
-	// ever returns a slave error, we'll propagate it back in the burst
-	// return.  Finally, on an exclusive access burst, we'll return EXOKAY
-	// if we could write the values.
-	always @(posedge S_AXI_ACLK)
-	if (write_beat_bvalid)
-	begin
-		if (write_no_index)
-			write_resp <= INTERCONNECT_ERROR;
-		else if (M_AXI_BRESP[2*write_bindex])
-			write_resp <= { 1'b1, (write_top_beat)
-						? 1'b0 : write_resp[0] };
-		else if (write_top_beat || !write_resp[1])
-			write_resp <= { 1'b0, (write_top_beat && locked_burst && locked_write) };
-	end else if (OPT_LOWPOWER)
-		write_resp <= 2'b00;
-	// }}}
-
-	// write_retid
-	// {{{
-	always @(posedge S_AXI_ACLK)
-		write_retid <= write_bid;
-	// }}}
-
-	// write_count and bfull -- pseudo FIFO counters
-	// {{{
-	// The pseudo-FIFO for the write side.  This counter will let us know
-	// if any write response will ever overflow our write response FIFO,
-	// allowing us to be able to confidently deal with any backpressure.
-	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
-	// }}}
-
-	// Backpressure FIFO on write response returns
-	// {{{
-	sfifo #(
-		// {{{
-		.BW(C_AXI_ID_WIDTH+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_retid, write_resp }),
-			.o_full(bffull), .o_fill(bfill),
-		.i_rd(S_AXI_BVALID && S_AXI_BREADY),
-			.o_data({ S_AXI_BID, S_AXI_BRESP }),
-			.o_empty(bempty)
-		// }}}
-	);
-	// }}}
-
-	assign	S_AXI_BVALID = !bempty;
-
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Read logic
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	// ar*
-	// {{{
-	// Copy the burst information, for use in determining the next address
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARVALID && S_AXI_ARREADY)
-	begin
-		// {{{
-		araddr  <= S_AXI_ARADDR;
-		arid    <= S_AXI_ARID;
-		arlen   <= S_AXI_ARLEN;
-		arsize  <= S_AXI_ARSIZE;
-		arburst <= S_AXI_ARBURST;
-		arlock  <= S_AXI_ARLOCK && S_AXI_ARBURST == 2'b01;
-		arprot  <= S_AXI_ARPROT;
-		// }}}
-	end else if (issue_read)
-		araddr  <= next_araddr;
-	// }}}
-
-	// rlen
-	// {{{
-	// Count the number of remaining items in a burst.  Note that rlen
-	// counts from N-1 to 0, not from N to 1.
-	initial	rlen = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		rlen   <= 0;
-	else if (S_AXI_ARVALID && S_AXI_ARREADY)
-		rlen    <= S_AXI_ARLEN;
-	else if (issue_read && (rlen > 0))
-		rlen <= rlen - 1;
-	// }}}
-
-	// arvalid
-	// {{{
-	// Should the slave M_AXI_ARVALID be true in general?  Based upon
-	// rlen above, but still needs to be gated across all slaves.
-	initial	arvalid = 1'b0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		arvalid <= 1'b0;
-	else if (S_AXI_ARVALID && S_AXI_ARREADY)
-		arvalid <= 1'b1;
-	else if (issue_read && (rlen == 0))
-		arvalid <= 1'b0;
-	// }}}
-
-	// next_araddr -- Get the next AXI address
-	// {{{
-	axi_addr #(
-		// {{{
-		.AW(C_AXI_ADDR_WIDTH), .DW(C_AXI_DATA_WIDTH)
-		// }}}
-	) get_next_read_address(
-		// {{{
-		araddr,
-			arsize, arburst, arlen, next_araddr
-		// }}}
-	);
-	// }}}
-
-	// raw_rdecode-- Decode which slave is being addressed by this read.
-	// {{{
-	addrdecode #(
-		// {{{
-		.AW(AW), .DW(1), .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 || rlen>0),
-			// Warning: there's no skid on this stall
-			.o_stall(arskd_stall),
-			.i_addr((S_AXI_ARVALID & S_AXI_ARREADY)
-				? S_AXI_ARADDR : next_araddr),
-			.i_data(1'b0),
-		.o_valid(read_rwait), .i_stall(!issue_read),
-			.o_decode(raw_rdecode), .o_addr(m_araddr),
-			.o_data(unused_pin[0])
-		// }}}
-	);
-	// }}}
-
-	// last_rdecode
-	// {{{
-	// We want the value from the decoder on the first clock cycle.  It
-	// may not be valid after that, so we'll hold on to it in last_rdecode
-	initial	last_rdecode = 0;
-	always @(posedge S_AXI_ACLK)
-	if (read_rwait)
-		last_rdecode <= raw_rdecode;
-	// }}}
-
-	// rdecode
-	// {{{
-	always @(*)
-	if (read_rwait)
-		rdecode = raw_rdecode;
-	else
-		rdecode = last_rdecode;
-	// }}}
-
-	// Finally, issue our read request any time the FIFO isn't full
-	// {{{
-	assign	issue_read    = !read_full;
-
-	assign	M_AXI_ARVALID = issue_read ? rdecode[NS-1:0] : 0;
-	assign	M_AXI_ARADDR  = m_araddr;
-	assign	M_AXI_ARPROT  = arprot;
-	assign	M_AXI_ARSIZE  = arsize;
-	// }}}
-
-	// read_rvalid, read_result
-	// {{{
-	// read_rvalid would be the RVALID response from the slave that would
-	// be returned if we checked it.  read_result is the same thing--one
-	// clock later.
-	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,
-				(arvalid&issue_read) };
-	// }}}
-
-	// read_rvid, read_rvlast, read_rvlock
-	// {{{
-	// On the same clock when rvalid is true, we'll also want to know
-	// if RLAST should be true (decoded here, not in the slave), and
-	// whether or not the transaction is locked.  These values are valid
-	// any time read_rvalid is true.
-	always @(posedge S_AXI_ACLK)
-	begin
-		if (arvalid && issue_read)
-		begin
-			read_rvid   <= arid;
-			read_rvlast <= (rlen == 0);
-			read_rvlock <= (read_rvlock && !read_rvlast) || (OPT_EXCLUSIVE_ACCESS && arlock && lock_valid);
-		end else if (read_rvlast)
-			read_rvlock <= 1'b0;
-
-		if (!S_AXI_ARESETN)
-		begin
-			read_rvlock <= 1'b0;
-			read_rvlast <= 1'b1;
-		end
-	end
-	// }}}
-
-	// read_retid, read_retlast
-	// {{{
-	// read_result is true one clock after read_rvalid is true.  Copy
-	// the ID and LAST values into this pipeline clock cycle
-	always @(posedge S_AXI_ACLK)
-	begin
-		read_retid   <= read_rvid;
-		read_retlast <= read_rvlast;
-	end
-	// }}}
-
-	//
-	// Decode the read value.
-	//
-
-	// read_index - First step is to calculate the index of the slave
-	// {{{
-	generate if (NS <= 1)
-	begin : RD_ONE_SLAVE
-
-		assign	read_index = 0;
-
-	end else begin : RD_INDEX
-		reg	[LGNS-1:0]	r_read_index = 0;
-		integer			k;
-
-		always @(*)
-		begin
-			r_read_index = 0;
-
-			for(k=0; k<NS; k=k+1)
-			if (rdecode[k])
-				r_read_index = r_read_index | k[LGNS-1:0];
-		end
-
-		assign	read_index = r_read_index;
-	end endgenerate
-	// }}}
-
-	// last_read_index
-	// {{{
-	// Keep this index into the RVALID cycle
-	always @(posedge S_AXI_ACLK)
-		last_read_index <= read_index;
-	// }}}
-
-	// read_no_index is a flag to indicate that no slave was indexed.
-	// {{{
-	always @(posedge S_AXI_ACLK)
-		read_no_index <= rdecode[NS];
-	// }}}
-
-	// read_rdata
-	// {{{
-	// Now we can use last_read_index to determine the return data.
-	// read_rdata will be valid on the same clock $past(RVALID) or
-	// read_return cycle
-	always @(posedge S_AXI_ACLK)
-		read_rdata <= M_AXI_RDATA[DW*last_read_index +: DW];
-	// }}}
-
-	// read_resp
-	// {{{
-	// As with read_rdata, read_resp is the response from the slave
-	always @(posedge S_AXI_ACLK)
-	if (read_no_index)
-		read_resp <= INTERCONNECT_ERROR;
-	else if (M_AXI_RRESP[2*last_read_index + 1])
-		read_resp <= SLVERR;	// SLVERR
-	else if (OPT_EXCLUSIVE_ACCESS && read_rvlock)
-		read_resp <= EXOKAY;	// Exclusive access Okay
-	else
-		read_resp <= OKAY;	// OKAY
-	// }}}
-
-	// read_count, read_full
-	// {{{
-	// Since we can't allow the incoming requests to overflow in the
-	// presence of any back pressure, let's create a phantom FIFO here
-	// counting the number of values either in the final pipeline or in
-	// final read FIFO.  If read_full is true, the FIFO is full and we
-	// cannot move any more data forward.
-	initial	{ read_count, read_full } = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		{ read_count, read_full } <= 0;
-	else case({ read_rwait && issue_read, 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
-	// }}}
-
-	assign	S_AXI_ARREADY = (rlen == 0) && !read_full;
-
-	// Read return FIFO for dealing with backpressure
-	// {{{
-	// Send the return results through a synchronous FIFO to handle
-	// back-pressure.  Doing this costs us one clock of latency.
-	sfifo #(
-		// {{{
-		.BW(C_AXI_ID_WIDTH+DW+1+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_retid, read_rdata,
-						read_retlast, read_resp }),
-			.o_full(rdfull), .o_fill(rfill),
-		.i_rd(S_AXI_RVALID && S_AXI_RREADY),
-			.o_data({ S_AXI_RID, S_AXI_RDATA,
-						S_AXI_RLAST, S_AXI_RRESP }),
-			.o_empty(rempty)
-		// }}}
-	);
-	// }}}
-
-	assign	S_AXI_RVALID = !rempty;
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Exclusive access / Bus locking logic
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	generate if (OPT_EXCLUSIVE_ACCESS)
-	begin : EXCLUSIVE_ACCESS
-		// {{{
-		reg			r_lock_valid, r_locked_burst;
-		reg	[AW-1:0]	lock_addr, lock_last;
-		reg	[4-1:0]		lock_len;
-		reg	[3-1:0]		lock_size;
-		reg	[IW-1:0]	lock_id;
-
-		initial	r_lock_valid   = 1'b0;
-		initial	r_locked_burst = 1'b0;
-		initial	locked_write = 1'b0;
-		always @(posedge S_AXI_ACLK)
-		begin
-
-			//
-			// Step one: Set the lock_valid signal.  This means
-			// that a read request has been successful requesting
-			// the lock for this address.
-			//
-			if (awskid_valid && write_awskidready)
-			begin
-				// On any write to the value inside our lock
-				// range, disable the lock_valid signal
-				if ((awskid_awaddr
-					+ ({ {(AW-4){1'b0}},awskid_awlen[3:0]} << S_AXI_AWSIZE)
-						>= lock_addr)
-					&&(S_AXI_AWADDR <= lock_last))
-					r_lock_valid <= 0;
-			end
-
-			if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLOCK
-				&& S_AXI_ARBURST == 2'b01)
-			begin
-				r_lock_valid <= !locked_write;
-				lock_addr  <= S_AXI_ARADDR;
-				lock_id    <= S_AXI_ARID;
-				lock_size  <= S_AXI_ARSIZE;
-				lock_len   <= S_AXI_ARLEN[3:0];
-				lock_last  <= S_AXI_ARADDR
-					+ ({ {(AW-4){1'b0}}, lock_len }
-							<< S_AXI_ARSIZE);
-			end
-
-			if (awskid_valid && write_awskidready)
-			begin
-				r_locked_burst <= 1'b0;
-				locked_write <= awskid_awlock;
-
-				if (awskid_awlock)
-				begin
-					r_locked_burst <= r_lock_valid;
-					if (lock_addr != awskid_awaddr)
-						r_locked_burst <= 1'b0;
-					if (lock_id != awskid_awid)
-						r_locked_burst <= 1'b0;
-					if (lock_size != awskid_awsize)
-						r_locked_burst <= 1'b0;
-					if (lock_len != awskid_awlen[3:0])
-						r_locked_burst <= 1'b0;
-					if (2'b01 != awskid_awburst)
-						r_locked_burst <= 1'b0;
-				end
-
-				// Write if !locked_write || write_burst
-				// EXOKAY on locked_write && write_burst
-				// OKAY on all other writes where the slave
-				//   does not assert an error
-			end else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST)
-				r_locked_burst <= 1'b0;
-
-			if (!S_AXI_ARESETN)
-			begin
-				r_lock_valid  <= 1'b0;
-				r_locked_burst <= 1'b0;
-			end
-		end
-
-		assign	locked_burst = r_locked_burst;
-		assign	lock_valid = r_lock_valid;
-		// }}}
-	end else begin : NO_EXCLUSIVE_ACCESS
-		// {{{
-		// Keep track of whether or not the current burst requests
-		// exclusive access or not.  locked_write is an important
-		// signal used to make certain that we do not write to our
-		// slave on any locked write requests.  (Shouldn't happen,
-		// since we aren't returning any EXOKAY's from reads ...)
-		always @(posedge S_AXI_ACLK)
-		if (awskid_valid && write_awskidready)
-			locked_write <= awskid_awlock;
-		else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST)
-			locked_write <= 1'b0;
-
-		assign	locked_burst = 0;
-		assign	lock_valid = 0;
-		// }}}
-	end endgenerate
-	// }}}
-
-	// Make Verilator happy
-	// {{{
-	// verilator lint_off UNUSED
-	wire	unused;
-	assign	unused = &{ 1'b0,
-			S_AXI_AWCACHE, S_AXI_ARCACHE,
-			S_AXI_AWQOS,   S_AXI_ARQOS,
-			dcd_awvalid, m_awaddr, unused_pin,
-			bffull, rdfull, bfill, rfill,
-			awskd_stall, arskd_stall };
-	// verilator lint_on  UNUSED
-	// }}}
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-//
-// Formal verification properties
-// {{{
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-`ifdef	FORMAL
-	localparam	F_LGDEPTH = LGFLEN+9;
-
-	//
-	// ...
-	//
-
-	faxi_slave #(	.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
-			.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
-			.C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
-			.F_AXI_MAXDELAY(5),
-			.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_awid(   S_AXI_AWID),
-		.i_axi_awaddr( S_AXI_AWADDR),
-		.i_axi_awlen(  S_AXI_AWLEN),
-		.i_axi_awsize( S_AXI_AWSIZE),
-		.i_axi_awburst(S_AXI_AWBURST),
-		.i_axi_awlock( S_AXI_AWLOCK),
-		.i_axi_awcache(S_AXI_AWCACHE),
-		.i_axi_awprot( S_AXI_AWPROT),
-		.i_axi_awqos(  S_AXI_AWQOS),
-		//
-		.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_wlast( S_AXI_WLAST),
-		//
-		.i_axi_bvalid(S_AXI_BVALID),
-		.i_axi_bready(S_AXI_BREADY),
-		.i_axi_bid(   S_AXI_BID),
-		.i_axi_bresp( S_AXI_BRESP),
-		//
-		.i_axi_arvalid(S_AXI_ARVALID),
-		.i_axi_arready(S_AXI_ARREADY),
-		.i_axi_arid(   S_AXI_ARID),
-		.i_axi_araddr( S_AXI_ARADDR),
-		.i_axi_arlen(  S_AXI_ARLEN),
-		.i_axi_arsize( S_AXI_ARSIZE),
-		.i_axi_arburst(S_AXI_ARBURST),
-		.i_axi_arlock( S_AXI_ARLOCK),
-		.i_axi_arcache(S_AXI_ARCACHE),
-		.i_axi_arprot( S_AXI_ARPROT),
-		.i_axi_arqos(  S_AXI_ARQOS),
-		//
-		.i_axi_rvalid(S_AXI_RVALID),
-		.i_axi_rready(S_AXI_RREADY),
-		.i_axi_rid(   S_AXI_RID),
-		.i_axi_rdata( S_AXI_RDATA),
-		.i_axi_rlast( S_AXI_RLAST),
-		.i_axi_rresp( S_AXI_RRESP)
-		//
-		// ...
-		//
-		);
-
-	//
-	// ...
-	//
-
-	always @(*)
-	if (!OPT_EXCLUSIVE_ACCESS)
-	begin
-		assert(!S_AXI_BVALID || S_AXI_BRESP != EXOKAY);
-		assert(!S_AXI_RVALID || S_AXI_RRESP != EXOKAY);
-	end
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Properties necessary to pass induction
-	//
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	always @(*)
-		assert($onehot0(M_AXI_AWVALID));
-
-	always @(*)
-		assert($onehot0(M_AXI_ARVALID));
-
-	//
-	//
-	// Write properties
-	//
-	//
-
-	always @(*)
-	if (S_AXI_WVALID && S_AXI_WREADY)
-	begin
-		if (locked_burst && !locked_write)
-			assert(M_AXI_AWVALID == 0);
-		else if (wdecode[NS])
-			assert(M_AXI_AWVALID == 0);
-		else begin
-			assert($onehot(M_AXI_AWVALID));
-			assert(M_AXI_AWVALID == wdecode[NS-1:0]);
-		end
-	end else
-		assert(M_AXI_AWVALID == 0);
-
-	//
-	// ...
-	//
-
-	//
-	//
-	// Read properties
-	//
-	//
-
-	//
-	// ...
-	//
-
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Simplifying (careless) assumptions
-	//
-	// Caution: these might void your proof
-	//
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	localparam	[0:0]	F_CHECK_WRITES = 1'b1;
-	localparam	[0:0]	F_CHECK_READS  = 1'b1;
-
-	generate if (!F_CHECK_WRITES)
-	begin
-		always @(*)
-			assume(!S_AXI_AWVALID);
-		always @(*)
-			assert(!S_AXI_BVALID);
-		always @(*)
-			assert(!M_AXI_AWVALID);
-
-		// ...
-	end endgenerate
-
-	generate if (!F_CHECK_READS)
-	begin
-		always @(*)
-			assume(!S_AXI_ARVALID);
-		always @(*)
-			assert(!S_AXI_RVALID);
-		always @(*)
-			assert(M_AXI_ARVALID == 0);
-		always @(*)
-			assert(rdecode == 0);
-		// ...
-	end endgenerate
-
-	//
-	// ...
-	//
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Cover properties
-	//
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	reg	[3:0]	cvr_arvalids, cvr_awvalids, cvr_reads, cvr_writes;
-	(* anyconst *)	reg	cvr_burst;
-
-	always @(*)
-	if (cvr_burst && S_AXI_AWVALID)
-		assume(S_AXI_AWLEN > 2);
-
-	always @(*)
-	if (cvr_burst && S_AXI_ARVALID)
-		assume(S_AXI_ARLEN > 2);
-
-	initial	cvr_awvalids = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!cvr_burst || !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 (!cvr_burst || !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 (!cvr_burst || !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 && S_AXI_RLAST
-				&& !(&cvr_arvalids))
-		cvr_reads <= cvr_reads + 1;
-
-	generate if (F_CHECK_WRITES)
-	begin : COVER_WRITES
-
-		always @(*)
-			cover(cvr_awvalids > 2);
-
-		always @(*)
-			cover(cvr_writes > 2);
-
-		always @(*)
-			cover(cvr_writes > 4);
-	end endgenerate
-
-	generate if (F_CHECK_READS)
-	begin : COVER_READS
-		always @(*)
-			cover(cvr_arvalids > 2);
-
-		always @(*)
-			cover(cvr_reads > 2);
-
-		always @(*)
-			cover(cvr_reads > 4);
-	end endgenerate
-
-	always @(*)
-		cover((cvr_writes > 2) && (cvr_reads > 2));
-
-	generate if (OPT_EXCLUSIVE_ACCESS)
-	begin : COVER_EXCLUSIVE_ACCESS
-
-		always @(*)
-			cover(S_AXI_BVALID && S_AXI_BRESP == EXOKAY);
-
-	end endgenerate
-`endif
-endmodule