diff options
Diffstat (limited to 'rtl/wb2axip/axilsafety.v')
| -rw-r--r-- | rtl/wb2axip/axilsafety.v | 1449 |
1 files changed, 0 insertions, 1449 deletions
diff --git a/rtl/wb2axip/axilsafety.v b/rtl/wb2axip/axilsafety.v deleted file mode 100644 index ff8b391..0000000 --- a/rtl/wb2axip/axilsafety.v +++ /dev/null @@ -1,1449 +0,0 @@ -//////////////////////////////////////////////////////////////////////////////// -// -// Filename: axilsafety.v -// {{{ -// Project: WB2AXIPSP: bus bridges and other odds and ends -// -// Purpose: A AXI-Lite bus fault isolator. This core will isolate any -// downstream AXI-liite slave faults from the upstream channel. -// It sits as a bump in the wire between upstream and downstream channels, -// and so it will consume two clocks--slowing down the slave, but -// potentially allowing developer to recover in case of a fault. -// -// This core is configured by a couple parameters, which are key to its -// functionality. -// -// OPT_TIMEOUT Set this to a number to be roughly the longest time -// period you expect the slave to stall the bus, or likewise -// the longest time period you expect it to wait for a response. -// If the slave takes longer for either task, a fault will be -// detected and reported. -// -// OPT_SELF_RESET If set, this will send a reset signal to the downstream -// core so that you can attempt to restart it without reloading -// the FPGA. If set, the o_reset signal will be used to reset -// the downstream core. -// -// A second key feature of this core are the outgoing fault indicators, -// o_write_fault and o_read_fault. If either signal is ever raised, the -// slave has (somehow) violated protocol on either the write or the -// read channels respectively. Such a violation may (or may not) return an -// error upstream. For example, if the slave returns a response -// following no requests from the master, then no error will be returned -// up stream (doing so would be a protocol violation), but a fault will -// still be detected. Use this line to trigger any internal logic -// analyzers. -// -// Creator: Dan Gisselquist, Ph.D. -// Gisselquist Technology, LLC -// -//////////////////////////////////////////////////////////////////////////////// -// }}} -// Copyright (C) 2020-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 axilsafety #( - // {{{ - parameter C_AXI_ADDR_WIDTH = 28, - parameter C_AXI_DATA_WIDTH = 32, - parameter OPT_TIMEOUT = 12, - parameter MAX_DEPTH = (OPT_TIMEOUT), - localparam AW = C_AXI_ADDR_WIDTH, - localparam DW = C_AXI_DATA_WIDTH, - localparam LGTIMEOUT = $clog2(OPT_TIMEOUT+1), - localparam LGDEPTH = $clog2(MAX_DEPTH+1), - parameter [0:0] OPT_SELF_RESET = 1'b1, - parameter OPT_MIN_RESET = 16 -`ifdef FORMAL - , parameter [0:0] F_OPT_WRITES = 1'b1, - parameter [0:0] F_OPT_READS = 1'b1, - parameter [0:0] F_OPT_FAULTLESS = 1'b1 -`endif - // }}} - ) ( - // {{{ - output reg o_write_fault, - output reg o_read_fault, - // - input wire S_AXI_ACLK, - input wire S_AXI_ARESETN, - output reg M_AXI_ARESETN, - // - input wire S_AXI_AWVALID, - output reg S_AXI_AWREADY, - input wire [AW-1:0] S_AXI_AWADDR, - input wire [2:0] S_AXI_AWPROT, - // - input wire S_AXI_WVALID, - output reg S_AXI_WREADY, - input wire [DW-1:0] S_AXI_WDATA, - input wire [DW/8-1:0] S_AXI_WSTRB, - // - output reg S_AXI_BVALID, - input wire S_AXI_BREADY, - output reg [1:0] S_AXI_BRESP, - // - input wire S_AXI_ARVALID, - output reg S_AXI_ARREADY, - input wire [AW-1:0] S_AXI_ARADDR, - input wire [2:0] S_AXI_ARPROT, - // - output reg S_AXI_RVALID, - input wire S_AXI_RREADY, - output reg [DW-1:0] S_AXI_RDATA, - output reg [1:0] S_AXI_RRESP, - // - // - // - output reg M_AXI_AWVALID, - input wire M_AXI_AWREADY, - output reg [AW-1:0] M_AXI_AWADDR, - output reg [2:0] M_AXI_AWPROT, - // - output reg M_AXI_WVALID, - input wire M_AXI_WREADY, - output reg [DW-1:0] M_AXI_WDATA, - output reg [DW/8-1:0] M_AXI_WSTRB, - // - input wire M_AXI_BVALID, - output wire M_AXI_BREADY, - input wire [1:0] M_AXI_BRESP, - // - output reg M_AXI_ARVALID, - input wire M_AXI_ARREADY, - output reg [AW-1:0] M_AXI_ARADDR, - output reg [2:0] M_AXI_ARPROT, - // - input wire M_AXI_RVALID, - output wire M_AXI_RREADY, - input wire [DW-1:0] M_AXI_RDATA, - input wire [1:0] M_AXI_RRESP - // }}} - ); - - // localparam, wire, and register declarations - // {{{ - localparam OPT_LOWPOWER = 1'b0; - localparam OKAY = 2'b00, - EXOKAY = 2'b01, - SLVERR = 2'b10; - - reg [LGDEPTH-1:0] aw_count, w_count, r_count; - reg aw_zero, w_zero, r_zero, - aw_full, w_full, r_full, - aw_w_greater, w_aw_greater; - reg [LGDEPTH-1:0] downstream_aw_count, downstream_w_count, downstream_r_count; - reg downstream_aw_zero, downstream_w_zero, downstream_r_zero; - // downstream_aw_w_greater, downstream_w_aw_greater; - - wire awskd_valid; - wire [2:0] awskd_prot; - wire [AW-1:0] awskd_addr; - reg awskd_ready; - - wire wskd_valid; - wire [DW-1:0] wskd_data; - wire [DW/8-1:0] wskd_strb; - reg wskd_ready; - - wire bskd_valid; - wire [1:0] bskd_resp; - reg bskd_ready; - - reg last_bvalid; - reg [1:0] last_bdata; - reg last_bchanged; - - wire arskd_valid; - wire [2:0] arskd_prot; - wire [AW-1:0] arskd_addr; - reg arskd_ready; - - reg last_rvalid; - reg [DW+1:0] last_rdata; - reg last_rchanged; - - wire rskd_valid; - wire [1:0] rskd_resp; - wire [DW-1:0] rskd_data; - reg rskd_ready; - - reg [LGTIMEOUT-1:0] aw_stall_counter, w_stall_counter, - r_stall_counter, w_ack_timer, r_ack_timer; - reg aw_stall_limit, w_stall_limit, r_stall_limit, - w_ack_limit, r_ack_limit; - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Write signaling - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Write address channel - // {{{ - - skidbuffer #(.DW(AW+3) - // {{{ -`ifdef FORMAL - , .OPT_PASSTHROUGH(1'b1) -`endif - // }}} - ) awskd(S_AXI_ACLK, !S_AXI_ARESETN, - // {{{ - S_AXI_AWVALID, S_AXI_AWREADY, { S_AXI_AWPROT, S_AXI_AWADDR }, - awskd_valid, awskd_ready, { awskd_prot, awskd_addr}); - // }}} - - // awskd_ready - // {{{ - // awskd_ready is the critical piece here, since it determines when - // we accept a packet from the skid buffer. - // - always @(*) - if (!M_AXI_ARESETN || o_write_fault) - // On any fault, we'll always accept a request (and return an - // error). We always accept a value if there are already - // more writes than write addresses accepted. - awskd_ready = (w_aw_greater) - ||((aw_zero)&&(!S_AXI_BVALID || S_AXI_BREADY)); - else - // Otherwise, we accept if ever our counters aren't about to - // overflow, and there's a place downstream to accept it - awskd_ready = (!M_AXI_AWVALID || M_AXI_AWREADY)&& (!aw_full); - // }}} - - // M_AXI_AWVALID - // {{{ - initial M_AXI_AWVALID = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN) - M_AXI_AWVALID <= 1'b0; - else if (!M_AXI_AWVALID || M_AXI_AWREADY) - M_AXI_AWVALID <= awskd_valid && awskd_ready && !o_write_fault; - // }}} - - // M_AXI_AWADDR, M_AXI_AWPROT - // {{{ - always @(posedge S_AXI_ACLK) - if (OPT_LOWPOWER && (!M_AXI_ARESETN || o_write_fault)) - begin - M_AXI_AWADDR <= 0; - M_AXI_AWPROT <= 0; - end else if (!M_AXI_AWVALID || M_AXI_AWREADY) - begin - M_AXI_AWADDR <= awskd_addr; - M_AXI_AWPROT <= awskd_prot; - end - // }}} - // }}} - - // - // Write data channel - // {{{ - - skidbuffer #(.DW(DW+DW/8) - // {{{ -`ifdef FORMAL - , .OPT_PASSTHROUGH(1'b1) -`endif - // }}} - ) wskd(S_AXI_ACLK, !S_AXI_ARESETN, - // {{{ - S_AXI_WVALID, S_AXI_WREADY, { S_AXI_WDATA, S_AXI_WSTRB }, - wskd_valid, wskd_ready, { wskd_data, wskd_strb}); - // }}} - - // wskd_ready - // {{{ - // As with awskd_ready, this logic is the critical key. - // - always @(*) - if (!M_AXI_ARESETN || o_write_fault) - wskd_ready = (aw_w_greater) - || ((w_zero)&&(!S_AXI_BVALID || S_AXI_BREADY)); - else - wskd_ready = (!M_AXI_WVALID || M_AXI_WREADY) && (!w_full); - // }}} - - // M_AXI_WVALID - // {{{ - initial M_AXI_WVALID = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN) - M_AXI_WVALID <= 1'b0; - else if (!M_AXI_WVALID || M_AXI_WREADY) - M_AXI_WVALID <= wskd_valid && wskd_ready && !o_write_fault; - // }}} - - // M_AXI_WDATA, M_AXI_WSTRB - // {{{ - always @(posedge S_AXI_ACLK) - if (OPT_LOWPOWER && (!M_AXI_ARESETN || o_write_fault)) - begin - M_AXI_WDATA <= 0; - M_AXI_WSTRB <= 0; - end else if (!M_AXI_WVALID || M_AXI_WREADY) - begin - M_AXI_WDATA <= wskd_data; - M_AXI_WSTRB <= (o_write_fault) ? 0 : wskd_strb; - end - // }}} - // }}} - - // - // Write return channel - // {{{ - - // bskd_valid, M_AXI_BREADY, bskd_resp - // {{{ -`ifdef FORMAL - assign bskd_valid = M_AXI_BVALID; - assign M_AXI_BREADY= bskd_ready; - assign bskd_resp = M_AXI_BRESP; -`else - skidbuffer #(.DW(2) - ) bskd(S_AXI_ACLK, !S_AXI_ARESETN || !M_AXI_ARESETN, - M_AXI_BVALID, M_AXI_BREADY, M_AXI_BRESP, - bskd_valid, bskd_ready, bskd_resp); -`endif - // }}} - - // bskd_ready - // {{{ - always @(*) - if (o_write_fault) - bskd_ready = 1'b1; - else - bskd_ready = (!S_AXI_BVALID || S_AXI_BREADY); - // }}} - - // S_AXI_BVALID - // {{{ - initial S_AXI_BVALID = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - S_AXI_BVALID <= 1'b0; - else if (!S_AXI_BVALID || S_AXI_BREADY) - begin - if (o_write_fault || !M_AXI_ARESETN) - S_AXI_BVALID <= (!S_AXI_BVALID&&(!aw_zero)&&(!w_zero)); - else - S_AXI_BVALID <= (!downstream_aw_zero) - &&(!downstream_w_zero)&&(bskd_valid); - end - // }}} - - // last_bvalid - // {{{ - initial last_bvalid = 1'b0; - always @(posedge S_AXI_ACLK) - if (!M_AXI_ARESETN || o_write_fault) - last_bvalid <= 1'b0; - else - last_bvalid <= (M_AXI_BVALID && !M_AXI_BREADY); - // }}} - - // last_bdata - // {{{ - always @(posedge S_AXI_ACLK) - if (M_AXI_BVALID) - last_bdata <= M_AXI_BRESP; - // }}} - - // last_bchanged - // {{{ - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - last_bchanged <= 1'b0; - else - last_bchanged <= (last_bvalid && (!M_AXI_BVALID - || last_bdata != M_AXI_BRESP)); - // }}} - - // S_AXI_BRESP - // {{{ - initial S_AXI_BRESP = OKAY; - always @(posedge S_AXI_ACLK) - if (!S_AXI_BVALID || S_AXI_BREADY) - begin - if (o_write_fault) - S_AXI_BRESP <= SLVERR; - else if (bskd_resp == EXOKAY) - S_AXI_BRESP <= SLVERR; - else - S_AXI_BRESP <= bskd_resp; - end - // }}} - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Read signaling - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Read address channel - // {{{ - - skidbuffer #(.DW(AW+3) - // {{{ -`ifdef FORMAL - , .OPT_PASSTHROUGH(1'b1) -`endif - // }}} - ) arskd(S_AXI_ACLK, !S_AXI_ARESETN, - // {{{ - S_AXI_ARVALID, S_AXI_ARREADY, { S_AXI_ARPROT, S_AXI_ARADDR }, - arskd_valid, arskd_ready, { arskd_prot, arskd_addr }); - // }}} - - // arskd_ready - // {{{ - always @(*) - if (!M_AXI_ARESETN || o_read_fault) - arskd_ready =((r_zero)&&(!S_AXI_RVALID || S_AXI_RREADY)); - else - arskd_ready = (!M_AXI_ARVALID || M_AXI_ARREADY) && (!r_full); - // }}} - - // M_AXI_ARVALID - // {{{ - initial M_AXI_ARVALID = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN) - M_AXI_ARVALID <= 1'b0; - else if (!M_AXI_ARVALID || M_AXI_ARREADY) - M_AXI_ARVALID <= arskd_valid && arskd_ready && !o_read_fault; - // }}} - - // M_AXI_ARADDR, M_AXI_ARPROT - // {{{ - always @(posedge S_AXI_ACLK) - if (OPT_LOWPOWER && (!M_AXI_ARESETN || o_read_fault)) - begin - M_AXI_ARADDR <= 0; - M_AXI_ARPROT <= 0; - end else if (!M_AXI_ARVALID || M_AXI_ARREADY) - begin - M_AXI_ARADDR <= arskd_addr; - M_AXI_ARPROT <= arskd_prot; - end - // }}} - // }}} - - // - // Read data channel - // {{{ - - // rskd_valid, rskd_resp, rskd_data skid buffer - // {{{ -`ifdef FORMAL - assign rskd_valid = M_AXI_RVALID; - assign M_AXI_RREADY = rskd_ready; - assign { rskd_resp, rskd_data } = { M_AXI_RRESP, M_AXI_RDATA }; -`else - skidbuffer #(.DW(DW+2) - ) rskd(S_AXI_ACLK, !S_AXI_ARESETN || !M_AXI_ARESETN, - M_AXI_RVALID, M_AXI_RREADY, { M_AXI_RRESP, M_AXI_RDATA }, - rskd_valid, rskd_ready, { rskd_resp, rskd_data }); -`endif - // ?}}} - - // rskd_ready - // {{{ - always @(*) - if (o_read_fault) - rskd_ready = 1; - else - rskd_ready = (!S_AXI_RVALID || S_AXI_RREADY); - // }}} - - // S_AXI_RVALID - // {{{ - initial S_AXI_RVALID = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - S_AXI_RVALID <= 1'b0; - else if (!S_AXI_RVALID || S_AXI_RREADY) - begin - if (o_read_fault || !M_AXI_ARESETN) - S_AXI_RVALID <= (!S_AXI_RVALID && !r_zero) - || (arskd_valid && arskd_ready); - else - S_AXI_RVALID <= (!downstream_r_zero)&&(rskd_valid); - end - // }}} - - // S_AXI_RDATA, S_AXI_RRESP - // {{{ - always @(posedge S_AXI_ACLK) - if (!S_AXI_RVALID || S_AXI_RREADY) - begin - if (o_read_fault || !M_AXI_ARESETN) - S_AXI_RDATA <= 0; - else - S_AXI_RDATA <= rskd_data; - - S_AXI_RRESP <= OKAY; - if (o_read_fault || rskd_resp == EXOKAY || !M_AXI_ARESETN) - S_AXI_RRESP <= SLVERR; - else if (!downstream_r_zero) - S_AXI_RRESP <= rskd_resp; - end - // }}} - - // last_rvalid - // {{{ - initial last_rvalid = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - last_rvalid <= 1'b0; - else - last_rvalid <= (M_AXI_RVALID && !M_AXI_RREADY); - // }}} - - // last_rdata - // {{{ - always @(posedge S_AXI_ACLK) - if (M_AXI_RVALID) - last_rdata <= { M_AXI_RRESP, M_AXI_RDATA }; - // }}} - - // last_rchanged - // {{{ - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - last_rchanged <= 1'b0; - else - last_rchanged <= (last_rvalid && (!M_AXI_RVALID - || last_rdata != { M_AXI_RRESP, M_AXI_RDATA })); - // }}} - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Usage counters - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Write address channel - // {{{ - - initial aw_count = 0; - initial aw_zero = 1; - initial aw_full = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - aw_count <= 0; - aw_zero <= 1; - aw_full <= 0; - end else case({(awskd_valid && awskd_ready),S_AXI_BVALID&&S_AXI_BREADY}) - 2'b10: begin - aw_count <= aw_count + 1; - aw_zero <= 0; - aw_full <= (aw_count == { {(LGDEPTH-1){1'b1}}, 1'b0 }); - end - 2'b01: begin - aw_count <= aw_count - 1; - aw_zero <= (aw_count <= 1); - aw_full <= 0; - end - default: begin end - endcase - // }}} - - // - // Write data channel - // {{{ - initial w_count = 0; - initial w_zero = 1; - initial w_full = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - w_count <= 0; - w_zero <= 1; - w_full <= 0; - end else case({(wskd_valid && wskd_ready), S_AXI_BVALID&& S_AXI_BREADY}) - 2'b10: begin - w_count <= w_count + 1; - w_zero <= 0; - w_full <= (w_count == { {(LGDEPTH-1){1'b1}}, 1'b0 }); - end - 2'b01: begin - w_count <= w_count - 1; - w_zero <= (w_count <= 1); - w_full <= 1'b0; - end - default: begin end - endcase - // }}} - - // aw_w_greater, w_aw_greater - // {{{ - initial aw_w_greater = 0; - initial w_aw_greater = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - aw_w_greater <= 0; - w_aw_greater <= 0; - end else case({(awskd_valid && awskd_ready), - (wskd_valid && wskd_ready)}) - 2'b10: begin - aw_w_greater <= (aw_count + 1 > w_count); - w_aw_greater <= ( w_count > aw_count + 1); - end - 2'b01: begin - aw_w_greater <= (aw_count > w_count + 1); - w_aw_greater <= ( w_count + 1 > aw_count); - end - default: begin end - endcase - // }}} - // - // Read channel - // {{{ - - // r_count, r_zero, r_full - initial r_count = 0; - initial r_zero = 1; - initial r_full = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - begin - r_count <= 0; - r_zero <= 1; - r_full <= 0; - end else case({(arskd_valid&&arskd_ready), S_AXI_RVALID&&S_AXI_RREADY}) - 2'b10: begin - r_count <= r_count + 1; - r_zero <= 0; - r_full <= (r_count == { {(LGDEPTH-1){1'b1}}, 1'b0 }); - end - 2'b01: begin - r_count <= r_count - 1; - r_zero <= (r_count <= 1); - r_full <= 0; - end - default: begin end - endcase - // }}} - - // - // Downstream write address channel - // {{{ - - initial downstream_aw_count = 0; - initial downstream_aw_zero = 1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - downstream_aw_count <= 0; - downstream_aw_zero <= 1; - end else case({(M_AXI_AWVALID && M_AXI_AWREADY), M_AXI_BVALID && M_AXI_BREADY}) - 2'b10: begin - downstream_aw_count <= downstream_aw_count + 1; - downstream_aw_zero <= 0; - end - 2'b01: begin - downstream_aw_count <= downstream_aw_count - 1; - downstream_aw_zero <= (downstream_aw_count <= 1); - end - default: begin end - endcase - // }}} - - // - // Downstream write data channel - // {{{ - initial downstream_w_count = 0; - initial downstream_w_zero = 1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - downstream_w_count <= 0; - downstream_w_zero <= 1; - end else case({(M_AXI_WVALID && M_AXI_WREADY), M_AXI_BVALID && M_AXI_BREADY}) - 2'b10: begin - downstream_w_count <= downstream_w_count + 1; - downstream_w_zero <= 0; - end - 2'b01: begin - downstream_w_count <= downstream_w_count - 1; - downstream_w_zero <= (downstream_w_count <= 1); - end - default: begin end - endcase - // }}} - - // - // Downstream read channel - // {{{ - - initial downstream_r_count = 0; - initial downstream_r_zero = 1; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - begin - downstream_r_count <= 0; - downstream_r_zero <= 1; - end else case({M_AXI_ARVALID && M_AXI_ARREADY, M_AXI_RVALID && M_AXI_RREADY}) - 2'b10: begin - downstream_r_count <= downstream_r_count + 1; - downstream_r_zero <= 0; - end - 2'b01: begin - downstream_r_count <= downstream_r_count - 1; - downstream_r_zero <= (downstream_r_count <= 1); - end - default: begin end - endcase - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Timeout checking - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // The key piece here is that we define the timeout depending upon - // what happens (or doesn't happen) *DOWNSTREAM*. These timeouts - // will need to propagate upstream before taking place. - - // - // Write address stall counter - // {{{ - initial aw_stall_counter = 0; - initial aw_stall_limit = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || o_write_fault || !M_AXI_ARESETN) - begin - aw_stall_counter <= 0; - aw_stall_limit <= 0; - end else if (!M_AXI_AWVALID || M_AXI_AWREADY || M_AXI_BVALID) - begin - aw_stall_counter <= 0; - aw_stall_limit <= 0; - end else if (aw_w_greater && !M_AXI_WVALID) - begin - aw_stall_counter <= 0; - aw_stall_limit <= 0; - end else // if (!S_AXI_BVALID || S_AXI_BREADY) - begin - aw_stall_counter <= aw_stall_counter + 1; - aw_stall_limit <= (aw_stall_counter+1 >= OPT_TIMEOUT); - end - // }}} - - // - // Write data stall counter - // {{{ - initial w_stall_counter = 0; - initial w_stall_limit = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - w_stall_counter <= 0; - w_stall_limit <= 0; - end else if (!M_AXI_WVALID || M_AXI_WREADY || M_AXI_BVALID) - begin - w_stall_counter <= 0; - w_stall_limit <= 0; - end else if (w_aw_greater && !M_AXI_AWVALID) - begin - w_stall_counter <= 0; - w_stall_limit <= 0; - end else // if (!M_AXI_BVALID || M_AXI_BREADY) - begin - w_stall_counter <= w_stall_counter + 1; - w_stall_limit <= (w_stall_counter + 1 >= OPT_TIMEOUT); - end - // }}} - - // - // Write acknowledgment delay counter - // {{{ - initial w_ack_timer = 0; - initial w_ack_limit = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - begin - w_ack_timer <= 0; - w_ack_limit <= 0; - end else if (M_AXI_BVALID || downstream_aw_zero || downstream_w_zero) - begin - w_ack_timer <= 0; - w_ack_limit <= 0; - end else - begin - w_ack_timer <= w_ack_timer + 1; - w_ack_limit <= (w_ack_timer + 1 >= OPT_TIMEOUT); - end - // }}} - - // - // Read request stall counter - // {{{ - initial r_stall_counter = 0; - initial r_stall_limit = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - begin - r_stall_counter <= 0; - r_stall_limit <= 0; - end else if (!M_AXI_ARVALID || M_AXI_ARREADY || M_AXI_RVALID) - begin - r_stall_counter <= 0; - r_stall_limit <= 0; - end else begin - r_stall_counter <= r_stall_counter + 1; - r_stall_limit <= (r_stall_counter + 1 >= OPT_TIMEOUT); - end - // }}} - - // - // Read acknowledgement delay counter - // {{{ - initial r_ack_timer = 0; - initial r_ack_limit = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - begin - r_ack_timer <= 0; - r_ack_limit <= 0; - end else if (M_AXI_RVALID || downstream_r_zero) - begin - r_ack_timer <= 0; - r_ack_limit <= 0; - end else begin - r_ack_timer <= r_ack_timer + 1; - r_ack_limit <= (r_ack_timer + 1 >= OPT_TIMEOUT); - end - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Fault detection - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - // - // Determine if a write fault has taken place - // {{{ - initial o_write_fault =1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - o_write_fault <= 1'b0; - else if (OPT_SELF_RESET && o_write_fault) - begin - // - // Clear any fault on reset - if (!M_AXI_ARESETN) - o_write_fault <= 1'b0; - end else begin - // - // A write fault takes place if you respond without a prior - // bus request on both write address and write data channels. - if ((downstream_aw_zero || downstream_w_zero)&&(bskd_valid)) - o_write_fault <= 1'b1; - - // AXI-lite slaves are not allowed to return EXOKAY responses - // from the bus - if (bskd_valid && bskd_resp == EXOKAY) - o_write_fault <= 1'b1; - - // If the downstream core refuses to accept either a - // write address request, or a write data request, or for that - // matter if it doesn't return an acknowledgment in a timely - // fashion, then a fault has been detected. - if (aw_stall_limit || w_stall_limit || w_ack_limit) - o_write_fault <= 1'b1; - - // If the downstream core changes BRESP while VALID && !READY, - // then it isn't stalling the channel properly--that's a fault. - if (last_bchanged) - o_write_fault <= 1'b1; - end - // }}} - - // o_read_fault - // {{{ - initial o_read_fault =1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - o_read_fault <= 1'b0; - else if (OPT_SELF_RESET && o_read_fault) - begin - // - // Clear any fault on reset - if (!M_AXI_ARESETN) - o_read_fault <= 1'b0; - end else begin - // Responding without a prior request is a fault. Can only - // respond after a request has been made. - if (downstream_r_zero && rskd_valid) - o_read_fault <= 1'b1; - - // AXI-lite slaves are not allowed to return EXOKAY. This is - // an error. - if (rskd_valid && rskd_resp == EXOKAY) - o_read_fault <= 1'b1; - - // The slave cannot stall the bus forever, nor should the - // master wait forever for a response from the slave. - if (r_stall_limit || r_ack_limit) - o_read_fault <= 1'b1; - - // If the slave changes the data, or the RRESP on the wire, - // while the incoming bus is stalled, then that's also a fault. - if (last_rchanged) - o_read_fault <= 1'b1; - end - // }}} - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Self reset handling - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - - generate if (OPT_SELF_RESET) - begin : SELF_RESET_GENERATION - // {{{ - wire min_reset; - - if (OPT_MIN_RESET > 1) - begin : MIN_RESET - // {{{ - reg r_min_reset; - reg [$clog2(OPT_MIN_RESET+1):0] reset_counter; - - // - // Optionally insist that any downstream reset have a - // minimum duration. Many Xilinx components require - // a 16-clock reset. This ensures such reset - // requirements are achieved. - // - - initial reset_counter = OPT_MIN_RESET-1; - initial r_min_reset = 1'b0; - always @(posedge S_AXI_ARESETN) - if (M_AXI_ARESETN) - begin - reset_counter <= OPT_MIN_RESET-1; - r_min_reset <= 1'b0; - end else if (!M_AXI_ARESETN) - begin - if (reset_counter > 0) - reset_counter <= reset_counter-1; - min_reset <= (reset_counter <= 1); - end - - assign min_reset = r_min_reset; -`ifdef FORMAL - always @(*) - assert(reset_counter < OPT_MIN_RESET); - always @(*) - assert(min_reset == (reset_counter == 0)); -`endif - // }}} - end else begin : NO_MIN_RESET - // {{{ - assign min_reset = 1'b1; - // }}} - end - - // M_AXI_ARESETN - // {{{ - // Reset the downstream bus on either a write or a read fault. - // Once the bus returns to idle, and any minimum reset durations - // have been achieved, then release the downstream from reset. - // - initial M_AXI_ARESETN = 1'b0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - M_AXI_ARESETN <= 1'b0; - else if (o_write_fault || o_read_fault) - M_AXI_ARESETN <= 1'b0; - else if (aw_zero && w_zero && r_zero && min_reset - && !awskd_valid && !wskd_valid && !arskd_valid) - M_AXI_ARESETN <= 1'b1; - // }}} - // }}} - end else begin : SAME_RESET - // {{{ - // - // The downstream reset equals the upstream reset - // - always @(*) - M_AXI_ARESETN = S_AXI_ARESETN; - // }}} - end endgenerate - // }}} -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -// -// Formal property section -// {{{ -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -//////////////////////////////////////////////////////////////////////////////// -`ifdef FORMAL - // {{{ - // - // The following proof comes in several parts. - // - // 1. PROVE that the upstream properties will hold independent of - // what the downstream slave ever does. - // - // 2. PROVE that if the downstream slave follows protocol, then - // neither o_write_fault nor o_read_fault will never get raised. - // - // We then repeat these proofs again with both OPT_SELF_RESET set and - // clear. Which of the four proofs is accomplished is dependent upon - // parameters set by the formal engine. - // - // - wire [LGDEPTH:0] faxils_awr_outstanding, faxils_wr_outstanding, - faxils_rd_outstanding; - - reg f_past_valid; - initial f_past_valid = 0; - always @(posedge S_AXI_ACLK) - f_past_valid <= 1; - // }}} - //////////////////////////////////////////////////////////////////////// - // - // Upstream master Bus properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - always @(*) - if (!f_past_valid) - begin - assume(!S_AXI_ARESETN); - assert(!M_AXI_ARESETN); - end - - faxil_slave #( - // {{{ - .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), - .F_OPT_ASSUME_RESET(1'b1), - .F_OPT_NO_RESET((OPT_MIN_RESET == 0) ? 1:0), -// .F_AXI_MAXWAIT((F_OPT_FAULTLESS) ? (2*OPT_TIMEOUT+2) : 0), - .F_AXI_MAXRSTALL(3), -// .F_AXI_MAXDELAY(OPT_TIMEOUT+OPT_TIMEOUT+5), - .F_LGDEPTH(LGDEPTH+1), - // - .F_AXI_MAXWAIT((F_OPT_FAULTLESS) ? (2*OPT_TIMEOUT+2) : 0), - .F_AXI_MAXDELAY(2*OPT_TIMEOUT+3) - // }}} - ) axils ( - // {{{ - .i_clk(S_AXI_ACLK), - .i_axi_reset_n(S_AXI_ARESETN), - // - .i_axi_awvalid(S_AXI_AWVALID), - .i_axi_awready(S_AXI_AWREADY), - .i_axi_awaddr( S_AXI_AWADDR), - .i_axi_awprot( S_AXI_AWPROT), - // - .i_axi_wvalid(S_AXI_WVALID), - .i_axi_wready(S_AXI_WREADY), - .i_axi_wdata( S_AXI_WDATA), - .i_axi_wstrb( S_AXI_WSTRB), - // - .i_axi_bvalid(S_AXI_BVALID), - .i_axi_bready(S_AXI_BREADY), - .i_axi_bresp( S_AXI_BRESP), - // - .i_axi_arvalid(S_AXI_ARVALID), - .i_axi_arready(S_AXI_ARREADY), - .i_axi_araddr( S_AXI_ARADDR), - .i_axi_arprot( S_AXI_ARPROT), - // - .i_axi_rvalid(S_AXI_RVALID), - .i_axi_rready(S_AXI_RREADY), - .i_axi_rdata( S_AXI_RDATA), - .i_axi_rresp( S_AXI_RRESP), - // - .f_axi_awr_outstanding(faxils_awr_outstanding), - .f_axi_wr_outstanding(faxils_wr_outstanding), - .f_axi_rd_outstanding(faxils_rd_outstanding) - // }}} - ); - - always @(*) - if (!F_OPT_WRITES) - begin - // {{{ - assume(!S_AXI_AWVALID); - assume(!S_AXI_WVALID); - assert(aw_count == 0); - assert(w_count == 0); - assert(!M_AXI_AWVALID); - assert(!M_AXI_WVALID); - // }}} - end - - always @(*) - if (!F_OPT_READS) - begin - // {{{ - assume(!S_AXI_ARVALID); - assert(r_count == 0); - assert(!S_AXI_RVALID); - assert(!M_AXI_ARVALID); - // }}} - end - // }}} - //////////////////////////////////////////////////////////////////////// - // - // General Induction properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - - always @(*) - begin - // {{{ - assert(aw_zero == (aw_count == 0)); - assert(w_zero == (w_count == 0)); - assert(r_zero == (r_count == 0)); - - // - assert(aw_full == (&aw_count)); - assert(w_full == (&w_count)); - assert(r_full == (&r_count)); - // - if (M_AXI_ARESETN && !o_write_fault) - begin - assert(downstream_aw_zero == (downstream_aw_count == 0)); - assert(downstream_w_zero == (downstream_w_count == 0)); - assert(downstream_aw_count + (M_AXI_AWVALID ? 1:0) - + (S_AXI_BVALID ? 1:0) == aw_count); - assert(downstream_w_count + (M_AXI_WVALID ? 1:0) - + (S_AXI_BVALID ? 1:0) == w_count); - end - - if (M_AXI_ARESETN && !o_read_fault) - begin - assert(downstream_r_zero == (downstream_r_count == 0)); - assert(downstream_r_count + (M_AXI_ARVALID ? 1:0) - + (S_AXI_RVALID ? 1:0) == r_count); - end - // - assert(aw_count == faxils_awr_outstanding); - assert(w_count == faxils_wr_outstanding); - assert(r_count == faxils_rd_outstanding); - - assert(aw_w_greater == (aw_count > w_count)); - assert(w_aw_greater == (w_count > aw_count)); - // }}} - end - // }}} - generate if (F_OPT_FAULTLESS) - begin : ASSUME_FAULTLESS - // {{{ - //////////////////////////////////////////////////////////////// - // - // Assume the downstream core is protocol compliant, and - // prove that o_fault stays low. - // {{{ - //////////////////////////////////////////////////////////////// - // - wire [LGDEPTH:0] faxilm_awr_outstanding, - faxilm_wr_outstanding, - faxilm_rd_outstanding; - - faxil_master #( - // {{{ - .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), - .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), - .F_OPT_NO_RESET((OPT_MIN_RESET == 0) ? 1:0), - .F_AXI_MAXWAIT(OPT_TIMEOUT), - .F_AXI_MAXRSTALL(4), - .F_AXI_MAXDELAY(OPT_TIMEOUT), - .F_LGDEPTH(LGDEPTH+1) - // }}} - ) axilm ( - // {{{ - .i_clk(S_AXI_ACLK), - .i_axi_reset_n(M_AXI_ARESETN && S_AXI_ARESETN), - // - .i_axi_awvalid(M_AXI_AWVALID), - .i_axi_awready(M_AXI_AWREADY), - .i_axi_awaddr( M_AXI_AWADDR), - .i_axi_awprot( M_AXI_AWPROT), - // - .i_axi_wvalid(M_AXI_WVALID), - .i_axi_wready(M_AXI_WREADY), - .i_axi_wdata( M_AXI_WDATA), - .i_axi_wstrb( M_AXI_WSTRB), - // - .i_axi_bvalid(M_AXI_BVALID), - .i_axi_bready(M_AXI_BREADY), - .i_axi_bresp( M_AXI_BRESP), - // - .i_axi_arvalid(M_AXI_ARVALID), - .i_axi_arready(M_AXI_ARREADY), - .i_axi_araddr( M_AXI_ARADDR), - .i_axi_arprot( M_AXI_ARPROT), - // - .i_axi_rvalid(M_AXI_RVALID), - .i_axi_rready(M_AXI_RREADY), - .i_axi_rdata( M_AXI_RDATA), - .i_axi_rresp( M_AXI_RRESP), - // - .f_axi_awr_outstanding(faxilm_awr_outstanding), - .f_axi_wr_outstanding(faxilm_wr_outstanding), - .f_axi_rd_outstanding(faxilm_rd_outstanding) - // }}} - ); - - // - // Here's the big proof - // {{{ - always @(*) - assert(!o_write_fault); - always @(*) - assert(!o_read_fault); - // }}} - // }}} - //////////////////////////////////////////////////////////////// - // - // The following properties are necessary for passing induction - // {{{ - //////////////////////////////////////////////////////////////// - // - // - always @(*) - begin - assert(!aw_stall_limit); - assert(!w_stall_limit); - assert(!w_ack_limit); - - assert(!r_stall_limit); - assert(!r_ack_limit); - - if (M_AXI_ARESETN) - begin - assert(downstream_aw_count == faxilm_awr_outstanding); - assert(downstream_w_count == faxilm_wr_outstanding); - assert(downstream_r_count == faxilm_rd_outstanding); - end - end - - if (OPT_SELF_RESET) - begin - always @(posedge S_AXI_ACLK) - if (f_past_valid) - assert(M_AXI_ARESETN == $past(S_AXI_ARESETN)); - end - -`ifdef VERIFIC - wire [LGDEPTH:0] f_axi_arstall; - wire [LGDEPTH:0] f_axi_awstall; - wire [LGDEPTH:0] f_axi_wstall; - - assign f_axi_awstall = axilm.CHECK_STALL_COUNT.f_axi_awstall; - assign f_axi_wstall = axilm.CHECK_STALL_COUNT.f_axi_wstall; - assign f_axi_arstall = axilm.CHECK_STALL_COUNT.f_axi_arstall; - - always @(*) - if (M_AXI_ARESETN && S_AXI_ARESETN && !o_write_fault) - assert(f_axi_awstall == aw_stall_counter); - - always @(*) - if (M_AXI_ARESETN && S_AXI_ARESETN && !o_write_fault) - assert(f_axi_wstall == w_stall_counter); - - always @(*) - if (M_AXI_ARESETN && S_AXI_ARESETN && !o_read_fault) - assert(f_axi_arstall == r_stall_counter); -`endif - // }}} - // }}} - end else begin : WILD_DOWNSTREAM - // {{{ - //////////////////////////////////////////////////////////////// - // - // cover() checks, checks that only make sense if faults are - // possible - // - - reg write_faulted, read_faulted, faulted; - reg [3:0] cvr_writes, cvr_reads; - - - if (OPT_SELF_RESET) - begin - //////////////////////////////////////////////////////// - // - // Prove that we can actually reset the downstream - // bus/core as desired - // {{{ - //////////////////////////////////////////////////////// - // - // - initial write_faulted = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - write_faulted <= 0; - else if (o_write_fault) - write_faulted <= 1; - - - initial faulted = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN) - read_faulted <= 0; - else if (o_read_fault) - read_faulted <= 1; - - always @(*) - faulted = (write_faulted || read_faulted); - - always @(posedge S_AXI_ACLK) - cover(write_faulted && $rose(M_AXI_ARESETN)); - - always @(posedge S_AXI_ACLK) - cover(read_faulted && $rose(M_AXI_ARESETN)); - - always @(posedge S_AXI_ACLK) - cover(faulted && M_AXI_ARESETN && S_AXI_BVALID); - - always @(posedge S_AXI_ACLK) - cover(faulted && M_AXI_ARESETN && S_AXI_RVALID); - - - initial cvr_writes = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_write_fault) - cvr_writes <= 0; - else if (write_faulted && S_AXI_BVALID && S_AXI_BREADY - && S_AXI_BRESP == OKAY - &&(!(&cvr_writes))) - cvr_writes <= cvr_writes + 1; - - always @(*) - cover(cvr_writes > 5); - - initial cvr_reads = 0; - always @(posedge S_AXI_ACLK) - if (!S_AXI_ARESETN || !M_AXI_ARESETN || o_read_fault) - cvr_reads <= 0; - else if (read_faulted && S_AXI_RVALID && S_AXI_RREADY - && S_AXI_RRESP == OKAY - &&(!(&cvr_reads))) - cvr_reads <= cvr_reads + 1; - - always @(*) - cover(cvr_reads > 5); - // }}} - end - - // }}} - end endgenerate - //////////////////////////////////////////////////////////////////////// - // - // Never data properties - // {{{ - //////////////////////////////////////////////////////////////////////// - // - // - (* anyconst *) reg [C_AXI_DATA_WIDTH-1:0] fc_never_read_data; - (* anyconst *) reg [C_AXI_DATA_WIDTH+C_AXI_DATA_WIDTH/8-1:0] - fc_never_write_data; - - (* anyconst *) reg [C_AXI_ADDR_WIDTH-1:0] fc_never_read_addr, - fc_never_write_addr; - - // Write address checking - // {{{ - always @(*) - if (S_AXI_ARESETN && S_AXI_AWVALID) - assume(S_AXI_AWADDR != fc_never_write_addr); - - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && !o_write_fault && M_AXI_AWVALID) - assert(M_AXI_AWADDR != fc_never_write_addr); - // }}} - - // Write checking - // {{{ - always @(*) - if (S_AXI_ARESETN && S_AXI_WVALID) - assume({ S_AXI_WDATA, S_AXI_WSTRB } != fc_never_write_data); - - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && !o_write_fault && M_AXI_WVALID) - assert({ M_AXI_WDATA, M_AXI_WSTRB } != fc_never_write_data); - // }}} - - // Read address checking - // {{{ - always @(*) - if (S_AXI_ARESETN && S_AXI_ARVALID) - assume(S_AXI_ARADDR != fc_never_read_addr); - - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && !o_read_fault && M_AXI_ARVALID) - assert(M_AXI_ARADDR != fc_never_read_addr); - // }}} - - // Read checking - // {{{ - always @(*) - if (S_AXI_ARESETN && M_AXI_ARESETN && M_AXI_RVALID) - assume(M_AXI_RDATA != fc_never_read_data); - - always @(*) - if (S_AXI_ARESETN && S_AXI_RVALID && S_AXI_RRESP == 2'b00) - assert(S_AXI_RDATA != fc_never_read_data); - // }}} - - // }}} - -`endif -// }}} -endmodule |