| Line 13... |
Line 13... |
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
|
// Copyright (C) 2015-2016, Gisselquist Technology, LLC
|
//
|
//
|
// This program is free software (firmware): you can redistribute it and/or
|
// This file is part of the pipelined Wishbone to AXI converter project, a
|
// modify it under the terms of the GNU General Public License as published
|
// project that contains multiple bus bridging designs and formal bus property
|
// by the Free Software Foundation, either version 3 of the License, or (at
|
// sets.
|
// your option) any later version.
|
//
|
//
|
// The bus bridge designs and property sets are free RTL designs: you can
|
// This program is distributed in the hope that it will be useful, but WITHOUT
|
// redistribute them and/or modify any of them under the terms of the GNU
|
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
|
// Lesser General Public License as published by the Free Software Foundation,
|
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
// either version 3 of the License, or (at your option) any later version.
|
// for more details.
|
//
|
//
|
// The bus bridge designs and property sets are distributed in the hope that
|
// You should have received a copy of the GNU General Public License along
|
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
|
// with this program. (It's in the $(ROOT)/doc directory, run make with no
|
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
// target there if the PDF file isn't present.) If not, see
|
// 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.
|
// <http://www.gnu.org/licenses/> for a copy.
|
//
|
//
|
// License: GPL, v3, as defined and found on www.gnu.org,
|
// License: LGPL, v3, as defined and found on www.gnu.org,
|
// http://www.gnu.org/licenses/gpl.html
|
// http://www.gnu.org/licenses/lgpl.html
|
//
|
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
`default_nettype none
|
`default_nettype none
|
| Line 86... |
Line 89... |
always @(posedge i_clk)
|
always @(posedge i_clk)
|
f_past_valid <= 1'b1;
|
f_past_valid <= 1'b1;
|
always @(*)
|
always @(*)
|
assert((f_past_valid) || (i_reset));
|
assert((f_past_valid) || (i_reset));
|
|
|
wire [AW:0] f_rd_request;
|
wire [AW+(DW/8):0] f_rd_request;
|
assign f_rd_request = { i_av_read, i_av_address };
|
assign f_rd_request = { i_av_read, i_av_byteenable, i_av_address };
|
|
|
wire [(AW+DW+(DW/8)):0] f_wr_request;
|
wire [(AW+DW+(DW/8)):0] f_wr_request;
|
assign f_wr_request = { i_av_write, i_av_address, i_av_writedata,
|
assign f_wr_request = { i_av_write, i_av_address, i_av_writedata,
|
i_av_byteenable };
|
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)
|
always @($global_clock)
|
if ((f_past_valid)&&(!$rose(i_clk)))
|
if ((f_past_valid)&&(!$rose(i_clk)))
|
begin
|
begin
|
assume($stable(f_rd_request));
|
assume($stable(f_rd_request));
|
assume($stable(f_wr_request));
|
assume($stable(f_wr_request));
|
| Line 106... |
Line 122... |
assert($stable(i_av_readdatavalid));
|
assert($stable(i_av_readdatavalid));
|
assert($stable(i_av_writeresponsevalid));
|
assert($stable(i_av_writeresponsevalid));
|
assert($stable(i_av_readdata));
|
assert($stable(i_av_readdata));
|
assert($stable(i_av_response));
|
assert($stable(i_av_response));
|
end
|
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)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&(!$past(i_av_lock)))
|
if ((f_past_valid)&&(!$past(i_av_lock)))
|
assume((!i_av_lock)||(i_av_read)||(i_av_write));
|
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;
|
initial f_rd_nreqs = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
f_rd_nreqs <= 0;
|
f_rd_nreqs <= 0;
|
else if ((i_av_read)&&(!i_av_waitrequest))
|
else if ((i_av_read)&&(!i_av_waitrequest))
|
f_rd_nreqs <= f_rd_nreqs + 1'b1;
|
f_rd_nreqs <= f_rd_nreqs + 1'b1;
|
|
|
|
// Count the number of read acknowledgements
|
initial f_rd_nacks = 0;
|
initial f_rd_nacks = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
f_rd_nacks <= 0;
|
f_rd_nacks <= 0;
|
else if (i_av_readdatavalid)
|
else if (i_av_readdatavalid)
|
f_rd_nacks <= f_rd_nacks + 1'b1;
|
f_rd_nacks <= f_rd_nacks + 1'b1;
|
|
|
assign f_rd_outstanding = f_rd_nreqs - f_rd_nacks;
|
// 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;
|
initial f_wr_nreqs = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
f_wr_nreqs <= 0;
|
f_wr_nreqs <= 0;
|
else if ((i_av_write)&&(!i_av_waitrequest))
|
else if ((i_av_write)&&(!i_av_waitrequest))
|
f_wr_nreqs <= f_wr_nreqs + 1'b1;
|
f_wr_nreqs <= f_wr_nreqs + 1'b1;
|
|
|
|
// Count the number of write acknowledgements/responses
|
initial f_wr_nacks = 0;
|
initial f_wr_nacks = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_reset)
|
if (i_reset)
|
f_wr_nacks <= 0;
|
f_wr_nacks <= 0;
|
else if (i_av_writeresponsevalid)
|
else if (i_av_writeresponsevalid)
|
| Line 170... |
Line 253... |
assert(f_rd_nacks == 0);
|
assert(f_rd_nacks == 0);
|
assert(f_wr_nreqs == 0);
|
assert(f_wr_nreqs == 0);
|
assert(f_wr_nacks == 0);
|
assert(f_wr_nacks == 0);
|
end
|
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)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_read)))
|
if ((f_rd_outstanding == 0)&&(!i_reset)
|
assume($stable(f_rd_request));
|
&&((!i_av_read)||(i_av_waitrequest)))
|
|
assert(!i_av_readdatavalid);
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_write)))
|
if ((f_wr_outstanding == 0)&&(!i_reset)
|
assume($stable(f_wr_request));
|
&&((!i_av_write)||(i_av_waitrequest)))
|
|
assert(!i_av_writeresponsevalid);
|
|
|
always @(*)
|
always @(*)
|
assume((!i_av_read)||(!i_av_write));
|
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 @(*)
|
always @(*)
|
assert((!i_av_writeresponsevalid)||(!i_av_readdatavalid));
|
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)
|
always @(posedge i_clk)
|
if (f_rd_outstanding == 0)
|
if (i_reset)
|
assert(!i_av_readdatavalid);
|
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)
|
always @(posedge i_clk)
|
if (f_wr_outstanding == 0)
|
if (i_reset)
|
assert(!i_av_writeresponsevalid);
|
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
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
