| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: rtl/wbxclk.v |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: To cross clock domains with a (pipelined) wishbone bus. |
| // |
| // Challenges: |
| // 1. Wishbone has no capacity for back pressure. That means that we'll |
| // need to be careful not to issue more STB requests than ACKs |
| // that will fit in the return buffer. |
| // |
| // Imagine, for example, a faster return clock but a slave that needs |
| // many clocks to get going. During that time, many requests |
| // might be issued. If they all suddenly get returned at once, |
| // flooding the return ACK FIFO, then we have a problem. |
| // |
| // 2. Bus aborts. If we ever have to abort a transaction, that's going |
| // to be a pain. The FIFOs will need to be reset and the |
| // downstream CYC line dropped. This needs to be done |
| // synchronously in both domains, but there's no real choice but |
| // to make the crossing asynchronous. |
| // |
| // 3. Synchronous CYC. Lowering CYC is a normal part of the protocol, as |
| // is raising CYC. CYC is used as a bus locking scheme, so we'll |
| // need to know when it is (properly) lowered downstream. This |
| // can be done by passing a synchronous CYC drop request through |
| // the pipeline in addition to the bus aborts above. |
| // |
| // Status: |
| // Formally verified against a set of bus properties, not yet |
| // used in any real or simulated designs |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // Copyright (C) 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 wbxclk #( |
| // {{{ |
| parameter AW=32, |
| DW=32, |
| DELAY_STALL = 0, |
| LGFIFO = 5, |
| parameter [(LGFIFO-1):0] THRESHOLD = {{(LGFIFO-4){1'b0}},4'h8}, |
| localparam NFF = 2, |
| localparam FIFOLN = (1<<LGFIFO) |
| // }}} |
| ) ( |
| // {{{ |
| input wire i_wb_clk, i_reset, |
| // Input/master bus |
| 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 wire o_wb_stall, |
| output reg o_wb_ack, |
| output reg [(DW-1):0] o_wb_data, |
| output reg o_wb_err, |
| // Delayed bus |
| input wire i_xclk_clk, |
| output reg o_xclk_cyc, |
| output reg o_xclk_stb, |
| output reg o_xclk_we, |
| output reg [(AW-1):0] o_xclk_addr, |
| output reg [(DW-1):0] o_xclk_data, |
| output reg [(DW/8-1):0] o_xclk_sel, |
| input wire i_xclk_stall, |
| input wire i_xclk_ack, |
| input wire [(DW-1):0] i_xclk_data, |
| input wire i_xclk_err |
| // }}} |
| ); |
| |
| // |
| // Declare our signals |
| // {{{ |
| reg wb_active; |
| reg [NFF-2:0] bus_abort_pipe; |
| reg [LGFIFO:0] acks_outstanding; |
| reg ackfifo_single, ackfifo_empty, ackfifo_full; |
| wire ack_stb, err_stb; |
| wire [DW-1:0] ret_wb_data; |
| wire req_fifo_stall, no_returns; |
| // |
| // Verilator lint_off SYNCASYNCNET |
| reg bus_abort; |
| // Verilator lint_on SYNCASYNCNET |
| // |
| wire req_stb, req_fifo_empty; |
| reg xclk_err_state, ign_ackfifo_stall; |
| reg xck_reset; |
| reg [NFF-2:0] xck_reset_pipe; |
| reg r_we; |
| wire req_we; |
| wire [AW-1:0] req_addr; |
| wire [DW-1:0] req_data; |
| wire [DW/8-1:0] req_sel; |
| `ifdef FORMAL |
| wire [LGFIFO:0] ackfifo_prefill, reqfifo_prefill; |
| `endif |
| // }}} |
| |
| // |
| // |
| // On the original wishbone clock ... |
| // |
| // FIFO/queue up our requests |
| // {{{ |
| initial wb_active = 1'b0; |
| always @(posedge i_wb_clk) |
| if (i_reset || !i_wb_cyc) |
| wb_active <= 1'b0; |
| else if (i_wb_stb && !o_wb_stall) |
| wb_active <= 1'b1; |
| |
| initial { bus_abort, bus_abort_pipe } = -1; |
| always @(posedge i_wb_clk) |
| if (i_reset) |
| { bus_abort, bus_abort_pipe } <= -1; |
| else if (!i_wb_cyc && (!ackfifo_empty)) |
| { bus_abort, bus_abort_pipe } <= -1; |
| else if (o_wb_err) |
| { bus_abort, bus_abort_pipe } <= -1; |
| else if (ackfifo_empty) |
| { bus_abort, bus_abort_pipe } <= { bus_abort_pipe, 1'b0 }; |
| `ifdef FORMAL |
| always @(*) |
| if (bus_abort_pipe) |
| assert(bus_abort); |
| `endif |
| // }}} |
| |
| // |
| // The request FIFO itself |
| // {{{ |
| afifo #( |
| `ifdef FORMAL |
| .OPT_REGISTER_READS(0), |
| `endif |
| .NFF(NFF), .LGFIFO(LGFIFO), |
| .WIDTH(2+AW+DW+(DW/8)) |
| ) reqfifo(.i_wclk(i_wb_clk), .i_wr_reset_n(!bus_abort), |
| .i_wr((i_wb_stb&&!o_wb_stall) || (wb_active && !i_wb_cyc)), |
| .i_wr_data({ i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }), |
| .o_wr_full(req_fifo_stall), |
| // |
| .i_rclk(i_xclk_clk), .i_rd_reset_n(!xck_reset), |
| .i_rd(!o_xclk_stb || !i_xclk_stall), |
| .o_rd_data({ req_stb, req_we, req_addr, req_data, req_sel }), |
| .o_rd_empty(req_fifo_empty) |
| `ifdef FORMAL |
| , .f_fill(reqfifo_prefill) |
| `endif |
| ); |
| // }}} |
| |
| // |
| // Downstream bus--issuing requests |
| // {{{ |
| initial { xck_reset, xck_reset_pipe } = -1; |
| always @(posedge i_xclk_clk or posedge bus_abort) |
| if (bus_abort) |
| { xck_reset, xck_reset_pipe } <= -1; |
| else |
| { xck_reset, xck_reset_pipe } <= { xck_reset_pipe, 1'b0 }; |
| `ifdef FORMAL |
| always @(*) |
| if (xck_reset_pipe) |
| assert(xck_reset); |
| `endif |
| |
| initial xclk_err_state = 1'b0; |
| always @(posedge i_xclk_clk) |
| if (xck_reset || (!req_fifo_empty && !req_stb)) |
| xclk_err_state <= 1'b0; |
| else if (o_xclk_cyc && i_xclk_err) |
| xclk_err_state <= 1'b1; |
| |
| initial o_xclk_cyc = 1'b0; |
| always @(posedge i_xclk_clk) |
| if (xck_reset || (o_xclk_cyc && i_xclk_err)) |
| o_xclk_cyc <= 1'b0; |
| else if (!req_fifo_empty && !req_stb) |
| o_xclk_cyc <= 1'b0; |
| else if (!req_fifo_empty && !xclk_err_state) |
| o_xclk_cyc <= req_stb; |
| |
| initial o_xclk_stb = 1'b0; |
| always @(posedge i_xclk_clk) |
| if (xck_reset || (o_xclk_cyc && i_xclk_err) || xclk_err_state) |
| o_xclk_stb <= 1'b0; |
| else if (!o_xclk_stb || !i_xclk_stall) |
| o_xclk_stb <= req_stb && !req_fifo_empty; |
| |
| always @(posedge i_xclk_clk) |
| if ((!o_xclk_stb || !i_xclk_stall) && req_stb && !req_fifo_empty) |
| o_xclk_we <= req_we; |
| |
| always @(posedge i_xclk_clk) |
| if (!o_xclk_stb || !i_xclk_stall) |
| begin |
| o_xclk_addr <= req_addr; |
| o_xclk_data <= req_data; |
| o_xclk_sel <= req_sel; |
| end |
| // }}} |
| |
| |
| // |
| // Request counting |
| // {{{ |
| initial acks_outstanding = 0; |
| initial ackfifo_single = 0; |
| initial ackfifo_empty = 1; |
| initial ackfifo_full = 0; |
| always @(posedge i_wb_clk) |
| if (i_reset || !i_wb_cyc || o_wb_err) |
| begin |
| acks_outstanding <= 0; |
| ackfifo_single <= 0; |
| ackfifo_empty <= 1; |
| ackfifo_full <= 0; |
| end else case({ (i_wb_stb && !o_wb_stall), o_wb_ack }) |
| 2'b10: begin |
| acks_outstanding <= acks_outstanding + 1; |
| ackfifo_empty <= 0; |
| ackfifo_single <= ackfifo_empty; |
| ackfifo_full <= (&acks_outstanding[LGFIFO-1:0]); |
| end |
| 2'b01: begin |
| acks_outstanding <= acks_outstanding - 1; |
| ackfifo_empty <= (acks_outstanding <= 1); |
| ackfifo_single <= (acks_outstanding == 2); |
| ackfifo_full <= 0; |
| end |
| default: begin end |
| endcase |
| |
| `ifdef FORMAL |
| always @(*) |
| begin |
| assert(ackfifo_single == (acks_outstanding == 1)); |
| assert(ackfifo_empty == (acks_outstanding == 0)); |
| assert(ackfifo_full == (acks_outstanding >= (1<<LGFIFO))); |
| assert(acks_outstanding <= (1<<LGFIFO)); |
| end |
| `endif |
| |
| assign o_wb_stall = ackfifo_full || bus_abort || req_fifo_stall; |
| // }}} |
| |
| // |
| // The return FIFO |
| // {{{ |
| afifo #( |
| .OPT_REGISTER_READS(0), |
| .NFF(NFF), .LGFIFO(LGFIFO), |
| .WIDTH(2+DW) |
| ) ackfifo(.i_wclk(i_xclk_clk), .i_wr_reset_n(!xck_reset), |
| .i_wr(o_xclk_cyc && ( i_xclk_ack || i_xclk_err )), |
| .i_wr_data({ i_xclk_ack, i_xclk_err, i_xclk_data }), |
| .o_wr_full(ign_ackfifo_stall), |
| // |
| .i_rclk(i_wb_clk), .i_rd_reset_n(!bus_abort), |
| .i_rd(!no_returns), |
| .o_rd_data({ ack_stb, err_stb, ret_wb_data }), |
| .o_rd_empty(no_returns) |
| `ifdef FORMAL |
| , .f_fill(ackfifo_prefill) |
| `endif |
| ); |
| // }}} |
| |
| // |
| // Final return processing |
| // {{{ |
| initial { o_wb_ack, o_wb_err } = 2'b00; |
| always @(posedge i_wb_clk) |
| if (i_reset || bus_abort || !i_wb_cyc || no_returns || o_wb_err) |
| { o_wb_ack, o_wb_err } <= 2'b00; |
| else |
| { o_wb_ack, o_wb_err } <= { ack_stb, err_stb }; |
| |
| always @(posedge i_wb_clk) |
| o_wb_data <= ret_wb_data; |
| // }}} |
| |
| // Make Verilator happy |
| // {{{ |
| // Verilator lint_off UNUSED |
| wire unused; |
| assign unused = &{ 1'b0, req_fifo_stall, ign_ackfifo_stall }; |
| // Verilator lint_on UNUSED |
| // }}} |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| // Register/net/macro declarations |
| // {{{ |
| `ifdef BMC |
| `define BMC_ASSERT assert |
| `else |
| `define BMC_ASSERT assume |
| `endif |
| |
| (* gclk *) reg gbl_clk; |
| |
| wire [LGFIFO:0] fwb_nreqs, fwb_nacks, fwb_outstanding; |
| wire [LGFIFO:0] fxck_nreqs, fxck_nacks, fxck_outstanding; |
| reg [LGFIFO:0] ackfifo_fill, reqfifo_fill; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Assume a clock |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| (* anyconst *) reg [3:0] fwb_step, fxck_step; |
| reg [3:0] fwb_count, fxck_count; |
| |
| always @(*) |
| begin |
| assume(fwb_step >= 2); |
| assume(fxck_step >= 2); |
| |
| assume(fwb_step <= 4'b1000); |
| assume(fxck_step <= 4'b1000); |
| |
| // assume(fwb_step == 4'b1000); |
| // assume(fxck_step == 4'b0111); |
| assume((fwb_step == 4'b0111) |
| || (fxck_step == 4'b0111)); |
| end |
| |
| always @(posedge gbl_clk) |
| begin |
| fwb_count <= fwb_count + fwb_step; |
| fxck_count <= fxck_count + fxck_step; |
| end |
| |
| always @(*) |
| begin |
| assume(i_wb_clk == fwb_count[3]); |
| assume(i_xclk_clk == fxck_count[3]); |
| end |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // .... |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // |
| // Cross clock stability assumptions |
| // {{{ |
| always @(posedge gbl_clk) |
| if (!$rose(i_wb_clk)) |
| begin |
| assume($stable(i_reset)); |
| |
| assume($stable(i_wb_cyc)); |
| assume($stable(i_wb_stb)); |
| assume($stable(i_wb_we)); |
| assume($stable(i_wb_addr)); |
| assume($stable(i_wb_data)); |
| assume($stable(i_wb_sel)); |
| end |
| |
| always @(posedge gbl_clk) |
| if (!$rose(i_xclk_clk)) |
| begin |
| assume($stable(i_xclk_ack)); |
| assume($stable(i_xclk_err)); |
| assume($stable(i_xclk_data)); |
| assume($stable(i_xclk_stall)); |
| end |
| |
| reg past_wb_clk, past_wb_stb, past_wb_we, |
| past_wb_cyc, past_wb_reset, past_wb_err; |
| reg past_xclk, past_xclk_stall, past_xclk_ack, |
| past_xclk_err; |
| reg [DW-1:0] past_xclk_data; |
| reg f_drop_cyc_request; |
| |
| always @(posedge gbl_clk) |
| begin |
| past_wb_clk <= i_wb_clk; |
| past_wb_reset<= i_reset; |
| past_wb_cyc <= i_wb_cyc; |
| past_wb_stb <= i_wb_stb; |
| past_wb_we <= i_wb_we; |
| past_wb_err <= o_wb_err; |
| end |
| |
| always @(*) |
| if (!i_wb_clk || past_wb_clk) |
| begin |
| assume(past_wb_reset== i_reset); |
| assume(past_wb_cyc == i_wb_cyc); |
| assume(past_wb_stb == i_wb_stb); |
| assume(past_wb_we == i_wb_we); |
| assume(past_wb_err == o_wb_err); |
| end else begin |
| if (past_wb_err && past_wb_cyc) |
| assume(!i_wb_cyc); |
| if (fwb_outstanding > 0) |
| assume(past_wb_we == i_wb_we); |
| end |
| |
| always @(posedge gbl_clk) |
| begin |
| past_xclk <= i_xclk_clk; |
| past_xclk_stall <= i_xclk_stall; |
| past_xclk_data <= i_xclk_data; |
| past_xclk_ack <= i_xclk_ack; |
| past_xclk_err <= i_xclk_err; |
| end |
| |
| always @(*) |
| if (!i_xclk_clk || past_xclk) |
| begin |
| assume(past_xclk_stall == i_xclk_stall); |
| assume(past_xclk_data == i_xclk_data); |
| assume(past_xclk_ack == i_xclk_ack); |
| assume(past_xclk_err == i_xclk_err); |
| end |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Wishbone bus property checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| fwb_slave #(.AW(AW), .DW(DW), |
| .F_LGDEPTH(LGFIFO+1), .F_OPT_DISCONTINUOUS(1) |
| ) slv(i_wb_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_data, o_wb_err, |
| fwb_nreqs, fwb_nacks, fwb_outstanding); |
| |
| fwb_master #(.AW(AW), .DW(DW), |
| .F_LGDEPTH(LGFIFO+1), .F_OPT_DISCONTINUOUS(1), |
| .F_MAX_STALL(4), |
| .F_MAX_ACK_DELAY(7) |
| ) xclkwb(i_xclk_clk, xck_reset, |
| o_xclk_cyc, o_xclk_stb, o_xclk_we, o_xclk_addr, o_xclk_data, o_xclk_sel, |
| i_xclk_ack, i_xclk_stall, i_xclk_data, i_xclk_err, |
| fxck_nreqs, fxck_nacks, fxck_outstanding); |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // (Random/unsorted) properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| always @(*) |
| if (reqfifo_fill != (o_xclk_stb ? 1:0) && !req_stb) |
| assert(ackfifo_fill == 0 || xclk_err_state); |
| |
| always @(*) |
| reqfifo_fill = reqfifo_prefill + (o_xclk_stb ? 1:0); |
| |
| always @(*) |
| ackfifo_fill = ackfifo_prefill // + (no_returns ? 0:1) |
| + ((o_wb_ack || o_wb_err) ? 1:0); |
| |
| always @(*) |
| if (fwb_outstanding > 0) |
| assert(wb_active); |
| |
| always @(*) |
| if (f_drop_cyc_request && !bus_abort && !xclk_err_state) |
| begin |
| // req_stb is low, so cycle line has dropped normally |
| |
| // If the cycle line has since risen, there may be requests |
| // within the request FIFO in addition to the drop-CYC message. |
| if (i_wb_cyc && wb_active) |
| assert(reqfifo_fill == fwb_outstanding + 1); |
| |
| // We wouldn't place a drop CYC message into the FIFO |
| // unless XCLK-CYC was already high |
| assert(o_xclk_cyc && !o_xclk_stb); |
| assert(ackfifo_fill == 0); |
| assert(fxck_outstanding == 0); |
| |
| if (reqfifo_fill > 1) |
| assert(wb_active); |
| else |
| assert(!wb_active); |
| end else if (!bus_abort && xclk_err_state) |
| begin |
| // |
| // Bus error downstream causes an abort |
| assert(fxck_outstanding == 0); |
| assert(xck_reset || wb_active || !i_wb_cyc); |
| assert(!o_xclk_stb); |
| if (ackfifo_fill == 1) |
| assert(no_returns || err_stb); |
| else if (!xck_reset && ackfifo_fill == 1) |
| assert(o_wb_err); |
| end else if (!bus_abort && i_wb_cyc && !xck_reset && !xclk_err_state) |
| begin |
| // |
| // Normal operation in operation |
| // |
| assert(reqfifo_fill <= fwb_outstanding + 1); |
| assert(ackfifo_fill <= fwb_outstanding); |
| assert(fxck_outstanding <= fwb_outstanding); |
| if (o_xclk_cyc) |
| assert(wb_active || f_drop_cyc_request); |
| if (reqfifo_fill == (o_xclk_stb ? 1:0) || req_stb) |
| // Either first request is for strobe, or other |
| // request counters are valid |
| assert(reqfifo_fill + ackfifo_fill |
| + fxck_outstanding == fwb_outstanding); |
| else begin |
| // First request is to drop CYC |
| assert(reqfifo_fill== fwb_outstanding + 1); |
| assert(ackfifo_fill == 0); |
| assert(fxck_outstanding == 0); |
| assert(!o_xclk_stb); |
| assert(o_xclk_cyc); |
| end |
| if (acks_outstanding == 0) |
| assert((reqfifo_fill == 0)||!req_stb); |
| end |
| |
| always @(*) |
| if (o_wb_ack && wb_active) |
| begin |
| assert(o_xclk_cyc || xclk_err_state); |
| assert(!f_drop_cyc_request); |
| assert(!xck_reset || bus_abort); |
| end |
| |
| always @(*) |
| if (!bus_abort && acks_outstanding == 0) |
| assert(reqfifo_fill <= (f_drop_cyc_request ? 1:0) |
| + ((o_xclk_stb && xck_reset) ? 1:0)); |
| |
| always @(*) |
| if (ackfifo_fill != 0) |
| assert(o_xclk_cyc || xck_reset || xclk_err_state); |
| |
| always @(*) |
| if (fxck_outstanding > fwb_outstanding) |
| assert((!i_wb_cyc && wb_active) |
| || i_reset || bus_abort || xck_reset); |
| |
| always @(*) |
| if (!i_reset && xck_reset && !o_xclk_cyc) |
| assert(!i_wb_cyc || fwb_outstanding == reqfifo_fill); |
| |
| always @(*) |
| if (bus_abort && i_wb_cyc) |
| assert(!wb_active); |
| |
| always @(*) |
| if (acks_outstanding < (1<<LGFIFO)) |
| begin |
| // assert(!reqfifo_full); |
| assert(!ackfifo_full); |
| end |
| |
| always @(*) |
| if (!i_reset && !xck_reset && (fwb_outstanding > 0) |
| && ((fxck_outstanding > 0) || o_xclk_stb)) |
| assert(i_wb_we == o_xclk_we); |
| |
| always @(*) |
| if (!i_reset && i_wb_cyc) |
| assert(acks_outstanding == fwb_outstanding); |
| |
| always @(*) |
| if (xclk_err_state) |
| assert(!o_xclk_cyc); |
| |
| always @(*) |
| if (!i_reset && !bus_abort && !i_wb_cyc) |
| begin |
| if (ackfifo_empty) |
| begin |
| if (reqfifo_fill > (o_xclk_stb ? 1:0)) |
| assert(!req_stb || xck_reset); |
| assert(reqfifo_fill <= 1); |
| if (xck_reset && !xck_reset_pipe) |
| assert(!o_xclk_cyc); |
| end else begin |
| // ??? |
| end |
| end |
| |
| always @(*) |
| f_drop_cyc_request = !req_stb |
| && (reqfifo_fill > (o_xclk_stb ? 1:0)); |
| |
| always @(*) |
| if (!i_reset && !xck_reset && !bus_abort && i_wb_cyc) |
| begin |
| if (!o_xclk_cyc && !xclk_err_state) |
| assert(acks_outstanding == reqfifo_fill |
| - (f_drop_cyc_request ? 1:0)); |
| else if (!o_xclk_cyc && xclk_err_state) |
| assert(acks_outstanding >= reqfifo_fill |
| + ackfifo_fill); |
| else if (o_xclk_cyc && !xclk_err_state) |
| begin |
| assert(acks_outstanding >= reqfifo_fill |
| - (f_drop_cyc_request ? 1:0)); |
| assert(acks_outstanding >= ackfifo_fill); |
| assert(acks_outstanding >= fxck_outstanding); |
| assert(acks_outstanding == |
| reqfifo_fill - (((reqfifo_fill > (o_xclk_stb ? 1:0))&&(!req_stb)) ? 1:0) |
| + ackfifo_fill |
| + fxck_outstanding); |
| end |
| if (f_drop_cyc_request) |
| assert(acks_outstanding +1 == reqfifo_fill); |
| else if (reqfifo_fill == 0) |
| assert(!wb_active || o_xclk_cyc || xclk_err_state); |
| end else if (!i_reset && !xck_reset && !bus_abort && f_drop_cyc_request) |
| begin |
| assert(acks_outstanding +1 == reqfifo_fill); |
| assert(ackfifo_fill == 0); |
| assert(fxck_outstanding == 0); |
| assert(!o_xclk_stb); |
| assert(o_xclk_cyc); |
| end |
| |
| |
| always @(*) |
| if (!bus_abort && wb_active && reqfifo_fill == 0 && !xclk_err_state) |
| assert(o_xclk_cyc); |
| |
| always @(*) |
| if (f_drop_cyc_request && !bus_abort) |
| assert(!xck_reset); |
| |
| always @(*) |
| assert(!xclk_err_state || acks_outstanding != 0 || xck_reset); |
| |
| always @(*) |
| if (o_xclk_cyc && !i_wb_cyc) |
| begin |
| // assert(bus_abort || !xclk_err_state); |
| if (!wb_active && !bus_abort && !xck_reset) |
| assert(f_drop_cyc_request); |
| end else if (i_wb_cyc) |
| begin |
| if (wb_active && !xck_reset) |
| assert(o_xclk_cyc || xclk_err_state |
| ||(reqfifo_fill >= acks_outstanding)); |
| end |
| |
| // always @(*) |
| // if (acks_outstanding >= (1<<LGFIFO)) |
| // assert(o_xclk_cyc || xclk_err_state || xck_reset); // !!!! |
| |
| // |
| // !!!!!!!!!!! |
| // |
| // Fig me here |
| always @(*) |
| if (wb_active && !bus_abort && !xck_reset && i_wb_cyc && !xclk_err_state) |
| begin |
| if (reqfifo_fill == 0) |
| assert(o_xclk_cyc); |
| end |
| |
| always @(*) |
| if (fxck_outstanding > 0 || o_xclk_stb) |
| assert(!ign_ackfifo_stall); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Sub properties for the REQ FIFO |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| always @(*) |
| if ((acks_outstanding > 0)&&(reqfifo_fill != (o_xclk_stb ? 1:0))) |
| begin |
| // Something valuable is in the request FIFO |
| if (i_wb_cyc && !f_drop_cyc_request) |
| `BMC_ASSERT(req_we == i_wb_we); |
| else if (req_stb && o_xclk_stb) |
| `BMC_ASSERT(o_xclk_we == req_we); |
| |
| // if (acks_outstanding > 0) |
| if (!o_xclk_cyc || o_xclk_stb || |
| fxck_outstanding > 0 || ackfifo_fill > 0) |
| `BMC_ASSERT(req_stb); |
| end // else the request FIFO is empty, nothing is in it |
| // No assumptions therefore need be made |
| |
| always @(*) |
| if (!bus_abort && reqfifo_fill == acks_outstanding) |
| `BMC_ASSERT(!req_fifo_stall || !f_drop_cyc_request); |
| |
| always @(*) |
| if (!i_reset && o_xclk_cyc && (reqfifo_fill != (o_xclk_stb ? 1:0))) |
| `BMC_ASSERT(!req_stb || req_we == o_xclk_we |
| || fxck_outstanding == 0); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Sub properties for the ACK FIFO |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| always @(*) |
| if (!no_returns) |
| begin |
| `BMC_ASSERT(ack_stb ^ err_stb); |
| |
| if ((ackfifo_fill ==(o_wb_ack ? 2:1)) && xclk_err_state) |
| `BMC_ASSERT(err_stb); |
| else if (ackfifo_fill > (o_wb_ack ? 2:1)) |
| `BMC_ASSERT(!err_stb); |
| end |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| reg cvr_abort; |
| reg [3:0] cvr_replies, cvr_post_abort; |
| |
| initial cvr_abort = 0; |
| always @(posedge i_wb_clk) |
| if (i_reset) |
| cvr_abort <= 0; |
| else if (o_wb_err && acks_outstanding > 2) |
| cvr_abort <= 1; |
| |
| initial cvr_replies = 0; |
| always @(posedge i_wb_clk) |
| if (i_reset) |
| cvr_replies <= 0; |
| else if (o_wb_ack || o_wb_err) |
| cvr_replies <= cvr_replies + 1; |
| |
| initial cvr_post_abort = 0; |
| always @(posedge i_wb_clk) |
| if (i_reset) |
| cvr_post_abort <= 0; |
| else if (cvr_abort && o_wb_ack) |
| cvr_post_abort <= cvr_post_abort + 1; |
| |
| always @(*) |
| begin |
| cover(cvr_replies > 1); // 33 |
| cover(cvr_replies > 3); // 38 |
| cover(cvr_replies > 9); |
| |
| cover(cvr_abort); // 31 |
| cover(cvr_post_abort > 1 && cvr_replies > 1); // 63 |
| cover(cvr_post_abort > 1 && cvr_replies > 2); // 63 |
| cover(cvr_post_abort > 1 && cvr_replies > 3); // 65 |
| cover(cvr_post_abort > 2 && cvr_replies > 3); // 65 |
| cover(cvr_post_abort > 3 && cvr_replies > 3); // 68 |
| cover(cvr_post_abort > 4 && cvr_replies > 3); // 70 |
| cover(cvr_post_abort > 3 && cvr_replies > 6); // 72 |
| end |
| |
| always @(posedge gbl_clk) |
| if (!i_reset) |
| cover(cvr_replies > 9 && !i_wb_clk && acks_outstanding == 0 |
| && fwb_nreqs == fwb_nacks && fwb_nreqs == cvr_replies |
| && !bus_abort && fwb_count != fxck_count); |
| |
| always @(posedge gbl_clk) |
| if (!i_reset) |
| cover(cvr_replies > 9 && !i_wb_clk && acks_outstanding == 0 |
| && fwb_nreqs == fwb_nacks && fwb_nreqs == cvr_replies |
| && !bus_abort && fwb_count != fxck_count |
| && fwb_step != fxck_step); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Simplifying (careless) assumptions |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // None (at present) |
| |
| // }}} |
| `endif |
| // }}} |
| endmodule |