| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: wbsafety.v |
| // |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: A WB bus fault isolator. This core will isolate any downstream |
| // WB 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 |
| // the 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 is the outgoing fault detector, |
| // o_fault. If this signal is ever raised, the slave has (somehow) |
| // violated protocol. 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 |
| // be detected. Use this line to trigger any internal logic analyzers. |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Copyright (C) 2019-2020, 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 wbsafety(i_clk, i_reset, |
| // |
| // The incoming WB interface from the (trusted) master |
| // This interface is guaranteed to follow the protocol. |
| i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, |
| o_wb_stall, o_wb_ack, o_wb_idata, o_wb_err, |
| // |
| // The outgoing interface to the untrusted slave |
| // This interface may or may not follow the WB protocol |
| o_reset, o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, |
| o_wb_sel, |
| i_wb_stall, i_wb_ack, i_wb_idata, i_wb_err, |
| // |
| // The fault signal, indicating the downstream slave was |
| // misbehaving |
| o_fault); |
| parameter AW = 28, DW = 32; |
| parameter OPT_TIMEOUT = 12; |
| parameter MAX_DEPTH = (OPT_TIMEOUT); |
| localparam LGTIMEOUT = $clog2(OPT_TIMEOUT+1); |
| localparam LGDEPTH = $clog2(MAX_DEPTH+1); |
| parameter [0:0] OPT_SELF_RESET = 1'b1; |
| parameter [0:0] F_OPT_FAULTLESS = 1'b1; |
| // |
| input wire i_clk, i_reset; |
| // |
| input wire i_wb_cyc, i_wb_stb, i_wb_we; |
| input wire [AW-1:0] i_wb_addr; |
| input wire [DW-1:0] i_wb_data; |
| input wire [DW/8-1:0] i_wb_sel; |
| output reg o_wb_ack, o_wb_err, o_wb_stall; |
| output reg [DW-1:0] o_wb_idata; |
| // |
| output reg o_reset; |
| output reg o_wb_cyc, o_wb_stb, o_wb_we; |
| output reg [AW-1:0] o_wb_addr; |
| output reg [DW-1:0] o_wb_data; |
| output reg [DW/8-1:0] o_wb_sel; |
| input wire i_wb_ack, i_wb_err, i_wb_stall; |
| input wire [DW-1:0] i_wb_idata; |
| // |
| output reg o_fault; |
| |
| reg none_expected; |
| reg [LGDEPTH-1:0] expected_returns; |
| reg [LGTIMEOUT-1:0] stall_timer, wait_timer; |
| reg timeout; |
| reg faulty_return; |
| |
| wire skd_stb, skd_o_ready, skd_we; |
| reg skd_stall; |
| wire [AW-1:0] skd_addr; |
| wire [DW-1:0] skd_data; |
| wire [DW/8-1:0] skd_sel; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Start with a skid buffer on all incoming signals |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| `ifdef FORMAL |
| // |
| // We know the skid buffer works. It's irrelevant to our proof. |
| // Therefore, remove it during formal testing, lest we need to |
| // check it as well. Further, we make this a parameter--but only |
| // when FORMAL is defined--so that it may be overridden in that case. |
| // |
| parameter [0:0] SKID_PASSTHROUGH = 1'b1; |
| `else |
| localparam [0:0] SKID_PASSTHROUGH = 1'b0; |
| `endif |
| |
| skidbuffer #(.DW(1+AW+DW+(DW/8)), |
| .OPT_PASSTHROUGH(SKID_PASSTHROUGH)) |
| skd(i_clk, i_reset || !i_wb_cyc, i_wb_stb, skd_o_ready, |
| { i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }, |
| skd_stb, !skd_stall, { skd_we, skd_addr, skd_data, skd_sel }); |
| |
| always @(*) |
| o_wb_stall = !skd_o_ready; |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Timeout checking |
| // |
| |
| |
| // |
| // Insist on a maximum number of downstream stalls |
| // |
| initial stall_timer = 0; |
| always @(posedge i_clk) |
| if (!i_reset && o_wb_stb && i_wb_stall) |
| begin |
| if (stall_timer <= OPT_TIMEOUT) |
| stall_timer <= stall_timer + 1; |
| end else |
| stall_timer <= 0; |
| |
| // |
| // Insist on a maximum number cyles waiting for an acknowledgment |
| // |
| initial wait_timer = 0; |
| always @(posedge i_clk) |
| if (!i_reset && o_wb_cyc && !o_wb_stb && !i_wb_ack && !i_wb_err |
| && !none_expected) |
| begin |
| if (wait_timer <= OPT_TIMEOUT) |
| wait_timer <= wait_timer + 1; |
| end else |
| wait_timer <= 0; |
| |
| // |
| // Generate a timeout signal on any error |
| // |
| initial timeout = 0; |
| always @(posedge i_clk) |
| if (timeout && o_wb_err) |
| timeout <= 0; |
| else |
| timeout <= (i_wb_stall)&&(stall_timer >= OPT_TIMEOUT) |
| || ((!i_wb_ack && !i_wb_err)&&(wait_timer >= OPT_TIMEOUT)); |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Return counting |
| // |
| |
| initial none_expected = 1; |
| initial expected_returns = 0; |
| always @(posedge i_clk) |
| if (i_reset || o_reset || o_wb_err || !i_wb_cyc) |
| begin |
| expected_returns <= 0; |
| none_expected <= 1; |
| end else case({skd_stb && !skd_stall, o_wb_ack }) |
| 2'b10: begin |
| expected_returns <= expected_returns + 1; |
| none_expected <= 1'b0; |
| end |
| 2'b01: begin |
| expected_returns <= expected_returns - 1; |
| none_expected <= (expected_returns == 1); |
| end |
| default: begin end |
| endcase |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Downstream reset generation |
| // |
| generate if (OPT_SELF_RESET) |
| begin |
| |
| initial o_reset = 1; |
| always @(posedge i_clk) |
| if (i_reset || o_fault) |
| o_reset <= 1; |
| else begin |
| o_reset <= 0; |
| if (o_wb_cyc && none_expected |
| &&(i_wb_ack || i_wb_err)) |
| o_reset <= 1; |
| if (timeout) |
| o_reset <= 1; |
| end |
| end else begin |
| |
| always @(*) |
| o_reset = i_reset || o_fault; |
| |
| end endgenerate |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Fault detection |
| // |
| |
| // |
| // A faulty return is a response from the slave at a time, or in |
| // a fashion that it unexpected and violates protocol |
| // |
| always @(*) |
| begin |
| faulty_return = 0; |
| if (expected_returns <= ((o_wb_stb && i_wb_stall) ? 1:0) |
| + ((o_wb_ack || o_wb_err) ? 1:0)) |
| faulty_return = i_wb_ack || i_wb_err; |
| if (i_wb_ack && i_wb_err) |
| faulty_return = 1; |
| if (!i_wb_cyc || !o_wb_cyc) |
| faulty_return = 0; |
| end |
| |
| initial o_fault = 0; |
| always @(posedge i_clk) |
| if (o_reset && !i_wb_cyc) |
| o_fault <= 0; |
| else begin |
| if (o_wb_cyc && faulty_return) |
| o_fault <= 1; |
| if (i_wb_cyc && timeout) |
| o_fault <= 1; |
| end |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Downstream bus signal generation |
| // |
| |
| initial o_wb_cyc = 1'b0; |
| always @(posedge i_clk) |
| if (i_reset || (o_wb_cyc && i_wb_err) || o_reset || o_fault |
| || (i_wb_cyc && o_wb_err)) |
| o_wb_cyc <= 1'b0; |
| else |
| o_wb_cyc <= i_wb_cyc && (o_wb_cyc || i_wb_stb); |
| |
| initial o_wb_stb = 1'b0; |
| always @(posedge i_clk) |
| if (i_reset || (o_wb_cyc && i_wb_err) || o_reset || o_fault || !i_wb_cyc |
| || (i_wb_cyc && o_wb_err)) |
| o_wb_stb <= 1'b0; |
| else if (!o_wb_stb || !i_wb_stall) |
| o_wb_stb <= skd_stb; |
| |
| always @(posedge i_clk) |
| if (!o_wb_stb || !i_wb_stall) |
| begin |
| o_wb_we <= skd_we; |
| o_wb_addr <= skd_addr; |
| o_wb_data <= skd_data; |
| o_wb_sel <= skd_sel; |
| end |
| |
| always @(posedge i_clk) |
| o_wb_idata <= i_wb_idata; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Return signal generation |
| // |
| |
| always @(*) |
| begin |
| skd_stall = (o_wb_stb && i_wb_stall); |
| if (i_reset) |
| skd_stall = 1'b1; |
| if (o_fault) |
| skd_stall = 1'b0; |
| else if (o_reset) |
| skd_stall = 1'b1; |
| end |
| |
| initial o_wb_ack = 0; |
| initial o_wb_err = 0; |
| always @(posedge i_clk) |
| if (i_reset || !i_wb_cyc) |
| begin |
| o_wb_ack <= 1'b0; |
| o_wb_err <= 1'b0; |
| end else if (!o_reset && !o_fault) |
| begin |
| if (timeout || faulty_return || i_wb_err) |
| begin |
| o_wb_ack <= 1'b0; |
| o_wb_err <= (expected_returns > ((o_wb_ack||o_wb_err) ? 1:0)); |
| end else begin |
| o_wb_ack <= o_wb_cyc && i_wb_ack && !i_wb_err; |
| o_wb_err <= 1'b0; |
| end |
| end else begin |
| o_wb_ack <= 1'b0; |
| o_wb_err <= (i_wb_stb && !skd_stall); |
| end |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // 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 |
| // o_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. |
| // |
| // |
| localparam DOWNSTREAM_ACK_DELAY = OPT_TIMEOUT/2-1; |
| localparam UPSTREAM_ACK_DELAY = OPT_TIMEOUT + 3; |
| wire [LGDEPTH-1:0] fwbs_nreqs, fwbs_nacks, fwbs_outstanding; |
| |
| reg f_past_valid; |
| initial f_past_valid = 0; |
| always @(posedge i_clk) |
| f_past_valid <= 1; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Upstream master Bus properties |
| // |
| always @(*) |
| if (!f_past_valid) |
| assume(i_reset); |
| |
| fwb_slave #(.AW(AW), .DW(DW), |
| // .F_MAX_ACK_DELAY(UPSTREAM_ACK_DELAY), |
| .F_LGDEPTH(LGDEPTH), |
| .F_OPT_DISCONTINUOUS(1), |
| .F_OPT_MINCLOCK_DELAY(0) |
| ) wbs (i_clk, i_reset, |
| i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, |
| o_wb_ack, o_wb_stall, o_wb_idata, o_wb_err, |
| fwbs_nreqs, fwbs_nacks, fwbs_outstanding |
| ); |
| |
| always @(*) |
| assert(none_expected == (expected_returns == 0)); |
| |
| // Just so we pass the skid buffer's assumptions ... |
| always @(posedge i_clk) |
| if (f_past_valid && $past(i_wb_stb && o_wb_stall)) |
| assume($stable(i_wb_data)); |
| |
| always @(*) |
| if (i_wb_cyc && !o_wb_err && !o_fault) |
| assert(expected_returns == fwbs_outstanding); |
| |
| generate if (F_OPT_FAULTLESS) |
| begin |
| //////////////////////////////////////////////////////////////// |
| // |
| // Assume the downstream core is protocol compliant, and |
| // prove that o_fault stays low. |
| // |
| wire [LGDEPTH-1:0] fwbm_nreqs, fwbm_nacks,fwbm_outstanding; |
| reg [LGDEPTH-1:0] mreqs, sacks; |
| |
| |
| fwb_master #(.AW(AW), .DW(DW), |
| .F_MAX_ACK_DELAY(DOWNSTREAM_ACK_DELAY), |
| .F_MAX_STALL(DOWNSTREAM_ACK_DELAY), |
| .F_LGDEPTH(LGDEPTH), |
| .F_OPT_DISCONTINUOUS(1), |
| .F_OPT_MINCLOCK_DELAY(0) |
| ) wbm (i_clk, o_reset, |
| o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, |
| o_wb_sel, |
| i_wb_ack, i_wb_stall, i_wb_idata, i_wb_err, |
| fwbm_nreqs, fwbm_nacks, fwbm_outstanding); |
| |
| // |
| // Here's the big proof |
| always @(*) |
| assert(!o_fault); |
| |
| //////////////////////////////////////////////////////////////// |
| // |
| // The following properties are necessary for passing induction |
| // |
| always @(*) |
| if (!i_reset && i_wb_cyc && o_wb_cyc) |
| assert(expected_returns == fwbm_outstanding |
| + (o_wb_stb ? 1:0) |
| + ((o_wb_ack|o_wb_err) ? 1:0)); |
| |
| always @(*) |
| assert(!timeout); |
| |
| always @(*) |
| if (o_wb_err) |
| assert(!o_wb_cyc); |
| |
| always @(*) |
| sacks = fwbs_nacks + (o_wb_ack ? 1:0); |
| |
| always @(*) |
| if (!o_wb_err && i_wb_cyc && o_wb_cyc) |
| assert(sacks == fwbm_nacks); |
| |
| always @(posedge i_clk) |
| if (!i_reset && i_wb_cyc && expected_returns > 0) |
| assert(o_wb_cyc || o_wb_err); |
| |
| always @(*) |
| mreqs = fwbm_nreqs + (o_wb_stb ? 1:0); |
| |
| always @(*) |
| if (!o_wb_err && i_wb_cyc && o_wb_cyc) |
| assert(fwbs_nreqs == mreqs); |
| |
| always @(*) |
| if (i_wb_cyc && o_wb_cyc && fwbs_outstanding > 0) |
| assert(i_wb_we == o_wb_we); |
| |
| always @(*) |
| if (fwbs_nacks != 0 && i_wb_cyc) |
| assert(o_wb_cyc || o_wb_err); |
| |
| end else begin |
| //////////////////////////////////////////////////////////////// |
| // |
| // cover() checks, checks that only make sense if faults are |
| // possible |
| // |
| |
| always @(posedge i_clk) |
| cover(o_fault); |
| |
| always @(posedge i_clk) |
| if (f_past_valid && $past(faulty_return)) |
| cover(o_fault); |
| |
| always @(posedge i_clk) |
| if (f_past_valid && $past(timeout)) |
| cover(o_fault); |
| |
| if (OPT_SELF_RESET) |
| begin |
| //////////////////////////////////////////////////////// |
| // |
| // Prove that we can actually reset the downstream |
| // bus/core as desired |
| // |
| reg faulted; |
| |
| initial faulted = 0; |
| always @(posedge i_clk) |
| if (i_reset) |
| faulted <= 0; |
| else if (o_fault) |
| faulted <= 1; |
| |
| |
| always @(posedge i_clk) |
| cover(faulted && $fell(o_reset)); |
| |
| always @(posedge i_clk) |
| cover(faulted && !o_reset && o_wb_ack); |
| |
| end |
| |
| end endgenerate |
| |
| always @(*) |
| cover(!i_reset && fwbs_nacks > 4); |
| |
| `endif |
| endmodule |
