| Line 21... |
Line 21... |
// assertions are made about the outputs: o_wb_stall, o_wb_ack, o_wb_data,
|
// assertions are made about the outputs: o_wb_stall, o_wb_ack, o_wb_data,
|
// o_wb_err. In the formal_master.v, assertions are made about the
|
// o_wb_err. In the formal_master.v, assertions are made about the
|
// master outputs (slave inputs)), and assumptions are made about the
|
// master outputs (slave inputs)), and assumptions are made about the
|
// master inputs (the slave outputs).
|
// master inputs (the slave outputs).
|
//
|
//
|
//
|
// In order to make it easier to compare the slave against the master,
|
|
// assumptions with respect to the slave have been marked with the
|
|
// `SLAVE_ASSUME macro. Similarly, assertions the slave would make have
|
|
// been marked with `SLAVE_ASSERT. This allows the master to redefine
|
|
// these two macros to be from his perspective, and therefore the
|
|
// diffs between the two files actually show true differences, rather
|
|
// than just these differences in perspective.
|
//
|
//
|
//
|
//
|
// Creator: Dan Gisselquist, Ph.D.
|
// Creator: Dan Gisselquist, Ph.D.
|
// Gisselquist Technology, LLC
|
// Gisselquist Technology, LLC
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2017, Gisselquist Technology, LLC
|
// Copyright (C) 2017-2018, 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 79... |
Line 88... |
// Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other
|
// Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other
|
// requests are outstanding
|
// requests are outstanding
|
parameter [0:0] F_OPT_DISCONTINUOUS = 0;
|
parameter [0:0] F_OPT_DISCONTINUOUS = 0;
|
//
|
//
|
//
|
//
|
|
// If true, insist that there be a minimum of a single clock delay
|
|
// between request and response. This defaults to off since the
|
|
// wishbone specification specifically doesn't require this. However,
|
|
// some interfaces do, so we allow it as an option here.
|
|
parameter [0:0] F_OPT_MINCLOCK_DELAY = 0;
|
|
//
|
|
//
|
|
//
|
localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
|
localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
|
localparam MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
|
localparam MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
|
? F_MAX_STALL : F_MAX_ACK_DELAY;
|
? F_MAX_STALL : F_MAX_ACK_DELAY;
|
localparam DLYBITS= (MAX_DELAY < 4) ? 2
|
localparam DLYBITS= (MAX_DELAY < 4) ? 2
|
: ((MAX_DELAY < 16) ? 4
|
: ((MAX_DELAY < 16) ? 4
|
| Line 107... |
Line 124... |
input wire i_wb_err;
|
input wire i_wb_err;
|
//
|
//
|
output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks;
|
output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks;
|
output wire [(F_LGDEPTH-1):0] f_outstanding;
|
output wire [(F_LGDEPTH-1):0] f_outstanding;
|
|
|
|
`define SLAVE_ASSUME assume
|
|
`define SLAVE_ASSERT assert
|
//
|
//
|
// Let's just make sure our parameters are set up right
|
// Let's just make sure our parameters are set up right
|
//
|
//
|
assert property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
|
initial assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
|
|
|
//
|
//
|
// Wrap the request line in a bundle. The top bit, named STB_BIT,
|
// Wrap the request line in a bundle. The top bit, named STB_BIT,
|
// is the bit indicating whether the request described by this vector
|
// is the bit indicating whether the request described by this vector
|
// is a valid request or not.
|
// is a valid request or not.
|
| Line 130... |
Line 149... |
initial f_past_valid = 1'b0;
|
initial f_past_valid = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
f_past_valid <= 1'b1;
|
f_past_valid <= 1'b1;
|
always @(*)
|
always @(*)
|
if (!f_past_valid)
|
if (!f_past_valid)
|
assume(i_reset);
|
`SLAVE_ASSUME(i_reset);
|
//
|
//
|
//
|
//
|
// Assertions regarding the initial (and reset) state
|
// Assertions regarding the initial (and reset) state
|
//
|
//
|
//
|
//
|
|
|
//
|
//
|
// Assume we start from a reset condition
|
// Assume we start from a reset condition
|
initial assume(i_reset);
|
initial assert(i_reset);
|
initial assume(!i_wb_cyc);
|
initial `SLAVE_ASSUME(!i_wb_cyc);
|
initial assume(!i_wb_stb);
|
initial `SLAVE_ASSUME(!i_wb_stb);
|
//
|
//
|
initial assert(!i_wb_ack);
|
initial `SLAVE_ASSERT(!i_wb_ack);
|
initial assert(!i_wb_err);
|
initial `SLAVE_ASSERT(!i_wb_err);
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_reset)))
|
if ((!f_past_valid)||($past(i_reset)))
|
begin
|
begin
|
assume(!i_wb_cyc);
|
`SLAVE_ASSUME(!i_wb_cyc);
|
assume(!i_wb_stb);
|
`SLAVE_ASSUME(!i_wb_stb);
|
//
|
//
|
assert(!i_wb_ack);
|
`SLAVE_ASSERT(!i_wb_ack);
|
assert(!i_wb_err);
|
`SLAVE_ASSERT(!i_wb_err);
|
end
|
end
|
|
|
// Things can only change on the positive edge of the clock
|
always @(*)
|
always @($global_clock)
|
if (!f_past_valid)
|
if ((f_past_valid)&&(!$rose(i_clk)))
|
`SLAVE_ASSUME(!i_wb_cyc);
|
begin
|
|
assume($stable(i_reset));
|
|
assume($stable(i_wb_cyc));
|
|
assume($stable(f_request));
|
|
if (i_wb_we)
|
|
assume($stable(f_request)); // The entire request should b stabl
|
|
else
|
|
assume($stable(f_request[(2+AW-1):(DW+DW/8)]));
|
|
//
|
|
assert($stable(i_wb_ack));
|
|
assert($stable(i_wb_stall));
|
|
assert($stable(i_wb_idata));
|
|
assert($stable(i_wb_err));
|
|
end
|
|
|
|
//
|
//
|
//
|
//
|
// Bus requests
|
// Bus requests
|
//
|
//
|
| Line 184... |
Line 189... |
|
|
// Following any bus error, the CYC line should be dropped to abort
|
// Following any bus error, the CYC line should be dropped to abort
|
// the transaction
|
// the transaction
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
|
if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
|
assume(!i_wb_cyc);
|
`SLAVE_ASSUME(!i_wb_cyc);
|
|
|
// STB can only be true if CYC is also true
|
// STB can only be true if CYC is also true
|
always @(posedge i_clk)
|
always @(*)
|
if (i_wb_stb)
|
if (i_wb_stb)
|
assume(i_wb_cyc);
|
`SLAVE_ASSUME(i_wb_cyc);
|
|
|
// If a request was both outstanding and stalled on the last clock,
|
// If a request was both outstanding and stalled on the last clock,
|
// then nothing should change on this clock regarding it.
|
// then nothing should change on this clock regarding it.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
|
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
|
&&($past(i_wb_stall))&&(i_wb_cyc))
|
&&($past(i_wb_stall))&&(i_wb_cyc))
|
begin
|
begin
|
assume(i_wb_stb);
|
`SLAVE_ASSUME(i_wb_stb);
|
assume($stable(f_request));
|
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
|
|
`SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
|
|
`SLAVE_ASSUME(i_wb_sel == $past(i_wb_sel));
|
|
if (i_wb_we)
|
|
`SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
|
end
|
end
|
|
|
// Within any series of STB/requests, the direction of the request
|
// Within any series of STB/requests, the direction of the request
|
// may not change.
|
// may not change.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
|
if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
|
assume(i_wb_we == $past(i_wb_we));
|
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
|
|
|
|
|
// Within any given bus cycle, the direction may *only* change when
|
// Within any given bus cycle, the direction may *only* change when
|
// there are no further outstanding requests.
|
// there are no further outstanding requests.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&(f_outstanding > 0))
|
if ((f_past_valid)&&(f_outstanding > 0))
|
assume(i_wb_we == $past(i_wb_we));
|
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
|
|
|
// Write requests must also set one (or more) of i_wb_sel
|
// Write requests must also set one (or more) of i_wb_sel
|
always @(posedge i_clk)
|
// always @(*)
|
if ((i_wb_stb)&&(i_wb_we))
|
// if ((i_wb_stb)&&(i_wb_we))
|
assume(|i_wb_sel);
|
// `SLAVE_ASSUME(|i_wb_sel);
|
|
|
|
|
//
|
//
|
//
|
//
|
// Bus responses
|
// Bus responses
|
| Line 229... |
Line 238... |
//
|
//
|
|
|
// If CYC was low on the last clock, then both ACK and ERR should be
|
// If CYC was low on the last clock, then both ACK and ERR should be
|
// low on this clock.
|
// low on this clock.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&(!$past(i_wb_cyc)))
|
if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
|
begin
|
begin
|
assert(!i_wb_ack);
|
`SLAVE_ASSERT(!i_wb_ack);
|
assert(!i_wb_err);
|
`SLAVE_ASSERT(!i_wb_err);
|
// Stall may still be true--such as when we are not
|
// Stall may still be true--such as when we are not
|
// selected at some arbiter between us and the slave
|
// selected at some arbiter between us and the slave
|
end
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
|
|
begin
|
|
if (($past(f_outstanding == 0))
|
|
&&((!$past(i_wb_stb && !i_wb_stall))
|
|
||($past(i_wb_ack|i_wb_err))))
|
|
begin
|
|
`SLAVE_ASSERT(!i_wb_ack);
|
|
`SLAVE_ASSERT(!i_wb_err);
|
|
end
|
|
end
|
|
|
// ACK and ERR may never both be true at the same time
|
// ACK and ERR may never both be true at the same time
|
always @(*)
|
always @(*)
|
assume((!i_wb_ack)||(!i_wb_err));
|
`SLAVE_ASSERT((!i_wb_ack)||(!i_wb_err));
|
|
|
generate if (F_MAX_STALL > 0)
|
generate if (F_MAX_STALL > 0)
|
begin : MXSTALL
|
begin : MXSTALL
|
//
|
//
|
// Assume the slave cannnot stall for more than F_MAX_STALL
|
// Assume the slave cannnot stall for more than F_MAX_STALL
|
| Line 256... |
Line 277... |
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
|
if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
|
f_stall_count <= f_stall_count + 1'b1;
|
f_stall_count <= f_stall_count + 1'b1;
|
else
|
else
|
f_stall_count <= 0;
|
f_stall_count <= 0;
|
always @(posedge i_clk)
|
|
|
always @(*)
|
if (i_wb_cyc)
|
if (i_wb_cyc)
|
assert(f_stall_count < F_MAX_STALL);
|
`SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
|
end endgenerate
|
end endgenerate
|
|
|
generate if (F_MAX_ACK_DELAY > 0)
|
generate if (F_MAX_ACK_DELAY > 0)
|
begin : MXWAIT
|
begin : MXWAIT
|
//
|
//
|
| Line 273... |
Line 295... |
reg [(DLYBITS-1):0] f_ackwait_count;
|
reg [(DLYBITS-1):0] f_ackwait_count;
|
|
|
initial f_ackwait_count = 0;
|
initial f_ackwait_count = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
|
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
|
&&(!i_wb_ack)&&(!i_wb_err))
|
&&(!i_wb_ack)&&(!i_wb_err)
|
begin
|
&&(f_outstanding > 0))
|
f_ackwait_count <= f_ackwait_count + 1'b1;
|
f_ackwait_count <= f_ackwait_count + 1'b1;
|
assert(f_ackwait_count < F_MAX_ACK_DELAY);
|
else
|
end else
|
|
f_ackwait_count <= 0;
|
f_ackwait_count <= 0;
|
|
|
|
always @(*)
|
|
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
|
|
&&(!i_wb_ack)&&(!i_wb_err)
|
|
&&(f_outstanding > 0))
|
|
`SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
|
end endgenerate
|
end endgenerate
|
|
|
//
|
//
|
// Count the number of requests that have been received
|
// Count the number of requests that have been received
|
//
|
//
|
| Line 297... |
Line 324... |
//
|
//
|
// Count the number of acknowledgements that have been returned
|
// Count the number of acknowledgements that have been returned
|
//
|
//
|
initial f_nacks = 0;
|
initial f_nacks = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!i_wb_cyc)
|
if (i_reset)
|
|
f_nacks <= 0;
|
|
else if (!i_wb_cyc)
|
f_nacks <= 0;
|
f_nacks <= 0;
|
else if ((i_wb_ack)||(i_wb_err))
|
else if ((i_wb_ack)||(i_wb_err))
|
f_nacks <= f_nacks + 1'b1;
|
f_nacks <= f_nacks + 1'b1;
|
|
|
//
|
//
|
// The number of outstanding requests is the difference between
|
// The number of outstanding requests is the difference between
|
// the number of requests and the number of acknowledgements
|
// the number of requests and the number of acknowledgements
|
//
|
//
|
assign f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;
|
assign f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;
|
|
|
always @(posedge i_clk)
|
always @(*)
|
if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
|
if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
|
begin
|
begin
|
if (i_wb_stb)
|
if (i_wb_stb)
|
assume(f_nreqs < F_MAX_REQUESTS);
|
`SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
|
else
|
else
|
assume(f_nreqs <= F_MAX_REQUESTS);
|
`SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
|
assert(f_nacks <= f_nreqs);
|
`SLAVE_ASSERT(f_nacks <= f_nreqs);
|
assert(f_outstanding < (1<<F_LGDEPTH)-1);
|
assert(f_outstanding < (1<<F_LGDEPTH)-1);
|
end else
|
end else
|
assert(f_outstanding < (1<<F_LGDEPTH)-1);
|
assume(f_outstanding < (1<<F_LGDEPTH)-1);
|
|
|
always @(posedge i_clk)
|
always @(*)
|
if ((i_wb_cyc)&&(f_outstanding == 0))
|
if ((i_wb_cyc)&&(f_outstanding == 0))
|
begin
|
begin
|
// If nothing is outstanding, then there should be
|
// If nothing is outstanding, then there should be
|
// no acknowledgements
|
// no acknowledgements ... however, an acknowledgement
|
assert(!i_wb_ack);
|
// *can* come back on the same clock as the stb is
|
// The same is not true of errors. It may be that an
|
// going out.
|
// error is created before the request gets through
|
if (F_OPT_MINCLOCK_DELAY)
|
// assert(!i_wb_err);
|
begin
|
|
`SLAVE_ASSERT(!i_wb_ack);
|
|
`SLAVE_ASSERT(!i_wb_err);
|
|
end else begin
|
|
`SLAVE_ASSERT((!i_wb_ack)||((i_wb_stb)&&(!i_wb_stall)));
|
|
// The same is true of errors. They may not be
|
|
// created before the request gets through
|
|
`SLAVE_ASSERT((!i_wb_err)||((i_wb_stb)&&(!i_wb_stall)));
|
|
end
|
end
|
end
|
|
|
// While the error signal may be asserted immediately before
|
|
// anything is outstanding, it may only be asserted in
|
|
// response to a transaction request--whether completed or
|
|
// not.
|
|
always @(posedge i_clk)
|
|
if ((i_wb_cyc)&&(!i_wb_stb)&&(f_outstanding == 0))
|
|
assert(!i_wb_err);
|
|
|
|
generate if (!F_OPT_RMW_BUS_OPTION)
|
generate if (!F_OPT_RMW_BUS_OPTION)
|
begin
|
begin
|
// If we aren't waiting for anything, and we aren't issuing
|
// If we aren't waiting for anything, and we aren't issuing
|
// any requests, then then our transaction is over and we
|
// any requests, then then our transaction is over and we
|
// should be dropping the CYC line.
|
// should be dropping the CYC line.
|
always @(posedge i_clk)
|
always @(*)
|
if (f_outstanding == 0)
|
if (f_outstanding == 0)
|
assume((i_wb_stb)||(!i_wb_cyc));
|
`SLAVE_ASSUME((i_wb_stb)||(!i_wb_cyc));
|
// Not all masters will abide by this restriction. Some
|
// Not all masters will abide by this restriction. Some
|
// masters may wish to implement read-modify-write bus
|
// masters may wish to implement read-modify-write bus
|
// interactions. These masters need to keep CYC high between
|
// interactions. These masters need to keep CYC high between
|
// transactions, even though nothing is outstanding. For
|
// transactions, even though nothing is outstanding. For
|
// these busses, turn F_OPT_RMW_BUS_OPTION on.
|
// these busses, turn F_OPT_RMW_BUS_OPTION on.
|
| Line 366... |
Line 395... |
// However, in any RMW scheme, discontinuous requests are
|
// However, in any RMW scheme, discontinuous requests are
|
// necessary, and the spec doesn't disallow them. Hence we
|
// necessary, and the spec doesn't disallow them. Hence we
|
// make this check optional.
|
// make this check optional.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
|
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
|
assume(!i_wb_stb);
|
`SLAVE_ASSUME(!i_wb_stb);
|
end endgenerate
|
end endgenerate
|
|
|
endmodule
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
