rtl/wb2axip: add to version control

1 files changed, 854 insertions, 0 deletions

diff --git a/rtl/wb2axip/wbxclk.v b/rtl/wb2axip/wbxclk.v
new file mode 100644
index 0000000..5f404b0
--- /dev/null
+++ b/rtl/wb2axip/wbxclk.v
@@ -0,0 +1,854 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: 	rtl/wbxclk.v
+// {{{
+// Project:	WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose:	To cross clock domains with a (pipelined) wishbone bus.
+//
+// Challenges:
+//	1. Wishbone has no capacity for back pressure.  That means that we'll
+//		need to be careful not to issue more STB requests than ACKs
+//		that will fit in the return buffer.
+//
+//	    Imagine, for example, a faster return clock but a slave that needs
+//		many clocks to get going.  During that time, many requests
+//		might be issued.  If they all suddenly get returned at once,
+//		flooding the return ACK FIFO, then we have a problem.
+//
+//	2. Bus aborts.  If we ever have to abort a transaction, that's going
+//		to be a pain.  The FIFOs will need to be reset and the
+//		downstream CYC line dropped.  This needs to be done
+//		synchronously in both domains, but there's no real choice but
+//		to make the crossing asynchronous.
+//
+//	3. Synchronous CYC.  Lowering CYC is a normal part of the protocol, as
+//		is raising CYC.  CYC is used as a bus locking scheme, so we'll
+//		need to know when it is (properly) lowered downstream.  This
+//		can be done by passing a synchronous CYC drop request through
+//		the pipeline in addition to the bus aborts above.
+//
+//	Status:
+//		Formally verified against a set of bus properties, not yet
+//		used in any real or simulated designs
+//
+// Creator:	Dan Gisselquist, Ph.D.
+//		Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2020-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	wbxclk #(
+		// {{{
+		parameter	AW=32,
+				DW=32,
+				LGFIFO = 5
+		// }}}
+	) (
+		// {{{
+		input	wire			i_wb_clk, i_reset,
+		// Input/master bus
+		input	wire			i_wb_cyc, i_wb_stb, i_wb_we,
+		input	wire	[(AW-1):0]	i_wb_addr,
+		input	wire	[(DW-1):0]	i_wb_data,
+		input	wire	[(DW/8-1):0]	i_wb_sel,
+		output	wire			o_wb_stall,
+		output	reg			o_wb_ack,
+		output	reg	[(DW-1):0]	o_wb_data,
+		output	reg			o_wb_err,
+		// Delayed bus
+		input	wire			i_xclk_clk,
+		output	reg			o_xclk_cyc,
+		output	reg			o_xclk_stb,
+		output	reg			o_xclk_we,
+		output	reg	[(AW-1):0]	o_xclk_addr,
+		output	reg	[(DW-1):0]	o_xclk_data,
+		output	reg	[(DW/8-1):0]	o_xclk_sel,
+		input	wire			i_xclk_stall,
+		input	wire			i_xclk_ack,
+		input	wire	[(DW-1):0]	i_xclk_data,
+		input	wire			i_xclk_err
+		// }}}
+	);
+
+	//
+	// Declare our signals
+	// {{{
+	localparam	NFF = 2;
+	reg		wb_active;
+	reg [NFF-2:0]	bus_abort_pipe;
+	reg [LGFIFO:0]	acks_outstanding;
+	reg		ackfifo_single, ackfifo_empty, ackfifo_full;
+	wire		ack_stb, err_stb;
+	wire [DW-1:0]	ret_wb_data;
+	wire		req_fifo_stall, no_returns;
+	//
+	// Verilator lint_off SYNCASYNCNET
+	reg		bus_abort;
+	// Verilator lint_on  SYNCASYNCNET
+	//
+	wire		req_stb, req_fifo_empty;
+	reg		xclk_err_state, ign_ackfifo_stall;
+	reg		xck_reset;
+	reg [NFF-2:0]	xck_reset_pipe;
+	wire		req_we;
+	wire [AW-1:0]	req_addr;
+	wire [DW-1:0]	req_data;
+	wire [DW/8-1:0]	req_sel;
+`ifdef	FORMAL
+	wire	[LGFIFO:0]	ackfifo_prefill, reqfifo_prefill;
+`endif
+	// }}}
+
+	//
+	//
+	// On the original wishbone clock ...
+	//
+	//	 FIFO/queue up our requests
+	// {{{
+	initial	wb_active = 1'b0;
+	always	@(posedge i_wb_clk)
+	if (i_reset || !i_wb_cyc)
+		wb_active <= 1'b0;
+	else if (i_wb_stb && !o_wb_stall)
+		wb_active <= 1'b1;
+
+	initial	{ bus_abort, bus_abort_pipe } = -1;
+	always	@(posedge i_wb_clk)
+	if (i_reset)
+		{ bus_abort, bus_abort_pipe } <= -1;
+	else if (!i_wb_cyc && (!ackfifo_empty))
+		{ bus_abort, bus_abort_pipe } <= -1;
+	else if (o_wb_err)
+		{ bus_abort, bus_abort_pipe } <= -1;
+	else if (ackfifo_empty)
+		{ bus_abort, bus_abort_pipe } <= { bus_abort_pipe, 1'b0 };
+`ifdef	FORMAL
+	always @(*)
+	if (bus_abort_pipe)
+		assert(bus_abort);
+`endif
+	// }}}
+
+	//
+	// The request FIFO itself
+	// {{{
+	afifo #(
+`ifdef	FORMAL
+		.OPT_REGISTER_READS(0),
+		.F_OPT_DATA_STB(1'b0),
+`endif
+		.NFF(NFF), .LGFIFO(LGFIFO),
+		.WIDTH(2+AW+DW+(DW/8))
+	) reqfifo(.i_wclk(i_wb_clk), .i_wr_reset_n(!bus_abort),
+		.i_wr((i_wb_stb&&!o_wb_stall) || (wb_active && !i_wb_cyc)),
+		.i_wr_data({ i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }),
+		.o_wr_full(req_fifo_stall),
+		//
+		.i_rclk(i_xclk_clk), .i_rd_reset_n(!xck_reset),
+		.i_rd(!o_xclk_stb || !i_xclk_stall),
+		.o_rd_data({ req_stb, req_we, req_addr, req_data, req_sel }),
+		.o_rd_empty(req_fifo_empty)
+`ifdef	FORMAL
+		, .f_fill(reqfifo_prefill)
+`endif
+	);
+	// }}}
+
+	//
+	// Downstream bus--issuing requests
+	// {{{
+	initial	{ xck_reset, xck_reset_pipe } = -1;
+	always	@(posedge i_xclk_clk or posedge bus_abort)
+	if (bus_abort)
+		{ xck_reset, xck_reset_pipe } <= -1;
+	else
+		{ xck_reset, xck_reset_pipe } <= { xck_reset_pipe, 1'b0 };
+`ifdef	FORMAL
+	always @(*)
+	if (xck_reset_pipe)
+		assert(xck_reset);
+`endif
+
+	initial	xclk_err_state = 1'b0;
+	always @(posedge i_xclk_clk)
+	if (xck_reset || (!req_fifo_empty && !req_stb))
+		xclk_err_state <= 1'b0;
+	else if (o_xclk_cyc && i_xclk_err)
+		xclk_err_state <= 1'b1;
+
+	initial	o_xclk_cyc = 1'b0;
+	always @(posedge i_xclk_clk)
+	if (xck_reset || (o_xclk_cyc && i_xclk_err))
+		o_xclk_cyc <= 1'b0;
+	else if (!req_fifo_empty && !req_stb)
+		o_xclk_cyc <= 1'b0;
+	else if (!req_fifo_empty && !xclk_err_state)
+		o_xclk_cyc <= req_stb;
+
+	initial	o_xclk_stb = 1'b0;
+	always @(posedge i_xclk_clk)
+	if (xck_reset || (o_xclk_cyc && i_xclk_err) || xclk_err_state)
+		o_xclk_stb <= 1'b0;
+	else if (!o_xclk_stb || !i_xclk_stall)
+		o_xclk_stb <= req_stb && !req_fifo_empty;
+
+	always @(posedge i_xclk_clk)
+	if ((!o_xclk_stb || !i_xclk_stall) && req_stb && !req_fifo_empty)
+		o_xclk_we <= req_we;
+
+	always @(posedge i_xclk_clk)
+	if (!o_xclk_stb || !i_xclk_stall)
+	begin
+		o_xclk_addr <= req_addr;
+		o_xclk_data <= req_data;
+		o_xclk_sel  <= req_sel;
+	end
+	// }}}
+
+
+	//
+	// Request counting
+	// {{{
+	initial	acks_outstanding = 0;
+	initial	ackfifo_single = 0;
+	initial	ackfifo_empty  = 1;
+	initial	ackfifo_full   = 0;
+	always @(posedge i_wb_clk)
+	if (i_reset || !i_wb_cyc || o_wb_err)
+	begin
+		acks_outstanding <= 0;
+		ackfifo_single   <= 0;
+		ackfifo_empty    <= 1;
+		ackfifo_full     <= 0;
+	end else case({ (i_wb_stb && !o_wb_stall), o_wb_ack })
+	2'b10: begin
+		acks_outstanding <= acks_outstanding + 1;
+		ackfifo_empty <= 0;
+		ackfifo_single <= ackfifo_empty;
+		ackfifo_full   <= (&acks_outstanding[LGFIFO-1:0]);
+		end
+	2'b01: begin
+		acks_outstanding <= acks_outstanding - 1;
+		ackfifo_empty <= (acks_outstanding <= 1);
+		ackfifo_single <= (acks_outstanding == 2);
+		ackfifo_full   <= 0;
+		end
+	default: begin end
+	endcase
+
+`ifdef	FORMAL
+	always @(*)
+	begin
+		assert(ackfifo_single == (acks_outstanding == 1));
+		assert(ackfifo_empty == (acks_outstanding == 0));
+		assert(ackfifo_full == (acks_outstanding >= (1<<LGFIFO)));
+		assert(acks_outstanding <= (1<<LGFIFO));
+	end
+`endif
+
+	assign	o_wb_stall = ackfifo_full || bus_abort || req_fifo_stall;
+	// }}}
+
+	//
+	// The return FIFO
+	// {{{
+	afifo #(
+		.OPT_REGISTER_READS(0),
+		.NFF(NFF), .LGFIFO(LGFIFO),
+		.WIDTH(2+DW)
+`ifdef	FORMAL
+		, .F_OPT_DATA_STB(1'b0)
+`endif
+	) ackfifo(.i_wclk(i_xclk_clk), .i_wr_reset_n(!xck_reset),
+		.i_wr(o_xclk_cyc && ( i_xclk_ack || i_xclk_err )),
+		.i_wr_data({ i_xclk_ack, i_xclk_err, i_xclk_data }),
+		.o_wr_full(ign_ackfifo_stall),
+		//
+		.i_rclk(i_wb_clk), .i_rd_reset_n(!bus_abort),
+		.i_rd(!no_returns),
+		.o_rd_data({ ack_stb, err_stb, ret_wb_data }),
+		.o_rd_empty(no_returns)
+`ifdef	FORMAL
+		, .f_fill(ackfifo_prefill)
+`endif
+	);
+	// }}}
+
+	//
+	// Final return processing
+	// {{{
+	initial	{ o_wb_ack, o_wb_err } = 2'b00;
+	always @(posedge i_wb_clk)
+	if (i_reset || bus_abort || !i_wb_cyc || no_returns || o_wb_err)
+		{ o_wb_ack, o_wb_err } <=  2'b00;
+	else
+		{ o_wb_ack, o_wb_err } <= { ack_stb, err_stb };
+
+	always @(posedge i_wb_clk)
+		o_wb_data <= ret_wb_data;
+	// }}}
+
+	// Make Verilator happy
+	// {{{
+	// Verilator lint_off UNUSED
+	wire	unused;
+	assign	unused = &{ 1'b0, req_fifo_stall, ign_ackfifo_stall,
+			ackfifo_single };
+	// Verilator lint_on  UNUSED
+	// }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal properties
+// {{{
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef	FORMAL
+	// Register/net/macro declarations
+	// {{{
+`ifdef	BMC
+`define	BMC_ASSERT	assert
+`else
+`define	BMC_ASSERT	assume
+`endif
+
+	(* gclk *)	reg	gbl_clk;
+
+	wire	[LGFIFO:0]	fwb_nreqs, fwb_nacks, fwb_outstanding;
+	wire	[LGFIFO:0]	fxck_nreqs, fxck_nacks, fxck_outstanding;
+	reg	[LGFIFO:0]	ackfifo_fill, reqfifo_fill;
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Assume a clock
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	(* anyconst *)	reg	[3:0]	fwb_step, fxck_step;
+	reg	[3:0]	fwb_count, fxck_count;
+
+	always @(*)
+	begin
+		assume(fwb_step  >= 2);
+		assume(fxck_step >= 2);
+
+		assume(fwb_step  <= 4'b1000);
+		assume(fxck_step <= 4'b1000);
+
+	//	assume(fwb_step  == 4'b1000);
+	//	assume(fxck_step  == 4'b0111);
+		assume((fwb_step  == 4'b0111)
+			|| (fxck_step == 4'b0111));
+	end
+
+	always @(posedge gbl_clk)
+	begin
+		fwb_count  <= fwb_count  + fwb_step;
+		fxck_count <= fxck_count + fxck_step;
+	end
+
+	always @(*)
+	begin
+		assume(i_wb_clk   == fwb_count[3]);
+		assume(i_xclk_clk == fxck_count[3]);
+	end
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// ....
+	//
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	//
+	// Cross clock stability assumptions
+	// {{{
+	always @(posedge gbl_clk)
+	if (!$rose(i_wb_clk))
+	begin
+		assume($stable(i_reset));
+
+		assume($stable(i_wb_cyc));
+		assume($stable(i_wb_stb));
+		assume($stable(i_wb_we));
+		assume($stable(i_wb_addr));
+		assume($stable(i_wb_data));
+		assume($stable(i_wb_sel));
+	end
+
+	always @(posedge gbl_clk)
+	if (!$rose(i_xclk_clk))
+	begin
+		assume($stable(i_xclk_ack));
+		assume($stable(i_xclk_err));
+		assume($stable(i_xclk_data));
+		assume($stable(i_xclk_stall));
+	end
+
+	reg			past_wb_clk, past_wb_stb, past_wb_we,
+				past_wb_cyc, past_wb_reset, past_wb_err;
+	reg			past_xclk, past_xclk_stall, past_xclk_ack,
+				past_xclk_err;
+	reg	[DW-1:0]	past_xclk_data;
+	reg			f_drop_cyc_request;
+
+	always @(posedge gbl_clk)
+	begin
+		past_wb_clk  <= i_wb_clk;
+		past_wb_reset<= i_reset;
+		past_wb_cyc  <= i_wb_cyc;
+		past_wb_stb  <= i_wb_stb;
+		past_wb_we   <= i_wb_we;
+		past_wb_err  <= o_wb_err;
+	end
+
+	always @(*)
+	if (!i_wb_clk || past_wb_clk)
+	begin
+		assume(past_wb_reset== i_reset);
+		assume(past_wb_cyc == i_wb_cyc);
+		assume(past_wb_stb == i_wb_stb);
+		assume(past_wb_we  == i_wb_we);
+		assume(past_wb_err == o_wb_err);
+	end else begin
+		if (past_wb_err && past_wb_cyc)
+			assume(!i_wb_cyc);
+		if (fwb_outstanding > 0)
+			assume(past_wb_we == i_wb_we);
+	end
+
+	always @(posedge gbl_clk)
+	begin
+		past_xclk       <= i_xclk_clk;
+		past_xclk_stall <= i_xclk_stall;
+		past_xclk_data  <= i_xclk_data;
+		past_xclk_ack   <= i_xclk_ack;
+		past_xclk_err   <= i_xclk_err;
+	end
+
+	always @(*)
+	if (!i_xclk_clk || past_xclk)
+	begin
+		assume(past_xclk_stall == i_xclk_stall);
+		assume(past_xclk_data  == i_xclk_data);
+		assume(past_xclk_ack   == i_xclk_ack);
+		assume(past_xclk_err   == i_xclk_err);
+	end
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Wishbone bus property checks
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	fwb_slave #(
+		// {{{
+		.AW(AW), .DW(DW),
+		.F_LGDEPTH(LGFIFO+1), .F_OPT_DISCONTINUOUS(1)
+		// }}}
+	) slv(
+		// {{{
+		i_wb_clk, i_reset,
+		i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel,
+		o_wb_ack, o_wb_stall, o_wb_data, o_wb_err,
+		fwb_nreqs, fwb_nacks, fwb_outstanding
+		// }}}
+	);
+
+	fwb_master #(
+		// {{{
+		.AW(AW), .DW(DW),
+		.F_LGDEPTH(LGFIFO+1), .F_OPT_DISCONTINUOUS(1),
+		.F_MAX_STALL(4),
+		.F_MAX_ACK_DELAY(7)
+		// }}}
+	) xclkwb(
+		// {{{
+		i_xclk_clk, xck_reset,
+		o_xclk_cyc, o_xclk_stb, o_xclk_we, o_xclk_addr, o_xclk_data, o_xclk_sel,
+		i_xclk_ack, i_xclk_stall, i_xclk_data, i_xclk_err,
+		fxck_nreqs, fxck_nacks, fxck_outstanding
+		// }}}
+	);
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// (Random/unsorted) properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	always @(*)
+	if (reqfifo_fill != (o_xclk_stb ? 1:0) && !req_stb)
+		assert(ackfifo_fill == 0 || xclk_err_state);
+
+	always @(*)
+		reqfifo_fill = reqfifo_prefill + (o_xclk_stb ? 1:0);
+
+	always @(*)
+		ackfifo_fill = ackfifo_prefill // + (no_returns ? 0:1)
+			+ ((o_wb_ack || o_wb_err) ? 1:0);
+
+	always @(*)
+	if (fwb_outstanding > 0)
+		assert(wb_active);
+
+	always @(*)
+	if (f_drop_cyc_request && !bus_abort && !xclk_err_state)
+	begin
+		// req_stb is low, so cycle line has dropped normally
+
+		// If the cycle line has since risen, there may be requests
+		// within the request FIFO in addition to the drop-CYC message.
+		if (i_wb_cyc && wb_active)
+			assert(reqfifo_fill == fwb_outstanding + 1);
+
+		// We wouldn't place a drop CYC message into the FIFO
+		// unless XCLK-CYC  was already high
+		assert(o_xclk_cyc && !o_xclk_stb);
+		assert(ackfifo_fill == 0);
+		assert(fxck_outstanding == 0);
+
+		if (reqfifo_fill > 1)
+			assert(wb_active);
+		else
+			assert(!wb_active);
+	end else if (!bus_abort && xclk_err_state)
+	begin
+		//
+		// Bus error downstream causes an abort
+		assert(fxck_outstanding == 0);
+		assert(xck_reset  || wb_active || !i_wb_cyc);
+		assert(!o_xclk_stb);
+		if (ackfifo_fill == 1)
+			assert(no_returns || err_stb);
+		else if (!xck_reset && ackfifo_fill == 1)
+			assert(o_wb_err);
+	end else if (!bus_abort && i_wb_cyc && !xck_reset && !xclk_err_state)
+	begin
+		//
+		// Normal operation in operation
+		//
+		assert(reqfifo_fill <= fwb_outstanding + 1);
+		assert(ackfifo_fill <= fwb_outstanding);
+		assert(fxck_outstanding <= fwb_outstanding);
+		if (o_xclk_cyc)
+			assert(wb_active || f_drop_cyc_request);
+		if (reqfifo_fill == (o_xclk_stb ? 1:0) || req_stb)
+			// Either first request is for strobe, or other
+			// request counters are valid
+			assert(reqfifo_fill + ackfifo_fill
+				+ fxck_outstanding == fwb_outstanding);
+		else begin
+			// First request is to drop CYC
+			assert(reqfifo_fill== fwb_outstanding + 1);
+			assert(ackfifo_fill == 0);
+			assert(fxck_outstanding == 0);
+			assert(!o_xclk_stb);
+			assert(o_xclk_cyc);
+		end
+		if (acks_outstanding == 0)
+			assert((reqfifo_fill == 0)||!req_stb);
+	end
+
+	always @(*)
+	if (o_wb_ack && wb_active)
+	begin
+		assert(o_xclk_cyc || xclk_err_state);
+		assert(!f_drop_cyc_request);
+		assert(!xck_reset || bus_abort);
+	end
+
+	always @(*)
+	if (!bus_abort && acks_outstanding == 0)
+		assert(reqfifo_fill <= (f_drop_cyc_request ? 1:0)
+			+ ((o_xclk_stb && xck_reset) ? 1:0));
+
+	always @(*)
+	if (ackfifo_fill != 0)
+		assert(o_xclk_cyc || xck_reset || xclk_err_state);
+
+	always @(*)
+	if (fxck_outstanding > fwb_outstanding)
+		assert((!i_wb_cyc && wb_active)
+			|| i_reset || bus_abort || xck_reset);
+
+	always @(*)
+	if (!i_reset && xck_reset && !o_xclk_cyc)
+		assert(!i_wb_cyc || fwb_outstanding == reqfifo_fill);
+
+	always @(*)
+	if (bus_abort && i_wb_cyc)
+		assert(!wb_active);
+
+	always @(*)
+	if (acks_outstanding < (1<<LGFIFO))
+	begin
+		// assert(!reqfifo_full);
+		assert(!ackfifo_full);
+	end
+
+	always @(*)
+	if (!i_reset && !xck_reset && (fwb_outstanding > 0)
+		&& ((fxck_outstanding > 0) || o_xclk_stb))
+		assert(i_wb_we == o_xclk_we);
+
+	always @(*)
+	if (!i_reset && i_wb_cyc)
+		assert(acks_outstanding == fwb_outstanding);
+
+	always @(*)
+	if (xclk_err_state)
+		assert(!o_xclk_cyc);
+
+	always @(*)
+	if (!i_reset && !bus_abort && !i_wb_cyc)
+	begin
+		if (ackfifo_empty)
+		begin
+			if (reqfifo_fill > (o_xclk_stb ? 1:0))
+				assert(!req_stb || xck_reset);
+			assert(reqfifo_fill <= 1);
+			if (xck_reset && !xck_reset_pipe)
+				assert(!o_xclk_cyc);
+		end else begin
+			// ???
+		end
+	end
+
+	always @(*)
+		f_drop_cyc_request = !req_stb
+				&& (reqfifo_fill > (o_xclk_stb ? 1:0));
+
+	always @(*)
+	if (!i_reset && !xck_reset && !bus_abort && i_wb_cyc)
+	begin
+		if (!o_xclk_cyc && !xclk_err_state)
+			assert(acks_outstanding == reqfifo_fill
+				- (f_drop_cyc_request ? 1:0));
+		else if (!o_xclk_cyc && xclk_err_state)
+			assert(acks_outstanding >= reqfifo_fill
+				+ ackfifo_fill);
+		else if (o_xclk_cyc && !xclk_err_state)
+		begin
+			assert(acks_outstanding >= reqfifo_fill
+				- (f_drop_cyc_request ? 1:0));
+			assert(acks_outstanding >= ackfifo_fill);
+			assert(acks_outstanding >= fxck_outstanding);
+			assert(acks_outstanding ==
+				reqfifo_fill - (((reqfifo_fill > (o_xclk_stb ? 1:0))&&(!req_stb)) ? 1:0)
+				+ ackfifo_fill
+				+ fxck_outstanding);
+		end
+		if (f_drop_cyc_request)
+			assert(acks_outstanding +1 == reqfifo_fill);
+		else if (reqfifo_fill == 0)
+			assert(!wb_active || o_xclk_cyc || xclk_err_state);
+	end else if (!i_reset && !xck_reset && !bus_abort && f_drop_cyc_request)
+	begin
+		assert(acks_outstanding +1 == reqfifo_fill);
+		assert(ackfifo_fill == 0);
+		assert(fxck_outstanding == 0);
+		assert(!o_xclk_stb);
+		assert(o_xclk_cyc);
+	end
+
+
+	always @(*)
+	if (!bus_abort && wb_active && reqfifo_fill == 0 && !xclk_err_state)
+		assert(o_xclk_cyc);
+
+	always @(*)
+	if (f_drop_cyc_request && !bus_abort)
+		assert(!xck_reset);
+
+	always @(*)
+		assert(!xclk_err_state || acks_outstanding != 0 || xck_reset);
+
+	always @(*)
+	if (o_xclk_cyc && !i_wb_cyc)
+	begin
+		// assert(bus_abort || !xclk_err_state);
+		if (!wb_active && !bus_abort && !xck_reset)
+			assert(f_drop_cyc_request);
+	end else if (i_wb_cyc)
+	begin
+		if (wb_active && !xck_reset)
+			assert(o_xclk_cyc || xclk_err_state
+				||(reqfifo_fill >= acks_outstanding));
+	end
+
+	// always @(*)
+	// if (acks_outstanding >= (1<<LGFIFO))
+	//	assert(o_xclk_cyc || xclk_err_state || xck_reset);	// !!!!
+
+	//
+	// !!!!!!!!!!!
+	//
+	// Fig me here
+	always @(*)
+	if (wb_active && !bus_abort && !xck_reset && i_wb_cyc && !xclk_err_state)
+	begin
+		if (reqfifo_fill == 0)
+			assert(o_xclk_cyc);
+	end
+
+	always @(*)
+	if (fxck_outstanding > 0 || o_xclk_stb)
+		assert(!ign_ackfifo_stall);
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Sub properties for the REQ FIFO
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	always @(*)
+	if ((acks_outstanding > 0)&&(reqfifo_fill != (o_xclk_stb ? 1:0)))
+	begin
+		// Something valuable is in the request FIFO
+		if (i_wb_cyc && !f_drop_cyc_request)
+			`BMC_ASSERT(req_we == i_wb_we);
+		else if (req_stb && o_xclk_stb)
+			`BMC_ASSERT(o_xclk_we == req_we);
+
+		// if (acks_outstanding > 0)
+		if (!o_xclk_cyc || o_xclk_stb ||
+				fxck_outstanding > 0 || ackfifo_fill > 0)
+			`BMC_ASSERT(req_stb);
+	end // else the request FIFO is empty, nothing is in it
+		// No assumptions therefore need be made
+
+	always @(*)
+	if (!bus_abort && reqfifo_fill == acks_outstanding)
+		`BMC_ASSERT(!req_fifo_stall || !f_drop_cyc_request);
+
+	always @(*)
+	if (!i_reset && o_xclk_cyc && (reqfifo_fill != (o_xclk_stb ? 1:0)))
+		`BMC_ASSERT(!req_stb || req_we == o_xclk_we
+			|| fxck_outstanding == 0);
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Sub properties for the ACK FIFO
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	always @(*)
+	if (!no_returns)
+	begin
+		`BMC_ASSERT(ack_stb ^ err_stb);
+
+		if ((ackfifo_fill ==(o_wb_ack ? 2:1)) && xclk_err_state)
+			`BMC_ASSERT(err_stb);
+		else if (ackfifo_fill > (o_wb_ack ? 2:1))
+			`BMC_ASSERT(!err_stb);
+	end
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Cover properties
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+	reg		cvr_abort;
+	reg	[3:0]	cvr_replies, cvr_post_abort;
+
+	initial	cvr_abort = 0;
+	always @(posedge i_wb_clk)
+	if (i_reset)
+		cvr_abort <= 0;
+	else if (o_wb_err && acks_outstanding > 2)
+		cvr_abort <= 1;
+
+	initial	cvr_replies = 0;
+	always @(posedge i_wb_clk)
+	if (i_reset)
+		cvr_replies <= 0;
+	else if (o_wb_ack || o_wb_err)
+		cvr_replies <= cvr_replies + 1;
+
+	initial	cvr_post_abort = 0;
+	always @(posedge i_wb_clk)
+	if (i_reset)
+		cvr_post_abort <= 0;
+	else if (cvr_abort && o_wb_ack)
+		cvr_post_abort <= cvr_post_abort + 1;
+
+	always @(*)
+	begin
+		cover(cvr_replies > 1);	// 33
+		cover(cvr_replies > 3);	// 38
+		cover(cvr_replies > 9);
+
+		cover(cvr_abort);	// 31
+		cover(cvr_post_abort > 1 && cvr_replies > 1);	// 63
+		cover(cvr_post_abort > 1 && cvr_replies > 2);	// 63
+		cover(cvr_post_abort > 1 && cvr_replies > 3);	// 65
+		cover(cvr_post_abort > 2 && cvr_replies > 3);	// 65
+		cover(cvr_post_abort > 3 && cvr_replies > 3);	// 68
+		cover(cvr_post_abort > 4 && cvr_replies > 3);	// 70
+		cover(cvr_post_abort > 3 && cvr_replies > 6);	// 72
+	end
+
+	always @(posedge gbl_clk)
+	if (!i_reset)
+		cover(cvr_replies > 9 && !i_wb_clk && acks_outstanding == 0
+			&& fwb_nreqs == fwb_nacks && fwb_nreqs == cvr_replies
+			&& !bus_abort && fwb_count != fxck_count);
+
+	always @(posedge gbl_clk)
+	if (!i_reset)
+		cover(cvr_replies > 9 && !i_wb_clk && acks_outstanding == 0
+			&& fwb_nreqs == fwb_nacks && fwb_nreqs == cvr_replies
+			&& !bus_abort && fwb_count != fxck_count
+			&& fwb_step != fxck_step);
+
+	// }}}
+	////////////////////////////////////////////////////////////////////////
+	//
+	// Simplifying (careless) assumptions
+	// {{{
+	////////////////////////////////////////////////////////////////////////
+	//
+	//
+
+	// None (at present)
+
+	// }}}
+`endif
+// }}}
+endmodule