Check signal assert for n cycles where n is configurable

SystemVerilog
, ,
4

In reply to Fpfermoselle:

In reply to ben@SystemVerilog.us:
Thank you very much for your reply. I will use the second approach but I want to understand why did you say . g_i is not an integer that can have any value in the range 2^31 to 2^31-1 ?

That is correct.

And also I need help with the SVA solution


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

I understand that the first_match sentence will last until b goes to 0 and one cycle later local_v has to be 0.

the first_match sentence will last until v goes to 0 or -1.
“…and one cycle later local_v has to be 0.” that is incorrect.


(b, local_v=local_v - 1)[*0] ##1 local_v<=0) // is equivalent to
 (local_v)  or //because
 // any_seq[*0] ##1 w // is same as w
 // any_seq[*0] ##0 w // is a no match 
(b, local_v=local_v - 1)[*1] ##1 local_v<=0) or 
(b, local_v=local_v - 1)[*2] ##1 local_v<=0) or ...
Now, if the dynamic variable is 1, then you have 
Thus, If local_v is initially 1, 
 1<=0) or
(b[*1] ##1 0 <=0)  // same as (b ##1 )

If that is how it works I do not understand the example of the “Understanding the SVA Engine” paper:


// ap_ab_then_min_max_c : assert property($rose(a) ##dly1 b |-> ##dly2 c); // ILLEGAL SVA
property p_ab_then_min_max_c;
int v_dly1, v_dly2;
($rose(a), v_dly1=dly1, v_dly2=dly2) ##0
first_match((1, v_dly1=v_dly1-1'b1)[*1:$] ##0 v_dly1 < 0) ##0 b |->
first_match((1, v_dly2=v_dly2-1'b1)[*1:$] ##0 v_dly2 < 0) ##0 c;
endproperty
ap_ab_then_min_max_c: assert property( p_ab_then_min_max_c); //

I do not understand when the first_match sentence ends

 
first_match(
             (1, v_dly1=v_dly1-1'b1)[*1:$] ##0 v_dly1 < 0  
           ) 
             ##0 b |-> ...

Below is a link to a couple of pages from my SVA book that addresses some models in handling dynamic delays.

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