[AsyncFIFO] Clock crossing domain assertions

SystemVerilog
, ,
3

In reply to ben@SystemVerilog.us:

Could you please explain these two properties:

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

Where is the ‘buffer[ptr]’ defined/declared? Is the array common/visible for these two properties?