Usage of $past in System Verilog Assertions

Question

I want to check if the current value of variable is '1' then the previous value of the variable should be '0'. I am using $past in System Verilog Assertions. Here I am checking if cal_frame_mode=1, then it's previous value of cal_frame_mode=0. My code is below. However, I am seeing assertion failure. When I check in the waveform it's behaving correctly. Assertion flags 2 clock after the the first check. How to stop this assertion after checking just one clock cycle?.

property p_NOP_2_RX_CAL;
  @(posedge clk)
  (cal_frame_mode==3'b001) |-> ##2 $past(cal_frame_mode)==3'b000;  
endproperty

assert_nop2cal : assert property(p_NOP_2_RX_CAL);

Answer 1

##2 means wait two clocks. The default of $past looks at the value of the expression one clock back from the current clock (by default this is the clock defined in the property). Therefore:

(cal_frame_mode==3'b001) |-> ##2 $past(cal_frame_mode)==3'b000;

Is equivalent to:

(cal_frame_mode==3'b001) |-> ##1 cal_frame_mode==3'b000;

What you want is: (cal_frame_mode==3'b001) |-> $past(cal_frame_mode)==3'b000; but I'm guessing the reason you had the ##2 is to filter out cal_frame_mode equaling one for two clocks. If so, then the better solution is to add $change or !$stable to the antecedent, this what the check is only performed when the cal_frame_mode changed and the current value is one.

$changed(cal_frame_mode) && (cal_frame_mode==3'b001) |-> $past(cal_frame_mode)==3'b000;

Assertions are documented in IEEE Std 1800-2012 § 16 Assertions
§ 16.9.3 Sampled value functions describes $sample, $rose, $fell, $stable, $changed, and $past in detail
§ 16.12.6 Implication describes |-> and |=>