Writing a property for Program Counter increment

I am new to Systemverilog assertion and i am trying to write a property for the program counter which is “When the pc increments, it increments by 1”. I have written a property below, can some one check and let me know if i made a mistake

It has a input signal inc_pc, load_pc , sys_clk, d and output of [11:0]pc_cnt

property pc_incrementing_check;
@(posedge sys_clk) $rose(inc_pc) |=> ((pc_cnt - $past(pc_cnt, 1)) == 1);
endproperty

In reply to gounder:
The $rose should not be used in this case because at every cycle inc_pc==1’b1 you want to pc_cnt to be incremented. I discussed in this forum that though
|=> is same as ##1 1’b1 |->
I prefer to write |-> ##1 sequence // reads as implies at next cycle the sequence.
It’s really a matter of preference.


// My first choice because it is forward looking 
property pc_incrementing_check;inc_pc
@(posedge sys_clk) inc_pc |-> ##1 pc_cnt==$past(pc_cnt) +1'b1);
endproperty

// OK too, a different way at looking at the property 
property pc_incrementing_check;inc_pc
@(posedge sys_clk) inc_pc |=> ((pc_cnt - $past(pc_cnt, 1)) == 1);
endproperty

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/