What is the use of comparing $past with 0?

SystemVerilog
,
1

In the below assertion what is the reason of comparing the $past with 0? If i dont do that assertion fails. i can workaround it by specifying the number of clocks to do the match. just want to understand.



reg [3:0] cnt=0;
  
  always @ (posedge clk) begin
    cnt <= cnt+1;
  end

property p2;
      @(posedge clk) 
      ((cnt==3) |=> $past (cnt==2)==0);
    endproperty
      
      a20: assert property (p2) 
        $display ("Assertion passed at %d\n",$time);
      else 
        $display("Assertion Failed at %d\n",$time);
    

[\systemverilog]
2

In reply to rag123:

In the below assertion what is the reason of comparing the $past with 0? If i dont do that assertion fails. i can workaround it by specifying the number of clocks to do the match. just want to understand.


reg [3:0] cnt=0;
always @ (posedge clk) begin
cnt <= cnt+1;
end
property p2;
@(posedge clk) 
((cnt==3) |=> $past (cnt==2)==0);
endproperty
a20: assert property (p2) 
$display ("Assertion passed at %d\n",$time);
else 
$display("Assertion Failed at %d\n",$time);
[\systemverilog]




``` verilog

$past (cnt==2)==0

It means, the expression “cnt==2” must be false previous clock. In other words, in previous clock, the cnt value is not 2.

3

In reply to chris90:

whatever value i give the assertion seems to be passing.

4

In reply to rag123:

Yes, according to your assertion code. What are you going to check when you implement this assertion?

5

In reply to rag123:

In reply to chris90:
whatever value i give the assertion seems to be passing.

Issue is with use of |=> non-overlapped operator. Use |-> operator.



//it is passing due to use of |=> non-overlapped operator
//$past(cnt==2) execution happen one clock after (cnt==3) execution. so now cnt=4 and $past(cnt) value is 3.  
// so $past(cnt==2) return 0. hence $past (cnt==2)==0 condition is correct which makes assertion pass.    
property p2;
      @(posedge clk) 
      ((cnt==3) |=> $past (cnt==2)==0);
endproperty


//this should fail.
//(cnt==3) and $past(cnt==2) execution happen on same posedge of clock. 
//cnt value is 2 on previous clock. so $past(cnt==2) is correct and return 1. hence $past (cnt==2)==0 condition isn't correct which leads to assertion failure.   
property p2;
      @(posedge clk) 
      ((cnt==3) |-> $past (cnt==2)==0);
endproperty
6

In reply to Rahulkumar Patel:

Thanks Rahul and Chris !

7

In reply to rag123:

Rahul/Chris,
One more question is i often see SVA syntax as below. what does that really mean is it appending one before the value or just another expression.



reg [3:0] cnt=0;
  
  always @ (posedge clk) begin
    cnt <= cnt+1;
  end

property p3;
realtime stop;
 (1,stop=cnt);
8

In reply to rag123:

In reply to rag123:
Rahul/Chris,
One more question is i often see SVA syntax as below. what does that really mean is it appending one before the value or just another expression.


reg [3:0] cnt=0;
always @ (posedge clk) begin
cnt <= cnt+1;
end
property p3;
realtime stop;
(1,stop=cnt);



(statement1, statement2)

means if statement1 true, statement2 will be executed.