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