Check a value for 'var' number of cycles in SVA

Hi All,

I want to write an assertion which checks a value continuously for a variable number of cycles as shown below :

@posedge (clock) ($rose(a)) |=> ((data == 4'h5)[*cycles]);

Can you tell me how to implement this in SVA?

Thanks

I provide 2 solutions in my SVA Handbook 4th Edition, 2016

*Simple repeat (e.g., a[v]]


ap_repeat_fix: assert property( $rose(a) |-> b[*v] ##1 c); //1800'2018 property 
// Above is illegal in 1800'2012

p_repeat_equivalent; // /11.4/m5067_gen_options.sv. works in 1800'2012
  int local_v; //  
      $rose(a) |-> 
    (1, local_v = v) ##0 first_match((b, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
                                                                          ##0 c; // 
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent); // with default clocking

generate option
If the variable used to define the repeat has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item.

 
generate for (genvar g_i=0; g_i<8; g_i++) begin
  ap_repeat_gen: assert property (v==g_i && $rose(a) |-> b[*g_i] ##1 c);
end endgenerate  

The generate
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for your answer. In your second method, can you tell me what does first_match do? Though I don’t know the exact functioning of that, I tried to imitate it in my example below. Can you tell me if I’m right?

p_repeat_equivalent;
  int local_v; //  
      $rose(a) |-> 
    (1, local_v = v) ##0 first_match((b == 4'h5, local_v=local_v - 1)[*0:$];
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent);

Thanks,

In reply to szy0014:
In my model (see below), if b==1 at all cycles (i.e., dc), and c==0 at all cycles, then without the first_match()the assertion will never complete, even if v==1 (the repeat will keep on trying searching for a c==1).

 
 (1, local_v = v) ##0 first_match((b, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
                                             ##0 c; //  

Your case does not have “c”. thus, the following will work

 
p_repeat_equivalent;
  int local_v; //  
      $rose(a) |-> 
    (1, local_v = v) ##0 (b == 4'h5, local_v=local_v - 1)[*0:$] ##1 local_v<=0;
endproperty
ap_repeat_equivalent: assert property(p_repeat_equivalent);

The first_match() is not needed because if b==0 at any cycle, the assertion will fail. If b==1 at all cycles (i.e., dc), the assertion will terminate successfully after v cycles.
If You had a term after the repeat, like my “c”, then the first_match() would terminate the count (because, eventually, local_v will be <=0 if b==1 during those cycles), and then you would test for he other terms in the sequence. remember

 
b[*0:$] ##1 c// is same as 
c or (b ##1 c) or (b ##2 c) or (b ##n c) 

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


In reply to ben@SystemVerilog.us:

Thanks Ben,

That is working for me.