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 program is free software (firmware): you can redistribute it and/or
// modify it under the terms of  the GNU General Public License as published
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
// for more details.
//
// You should have received a copy of the GNU General Public License along
// with this program.  (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:	GPL, v3, as defined and found on www.gnu.org,
//		http://www.gnu.org/licenses/gpl.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:0]	f_rd_request;
	assign	f_rd_request = { i_av_read,  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 };
 
 
	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
 
	always @(posedge i_clk)
		if ((f_past_valid)&&(!$past(i_av_lock)))
			assume((!i_av_lock)||(i_av_read)||(i_av_write));
 
	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;
 
	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;
 
	assign	f_rd_outstanding = f_rd_nreqs - f_rd_nacks;
 
	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;
 
	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
 
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_read)))
		assume($stable(f_rd_request));
 
	always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_write)))
		assume($stable(f_wr_request));
 
	always @(*)
		assume((!i_av_read)||(!i_av_write));
 
	always @(*)
		assert((!i_av_writeresponsevalid)||(!i_av_readdatavalid));
 
	always @(posedge i_clk)
		if (f_rd_outstanding == 0)
			assert(!i_av_readdatavalid);
 
	always @(posedge i_clk)
		if (f_wr_outstanding == 0)
			assert(!i_av_writeresponsevalid);
 
endmodule