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.

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:

w_addr is collected for 2 consecutive cycles using clk1

r_addr is collected for 2 consecutive cycles using clk2

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.