diff options
Diffstat (limited to '')
| -rw-r--r-- | rtl/wb2axip/skidbuffer.v | 495 |
1 files changed, 495 insertions, 0 deletions
diff --git a/rtl/wb2axip/skidbuffer.v b/rtl/wb2axip/skidbuffer.v new file mode 100644 index 0000000..3d19cbb --- /dev/null +++ b/rtl/wb2axip/skidbuffer.v @@ -0,0 +1,495 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// 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 |