##delay and $past() in SVA

SystemVerilog
,
1

I’m a newbie learning SVA. I got confused at the code below.

…
assume property(
@(posedge clk) disable iff(rst)
##2
(A == $past(B))
);
…

Question 1: typically we see “seq_a #Delay seq_b”, meaning at current cycle (t0), seq_a is true. “delay” cycles later, seq_b is true. If there is no seq_a, does it mean regardless of current cycle’s status, “delay” cycles later, seq_b is true?
Question 2: by definition, $past(A) means value of signal A at “previous” cycle. Here “previous” is related to current cycle (t0) or the cycle after #Delay (in this example t2)?
Question 3: what’s the overall behavior of the property? A should be the same value as B 3 cycles earlier?

Thanks!

2

In reply to eda2k4:
A1: Yes,
#Delay seq_b is the same as
1’b1 #Delay seq_b

A2: $past is relative to the current cycle when the expression gets evaluated.

A3: Assuming there is no rst,
(A == $past(B))gets evaluated at t2, t3, t4, etc. using the value of B at t1, t2, t3, etc. respectively. In other words, the value of At is compared to the value of Bt-1.