496 lines
12 KiB
Verilog
496 lines
12 KiB
Verilog
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Filename: skidbuffer.v
|
|
// {{{
|
|
// Project: WB2AXIPSP: bus bridges and other odds and ends
|
|
//
|
|
// Purpose: A basic SKID buffer.
|
|
// {{{
|
|
// Skid buffers are required for high throughput AXI code, since the AXI
|
|
// specification requires that all outputs be registered. This means
|
|
// that, if there are any stall conditions calculated, it will take a clock
|
|
// cycle before the stall can be propagated up stream. This means that
|
|
// the data will need to be buffered for a cycle until the stall signal
|
|
// can make it to the output.
|
|
//
|
|
// Handling that buffer is the purpose of this core.
|
|
//
|
|
// On one end of this core, you have the i_valid and i_data inputs to
|
|
// connect to your bus interface. There's also a registered o_ready
|
|
// signal to signal stalls for the bus interface.
|
|
//
|
|
// The other end of the core has the same basic interface, but it isn't
|
|
// registered. This allows you to interact with the bus interfaces
|
|
// as though they were combinatorial logic, by interacting with this half
|
|
// of the core.
|
|
//
|
|
// If at any time the incoming !stall signal, i_ready, signals a stall,
|
|
// the incoming data is placed into a buffer. Internally, that buffer
|
|
// is held in r_data with the r_valid flag used to indicate that valid
|
|
// data is within it.
|
|
// }}}
|
|
// Parameters:
|
|
// {{{
|
|
// DW or data width
|
|
// In order to make this core generic, the width of the data in the
|
|
// skid buffer is parameterized
|
|
//
|
|
// OPT_LOWPOWER
|
|
// Forces both o_data and r_data to zero if the respective *VALID
|
|
// signal is also low. While this costs extra logic, it can also
|
|
// be used to guarantee that any unused values aren't toggling and
|
|
// therefore unnecessarily using power.
|
|
//
|
|
// This excess toggling can be particularly problematic if the
|
|
// bus signals have a high fanout rate, or a long signal path
|
|
// across an FPGA.
|
|
//
|
|
// OPT_OUTREG
|
|
// Causes the outputs to be registered
|
|
//
|
|
// OPT_PASSTHROUGH
|
|
// Turns the skid buffer into a passthrough. Used for formal
|
|
// verification only.
|
|
// }}}
|
|
// Creator: Dan Gisselquist, Ph.D.
|
|
// Gisselquist Technology, LLC
|
|
//
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
// }}}
|
|
// Copyright (C) 2019-2024, Gisselquist Technology, LLC
|
|
// {{{
|
|
// This file is part of the WB2AXIP project.
|
|
//
|
|
// The WB2AXIP project contains free software and gateware, licensed under the
|
|
// Apache License, Version 2.0 (the "License"). You may not use this project,
|
|
// or this file, except in compliance with the License. You may obtain a copy
|
|
// of the License at
|
|
//
|
|
// http://www.apache.org/licenses/LICENSE-2.0
|
|
//
|
|
// Unless required by applicable law or agreed to in writing, software
|
|
// distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
|
|
// WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
|
|
// License for the specific language governing permissions and limitations
|
|
// under the License.
|
|
//
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
`default_nettype none
|
|
// }}}
|
|
module skidbuffer #(
|
|
// {{{
|
|
parameter [0:0] OPT_LOWPOWER = 0,
|
|
parameter [0:0] OPT_OUTREG = 1,
|
|
//
|
|
parameter [0:0] OPT_PASSTHROUGH = 0,
|
|
parameter DW = 8,
|
|
parameter [0:0] OPT_INITIAL = 1'b1
|
|
// }}}
|
|
) (
|
|
// {{{
|
|
input wire i_clk, i_reset,
|
|
input wire i_valid,
|
|
output wire o_ready,
|
|
input wire [DW-1:0] i_data,
|
|
output wire o_valid,
|
|
input wire i_ready,
|
|
output reg [DW-1:0] o_data
|
|
// }}}
|
|
);
|
|
|
|
wire [DW-1:0] w_data;
|
|
|
|
generate if (OPT_PASSTHROUGH)
|
|
begin : PASSTHROUGH
|
|
// {{{
|
|
assign { o_valid, o_ready } = { i_valid, i_ready };
|
|
|
|
always @(*)
|
|
if (!i_valid && OPT_LOWPOWER)
|
|
o_data = 0;
|
|
else
|
|
o_data = i_data;
|
|
|
|
assign w_data = 0;
|
|
|
|
// Keep Verilator happy
|
|
// Verilator lint_off UNUSED
|
|
// {{{
|
|
wire unused_passthrough;
|
|
assign unused_passthrough = &{ 1'b0, i_clk, i_reset };
|
|
// }}}
|
|
// Verilator lint_on UNUSED
|
|
// }}}
|
|
end else begin : LOGIC
|
|
// We'll start with skid buffer itself
|
|
// {{{
|
|
reg r_valid;
|
|
reg [DW-1:0] r_data;
|
|
|
|
// r_valid
|
|
// {{{
|
|
initial if (OPT_INITIAL) r_valid = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
r_valid <= 0;
|
|
else if ((i_valid && o_ready) && (o_valid && !i_ready))
|
|
// We have incoming data, but the output is stalled
|
|
r_valid <= 1;
|
|
else if (i_ready)
|
|
r_valid <= 0;
|
|
// }}}
|
|
|
|
// r_data
|
|
// {{{
|
|
initial if (OPT_INITIAL) r_data = 0;
|
|
always @(posedge i_clk)
|
|
if (OPT_LOWPOWER && i_reset)
|
|
r_data <= 0;
|
|
else if (OPT_LOWPOWER && (!o_valid || i_ready))
|
|
r_data <= 0;
|
|
else if ((!OPT_LOWPOWER || !OPT_OUTREG || i_valid) && o_ready)
|
|
r_data <= i_data;
|
|
|
|
assign w_data = r_data;
|
|
// }}}
|
|
|
|
// o_ready
|
|
// {{{
|
|
assign o_ready = !r_valid;
|
|
// }}}
|
|
|
|
//
|
|
// And then move on to the output port
|
|
//
|
|
if (!OPT_OUTREG)
|
|
begin : NET_OUTPUT
|
|
// Outputs are combinatorially determined from inputs
|
|
// {{{
|
|
// o_valid
|
|
// {{{
|
|
assign o_valid = !i_reset && (i_valid || r_valid);
|
|
// }}}
|
|
|
|
// o_data
|
|
// {{{
|
|
always @(*)
|
|
if (r_valid)
|
|
o_data = r_data;
|
|
else if (!OPT_LOWPOWER || i_valid)
|
|
o_data = i_data;
|
|
else
|
|
o_data = 0;
|
|
// }}}
|
|
// }}}
|
|
end else begin : REG_OUTPUT
|
|
// Register our outputs
|
|
// {{{
|
|
// o_valid
|
|
// {{{
|
|
reg ro_valid;
|
|
|
|
initial if (OPT_INITIAL) ro_valid = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
ro_valid <= 0;
|
|
else if (!o_valid || i_ready)
|
|
ro_valid <= (i_valid || r_valid);
|
|
|
|
assign o_valid = ro_valid;
|
|
// }}}
|
|
|
|
// o_data
|
|
// {{{
|
|
initial if (OPT_INITIAL) o_data = 0;
|
|
always @(posedge i_clk)
|
|
if (OPT_LOWPOWER && i_reset)
|
|
o_data <= 0;
|
|
else if (!o_valid || i_ready)
|
|
begin
|
|
|
|
if (r_valid)
|
|
o_data <= r_data;
|
|
else if (!OPT_LOWPOWER || i_valid)
|
|
o_data <= i_data;
|
|
else
|
|
o_data <= 0;
|
|
end
|
|
// }}}
|
|
|
|
// }}}
|
|
end
|
|
// }}}
|
|
end endgenerate
|
|
|
|
// Keep Verilator happy
|
|
// {{{
|
|
// Verilator lint_off UNUSED
|
|
wire unused;
|
|
assign unused = &{ 1'b0, w_data };
|
|
// Verilator lint_on UNUSED
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Formal properties
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
////////////////////////////////////////////////////////////////////////////////
|
|
`ifdef FORMAL
|
|
`ifdef SKIDBUFFER
|
|
`define ASSUME assume
|
|
`else
|
|
`define ASSUME assert
|
|
`endif
|
|
|
|
reg f_past_valid;
|
|
|
|
initial f_past_valid = 0;
|
|
always @(posedge i_clk)
|
|
f_past_valid <= 1;
|
|
|
|
always @(*)
|
|
if (!f_past_valid)
|
|
assume(i_reset);
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Incoming stream properties / assumptions
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
always @(posedge i_clk)
|
|
if (!f_past_valid)
|
|
begin
|
|
`ASSUME(!i_valid || !OPT_INITIAL);
|
|
end else if ($past(i_valid && !o_ready && !i_reset) && !i_reset)
|
|
`ASSUME(i_valid && $stable(i_data));
|
|
|
|
`ifdef VERIFIC
|
|
`define FORMAL_VERIFIC
|
|
// Reset properties
|
|
property RESET_CLEARS_IVALID;
|
|
@(posedge i_clk) i_reset |=> !i_valid;
|
|
endproperty
|
|
|
|
property IDATA_HELD_WHEN_NOT_READY;
|
|
@(posedge i_clk) disable iff (i_reset)
|
|
i_valid && !o_ready |=> i_valid && $stable(i_data);
|
|
endproperty
|
|
|
|
`ifdef SKIDBUFFER
|
|
assume property (IDATA_HELD_WHEN_NOT_READY);
|
|
`else
|
|
assert property (IDATA_HELD_WHEN_NOT_READY);
|
|
`endif
|
|
`endif
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Outgoing stream properties / assumptions
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
|
|
generate if (!OPT_PASSTHROUGH)
|
|
begin
|
|
|
|
always @(posedge i_clk)
|
|
if (!f_past_valid) // || $past(i_reset))
|
|
begin
|
|
// Following any reset, valid must be deasserted
|
|
assert(!o_valid || !OPT_INITIAL);
|
|
end else if ($past(o_valid && !i_ready && !i_reset) && !i_reset)
|
|
// Following any stall, valid must remain high and
|
|
// data must be preserved
|
|
assert(o_valid && $stable(o_data));
|
|
|
|
end endgenerate
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Other properties
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
generate if (!OPT_PASSTHROUGH)
|
|
begin
|
|
// Rule #1:
|
|
// If registered, then following any reset we should be
|
|
// ready for a new request
|
|
// {{{
|
|
always @(posedge i_clk)
|
|
if (f_past_valid && $past(OPT_OUTREG && i_reset))
|
|
assert(o_ready);
|
|
// }}}
|
|
|
|
// Rule #2:
|
|
// All incoming data must either go directly to the
|
|
// output port, or into the skid buffer
|
|
// {{{
|
|
`ifndef VERIFIC
|
|
always @(posedge i_clk)
|
|
if (f_past_valid && !$past(i_reset) && $past(i_valid && o_ready
|
|
&& (!OPT_OUTREG || o_valid) && !i_ready))
|
|
assert(!o_ready && w_data == $past(i_data));
|
|
`else
|
|
assert property (@(posedge i_clk)
|
|
disable iff (i_reset)
|
|
(i_valid && o_ready
|
|
&& (!OPT_OUTREG || o_valid) && !i_ready)
|
|
|=> (!o_ready && w_data == $past(i_data)));
|
|
`endif
|
|
// }}}
|
|
|
|
// Rule #3:
|
|
// After the last transaction, o_valid should become idle
|
|
// {{{
|
|
if (!OPT_OUTREG)
|
|
begin
|
|
// {{{
|
|
always @(posedge i_clk)
|
|
if (f_past_valid && !$past(i_reset) && !i_reset
|
|
&& $past(i_ready))
|
|
begin
|
|
assert(o_valid == i_valid);
|
|
assert(!i_valid || (o_data == i_data));
|
|
end
|
|
// }}}
|
|
end else begin
|
|
// {{{
|
|
always @(posedge i_clk)
|
|
if (f_past_valid && !$past(i_reset))
|
|
begin
|
|
if ($past(i_valid && o_ready))
|
|
assert(o_valid);
|
|
|
|
if ($past(!i_valid && o_ready && i_ready))
|
|
assert(!o_valid);
|
|
end
|
|
// }}}
|
|
end
|
|
// }}}
|
|
|
|
// Rule #4
|
|
// Same thing, but this time for o_ready
|
|
// {{{
|
|
always @(posedge i_clk)
|
|
if (f_past_valid && $past(!o_ready && i_ready))
|
|
assert(o_ready);
|
|
// }}}
|
|
|
|
// If OPT_LOWPOWER is set, o_data and w_data both need to be
|
|
// zero any time !o_valid or !r_valid respectively
|
|
// {{{
|
|
if (OPT_LOWPOWER)
|
|
begin
|
|
always @(*)
|
|
if ((OPT_OUTREG || !i_reset) && !o_valid)
|
|
assert(o_data == 0);
|
|
|
|
always @(*)
|
|
if (o_ready)
|
|
assert(w_data == 0);
|
|
|
|
end
|
|
// }}}
|
|
end endgenerate
|
|
// }}}
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
// Cover checks
|
|
// {{{
|
|
////////////////////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
`ifdef SKIDBUFFER
|
|
generate if (!OPT_PASSTHROUGH)
|
|
begin
|
|
reg f_changed_data;
|
|
|
|
initial f_changed_data = 0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
f_changed_data <= 1;
|
|
else if (i_valid && $past(!i_valid || o_ready))
|
|
begin
|
|
if (i_data != $past(i_data + 1))
|
|
f_changed_data <= 0;
|
|
end else if (!i_valid && i_data != 0)
|
|
f_changed_data <= 0;
|
|
|
|
|
|
`ifndef VERIFIC
|
|
reg [3:0] cvr_steps, cvr_hold;
|
|
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
begin
|
|
cvr_steps <= 0;
|
|
cvr_hold <= 0;
|
|
end else begin
|
|
cvr_steps <= cvr_steps + 1;
|
|
cvr_hold <= cvr_hold + 1;
|
|
case(cvr_steps)
|
|
0: if (o_valid || i_valid)
|
|
cvr_steps <= 0;
|
|
1: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
2: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
3: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
4: if (!i_valid || i_ready)
|
|
cvr_steps <= 0;
|
|
5: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
6: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
7: if (!i_valid || i_ready)
|
|
cvr_steps <= 0;
|
|
8: if (!i_valid || i_ready)
|
|
cvr_steps <= 0;
|
|
9: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
10: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
11: if (!i_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
12: begin
|
|
cvr_steps <= cvr_steps;
|
|
cover(!o_valid && !i_valid && f_changed_data);
|
|
if (!o_valid || !i_ready)
|
|
cvr_steps <= 0;
|
|
else
|
|
cvr_hold <= cvr_hold + 1;
|
|
end
|
|
default: assert(0);
|
|
endcase
|
|
end
|
|
|
|
`else
|
|
// Cover test
|
|
cover property (@(posedge i_clk)
|
|
disable iff (i_reset)
|
|
(!o_valid && !i_valid)
|
|
##1 i_valid && i_ready [*3]
|
|
##1 i_valid && !i_ready
|
|
##1 i_valid && i_ready [*2]
|
|
##1 i_valid && !i_ready [*2]
|
|
##1 i_valid && i_ready [*3]
|
|
// Wait for the design to clear
|
|
##1 o_valid && i_ready [*0:5]
|
|
##1 (!o_valid && !i_valid && f_changed_data));
|
|
`endif
|
|
end endgenerate
|
|
`endif // SKIDBUFFER
|
|
// }}}
|
|
`endif
|
|
// }}}
|
|
endmodule
|