In reply to ben@SystemVerilog.us:
In reply to rkg_:
So your increment / decrement for a 4-bit “a” is
bit[3:0] a;
a = {1'b1, a[3:1]}; // increment, 1'b1 concat with a right shift by 1
a = {a[2:0], 1'b0}; // deccrement, shift left by 1 with concat of 0
property out_bits_incr_prpty;
@(negedge refclk_output) disable iff(!reset)
(monclk_count < count) && Enable|=>
out_bits == {1'b1, $past(out_bits[3:1])};
// was: (out_bits > ($past(out_bits, 1) );
endproperty
/* check the out bits decrement */
property out_bits_decr_prpty;
@(negedge refclk_output) disable iff(!en_reset)
(negclk_count > count) && Enable|=>
out_bits == {$past(out_bits[2:0]), 1'b0)}; //before
out_bits == {$past(1'b0,out_bits[3:1])}; // modified
// was: (out_bits < ($past(out_bits, 1));
endproperty
Hi Ben,
it will work only on below sequence only:
for DECR :- 10000000 → 01000000 → 00100000 … so on
for incr :- 10000000 → 11000000 → 11100000
This assertion will not work on below
For DECR:- 11000000 → 10100000 → 10010000 → 10001000 …etc
for incr :- 10100000 → 10110000 → 10111000
Any suggestion