////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	fav_slave.v
//
// Project:	WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose:	Formal properties of an Avalon slave.  These are the properties
//		the module owning the slave should use: they assume inputs from
//	the bus master, and assert that the outputs from the slave are valid.
//
// Creator:	Dan Gisselquist, Ph.D.
//		Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-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	fav_slave(i_clk, i_reset,
		i_av_read,
		i_av_write,
		i_av_address,
		i_av_writedata,
			i_av_byteenable,
		i_av_lock,
		i_av_waitrequest,	// = wb_stall
		//
		i_av_writeresponsevalid,
		//
		i_av_readdatavalid,
		i_av_readdata,
		i_av_response,	// Error response = 2'b11
		f_rd_nreqs, f_rd_nacks, f_rd_outstanding,
		f_wr_nreqs, f_wr_nacks, f_wr_outstanding);
	parameter	DW=32, AW=14;
	parameter	F_LGDEPTH=6;
	parameter	[(F_LGDEPTH-1):0]	F_MAX_REQUESTS = 62;
	input	wire			i_clk, i_reset;
	input	wire			i_av_read;
	input	wire			i_av_write;
	input	wire	[(AW-1):0]	i_av_address;
	input	wire	[(DW-1):0]	i_av_writedata;
	input	wire	[(DW/8-1):0]	i_av_byteenable;
	input	wire			i_av_lock;
	//
	input	wire			i_av_waitrequest;
	input	wire			i_av_writeresponsevalid;
	input	wire			i_av_readdatavalid;
	input	wire	[(DW-1):0]	i_av_readdata;
	input	wire	[1:0]		i_av_response;
	//
	output	reg	[(F_LGDEPTH-1):0] f_rd_nreqs, f_rd_nacks;
	output	wire	[(F_LGDEPTH-1):0] f_rd_outstanding;
	output	reg	[(F_LGDEPTH-1):0] f_wr_nreqs, f_wr_nacks;
	output	wire	[(F_LGDEPTH-1):0] f_wr_outstanding;

	assert	property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});


	reg	f_past_valid;
	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid <= 1'b1;
	always @(*)
		assert((f_past_valid) || (i_reset));

	wire	[AW+(DW/8):0]	f_rd_request;
	assign	f_rd_request = { i_av_read,  i_av_byteenable, i_av_address };

	wire	[(AW+DW+(DW/8)):0]	f_wr_request;
	assign	f_wr_request = { i_av_write, i_av_address, i_av_writedata,
					i_av_byteenable };

	/////////////////////////////
	//
	// Require that nothing changes, save on a clock tick.
	//
	// This is only required if yosys is using the clk2fflogic
	// command, a command only required if multiple clocks are
	// in use.  Since this can greatly slow down formal proofs,
	// we limit any code associated with this option to only
	// those times the option is in play.
	//
	/////////////////////////////

	generate if (F_OPT_CLK2FFLOGIC)
	begin
		always @($global_clock)
		if ((f_past_valid)&&(!$rose(i_clk)))
		begin
			assume($stable(f_rd_request));
			assume($stable(f_wr_request));
			assume($stable(i_av_lock));

			assert($stable(i_av_readdatavalid));
			assert($stable(i_av_writeresponsevalid));
			assert($stable(i_av_readdata));
			assert($stable(i_av_response));
		end
	end endgenerate

	/////////////////////////////
	//
	// Assumptions about a slave's inputs
	//
	/////////////////////////////


	initial	assume(!i_av_read);
	initial	assume(!i_av_write);
	initial	assume(!i_av_lock);
	//
	initial	assert(!i_av_readdatavalid);
	initial	assert(!i_av_writeresponsevalid);
	//

	always @(posedge i_clk)
		if (i_reset)
		begin
			assume(!i_av_read);
			assume(!i_av_write);
			assume(!i_av_lock);
		end

	always @(*)
		if (i_av_write)
			assume(|i_av_byteenable);

	// It is a protocol violation to issue both read and write requests
	// on the same clock
	always @(*)
		assume((!i_av_read)||(!i_av_write));

	// Once a read request has been placed upon the bus, it will remain
	// there until wait request goes low
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_read)))
		assume((i_reset)||(f_rd_request == $past(f_rd_request)));

	// Same thing for a write request
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_write)))
		assume((i_reset)||(f_wr_request == $past(f_wr_request)));

	// A lock request can only be asserted at the same time a read or
	// write request is being made.
	always @(posedge i_clk)
		if ((f_past_valid)&&(!$past(i_av_lock)))
			assume((!i_av_lock)||(i_av_read)||(i_av_write));

	// A lock request can only be de-asserted following the last read
	// or write request made with it asserted
	always @(posedge i_clk)
		if ((f_past_valid)&&($past(i_av_lock)
				&&(!i_av_read)&&(!i_av_write)))
			assume((i_reset)||(i_av_lock)
				||(i_av_read)||(i_av_write));


	/////////////////////////////
	//
	// Internal state variables
	//
	/////////////////////////////

	// Count the number of read requests
	initial	f_rd_nreqs = 0;
	always @(posedge i_clk)
		if (i_reset)
			f_rd_nreqs <= 0;
		else if ((i_av_read)&&(!i_av_waitrequest))
			f_rd_nreqs <= f_rd_nreqs + 1'b1;

	// Count the number of read acknowledgements
	initial	f_rd_nacks = 0;
	always @(posedge i_clk)
		if (i_reset)
			f_rd_nacks <= 0;
		else if (i_av_readdatavalid)
			f_rd_nacks <= f_rd_nacks + 1'b1;

	// The difference between read requests and acknowledgements is
	// the number of outstanding read requests
	assign	f_rd_outstanding = (i_reset) ? 0 : (f_rd_nreqs - f_rd_nacks);

	// Count the number of write requests
	initial	f_wr_nreqs = 0;
	always @(posedge i_clk)
		if (i_reset)
			f_wr_nreqs <= 0;
		else if ((i_av_write)&&(!i_av_waitrequest))
			f_wr_nreqs <= f_wr_nreqs + 1'b1;

	// Count the number of write acknowledgements/responses
	initial	f_wr_nacks = 0;
	always @(posedge i_clk)
		if (i_reset)
			f_wr_nacks <= 0;
		else if (i_av_writeresponsevalid)
			f_wr_nacks <= f_wr_nacks + 1'b1;

	assign	f_wr_outstanding = f_wr_nreqs - f_wr_nacks;


	initial	assume(!i_av_read);
	initial	assume(!i_av_write);
	initial	assume(!i_av_lock);
	//
	initial	assert(!i_av_readdatavalid);
	initial	assert(!i_av_writeresponsevalid);
	//

	always @(posedge i_clk)
		if (i_reset)
		begin
			assume(!i_av_read);
			assume(!i_av_write);
		end

	always @(posedge i_clk)
		if ((f_past_valid)&&($past(i_reset)))
		begin
			assert(!i_av_readdatavalid);
			assert(!i_av_writeresponsevalid);
			assert(f_rd_nreqs == 0);
			assert(f_rd_nacks == 0);
			assert(f_wr_nreqs == 0);
			assert(f_wr_nacks == 0);
		end

	// Just like a read and write request cannot both be made at the same
	// time, neither can both responses come back at the same time
	always @(*)
		assert((!i_av_writeresponsevalid)||(!i_av_readdatavalid));

	// If nothing is outstanding, then there should be no responses.
	// If i_reset is asserted, a response may have been registered, and
	// so may still return on this clock.
	always @(posedge i_clk)
		if ((f_rd_outstanding == 0)&&(!i_reset)
				&&((!i_av_read)||(i_av_waitrequest)))
			assert(!i_av_readdatavalid);

	always @(posedge i_clk)
		if ((f_wr_outstanding == 0)&&(!i_reset)
				&&((!i_av_write)||(i_av_waitrequest)))
			assert(!i_av_writeresponsevalid);

	always @(*)
		assert({1'b0, f_wr_outstanding} + { 1'b0, f_rd_outstanding }
			< F_MAX_REQUESTS);

	generate if (F_OPT_MAX_STALL > 0)
	begin
		reg	[(LGWAIT-1):0]	stall_count;

		initial	stall_count = 0;
		always @(posedge i_clk)
			if (i_reset)
				stall_count <= 0;
			else if (((i_av_read)||(i_av_write))&&(i_av_waitrequest))
				stall_count <= stall_count + 1'b1;
			else
				stall_count <= 0;

		always @(*)
			assert((i_reset)||(stall_count < F_OPT_MAX_STALL));
	end endgenerate

	generate if (F_OPT_MAX_WAIT > 0)
	begin
		reg	[(LGWAIT-1):0]	read_wait, write_wait;

		//
		// Insist on a minimum amount of time to wait for a *read*
		// response.
		//
		always @(posedge i_clk)
			if (i_reset)
				read_wait <= 0;
			else if ((i_av_readdatavalid)
					||((i_av_read)&&(!i_av_waitrequest)))
				read_wait <= 0;
			else if (f_rd_outstanding > 0)
				read_wait <= read_wait + 1'b1;

		always @(*)
			assert((i_av_readdatavalid)
				||(f_rd_outstanding == 0)
				||(read_wait < F_OPT_MAX_WAIT));


		//
		// Insist on a minimum amount of time to wait for a *write*
		// response.
		//
		always @(posedge i_clk)
			if (i_reset)
				write_wait <= 0;
			else if ((i_av_writeresponsevalid)
					||((i_av_write)&&(!i_av_waitrequest)))
				write_wait <= 0;
			else if (f_wr_outstanding > 0)
				write_wait <= write_wait + 1'b1;

		always @(*)
			assert((i_av_writeresponsevalid)
				||(f_wr_outstanding == 0)
				||(write_wait < F_OPT_MAX_WAIT));
	end endgenerate

endmodule