Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
340 lines (294 sloc) 9.36 KB
////////////////////////////////////////////////////////////////////////////////
//
// 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-2019, 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
You can’t perform that action at this time.