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

SystemVerilog
,
21

In reply to rkg_:
Look at the the syntax of a sequence; one of them is

 

sequence_expr ::=   
... | ( sequence_expr {, sequence_match_item} ) [ sequence_abbrev ] 
   
// example 
// At end of subsequence a ##1 b, j=0.  
// Starting from next cycle c must remain 1 for as  
// many cycles as defined by the value of the    
// argument cy (j is incremented until j==cy).   
property P(int cy);   
  int j=0; // initialization optional,  legal in SV’09   
   (a ##1 b, j=0)|->     
    ##1 (c, j+= 1) [*0:$] ##1 j==cy;  
endproperty : P // See below for more  examples  
 
// corrected using 1'b1 as the sequence_expr
property out_bits_incr_prpty;
  bit[7:0] v;
//  @(posedge monclk_output) disable iff(!i_en_fll)
@(posedge sampled_monclk) disable iff (!i_en_fll)
  ##1  1   |->   if (monclk_count < i_count)
   (1'b1, v=incr(o_prog_out_fll, sar_mask ,monclk_count, i_count)) ##0 v 
  else
   (1'b1, v=decr(o_prog_out_fll, sar_mask ,monclk_count, i_count))  ##0 v ;
endproperty