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

3

Hi Ben,
Would your proposed approach be suitable for formal?

4

NO. Queues and associative arrays are not suitable for formal.
From my book on assertions for FIFO:

module fifo_props (input clk, input reset_n, fifo_if fifo_if);
  timeunit 1ns;
  timeprecision 100ps;

// Activating reset during interesting corner cases
// is covered via cover directives.

  property p_t1_full;  @ (posedge clk) 
    fifo_if.full ##1 reset_n==0;
  endproperty : p_t1_full
  cp_t1_full_1: cover property (p_t1_full);
  

  property p_t2_afull;  @ (posedge clk) 
    fifo_if.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) 
     fifo_if.empty ##1 reset_n==0;
  endproperty : p_t3_empty
  cp_t3_empty_1: cover property (p_t3_empty);
  
  property p_t4_aempty;  @ (posedge clk) 
    fifo_if.almost_empty ##1  reset_n==0;
  endproperty : p_t4_aempty
  cp_t4_aempty_1 : cover property (p_t4_aempty);
  

  property p_push_pop_sequencing;
      @ (posedge clk) fifo_if.push |=> ##[0:$] fifo_if.pop;
  endproperty : p_push_pop_sequencing
     
  // coverage of sequences 
  cp_push_pop_sequencing  : cover property  (p_push_pop_sequencing);
 
  c_qFull :               cover property  ( @ (posedge clk) fifo_if.qFull);
  c_qEmpty  :              cover property  (@ (posedge clk)  fifo_if.qEmpty);
  
  c_qAlmost_empty :       cover property  (@ (posedge clk)  fifo_if.qAlmost_empty);
  c_qAlmost_full :        cover property  (@ (posedge clk)  fifo_if.qAlmost_full);
  
endmodule : fifo_props   

interface fifo_if(input wire clk, reset_n);
  timeunit 1ns;
  timeprecision 100ps;
  import fifo_pkg::*;

  logic push; // push data into the fifo
  logic pop;  // pop data from the fifo
  logic almost_full;  // fifo is at 3/4 maximum level
  logic almost_empty;  // fifo is at 1/4 maximum level
  logic full;  // fifo is at maximum level
  logic empty; // fifo is at the zero level (no data)
  logic error; // fifo push or pop error   
  word_t data_in;
  word_t data_out;

  // local variables for verification purpose
  logic [BIT_DEPTH-1 : 0] wr_ptr = 0;
  logic [BIT_DEPTH-1 : 0] rd_ptr = 0;

  logic fifo_is_full;
  logic fifo_is_empty;
  logic fifo_is_almost_full;
  logic fifo_is_almost_empty;
  
  // FIFO DUV 
  modport fslave_if (output empty,
                     output almost_empty,
                     output almost_full,
                     output full,
                     output data_out,
                     output error,
                     input data_in,
                     input push,
                     input pop);

  // FIFO driver 
   modport fdrvr_if (input empty,
                     input almost_empty,
                     input almost_full,
                     input full,
                     input data_out,
                     input error,
                     output data_in,
                     output push,
                     output pop);
     
  // 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);

   // 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);

  `ifdef SV_3.1a
    property p_error_flag; 
   @ (posedge clk) 
   p_push_error or p_pop_error |=> error;
   endproperty : p_error_flag
   ap_error_flag : assert property (p_error_flag);     
  `endif
  
 
    // sequence definition, use in cover.  FIFO_B.FULL 
  sequence qFull; 
    fifo_is_full;
  endsequence : qFull

  // sequence definition, use in cover.  empty  
  sequence qEmpty; 
      fifo_is_empty;
  endsequence : qEmpty

  // sequence definition, use in cover.  almost_empty   
  sequence qAlmost_empty; 
     fifo_is_almost_empty;
   endsequence : qAlmost_empty

  // sequence definition, use in cover.  almost_full
  sequence qAlmost_full; 
     fifo_is_almost_full;
   endsequence : qAlmost_full

  // Definition of a fifo_b.full fifo, based on environment addresses.
  property p_fifo_full; 
     @ (posedge clk)   qFull |=> full; 
  endproperty : p_fifo_full
  ap_fifo_full : assert property (p_fifo_full);
  
  // Definition of an almost_fifo_b.full fifo, based on environment addresses
  property p_fifo_almost_full; 
     @ (posedge clk)   qAlmost_full |=> almost_full; 
  endproperty : p_fifo_almost_full
  ap_fifo_almost_full : assert property (p_fifo_almost_full);

  // If empty fifo, check empty flag   
  property p_fifo_empty; 
    @ (posedge clk) 
             qEmpty |=> empty; 
  endproperty : p_fifo_empty
  ap_fifo_empty : assert property (p_fifo_empty);
  
  // Flags at reset 
  property p_fifo_ptrs_flags_at_reset; 
    @ (posedge clk) 
       !reset_n |-> almost_empty && ! full && !almost_full && empty; 
  endproperty  : p_fifo_ptrs_flags_at_reset
  ap_fifo_ptrs_flags_at_reset : assert property (p_fifo_ptrs_flags_at_reset);
  
  // Flag at almost_empty state
  property p_fifo_almost_empty; 
    @ (posedge clk)  qAlmost_empty |-> almost_empty;  // BUG: should use |=> !!!! 
  endproperty : p_fifo_almost_empty
  ap_fifo_almost_empty : assert property (p_fifo_almost_empty);

 
  // ------------------------------

  always @ (posedge clk)
  begin : status_flag
    fifo_is_empty = (wr_ptr == rd_ptr);
    fifo_is_full = (wr_ptr - rd_ptr) == FULL;
    fifo_is_almost_full = (wr_ptr - rd_ptr) >= ALMOST_FULL;
    fifo_is_almost_empty = (wr_ptr - rd_ptr) <= ALMOST_EMPTY;
  end : status_flag
  default clocking  @ ( posedge clk );endclocking  
   task push_task (word_t data);
     begin
       $display ("%0t %m Push data %0h ", $time, data);
	   data_in <= data;
	   push <= 1'b1;
	   pop  <= 1'b0;
       	   wr_ptr++;
	   ##1;
      end
    endtask : push_task 

    task pop_task;
      begin
        data_in <= 'X; // unsized Xs 
        push <= 1'b0;
        pop  <= 1'b1;
        rd_ptr++;
        ##1;
       end
    endtask : pop_task
      
    task idle_task (int num_idle_cycles);
      begin
        assert (num_idle_cycles < 10000) else 
          $warning ("%0t %0m idle_task is invoked with LARGE number of idle cycles %0d ",
                    $time, num_idle_cycles); 
        data_in <= 'X; // unsized Xs 
        push <= 1'b0;
        pop  <= 1'b0;
        repeat (num_idle_cycles) ##1;
      end
    endtask : idle_task 


endinterface : fifo_if
5

So then, is it possible to verify the first-in-first-out functionality of the FIFO?
Using local variables to hold the data being pushed, and the address pointers to then check if the data out is the same during a pop isn’t possible as local variables cause performance issues/not allowed depending on local variable size. We can’t have queues to hold the values either to write assertions on. If I wanted to write auxiliary code then it will mostly be a copy of the RTL which defeats the purpose. Is there something I am missing?

6

Yes, you’ll need support logic for a ghost Fifo (golden copy).
Another approach (untested and incorrect as it is written) is to use support logic with local variables. Below is the concept, modified from a different model.

    int data_in, data_out;
    
    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n) begin
          push_count <= 0;
          pop_count <= 0;
        end
        else begin  // RTL updates push and pop counts, not the assertion
          if ($rose(push)) push_count <= push_count + 1;
          if (pop) pop_count <= pop_count + 1;
        end
      end

    property pushpop_unique;
        int v_serving_push_count;
        int v_data;
        @(posedge clk) ($rose(push),  v_serving_push_count=push_count, v_data=data_in) |-> 
             (##[1:5] pop ##1 pop_count==v_serving_push_count) ##0 v_data==data_out; 
    endproperty
    ap_pushpop_unique: assert property(pushpop_unique);