rtl: fix quartus errors: parser, synthesis, fitter

1 files changed, 0 insertions, 2339 deletions

diff --git a/rtl/wb2axip/axisafety.v b/rtl/wb2axip/axisafety.v
deleted file mode 100644
index ff7e351..0000000
--- a/rtl/wb2axip/axisafety.v
+++ /dev/null
@@ -1,2339 +0,0 @@
-////////////////////////////////////////////////////////////////////////////////
-//
-// Filename:	axisafety.v
-// {{{
-// Project:	WB2AXIPSP: bus bridges and other odds and ends
-//
-// Purpose:	Given that 1) AXI interfaces can be difficult to write and to
-//		get right, 2) my experiences with the AXI infrastructure of an
-//	ARM+FPGA is that the device needs a power cycle following a bus fault,
-//	and given that I've now found multiple interfaces that had some bug
-//	or other within them, the following is a bus fault isolator.  It acts
-//	as a bump in the log between the interconnect and the user core.  As
-//	such, it has two interfaces:  The first is the slave interface,
-//	coming from the interconnect.  The second interface is the master
-//	interface, proceeding to a slave that might be faulty.
-//
-//		INTERCONNECT --> (S) AXISAFETY (M) --> POTENTIALLY FAULTY CORE
-//
-//	The slave interface has been formally verified to be a valid AXI
-//	slave, independent of whatever the potentially faulty core might do.
-//	If the user core (i.e. the potentially faulty one) responds validly
-//	to the requests of a master, then this core will turn into a simple
-//	delay on the bus.  If, on the other hand, the user core suffers from
-//	a protocol error, then this core will set one of two output
-//	flags--either o_write_fault or o_read_fault indicating whether a write
-//	or a read fault was detected.  Further attempts to access the user
-//	core will result in bus errors, generated by the AXISAFETY core.
-//
-//	Assuming the bus master can properly detect and deal with a bus error,
-//	this should then make it possible to properly recover from a bus
-//	protocol error without later needing to cycle power.
-//
-//	The core does have a couple of limitations.  For example, it can only
-//	handle one burst transaction, and one ID at a time.  This matches the
-//	performances of Xilinx's example AXI full core, from which many user
-//	cores have have been copied/modified from.  Therefore, there will be
-//	no performance loss for such a core.
-//
-//	Because of this, it is still possible that the user core might have an
-//	undetected fault when using this core.  For example, if the interconnect
-//	issues more than one bus request before receiving the response from the
-//	first request, this safety core will stall the second request,
-//	preventing the downstream core from seeing this second request.  If the
-//	downstream core would suffer from an error while handling the second
-//	request, by preventing the user core from seeing the second request this
-//	core eliminates that potential for error.
-//
-// Usage:	The important part of using this core is to connect the slave
-//		side to the interconnect, and the master side to the user core.
-//
-//	Some options are available:
-//
-//	1) C_S_AXI_ADDR_WIDTH	The number of address bits in the AXI channel
-//	1) C_S_AXI_DATA_WIDTH	The number of data bits in the AXI channel
-//	3) C_S_AXI_ID_WIDTH	The number of bits in an AXI ID.  As currently
-//		written, this number cannot be zero.  You can, however, set it
-//		to '1' and connect all of the relevant ID inputs to zero.
-//
-//	These three parameters have currently been abbreviated with AW, DW, and
-//	IW.  I anticipate returning them to their original meanings, I just
-//	haven't done so (yet).
-//
-//	4) OPT_TIMEOUT		This is the number of clock periods, from
-//		interconnect request to interconnect response, that the
-//		slave needs to respond within.  (The actual timeout from the
-//		user slave's perspective will be shorter than this.)
-//
-//		This timeout is part of the check that a slave core will
-//		always return a response.  From the standpoint of this core,
-//		it can be set arbitrarily large.  (From the standpoint of
-//		formal verification, it needs to be kept short ...)
-//		Feel free to set this even as large as 1ms if you would like.
-//
-//	5) OPT_SELF_RESET	If set, will send a reset signal to the slave
-//		following any write or read fault.  This will cause the other
-//		side of the link (write or read) to fault as well.  Once the
-//		channel then becomes inactive, the slave will be released from
-//		reset and will be able to interact with the rest of the bus
-//		again.
-//
-//	5) OPT_EXCLUSIVE	If clear, will prohibit the slave from ever
-//		receiving an exclusive access request.  This saves the logic
-//		in the firewall necessary to check that an EXOKAY response
-//		to a write request was truly an allowed response.  Since that
-//		logic can explode with the ID width, sparing it can be quite
-//		useful.  If set, provides full exclusive access checking in
-//		addition to the normal bus fault checking.
-//
-// Performance:	As mentioned above, this core can handle one read burst and one
-//		write burst at a time, no more.  Further, the core will delay
-//	an input path by one clock and the output path by another clock, so that
-//	the latency involved with using this core is a minimum of two extra
-//	clocks beyond the latency user slave core.
-//
-//	Maximum write latency: N+3 clocks for a burst of N values
-//	Maximum read latency:  N+3 clocks for a burst of N values
-//
-// Faults detected:
-//
-//	Write channel:
-//		1. Raising BVALID prior to the last write value being sent
-//			to the user/slave core.
-//		2. Raising BVALID prior to accepting the write address
-//		3. A BID return ID that doesn't match the request AWID
-//		4. Sending too many returns, such as not dropping BVALID
-//			or raising it when there is no outstanding write
-//			request
-//
-//		While the following technically isn't a violation of the
-//		AXI protocol, it is treated as such by this fault isolator.
-//
-//		5. Accepting write data prior to the write address
-//
-//		The fault isolator will guarantee that AWVALID is raised before
-//		WVALID, so this shouldn't be a problem.
-//
-//	Read channel:
-//
-//		1. Raising RVALID before accepting the read address, ARVALID
-//		2. A return ID that doesn't match the ID that was sent.
-//		3. Raising RVALID after the last return value, and so returning
-//			too many response values
-//		4. Setting the RLAST value on anything but the last value from
-//			the bus.
-//
-//
-// 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 axisafety #(
-	// {{{
-	parameter C_S_AXI_ID_WIDTH	= 1,
-	parameter C_S_AXI_DATA_WIDTH	= 32,
-	parameter C_S_AXI_ADDR_WIDTH	= 16,
-	// OPT_SELF_RESET: Set to true if the downstream slave should be
-	// reset upon detecting an error and separate from the upstream reset
-	// domain
-	parameter [0:0] OPT_SELF_RESET  = 1'b0,
-	// OPT_EXCLUSIVE: Set to true if the downstream slave might possibly
-	// offer an exclusive access capability
-	parameter [0:0] OPT_EXCLUSIVE  = 1'b0,
-	//
-	// I use the following abbreviations, IW, DW, and AW, to simplify
-	// the code below (and to help it fit within an 80 col terminal)
-	localparam	IW	= C_S_AXI_ID_WIDTH,
-	localparam	DW	= C_S_AXI_DATA_WIDTH,
-	localparam	AW	= C_S_AXI_ADDR_WIDTH,
-	//
-	// OPT_TIMEOUT references the number of clock cycles to wait
-	// between raising the *VALID signal and when the respective
-	// *VALID return signal must be high.  You might wish to set this
-	// to a very high number, to allow your core to work its magic.
-	parameter	OPT_TIMEOUT = 20
-	// }}}
-	) (
-		// {{{
-		output	reg	o_read_fault,
-		output	reg	o_write_fault,
-		// User ports ends
-		// Do not modify the ports beyond this line
-
-		// Global Clock Signal
-		input	wire			S_AXI_ACLK,
-		// Global Reset Signal. This Signal is Active LOW
-		input	wire			S_AXI_ARESETN,
-		output	reg			M_AXI_ARESETN,
-		//
-		// The input side.  This is where slave requests come into
-		// the core.
-		// {{{
-		//
-		//	Write address
-		input	wire [IW-1 : 0]		S_AXI_AWID,
-		input	wire [AW-1 : 0]		S_AXI_AWADDR,
-		input	wire [7 : 0]		S_AXI_AWLEN,
-		input	wire [2 : 0]		S_AXI_AWSIZE,
-		input	wire [1 : 0]		S_AXI_AWBURST,
-		input	wire			S_AXI_AWLOCK,
-		input	wire [3 : 0]		S_AXI_AWCACHE,
-		input	wire [2 : 0]		S_AXI_AWPROT,
-		input	wire [3 : 0]		S_AXI_AWQOS,
-		input	wire			S_AXI_AWVALID,
-		output	reg			S_AXI_AWREADY,
-		//	Write data
-		input	wire [DW-1 : 0]		S_AXI_WDATA,
-		input	wire [(DW/8)-1 : 0]	S_AXI_WSTRB,
-		input	wire			S_AXI_WLAST,
-		input	wire			S_AXI_WVALID,
-		output	reg			S_AXI_WREADY,
-		//	Write return
-		output	reg [IW-1 : 0]		S_AXI_BID,
-		output	reg [1 : 0]		S_AXI_BRESP,
-		output	reg			S_AXI_BVALID,
-		input	wire			S_AXI_BREADY,
-		//	Read address
-		input	wire [IW-1 : 0]		S_AXI_ARID,
-		input	wire [AW-1 : 0]		S_AXI_ARADDR,
-		input	wire [7 : 0]		S_AXI_ARLEN,
-		input	wire [2 : 0]		S_AXI_ARSIZE,
-		input	wire [1 : 0]		S_AXI_ARBURST,
-		input	wire			S_AXI_ARLOCK,
-		input	wire [3 : 0]		S_AXI_ARCACHE,
-		input	wire [2 : 0]		S_AXI_ARPROT,
-		input	wire [3 : 0]		S_AXI_ARQOS,
-		input	wire			S_AXI_ARVALID,
-		output	reg			S_AXI_ARREADY,
-		//	Read data
-		output	reg [IW-1 : 0]		S_AXI_RID,
-		output	reg [DW-1 : 0]		S_AXI_RDATA,
-		output	reg [1 : 0]		S_AXI_RRESP,
-		output	reg			S_AXI_RLAST,
-		output	reg			S_AXI_RVALID,
-		input	wire			S_AXI_RREADY,
-		// }}}
-		//
-		// The output side, where slave requests are forwarded to the
-		// actual slave
-		// {{{
-		//	Write address
-		// {{{
-		output	reg [IW-1 : 0]		M_AXI_AWID,
-		output	reg [AW-1 : 0]		M_AXI_AWADDR,
-		output	reg [7 : 0]		M_AXI_AWLEN,
-		output	reg [2 : 0]		M_AXI_AWSIZE,
-		output	reg [1 : 0]		M_AXI_AWBURST,
-		output	reg			M_AXI_AWLOCK,
-		output	reg [3 : 0]		M_AXI_AWCACHE,
-		output	reg [2 : 0]		M_AXI_AWPROT,
-		output	reg [3 : 0]		M_AXI_AWQOS,
-		output	reg			M_AXI_AWVALID,
-		input	wire			M_AXI_AWREADY,
-		//	Write data
-		output	reg [DW-1 : 0]		M_AXI_WDATA,
-		output	reg [(DW/8)-1 : 0]	M_AXI_WSTRB,
-		output	reg			M_AXI_WLAST,
-		output	reg			M_AXI_WVALID,
-		input	wire			M_AXI_WREADY,
-		//	Write return
-		input	wire [IW-1 : 0]		M_AXI_BID,
-		input	wire [1 : 0]		M_AXI_BRESP,
-		input	wire			M_AXI_BVALID,
-		output	wire			M_AXI_BREADY,
-		// }}}
-		//	Read address
-		// {{{
-		output	reg [IW-1 : 0]		M_AXI_ARID,
-		output	reg [AW-1 : 0]		M_AXI_ARADDR,
-		output	reg [7 : 0]		M_AXI_ARLEN,
-		output	reg [2 : 0]		M_AXI_ARSIZE,
-		output	reg [1 : 0]		M_AXI_ARBURST,
-		output	reg			M_AXI_ARLOCK,
-		output	reg [3 : 0]		M_AXI_ARCACHE,
-		output	reg [2 : 0]		M_AXI_ARPROT,
-		output	reg [3 : 0]		M_AXI_ARQOS,
-		output	reg			M_AXI_ARVALID,
-		input	wire			M_AXI_ARREADY,
-		//	Read data
-		input	wire [IW-1 : 0]		M_AXI_RID,
-		input	wire [DW-1 : 0]		M_AXI_RDATA,
-		input	wire [1 : 0]		M_AXI_RRESP,
-		input	wire			M_AXI_RLAST,
-		input	wire			M_AXI_RVALID,
-		output	wire			M_AXI_RREADY
-		// }}}
-		// }}}
-		// }}}
-	);
-
-	localparam	LGTIMEOUT = $clog2(OPT_TIMEOUT+1);
-	localparam [1:0]	OKAY = 2'b00, EXOKAY = 2'b01;
-	localparam	SLAVE_ERROR = 2'b10;
-	//
-	//
-	// Register declarations
-	// {{{
-	reg			faulty_write_return, faulty_read_return;
-	reg			clear_fault;
-	//
-	// Timer/timeout variables
-	reg	[LGTIMEOUT-1:0]	write_timer,   read_timer;
-	reg			write_timeout, read_timeout;
-
-	//
-	// Double buffer the write address channel
-	reg		r_awvalid, m_awvalid;
-	reg	[IW-1:0] r_awid,   m_awid;
-	reg	[AW-1:0] r_awaddr, m_awaddr;
-	reg	[7:0]	r_awlen,   m_awlen;
-	reg	[2:0]	r_awsize,  m_awsize;
-	reg	[1:0]	r_awburst, m_awburst;
-	reg		r_awlock,  m_awlock;
-	reg	[3:0]	r_awcache, m_awcache;
-	reg	[2:0]	r_awprot,  m_awprot;
-	reg	[3:0]	r_awqos,   m_awqos;
-
-	//
-	// Double buffer for the write channel
-	reg			r_wvalid,m_wvalid;
-	reg	[DW-1:0]	r_wdata, m_wdata;
-	reg	[DW/8-1:0]	r_wstrb, m_wstrb;
-	reg			r_wlast, m_wlast;
-
-	//
-	// Double buffer the write response channel
-	reg			m_bvalid;	// r_bvalid == 0
-	reg	[IW-1:0]	m_bid;
-	reg	[1:0]		m_bresp;
-
-	//
-	// Double buffer the read address channel
-	reg		r_arvalid, m_arvalid;
-	reg	[IW-1:0]	r_arid,    m_arid;
-	reg	[AW-1:0] r_araddr, m_araddr;
-	reg	[7:0]	r_arlen,   m_arlen;
-	reg	[2:0]	r_arsize,  m_arsize;
-	reg	[1:0]	r_arburst, m_arburst;
-	reg		r_arlock,  m_arlock;
-	reg	[3:0]	r_arcache, m_arcache;
-	reg	[2:0]	r_arprot,  m_arprot;
-	reg	[3:0]	r_arqos,   m_arqos;
-
-	//
-	// Double buffer the read data response channel
-	reg			r_rvalid,m_rvalid;
-	reg	[IW-1:0]	         m_rid;
-	reg	[1:0]		r_rresp, m_rresp;
-	reg			         m_rlast;
-	reg	[DW-1:0]	r_rdata, m_rdata;
-
-	//
-	// Write FIFO data
-	wire	[IW-1:0]	wfifo_id;
-	wire			wfifo_lock;
-
-	//
-	// Read FIFO data
-	reg	[IW-1:0]	rfifo_id;
-	reg			rfifo_lock;
-	reg	[8:0]		rfifo_counter;
-	reg			rfifo_empty, rfifo_last, rfifo_penultimate;
-
-	//
-	//
-	reg	[0:0]	s_wbursts;
-	reg	[8:0]	m_wpending;
-	reg		m_wempty, m_wlastctr;
-	wire		waddr_valid, raddr_valid;
-
-	wire			lock_enabled, lock_failed;
-	wire	[(1<<IW)-1:0]	lock_active;
-	reg			rfifo_first, exread;
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Write channel processing
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	// Write address processing
-	// {{{
-	// S_AXI_AWREADY
-	// {{{
-	initial	S_AXI_AWREADY = (OPT_SELF_RESET) ? 0:1;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		S_AXI_AWREADY <= !OPT_SELF_RESET;
-	else if (S_AXI_AWVALID && S_AXI_AWREADY)
-		S_AXI_AWREADY <= 0;
-	// else if (clear_fault)
-	//	S_AXI_AWREADY <= 1;
-	else if (!S_AXI_AWREADY)
-		S_AXI_AWREADY <= S_AXI_BVALID && S_AXI_BREADY;
-	// }}}
-
-	generate if (OPT_EXCLUSIVE)
-	begin : GEN_LOCK_ENABLED
-		// {{{
-		reg	r_lock_enabled, r_lock_failed;
-
-		// lock_enabled
-		// {{{
-		initial	r_lock_enabled = 0;
-		always @(posedge S_AXI_ACLK)
-		if (!S_AXI_ARESETN || !OPT_EXCLUSIVE)
-			r_lock_enabled <= 0;
-		else if (S_AXI_AWVALID && S_AXI_AWREADY)
-			r_lock_enabled <= S_AXI_AWLOCK && lock_active[S_AXI_AWID];
-		else if (S_AXI_BVALID && S_AXI_BREADY)
-			r_lock_enabled <= 0;
-		// }}}
-
-		// lock_failed
-		// {{{
-		initial	r_lock_failed = 0;
-		always @(posedge S_AXI_ACLK)
-		if (!S_AXI_ARESETN || !OPT_EXCLUSIVE)
-			r_lock_failed <= 0;
-		else if (S_AXI_AWVALID && S_AXI_AWREADY)
-			r_lock_failed <= S_AXI_AWLOCK && !lock_active[S_AXI_AWID];
-		else if (S_AXI_BVALID && S_AXI_BREADY)
-			r_lock_failed <= 0;
-		// }}}
-
-		assign	lock_enabled = r_lock_enabled;
-		assign	lock_failed  = r_lock_failed;
-		// }}}
-	end else begin : NO_LOCK_ENABLE
-		// {{{
-		assign	lock_enabled = 0;
-		assign	lock_failed  = 0;
-		// }}}
-	end endgenerate
-
-	// waddr_valid
-	// {{{
-	generate if (OPT_SELF_RESET)
-	begin : GEN_LCL_RESET
-		reg	r_waddr_valid;
-
-		initial	r_waddr_valid = 0;
-		always @(posedge S_AXI_ACLK)
-		if (!S_AXI_ARESETN)
-			r_waddr_valid <= 0;
-		else if (S_AXI_AWVALID && S_AXI_AWREADY)
-			r_waddr_valid <= 1;
-		else if (waddr_valid)
-			r_waddr_valid <= !S_AXI_BVALID || !S_AXI_BREADY;
-
-		assign	waddr_valid = r_waddr_valid;
-	end else begin : NO_LCL_RESET
-		assign	waddr_valid = !S_AXI_AWREADY;
-	end endgenerate
-	// }}}
-
-	// r_aw*
-	// {{{
-	// Double buffer for the AW* channel
-	//
-	initial	r_awvalid = 0;
-	always @(posedge S_AXI_ACLK)
-	begin
-		if (S_AXI_AWVALID && S_AXI_AWREADY)
-		begin
-			r_awvalid <= 1'b0;
-			r_awid    <= S_AXI_AWID;
-			r_awaddr  <= S_AXI_AWADDR;
-			r_awlen   <= S_AXI_AWLEN;
-			r_awsize  <= S_AXI_AWSIZE;
-			r_awburst <= S_AXI_AWBURST;
-			r_awlock  <= S_AXI_AWLOCK;
-			r_awcache <= S_AXI_AWCACHE;
-			r_awprot  <= S_AXI_AWPROT;
-			r_awqos   <= S_AXI_AWQOS;
-		end else if (M_AXI_AWREADY)
-			r_awvalid <= 0;
-
-		if (!S_AXI_ARESETN)
-		begin
-			r_awvalid <= 0;
-			r_awlock  <= 0;
-		end
-
-		if (!OPT_EXCLUSIVE)
-			r_awlock <= 1'b0;
-	end
-	// }}}
-
-	// m_aw*
-	// {{{
-	// Second half of the AW* double-buffer.  The m_* terms reference
-	// either the value in the double buffer (assuming one is in there),
-	// or the incoming value (if the double buffer is empty)
-	//
-	always @(*)
-	if (r_awvalid)
-	begin
-		m_awvalid = r_awvalid;
-		m_awid    = r_awid;
-		m_awaddr  = r_awaddr;
-		m_awlen   = r_awlen;
-		m_awsize  = r_awsize;
-		m_awburst = r_awburst;
-		m_awlock  = r_awlock;
-		m_awcache = r_awcache;
-		m_awprot  = r_awprot;
-		m_awqos   = r_awqos;
-	end else begin
-		m_awvalid = S_AXI_AWVALID && S_AXI_AWREADY;
-		m_awid    = S_AXI_AWID;
-		m_awaddr  = S_AXI_AWADDR;
-		m_awlen   = S_AXI_AWLEN;
-		m_awsize  = S_AXI_AWSIZE;
-		m_awburst = S_AXI_AWBURST;
-		m_awlock  = S_AXI_AWLOCK && OPT_EXCLUSIVE;
-		m_awcache = S_AXI_AWCACHE;
-		m_awprot  = S_AXI_AWPROT;
-		m_awqos   = S_AXI_AWQOS;
-	end
-	// }}}
-
-	// M_AXI_AW*
-	// {{{
-	// Set the output AW* channel outputs--but only on no fault
-	//
-	initial	M_AXI_AWVALID = 0;
-	always @(posedge S_AXI_ACLK)
-	begin
-		if (!M_AXI_AWVALID || M_AXI_AWREADY)
-		begin
-
-			if (o_write_fault)
-				M_AXI_AWVALID <= 0;
-			else
-				M_AXI_AWVALID <= m_awvalid;
-
-			M_AXI_AWID    <= m_awid;
-			M_AXI_AWADDR  <= m_awaddr;
-			M_AXI_AWLEN   <= m_awlen;
-			M_AXI_AWSIZE  <= m_awsize;
-			M_AXI_AWBURST <= m_awburst;
-			M_AXI_AWLOCK  <= m_awlock && lock_active[m_awid];
-			M_AXI_AWCACHE <= m_awcache;
-			M_AXI_AWPROT  <= m_awprot;
-			M_AXI_AWQOS   <= m_awqos;
-		end
-
-		if (!OPT_EXCLUSIVE)
-			M_AXI_AWLOCK  <= 0;
-		if (!M_AXI_ARESETN)
-			M_AXI_AWVALID <= 0;
-	end
-	// }}}
-	// }}}
-
-	// s_wbursts
-	// {{{
-	// Count write bursts outstanding from the standpoint of
-	// the incoming (slave) channel
-	//
-	// Notice that, as currently built, the count can only ever be one
-	// or zero.
-	//
-	// We'll use this count in a moment to determine if a response
-	// has taken too long, or if a response is returned when there's
-	// no outstanding request
-	initial	s_wbursts = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		s_wbursts <= 0;
-	else if (S_AXI_WVALID && S_AXI_WREADY && S_AXI_WLAST)
-		s_wbursts <= 1;
-	else if (S_AXI_BVALID && S_AXI_BREADY)
-		s_wbursts <= 0;
-	// }}}
-
-	// wfifo_id, wfifo_lock
-	// {{{
-	// Keep track of the ID of the last transaction.  Since we only
-	// ever have one write transaction outstanding, this will need to be
-	// the ID of the returned value.
-
-	assign	wfifo_id = r_awid;
-	assign	wfifo_lock = r_awlock;
-	// }}}
-
-	// m_wpending, m_wempty, m_wlastctr
-	// {{{
-	// m_wpending counts the number of (remaining) write data values that
-	// need to be sent to the slave.  It counts this number with respect
-	// to the *SLAVE*, not the master.  When m_wpending == 1, WLAST shall
-	// be true.  To make comparisons of (m_wpending == 0) or (m_wpending>0),
-	// m_wempty is assigned to (m_wpending).  Similarly, m_wlastctr is
-	// assigned to (m_wpending == 1).
-	//
-	initial	m_wpending = 0;
-	initial	m_wempty   = 1;
-	initial	m_wlastctr = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || o_write_fault)
-	begin
-		// {{{
-		m_wpending <= 0;
-		m_wempty   <= 1;
-		m_wlastctr <= 0;
-		// }}}
-	end else if (M_AXI_AWVALID && M_AXI_AWREADY)
-	begin
-		// {{{
-		if (M_AXI_WVALID && M_AXI_WREADY)
-		begin
-			// {{{
-			// Accepting AW* and W* packets on the same
-			// clock
-			if (m_wpending == 0)
-			begin
-				// The AW* and W* packets go together
-				m_wpending <= {1'b0, M_AXI_AWLEN};
-				m_wempty   <= (M_AXI_AWLEN == 0);
-				m_wlastctr <= (M_AXI_AWLEN == 1);
-			end else begin
-				// The W* packet goes with the last
-				// AW* command, the AW* packet with a
-				// new one
-				m_wpending <= M_AXI_AWLEN+1;
-				m_wempty   <= 0;
-				m_wlastctr <= (M_AXI_AWLEN == 0);
-			end
-			// }}}
-		end else begin
-			// {{{
-			m_wpending <= M_AXI_AWLEN+1;
-			m_wempty   <= 0;
-			m_wlastctr <= (M_AXI_AWLEN == 0);
-			// }}}
-		end
-		// }}}
-	end else if (M_AXI_WVALID && M_AXI_WREADY && (!m_wempty))
-	begin
-		// {{{
-		// The AW* channel is idle, and we just accepted a value
-		// on the W* channel
-		m_wpending <= m_wpending - 1;
-		m_wempty   <= (m_wpending <= 1);
-		m_wlastctr <= (m_wpending == 2);
-		// }}}
-	end
-	// }}}
-
-	// Write data processing
-	// {{{
-	// S_AXI_WREADY
-	// {{{
-	// The S_AXI_WREADY or write channel stall signal
-	//
-	// For this core, we idle at zero (stalled) until an AW* packet
-	// comes through
-	//
-	initial	S_AXI_WREADY = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		S_AXI_WREADY <= 0;
-	else if (S_AXI_WVALID && S_AXI_WREADY)
-	begin
-		// {{{
-		if (S_AXI_WLAST)
-			S_AXI_WREADY <= 0;
-		else if (o_write_fault)
-			S_AXI_WREADY <= 1;
-		else if (!M_AXI_WVALID || M_AXI_WREADY)
-			S_AXI_WREADY <= 1;
-		else
-			S_AXI_WREADY <= 0;
-		// }}}
-	end else if ((s_wbursts == 0)&&(waddr_valid)
-				&&(o_write_fault || M_AXI_WREADY))
-		S_AXI_WREADY <= 1;
-	else if (S_AXI_AWVALID && S_AXI_AWREADY)
-		S_AXI_WREADY <= 1;
-	// }}}
-
-	// r_w*
-	// {{{
-	// Double buffer for the write channel
-	//
-	// As before, the r_* values contain the values in the double
-	// buffer itself
-	//
-	initial	r_wvalid = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		r_wvalid <= 0;
-	else if (!r_wvalid)
-	begin
-		// {{{
-		r_wvalid <= (S_AXI_WVALID && S_AXI_WREADY
-				&& M_AXI_WVALID && !M_AXI_WREADY);
-		r_wdata <= S_AXI_WDATA;
-		r_wstrb <= S_AXI_WSTRB;
-		r_wlast <= S_AXI_WLAST;
-		// }}}
-	end else if (o_write_fault || M_AXI_WREADY || !M_AXI_ARESETN)
-		r_wvalid <= 0;
-	// }}}
-
-	// m_w*
-	// {{{
-	// Here's the result of our double buffer
-	//
-	// m_* references the value within the double buffer in the case that
-	// something is in the double buffer.  Otherwise, it is the values
-	// directly from the inputs.  In the case of a fault, neither is true.
-	// Write faults override.
-	//
-	always @(*)
-	if (o_write_fault)
-	begin
-		// {{{
-		m_wvalid = !m_wempty;
-		m_wlast  = m_wlastctr;
-		m_wstrb  = 0;
-		// }}}
-	end else if (r_wvalid)
-	begin
-		// {{{
-		m_wvalid = 1;
-		m_wstrb  = r_wstrb;
-		m_wlast  = r_wlast;
-		// }}}
-	end else begin
-		// {{{
-		m_wvalid = S_AXI_WVALID && S_AXI_WREADY;
-		m_wstrb  = S_AXI_WSTRB;
-		m_wlast  = S_AXI_WLAST;
-		// }}}
-	end
-	// }}}
-
-	// m_wdata
-	// {{{
-	// The logic for the DATA output of the double buffer doesn't
-	// matter so much in the case of o_write_fault
-	always @(*)
-	if (r_wvalid)
-		m_wdata = r_wdata;
-	else
-		m_wdata = S_AXI_WDATA;
-	// }}}
-
-	// M_AXI_W*
-	// {{{
-	// Set the downstream write channel values
-	//
-	// As per AXI spec, these values *must* be registered.  Note that our
-	// source here is the m_* double buffer/incoming write data switch.
-	initial	M_AXI_WVALID = 0;
-	always @(posedge S_AXI_ACLK)
-	begin
-		if (!M_AXI_WVALID || M_AXI_WREADY)
-		begin
-			M_AXI_WVALID <= m_wvalid;
-			M_AXI_WDATA  <= m_wdata;
-			M_AXI_WSTRB  <= m_wstrb;
-			if (OPT_EXCLUSIVE && lock_failed)
-				M_AXI_WSTRB <= 0;
-			M_AXI_WLAST  <= m_wlast;
-		end
-
-		// Override the WVALID signal (only) on reset, voiding any
-		// output we might otherwise send.
-		if (!M_AXI_ARESETN)
-			M_AXI_WVALID <= 0;
-	end
-	// }}}
-	// }}}
-
-	// Write fault detection
-	// {{{
-	// write_timer
-	// {{{
-	// The write timer
-	//
-	// The counter counts up to saturation.  It is reset any time
-	// the write channel is either clear, or a value is accepted
-	// at the *MASTER* (not slave) side.  Why the master side?  Simply
-	// because it makes the proof below easier.  (At one time I checked
-	// both, but then couldn't prove that the faults wouldn't get hit
-	// if the slave responded in time.)
-	initial	write_timer = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || !waddr_valid)
-		write_timer <= 0;
-	else if (!o_write_fault && M_AXI_BVALID)
-		write_timer <= 0;
-	else if (S_AXI_WREADY)
-		write_timer <= 0;
-	else if (!(&write_timer))
-		write_timer <= write_timer + 1;
-	// }}}
-
-	// write_timeout
-	// {{{
-	// Write timeout detector
-	//
-	// If the write_timer reaches the OPT_TIMEOUT, then the write_timeout
-	// will get set true.  This will force a fault, taking the write
-	// channel off line.
-	initial	write_timeout = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || clear_fault)
-		write_timeout <= 0;
-	else if (M_AXI_BVALID)
-		write_timeout <= write_timeout;
-	else if (S_AXI_WVALID && S_AXI_WREADY)
-		write_timeout <= write_timeout;
-	else if (write_timer >= OPT_TIMEOUT)
-		write_timeout <= 1;
-	// }}}
-
-	// faulty_write_return
-	// {{{
-	// fault_write_return
-	//
-	// This combinational logic is used to catch an invalid return, and
-	// so take the slave off-line before the return can corrupt the master
-	// channel.  Reasons for taking the write return off line are listed
-	// below.
-	always @(*)
-	begin
-		faulty_write_return = 0;
-		if (M_AXI_WVALID && M_AXI_WREADY
-				&& M_AXI_AWVALID && !M_AXI_AWREADY)
-			// Accepting the write *data* prior to the write
-			// *address* is a fault
-			faulty_write_return = 1;
-		if (M_AXI_BVALID)
-		begin
-			if (M_AXI_AWVALID || M_AXI_WVALID)
-				// Returning a B* acknowledgement while the
-				// request remains outstanding is also a fault
-				faulty_write_return = 1;
-			if (!m_wempty)
-				// Same as above, but this time the write
-				// channel is neither complete, nor is *WVALID
-				// active.  Values remain to be written,
-				// and so a return is a fault.
-				faulty_write_return = 1;
-			if (s_wbursts <= (S_AXI_BVALID ? 1:0))
-				// Too many acknowledgments
-				//
-				// Returning more than one BVALID&BREADY for
-				// every AWVALID & AWREADY is a fault.
-				faulty_write_return = 1;
-			if (M_AXI_BID != wfifo_id)
-				// An attempt to return the wrong ID
-				faulty_write_return = 1;
-			if (M_AXI_BRESP == EXOKAY && (!OPT_EXCLUSIVE
-					|| !lock_enabled))
-				// An attempt to return a valid lock, without
-				// a prior request
-				faulty_write_return = 1;
-		end
-	end
-	// }}}
-
-	// o_write_fault
-	// {{{
-	// On a write fault, we're going to disconnect the write port from
-	// the slave, and return errors on each write connect.  o_write_fault
-	// is our signal determining if the write channel is disconnected.
-	//
-	// Most of this work is determined within faulty_write_return above.
-	// Here we do just a bit more:
-	initial	o_write_fault = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || clear_fault)
-		o_write_fault <= 0;
-	else if ((!M_AXI_ARESETN&&o_read_fault) || write_timeout)
-		o_write_fault <= 1;
-	else if (M_AXI_BVALID && M_AXI_BREADY)
-		o_write_fault <= (o_write_fault) || faulty_write_return;
-	else if (M_AXI_WVALID && M_AXI_WREADY
-			&& M_AXI_AWVALID && !M_AXI_AWREADY)
-		// Accepting the write data prior to the write address
-		// is a fault
-		o_write_fault <= 1;
-	// }}}
-	// }}}
-
-	// Write return generation
-	// {{{
-	// m_b*
-	// {{{
-	// Since we only ever allow a single write burst at a time, we don't
-	// need to double buffer the return channel.  Hence, we'll set our
-	// return channel based upon the incoming values alone.  Note that
-	// we're overriding the M_AXI_BID below, in order to make certain that
-	// the return goes to the right source.
-	//
-	always @(*)
-	if (o_write_fault)
-	begin
-		m_bvalid = (s_wbursts > (S_AXI_BVALID ? 1:0));
-		m_bid    = wfifo_id;
-		m_bresp  = SLAVE_ERROR;
-	end else begin
-		m_bvalid = M_AXI_BVALID;
-		if (faulty_write_return)
-			m_bvalid = 0;
-		m_bid    = wfifo_id;
-		m_bresp  = M_AXI_BRESP;
-	end
-	// }}}
-
-	// S_AXI_B*
-	// {{{
-	// We'll *never* stall the slaves BREADY channel
-	//
-	// If the slave returns the response we are expecting, then S_AXI_BVALID
-	// will be low and it can go directly into the S_AXI_BVALID slot.  If
-	// on the other hand the slave returns M_AXI_BVALID at the wrong time,
-	// then we'll quietly accept it and send the write interface into
-	// fault detected mode, setting o_write_fault.
-	//
-	// Sadly, this will create a warning in Vivado.  If/when you see it,
-	// see this note and then just ignore it.
-	assign M_AXI_BREADY = 1;
-
-	//
-	// Return a write acknowlegement at the end of every write
-	// burst--regardless of whether or not the slave does so
-	//
-	initial	S_AXI_BVALID = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		S_AXI_BVALID <= 0;
-	else if (!S_AXI_BVALID || S_AXI_BREADY)
-		S_AXI_BVALID <= m_bvalid;
-
-	//
-	// Set the values associated with the response
-	//
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_BVALID || S_AXI_BREADY)
-	begin
-		S_AXI_BID    <= m_bid;
-		S_AXI_BRESP  <= m_bresp;
-	end
-	// }}}
-
-	// }}}
-
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Read channel processing
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	//
-	// Read address channel
-	// {{{
-
-	// S_AXI_ARREADY
-	// {{{
-	initial	S_AXI_ARREADY = (OPT_SELF_RESET) ? 0:1;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		S_AXI_ARREADY <= !OPT_SELF_RESET;
-	else if (S_AXI_ARVALID && S_AXI_ARREADY)
-		S_AXI_ARREADY <= 0;
-	// else if (clear_fault)
-	//	S_AXI_ARREADY <= 1;
-	else if (!S_AXI_ARREADY)
-		S_AXI_ARREADY <= (S_AXI_RVALID && S_AXI_RLAST && S_AXI_RREADY);
-	// }}}
-
-	// raddr_valid
-	// {{{
-	generate if (OPT_SELF_RESET)
-	begin : GEN_READ_RESET
-		assign	raddr_valid = !rfifo_empty;
-	end else begin : SIMPLE_RADDR_VALID
-		assign	raddr_valid = !S_AXI_ARREADY;
-	end endgenerate
-	// }}}
-
-	// r_ar*
-	// {{{
-	// Double buffer the values associated with any read address request
-	//
-	initial	r_arvalid = 0;
-	always @(posedge S_AXI_ACLK)
-	begin
-		if (S_AXI_ARVALID && S_AXI_ARREADY)
-		begin
-			r_arvalid <= 0; // (M_AXI_ARVALID && !M_AXI_ARREADY);
-			r_arid    <= S_AXI_ARID;
-			r_araddr  <= S_AXI_ARADDR;
-			r_arlen   <= S_AXI_ARLEN;
-			r_arsize  <= S_AXI_ARSIZE;
-			r_arburst <= S_AXI_ARBURST;
-			r_arlock  <= S_AXI_ARLOCK;
-			r_arcache <= S_AXI_ARCACHE;
-			r_arprot  <= S_AXI_ARPROT;
-			r_arqos   <= S_AXI_ARQOS;
-		end else if (M_AXI_ARREADY)
-			r_arvalid <= 0;
-
-		if (!M_AXI_ARESETN)
-			r_arvalid <= 0;
-		if (!OPT_EXCLUSIVE || !S_AXI_ARESETN)
-			r_arlock <= 1'b0;
-	end
-	// }}}
-
-	// m_ar*
-	// {{{
-	always @(*)
-	if (r_arvalid)
-	begin
-		m_arvalid = r_arvalid;
-		m_arid    = r_arid;
-		m_araddr  = r_araddr;
-		m_arlen   = r_arlen;
-		m_arsize  = r_arsize;
-		m_arburst = r_arburst;
-		m_arlock  = r_arlock;
-		m_arcache = r_arcache;
-		m_arprot  = r_arprot;
-		m_arqos   = r_arqos;
-	end else begin
-		m_arvalid = S_AXI_ARVALID && S_AXI_ARREADY;
-		m_arid    = S_AXI_ARID;
-		m_araddr  = S_AXI_ARADDR;
-		m_arlen   = S_AXI_ARLEN;
-		m_arsize  = S_AXI_ARSIZE;
-		m_arburst = S_AXI_ARBURST;
-		m_arlock  = S_AXI_ARLOCK && OPT_EXCLUSIVE;
-		m_arcache = S_AXI_ARCACHE;
-		m_arprot  = S_AXI_ARPROT;
-		m_arqos   = S_AXI_ARQOS;
-	end
-	// }}}
-
-	// M_AXI_AR*
-	// {{{
-	// Set the downstream values according to the transaction we've just
-	// received.
-	//
-	initial	M_AXI_ARVALID = 0;
-	always @(posedge S_AXI_ACLK)
-	begin
-		if (!M_AXI_ARVALID || M_AXI_ARREADY)
-		begin
-
-			if (o_read_fault)
-				M_AXI_ARVALID <= 0;
-			else
-				M_AXI_ARVALID <= m_arvalid;
-
-			M_AXI_ARID    <= m_arid;
-			M_AXI_ARADDR  <= m_araddr;
-			M_AXI_ARLEN   <= m_arlen;
-			M_AXI_ARSIZE  <= m_arsize;
-			M_AXI_ARBURST <= m_arburst;
-			M_AXI_ARLOCK  <= m_arlock && OPT_EXCLUSIVE;
-			M_AXI_ARCACHE <= m_arcache;
-			M_AXI_ARPROT  <= m_arprot;
-			M_AXI_ARQOS   <= m_arqos;
-		end
-
-		if (!M_AXI_ARESETN)
-			M_AXI_ARVALID <= 0;
-	end
-	// }}}
-
-	// }}}
-
-	//
-	// Read fault detection
-	// {{{
-
-	// read_timer
-	// {{{
-	// First step: a timer.  The timer starts as soon as the S_AXI_ARVALID
-	// is accepted.  Once that happens, rfifo_empty will no longer be true.
-	// The count is reset any time the slave produces a value for us to
-	// read.  Once the count saturates, it stops counting.
-	initial	read_timer = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || clear_fault)
-		read_timer <= 0;
-	else if (rfifo_empty||(S_AXI_RVALID))
-		read_timer <= 0;
-	else if (M_AXI_RVALID)
-		read_timer <= 0;
-	else if (!(&read_timer))
-		read_timer <= read_timer + 1;
-	// }}}
-
-	// read_timeout
-	// {{{
-	// Once the counter > OPT_TIMEOUT, we have a timeout condition.
-	// We'll detect this one clock earlier below.  If we ever enter
-	// a read time out condition, we'll set the read fault.  The read
-	// timeout condition can only be cleared by a reset.
-	initial	read_timeout = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || clear_fault)
-		read_timeout <= 0;
-	else if (rfifo_empty||S_AXI_RVALID)
-		read_timeout <= read_timeout;
-	else if (M_AXI_RVALID)
-		read_timeout <= read_timeout;
-	else if (read_timer == OPT_TIMEOUT)
-		read_timeout <= 1;
-	// }}}
-
-	//
-	// faulty_read_return
-	// {{{
-	// To avoid returning a fault from the slave, it is important to
-	// determine within a single clock period whether or not the slaves
-	// return value is at fault or not.  That's the purpose of the code
-	// below.
-	always @(*)
-	begin
-		faulty_read_return = 0;
-		if (M_AXI_RVALID)
-		begin
-			if (M_AXI_ARVALID)
-				// It is a fault to return data before the
-				// request has been accepted
-				faulty_read_return = 1;
-			if (M_AXI_RID != rfifo_id)
-				// It is a fault to return data from a
-				// different ID
-				faulty_read_return = 1;
-			if (rfifo_last && (S_AXI_RVALID || !M_AXI_RLAST))
-				faulty_read_return = 1;
-			if (rfifo_penultimate && S_AXI_RVALID && (r_rvalid || !M_AXI_RLAST))
-				faulty_read_return = 1;
-			if (M_AXI_RRESP == EXOKAY && (!OPT_EXCLUSIVE || !rfifo_lock))
-				faulty_read_return = 1;
-			if (OPT_EXCLUSIVE && exread && M_AXI_RRESP == OKAY)
-				// Can't switch from EXOKAY to OKAY
-				faulty_read_return = 1;
-			if ((!OPT_EXCLUSIVE || (!rfifo_first && !exread))
-						&& M_AXI_RRESP == EXOKAY)
-				// Can't switch from OKAY to EXOKAY
-				faulty_read_return = 1;
-		end
-	end
-	// }}}
-
-	// o_read_fault
-	// {{{
-	initial	o_read_fault = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || clear_fault)
-		o_read_fault <= 0;
-	else if ((!M_AXI_ARESETN && o_write_fault) || read_timeout)
-		o_read_fault <= 1;
-	else if (M_AXI_RVALID)
-	begin
-		if (faulty_read_return)
-			o_read_fault <= 1;
-		if (!raddr_valid)
-			// It is a fault if we haven't issued an AR* request
-			// yet, and a value is returned
-			o_read_fault <= 1;
-	end
-	// }}}
-
-	// }}}
-
-	//
-	// Read return/acknowledgment processing
-	// {{{
-
-
-	// exread
-	// {{{
-	always @(posedge S_AXI_ACLK)
-	if (!M_AXI_ARESETN || !OPT_EXCLUSIVE)
-		exread <= 0;
-	else if (M_AXI_RVALID && M_AXI_RREADY)
-	begin
-		if (!M_AXI_RRESP[1])
-			exread <= (M_AXI_RRESP == EXOKAY);
-	end else if (S_AXI_RVALID && S_AXI_RREADY)
-	begin
-		if (S_AXI_RLAST)
-			exread <= 1'b0;
-	end
-	// }}}
-
-	// r_rvalid
-	// {{{
-	// Step one, set/create the read return double buffer.  If r_rvalid
-	// is true, there's a valid value in the double buffer location.
-	//
-	initial r_rvalid = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || o_read_fault)
-		r_rvalid <= 0;
-	else if (!r_rvalid)
-	begin
-		// {{{
-		// Refuse to set the double-buffer valid on any fault.
-		// That will also keep (below) M_AXI_RREADY high--so that
-		// following the fault the slave might still (pretend) to
-		// respond properly
-		if (faulty_read_return)
-			r_rvalid <= 0;
-		else if (o_read_fault)
-			r_rvalid <= 0;
-		// If there's nothing in the double buffer, then we might
-		// place something in there.  The double buffer only gets
-		// filled under two conditions: 1) something is pending to be
-		// returned, and 2) there's another return that we can't
-		// stall and so need to accept here.
-		r_rvalid <= M_AXI_RVALID && M_AXI_RREADY
-				&& (S_AXI_RVALID && !S_AXI_RREADY);
-		// }}}
-	end else if (S_AXI_RREADY)
-		// Once the up-stream read-channel clears, we can always
-		// clear the double buffer
-		r_rvalid <= 0;
-	// }}}
-
-	// r_rresp, r_rdata
-	// {{{
-	// Here's the actual values kept whenever r_rvalid is true.  This is
-	// the double buffer.  Notice that r_rid and r_last are generated
-	// locally, so not recorded here.
-	//
-	always @(posedge S_AXI_ACLK)
-	if (!r_rvalid)
-	begin
-		r_rresp  <= M_AXI_RRESP;
-		r_rdata  <= M_AXI_RDATA;
-	end
-	// }}}
-
-	// M_AXI_RREADY
-	// {{{
-	// Stall the downstream channel any time there's something in the
-	// double buffer.  In spite of the ! here, this is a registered value.
-	assign M_AXI_RREADY = !r_rvalid;
-	// }}}
-
-	// rfifo_id, rfifo_lock
-	// {{{
-	// Copy the ID for later comparisons on the return
-	always @(*)
-		rfifo_id = r_arid;
-	always @(*)
-		rfifo_lock = r_arlock;
-	// }}}
-
-	// rfifo_[counter|empty|last|penultimate
-	// {{{
-	// Count the number of outstanding read elements.  This is the number
-	// of read returns we still expect--from the upstream perspective.  The
-	// downstream perspective will be off by both what's waiting for
-	// S_AXI_RREADY and what's in the double buffer
-	//
-	initial	rfifo_counter    = 0;
-	initial	rfifo_empty      = 1;
-	initial	rfifo_last       = 0;
-	initial	rfifo_penultimate= 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-	begin
-		rfifo_counter    <= 0;
-		rfifo_empty      <= 1;
-		rfifo_last       <= 0;
-		rfifo_penultimate<= 0;
-	end else if (S_AXI_ARVALID && S_AXI_ARREADY)
-	begin
-		rfifo_counter <= S_AXI_ARLEN+1;
-		rfifo_empty   <= 0;
-		rfifo_last    <= (S_AXI_ARLEN == 0);
-		rfifo_penultimate <= (S_AXI_ARLEN == 1);
-	end else if (!rfifo_empty)
-	begin
-		if (S_AXI_RVALID && S_AXI_RREADY)
-		begin
-			rfifo_counter <= rfifo_counter - 1;
-			rfifo_empty   <= (rfifo_counter <= 1);
-			rfifo_last    <= (rfifo_counter == 2);
-			rfifo_penultimate <= (rfifo_counter == 3);
-		end
-	end
-	// }}}
-
-	// lock_active
-	// {{{
-	generate if (OPT_EXCLUSIVE)
-	begin : CALC_LOCK_ACTIVE
-		// {{{
-		genvar	gk;
-
-		for(gk=0; gk<(1<<IW); gk=gk+1)
-		begin : LOCK_PER_ID
-			reg	r_lock_active;
-
-			initial	r_lock_active = 0;
-			always @(posedge S_AXI_ACLK)
-			if (!S_AXI_ARESETN || !M_AXI_ARESETN
-				|| faulty_read_return || faulty_write_return)
-				r_lock_active <= 0;
-			else if (M_AXI_RVALID && M_AXI_RREADY && rfifo_lock
-					&& !S_AXI_ARREADY
-					&& r_arid == gk[IW-1:0]
-					&&(!faulty_read_return && !o_read_fault)
-					&& M_AXI_RRESP == EXOKAY)
-				r_lock_active <= 1;
-			else if (M_AXI_BVALID && M_AXI_BREADY && wfifo_lock
-					&& r_awid == gk[IW-1:0]
-					&& (S_AXI_ARREADY
-						|| r_arid != gk[IW-1:0]
-						|| !r_arlock)
-					&& M_AXI_BRESP == OKAY)
-				r_lock_active <= 0;
-			else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLOCK
-					&& S_AXI_ARID == gk[IW-1:0])
-				r_lock_active <= 0;
-
-			assign	lock_active[gk] = r_lock_active;
-		end
-		// }}}
-	end else begin : LOCK_NEVER_ACTIVE
-		// {{{
-		assign	lock_active = 0;
-
-		// Keep Verilator happy
-		// Verilator lint_off UNUSED
-		wire	unused_lock;
-		assign	unused_lock = &{ 1'b0, wfifo_lock };
-		// Verilator lint_on  UNUSED
-		// }}}
-	end endgenerate
-	// }}}
-
-	// rfifo_first
-	// {{{
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || !OPT_EXCLUSIVE)
-		rfifo_first <= 1'b0;
-	else if (S_AXI_ARVALID && S_AXI_ARREADY)
-		rfifo_first <= 1'b1;
-	else if (M_AXI_RVALID && M_AXI_RREADY)
-		rfifo_first <= 1'b0;
-	else if (o_read_fault)
-		rfifo_first <= 1'b0;
-	// }}}
-
-	// m_rvalid, m_rresp
-	// {{{
-	// Determine values to send back and return
-	//
-	// This data set includes all the return values, even though only
-	// RRESP and RVALID are set in this block.
-	always @(*)
-	if (o_read_fault || (!M_AXI_ARESETN && OPT_SELF_RESET))
-	begin
-		m_rvalid = !rfifo_empty;
-		if (S_AXI_RVALID && rfifo_last)
-			m_rvalid = 0;
-		m_rresp  = SLAVE_ERROR;
-	end else if (r_rvalid)
-	begin
-		m_rvalid = r_rvalid;
-		m_rresp  = r_rresp;
-	end else begin
-		m_rvalid = M_AXI_RVALID && raddr_valid && !faulty_read_return;
-		m_rresp  = M_AXI_RRESP;
-	end
-	// }}}
-
-	// m_rid
-	// {{{
-	// We've stored the ID locally, so that our response will never be in
-	// error
-	always @(*)
-		m_rid = rfifo_id;
-	// }}}
-
-	// m_rlast
-	// {{{
-	// Ideally, we'd want to say m_rlast = rfifo_last.  However, we might
-	// have a value in S_AXI_RVALID already.  In that case, the last
-	// value can only be true if we are one further away from the end.
-	// (Remember, rfifo_last and rfifo_penultimate are both dependent upon
-	// the *upstream* number of read values outstanding, not the downstream
-	// number which we can't trust in all cases)
-	always @(*)
-	if (S_AXI_RVALID)
-		m_rlast = rfifo_penultimate;
-	else
-		m_rlast = (rfifo_last);
-	// }}}
-
-	// m_rdata
-	// {{{
-	// In the case of a fault, rdata is a don't care.  Therefore we can
-	// always set it based upon the values returned from the slave.
-	always @(*)
-	if (r_rvalid)
-		m_rdata = r_rdata;
-	else
-		m_rdata = M_AXI_RDATA;
-	// }}}
-
-	// S_AXI_R*
-	// {{{
-	// Record our return data values
-	//
-	// These are the values from either the slave, the double buffer,
-	// or an error value bypassing either as determined by the m_* values.
-	// Per spec, all of these values must be registered.  First the valid
-	// signal
-	initial	S_AXI_RVALID = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN)
-		S_AXI_RVALID <= 0;
-	else if (!S_AXI_RVALID || S_AXI_RREADY)
-		S_AXI_RVALID <= m_rvalid;
-
-	// Then the various slave data channels
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_RVALID || S_AXI_RREADY)
-	begin
-		S_AXI_RID    <= m_rid;
-		S_AXI_RRESP  <= m_rresp;
-		S_AXI_RLAST  <= m_rlast;
-		S_AXI_RDATA  <= m_rdata;
-	end
-	// }}}
-
-	// }}}
-
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Self-reset
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	generate if (OPT_SELF_RESET)
-	begin : GEN_SELFRESET
-		// {{{
-		// Declarations
-		// {{{
-		reg	[4:0]	reset_counter;
-		reg		r_clear_fault, w_clear_fault;
-		wire		reset_timeout;
-		// }}}
-
-		// M_AXI_ARESETN
-		// {{{
-		initial	M_AXI_ARESETN = 0;
-		always @(posedge S_AXI_ACLK)
-		if (!S_AXI_ARESETN)
-			M_AXI_ARESETN <= 0;
-		else if (clear_fault)
-			M_AXI_ARESETN <= 1;
-		else if (o_read_fault || o_write_fault)
-			M_AXI_ARESETN <= 0;
-		// }}}
-
-		// reset_counter
-		// {{{
-		initial	reset_counter = 0;
-		always @(posedge S_AXI_ACLK)
-		if (M_AXI_ARESETN)
-			reset_counter <= 0;
-		else if (!reset_timeout)
-			reset_counter <= reset_counter+1;
-		// }}}
-
-		assign	reset_timeout = reset_counter[4];
-
-		// r_clear_fault
-		// {{{
-		initial	r_clear_fault <= 1;
-		always @(posedge S_AXI_ACLK)
-		if (!S_AXI_ARESETN)
-			r_clear_fault <= 1;
-		else if (!M_AXI_ARESETN && !reset_timeout)
-			r_clear_fault <= 0;
-		else if (!o_read_fault && !o_write_fault)
-			r_clear_fault <= 0;
-		else if (raddr_valid || waddr_valid)
-			r_clear_fault <= 0;
-		else
-			r_clear_fault <= 1;
-		// }}}
-
-		// clear_fault
-		// {{{
-		always @(*)
-		if (S_AXI_AWVALID || S_AXI_ARVALID)
-			w_clear_fault = 0;
-		else if (raddr_valid || waddr_valid)
-			w_clear_fault = 0;
-		else
-			w_clear_fault = r_clear_fault;
-
-		assign	clear_fault = w_clear_fault;
-		// }}}
-
-		// }}}
-	end else begin : NO_SELFRESET
-		// {{{
-		always @(*)
-			M_AXI_ARESETN = S_AXI_ARESETN;
-		assign	clear_fault = 0;
-		// }}}
-	end endgenerate
-	// }}}
-
-	// Make Verilator happy
-	// {{{
-	// Verilator lint_off UNUSED
-	wire	unused;
-	assign	unused = &{ 1'b0 };
-	// Verilator lint_on  UNUSED
-	// }}}
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-//
-// Formal properties
-// {{{
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-////////////////////////////////////////////////////////////////////////////////
-`ifdef	FORMAL
-	// {{{
-	// Below are just some of the formal properties used to verify
-	// this core.  The full property set is maintained elsewhere.
-	//
-	parameter [0:0]	F_OPT_FAULTLESS = 1;
-
-	//
-	// ...
-	// }}}
-
-	faxi_slave	#(
-		// {{{
-		.C_AXI_ID_WIDTH(C_S_AXI_ID_WIDTH),
-		.C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH),
-		.C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH)
-		// ...
-		// }}}
-	) f_slave(
-		// {{{
-		.i_clk(S_AXI_ACLK),
-		.i_axi_reset_n(S_AXI_ARESETN),
-		//
-		// Address write channel
-		// {{{
-		.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_awvalid(S_AXI_AWVALID),
-		.i_axi_awready(S_AXI_AWREADY),
-		// }}}
-		// Write Data Channel
-		// {{{
-		.i_axi_wdata(S_AXI_WDATA),
-		.i_axi_wstrb(S_AXI_WSTRB),
-		.i_axi_wlast(S_AXI_WLAST),
-		.i_axi_wvalid(S_AXI_WVALID),
-		.i_axi_wready(S_AXI_WREADY),
-		// }}}
-		// Write response channel
-		// {{{
-		.i_axi_bid(S_AXI_BID),
-		.i_axi_bresp(S_AXI_BRESP),
-		.i_axi_bvalid(S_AXI_BVALID),
-		.i_axi_bready(S_AXI_BREADY),
-		// }}}
-		// Read address channel
-		// {{{
-		.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_arvalid(S_AXI_ARVALID),
-		.i_axi_arready(S_AXI_ARREADY),
-		// }}}
-		// Read data return channel
-		// {{{
-		.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_rresp(S_AXI_RRESP),
-		.i_axi_rlast(S_AXI_RLAST),
-		// }}}
-		// Formal induction values
-		// {{{
-		.f_axi_awr_nbursts(f_axi_awr_nbursts),
-		.f_axi_wr_pending(f_axi_wr_pending),
-		.f_axi_rd_nbursts(f_axi_rd_nbursts),
-		.f_axi_rd_outstanding(f_axi_rd_outstanding)
-		//
-		// ...
-		// }}}
-		// }}}
-	);
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Write induction properties
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	// 1. We will only ever handle a single burst--never any more
-	always @(*)
-		assert(f_axi_awr_nbursts <= 1);
-
-	always @(*)
-	if (f_axi_awr_nbursts == 1)
-	begin
-		assert(!S_AXI_AWREADY);
-		if (S_AXI_BVALID)
-			assert(f_axi_wr_pending == 0);
-		if (!o_write_fault && M_AXI_AWVALID)
-			assert(f_axi_wr_pending == M_AXI_AWLEN + 1
-					- (M_AXI_WVALID ? 1:0)
-					- (r_wvalid ? 1 : 0));
-		if (!o_write_fault && f_axi_wr_pending > 0)
-			assert((!M_AXI_WVALID || !M_AXI_WLAST)
-					&&(!r_wvalid || !r_wlast));
-		if (!o_write_fault && M_AXI_WVALID && M_AXI_WLAST)
-			assert(!r_wvalid || !r_wlast);
-	end else begin
-		assert(s_wbursts == 0);
-		assert(!S_AXI_WREADY);
-		if (OPT_SELF_RESET)
-		begin
-			assert(1 || S_AXI_AWREADY || !M_AXI_ARESETN || !S_AXI_ARESETN);
-		end else
-			assert(S_AXI_AWREADY);
-	end
-
-	//
-	// ...
-	//
-
-	//
-	// AWREADY will always be low mid-burst
-	always @(posedge S_AXI_ACLK)
-	if (!f_past_valid || $past(!S_AXI_ARESETN))
-	begin
-		assert(S_AXI_AWREADY == !OPT_SELF_RESET);
-	end else if (f_axi_wr_pending > 0)
-	begin
-		assert(!S_AXI_AWREADY);
-	end else if (s_wbursts)
-	begin
-		assert(!S_AXI_AWREADY);
-	end else if (!OPT_SELF_RESET)
-	begin
-		assert(S_AXI_AWREADY);
-	end else if (!o_write_fault && !o_read_fault)
-		assert(S_AXI_AWREADY || OPT_SELF_RESET);
-
-	always @(*)
-	if (f_axi_wr_pending > 0)
-	begin
-		assert(s_wbursts == 0);
-	end else if (f_axi_awr_nbursts > 0)
-	begin
-		assert((s_wbursts ? 1:0) == f_axi_awr_nbursts);
-	end else
-		assert(s_wbursts == 0);
-
-	always @(*)
-	if (!o_write_fault && S_AXI_AWREADY)
-		assert(!M_AXI_AWVALID);
-
-	always @(*)
-	if (M_AXI_ARESETN && (f_axi_awr_nbursts == 0))
-	begin
-		assert(o_write_fault || !M_AXI_AWVALID);
-		assert(!S_AXI_BVALID);
-		assert(s_wbursts == 0);
-	end else if (M_AXI_ARESETN && s_wbursts == 0)
-		assert(f_axi_wr_pending > 0);
-
-	always @(*)
-	if (S_AXI_WREADY)
-	begin
-		assert(waddr_valid);
-	end else if (f_axi_wr_pending > 0)
-	begin
-		if (!o_write_fault)
-			assert(M_AXI_WVALID && r_wvalid);
-	end
-
-	always @(*)
-	if (!OPT_SELF_RESET)
-	begin
-		assert(waddr_valid == !S_AXI_AWREADY);
-	end else begin
-		// ...
-		assert(waddr_valid == (f_axi_awr_nbursts > 0));
-	end
-
-	always @(*)
-	if (S_AXI_ARESETN && !o_write_fault && f_axi_wr_pending > 0 && !S_AXI_WREADY)
-		assert(M_AXI_WVALID);
-
-	always @(*)
-	if (S_AXI_ARESETN && !o_write_fault && m_wempty)
-	begin
-		assert(M_AXI_AWVALID || !M_AXI_WVALID);
-		assert(M_AXI_AWVALID || f_axi_wr_pending == 0);
-	end
-
-	always @(*)
-	if (S_AXI_ARESETN && M_AXI_AWVALID)
-	begin
-		if (!o_write_fault && !M_AXI_AWVALID)
-		begin
-			assert(f_axi_wr_pending + (M_AXI_WVALID ? 1:0) + (r_wvalid ? 1:0) == m_wpending);
-		end else if (!o_write_fault)
-		begin
-			assert(f_axi_wr_pending == M_AXI_AWLEN + 1 - (M_AXI_WVALID ? 1:0) - (r_wvalid ? 1:0));
-			assert(m_wpending == 0);
-		end
-	end
-
-	always @(*)
-		assert(m_wpending <= 9'h100);
-
-	always @(*)
-	if (M_AXI_ARESETN && (!o_write_fault)&&(f_axi_awr_nbursts == 0))
-		assert(!M_AXI_AWVALID);
-
-	always @(*)
-	if (S_AXI_ARESETN && !o_write_fault)
-	begin
-		if (f_axi_awr_nbursts == 0)
-		begin
-			assert(!M_AXI_AWVALID);
-			assert(!M_AXI_WVALID);
-		end
-
-		if (!M_AXI_AWVALID)
-			assert(f_axi_wr_pending
-					+(M_AXI_WVALID ? 1:0)
-					+ (r_wvalid ? 1:0)
-				== m_wpending);
-		if (f_axi_awr_nbursts == (S_AXI_BVALID ? 1:0))
-		begin
-			assert(!M_AXI_AWVALID);
-			assert(!M_AXI_WVALID);
-		end
-
-		if (S_AXI_BVALID)
-			assert(f_axi_awr_nbursts == 1);
-
-		if (M_AXI_AWVALID)
-			assert(m_wpending == 0);
-
-		if (S_AXI_AWREADY)
-			assert(!M_AXI_AWVALID);
-	end
-
-	always @(*)
-		assert(!r_awvalid);
-
-	always @(*)
-		assert(m_wempty == (m_wpending == 0));
-	always @(*)
-		assert(m_wlastctr == (m_wpending == 1));
-
-	//
-	// Verify the contents of the skid buffers
-	//
-
-	//
-	// ...
-	//
-
-	always @(*)
-	if (write_timer > OPT_TIMEOUT)
-		assert(o_write_fault || write_timeout);
-
-	always @(*)
-	if (!OPT_SELF_RESET)
-	begin
-		assert(waddr_valid == !S_AXI_AWREADY);
-	end else if (waddr_valid)
-		assert(!S_AXI_AWREADY);
-
-	always @(*)
-	if (!o_write_fault && M_AXI_ARESETN)
-		assert(waddr_valid == !S_AXI_AWREADY);
-
-	always @(*)
-	if (f_axi_wr_pending == 0)
-		assert(!S_AXI_WREADY);
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Read induction properties
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-
-	always @(*)
-		assert(f_axi_rd_nbursts <= 1);
-	always @(*)
-		assert(raddr_valid == (f_axi_rd_nbursts>0));
-	always @(*)
-	if (f_axi_rdid_nbursts > 0)
-	begin
-		assert(rfifo_id == f_axi_rd_checkid);
-	end else if (f_axi_rd_nbursts > 0)
-		assert(rfifo_id != f_axi_rd_checkid);
-
-	always @(*)
-	if (f_axi_rd_nbursts > 0)
-		assert(raddr_valid);
-
-	always @(*)
-	if (raddr_valid)
-		assert(!S_AXI_ARREADY);
-
-	always @(*)
-	if (!OPT_SELF_RESET)
-	begin
-		assert(raddr_valid == !S_AXI_ARREADY);
-	end else begin
-		// ...
-		assert(raddr_valid == (f_axi_rd_nbursts > 0));
-	end
-
-	//
-	// ...
-	//
-
-	always @(*)
-	if (f_axi_rd_outstanding == 0)
-		assert(!raddr_valid || OPT_SELF_RESET);
-
-	always @(*)
-	if (!o_read_fault && S_AXI_ARREADY)
-		assert(!M_AXI_ARVALID);
-
-	// Our "FIFO" counter
-	always @(*)
-		assert(rfifo_counter == f_axi_rd_outstanding);
-
-	always @(*)
-	begin
-		assert(rfifo_empty       == (rfifo_counter == 0));
-		assert(rfifo_last        == (rfifo_counter == 1));
-		assert(rfifo_penultimate == (rfifo_counter == 2));
-	end
-
-	//
-	// ...
-	//
-
-	always @(*)
-	if (r_arvalid)
-		assert(skid_arvalid);
-
-	always @(*)
-	if (read_timer > OPT_TIMEOUT)
-		assert(read_timeout);
-
-
-	always @(posedge S_AXI_ACLK)
-	if (OPT_SELF_RESET && (!f_past_valid || !$past(M_AXI_ARESETN)))
-	begin
-		assume(!M_AXI_BVALID);
-		assume(!M_AXI_RVALID);
-	end
-
-	always @(*)
-	if (!o_read_fault && M_AXI_ARESETN)
-		assert(raddr_valid == !S_AXI_ARREADY);
-
-	always @(*)
-	if (f_axi_rd_nbursts > 0)
-		assert(raddr_valid);
-
-	always @(*)
-	if (S_AXI_ARESETN && OPT_SELF_RESET)
-	begin
-		if (!M_AXI_ARESETN)
-			assert(o_read_fault || o_write_fault /* ... */ );
-	end
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Exclusive access property checking
-	// {{{
-	//
-	////////////////////////////////////////////////////////////////////////
-	//
-	// ...
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Cover properties
-	//
-	////////////////////////////////////////////////////////////////////////
-	//
-	// }}}
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Good interface check
-	//
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	generate if (F_OPT_FAULTLESS)
-	begin : ASSUME_FAULTLESS
-		// {{{
-		//
-		// ...
-		//
-
-		faxi_master #(
-			// {{{
-			.C_AXI_ID_WIDTH(C_S_AXI_ID_WIDTH),
-			.C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH),
-			.C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH)
-			// ...
-			// }}}
-		) f_master(
-			// {{{
-			.i_clk(S_AXI_ACLK),
-			.i_axi_reset_n(M_AXI_ARESETN),
-			//
-			// Address write channel
-			// {{{
-			.i_axi_awid(M_AXI_AWID),
-			.i_axi_awaddr(M_AXI_AWADDR),
-			.i_axi_awlen(M_AXI_AWLEN),
-			.i_axi_awsize(M_AXI_AWSIZE),
-			.i_axi_awburst(M_AXI_AWBURST),
-			.i_axi_awlock(M_AXI_AWLOCK),
-			.i_axi_awcache(M_AXI_AWCACHE),
-			.i_axi_awprot(M_AXI_AWPROT),
-			.i_axi_awqos(M_AXI_AWQOS),
-			.i_axi_awvalid(M_AXI_AWVALID),
-			.i_axi_awready(M_AXI_AWREADY),
-			// }}}
-			// Write Data Channel
-			// {{{
-			.i_axi_wvalid(M_AXI_WVALID),
-			.i_axi_wready(M_AXI_WREADY),
-			.i_axi_wdata(M_AXI_WDATA),
-			.i_axi_wstrb(M_AXI_WSTRB),
-			.i_axi_wlast(M_AXI_WLAST),
-			// }}}
-			// Write response channel
-			// {{{
-			.i_axi_bvalid(M_AXI_BVALID),
-			.i_axi_bready(M_AXI_BREADY),
-			.i_axi_bid(M_AXI_BID),
-			.i_axi_bresp(M_AXI_BRESP),
-			// }}}
-			// Read address channel
-			// {{{
-			.i_axi_arid(M_AXI_ARID),
-			.i_axi_araddr(M_AXI_ARADDR),
-			.i_axi_arlen(M_AXI_ARLEN),
-			.i_axi_arsize(M_AXI_ARSIZE),
-			.i_axi_arburst(M_AXI_ARBURST),
-			.i_axi_arlock(M_AXI_ARLOCK),
-			.i_axi_arcache(M_AXI_ARCACHE),
-			.i_axi_arprot(M_AXI_ARPROT),
-			.i_axi_arqos(M_AXI_ARQOS),
-			.i_axi_arvalid(M_AXI_ARVALID),
-			.i_axi_arready(M_AXI_ARREADY),
-			// }}}
-			// Read data return channel
-			// {{{
-			.i_axi_rvalid(M_AXI_RVALID),
-			.i_axi_rready(M_AXI_RREADY),
-			.i_axi_rid(M_AXI_RID),
-			.i_axi_rdata(M_AXI_RDATA),
-			.i_axi_rresp(M_AXI_RRESP),
-			.i_axi_rlast(M_AXI_RLAST),
-			// }}}
-			// Formal outputs
-			// {{{
-			.f_axi_awr_nbursts(fm_axi_awr_nbursts),
-			.f_axi_wr_pending(fm_axi_wr_pending),
-			.f_axi_rd_nbursts(fm_axi_rd_nbursts),
-			.f_axi_rd_outstanding(fm_axi_rd_outstanding)
-			//
-			// ...
-			// }}}
-			// }}}
-		);
-
-		////////////////////////////////////////////////////////////////
-		//
-		// Contract: If the downstream has no faults, then we
-		//	shouldn't detect any here.
-		// {{{
-		////////////////////////////////////////////////////////////////
-		//
-		//
-
-		always @(*)
-		if (OPT_SELF_RESET)
-		begin
-			assert(!o_write_fault || !M_AXI_ARESETN);
-		end else
-			assert(!o_write_fault);
-
-		always @(*)
-		if (OPT_SELF_RESET)
-		begin
-			assert(!o_read_fault || !M_AXI_ARESETN);
-		end else
-			assert(!o_read_fault);
-
-		always @(*)
-		if (OPT_SELF_RESET)
-		begin
-			assert(!read_timeout || !M_AXI_ARESETN);
-		end else
-			assert(!read_timeout);
-
-		always @(*)
-		if (OPT_SELF_RESET)
-		begin
-			assert(!write_timeout || !M_AXI_ARESETN);
-		end else
-			assert(!write_timeout);
-
-		always @(*)
-		if (S_AXI_AWREADY)
-			assert(!M_AXI_AWVALID);
-
-		//
-		// ...
-		//
-
-		always @(*)
-		if (M_AXI_ARESETN && f_axi_rd_nbursts > 0)
-			assert(f_axi_rd_nbursts == fm_axi_rd_nbursts
-				+ (M_AXI_ARVALID ? 1 : 0)
-				+ (r_rvalid&&m_rlast ? 1 : 0)
-				+ (S_AXI_RVALID&&S_AXI_RLAST ? 1 : 0));
-
-		always @(*)
-		if (M_AXI_ARESETN && f_axi_rd_outstanding > 0)
-			assert(f_axi_rd_outstanding == fm_axi_rd_outstanding
-				+ (M_AXI_ARVALID ? M_AXI_ARLEN+1 : 0)
-				+ (r_rvalid ? 1 : 0)
-				+ (S_AXI_RVALID ? 1 : 0));
-
-		//
-		// ...
-		//
-		always @(*)
-		if (M_AXI_RVALID)
-			assert(!M_AXI_ARVALID);
-
-		always @(*)
-		if (S_AXI_ARESETN)
-			assert(m_wpending == fm_axi_wr_pending);
-
-		always @(*)
-		if (S_AXI_ARESETN && fm_axi_awr_nbursts > 0)
-		begin
-			assert(fm_axi_awr_nbursts== f_axi_awr_nbursts);
-			assert(fm_axi_awr_nbursts == 1);
-			//
-			// ...
-			//
-		end
-		// }}}
-		////////////////////////////////////////////////////////////////
-		//
-		// Exclusive address checking
-		// {{{
-		////////////////////////////////////////////////////////////////
-		//
-		//
-
-		//
-		//
-		// ...
-		//
-
-		////////////////////////////////////////////////////////////////
-		//
-		// Cover checks
-		// {{{
-		////////////////////////////////////////////////////////////////
-		//
-		//
-
-		// }}}
-		////////////////////////////////////////////////////////////////
-		//
-		// "Careless" assumptions
-		// {{{
-		////////////////////////////////////////////////////////////////
-		//
-		//
-	end endgenerate
-
-	//
-	// ...
-	//
-
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Never path check
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	//
-	(* anyconst *) reg [C_S_AXI_ADDR_WIDTH-1:0]	fc_never_write_addr,
-							fc_never_read_addr;
-	(* anyconst *) reg [C_S_AXI_DATA_WIDTH + C_S_AXI_DATA_WIDTH/8-1:0]
-							fc_never_write_data;
-	(* anyconst *) reg [C_S_AXI_DATA_WIDTH-1:0]	fc_never_read_data;
-
-	// Write address
-	// {{{
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && S_AXI_AWVALID)
-		assume(S_AXI_AWADDR != fc_never_write_addr);
-
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && !o_write_fault && M_AXI_ARESETN && M_AXI_AWVALID)
-		assert(M_AXI_AWADDR != fc_never_write_addr);
-	// }}}
-
-	// Write data
-	// {{{
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && S_AXI_WVALID)
-		assume({ S_AXI_WDATA, S_AXI_WSTRB } != fc_never_write_data);
-
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && !o_write_fault && M_AXI_ARESETN && M_AXI_WVALID)
-	begin
-		if (lock_failed)
-			assert(M_AXI_WSTRB == 0);
-		else
-			assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data);
-	end
-	// }}}
-
-	// Read address
-	// {{{
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && S_AXI_ARVALID)
-		assume(S_AXI_ARADDR != fc_never_read_addr);
-
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && r_arvalid)
-		assume(r_araddr != fc_never_read_addr);
-
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && !o_read_fault && M_AXI_ARESETN && M_AXI_ARVALID)
-		assert(M_AXI_ARADDR != fc_never_read_addr);
-	// }}}
-
-	// Read data
-	// {{{
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && M_AXI_ARESETN && M_AXI_RVALID)
-		assume(M_AXI_RDATA != fc_never_read_data);
-
-	always @(posedge S_AXI_ACLK)
-	if (S_AXI_ARESETN && S_AXI_RVALID && S_AXI_RRESP != SLAVE_ERROR)
-		assert(S_AXI_RDATA != fc_never_read_data);
-	// }}}
-
-	// }}}
-	////////////////////////////////////////////////////////////////////////
-	//
-	// Cover properties
-	// {{{
-	////////////////////////////////////////////////////////////////////////
-	//
-	// We'll use these to determine the best performance this core
-	// can achieve
-	//
-	reg	[4:0]	f_dbl_rd_count, f_dbl_wr_count;
-	reg	[4:0]	f_rd_count, f_wr_count;
-
-	// f_wr_count
-	// {{{
-	initial	f_wr_count = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || o_write_fault)
-		f_wr_count <= 0;
-	else if (S_AXI_BVALID && S_AXI_BREADY)
-	begin
-		if (!(&f_wr_count))
-			f_wr_count <= f_wr_count + 1;
-	end
-	// }}}
-
-	// f_dbl_wr_count
-	// {{{
-	initial	f_dbl_wr_count = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || o_write_fault||(S_AXI_AWVALID && S_AXI_AWLEN < 3))
-		f_dbl_wr_count <= 0;
-	else if (S_AXI_BVALID && S_AXI_BREADY)
-	begin
-		if (!(&f_dbl_wr_count))
-			f_dbl_wr_count <= f_dbl_wr_count + 1;
-	end
-	// }}}
-
-	// f_rd_count
-	// {{{
-	initial	f_rd_count = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || o_read_fault)
-		f_rd_count <= 0;
-	else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST)
-	begin
-		if (!(&f_rd_count))
-			f_rd_count <= f_rd_count + 1;
-	end
-	// }}}
-
-	// f_dbl_rd_count
-	// {{{
-	initial	f_dbl_rd_count = 0;
-	always @(posedge S_AXI_ACLK)
-	if (!S_AXI_ARESETN || o_read_fault||(S_AXI_ARVALID && S_AXI_ARLEN < 3))
-		f_dbl_rd_count <= 0;
-	else if (S_AXI_RVALID && S_AXI_RREADY && S_AXI_RLAST)
-	begin
-		if (!(&f_dbl_rd_count))
-			f_dbl_rd_count <= f_dbl_rd_count + 1;
-	end
-	// }}}
-
-	// Can we complete a single write burst without fault?
-	// {{{
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_wr_count > 1) && (!o_write_fault));
-
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_dbl_wr_count > 1) && (!o_write_fault));
-	// }}}
-
-	// Can we complete four write bursts without fault? (and return to idle)
-	// {{{
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_wr_count > 3) && (!o_write_fault)
-			&&(!S_AXI_AWVALID && !S_AXI_WVALID
-					&& !S_AXI_BVALID)
-			&& (f_axi_awr_nbursts == 0)
-			&& (f_axi_wr_pending == 0));
-
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_dbl_wr_count > 3) && (!o_write_fault)
-			&&(!S_AXI_AWVALID && !S_AXI_WVALID
-					&& !S_AXI_BVALID)
-			&& (f_axi_awr_nbursts == 0)
-			&& (f_axi_wr_pending == 0));
-	// }}}
-
-	// Can we complete a single read burst without fault?
-	// {{{
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_rd_count > 1) && (!o_read_fault));
-
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_dbl_rd_count > 1) && (!o_read_fault));
-	// }}}
-
-	// Can we complete four read bursts without fault?
-	// {{{
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_rd_count > 3) && (f_axi_rd_nbursts == 0)
-			&& !S_AXI_ARVALID && !S_AXI_RVALID);
-
-	always @(*)
-	if (S_AXI_ARESETN)
-		cover((f_dbl_rd_count > 3) && (f_axi_rd_nbursts == 0)
-			&& !S_AXI_ARVALID && !S_AXI_RVALID);
-	// }}}
-`endif
-// }}}
-endmodule
-`ifndef	YOSYS
-`default_nettype wire
-`endif