I am new in system verilog verification and I am trying to check if a signal SIGNAL is asserted for n cycles. I understand that if N_CYCLES was constant the solution would be something like
property check_signal_assert;
@ (posedge clk)
SIGNAL |-> SIGNAL[*5]
But the thing is that the signal duration will change by means of a configuration register during the simulation and I need to check that the exact duration is performed by the signal. I do not want something like “the signal will be asserted from 4 cycles to 8”, I am looking for something like:
property check_signal_assert;
@ (posedge clk)
SIGNAL |-> SIGNAL[*N_CYCLES]
In reply to Fpfermoselle:
There are 3 replies: 1) My preferred solution
If the variable used to define the delay 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. Example:
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate
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:
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 ?
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:
I do not see why v is the one that ends first_match if it is not inside the first_match clause, Is not the local_v local variable the one being modified?
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 )
Lets say that the local_v value is initially 3, is the following correct?
(3<=0) or
(b[*1] ##1 2<=0) or
(b[*2] ##1 1<=0) or
(b[*3] ##1 0<=0) // same as b[*3] ## 1,
My real question here is; when is local_v modified? I mean:
(b, local_v=local_v - 1)[*1] ##1 local_v<=0) or // Is this local_v=local_v - 1 resolved
(b, local_v=local_v - 1)[*2] ##1 local_v<=0) or // before this one, and this one before the next one and so for ?
In reply to ben@SystemVerilog.us:
I do not see why v is the one that ends first_match if it is not inside the first_match clause, Is not the local_v local variable the one being modified?
I don’t follow your question. In the following assertion, the local_v is updated once with the “v”, and the “v” is no longer used, and does not complete the first_match().
The first_match() ends when “b==0” because the assertion fails, or when local_v<=0.
At every entry of the repeat of (b, local_v=local_v - 1)[*0:$], the local_v gets decremented.
ap_repeat_fix: assert property( $rose(a) |-> b[*v] ##1 c);
p_repeat_equivalent; // /11.4/m5067_gen_options.sv
int local_v; // this is an internal local variable defined by the tool
$rose(a) |-> (1, local_v = v)
##0 first_match((b, local_v=local_v - 1)[*0:$] ##1 local_v<=0)
##0 c;
endproperty
Lets say that the local_v value is initially 3, is the following correct?
(3<=0) or
(b[*1] ##1 2<=0) or
(b[*2] ##1 1<=0) or
(b[*3] ##1 0<=0) // same as b[*3] ## 1,
My real question here is; when is local_v modified? I mean:
(b, local_v=local_v - 1)[*1] ##1 local_v<=0) or // Is this local_v=local_v - 1 resolved
(b, local_v=local_v - 1)[*2] ##1 local_v<=0) or // before this one, and this one before the next one and so for ?
the local_v is computed inside the computation of the sequence.
1800: sequence_expre ::=
( sequence_expr {, sequence_match_item } ) [ sequence_abbrev ]
Thus, @(posedge clk) (b, local_v=local_v - 1, local_v2=varB, func_do_something(local_v))
If b==1, then the sequence_matched_item is computed. In the above example.
1) local_v is decremented, then
2) local_v2 is updated with the value of varB,
3) the function func_do_something is called with the already decremented local_v.
I believe the the confusion is the concept of threads.
cycle_delay_range ::=
## constant_primary
| ## [ cycle_delay_const_range_expression ]
| ##[*]
| ##[+]
Thus,
(a, lv=q) |-> (seq, lv=lv-1)[*1:N] ##0 lv==0; // is same as
(a, lv_copy1=q, lv_copy2=q, ..., lv_copyN=q) |->
( (seq, lv_copy1=lv_copy1-1)[*1] ##0 lv_copy1==0 ) or // one separate launched thread
( (seq, lv_copy2=lv_copy2-1)[*2] ##0 lv_copy2==0 ) or // one separate launched thread
...
( (seq, lv_copyN=lv_copyN-1)[*N] ##0 lv_copyN ==0); // one separate launched thread
Each thread has a life of its owns. However, if any of the threads completes (because this is a consequent, the assertion completes; there is no need to keep on computing useless work. If all the treads fails, then the assertion fails
One more thing: In the ORing, each thread maintain its own copy of the local variable.
That is internally generated by the simulation tool.
Obviously, the simulation tool handles this with optimization and internal code. It may even do something like my examples in my paper