rtl/wb2axip: add to version control

1 files changed, 2339 insertions, 0 deletions

diff --git a/rtl/wb2axip/axisafety.v b/rtl/wb2axip/axisafety.v
new file mode 100644
index 0000000..ff7e351
--- /dev/null
+++ b/rtl/wb2axip/axisafety.v
@@ -0,0 +1,2339 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// 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