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
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