Asynchronous FIFO Assertions For Verifying Data Pushed and Popped

SystemVerilog
, , , , ,
1

I am verifying an Async FIFO and want to verify that the data packets are pushed and popped in the correct order, with the right values.

I wrote a property, which is producing some spurious errors. Where am I going wrong? Thanks in advance. :
wrdata and rddata are actual data read from the bus. The pathnames to the signals, are passed to the property.

property p_check_data (clk_wr, clk_rd, push, pop, wrdata, rddata, full, rst_wr, rst_rd) ;
 logic txdata; // Local variable to store data written on a push
 disable iff (rst_wr | rst_rd)
 @(posedge clk_wr)
 (full !== 1)|->
 @(posedge push) @(posedge clk_wr) (1,txdata = wrdata)  ##1
 @(posedge pop) @(posedge clk_rd)##2 (rddata == txdata);
endproperty
2

In reply to assert_yourself:
Two issues with your code:

  1. Multiple pushes before a pop
    Your code tried to do a push followed by a pop. That does not address the multiple pushes and then a pop. The issue with your code is that if you have 2 or more pushes before a pop, all the pending attempts will execute immediately at the pop and the rdata will not be matched with the local variable data. Upon a push, you need to push the data into a verification queue to be used by SVA (instead of a local variable). Upon a pop, you pop that data.
    To fix this, you need a tag to be attached to the assertion so that all pending assertions are not answered with a single pop.
  2. Multiclocking
    How many clocks do you have? Four? the rd, wr, push, pop clocks?
    No you don’t!

@(posedge clk_wr)
(full !== 1)|->
@(posedge push) @(posedge clk_wr) (1,txdata = wrdata) ##1
@(posedge pop) @(posedge clk_rd)##2 (rddata == txdata);

Below is code that you need to tune, but it will give you the concept. ;


   int tag; 
   int tagQ [$:2**BIT_DEPTH-1];  
// Data queue for verification.
           // Queue, maximum size is 2**BIT_DEPTH
           word_t dataQ [$:2**BIT_DEPTH-1];   // Queue for SVA
           //word_t data_fromQ;  
           function automatic void push_f(word_t data);
             //$display ("%0t %m Push data %0h ", $time, data);
             tad =tag+1; // see comment below 
             tagQ.push_back(tag); // push the tag for SVA
             dataQ.push_back(data); // push to dataQ
           endfunction : push_f

           function automatic word_t pop_f();
              word_t sva_delay_repeat_range_pkg;
                tagQ.pop_font();  // see comment below 
               return dataQ.pop_front(); 
          endfunction : pop_f

// code is unchecked
property p_check_data (clk_wr, clk_rd, push, pop, wrdata, rddata, full, rst_wr, rst_rd) ;
             //logic txdata; // Need a verification Queue declared above 
             int vtag; 
             disable iff (rst_wr | rst_rd)
                     @(posedge clk_wr) (full !== 1) && push|->
                     (1,vtag=tag, push_f(wrdata)) ##1 1 // clock switch 
                     ##[1:$] @(posedge clk_rd) pop && tagQ[1]==vtag ##0 (rddata == pop_f() );
           endproperty

ADDED COMMENTS:
Edited the code, but it still needs tuning. COncept is to push/pop data and tags.
The tags ensure uniqueness when doing pops.

I would like to see your code after you fix it and get it right.
Please share.

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog