Subversion Repositories wb2axip

////////////////////////////////////////////////////////////////////////////////
//
// Filename: 	fav_slave.v
//
// Project:	Pipelined Wishbone to AXI converter
//
// 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-2016, Gisselquist Technology, LLC
//
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs.  (It's in the $(ROOT)/doc directory.  Run make
// with no target there if the PDF file isn't present.)  If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License:	LGPL, v3, as defined and found on www.gnu.org,
//		http://www.gnu.org/licenses/lgpl.html
//
////////////////////////////////////////////////////////////////////////////////
//
//
`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