I need to make sure the latency across the device is shorter than duration, where the value of the latter depends on some conditions. I have a piece of helper code that determines the conditions and defines what is the value of duration in number of clks. So the goal is to make sure that after sig_a is deasserted then sig_b should go to 1b1 within the specified duration`
Since the delay between the two events ($fell(sig_a) and sig_b[->1]) is dynamic, I’ve decided to use the dynamic delay package from Ben Cohen [1]. So my property looks like the following:
default clocking property_clock @(posedge clk);
endclocking
// need to see sig_b asserted at least once within the latency limits
sequence seq_b;
sig_b == 1`b1[->1];
endsequence
// start checking after the sig_a deasserts
sequence seq_a;
$fell(sig_a) ;
endsequence
// duration is provided in number of clk
property p_max_latency (duration);
seq_a |=> dynamic_delay_lohi_seq(0, duration, seq_b);
endproperty
While I see the assertion on the p_max_latency property is activated correctly, it doesn’t seem to be finishing correctly when seq_b is not set at the end of the duration window. The expectation is that either seq_b is happening within the duration provided in the property or it fails right after the duration expires.
Am I missing something? Is there another way to address the problem?
EDIT: for completeness I’ve also tried the following instead:
property p_max_latency (duration);
seq_a |=> seq_b within dynamic_delay(duration);
endproperty
which I found it more interesting and more readable as well, but it may have overlapping effects since the within doesn’t stop until the containing sequence completes despite the contained one has already completed.
// [Ben] if d1 were fixed at 2, and d2 dixeed at 5 the
// [Ben] NOTE from
/* [1] https://systemverilog.us/vf/sva_repeat_delay_thru_pkg_011624.sv */
$rose(a) |-> dynamic_delay_lohi_sq(d1, d2, sq_c1_4_b));
//is same as
ap_fix_2to5_consequent: assert property(@ (posedge clk)
$rose(a) |-> ##[2:5] sq_c1_4_b );
// Am I missing something? Is there another way to address the problem?
// [Ben]yes
// EDIT: for completeness I’ve also tried the following instead:
property p_max_latency (duration);
seq_a |=> seq_b within dynamic_delay(duration);
endproperty
// which I found it more interesting and more readable as well,
// but it may have overlapping effects since the within doesn’t stop until
// the containing sequence completes despite the contained one has already completed.
// [Ben]
(seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
// You don't want the within. You want
sequence seq_b;
sig_b == 1`b1[=1];
endsequence
seq_a |=> seq_b intersect dynamic_delay(duration) ##0 1;
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
The non-consecutive repetition operator [=const_of_range_expression] is specified as the following:
Nonconsecutive repetition specifies
finitely many iterative matches of the operand Boolean expression, with a delay of one or more clock ticks from one match of the operand to the next successive match and no match of the operand strictly in between. The overall repetition sequence matches at or after the last iterative match of the operand, but before any later match of the operand
As I read this, the sig_b == 1'b1[=1] will be true from the moment the operand is matching until the next sequence occurs, is the next sequence the combination of dynamic_delay(duration) ##0 1?
Additionally, is the term ##0 1 required to make the dynamic_delay(duration) term match?
EDIT: I have a second thought about the intersect, in a latency check what I really want to do is to terminate the check as soon as the sig_b goes to 1 and make sure it happened within a time bound, but I don’t want to continue the checking passed that time cause I can have a second sig_a event that will lead to an additional sig_b, messing up my sequence.
[You]the sig_b == 1'b1[=1] will be true from the moment the operand is matching until the next sequence occurs
[Ben] NO.
expr[->1] is same as !expr[*0:$] ##1 expr
expr[=1] is same as !expr[*0:$] ##1 expr ##1 !expr[*0:$]
// you want sig_b to be within a certain number of clocks.
// the sig[=1] is one occurrence F F F T F F F (F means sig_b==0)
sequence seq_b; sig_b == 1`b1[=1]; endsequence
seq_a |=> seq_b intersect dynamic_delay(duration) ##0 1;
// you coul also use the within
seq_a |=> sig_b within dynamic_delay(duration) ##0 1;
[You]EDIT: I have a second thought about the intersect, in a latency check what I really want to do is to terminate the check as soon as the sig_b goes to 1 and make sure it happened within a time bound, but I don’t want to continue the checking passed that time cause I can have a second sig_a event that will lead to an additional sig_b, messing up my sequence.
[Ben]The above 2 assertions start a separate thread when seq_a==1.
The consequent is satisfied with ONE occurrence of sig_b.
More do not cause a failure
The ‘go-to’ repetition works best since it captures what I’m actually looking for.
My missing bit initially wat the ##0 1 that I did not realize was necessary to have the dynamic delay sequence terminate with a match at the end of the duration.
Glad this works for you.
NOTE: The within can be tricky, thus always undersdand its construct. See the example in the last section of my paper:
11. Paper: Understanding SVA Degeneracy