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
such as between 0 and 7 (or 15, or at most 32)
. g_i is not an integer that can have any value in the range 2^31 to 2^31-1 ?
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. 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