Assertion Check

In reply to rkg_:
Your requirements are not clear; I don’t understand your need for the case.
The caseis a property statement


property_statement ::=
property_expr ;
| case ( expression_or_dist ) property_case_item
{ property_case_item } endcase
| if ( expression_or_dist ) property_expr
[ else property_expr ]
// example
case (cntrl)
  2'd0 : a |=> c;
  2'd1 : a ##2 b;
  2'd2 : a ##1 b |-> c;
  default: 0;
endcase
// You could also use the **generate** statement.
// For your model, consider this (again, requirements ??) 
/* if (a == 00) between 1 to 6 clock cycle of ref_clk if two positive edges of dec signal 
   or incr signal is detected then lock is asserted.

   I am not sure how to check two positive edges of dec or incr on 1 to 6 clock cycle of ref_clk.

   Can i write case statement inside property since a can have 01 , 10, 11 as well so Do need to
   to write four separate property for (a == 2'b01, 2'b11 ..) ? */
   module m; 
    bit[1:0] a, lock;
    bit ref_clk, inc, dec;
    property p_incdec; 
        int inc_count, dec_count;
        (a==2'b00, inc_count=0, dec_count=0) |-> 
            (##1 (1, inc_count+= $rose(inc), dec_count+= $rose(dec)))[*6] ##0 
            lock==(inc_count==2 || dec_count==2);
    endproperty 

    ap_incdec: assert property(@ (posedge ref_clk)  p_incdec );  

    generate for (genvar i=0; i<=3; i++)
        begin
            property p_incdeci; 
                int inc_count, dec_count;
                (a==i, inc_count=0, dec_count=0) |-> 
                    (##1 (1, inc_count+= $rose(inc), dec_count+= $rose(dec)))[*6] ##0 
                    lock==(inc_count==2 || dec_count==2);
            endproperty 
            ap_incdeci: assert property(@ (posedge ref_clk)  p_incdeci);  
        end
    endgenerate
   endmodule 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: