verilog/rtl/softshell/third_party/wb2axip/bench/formal/fwb_slave.v - third_party/shuttle/sky130/mpw-001/slot-003 - Git at Google

 ////////////////////////////////////////////////////////////////////////////////
 //
 // Filename:	fwb_slave.v
 //
 // Project:	WB2AXIPSP: bus bridges and other odds and ends
 //
 // Purpose:	This file describes the rules of a wishbone interaction from the
 //		perspective of a wishbone slave.  These formal rules may be used
 //	with yosys-smtbmc to *prove* that the slave properly handles outgoing
 //	responses to (assumed correct) incoming requests.
 //
 //	This module contains no functional logic.  It is intended for formal
 //	verification only.  The outputs returned, the number of requests that
 //	have been made, the number of acknowledgements received, and the number
 //	of outstanding requests, are designed for further formal verification
 //	purposes *only*.
 //
 //	This file is different from a companion formal_master.v file in that
 //	assumptions are made about the inputs to the slave: i_wb_cyc,
 //	i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, and i_wb_sel, while full
 //	assertions are made about the outputs: o_wb_stall, o_wb_ack, o_wb_data,
 //	o_wb_err.  In the formal_master.v, assertions are made about the
 //	master outputs (slave inputs)), and assumptions are made about the
 //	master inputs (the slave outputs).
 //
 //	In order to make it easier to compare the slave against the master,
 //	assumptions with respect to the slave have been marked with the
 //	`SLAVE_ASSUME macro.  Similarly, assertions the slave would make have
 //	been marked with `SLAVE_ASSERT.  This allows the master to redefine
 //	these two macros to be from his perspective, and therefore the
 //	diffs between the two files actually show true differences, rather
 //	than just these differences in perspective.
 //
 //
 // Creator:	Dan Gisselquist, Ph.D.
 //		Gisselquist Technology, LLC
 //
 ////////////////////////////////////////////////////////////////////////////////
 //
 // Copyright (C) 2017-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	fwb_slave(i_clk, i_reset,
 		// The Wishbone bus
 		i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel,
 			i_wb_ack, i_wb_stall, i_wb_idata, i_wb_err,
 		// Some convenience output parameters
 		f_nreqs, f_nacks, f_outstanding);
 	parameter		AW=32, DW=32;
 	parameter		F_MAX_STALL = 0,
 				F_MAX_ACK_DELAY = 0;
 	parameter		F_LGDEPTH = 4;
 	parameter [(F_LGDEPTH-1):0] F_MAX_REQUESTS = 0;
 	//
 	// If true, allow the bus to be kept open when there are no outstanding
 	// requests.  This is useful for any master that might execute a
 	// read modify write cycle, such as an atomic add.
 	parameter [0:0]		F_OPT_RMW_BUS_OPTION = 1;
 	//
 	//
 	// If true, allow the bus to issue multiple discontinuous requests.
 	// Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other
 	// requests are outstanding
 	parameter	[0:0]	F_OPT_DISCONTINUOUS = 1;
 	//
 	//
 	// If true, insist that there be a minimum of a single clock delay
 	// between request and response.  This defaults to off since the
 	// wishbone specification specifically doesn't require this.  However,
 	// some interfaces do, so we allow it as an option here.
 	parameter	[0:0]	F_OPT_MINCLOCK_DELAY = 0;
 	//
 	//
 	//
 	localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
 	localparam	MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
 				? F_MAX_STALL : F_MAX_ACK_DELAY;
 	localparam	DLYBITS= (MAX_DELAY < 4) ? 2
 				: ((MAX_DELAY <    16) ? 4
 				: ((MAX_DELAY <    64) ? 6
 				: ((MAX_DELAY <   256) ? 8
 				: ((MAX_DELAY <  1024) ? 10
 				: ((MAX_DELAY <  4096) ? 12
 				: ((MAX_DELAY < 16384) ? 14
 				: ((MAX_DELAY < 65536) ? 16
 				: 32)))))));
 	//
 	input	wire			i_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;
 	//
 	input	wire			i_wb_ack;
 	input	wire			i_wb_stall;
 	input	wire	[(DW-1):0]	i_wb_idata;
 	input	wire			i_wb_err;
 	//
 	output	reg	[(F_LGDEPTH-1):0]	f_nreqs, f_nacks;
 	output	wire	[(F_LGDEPTH-1):0]	f_outstanding;

 `define	SLAVE_ASSUME	assume
 `define	SLAVE_ASSERT	assert
 	//
 	// Let's just make sure our parameters are set up right
 	//
 	initial	assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});

 	//
 	// Wrap the request line in a bundle.  The top bit, named STB_BIT,
 	// is the bit indicating whether the request described by this vector
 	// is a valid request or not.
 	//
 	localparam	STB_BIT = 2+AW+DW+DW/8-1;
 	wire	[STB_BIT:0]	f_request;
 	assign	f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel };

 	//
 	// A quick register to be used later to know if the $past() operator
 	// will yield valid result
 	reg	f_past_valid;
 	initial	f_past_valid = 1'b0;
 	always @(posedge i_clk)
 		f_past_valid <= 1'b1;
 	always @(*)
 	if (!f_past_valid)
 		`SLAVE_ASSUME(i_reset);
 	//
 	//
 	// Assertions regarding the initial (and reset) state
 	//
 	//

 	//
 	// Assume we start from a reset condition
 	initial assert(i_reset);
 	initial `SLAVE_ASSUME(!i_wb_cyc);
 	initial `SLAVE_ASSUME(!i_wb_stb);
 	//
 	initial	`SLAVE_ASSERT(!i_wb_ack);
 	initial	`SLAVE_ASSERT(!i_wb_err);

 `ifdef	VERIFIC
 	always @(*)
 	if (!f_past_valid)
 	begin
 		`SLAVE_ASSUME(!i_wb_cyc);
 		`SLAVE_ASSUME(!i_wb_stb);
 		//
 		`SLAVE_ASSERT(!i_wb_ack);
 		`SLAVE_ASSERT(!i_wb_err);
 	end
 `endif
 	always @(posedge i_clk)
 	if ((!f_past_valid)||($past(i_reset)))
 	begin
 		`SLAVE_ASSUME(!i_wb_cyc);
 		`SLAVE_ASSUME(!i_wb_stb);
 		//
 		`SLAVE_ASSERT(!i_wb_ack);
 		`SLAVE_ASSERT(!i_wb_err);
 	end

 	always @(*)
 	if (!f_past_valid)
 		`SLAVE_ASSUME(!i_wb_cyc);

 	//
 	//
 	// Bus requests
 	//
 	//

 	// Following any bus error, the CYC line should be dropped to abort
 	// the transaction
 	always @(posedge i_clk)
 	if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
 		`SLAVE_ASSUME(!i_wb_cyc);

 	// STB can only be true if CYC is also true
 	always @(*)
 	if (i_wb_stb)
 		`SLAVE_ASSUME(i_wb_cyc);

 	// If a request was both outstanding and stalled on the last clock,
 	// then nothing should change on this clock regarding it.
 	always @(posedge i_clk)
 	if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
 			&&($past(i_wb_stall))&&(i_wb_cyc))
 	begin
 		`SLAVE_ASSUME(i_wb_stb);
 		`SLAVE_ASSUME(i_wb_we   == $past(i_wb_we));
 		`SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
 		`SLAVE_ASSUME(i_wb_sel  == $past(i_wb_sel));
 		if (i_wb_we)
 			`SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
 	end

 	// Within any series of STB/requests, the direction of the request
 	// may not change.
 	always @(posedge i_clk)
 	if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
 		`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));


 	// Within any given bus cycle, the direction may *only* change when
 	// there are no further outstanding requests.
 	always @(posedge i_clk)
 	if ((f_past_valid)&&(f_outstanding > 0))
 		`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));

 	// Write requests must also set one (or more) of i_wb_sel
 	//
 	// This test has been removed since down-sizers (taking bus from width
 	// DW to width dw < DW) might actually create empty requests that this
 	// would prevent.  Re-enabling it would also complicate AXI to WB
 	// transfers, since AXI explicitly allows WSTRB == 0.  Finally, this
 	// criteria isn't found in the WB spec--so while it might be a good
 	// idea to check, in hind sight there are too many exceptions to be
 	// dogmatic about it.
 	//
 	// always @(*)
 	// if ((i_wb_stb)&&(i_wb_we))
 	//	`SLAVE_ASSUME(|i_wb_sel);


 	//
 	//
 	// Bus responses
 	//
 	//

 	// If CYC was low on the last clock, then both ACK and ERR should be
 	// low on this clock.
 	always @(posedge i_clk)
 	if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
 	begin
 		`SLAVE_ASSERT(!i_wb_ack);
 		`SLAVE_ASSERT(!i_wb_err);
 		// Stall may still be true--such as when we are not
 		// selected at some arbiter between us and the slave
 	end

 	//
 	// Any time the CYC line drops, it is possible that there may be a
 	// remaining (registered) ACK or ERR that hasn't yet been returned.
 	// Restrict such out of band returns so that they are *only* returned
 	// if there is an outstanding operation.
 	//
 	// Update: As per spec, WB-classic to WB-pipeline conversions require
 	// that the ACK|ERR might come back on the same cycle that STB
 	// is low, yet also be registered.  Hence, if STB & STALL are true on
 	// one cycle, then CYC is dropped, ACK|ERR might still be true on the
 	// cycle when CYC is dropped
 	always @(posedge i_clk)
 	if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
 	begin
 		// Note that, unlike f_outstanding, f_nreqs and f_nacks are both
 		// registered.  Hence, we can check here if a response is still
 		// pending.  If not, no response should be returned.
 		if (f_nreqs == f_nacks)
 		begin
 			`SLAVE_ASSERT(!i_wb_ack);
 			`SLAVE_ASSERT(!i_wb_err);
 		end
 	end

 	// ACK and ERR may never both be true at the same time
 	always @(*)
 		`SLAVE_ASSERT((!i_wb_ack)||(!i_wb_err));

 	generate if (F_MAX_STALL > 0)
 	begin : MXSTALL
 		//
 		// Assume the slave cannnot stall for more than F_MAX_STALL
 		// counts.  We'll count this forward any time STB and STALL
 		// are both true.
 		//
 		reg	[(DLYBITS-1):0]		f_stall_count;

 		initial	f_stall_count = 0;
 		always @(posedge i_clk)
 		if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
 			f_stall_count <= f_stall_count + 1'b1;
 		else
 			f_stall_count <= 0;

 		always @(*)
 		if (i_wb_cyc)
 			`SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
 	end endgenerate

 	generate if (F_MAX_ACK_DELAY > 0)
 	begin : MXWAIT
 		//
 		// Assume the slave will respond within F_MAX_ACK_DELAY cycles,
 		// counted either from the end of the last request, or from the
 		// last ACK received
 		//
 		reg	[(DLYBITS-1):0]		f_ackwait_count;

 		initial	f_ackwait_count = 0;
 		always @(posedge i_clk)
 		if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
 				&&(!i_wb_ack)&&(!i_wb_err)
 				&&(f_outstanding > 0))
 			f_ackwait_count <= f_ackwait_count + 1'b1;
 		else
 			f_ackwait_count <= 0;

 		always @(*)
 		if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
 					&&(!i_wb_ack)&&(!i_wb_err)
 					&&(f_outstanding > 0))
 			`SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
 	end endgenerate

 	//
 	// Count the number of requests that have been received
 	//
 	initial	f_nreqs = 0;
 	always @(posedge i_clk)
 	if ((i_reset)||(!i_wb_cyc))
 		f_nreqs <= 0;
 	else if ((i_wb_stb)&&(!i_wb_stall))
 		f_nreqs <= f_nreqs + 1'b1;


 	//
 	// Count the number of acknowledgements that have been returned
 	//
 	initial	f_nacks = 0;
 	always @(posedge i_clk)
 	if (i_reset)
 		f_nacks <= 0;
 	else if (!i_wb_cyc)
 		f_nacks <= 0;
 	else if ((i_wb_ack)||(i_wb_err))
 		f_nacks <= f_nacks + 1'b1;

 	//
 	// The number of outstanding requests is the difference between
 	// the number of requests and the number of acknowledgements
 	//
 	assign	f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;

 	always @(*)
 	if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
 	begin
 		if (i_wb_stb)
 			`SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
 		else
 			`SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
 		`SLAVE_ASSERT(f_nacks <= f_nreqs);
 		assert(f_outstanding < (1<<F_LGDEPTH)-1);
 	end else
 		assume(f_outstanding < (1<<F_LGDEPTH)-1);

 	always @(*)
 	if ((i_wb_cyc)&&(f_outstanding == 0))
 	begin
 		// If nothing is outstanding, then there should be
 		// no acknowledgements ... however, an acknowledgement
 		// *can* come back on the same clock as the stb is
 		// going out.
 		if (F_OPT_MINCLOCK_DELAY)
 		begin
 			`SLAVE_ASSERT(!i_wb_ack);
 			`SLAVE_ASSERT(!i_wb_err);
 		end else begin
 			`SLAVE_ASSERT((!i_wb_ack)||((i_wb_stb)&&(!i_wb_stall)));
 			// The same is true of errors.  They may not be
 			// created before the request gets through
 			`SLAVE_ASSERT((!i_wb_err)||((i_wb_stb)&&(!i_wb_stall)));
 		end
 	end else if (!i_wb_cyc && f_nacks == f_nreqs)
 	begin
 		`SLAVE_ASSERT(!i_wb_ack);
 		`SLAVE_ASSERT(!i_wb_err);
 	end

 	generate if (!F_OPT_RMW_BUS_OPTION)
 	begin
 		// If we aren't waiting for anything, and we aren't issuing
 		// any requests, then then our transaction is over and we
 		// should be dropping the CYC line.
 		always @(*)
 		if (f_outstanding == 0)
 			`SLAVE_ASSUME((i_wb_stb)||(!i_wb_cyc));
 		// Not all masters will abide by this restriction.  Some
 		// masters may wish to implement read-modify-write bus
 		// interactions.  These masters need to keep CYC high between
 		// transactions, even though nothing is outstanding.  For
 		// these busses, turn F_OPT_RMW_BUS_OPTION on.
 	end endgenerate

 	generate if ((!F_OPT_DISCONTINUOUS)&&(!F_OPT_RMW_BUS_OPTION))
 	begin : INSIST_ON_NO_DISCONTINUOUS_STBS
 		// Within my own code, once a request begins it goes to
 		// completion and the CYC line is dropped.  The master
 		// is not allowed to raise STB again after dropping it.
 		// Doing so would be a *discontinuous* request.
 		//
 		// However, in any RMW scheme, discontinuous requests are
 		// necessary, and the spec doesn't disallow them.  Hence we
 		// make this check optional.
 		always @(posedge i_clk)
 		if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
 			`SLAVE_ASSUME(!i_wb_stb);
 	end endgenerate

 endmodule
 `undef	SLAVE_ASSUME
 `undef	SLAVE_ASSERT
	////////////////////////////////////////////////////////////////////////////////
	//
	// Filename: fwb_slave.v
	//
	// Project: WB2AXIPSP: bus bridges and other odds and ends
	//
	// Purpose: This file describes the rules of a wishbone interaction from the
	// perspective of a wishbone slave. These formal rules may be used
	// with yosys-smtbmc to prove that the slave properly handles outgoing
	// responses to (assumed correct) incoming requests.
	//
	// This module contains no functional logic. It is intended for formal
	// verification only. The outputs returned, the number of requests that
	// have been made, the number of acknowledgements received, and the number
	// of outstanding requests, are designed for further formal verification
	// purposes only.
	//
	// This file is different from a companion formal_master.v file in that
	// assumptions are made about the inputs to the slave: i_wb_cyc,
	// i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, and i_wb_sel, while full
	// assertions are made about the outputs: o_wb_stall, o_wb_ack, o_wb_data,
	// o_wb_err. In the formal_master.v, assertions are made about the
	// master outputs (slave inputs)), and assumptions are made about the
	// master inputs (the slave outputs).
	//
	// In order to make it easier to compare the slave against the master,
	// assumptions with respect to the slave have been marked with the
	// `SLAVE_ASSUME macro. Similarly, assertions the slave would make have
	// been marked with `SLAVE_ASSERT. This allows the master to redefine
	// these two macros to be from his perspective, and therefore the
	// diffs between the two files actually show true differences, rather
	// than just these differences in perspective.
	//
	//
	// Creator: Dan Gisselquist, Ph.D.
	// Gisselquist Technology, LLC
	//
	////////////////////////////////////////////////////////////////////////////////
	//
	// Copyright (C) 2017-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 fwb_slave(i_clk, i_reset,
	// The Wishbone bus
	i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel,
	i_wb_ack, i_wb_stall, i_wb_idata, i_wb_err,
	// Some convenience output parameters
	f_nreqs, f_nacks, f_outstanding);
	parameter AW=32, DW=32;
	parameter F_MAX_STALL = 0,
	F_MAX_ACK_DELAY = 0;
	parameter F_LGDEPTH = 4;
	parameter [(F_LGDEPTH-1):0] F_MAX_REQUESTS = 0;
	//
	// If true, allow the bus to be kept open when there are no outstanding
	// requests. This is useful for any master that might execute a
	// read modify write cycle, such as an atomic add.
	parameter [0:0] F_OPT_RMW_BUS_OPTION = 1;
	//
	//
	// If true, allow the bus to issue multiple discontinuous requests.
	// Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other
	// requests are outstanding
	parameter [0:0] F_OPT_DISCONTINUOUS = 1;
	//
	//
	// If true, insist that there be a minimum of a single clock delay
	// between request and response. This defaults to off since the
	// wishbone specification specifically doesn't require this. However,
	// some interfaces do, so we allow it as an option here.
	parameter [0:0] F_OPT_MINCLOCK_DELAY = 0;
	//
	//
	//
	localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
	localparam MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
	? F_MAX_STALL : F_MAX_ACK_DELAY;
	localparam DLYBITS= (MAX_DELAY < 4) ? 2
	: ((MAX_DELAY < 16) ? 4
	: ((MAX_DELAY < 64) ? 6
	: ((MAX_DELAY < 256) ? 8
	: ((MAX_DELAY < 1024) ? 10
	: ((MAX_DELAY < 4096) ? 12
	: ((MAX_DELAY < 16384) ? 14
	: ((MAX_DELAY < 65536) ? 16
	: 32)))))));
	//
	input wire i_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;
	//
	input wire i_wb_ack;
	input wire i_wb_stall;
	input wire [(DW-1):0] i_wb_idata;
	input wire i_wb_err;
	//
	output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks;
	output wire [(F_LGDEPTH-1):0] f_outstanding;

	`define SLAVE_ASSUME assume
	`define SLAVE_ASSERT assert
	//
	// Let's just make sure our parameters are set up right
	//
	initial assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});

	//
	// Wrap the request line in a bundle. The top bit, named STB_BIT,
	// is the bit indicating whether the request described by this vector
	// is a valid request or not.
	//
	localparam STB_BIT = 2+AW+DW+DW/8-1;
	wire [STB_BIT:0] f_request;
	assign f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel };

	//
	// A quick register to be used later to know if the $past() operator
	// will yield valid result
	reg f_past_valid;
	initial f_past_valid = 1'b0;
	always @(posedge i_clk)
	f_past_valid <= 1'b1;
	always @(*)
	if (!f_past_valid)
	`SLAVE_ASSUME(i_reset);
	//
	//
	// Assertions regarding the initial (and reset) state
	//
	//

	//
	// Assume we start from a reset condition
	initial assert(i_reset);
	initial `SLAVE_ASSUME(!i_wb_cyc);
	initial `SLAVE_ASSUME(!i_wb_stb);
	//
	initial `SLAVE_ASSERT(!i_wb_ack);
	initial `SLAVE_ASSERT(!i_wb_err);

	`ifdef VERIFIC
	always @(*)
	if (!f_past_valid)
	begin
	`SLAVE_ASSUME(!i_wb_cyc);
	`SLAVE_ASSUME(!i_wb_stb);
	//
	`SLAVE_ASSERT(!i_wb_ack);
	`SLAVE_ASSERT(!i_wb_err);
	end
	`endif
	always @(posedge i_clk)
	if ((!f_past_valid)\|\|($past(i_reset)))
	begin
	`SLAVE_ASSUME(!i_wb_cyc);
	`SLAVE_ASSUME(!i_wb_stb);
	//
	`SLAVE_ASSERT(!i_wb_ack);
	`SLAVE_ASSERT(!i_wb_err);
	end

	always @(*)
	if (!f_past_valid)
	`SLAVE_ASSUME(!i_wb_cyc);

	//
	//
	// Bus requests
	//
	//

	// Following any bus error, the CYC line should be dropped to abort
	// the transaction
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
	`SLAVE_ASSUME(!i_wb_cyc);

	// STB can only be true if CYC is also true
	always @(*)
	if (i_wb_stb)
	`SLAVE_ASSUME(i_wb_cyc);

	// If a request was both outstanding and stalled on the last clock,
	// then nothing should change on this clock regarding it.
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
	&&($past(i_wb_stall))&&(i_wb_cyc))
	begin
	`SLAVE_ASSUME(i_wb_stb);
	`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
	`SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
	`SLAVE_ASSUME(i_wb_sel == $past(i_wb_sel));
	if (i_wb_we)
	`SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
	end

	// Within any series of STB/requests, the direction of the request
	// may not change.
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
	`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));


	// Within any given bus cycle, the direction may only change when
	// there are no further outstanding requests.
	always @(posedge i_clk)
	if ((f_past_valid)&&(f_outstanding > 0))
	`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));

	// Write requests must also set one (or more) of i_wb_sel
	//
	// This test has been removed since down-sizers (taking bus from width
	// DW to width dw < DW) might actually create empty requests that this
	// would prevent. Re-enabling it would also complicate AXI to WB
	// transfers, since AXI explicitly allows WSTRB == 0. Finally, this
	// criteria isn't found in the WB spec--so while it might be a good
	// idea to check, in hind sight there are too many exceptions to be
	// dogmatic about it.
	//
	// always @(*)
	// if ((i_wb_stb)&&(i_wb_we))
	// `SLAVE_ASSUME(\|i_wb_sel);


	//
	//
	// Bus responses
	//
	//

	// If CYC was low on the last clock, then both ACK and ERR should be
	// low on this clock.
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
	begin
	`SLAVE_ASSERT(!i_wb_ack);
	`SLAVE_ASSERT(!i_wb_err);
	// Stall may still be true--such as when we are not
	// selected at some arbiter between us and the slave
	end

	//
	// Any time the CYC line drops, it is possible that there may be a
	// remaining (registered) ACK or ERR that hasn't yet been returned.
	// Restrict such out of band returns so that they are only returned
	// if there is an outstanding operation.
	//
	// Update: As per spec, WB-classic to WB-pipeline conversions require
	// that the ACK\|ERR might come back on the same cycle that STB
	// is low, yet also be registered. Hence, if STB & STALL are true on
	// one cycle, then CYC is dropped, ACK\|ERR might still be true on the
	// cycle when CYC is dropped
	always @(posedge i_clk)
	if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
	begin
	// Note that, unlike f_outstanding, f_nreqs and f_nacks are both
	// registered. Hence, we can check here if a response is still
	// pending. If not, no response should be returned.
	if (f_nreqs == f_nacks)
	begin
	`SLAVE_ASSERT(!i_wb_ack);
	`SLAVE_ASSERT(!i_wb_err);
	end
	end

	// ACK and ERR may never both be true at the same time
	always @(*)
	`SLAVE_ASSERT((!i_wb_ack)\|\|(!i_wb_err));

	generate if (F_MAX_STALL > 0)
	begin : MXSTALL
	//
	// Assume the slave cannnot stall for more than F_MAX_STALL
	// counts. We'll count this forward any time STB and STALL
	// are both true.
	//
	reg [(DLYBITS-1):0] f_stall_count;

	initial f_stall_count = 0;
	always @(posedge i_clk)
	if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
	f_stall_count <= f_stall_count + 1'b1;
	else
	f_stall_count <= 0;

	always @(*)
	if (i_wb_cyc)
	`SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
	end endgenerate

	generate if (F_MAX_ACK_DELAY > 0)
	begin : MXWAIT
	//
	// Assume the slave will respond within F_MAX_ACK_DELAY cycles,
	// counted either from the end of the last request, or from the
	// last ACK received
	//
	reg [(DLYBITS-1):0] f_ackwait_count;

	initial f_ackwait_count = 0;
	always @(posedge i_clk)
	if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
	&&(!i_wb_ack)&&(!i_wb_err)
	&&(f_outstanding > 0))
	f_ackwait_count <= f_ackwait_count + 1'b1;
	else
	f_ackwait_count <= 0;

	always @(*)
	if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
	&&(!i_wb_ack)&&(!i_wb_err)
	&&(f_outstanding > 0))
	`SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
	end endgenerate

	//
	// Count the number of requests that have been received
	//
	initial f_nreqs = 0;
	always @(posedge i_clk)
	if ((i_reset)\|\|(!i_wb_cyc))
	f_nreqs <= 0;
	else if ((i_wb_stb)&&(!i_wb_stall))
	f_nreqs <= f_nreqs + 1'b1;


	//
	// Count the number of acknowledgements that have been returned
	//
	initial f_nacks = 0;
	always @(posedge i_clk)
	if (i_reset)
	f_nacks <= 0;
	else if (!i_wb_cyc)
	f_nacks <= 0;
	else if ((i_wb_ack)\|\|(i_wb_err))
	f_nacks <= f_nacks + 1'b1;

	//
	// The number of outstanding requests is the difference between
	// the number of requests and the number of acknowledgements
	//
	assign f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;

	always @(*)
	if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
	begin
	if (i_wb_stb)
	`SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
	else
	`SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
	`SLAVE_ASSERT(f_nacks <= f_nreqs);
	assert(f_outstanding < (1<<F_LGDEPTH)-1);
	end else
	assume(f_outstanding < (1<<F_LGDEPTH)-1);

	always @(*)
	if ((i_wb_cyc)&&(f_outstanding == 0))
	begin
	// If nothing is outstanding, then there should be
	// no acknowledgements ... however, an acknowledgement
	// can come back on the same clock as the stb is
	// going out.
	if (F_OPT_MINCLOCK_DELAY)
	begin
	`SLAVE_ASSERT(!i_wb_ack);
	`SLAVE_ASSERT(!i_wb_err);
	end else begin
	`SLAVE_ASSERT((!i_wb_ack)\|\|((i_wb_stb)&&(!i_wb_stall)));
	// The same is true of errors. They may not be
	// created before the request gets through
	`SLAVE_ASSERT((!i_wb_err)\|\|((i_wb_stb)&&(!i_wb_stall)));
	end
	end else if (!i_wb_cyc && f_nacks == f_nreqs)
	begin
	`SLAVE_ASSERT(!i_wb_ack);
	`SLAVE_ASSERT(!i_wb_err);
	end

	generate if (!F_OPT_RMW_BUS_OPTION)
	begin
	// If we aren't waiting for anything, and we aren't issuing
	// any requests, then then our transaction is over and we
	// should be dropping the CYC line.
	always @(*)
	if (f_outstanding == 0)
	`SLAVE_ASSUME((i_wb_stb)\|\|(!i_wb_cyc));
	// Not all masters will abide by this restriction. Some
	// masters may wish to implement read-modify-write bus
	// interactions. These masters need to keep CYC high between
	// transactions, even though nothing is outstanding. For
	// these busses, turn F_OPT_RMW_BUS_OPTION on.
	end endgenerate

	generate if ((!F_OPT_DISCONTINUOUS)&&(!F_OPT_RMW_BUS_OPTION))
	begin : INSIST_ON_NO_DISCONTINUOUS_STBS
	// Within my own code, once a request begins it goes to
	// completion and the CYC line is dropped. The master
	// is not allowed to raise STB again after dropping it.
	// Doing so would be a discontinuous request.
	//
	// However, in any RMW scheme, discontinuous requests are
	// necessary, and the spec doesn't disallow them. Hence we
	// make this check optional.
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
	`SLAVE_ASSUME(!i_wb_stb);
	end endgenerate

	endmodule
	`undef SLAVE_ASSUME
	`undef SLAVE_ASSERT