Hi all. I am trying to verify an asynchronous FIFO. Here is my code (it isn’t complete)
module afifo_sva #(
parameter DATA_WIDTH = 64,
parameter FIFO_DEPTH = 16
)
(
// All signals of the DUT, as INPUTS only
input logic i_rclk,
input logic i_wclk,
input logic i_rrst,
input logic i_wrst,
input logic i_wr_en,
input logic i_rd_en,
input [DATA_WIDTH-1:0] i_wdata,
input logic [DATA_WIDTH-1:0] o_rdata,
input logic o_wfull,
input logic o_rempty
);
localparam PTR_WIDTH = $clog2(FIFO_DEPTH);
// Properties for Empty flag
// Reset
property p_empty_on_rrst;
@(posedge i_rclk)
i_rrst |-> ##[0:1] o_rempty;
endproperty
// Read last
property p_read_makes_fifo_empty;
@(posedge i_rclk)
disable iff (i_rrst)
(i_rd_en && !o_rempty &&
(testbench_top.dut.rgraynext == testbench_top.dut.rq2_wgray))
|=> o_rempty;
endproperty
// Write into empty FIFO
// Sequence to detect i_wr_en at write clock.
sequence s_wr_while_empty;
@(posedge i_wclk)
i_wr_en && o_rempty;
endsequence
sequence s_fifo_not_empty;
@(posedge i_rclk)
!o_rempty;
endsequence
property p_wr_en_when_empty;
disable iff (i_wrst || i_rrst)
s_wr_while_empty ##1 s_fifo_not_empty;
endproperty
// Properties for Full flag
// Reset
property p_full_on_wrst;
@(posedge i_wclk)
i_wrst |-> ##[0:1] !o_wfull;
endproperty
// Pointers
property p_write_makes_fifo_full;
@(posedge i_wclk)
disable iff (i_wrst)
(i_wr_en && !o_wfull &&
(testbench_top.dut.wgraynext == {~testbench_top.dut.wq2_rgray[PTR_WIDTH:PTR_WIDTH-1],
testbench_top.dut.wq2_rgray[PTR_WIDTH-2:0]}))
|=> o_wfull;
endproperty
// Assertions
a_empty_on_rrst: assert property (p_empty_on_rrst)
else $fatal(1, "Empty flag did not assert on reset");
a_full_on_wrst: assert property (p_full_on_wrst)
else $fatal(1, "Full flag did not assert on reset");
a_write_makes_fifo_full: assert property (p_write_makes_fifo_full)
else $error("FIFO did not assert full after final valid write");
a_read_makes_fifo_empty: assert property (p_read_makes_fifo_empty)
else $error("FIFO did not assert empty after reading last item");
a_wr_en_when_empty: assert property (p_wr_en_when_empty)
$display("T=%0t PASS: FIFO became non-empty after writing into empty FIFO", $time);
else
$fatal(1, "T=%0t FAIL: FIFO stayed empty after writing into empty FIFO", $time);
endmodule
The assertion “a_wr_en_when_empty” (Write to empty fifo test) isn’t ever triggered. I have also tried the opposite conditions (o_rempty instead of !op_rempty), to no avail. Could someone point out where I might be going wrong? This is my first time using assertions.