SVA- How we can write property such that it will check OUT_BITS increment and decrement

SystemVerilog
,
6

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)}; 
  // was: (out_bits < ($past(out_bits, 1));
endproperty