From 3d20f627adadeb5be724f877573030c1b030d0ef Mon Sep 17 00:00:00 2001 From: Caleb Whitehead Date: Thu, 16 May 2024 14:33:45 -0700 Subject: [PATCH] Initial pass at AXI sub -- read channel only --- src/axi/rtl/axi_addr.v | 235 ++++++++++++++++++ src/axi/rtl/axi_if.sv | 155 ++++++++++++ src/axi/rtl/axi_pkg.sv | 52 ++++ src/axi/rtl/axi_sub_rd.sv | 368 ++++++++++++++++++++++++++++ src/axi/rtl/skidbuffer.v | 495 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 1305 insertions(+) create mode 100644 src/axi/rtl/axi_addr.v create mode 100644 src/axi/rtl/axi_if.sv create mode 100644 src/axi/rtl/axi_pkg.sv create mode 100644 src/axi/rtl/axi_sub_rd.sv create mode 100644 src/axi/rtl/skidbuffer.v diff --git a/src/axi/rtl/axi_addr.v b/src/axi/rtl/axi_addr.v new file mode 100644 index 000000000..8b38874f7 --- /dev/null +++ b/src/axi/rtl/axi_addr.v @@ -0,0 +1,235 @@ +//////////////////////////////////////////////////////////////////////////////// +// +// Filename: axi_addr.v +// {{{ +// Project: WB2AXIPSP: bus bridges and other odds and ends +// +// Purpose: The AXI (full) standard has some rather complicated addressing +// modes, where the address can either be FIXED, INCRementing, or +// even where it can WRAP around some boundary. When in either INCR or +// WRAP modes, the next address must always be aligned. In WRAP mode, +// the next address calculation needs to wrap around a given value, and +// that value is dependent upon the burst size (i.e. bytes per beat) and +// length (total numbers of beats). Since this calculation can be +// non-trivial, and since it needs to be done multiple times, the logic +// below captures it for every time it might be needed. +// +// 20200918 - modified to accommodate (potential) AXI3 burst lengths +// +// 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 axi_addr #( + // {{{ + parameter AW = 32, + DW = 32, + // parameter [0:0] OPT_AXI3 = 1'b0, + localparam LENB = 8 + // }}} + ) ( + // {{{ + input wire [AW-1:0] i_last_addr, + input wire [2:0] i_size, // 1b, 2b, 4b, 8b, etc + input wire [1:0] i_burst, // fixed, incr, wrap, reserved + input wire [LENB-1:0] i_len, + output wire [AW-1:0] o_next_addr + // }}} + ); + + // Parameter/register declarations + // {{{ + localparam DSZ = $clog2(DW)-3; + localparam [1:0] FIXED = 2'b00; + // localparam [1:0] INCREMENT = 2'b01; + // localparam [1:0] WRAP = 2'b10; + localparam IN_AW = (AW >= 12) ? 12 : AW; + localparam [IN_AW-1:0] ONE = 1; + + reg [IN_AW-1:0] wrap_mask, increment; + reg [IN_AW-1:0] crossblk_addr, aligned_addr, unaligned_addr; + // }}} + + // Address increment + // {{{ + always @(*) + if (DSZ == 0) + increment = 1; + else if (DSZ == 1) + increment = (i_size[0]) ? 2 : 1; + else if (DSZ == 2) + increment = (i_size[1]) ? 4 : ((i_size[0]) ? 2 : 1); + else if (DSZ == 3) + case(i_size[1:0]) + 2'b00: increment = 1; + 2'b01: increment = 2; + 2'b10: increment = 4; + 2'b11: increment = 8; + endcase + else + increment = (1<1) ? 1 : (AW-1):0]= 0; + 2'b11: aligned_addr[(AW-1>2) ? 2 : (AW-1):0]= 0; + endcase + // }}} + end else begin + // {{{ + // Align any subsequent address + case(i_size) + 3'b001: aligned_addr[ 0] = 0; + 3'b010: aligned_addr[(AW-1>1) ? 1 : (AW-1):0]=0; + 3'b011: aligned_addr[(AW-1>2) ? 2 : (AW-1):0]=0; + 3'b100: aligned_addr[(AW-1>3) ? 3 : (AW-1):0]=0; + 3'b101: aligned_addr[(AW-1>4) ? 4 : (AW-1):0]=0; + 3'b110: aligned_addr[(AW-1>5) ? 5 : (AW-1):0]=0; + 3'b111: aligned_addr[(AW-1>6) ? 6 : (AW-1):0]=0; + default: aligned_addr = unaligned_addr; + endcase + // }}} + end + // }}} + end else + aligned_addr = i_last_addr[IN_AW-1:0]; + // }}} + + // crossblk_addr from aligned_addr, for WRAP addressing + // {{{ + always @(*) + if (i_burst[1]) + begin + // WRAP! + crossblk_addr[IN_AW-1:0] = (i_last_addr[IN_AW-1:0] & ~wrap_mask) + | (aligned_addr & wrap_mask); + end else + crossblk_addr[IN_AW-1:0] = aligned_addr; + // }}} + + // o_next_addr: Guarantee only the bottom 12 bits change + // {{{ + // This is really a logic simplification. AXI bursts aren't allowed + // to cross 4kB boundaries. Given that's the case, we don't have to + // suffer from the propagation across all AW bits, and can limit any + // address propagation to just the lower 12 bits + generate if (AW > 12) + begin : WIDE_ADDRESS + assign o_next_addr = { i_last_addr[AW-1:12], + crossblk_addr[11:0] }; + end else begin : NARROW_ADDRESS + assign o_next_addr = crossblk_addr[AW-1:0]; + end endgenerate + // }}} + + // Make Verilator happy + // {{{ + // Verilator lint_off UNUSED + wire unused; + assign unused = (LENB <= 4) ? &{1'b0, i_len[0] } + : &{ 1'b0, i_len[LENB-1:4], i_len[0] }; + // Verilator lint_on UNUSED + // }}} +endmodule diff --git a/src/axi/rtl/axi_if.sv b/src/axi/rtl/axi_if.sv new file mode 100644 index 000000000..3f4662788 --- /dev/null +++ b/src/axi/rtl/axi_if.sv @@ -0,0 +1,155 @@ +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use 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. +// +// Description: +// Signals for a standard AXI4 compliant interface +// + +interface axi_if #(parameter AW = 32, parameter DW = 32, parameter IW = 3, parameter UW = 32); + + import axi_pkg::*; + + // AXI AR + logic [AW-1:0] araddr; + logic [1:0] arburst; + logic [2:0] arsize; + logic [7:0] arlen; + logic [UW-1:0] aruser; + logic [IW-1:0] arid; + logic arlock; + logic arvalid; + logic arready; + + // AXI R + logic [DW-1:0] rdata; + logic [1:0] rresp; + logic [IW-1:0] rid; + logic rlast; + logic rvalid; + logic rready; + + // AXI AW + logic [AW-1:0] awaddr; + logic [1:0] awburst; + logic [2:0] awsize; + logic [7:0] awlen; + logic [UW-1:0] awuser; + logic [IW-1:0] awid; + logic awlock; + logic awvalid; + logic awready; + + // AXI W + logic [DW-1:0] wdata; + logic [DW/8-1:0] wstrb; + logic wvalid; + logic wready; + + // AXI B + logic [1:0] bresp; + logic [IW-1:0] bid; + logic bvalid; + logic bready; + + // Modport for read manager + modport r_mgr ( + // AR + output araddr, + output arburst, + output arsize, + output arlen, + output aruser, + output arid, + output arlock, + output arvalid, + input arready, + // R + input rdata, + input rresp, + input rid, + input rlast, + input rvalid, + output rready, + ); + + // Modport for write manager + modport w_mgr ( + // AW + output awaddr, + output awburst, + output awsize, + output awlen, + output awuser, + output awid, + output awlock, + output awvalid, + input awready, + // W + output wdata, + output wstrb, + output wvalid, + input wready, + // B + input bresp, + input bid, + input bvalid, + output bready + ); + + // Modport for read subordinate + modport r_sub ( + // AR + input araddr, + input arburst, + input arsize, + input arlen, + input aruser, + input arid, + input arlock, + input arvalid, + output arready, + // R + output rdata, + output rresp, + output rid, + output rlast, + output rvalid, + input rready, + ); + + // Modport for write subordinate + modport w_sub ( + // AW + input awaddr, + input awburst, + input awsize, + input awlen, + input awuser, + input awid, + input awlock, + input awvalid, + output awready, + // W + input wdata, + input wstrb, + input wvalid, + output wready, + // B + output bresp, + output bid, + output bvalid, + input bready + ); + +endinterface diff --git a/src/axi/rtl/axi_pkg.sv b/src/axi/rtl/axi_pkg.sv new file mode 100644 index 000000000..36346f00d --- /dev/null +++ b/src/axi/rtl/axi_pkg.sv @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use 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. +// + +package axi_pkg; + + // AXI Burst Enum + typedef enum logic [1:0] { + AXI_BURST_FIXED = 2'b00, + AXI_BURST_INCR = 2'b01, + AXI_BURST_WRAP = 2'b10, + AXI_BURST_RESERVED = 2'b11 + } axi_burst_e; + + // AXI Resp Enum + typedef enum logic [1:0] { + AXI_RESP_OKAY = 2'b00, + AXI_RESP_EXOKAY = 2'b01, + AXI_RESP_SLVERR = 2'b10, + AXI_RESP_DECERR = 2'b11 + } axi_resp_e; + + // Transaction context + typedef struct packed { + logic [AW-1:0] addr; + logic [1:0] burst; + logic [2:0] size; + logic [7:0] len; + logic [UW-1:0] user; + logic [IW-1:0] id; + logic lock; + } axi_ctx_t; + + typedef struct packed { + logic [IW-1:0] id; + logic [UW-1:0] user; + logic [ 1:0] resp; + logic last; + } xfer_ctx_t; + +endpackage diff --git a/src/axi/rtl/axi_sub_rd.sv b/src/axi/rtl/axi_sub_rd.sv new file mode 100644 index 000000000..186cf7bef --- /dev/null +++ b/src/axi/rtl/axi_sub_rd.sv @@ -0,0 +1,368 @@ +// SPDX-License-Identifier: Apache-2.0 +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use 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. +// + +// ------------------------------------------------------------- +// AXI Read Subordinate +// ------------------------------------------------------------- +// Description: +// Subordinate to convert AXI protocol reads into internal component accesses +// +// Limitations: +// - When multiple ID tracking is enabled, read responses are returned in the +// same order they are received, regardless of ID. +// +// ------------------------------------------------------------- + +module axi_sub_rd import axi_pkg::*; #( + parameter AW = 32, // Address Width + parameter DW = 32, // Data Width + BC = DW/8, // Byte Count + BW = $clog2(BC), // Byte count Width + parameter UW = 32, // User Width + parameter IW = 1, // ID Width + ID_NUM = 1 << IW, // Don't override + + parameter EX_EN = 1, // Enable exclusive access tracking w/ AxLOCK + parameter C_LAT = 0 // Component latency in clock cycles from (dv&&!hld) -> rdata + // Must be const per component + // For registers, typically 0 + // For SRAM, 1 or more +) ( + input clk, + input rst_n, + + // AXI INF + axi_if.r_sub s_axi_if, + + // Exclusive Access Signals + input logic ex_clr, + input logic [IW -1:0] ex_clr_id, + output logic [ID_NUM-1:0] ex_active, + output var axi_ctx_t [ID_NUM-1:0] ex_ctx, + + //COMPONENT INF + output logic dv, + output logic [AW-1:0] addr, // Byte address + output logic [UW-1:0] user, + output logic last, // Asserted with final 'dv' of a burst + input logic hld, + input logic err, + + input logic [DW-1:0] rdata // Integ requires: Component dwidth == AXI dwidth +); + + // --------------------------------------- // + // Localparams/Typedefs // + // --------------------------------------- // + + + // --------------------------------------- // + // Signals // + // --------------------------------------- // + + genvar cp; // Context pipeline + genvar dp; // Data pipeline + genvar ex; // Exclusive contexts + + // Active transaction signals + // track requests as they are sent to component + axi_ctx_t txn_ctx; + logic [AW-1:0] txn_addr_nxt; + logic [ 7:0] txn_cnt; // Internal down-counter to track txn progress + logic txn_active; + logic [C_LAT:0] txn_rvalid; + xfer_ctx_t [C_LAT:0] txn_xfer_ctx; + logic txn_final_beat; + + // Data pipeline signals (skid buffer) + // track data after it is received from component + logic [C_LAT+1:0] [DW-1:0] dp_rdata; + xfer_ctx_t [C_LAT+1:0] dp_xfer_ctx; + logic [C_LAT+1:0] dp_rvalid; + logic [C_LAT+1:0] dp_rready; + + + // --------------------------------------- // + // Address Request I/F // + // --------------------------------------- // + + assign s_axi_if.arready = !txn_active || txn_final_beat; + + // Indicates there are still reqs to be issued towards component. + // This active signal deasserts after final dv to component, meaning data is + // still in flight from component->AXI for C_LAT clocks after deassertion + always@(posedge clk or negedge rst_n) begin + if (!rst_n) begin + txn_active <= 1'b0; + end + else if (s_axi_if.arvalid) begin + txn_active <= 1'b1; + end + else if (txn_final_beat) begin + txn_active <= 1'b0; + end + else begin + txn_active <= txn_active; + end + end + + // TODO reset? + always@(posedge clk/* or negedge rst_n*/) begin +// if (!rst_n) begin +// txn_ctx <= '{default:0}; +// end + else if (s_axi_if.arvalid && s_axi_if.arready) begin + txn_ctx.addr <= s_axi_if.araddr; + txn_ctx.burst <= s_axi_if.arburst; + txn_ctx.size <= s_axi_if.arsize; + txn_ctx.len <= s_axi_if.arlen ; + txn_ctx.user <= s_axi_if.aruser; + txn_ctx.id <= s_axi_if.arid ; + txn_ctx.lock <= s_axi_if.arlock; + txn_cnt <= s_axi_if.arlen ; + end + else if (txn_rvalid[0]) begin + txn_ctx.addr <= txn_addr_nxt; + txn_ctx.burst <= s_axi_if.arburst; + txn_ctx.size <= s_axi_if.arsize; + txn_ctx.len <= s_axi_if.arlen ; + txn_ctx.user <= s_axi_if.aruser; + txn_ctx.id <= s_axi_if.arid ; + txn_ctx.lock <= s_axi_if.arlock; + txn_cnt <= |txn_cnt ? txn_cnt - 1 : txn_cnt; // Prevent underflow to 255 at end to reduce switching power. Extra logic cost worth it? + end + else begin + txn_ctx <= txn_ctx; + end + end + + // Only make the request to component if we have space in the pipeline to + // store the result (under worst-case AXI backpressure) + // To check this, look at the 'ready' output from the FINAL stage of the + // skidbuffer pipeline + always_comb dv = txn_active && dp_rready[C_LAT]; + always_comb txn_rvalid[0] = dv && !hld; + + // Asserts on the final beat of the COMPONENT INF which means it lags the + // final AXI beat by at least C_LAT clocks (or more depending on backpressure) + always_comb txn_final_beat = txn_rvalid[0] && txn_xfer_ctx[0].last; + + + // --------------------------------------- // + // Address Calculations // + // --------------------------------------- // + // Force aligned address to component + always_comb addr = {txn_ctx.addr[AW-1:BW],BW'(0)}; + + // Use full address to calculate next address (in case of arsize < data width) + axi_addr #( + .AW (AW), + .DW (DW), + .LENB(8 ) + ) i_axi_addr ( + .i_last_addr(txn_ctx.addr ), + .i_size (txn_ctx.size ), // 1b, 2b, 4b, 8b, etc + .i_burst (txn_ctx.burst), // fixed, incr, wrap, reserved + .i_len (txn_ctx.len ), + .o_next_addr(txn_addr_nxt ) + ); + + + // --------------------------------------- // + // Request Context Pipeline // + // --------------------------------------- // + always_comb begin + txn_xfer_ctx[0].id = txn_ctx.id; + txn_xfer_ctx[0].user = txn_ctx.user; + txn_xfer_ctx[0].last = txn_cnt == 0; + txn_xfer_ctx[0].resp = (EX_EN && txn_ctx.lock && /*FIXME*/) ? AXI_RESP_EXOKAY : AXI_RESP_OKAY; + end + + // Shift Register to track requests made to component + generate + if (C_LAT > 0) begin: TXN_SR + always@(posedge clk or negedge rst_n) begin + if (!rst_n) begin + txn_rvalid[C_LAT:1] <= C_LAT'(0); + end + else begin + txn_rvalid[C_LAT:1] <= txn_rvalid[C_LAT-1:0]; + end + end + + // Context is maintained alongside request while waiting for + // component response to arrive + if (C_LAT > 1) begin + for (cp = 1; cp <= C_LAT; cp++) begin: CTX_PIPELINE + // No reset needed on data path -- txn_rvalid (control path) is reset + always@(posedge clk) begin + txn_xfer_ctx[cp] <= txn_xfer_ctx[cp-1]; + end + end: CTX_PIPELINE + end + + end: TXN_SR + endgenerate + + + // --------------------------------------- // + // Exclusive Access Tracking // + // --------------------------------------- // + generate + if (EX_EN) begin: EX_AXS_TRACKER + always@(posedge clk or negedge rst_n) begin + if (!rst_n) begin + ex_active <= '0; + end + // give 'set' precedence over 'clr' in case of same ID + else if ((txn_rvalid[0] && txn_ctx.lock) && ex_clr) begin + ex_active <= (ex_active & ~(1 << ex_clr_id)) | (1 << txn_ctx.id); + end + else if (txn_rvalid[0] && txn_ctx.lock) begin + ex_active <= ex_active; + end + else if (ex_clr) begin + ex_active <= ex_active & ~(1 << ex_clr_id); + end + else begin + ex_active <= ex_active; + end + end + + for (ex = 0; ex < ID_NUM; ex++) begin: EX_CTX_TRACKER + // TODO: reset? + always@(posedge clk) begin + if (txn_rvalid[0] && txn_ctx.lock && (txn_ctx.id == ex)) begin + ex_ctx[ex] <= txn_ctx; + end + // Ignore the clear case, as ex_active is ctrl path + //else if (ex_clr && (ex_clr_id == ex)) begin + //end + else begin + ex_ctx[ex] <= ex_ctx[ex]; + end + end + end + end: EX_AXS_TRACKER + else begin: EX_UNSUPPORTED + for (ex = 0; ex < ID_NUM; ex++) begin: EX_SIG_0 + always_comb begin + ex_active[ex] = 1'b0; + ex_ctx[ex] = '{default:0}; + end + end: EX_SIG_0 + end: EX_UNSUPPORTED + endgenerate + + + // --------------------------------------- // + // Data/Response // + // --------------------------------------- // + always_comb dp_rvalid[0] = txn_rvalid[C_LAT]; + always_comb dp_rdata[0] = rdata; + always_comb begin + dp_xfer_ctx[0].id = txn_xfer_ctx[C_LAT].id; + dp_xfer_ctx[0].user = txn_xfer_ctx[C_LAT].user; // NOTE: Unused after it enters data pipeline + dp_xfer_ctx[0].resp = err ? AXI_RESP_SLVERR : + EX_EN ? txn_xfer_ctx[C_LAT].resp : + AXI_RESP_OKAY; + dp_xfer_ctx[0].last = txn_xfer_ctx[C_LAT].last; + end + + generate + for (dp = 0; dp <= C_LAT; dp++) begin: DATA_PIPELINE + // skidbuffer instance to pipeline data payload + context to AXI, + // after response is received from component. + // This is necessary when there is latency from dv->rdata, + // because AXI R channel can be stalled by dropping rready, + // and we can't drop the data (which was requested N cycles ago) + skidbuffer #( + .OPT_LOWPOWER (0 ), + .OPT_OUTREG (0 ), + // + .OPT_PASSTHROUGH(0 ), + .DW (DW + $bits(xfer_ctx_t)), + .OPT_INITIAL (1'b1) + ) i_dp_skd ( + .i_clk (clk ), + .i_reset(!rst_n ), + .i_valid(dp_rvalid[dp] ), + .o_ready(dp_rready[dp] ), + .i_data ({dp_rdata[dp] + dp_xfer_ctx[dp]} ), + .o_valid(dp_rvalid[dp+1] ), + .i_ready(dp_rready[dp+1] ), + .o_data ({dp_rdata[dp+1], + dp_xfer_ctx[dp+1]}) + ); + + end: DATA_PIPELINE + endgenerate + + always_comb dp_rready[C_LAT+1] = s_axi_if.rready; + always_comb begin + s_axi_if.rvalid = dp_rvalid[C_LAT+1]; + s_axi_if.rdata = dp_rdata[C_LAT+1]; + s_axi_if.rid = dp_xfer_ctx[C_LAT+1].id; + s_axi_if.rresp = dp_xfer_ctx[C_LAT+1].resp; + end + + + // --------------------------------------- // + // Formal Properties // + // --------------------------------------- // + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARADDR , s_axi_if.araddr , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARBURST, s_axi_if.arburst, clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARSIZE , s_axi_if.arsize , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARLEN , s_axi_if.arlen , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARUSER , s_axi_if.aruser , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARID , s_axi_if.arid , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARLOCK , s_axi_if.arlock , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARVALID, s_axi_if.arvalid, clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_ARREADY, s_axi_if.arready, clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RDATA , s_axi_if.rdata , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RRESP , s_axi_if.rresp , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RID , s_axi_if.rid , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RLAST , s_axi_if.rlast , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RVALID , s_axi_if.rvalid , clk, !rst_n) + `CALIPTRA_ASSERT_KNOWN(AXI_SUB_X_RREADY , s_axi_if.rready , clk, !rst_n) + + `CALIPTRA_ASSERT_NEVER(ERR_AXI_RD_DROP , dp_rvalid[0] && !dp_rready[0], clk, !rst_n) + `CALIPTRA_ASSERT_NEVER(ERR_AXI_RD_X , dp_rvalid[0] && !$isunknown({dp_rdata[0],dp_xfer_ctx[0]}), clk, !rst_n) + // Exclusive access rules: + // - Must have an address that is aligned to burst byte count + // - Byte count must be power of 2 inside 1:128 + // - Max burst length = 16 + `CALIPTRA_ASSERT (ERR_AXI_EX_UNALGN , (s_axi_if.arvalid && s_axi_if.arlock) -> ~|s_axi_if.araddr[$clog2((1< ((1< (s_axi_if.arlen < 16), clk, !rst_n) + + genvar sva_ii; + generate + if (C_LAT > 0) begin + for (sva_ii = 0; sva_ii < C_LAT; sva_ii++) begin + // Last stage should be first to fill and last to go empty + `CALIPTRA_ASSERT_NEVER(ERR_RD_SKD_BUF, dp_rready[sva_ii+1] && !dp_rready[sva_ii], clk, !rst_n) + end + end + endgenerate + + + // --------------------------------------- // + // Coverage // + // --------------------------------------- // + + +endmodule diff --git a/src/axi/rtl/skidbuffer.v b/src/axi/rtl/skidbuffer.v new file mode 100644 index 000000000..e6b1a62a2 --- /dev/null +++ b/src/axi/rtl/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