////////////////////////////////////////////////////////////////////////////////
//
// 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.
//
// 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-2020, 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,
	parameter [0:0] OPT_SELF_RESET  = 0,
	//
	// 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	LSB = $clog2(DW)-3;
	localparam	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
	reg	[IW-1:0]	wfifo_id;
	reg			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;
	reg		waddr_valid, raddr_valid;
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// 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_AWREADY && S_AXI_BVALID && S_AXI_BREADY;
	// }}}

	// waddr_valid
	// {{{
	generate if (OPT_SELF_RESET)
	begin
		initial	waddr_valid = 0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN)
			waddr_valid <= 0;
		else if (S_AXI_AWVALID && S_AXI_AWREADY)
			waddr_valid <= 1;
		else if (waddr_valid)
			waddr_valid <= !S_AXI_BVALID || !S_AXI_BREADY;
	end else begin
		always @(*)
			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)
			r_awvalid <= 0;
	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;
		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;
			M_AXI_AWCACHE <= m_awcache;
			M_AXI_AWPROT  <= m_awprot;
			M_AXI_AWQOS   <= m_awqos;
		end

		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.
	//
	always @(posedge S_AXI_ACLK)
	if (S_AXI_AWREADY && S_AXI_AWVALID)
	begin
		// {{{
		wfifo_id   <= S_AXI_AWID;
		wfifo_lock <= S_AXI_AWLOCK;
		// }}}
	end
	// }}}

	// 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;
			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 && !wfifo_lock)
				// An attempt to return the wrong ID
				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
	// {{{
	always @(*)
	if (OPT_SELF_RESET)
		raddr_valid = !rfifo_empty;
	else
		raddr_valid = !S_AXI_ARREADY;
	// }}}

	// 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 <= (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;
	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;
		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;
			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 apart from a
				// request.
				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 && !rfifo_lock)
				// An attempt to return the wrong ID
				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
	// {{{

	// 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 @(posedge S_AXI_ACLK)
	if (S_AXI_ARVALID && S_AXI_ARREADY)
	begin
		rfifo_id   <= S_AXI_ARID;
		rfifo_lock <= S_AXI_ARLOCK;
	end
	// }}}

	// 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
	// }}}

	// 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
		// {{{
		// Declarations
		// {{{
		reg	[4:0]	reset_counter;
		reg		reset_timeout, r_clear_fault;
		// }}}

		// 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;
		// }}}

		always @(*)
			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)
			clear_fault = 0;
		else if (raddr_valid || waddr_valid)
			clear_fault = 0;
		else
			clear_fault = r_clear_fault;
		// }}}

		// }}}
	end else begin
		// {{{
		always @(*)
			M_AXI_ARESETN = S_AXI_ARESETN;
		always @(*)
			clear_fault = 0;
		// }}}
	end endgenerate
	// }}}

	// Make Verilator happy
	// {{{
	// Verilator lint_off UNUSED
	wire	unused;
	assign	unused = &{ 1'b0 };
	// Verilator lint_on  UNUSED
	// }}}
// Add user logic here
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
// 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
		//
		// Write Data
		.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),
	//
	//
		// Response ID tag. This signal is the ID tag of the
		// write response.
		.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_rid(S_AXI_RID),
		.i_axi_rdata(S_AXI_RDATA),
		.i_axi_rresp(S_AXI_RRESP),
		.i_axi_rlast(S_AXI_RLAST),
		.i_axi_rvalid(S_AXI_RVALID),
		// Read ready. This signal indicates that the master can
		// accept the read data and response information.
		.i_axi_rready(S_AXI_RREADY),
		//
		// Formal outputs
		//
		.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)
			assert(1 || S_AXI_AWREADY || !M_AXI_ARESETN || !S_AXI_ARESETN);
		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))
		assert(S_AXI_AWREADY == !OPT_SELF_RESET);
	else if (f_axi_wr_pending > 0)
		assert(!S_AXI_AWREADY);
	else if (s_wbursts)
		assert(!S_AXI_AWREADY);
	else if (!OPT_SELF_RESET)
		assert(S_AXI_AWREADY);
	else if (!o_write_fault && !o_read_fault)
		assert(S_AXI_AWREADY || OPT_SELF_RESET);

	always @(*)
	if (f_axi_wr_pending > 0)
		assert(s_wbursts == 0);
	else if (f_axi_awr_nbursts > 0)
		assert(s_wbursts == f_axi_awr_nbursts);
	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)
		assert(waddr_valid);
	else if (f_axi_wr_pending > 0)
	begin
		if (!o_write_fault)
			assert(M_AXI_WVALID && r_wvalid);
	end

	always @(*)
	if (!OPT_SELF_RESET)
		assert(waddr_valid == !S_AXI_AWREADY);
	else begin
		// ...
		assert(waddr_valid == (f_axi_awr_nbursts > 0));
	end

	always @(*)
	if (S_AXI_ARESETN && !o_write_fault && f_axi_wr_pending && !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)
			assert(f_axi_wr_pending + (M_AXI_WVALID ? 1:0) + (r_wvalid ? 1:0) == m_wpending);
		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)
		assert(waddr_valid == !S_AXI_AWREADY);
	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)
		assert(rfifo_id == f_axi_rd_checkid);
	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)
		assert(raddr_valid == !S_AXI_ARREADY);
	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
	// }}}


	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	// Cover properties
	//
	////////////////////////////////////////////////////////////////////////
	//
	// }}}

	////////////////////////////////////////////////////////////////////////
	//
	// Good interface check
	//
	////////////////////////////////////////////////////////////////////////
	//
	//
	generate if (F_OPT_FAULTLESS)
	begin
		//
		// ...
		//

		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
		//
		// Write Data
		.i_axi_wdata(M_AXI_WDATA),
		.i_axi_wstrb(M_AXI_WSTRB),
		.i_axi_wlast(M_AXI_WLAST),
		.i_axi_wvalid(M_AXI_WVALID),
		.i_axi_wready(M_AXI_WREADY),
	//
	//
		// Response ID tag. This signal is the ID tag of the
		// write response.
		.i_axi_bid(M_AXI_BID),
		.i_axi_bresp(M_AXI_BRESP),
		.i_axi_bvalid(M_AXI_BVALID),
		.i_axi_bready(M_AXI_BREADY),
	//
	//
		//
		// 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_rid(M_AXI_RID),
		.i_axi_rdata(M_AXI_RDATA),
		.i_axi_rresp(M_AXI_RRESP),
		.i_axi_rlast(M_AXI_RLAST),
		.i_axi_rvalid(M_AXI_RVALID),
		.i_axi_rready(M_AXI_RREADY),
		//
		// 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)
		//
		// ...
		//
		// }}}
		);

		// {{{
		always @(*)
		if (OPT_SELF_RESET)
			assert(!o_write_fault || !M_AXI_ARESETN);
		else
			assert(!o_write_fault);

		always @(*)
		if (OPT_SELF_RESET)
			assert(!o_read_fault || !M_AXI_ARESETN);
		else
			assert(!o_read_fault);

		always @(*)
		if (OPT_SELF_RESET)
			assert(!read_timeout || !M_AXI_ARESETN);
		else
			assert(!read_timeout);

		always @(*)
		if (OPT_SELF_RESET)
			assert(!write_timeout || !M_AXI_ARESETN);
		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

		//
		// ...
		//

	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)
		assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data);
	// }}}

	// 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;

	initial	f_dbl_wr_count = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || o_write_fault)
		f_dbl_wr_count = 0;
	else if (S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN == 3)
	begin
		if (!(&f_dbl_wr_count))
			f_dbl_wr_count <= f_dbl_wr_count + 1;
	end

	always @(*)
		cover(!S_AXI_ARESETN && (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));

	always @(*)
		cover(!S_AXI_ARESETN && (f_dbl_wr_count > 1)
			&& (!o_write_fault)
			);

	always @(*)
		cover(S_AXI_AWVALID && S_AXI_AWREADY);

	always @(*)
		cover(S_AXI_AWVALID && S_AXI_AWREADY && S_AXI_AWLEN == 3);

	initial	f_dbl_rd_count = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || o_read_fault)
		f_dbl_rd_count = 0;
	else if (S_AXI_ARVALID && S_AXI_ARREADY && S_AXI_ARLEN == 3)
	begin
		if (!(&f_dbl_rd_count))
			f_dbl_rd_count <= f_dbl_rd_count + 1;
	end

	always @(*)
		cover(!S_AXI_ARESETN && (f_dbl_rd_count > 3)
			&& (f_axi_rd_nbursts == 0)
			&& !S_AXI_ARVALID && !S_AXI_RVALID);
	// }}}
`endif
// }}}
endmodule
`ifndef	YOSYS
`default_nettype wire
`endif