The code below should do the job, but you’ll need other assertions regarding writing on full, reading an empty.
module fifo_async (
// Outputs
wfull, rdata, rempty,
// Inputs
wrst_n, wclk, wen, wdata, rrst_n, rclk, ren
) ;
parameter WIDTH = 8;
output wfull; // Write full
output [WIDTH - 1: 0] rdata; // read data
output rempty; // fifo empty
input wrst_n; // asynchronous active low write reset
input wclk; // write clock input
input wen; // fifo active hi write enable
input [WIDTH-1:0] wdata; // write data
input rrst_n; // read reset active low
input rclk; // fifo read clock
input ren; // fifo read enable (active hi)
property p_async_fifo;
bit[WIDTH-1:0] v_wdata;
@(posedge wclk) (!wfull && wen, v_wdata=wdata) |->
@(posedge rclk) ##[1:$] !rempty && ren ##0 rdata==v_wdata;
endproperty
ap_async_fifo: assert property(p_async_fifo));
Below is code on a sync fifo, but it should help you consider other assertions for your designs (this is from stuff from my books).
/ Activating reset during interesting corner cases
// is covered via cover directives.
property p_t1_full; @ (posedge clk)
full ##1 reset_n==0;
endproperty : p_t1_full
cp_t1_full_1: cover property (p_t1_full);
property p_t2_afull; @ (posedge clk)
almost_full ##1 reset_n==0;
endproperty : p_t2_afull
cp_t2_afull_1: cover property (p_t2_afull);
property p_t3_empty; @ (posedge clk)
empty ##1 reset_n==0;
endproperty : p_t3_empty
cp_t3_empty_1: cover property (p_t3_empty);
property p_t4_aempty; @ (posedge clk)
almost_empty ##1 reset_n==0;
endproperty : p_t4_aempty
cp_t4_aempty_1 : cover property (p_t4_aempty);
// turned unbounded into bounded
property p_push_pop_sequencing;
@ (posedge clk) push |=> ##[0:99] pop;
endproperty : p_push_pop_sequencing
// coverage of sequences
cp_push_pop_sequencing : cover property (p_push_pop_sequencing);
property p_error_flag;
@ (posedge clk)
(push && full && !pop) || (pop && empty) == error;
endproperty : p_error_flag
ap_error_flag : assert property (p_error_flag);
begin: no_error
// never a push and full and no pop
property p_push_error;
@ (posedge clk)
not (push && full && !pop);
endproperty : p_push_error
// ap_push_error : assert property (p_push_error);
ap_push_error : assume property (p_push_error);
// never a pop on empty
property p_pop_error;
@ (posedge clk)
not (pop && empty);
endproperty : p_pop_error
// ap_pop_error : assert property (p_pop_error);
ap_pop_error : assume property (p_pop_error);
property p_push_data;
word_t data;
logic [BIT_DEPTH-1 : 0] ptr;
(push, data = data_in, ptr = wr_ptr) |=> buffer[ptr] == data;
endproperty : p_push_data
ap_push_data : assert property (@ (posedge clk) disable iff (!reset_n) p_push_data);
property p_pop_data; //===== From book:
pop |-> data_out == buffer[rd_ptr];
endproperty : p_pop_data
ap_pop_data : assert property (@ (posedge clk) disable iff (!reset_n) p_pop_data);
//===== correct pointer manuipulation:
property p_push;
@ (posedge clk) disable iff (!reset_n)
push |=> wr_ptr == ($past(wr_ptr) + 1 ) % DEPTH;
endproperty : p_push
ap_push : assert property (p_push);
property p_pop;
@ (posedge clk) disable iff (!reset_n)
pop |=> rd_ptr == ($past(rd_ptr) + 1 ) % DEPTH;
endproperty : p_pop
ap_pop: assert property (p_pop);
property p_nopush;
@ (posedge clk) disable iff (!reset_n)
!push |=> wr_ptr == $past(wr_ptr);
endproperty : p_nopush
ap_nopush : assert property (p_nopush);
property p_nopop;
@ (posedge clk) disable iff (!reset_n)
!pop |=> rd_ptr == $past(rd_ptr);
endproperty : p_nopop
ap_nopop: assert property (p_nopop);
end // no_error
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115