Asynchronous FIFO Multithreaded assertion

SystemVerilog
, ,
2

In reply to curious_learner:


@(posedge r_clk) disable iff (!w_rst_n || !r_rst_n)
     (r_valid && r_ready, p_rbaddr=r_baddr, p_rdata=r_data) ##0 
      @(posedge w_clk) (w_valid && w_ready, p_wbaddr=w_baddr, p_wdata=w_data) |=> 
                    (w_memory[p_wbaddr] === p_wdata) && (r_memory[p_rbaddr] === p_rdata);

I see no problem with your code. The consequent uses the w_clk.
What issue do you experience?

Sims OK. That module declares 2 clocks that are synchronous.

The issue I see is with your FIFO model is the memory model. Specifically, an Async fifo is implemented with ONE common memory, as shown below. Your SVA uses 2 memories:
a w_memory and a r_memory. I am puzzled.

951×681 67.2 KB

This fifo is explained in my book
Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
Code is available at
http://systemverilog.us/realchip_code.zip
ch3/fifo_async.v // Verilog code (before SystemVerilog days
ch3/fifo_async2.v
ch3/fifo_asyn_tb.v

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: * Component Design by Example https://rb.gy/9tcbhl
  1. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/