But I want this property to modify and take care the below requirement as well.
** o_prog_out will get decrement by 1 until it reach to (prog_trim - freq_dec).(means once the prog_out will reach to (prog_trim - freq_dec). it should stop the decrement)
* But I want this property to modify and take care the below requirement as well.
** o_prog_out will get decrement by 1 until it reach to (prog_trim - freq_dec).
(means once the prog_out will reach to (prog_trim - freq_dec). it should stop the decrement) */
//[Ben] Additional requirements: After the stop of the decrement, 0_prog_out is stable until cond_finish
// My assumption here on that finish
let cond_finish= ((i_en_rld == 1'b1) && (dec == 1'b1) && (lock == 1)); // needs to meet the requirements
property p_decr_check_prpty ;
@(posedge monclk_output_rld) disable iff (!i_en_rld)
((i_en_rld == 1'b1) && (dec == 1'b1) && (lock == 1)) |->
##1 first_match( (o_prog_out== $past(o_prog_out)-1'b1) [*1:$]
##0 0_prog_out== (prog_trim - freq_dec)
)
##1 $stable(0_prog_out)[*1:$] ##0 cond_finish;
endproperty
// Note: The first_match() is needed here because without it, the assertion will never finish.
// I am also assuming that there are enough decrements to have (0_prog_out== (prog_trim - freq_dec))
//
// Onother option: split this into 2 assertions
property p_decr_check_prpty ;
@(posedge monclk_output_rld) disable iff (!i_en_rld)
((i_en_rld == 1'b1) && (dec == 1'b1) && (lock == 1)) |->
##1 (o_prog_out== $past(o_prog_out)-1'b1) [*1:$]
##0 0_prog_out== (prog_trim - freq_dec );
endproperty
property p_decr_check_prpty_stable ;
@(posedge monclk_output_rld) disable iff (!i_en_rld)
0_prog_out== (prog_trim - freq_dec) |->
##1 $stable(0_prog_out)[*1:$] ##0 cond_finish;
endproperty