System verilog Assertion fail

SystemVerilog
, ,
1

Hi,
I have a system verilog assertion for scenario - w_addr aligned to clk1 and r_addr aligned to clk2. Assertion should check each posedge of clk1 and collect w_addr. If w_addr+3 or w_addr+2 is equal to 2 clk2 before of r_addr, then enable should be 1.
Output to check is enable and the condition is w_addr+3 || w_addr+2 == past(r_addr,2)
Below code doesn’t work for all scenario. It checks the condition should bbe true in all cases. Can you help to correct the code.

property wr_chk;
int p_wr;
  @(posedge clk1) (1,p_wr=w_addr) ##0
  (p_wr+3 == $(past(r_addr,2,1,@(posedge(clk2)) || p_wr+2 == $(past(r_addr,2,1,@(posedge(clk2)))
  |=> (enable==1);
endproperty
2

In reply to Umamageswari:
Your requirements are totally unclear. From what you wrote, I inferred the following, but for simplicity I removed that 3 occurrence of the w_addr being equal. I my understanding is correct, you can tune your model accordingly.
My understanding:

  1. w_addr is collected for 2 consecutive cycles using clk1
  2. r_addr is collected for 2 consecutive cycles using clk2
  3. if 2 of the collected w_addr have the same value as 2 of the collected r_addr
    then enable should be 1.

module m; 
    int w_addr, r_addr; 
    int w2[0:1];
    int r2[0:1]; 
    always_ff @(posedge clk1) begin
        w2[0] <= w2[1]; 
        w2[1] <= w_addr; 
    end
    always_ff @(posedge clk2) begin
        r2[0] <= r2[1]; 
        r2[1] <= r_addr; 
    end

     property p;
        int vw2[0:1]; 
          @(posedge clk1)  (1, vw2=w2) ##0 w2[0]==w2[1]  // 2 wr addr the same as 
                           @(posedge clk2) vw2[0]==r2[0] && r2[0]== r2[1]) // 2 of the read addr same as waddr 
                        |=> (enable==1) ;  // synchronous to clk2 
     endproperty
endmodule

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

or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh