| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: afifo.v |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: A basic asynchronous FIFO. |
| // |
| // 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 afifo #( |
| // {{{ |
| // LGFIFO is the log based-two of the number of entries |
| // in the FIFO, log_2(fifo size) |
| parameter LGFIFO = 3, |
| // |
| // WIDTH is the number of data bits in each entry |
| parameter WIDTH = 16, |
| // |
| // NFF is the number of flip flops used to cross clock domains. |
| // 2 is a minimum. Some applications appreciate the better |
| parameter NFF = 2, |
| // |
| // This core can either write on the positive edge of the clock |
| // or the negative edge. Set WRITE_ON_POSEDGE (the default) |
| // to write on the positive edge of the clock. |
| parameter [0:0] WRITE_ON_POSEDGE = 1'b1, |
| // |
| // Many logic elements can read from memory asynchronously. |
| // This burdens any following logic. By setting |
| // OPT_REGISTER_READS, we force all reads to be synchronous and |
| // not burdened by any logic. You can spare a clock of latency |
| // by clearing this register. |
| parameter [0:0] OPT_REGISTER_READS = 1'b1, |
| // |
| // MSB = most significant bit of the FIFO address vector. It's |
| // just short-hand for LGFIFO, and won't work any other way. |
| parameter MSB = LGFIFO |
| // }}} |
| ) ( |
| // {{{ |
| // |
| // The (incoming) write data interface |
| input wire i_wclk, i_wr_reset_n, i_wr, |
| input wire [WIDTH-1:0] i_wr_data, |
| output reg o_wr_full, |
| // |
| // The (incoming) write data interface |
| input wire i_rclk, i_rd_reset_n, i_rd, |
| output reg [WIDTH-1:0] o_rd_data, |
| output reg o_rd_empty |
| `ifdef FORMAL |
| , output reg [LGFIFO:0] f_fill |
| `endif |
| // }}} |
| ); |
| |
| // Register/net declarations |
| // {{{ |
| |
| reg [WIDTH-1:0] mem [(1<<LGFIFO)-1:0]; |
| reg [LGFIFO:0] rd_addr, wr_addr, |
| rd_wgray, wr_rgray; |
| wire [LGFIFO:0] next_rd_addr, next_wr_addr; |
| reg [LGFIFO:0] rgray, wgray; |
| (* ASYNC_REG = "TRUE" *) reg [(LGFIFO+1)*(NFF-1)-1:0] |
| rgray_cross, wgray_cross; |
| wire wclk; |
| reg [WIDTH-1:0] lcl_rd_data; |
| reg lcl_read, lcl_rd_empty; |
| // }}} |
| |
| // wclk - Write clock generation |
| // {{{ |
| generate if (WRITE_ON_POSEDGE) |
| begin |
| |
| assign wclk = i_wclk; |
| |
| end else begin |
| |
| assign wclk = !i_wclk; |
| |
| end endgenerate |
| // }}} |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Write to and read from memory |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // wr_addr, wgray |
| // {{{ |
| assign next_wr_addr = wr_addr + 1; |
| always @(posedge wclk or negedge i_wr_reset_n) |
| if (!i_wr_reset_n) |
| begin |
| wr_addr <= 0; |
| wgray <= 0; |
| end else if (i_wr && !o_wr_full) |
| begin |
| wr_addr <= next_wr_addr; |
| wgray <= next_wr_addr ^ (next_wr_addr >> 1); |
| end |
| // }}} |
| |
| // Write to memory |
| // {{{ |
| always @(posedge wclk) |
| if (i_wr && !o_wr_full) |
| mem[wr_addr[LGFIFO-1:0]] <= i_wr_data; |
| // }}} |
| |
| // rd_addr, rgray |
| // {{{ |
| assign next_rd_addr = rd_addr + 1; |
| always @(posedge i_rclk or negedge i_rd_reset_n) |
| if (!i_rd_reset_n) |
| begin |
| rd_addr <= 0; |
| rgray <= 0; |
| end else if (lcl_read && !lcl_rd_empty) |
| begin |
| rd_addr <= next_rd_addr; |
| rgray <= next_rd_addr ^ (next_rd_addr >> 1); |
| end |
| // }}} |
| |
| // Read from memory |
| // {{{ |
| always @(*) |
| lcl_rd_data = mem[rd_addr[LGFIFO-1:0]]; |
| // }}} |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cross clock domains |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // read pointer -> wr_rgray |
| // {{{ |
| always @(posedge wclk or negedge i_wr_reset_n) |
| if (!i_wr_reset_n) |
| { wr_rgray, rgray_cross } <= 0; |
| else |
| { wr_rgray, rgray_cross } <= { rgray_cross, rgray }; |
| // }}} |
| |
| // write pointer -> rd_wgray |
| // {{{ |
| always @(posedge i_rclk or negedge i_rd_reset_n) |
| if (!i_rd_reset_n) |
| { rd_wgray, wgray_cross } <= 0; |
| else |
| { rd_wgray, wgray_cross } <= { wgray_cross, wgray }; |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Flag generation |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| always @(*) |
| o_wr_full = (wr_rgray == { ~wgray[MSB:MSB-1], wgray[MSB-2:0] }); |
| |
| always @(*) |
| lcl_rd_empty = (rd_wgray == rgray); |
| |
| // o_rd_empty, o_rd_data |
| // {{{ |
| generate if (OPT_REGISTER_READS) |
| begin |
| // {{{ |
| always @(*) |
| lcl_read = (o_rd_empty || i_rd); |
| |
| always @(posedge i_rclk or negedge i_rd_reset_n) |
| if (!i_rd_reset_n) |
| o_rd_empty <= 1'b1; |
| else if (lcl_read) |
| o_rd_empty <= lcl_rd_empty; |
| |
| always @(posedge i_rclk) |
| if (lcl_read) |
| o_rd_data <= lcl_rd_data; |
| // }}} |
| end else begin |
| // {{{ |
| always @(*) |
| lcl_read = i_rd; |
| |
| always @(*) |
| o_rd_empty = lcl_rd_empty; |
| |
| always @(*) |
| o_rd_data = lcl_rd_data; |
| // }}} |
| end endgenerate |
| // }}} |
| // }}} |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| // Start out with some register/net/macro declarations, f_past_valid,etc |
| // {{{ |
| `ifdef AFIFO |
| `define ASSERT assert |
| `define ASSUME assume |
| `else |
| `define ASSERT assert |
| `define ASSUME assert |
| `endif |
| (* gclk *) reg gbl_clk; |
| reg f_past_valid_gbl, f_past_valid_rd, |
| f_rd_in_reset, f_wr_in_reset; |
| reg [WIDTH-1:0] past_rd_data, past_wr_data; |
| reg past_wr_reset_n, past_rd_reset_n, |
| past_rd_empty, past_wclk, past_rclk, past_rd; |
| reg [(LGFIFO+1)*(NFF-1)-1:0] f_wcross, f_rcross; |
| reg [LGFIFO:0] f_rd_waddr, f_wr_raddr; |
| reg [LGFIFO:0] f_rdcross_fill [NFF-1:0]; |
| reg [LGFIFO:0] f_wrcross_fill [NFF-1:0]; |
| |
| |
| initial f_past_valid_gbl = 1'b0; |
| always @(posedge gbl_clk) |
| f_past_valid_gbl <= 1'b1; |
| |
| initial f_past_valid_rd = 1'b0; |
| always @(posedge i_rclk) |
| f_past_valid_rd <= 1'b1; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Reset checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| initial f_wr_in_reset = 1'b1; |
| always @(posedge wclk or negedge i_wr_reset_n) |
| if (!i_wr_reset_n) |
| f_wr_in_reset <= 1'b1; |
| else |
| f_wr_in_reset <= 1'b0; |
| |
| initial f_rd_in_reset = 1'b1; |
| always @(posedge i_rclk or negedge i_rd_reset_n) |
| if (!i_rd_reset_n) |
| f_rd_in_reset <= 1'b1; |
| else |
| f_rd_in_reset <= 1'b0; |
| |
| // |
| // Resets are ... |
| // 1. Asserted always initially, and ... |
| always @(*) |
| if (!f_past_valid_gbl) |
| begin |
| `ASSUME(!i_wr_reset_n); |
| `ASSUME(!i_rd_reset_n); |
| end |
| |
| // 2. They only ever become active together |
| always @(*) |
| if (past_wr_reset_n && !i_wr_reset_n) |
| `ASSUME(!i_rd_reset_n); |
| |
| always @(*) |
| if (past_rd_reset_n && !i_rd_reset_n) |
| `ASSUME(!i_wr_reset_n); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Synchronous signal assumptions |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| always @(posedge gbl_clk) |
| begin |
| past_wr_reset_n <= i_wr_reset_n; |
| past_rd_reset_n <= i_rd_reset_n; |
| |
| past_wclk <= wclk; |
| past_rclk <= i_rclk; |
| |
| past_rd <= i_rd; |
| past_rd_data <= lcl_rd_data; |
| past_wr_data <= i_wr_data; |
| |
| past_rd_empty<= lcl_rd_empty; |
| end |
| |
| // |
| // Read side may be assumed to be synchronous |
| always @(*) |
| if (f_past_valid_gbl && i_rd_reset_n && (past_rclk || !i_rclk)) |
| // i.e. if (!$rose(i_rclk)) |
| `ASSUME(i_rd == past_rd); |
| |
| always @(*) |
| if (f_past_valid_rd && !f_rd_in_reset && !lcl_rd_empty |
| &&(past_rclk || !i_rclk)) |
| begin |
| `ASSERT(lcl_rd_data == past_rd_data); |
| `ASSERT(lcl_rd_empty == past_rd_empty); |
| end |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Fill checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| always @(*) |
| f_fill = wr_addr - rd_addr; |
| |
| always @(*) |
| if (!f_wr_in_reset) |
| `ASSERT(f_fill <= { 1'b1, {(MSB){1'b0}} }); |
| |
| always @(*) |
| if (wr_addr == rd_addr) |
| `ASSERT(lcl_rd_empty); |
| |
| always @(*) |
| if ((!f_wr_in_reset && !f_rd_in_reset) |
| && wr_addr == { ~rd_addr[MSB], rd_addr[MSB-1:0] }) |
| `ASSERT(o_wr_full); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Induction checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // f_wr_in_reset -- write logic is in its reset state |
| // {{{ |
| always @(*) |
| if (f_wr_in_reset) |
| begin |
| `ASSERT(wr_addr == 0); |
| `ASSERT(wgray_cross == 0); |
| |
| `ASSERT(rd_addr == 0); |
| `ASSERT(rgray_cross == 0); |
| `ASSERT(rd_wgray == 0); |
| |
| `ASSERT(lcl_rd_empty); |
| `ASSERT(!o_wr_full); |
| end |
| // }}} |
| |
| // f_rd_in_reset -- read logic is in its reset state |
| // {{{ |
| always @(*) |
| if (f_rd_in_reset) |
| begin |
| `ASSERT(rd_addr == 0); |
| `ASSERT(rgray_cross == 0); |
| `ASSERT(rd_wgray == 0); |
| |
| `ASSERT(lcl_rd_empty); |
| end |
| // }}} |
| |
| // f_wr_raddr -- a read address to match the gray values |
| // {{{ |
| always @(posedge wclk or negedge i_wr_reset_n) |
| if (!i_wr_reset_n) |
| { f_wr_raddr, f_rcross } <= 0; |
| else |
| { f_wr_raddr, f_rcross } <= { f_rcross, rd_addr }; |
| // }}} |
| |
| // f_rd_waddr -- a write address to match the gray values |
| // {{{ |
| always @(posedge i_rclk or negedge i_rd_reset_n) |
| if (!i_rd_reset_n) |
| { f_rd_waddr, f_wcross } <= 0; |
| else |
| { f_rd_waddr, f_wcross } <= { f_wcross, wr_addr }; |
| // }}} |
| |
| integer k; |
| |
| // wgray check |
| // {{{ |
| always @(*) |
| `ASSERT((wr_addr ^ (wr_addr >> 1)) == wgray); |
| // }}} |
| |
| // wgray_cross check |
| // {{{ |
| always @(*) |
| for(k=0; k<NFF-1; k=k+1) |
| `ASSERT((f_wcross[k*(LGFIFO+1) +: LGFIFO+1] |
| ^ (f_wcross[k*(LGFIFO+1)+: LGFIFO+1]>>1)) |
| == wgray_cross[k*(LGFIFO+1) +: LGFIFO+1]); |
| // }}} |
| |
| // rgray check |
| // {{{ |
| always @(*) |
| `ASSERT((rd_addr ^ (rd_addr >> 1)) == rgray); |
| // }}} |
| |
| // rgray_cross check |
| // {{{ |
| always @(*) |
| for(k=0; k<NFF-1; k=k+1) |
| `ASSERT((f_rcross[k*(LGFIFO+1) +: LGFIFO+1] |
| ^ (f_rcross[k*(LGFIFO+1) +: LGFIFO+1]>>1)) |
| == rgray_cross[k*(LGFIFO+1) +: LGFIFO+1]); |
| // }}} |
| |
| // wr_rgray |
| // {{{ |
| always @(*) |
| `ASSERT((f_wr_raddr ^ (f_wr_raddr >> 1)) == wr_rgray); |
| // }}} |
| |
| // rd_wgray |
| // {{{ |
| always @(*) |
| `ASSERT((f_rd_waddr ^ (f_rd_waddr >> 1)) == rd_wgray); |
| // }}} |
| |
| // f_rdcross_fill |
| // {{{ |
| always @(*) |
| for(k=0; k<NFF-1; k=k+1) |
| f_rdcross_fill[k] = f_wcross[k*(LGFIFO+1) +: LGFIFO+1] |
| - rd_addr; |
| |
| always @(*) |
| f_rdcross_fill[NFF-1] = f_rd_waddr - rd_addr; |
| |
| always @(*) |
| for(k=0; k<NFF; k=k+1) |
| `ASSERT(f_rdcross_fill[k] <= { 1'b1, {(LGFIFO){1'b0}} }); |
| |
| always @(*) |
| for(k=1; k<NFF; k=k+1) |
| `ASSERT(f_rdcross_fill[k] <= f_rdcross_fill[k-1]); |
| always @(*) |
| `ASSERT(f_rdcross_fill[0] <= f_fill); |
| // }}} |
| |
| // f_wrcross_fill |
| // {{{ |
| always @(*) |
| for(k=0; k<NFF-1; k=k+1) |
| f_wrcross_fill[k] = wr_addr - |
| f_rcross[k*(LGFIFO+1) +: LGFIFO+1]; |
| |
| always @(*) |
| f_wrcross_fill[NFF-1] = wr_addr - f_wr_raddr; |
| |
| always @(*) |
| for(k=0; k<NFF; k=k+1) |
| `ASSERT(f_wrcross_fill[k] <= { 1'b1, {(LGFIFO){1'b0}} }); |
| |
| always @(*) |
| for(k=1; k<NFF; k=k+1) |
| `ASSERT(f_wrcross_fill[k] >= f_wrcross_fill[k-1]); |
| always @(*) |
| `ASSERT(f_wrcross_fill[0] >= f_fill); |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Clock generation |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Here's the challenge: if we use $past with any of our clocks, such |
| // as to determine stability or any such, the proof takes forever, and |
| // we need to guarantee a minimum number of transitions within the |
| // depth of the proof. If, on the other hand, we build our own $past |
| // primitives--we can then finish much faster and be successful on |
| // any depth of proof. |
| |
| // pre_xclk is what the clock will become on the next global clock edge. |
| // By using it here, we can check things @(*) instead of |
| // @(posedge gbl_clk). Further, we can check $rose(pre_xclk) (or $fell) |
| // and essentially check things @(*) but while using @(global_clk). |
| // In other words, we can transition on @(posedge gbl_clk), but stay |
| // in sync with the data--rather than being behind by a clock. |
| // now_xclk is what the clock is currently. |
| // |
| (* anyseq *) reg pre_wclk, pre_rclk; |
| reg now_wclk, now_rclk; |
| always @(posedge gbl_clk) |
| begin |
| now_wclk <= pre_wclk; |
| now_rclk <= pre_rclk; |
| end |
| |
| always @(*) |
| begin |
| assume(i_wclk == now_wclk); |
| assume(i_rclk == now_rclk); |
| end |
| |
| always @(posedge gbl_clk) |
| assume(i_rclk == $past(pre_rclk)); |
| |
| // Assume both clocks start idle |
| // {{{ |
| always @(*) |
| if (!f_past_valid_gbl) |
| begin |
| assume(!pre_wclk && !wclk); |
| assume(!pre_rclk && !i_rclk); |
| end |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Formal contract check --- the twin write test |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // Tracking register declarations |
| // {{{ |
| reg [WIDTH-1:0] f_first, f_next; |
| (* anyconst *) reg [LGFIFO:0] f_addr; |
| reg [LGFIFO:0] f_next_addr; |
| reg f_first_in_fifo, f_next_in_fifo; |
| reg [LGFIFO:0] f_to_first, f_to_next; |
| reg [1:0] f_state; |
| |
| always @(*) |
| f_next_addr = f_addr + 1; |
| // }}} |
| |
| // distance_to*, *_in_fifo |
| // {{{ |
| always @(*) |
| begin |
| f_to_first = f_addr - rd_addr; |
| |
| f_first_in_fifo = 1'b1; |
| if ((f_to_first >= f_fill)||(f_fill == 0)) |
| f_first_in_fifo = 1'b0; |
| |
| if (mem[f_addr] != f_first) |
| f_first_in_fifo = 1'b0; |
| |
| // |
| // Check the second item |
| // |
| |
| f_to_next = f_next_addr - rd_addr; |
| f_next_in_fifo = 1'b1; |
| if ((f_to_next >= f_fill)||(f_fill == 0)) |
| f_next_in_fifo = 1'b0; |
| |
| if (mem[f_next_addr] != f_next) |
| f_next_in_fifo = 1'b0; |
| end |
| // }}} |
| |
| // f_state -- generate our state variable |
| // {{{ |
| initial f_state = 0; |
| always @(posedge gbl_clk) |
| if (!i_wr_reset_n) |
| f_state <= 0; |
| else case(f_state) |
| 2'b00: if (($rose(pre_wclk))&& i_wr && !o_wr_full &&(wr_addr == f_addr)) |
| begin |
| f_state <= 2'b01; |
| f_first <= i_wr_data; |
| end |
| 2'b01: if ($rose(pre_rclk)&& lcl_read && rd_addr == f_addr) |
| f_state <= 2'b00; |
| else if ($rose(pre_wclk) && i_wr && !o_wr_full ) |
| begin |
| f_state <= 2'b10; |
| f_next <= i_wr_data; |
| end |
| 2'b10: if ($rose(pre_rclk) && lcl_read && !lcl_rd_empty && rd_addr == f_addr) |
| f_state <= 2'b11; |
| 2'b11: if ($rose(pre_rclk) && lcl_read && !lcl_rd_empty && rd_addr == f_next_addr) |
| f_state <= 2'b00; |
| endcase |
| // }}} |
| |
| // f_state invariants |
| // {{{ |
| always @(*) |
| if (i_wr_reset_n) case(f_state) |
| 2'b00: begin end |
| 2'b01: begin |
| `ASSERT(f_first_in_fifo); |
| `ASSERT(wr_addr == f_next_addr); |
| `ASSERT(f_fill >= 1); |
| end |
| 2'b10: begin |
| `ASSERT(f_first_in_fifo); |
| `ASSERT(f_next_in_fifo); |
| if (!lcl_rd_empty && (rd_addr == f_addr)) |
| `ASSERT(lcl_rd_data == f_first); |
| `ASSERT(f_fill >= 2); |
| end |
| 2'b11: begin |
| `ASSERT(rd_addr == f_next_addr); |
| `ASSERT(f_next_in_fifo); |
| `ASSERT(f_fill >= 1); |
| if (!lcl_rd_empty) |
| `ASSERT(lcl_rd_data == f_next); |
| end |
| endcase |
| // }}} |
| |
| generate if (OPT_REGISTER_READS) |
| begin |
| reg past_o_rd_empty; |
| |
| always @(posedge gbl_clk) |
| past_o_rd_empty <= o_rd_empty; |
| |
| always @(posedge gbl_clk) |
| if (f_past_valid_gbl && i_rd_reset_n) |
| begin |
| if ($past(!o_rd_empty && !i_rd && i_rd_reset_n)) |
| `ASSERT($stable(o_rd_data)); |
| end |
| |
| always @(posedge gbl_clk) |
| if (!f_rd_in_reset && i_rd_reset_n && i_rclk && !past_rclk) |
| begin |
| if (past_o_rd_empty) |
| `ASSERT(o_rd_data == past_rd_data); |
| if (past_rd) |
| `ASSERT(o_rd_data == past_rd_data); |
| end |
| |
| end endgenerate |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| reg cvr_full; |
| |
| |
| always @(*) |
| if (i_wr_reset_n && i_rd_reset_n) |
| begin |
| cover(o_rd_empty); |
| cover(!o_rd_empty); |
| cover(f_state == 2'b01); |
| cover(f_state == 2'b10); |
| cover(f_state == 2'b11); |
| cover(&f_fill[MSB-1:0]); |
| |
| cover(i_rd); |
| cover(i_rd && !o_rd_empty); |
| end |
| |
| initial cvr_full = 1'b0; |
| always @(posedge gbl_clk) |
| if (!i_wr_reset_n) |
| cvr_full <= 1'b0; |
| else if (o_wr_full) |
| cvr_full <= 1'b1; |
| |
| |
| always @(*) |
| if (f_past_valid_gbl) |
| begin |
| cover(o_wr_full); |
| cover(o_rd_empty && cvr_full); |
| cover(o_rd_empty && f_fill == 0 && cvr_full); |
| end |
| |
| // }}} |
| `endif |
| // }}} |
| endmodule |