////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	axilsafety.v
// {{{
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	A AXI-Lite bus fault isolator.  This core will isolate any
//		downstream AXI-liite slave faults from the upstream channel.
//	It sits as a bump in the wire between upstream and downstream channels,
//	and so it will consume two clocks--slowing down the slave, but
//	potentially allowing developer to recover in case of a fault.
//
//	This core is configured by a couple parameters, which are key to its
//	functionality.
//
//	OPT_TIMEOUT	Set this to a number to be roughly the longest time
//		period you expect the slave to stall the bus, or likewise
//		the longest time period you expect it to wait for a response.
//		If the slave takes longer for either task, a fault will be
//		detected and reported.
//
//	OPT_SELF_RESET	If set, this will send a reset signal to the downstream
//		core so that you can attempt to restart it without reloading
//		the FPGA.  If set, the o_reset signal will be used to reset
//		the downstream core.
//
//	A second key feature of this core are the outgoing fault indicators,
//	o_write_fault and o_read_fault.  If either signal is ever raised, the
//	slave has (somehow) violated protocol on either the write or the
//	read channels respectively.  Such a violation may (or may not) return an
//	error upstream.  For example, if the slave returns a response
//	following no requests from the master, then no error will be returned
//	up stream (doing so would be a protocol violation), but a fault will
//	still be detected.  Use this line to trigger any internal logic
//	analyzers.
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
// }}}
// Copyright (C) 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 axilsafety #(
	// {{{
	parameter	C_AXI_ADDR_WIDTH = 28,
	parameter	C_AXI_DATA_WIDTH = 32,
	parameter	OPT_TIMEOUT = 12,
	parameter	MAX_DEPTH = (OPT_TIMEOUT),
	localparam	AW = C_AXI_ADDR_WIDTH,
	localparam	DW = C_AXI_DATA_WIDTH,
	localparam	LGTIMEOUT = $clog2(OPT_TIMEOUT+1),
	localparam	LGDEPTH   = $clog2(MAX_DEPTH+1),
	parameter [0:0]	OPT_SELF_RESET = 1'b1,
	parameter 	OPT_MIN_RESET = 16
`ifdef	FORMAL
	, parameter [0:0] F_OPT_WRITES = 1'b1,
	parameter [0:0] F_OPT_READS  = 1'b1,
	parameter [0:0]	F_OPT_FAULTLESS = 1'b1
`endif
	// }}}
	) (
		// {{{
		output	reg	o_write_fault,
		output	reg	o_read_fault,
		//
		input	wire			S_AXI_ACLK,
		input	wire			S_AXI_ARESETN,
		output	reg			M_AXI_ARESETN,
		//
		input	wire			S_AXI_AWVALID,
		output	reg			S_AXI_AWREADY,
		input	wire	[AW-1:0]	S_AXI_AWADDR,
		input	wire	[2:0]		S_AXI_AWPROT,
		//
		input	wire			S_AXI_WVALID,
		output	reg			S_AXI_WREADY,
		input	wire	[DW-1:0]	S_AXI_WDATA,
		input	wire	[DW/8-1:0]	S_AXI_WSTRB,
		//
		output	reg			S_AXI_BVALID,
		input	wire			S_AXI_BREADY,
		output	reg	[1:0]		S_AXI_BRESP,
		//
		input	wire			S_AXI_ARVALID,
		output	reg			S_AXI_ARREADY,
		input	wire	[AW-1:0]	S_AXI_ARADDR,
		input	wire	[2:0]		S_AXI_ARPROT,
		//
		output	reg			S_AXI_RVALID,
		input	wire			S_AXI_RREADY,
		output	reg	[DW-1:0]	S_AXI_RDATA,
		output	reg	[1:0]		S_AXI_RRESP,
		//
		//
		//
		output	reg			M_AXI_AWVALID,
		input	wire			M_AXI_AWREADY,
		output	reg	[AW-1:0]	M_AXI_AWADDR,
		output	reg	[2:0]		M_AXI_AWPROT,
		//
		output	reg			M_AXI_WVALID,
		input	wire			M_AXI_WREADY,
		output	reg	[DW-1:0]	M_AXI_WDATA,
		output	reg	[DW/8-1:0]	M_AXI_WSTRB,
		//
		input	wire			M_AXI_BVALID,
		output	wire			M_AXI_BREADY,
		input	wire	[1:0]		M_AXI_BRESP,
		//
		output	reg			M_AXI_ARVALID,
		input	wire			M_AXI_ARREADY,
		output	reg	[AW-1:0]	M_AXI_ARADDR,
		output	reg	[2:0]		M_AXI_ARPROT,
		//
		input	wire			M_AXI_RVALID,
		output	reg			M_AXI_RREADY,
		input	wire	[DW-1:0]	M_AXI_RDATA,
		input	wire	[1:0]		M_AXI_RRESP
		// }}}
	);

	// localparam, wire, and register declarations
	// {{{
	localparam	OPT_LOWPOWER = 1'b0;
	localparam	OKAY = 2'b00,
			EXOKAY = 2'b01,
			SLVERR = 2'b10;

	reg	[LGDEPTH-1:0]	aw_count, w_count, r_count;
	reg			aw_zero, w_zero, r_zero,
				aw_full, w_full, r_full,
				aw_w_greater, w_aw_greater;
	reg	[LGDEPTH-1:0]	downstream_aw_count, downstream_w_count, downstream_r_count;
	reg			downstream_aw_zero, downstream_w_zero, downstream_r_zero;
				// downstream_aw_w_greater, downstream_w_aw_greater;

	wire			awskd_valid;
	wire	[2:0]		awskd_prot;
	wire	[AW-1:0]	awskd_addr;
	reg			awskd_ready;

	wire			wskd_valid;
	wire	[DW-1:0]	wskd_data;
	wire	[DW/8-1:0]	wskd_strb;
	reg			wskd_ready;

	wire			bskd_valid;
	wire	[1:0]		bskd_resp;
	reg			bskd_ready;

	reg			last_bvalid;
	reg	[1:0]		last_bdata;
	reg			last_bchanged;

	wire			arskd_valid;
	wire	[2:0]		arskd_prot;
	wire	[AW-1:0]	arskd_addr;
	reg			arskd_ready;

	reg			last_rvalid;
	reg [DW+1:0]		last_rdata;
	reg			last_rchanged;

	wire			rskd_valid;
	wire	[1:0]		rskd_resp;
	wire	[DW-1:0]	rskd_data;
	reg			rskd_ready;

	reg [LGTIMEOUT-1:0]	aw_stall_counter, w_stall_counter,
				r_stall_counter, w_ack_timer, r_ack_timer;
	reg 			aw_stall_limit, w_stall_limit, r_stall_limit,
				w_ack_limit, r_ack_limit;
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Write signaling
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	//
	// Write address channel
	// {{{

	skidbuffer #(.DW(AW+3)
		// {{{
`ifdef	FORMAL
		, .OPT_PASSTHROUGH(1'b1)
`endif
		// }}}
	) awskd(S_AXI_ACLK, !S_AXI_ARESETN,
		// {{{
		S_AXI_AWVALID, S_AXI_AWREADY, { S_AXI_AWPROT, S_AXI_AWADDR },
		awskd_valid, awskd_ready, { awskd_prot, awskd_addr});
		// }}}

	// awskd_ready
	// {{{
	// awskd_ready is the critical piece here, since it determines when
	// we accept a packet from the skid buffer.
	//
	always @(*)
	if (!M_AXI_ARESETN || o_write_fault)
		// On any fault, we'll always accept a request (and return an
		// error).  We always accept a value if there are already
		// more writes than write addresses accepted.
		awskd_ready = (w_aw_greater)
			||((aw_zero)&&(!S_AXI_BVALID || S_AXI_BREADY));
	else
		// Otherwise, we accept if ever our counters aren't about to
		// overflow, and there's a place downstream to accept it
		awskd_ready = (!M_AXI_AWVALID || M_AXI_AWREADY)&& (!aw_full);
	// }}}

	// M_AXI_AWVALID
	// {{{
	initial	M_AXI_AWVALID = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN)
		M_AXI_AWVALID <= 1'b0;
	else if (!M_AXI_AWVALID || M_AXI_AWREADY)
		M_AXI_AWVALID <= awskd_valid && awskd_ready && !o_write_fault;
	// }}}

	// M_AXI_AWADDR, M_AXI_AWPROT
	// {{{
	always @(posedge S_AXI_ACLK)
	if (OPT_LOWPOWER && (!M_AXI_ARESETN || o_write_fault))
	begin
		M_AXI_AWADDR <= 0;
		M_AXI_AWPROT <= 0;
	end else if (!M_AXI_AWVALID || M_AXI_AWREADY)
	begin
		M_AXI_AWADDR <= awskd_addr;
		M_AXI_AWPROT <= awskd_prot;
	end
	// }}}
	// }}}

	//
	// Write data channel
	// {{{

	skidbuffer #(.DW(DW+DW/8)
		// {{{
`ifdef	FORMAL
		, .OPT_PASSTHROUGH(1'b1)
`endif
		// }}}
	) wskd(S_AXI_ACLK, !S_AXI_ARESETN,
		// {{{
		S_AXI_WVALID, S_AXI_WREADY, { S_AXI_WDATA, S_AXI_WSTRB },
		wskd_valid, wskd_ready, { wskd_data, wskd_strb});
		// }}}

	// wskd_ready
	// {{{
	// As with awskd_ready, this logic is the critical key.
	//
	always @(*)
	if (!M_AXI_ARESETN || o_write_fault)
		wskd_ready = (aw_w_greater)
			|| ((w_zero)&&(!S_AXI_BVALID || S_AXI_BREADY));
	else
		wskd_ready = (!M_AXI_WVALID || M_AXI_WREADY) && (!w_full);
	// }}}

	// M_AXI_WVALID
	// {{{
	initial	M_AXI_WVALID = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN)
		M_AXI_WVALID <= 1'b0;
	else if (!M_AXI_WVALID || M_AXI_WREADY)
		M_AXI_WVALID <= wskd_valid && wskd_ready && !o_write_fault;
	// }}}

	// M_AXI_WDATA, M_AXI_WSTRB
	// {{{
	always @(posedge S_AXI_ACLK)
	if (OPT_LOWPOWER && (!M_AXI_ARESETN || o_write_fault))
	begin
		M_AXI_WDATA <= 0;
		M_AXI_WSTRB <= 0;
	end else if (!M_AXI_WVALID || M_AXI_WREADY)
	begin
		M_AXI_WDATA <= wskd_data;
		M_AXI_WSTRB <= (o_write_fault) ? 0 : wskd_strb;
	end
	// }}}
	// }}}

	//
	// Write return channel
	// {{{

	// bskd_valid, M_AXI_BREADY, bskd_resp
	// {{{
`ifdef	FORMAL
	assign	bskd_valid = M_AXI_BVALID;
	assign	M_AXI_BREADY= bskd_ready;
	assign	bskd_resp  = M_AXI_BRESP;
`else
	skidbuffer #(.DW(2)
	) bskd(S_AXI_ACLK, !S_AXI_ARESETN || !M_AXI_ARESETN,
		M_AXI_BVALID, M_AXI_BREADY, M_AXI_BRESP,
		bskd_valid, bskd_ready,  bskd_resp);
`endif
	// }}}

	// bskd_ready
	// {{{
	always @(*)
	if (o_write_fault)
		bskd_ready = 1'b1;
	else
		bskd_ready = (!S_AXI_BVALID || S_AXI_BREADY);
	// }}}

	// S_AXI_BVALID
	// {{{
	initial	S_AXI_BVALID = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		S_AXI_BVALID <= 1'b0;
	else if (!S_AXI_BVALID || S_AXI_BREADY)
	begin
		if (o_write_fault || !M_AXI_ARESETN)
			S_AXI_BVALID <= (!S_AXI_BVALID&&(!aw_zero)&&(!w_zero));
		else
			S_AXI_BVALID <= (!downstream_aw_zero)
				&&(!downstream_w_zero)&&(bskd_valid);
	end
	// }}}

	// last_bvalid
	// {{{
	initial	last_bvalid = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!M_AXI_ARESETN || o_write_fault)
		last_bvalid <= 1'b0;
	else
		last_bvalid <= (M_AXI_BVALID && !M_AXI_BREADY);
	// }}}

	// last_bdata
	// {{{
	always @(posedge S_AXI_ACLK)
	if (M_AXI_BVALID)
		last_bdata <= M_AXI_BRESP;
	// }}}

	// last_bchanged
	// {{{
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault)
		last_bchanged <= 1'b0;
	else
		last_bchanged <= (last_bvalid && (!M_AXI_BVALID
					|| last_bdata != M_AXI_BRESP));
	// }}}

	// S_AXI_BRESP
	// {{{
	initial	S_AXI_BRESP = OKAY;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_BVALID || S_AXI_BREADY)
	begin
		if (o_write_fault)
			S_AXI_BRESP <= SLVERR;
		else if (bskd_resp == EXOKAY)
			S_AXI_BRESP <= SLVERR;
		else
			S_AXI_BRESP <= bskd_resp;
	end
	// }}}
	// }}}
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Read signaling
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	//
	// Read address channel
	// {{{

	skidbuffer #(.DW(AW+3)
		// {{{
`ifdef	FORMAL
		, .OPT_PASSTHROUGH(1'b1)
`endif
		// }}}
	) arskd(S_AXI_ACLK, !S_AXI_ARESETN,
		// {{{
		S_AXI_ARVALID, S_AXI_ARREADY, { S_AXI_ARPROT, S_AXI_ARADDR },
		arskd_valid, arskd_ready,  { arskd_prot, arskd_addr });
		// }}}

	// arskd_ready
	// {{{
	always @(*)
	if (!M_AXI_ARESETN || o_read_fault)
		arskd_ready =((r_zero)&&(!S_AXI_RVALID || S_AXI_RREADY));
	else
		arskd_ready = (!M_AXI_ARVALID || M_AXI_ARREADY) && (!r_full);
	// }}}

	// M_AXI_ARVALID
	// {{{
	initial	M_AXI_ARVALID = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN)
		M_AXI_ARVALID <= 1'b0;
	else if (!M_AXI_ARVALID || M_AXI_ARREADY)
		M_AXI_ARVALID <= arskd_valid && arskd_ready && !o_read_fault;
	// }}}

	// M_AXI_ARADDR, M_AXI_ARPROT
	// {{{
	always @(posedge S_AXI_ACLK)
	if (OPT_LOWPOWER && (!M_AXI_ARESETN || o_read_fault))
	begin
		M_AXI_ARADDR <= 0;
		M_AXI_ARPROT <= 0;
	end else if (!M_AXI_ARVALID || M_AXI_ARREADY)
	begin
		M_AXI_ARADDR <= arskd_addr;
		M_AXI_ARPROT <= arskd_prot;
	end
	// }}}
	// }}}

	//
	// Read data channel
	// {{{

	// rskd_valid, rskd_resp, rskd_data skid buffer
	// {{{
`ifdef	FORMAL
	assign	rskd_valid = M_AXI_RVALID;
	assign	M_AXI_RREADY = rskd_ready;
	assign	{ rskd_resp, rskd_data } = { M_AXI_RRESP, M_AXI_RDATA };
`else
	skidbuffer #(.DW(DW+2)
	) rskd(S_AXI_ACLK, !S_AXI_ARESETN || !M_AXI_ARESETN,
		M_AXI_RVALID, M_AXI_RREADY, { M_AXI_RRESP, M_AXI_RDATA },
		rskd_valid, rskd_ready,  { rskd_resp, rskd_data });
`endif
	// ?}}}

	// rskd_ready
	// {{{
	always @(*)
	if (o_read_fault)
		rskd_ready = 1;
	else
		rskd_ready = (!S_AXI_RVALID || S_AXI_RREADY);
	// }}}

	// S_AXI_RVALID
	// {{{
	initial	S_AXI_RVALID = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		S_AXI_RVALID <= 1'b0;
	else if (!S_AXI_RVALID || S_AXI_RREADY)
	begin
		if (o_read_fault || !M_AXI_ARESETN)
			S_AXI_RVALID <= (!S_AXI_RVALID && !r_zero)
					|| (arskd_valid && arskd_ready);
		else
			S_AXI_RVALID <= (!downstream_r_zero)&&(rskd_valid);
	end
	// }}}

	// S_AXI_RDATA, S_AXI_RRESP
	// {{{
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_RVALID || S_AXI_RREADY)
	begin
		if (o_read_fault || !M_AXI_ARESETN)
			S_AXI_RDATA <= 0;
		else
			S_AXI_RDATA <= rskd_data;

		S_AXI_RRESP <= OKAY;
		if (o_read_fault || rskd_resp == EXOKAY)
			S_AXI_RRESP <= SLVERR;
		else if (!downstream_r_zero)
			S_AXI_RRESP <= rskd_resp;
	end
	// }}}

	// last_rvalid
	// {{{
	initial	last_rvalid = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault)
		last_rvalid <= 1'b0;
	else
		last_rvalid <= (M_AXI_RVALID && !M_AXI_RREADY);
	// }}}

	// last_rdata
	// {{{
	always @(posedge S_AXI_ACLK)
	if (M_AXI_RVALID)
		last_rdata <= { M_AXI_RRESP, M_AXI_RDATA };
	// }}}

	// last_rchanged
	// {{{
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault)
		last_rchanged <= 1'b0;
	else
		last_rchanged <= (last_rvalid && (!M_AXI_RVALID
			|| last_rdata != { M_AXI_RRESP, M_AXI_RDATA }));
	// }}}
	// }}}
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Usage counters
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	//
	// Write address channel
	// {{{

	initial	aw_count = 0;
	initial	aw_zero  = 1;
	initial	aw_full  = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	begin
		aw_count <= 0;
		aw_zero  <= 1;
		aw_full  <= 0;
	end else case({(awskd_valid && awskd_ready),S_AXI_BVALID&&S_AXI_BREADY})
	2'b10: begin
		aw_count <= aw_count + 1;
		aw_zero <= 0;
		aw_full <= (aw_count == { {(LGDEPTH-1){1'b1}}, 1'b0 });
		end
	2'b01: begin
		aw_count <= aw_count - 1;
		aw_zero <= (aw_count <= 1);
		aw_full <= 0;
		end
	default: begin end
	endcase
	// }}}

	//
	// Write data channel
	// {{{
	initial	w_count = 0;
	initial	w_zero  = 1;
	initial	w_full  = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	begin
		w_count <= 0;
		w_zero  <= 1;
		w_full  <= 0;
	end else case({(wskd_valid && wskd_ready), S_AXI_BVALID&& S_AXI_BREADY})
	2'b10: begin
		w_count <= w_count + 1;
		w_zero <= 0;
		w_full <= (w_count == { {(LGDEPTH-1){1'b1}}, 1'b0 });
		end
	2'b01: begin
		w_count <= w_count - 1;
		w_zero <= (w_count <= 1);
		w_full <= 1'b0;
		end
	default: begin end
	endcase
	// }}}

	// aw_w_greater, w_aw_greater
	// {{{
	initial	aw_w_greater = 0;
	initial	w_aw_greater = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	begin
		aw_w_greater <= 0;
		w_aw_greater <= 0;
	end else case({(awskd_valid && awskd_ready),
			(wskd_valid && wskd_ready)})
	2'b10: begin
		aw_w_greater <= (aw_count + 1 >  w_count);
		w_aw_greater <= ( w_count     > aw_count + 1);
		end
	2'b01: begin
		aw_w_greater <= (aw_count     >  w_count + 1);
		w_aw_greater <= ( w_count + 1 > aw_count);
		end
	default: begin end
	endcase
	// }}}
	//
	// Read channel
	// {{{

	// r_count, r_zero, r_full
	initial	r_count = 0;
	initial	r_zero  = 1;
	initial	r_full  = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
	begin
		r_count <= 0;
		r_zero  <= 1;
		r_full  <= 0;
	end else case({(arskd_valid&&arskd_ready), S_AXI_RVALID&&S_AXI_RREADY})
	2'b10: begin
		r_count <= r_count + 1;
		r_zero <= 0;
		r_full <= (r_count == { {(LGDEPTH-1){1'b1}}, 1'b0 });
		end
	2'b01: begin
		r_count <= r_count - 1;
		r_zero <= (r_count <= 1);
		r_full <= 0;
		end
	default: begin end
	endcase
	// }}}

	//
	// Downstream write address channel
	// {{{

	initial	downstream_aw_count = 0;
	initial	downstream_aw_zero = 1;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault)
	begin
		downstream_aw_count <= 0;
		downstream_aw_zero <= 1;
	end else case({(M_AXI_AWVALID && M_AXI_AWREADY), M_AXI_BVALID && M_AXI_BREADY})
	2'b10: begin
		downstream_aw_count <= downstream_aw_count + 1;
		downstream_aw_zero <= 0;
		end
	2'b01: begin
		downstream_aw_count <= downstream_aw_count - 1;
		downstream_aw_zero <= (downstream_aw_count <= 1);
		end
	default: begin end
	endcase
	// }}}

	//
	// Downstream write data channel
	// {{{
	initial	downstream_w_count = 0;
	initial	downstream_w_zero  = 1;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault)
	begin
		downstream_w_count <= 0;
		downstream_w_zero  <= 1;
	end else case({(M_AXI_WVALID && M_AXI_WREADY), M_AXI_BVALID && M_AXI_BREADY})
	2'b10: begin
		downstream_w_count <= downstream_w_count + 1;
		downstream_w_zero <= 0;
		end
	2'b01: begin
		downstream_w_count <= downstream_w_count - 1;
		downstream_w_zero <= (downstream_w_count <= 1);
		end
	default: begin end
	endcase
	// }}}

	//
	// Downstream read channel
	// {{{

	initial	downstream_r_count = 0;
	initial	downstream_r_zero  = 1;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault)
	begin
		downstream_r_count <= 0;
		downstream_r_zero  <= 1;
	end else case({M_AXI_ARVALID && M_AXI_ARREADY, M_AXI_RVALID && M_AXI_RREADY})
	2'b10: begin
		downstream_r_count <= downstream_r_count + 1;
		downstream_r_zero  <= 0;
		end
	2'b01: begin
		downstream_r_count <= downstream_r_count - 1;
		downstream_r_zero  <= (downstream_r_count <= 1);
		end
	default: begin end
	endcase
	// }}}
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Timeout checking
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	// The key piece here is that we define the timeout depending upon
	// what happens (or doesn't happen) *DOWNSTREAM*.  These timeouts
	// will need to propagate upstream before taking place.

	//
	// Write address stall counter
	// {{{
	initial	aw_stall_counter = 0;
	initial	aw_stall_limit   = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || o_write_fault || !M_AXI_ARESETN)
	begin
		aw_stall_counter <= 0;
		aw_stall_limit   <= 0;
	end else if (!M_AXI_AWVALID || M_AXI_AWREADY || M_AXI_BVALID)
	begin
		aw_stall_counter <= 0;
		aw_stall_limit   <= 0;
	end else if (aw_w_greater && !M_AXI_WVALID)
	begin
		aw_stall_counter <= 0;
		aw_stall_limit   <= 0;
	end else // if (!S_AXI_BVALID || S_AXI_BREADY)
	begin
		aw_stall_counter <= aw_stall_counter + 1;
		aw_stall_limit   <= (aw_stall_counter+1 >= OPT_TIMEOUT);
	end
	// }}}

	//
	// Write data stall counter
	// {{{
	initial	w_stall_counter = 0;
	initial	w_stall_limit   = 1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault)
	begin
		w_stall_counter <= 0;
		w_stall_limit   <= 0;
	end else if (!M_AXI_WVALID || M_AXI_WREADY || M_AXI_BVALID)
	begin
		w_stall_counter <= 0;
		w_stall_limit   <= 0;
	end else if (w_aw_greater && !M_AXI_AWVALID)
	begin
		w_stall_counter <= 0;
		w_stall_limit   <= 0;
	end else // if (!M_AXI_BVALID || M_AXI_BREADY)
	begin
		w_stall_counter <= w_stall_counter + 1;
		w_stall_limit   <= (w_stall_counter + 1 >= OPT_TIMEOUT);
	end
	// }}}

	//
	// Write acknowledgment delay counter
	// {{{
	initial w_ack_timer = 0;
	initial	w_ack_limit = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault)
	begin
		w_ack_timer <= 0;
		w_ack_limit <= 0;
	end else if (M_AXI_BVALID || downstream_aw_zero || downstream_w_zero)
	begin
		w_ack_timer <= 0;
		w_ack_limit <= 0;
	end else
	begin
		w_ack_timer <= w_ack_timer + 1;
		w_ack_limit <= (w_ack_timer + 1 >= OPT_TIMEOUT);
	end
	// }}}

	//
	// Read request stall counter
	// {{{
	initial r_stall_counter = 0;
	initial	r_stall_limit   = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault)
	begin
		r_stall_counter <= 0;
		r_stall_limit   <= 0;
	end else if (!M_AXI_ARVALID || M_AXI_ARREADY || M_AXI_RVALID)
	begin
		r_stall_counter <= 0;
		r_stall_limit   <= 0;
	end else begin
		r_stall_counter <= r_stall_counter + 1;
		r_stall_limit   <= (r_stall_counter + 1 >= OPT_TIMEOUT);
	end
	// }}}

	//
	// Read acknowledgement delay counter
	// {{{
	initial r_ack_timer = 0;
	initial	r_ack_limit = 0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault)
	begin
		r_ack_timer <= 0;
		r_ack_limit <= 0;
	end else if (M_AXI_RVALID || downstream_r_zero)
	begin
		r_ack_timer <= 0;
		r_ack_limit <= 0;
	end else begin
		r_ack_timer <= r_ack_timer + 1;
		r_ack_limit <= (r_ack_timer + 1 >= OPT_TIMEOUT);
	end
	// }}}
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Fault detection
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	//
	// Determine if a write fault has taken place
	// {{{
	initial	o_write_fault =1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		o_write_fault <= 1'b0;
	else if (OPT_SELF_RESET && o_write_fault)
	begin
		//
		// Clear any fault on reset
		if (!M_AXI_ARESETN)
			o_write_fault <= 1'b0;
	end else begin
		//
		// A write fault takes place if you respond without a prior
		// bus request on both write address and write data channels.
		if ((downstream_aw_zero || downstream_w_zero)&&(bskd_valid))
			o_write_fault <= 1'b1;

		// AXI-lite slaves are not allowed to return EXOKAY responses
		// from the bus
		if (bskd_valid && bskd_resp == EXOKAY)
			o_write_fault <= 1'b1;

		// If the downstream core refuses to accept either a
		// write address request, or a write data request, or for that
		// matter if it doesn't return an acknowledgment in a timely
		// fashion, then a fault has been detected.
		if (aw_stall_limit || w_stall_limit || w_ack_limit)
			o_write_fault <= 1'b1;

		// If the downstream core changes BRESP while VALID && !READY,
		// then it isn't stalling the channel properly--that's a fault.
		if (last_bchanged)
			o_write_fault <= 1'b1;
	end
	// }}}

	// o_read_fault
	// {{{
	initial	o_read_fault =1'b0;
	always @(posedge S_AXI_ACLK)
	if (!S_AXI_ARESETN)
		o_read_fault <= 1'b0;
	else if (OPT_SELF_RESET && o_read_fault)
	begin
		//
		// Clear any fault on reset
		if (!M_AXI_ARESETN)
			o_read_fault <= 1'b0;
	end else begin
		// Responding without a prior request is a fault.  Can only
		// respond after a request has been made.
		if (downstream_r_zero && rskd_valid)
			o_read_fault <= 1'b1;

		// AXI-lite slaves are not allowed to return EXOKAY.  This is
		// an error.
		if (rskd_valid && rskd_resp == EXOKAY)
			o_read_fault <= 1'b1;

		// The slave cannot stall the bus forever, nor should the
		// master wait forever for a response from the slave.
		if (r_stall_limit || r_ack_limit)
			o_read_fault <= 1'b1;

		// If the slave changes the data, or the RRESP on the wire,
		// while the incoming bus is stalled, then that's also a fault.
		if (last_rchanged)
			o_read_fault <= 1'b1;
	end
	// }}}
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Self reset handling
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//

	generate if (OPT_SELF_RESET)
	begin : SELF_RESET_GENERATION
		// {{{
		reg		min_reset;

		if (OPT_MIN_RESET > 1)
		begin : MIN_RESET
			// {{{
			reg	[$clog2(OPT_MIN_RESET+1):0]	reset_counter;

			//
			// Optionally insist that any downstream reset have a
			// minimum duration.  Many Xilinx components require
			// a 16-clock reset.  This ensures such reset
			// requirements are achieved.
			//

			initial reset_counter = OPT_MIN_RESET-1;
			initial	min_reset = 1'b0;
			always @(posedge S_AXI_ARESETN)
			if (M_AXI_ARESETN)
			begin
				reset_counter <= OPT_MIN_RESET-1;
				min_reset <= 1'b0;
			end else if (!M_AXI_ARESETN)
			begin
				if (reset_counter > 0)
					reset_counter <= reset_counter-1;
				min_reset <= (reset_counter <= 1);
			end

`ifdef	FORMAL
			always @(*)
				assert(reset_counter < OPT_MIN_RESET);
			always @(*)
				assert(min_reset == (reset_counter == 0));
`endif
			// }}}
		end else begin
			// {{{
			always @(*)
				min_reset = 1'b1;
			// }}}
		end

		// M_AXI_ARESETN
		// {{{
		// Reset the downstream bus on either a write or a read fault.
		// Once the bus returns to idle, and any minimum reset durations
		// have been achieved, then release the downstream from reset.
		//
		initial	M_AXI_ARESETN = 1'b0;
		always @(posedge S_AXI_ACLK)
		if (!S_AXI_ARESETN)
			M_AXI_ARESETN <= 1'b0;
		else if (o_write_fault || o_read_fault)
			M_AXI_ARESETN <= 1'b0;
		else if (aw_zero && w_zero && r_zero && min_reset
			&& !awskd_valid && !wskd_valid && !arskd_valid)
			M_AXI_ARESETN <= 1'b1;
		// }}}
		// }}}
	end else begin : SAME_RESET
		// {{{
		//
		// The downstream reset equals the upstream reset
		//
		always @(*)
			M_AXI_ARESETN = S_AXI_ARESETN;
		// }}}
	end endgenerate
	// }}}
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
// Formal property section
// {{{
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
`ifdef	FORMAL
	// {{{
	//
	// The following proof comes in several parts.
	//
	// 1. PROVE that the upstream properties will hold independent of
	//	what the downstream slave ever does.
	//
	// 2. PROVE that if the downstream slave follows protocol, then
	//	neither o_write_fault nor o_read_fault will never get raised.
	//
	// We then repeat these proofs again with both OPT_SELF_RESET set and
	// clear.  Which of the four proofs is accomplished is dependent upon
	// parameters set by the formal engine.
	//
	//
	wire	[LGDEPTH:0]	faxils_awr_outstanding, faxils_wr_outstanding,
				faxils_rd_outstanding;

	reg	f_past_valid;
	initial	f_past_valid = 0;
	always @(posedge S_AXI_ACLK)
		f_past_valid <= 1;
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// Upstream master Bus properties
	// {{{
	////////////////////////////////////////////////////////////////////////
	//
	//
	always @(*)
	if (!f_past_valid)
	begin
		assume(!S_AXI_ARESETN);
		assert(!M_AXI_ARESETN);
	end

	faxil_slave #(
		// {{{
		.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
		.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
		.F_OPT_ASSUME_RESET(1'b1),
		.F_OPT_NO_RESET((OPT_MIN_RESET == 0) ? 1:0),
//		.F_AXI_MAXWAIT((F_OPT_FAULTLESS) ? (2*OPT_TIMEOUT+2) : 0),
		.F_AXI_MAXRSTALL(3),
//		.F_AXI_MAXDELAY(OPT_TIMEOUT+OPT_TIMEOUT+5),
		.F_LGDEPTH(LGDEPTH+1),
		//
		.F_AXI_MAXWAIT((F_OPT_FAULTLESS) ? (2*OPT_TIMEOUT+2) : 0),
		.F_AXI_MAXDELAY(2*OPT_TIMEOUT+3)
		// }}}
	) axils (
		// {{{
		.i_clk(S_AXI_ACLK),
		.i_axi_reset_n(S_AXI_ARESETN),
		//
		.i_axi_awvalid(S_AXI_AWVALID),
		.i_axi_awready(S_AXI_AWREADY),
		.i_axi_awaddr( S_AXI_AWADDR),
		.i_axi_awprot( S_AXI_AWPROT),
		.i_axi_awcache(4'h0),
		//
		.i_axi_wvalid(S_AXI_WVALID),
		.i_axi_wready(S_AXI_WREADY),
		.i_axi_wdata( S_AXI_WDATA),
		.i_axi_wstrb( S_AXI_WSTRB),
		//
		.i_axi_bvalid(S_AXI_BVALID),
		.i_axi_bready(S_AXI_BREADY),
		.i_axi_bresp( S_AXI_BRESP),
		//
		.i_axi_arvalid(S_AXI_ARVALID),
		.i_axi_arready(S_AXI_ARREADY),
		.i_axi_araddr( S_AXI_ARADDR),
		.i_axi_arprot( S_AXI_ARPROT),
		.i_axi_arcache(4'h0),
		//
		.i_axi_rvalid(S_AXI_RVALID),
		.i_axi_rready(S_AXI_RREADY),
		.i_axi_rdata( S_AXI_RDATA),
		.i_axi_rresp( S_AXI_RRESP),
		//
		.f_axi_awr_outstanding(faxils_awr_outstanding),
		.f_axi_wr_outstanding(faxils_wr_outstanding),
		.f_axi_rd_outstanding(faxils_rd_outstanding)
		// }}}
	);

	always @(*)
	if (!F_OPT_WRITES)
	begin
		// {{{
		assume(!S_AXI_AWVALID);
		assume(!S_AXI_WVALID);
		assert(aw_count == 0);
		assert(w_count == 0);
		assert(!M_AXI_AWVALID);
		assert(!M_AXI_WVALID);
		// }}}
	end

	always @(*)
	if (!F_OPT_READS)
	begin
		// {{{
		assume(!S_AXI_ARVALID);
		assert(r_count == 0);
		assert(!S_AXI_RVALID);
		assert(!M_AXI_ARVALID);
		// }}}
	end
	// }}}
	////////////////////////////////////////////////////////////////////////
	//
	// General Induction properties
	// {{{
	////////////////////////////////////////////////////////////////////////
	//

	always @(*)
	begin
		// {{{
		assert(aw_zero == (aw_count  == 0));
		assert(w_zero  == (w_count   == 0));
		assert(r_zero  == (r_count   == 0));

		//
		assert(aw_full == (&aw_count));
		assert(w_full  == (&w_count));
		assert(r_full  == (&r_count));
		//
		if (M_AXI_ARESETN && !o_write_fault)
		begin
			assert(downstream_aw_zero  == (downstream_aw_count == 0));
			assert(downstream_w_zero   == (downstream_w_count  == 0));
			assert(downstream_aw_count + (M_AXI_AWVALID ? 1:0)
					+ (S_AXI_BVALID ? 1:0) == aw_count);
			assert(downstream_w_count + (M_AXI_WVALID ? 1:0)
					+ (S_AXI_BVALID ? 1:0) ==  w_count);
		end

		if (M_AXI_ARESETN && !o_read_fault)
		begin
			assert(downstream_r_zero   == (downstream_r_count  == 0));
			assert(downstream_r_count + (M_AXI_ARVALID ? 1:0)
					+ (S_AXI_RVALID ? 1:0) ==  r_count);
		end
		//
		assert(aw_count == faxils_awr_outstanding);
		assert(w_count  == faxils_wr_outstanding);
		assert(r_count  == faxils_rd_outstanding);

		assert(aw_w_greater == (aw_count > w_count));
		assert(w_aw_greater == (w_count > aw_count));
		// }}}
	end
	// }}}
	generate if (F_OPT_FAULTLESS)
	begin : ASSUME_FAULTLESS
		// {{{
		////////////////////////////////////////////////////////////////
		//
		// Assume the downstream core is protocol compliant, and
		// prove that o_fault stays low.
		// {{{
		////////////////////////////////////////////////////////////////
		//
		wire	[LGDEPTH:0]	faxilm_awr_outstanding,
					faxilm_wr_outstanding,
					faxilm_rd_outstanding;

		faxil_master #(
			// {{{
			.C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
			.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
			.F_OPT_NO_RESET((OPT_MIN_RESET == 0) ? 1:0),
			.F_AXI_MAXWAIT(OPT_TIMEOUT),
			.F_AXI_MAXRSTALL(4),
			.F_AXI_MAXDELAY(OPT_TIMEOUT),
			.F_LGDEPTH(LGDEPTH+1)
			// }}}
		) axilm (
			// {{{
			.i_clk(S_AXI_ACLK),
			.i_axi_reset_n(M_AXI_ARESETN && S_AXI_ARESETN),
			//
			.i_axi_awvalid(M_AXI_AWVALID),
			.i_axi_awready(M_AXI_AWREADY),
			.i_axi_awaddr( M_AXI_AWADDR),
			.i_axi_awprot( M_AXI_AWPROT),
			.i_axi_awcache(4'h0),
			//
			.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_bvalid(M_AXI_BVALID),
			.i_axi_bready(M_AXI_BREADY),
			.i_axi_bresp( M_AXI_BRESP),
			//
			.i_axi_arvalid(M_AXI_ARVALID),
			.i_axi_arready(M_AXI_ARREADY),
			.i_axi_araddr( M_AXI_ARADDR),
			.i_axi_arprot( M_AXI_ARPROT),
			.i_axi_arcache(4'h0),
			//
			.i_axi_rvalid(M_AXI_RVALID),
			.i_axi_rready(M_AXI_RREADY),
			.i_axi_rdata( M_AXI_RDATA),
			.i_axi_rresp( M_AXI_RRESP),
			//
			.f_axi_awr_outstanding(faxilm_awr_outstanding),
			.f_axi_wr_outstanding(faxilm_wr_outstanding),
			.f_axi_rd_outstanding(faxilm_rd_outstanding)
			// }}}
		);

		//
		// Here's the big proof
		// {{{
		always @(*)
			assert(!o_write_fault);
		always @(*)
			assert(!o_read_fault);
		// }}}
		// }}}
		////////////////////////////////////////////////////////////////
		//
		// The following properties are necessary for passing induction
		// {{{
		////////////////////////////////////////////////////////////////
		//
		//
		always @(*)
		begin
			assert(!aw_stall_limit);
			assert(!w_stall_limit);
			assert(!w_ack_limit);

			assert(!r_stall_limit);
			assert(!r_ack_limit);

			if (M_AXI_ARESETN)
			begin
			assert(downstream_aw_count == faxilm_awr_outstanding);
			assert(downstream_w_count  == faxilm_wr_outstanding);
			assert(downstream_r_count  == faxilm_rd_outstanding);
			end
		end

		if (OPT_SELF_RESET)
		begin
			always @(posedge S_AXI_ACLK)
			if (f_past_valid)
				assert(M_AXI_ARESETN == $past(S_AXI_ARESETN));
		end

`ifdef	VERIFIC
		wire	[LGDEPTH:0]	f_axi_arstall;
		wire	[LGDEPTH:0]	f_axi_awstall;
		wire	[LGDEPTH:0]	f_axi_wstall;

		assign	f_axi_awstall = axilm.CHECK_STALL_COUNT.f_axi_awstall;
		assign	f_axi_wstall  = axilm.CHECK_STALL_COUNT.f_axi_wstall;
		assign	f_axi_arstall = axilm.CHECK_STALL_COUNT.f_axi_arstall;

		always @(*)
		if (M_AXI_ARESETN && S_AXI_ARESETN && !o_write_fault)
			assert(f_axi_awstall == aw_stall_counter);

		always @(*)
		if (M_AXI_ARESETN && S_AXI_ARESETN && !o_write_fault)
			assert(f_axi_wstall == w_stall_counter);

		always @(*)
		if (M_AXI_ARESETN && S_AXI_ARESETN && !o_read_fault)
			assert(f_axi_arstall == r_stall_counter);
`endif
		// }}}
		// }}}
	end else begin : WILD_DOWNSTREAM
		// {{{
		////////////////////////////////////////////////////////////////
		//
		// cover() checks, checks that only make sense if faults are
		// possible
		//

		reg		write_faulted, read_faulted, faulted;
		reg	[3:0]	cvr_writes, cvr_reads;


		if (OPT_SELF_RESET)
		begin
			////////////////////////////////////////////////////////
			//
			// Prove that we can actually reset the downstream
			// bus/core as desired
			// {{{
			////////////////////////////////////////////////////////
			//
			//
			initial	write_faulted = 0;
			always @(posedge S_AXI_ACLK)
			if (!S_AXI_ARESETN)
				write_faulted <= 0;
			else if (o_write_fault)
				write_faulted <= 1;


			initial	faulted = 0;
			always @(posedge S_AXI_ACLK)
			if (!S_AXI_ARESETN)
				read_faulted <= 0;
			else if (o_read_fault)
				read_faulted <= 1;

			always @(*)
				faulted = (write_faulted || read_faulted);

			always @(posedge S_AXI_ACLK)
				cover(write_faulted && $rose(M_AXI_ARESETN));

			always @(posedge S_AXI_ACLK)
				cover(read_faulted && $rose(M_AXI_ARESETN));

			always @(posedge S_AXI_ACLK)
				cover(faulted && M_AXI_ARESETN && S_AXI_BVALID);

			always @(posedge S_AXI_ACLK)
				cover(faulted && M_AXI_ARESETN && S_AXI_RVALID);


			initial	cvr_writes = 0;
			always @(posedge S_AXI_ACLK)
			if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault)
				cvr_writes <= 0;
			else if (write_faulted && S_AXI_BVALID && S_AXI_BREADY
				&& S_AXI_BRESP == OKAY
				&&(!(&cvr_writes)))
				cvr_writes <= cvr_writes + 1;

			always @(*)
				cover(cvr_writes > 5);

			initial	cvr_reads = 0;
			always @(posedge S_AXI_ACLK)
			if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault)
				cvr_reads <= 0;
			else if (read_faulted && S_AXI_RVALID && S_AXI_RREADY
				&& S_AXI_RRESP == OKAY
				&&(!(&cvr_reads)))
				cvr_reads <= cvr_reads + 1;

			always @(*)
				cover(cvr_reads > 5);
			// }}}
		end

		// }}}
	end endgenerate

`endif
// }}}
endmodule