Hi all,
I’m trying to check that a signal is stable after two (non-clock consecutive) falling edge of another signal.
I tried with assert property (@(posedge clk) disable iff (!reset_n) fell(a) ##[0:] $fell(a) |-> $stable(dist_value))
but it fails after the first falling edge and after that it will be not evaluated.
Can anyone suggest another approach/solution? Or explain to me where i’m wrong?
Thanks
// Two problems with
assert property (@(posedge clk) disable iff (!reset_n) $fell(a) ##[0:$] $fell(a) |-> $stable(dist_value))
1) $fell(a) ##[0:$] $fell(a) // is same as
$fell(a) ##0 $fell(a) or $fell(a) ##1 $fell(a) or ...
// Thus, upon the first $fell(a) the $fell(a) ##0 $fell(a) is satisfied.
// However, the other problem is that
2) the antecedent has multiple matches, and all matches must be evaluated
// before the property succeeds.
//You can do one of the following solutions:
assert property (@(posedge clk) disable iff (!reset_n)
first_match($fell(a) ##[1:$] $fell(a)) |-> $stable(dist_value));
assert property (@(posedge clk) disable iff (!reset_n)
$fell(a) ##1 $fell(a)[->1] |-> $stable(dist_value));
// Note: : b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m]
// NOTE: The following assertion, though more brief, is NOT recommended
// because it is inefficient because multiple threads are started when !$fell(a)
ap_VERY_BAD_STYLE: assert property (@(posedge clk) disable iff (!reset_n)
$fell(a)[->2] |-> $stable(dist_value)); // INEFFICIENT!!!
// b[->2] is equivalent to:
// !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Hi Ben ,
i have question on above question itself . since if use first match operator what about when “A” goes zero third time how can we handle this.
i.e
First time when “A” goes zero and followed after some clock cycles again when “A” goes zero the antecedent gets triggered which then check stable value of Dist_value
ssert property (@(posedge clk) disable iff (!reset_n)
first_match(fell(a) ##[1:] $fell(a)) |-> $stable(dist_value));
Now what happens when “A” goes low for third time will it be considered as fresh new cycle of assertion check or will it be ignored since we are using first_match operator.
Thanks
Also sorry for my bad English
In reply to raku:
At every clocking event, there is an attempt in evaluating the assertion. If the attempt is successful, then a thread is started. Every attempt has no correlation to other (previous) or future attempts. Thus, in this example, assume that dist_value is stable all the time (for simplicity and discussion), and assume that $fell(a) is true in the following cycles: 2, 5, 7, 10, 25
assert property (@(posedge clk) disable iff (!reset_n)
first_match($fell(a) ##[1:$] $fell(a)) |-> $stable(dist_value));
@cycle 2 attempt is successful, must wait for a 2nd $fell(a). // thread@t2 started
@cycle 5 attempt is successful, must wait for a 2nd $fell(a). // thread@t5 started
$fell(a)==1, antecedent for thread@t2 is true, assertion for thread@t2 passes
@cycle 7 attempt is successful, must wait for a 2nd $fell(a). // thread@t7 started
$fell(a)==1, antecedent for thread@t5 is true, assertion for thread@t5 passes
@cycle 10 attempt is successful, must wait for a 2nd $fell(a). // thread@t10 started
$fell(a)==1, antecedent for thread@t7 is true, assertion for thread@t7 passes
The first_match is for antecedent that started at the attempt. It has no correlation or relationships to other threads that started at other attempts. All the attempts are mutually exclusive and independent.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
Thanks Ben for very good explanation with example.
But now i am getting confused with first _match operator what is the use of first match operator. If you can explain with example like above example it would be very helpful.
i am thinking use of first_match is if @cycle 2 thread 2 starts @cycle 5 antecedent of thread gets success so thread2 immediately check for stable valueof other signal . But still thread2 is not killed at @cycle7 again it antecedent gets success and again matches stable value of other signal .
So in order to avoid are using first_match operator ?
Please correct me if i am wrong.
Thanks
In reply to raku:
From my SVA Handbook
The first_match operator matches only the first of possibly multiple matches for an evaluation attempt of its operand sequence. This allows all subsequent matches to be discarded from consideration. This is significant when a sequence is used in the antecedent of an assertion because when a range is used in the antecedent, it can create multiple threads, each triggering the evaluation of the consequent when matched, and all threads must hold for the assertion to hold. This can cause significant performance impacts and possible unexpected errors. However, when a sequence is a subsequence of a larger sequence, then applying the first_match operator has significant (positive) effect on the evaluation of the enclosing sequence. Consider the following example:
ap_never_succeed: assert property(($rose(a) ##[2:$] b) |=> c);
The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(($rose(a) ##2 b)or ($rose(a) ##3 b)or
… ($rose(a) ##n b)|=> c); // where n is infinity
For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and there are an infinite number of threads; specifically, these threads include:
($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2
…
($rose(a) ##n b)|=> c // thread n
If any of these threads fails, then the assertion fails; however success cannot be achieved. With the first_match method, only the first match of the sequence is considered, and all other threads are ignored. Thus, in the assertion ap_FM_can_succeed a first match of the antecedent is considered for the evaluation of the consequent.
ap_FM_can_succeed: assert property(
first_match($rose(a) ##[2:$] b) |=> c);
i am thinking use of first_match is if @cycle 2 thread 2 starts @cycle 5 antecedent of thread gets success so thread2 immediately check for stable valueof other signal . But still thread2 is not killed at @cycle7 again it antecedent gets success and again matches stable value of other signal .
Let me rephrase this with proper terms
i am thinking use of first_match is if
@cycle 2, thread@t2 (that is the name I gave to that independent, separate thread) starts.
@cycle 5 antecedent of thread gets success so thread@t2 immediately check for stable valueof other signal (the consequent). Since the consequent succeeds for thread@t2, that thread get kills, and is marked as a PASS. Now, we're DONE with that thread@t2.
@cycle 5, thread@t5 starts (this is the 1st occurrence of $fell(a).
@cycle7 again it antecedent for thread@t5 gets success and again matches stable value of other signal, Thus, at cycle 7, we're done with thread@t5 at that cycle 7; that thread@t5 is considered a PASS.
Another wasy of thinking about this is you standing on a corner of a one-way street.
A car with license plate 0001 passes by at t2.
At t5, car with license plate 0001 reaches its destination (the freeway); we're done with that car.
At t5, another car, with license plate 0002 passes the oorner where you stand.
At t7, car with license plate 0002 reaches its destination (the freeway); we're done with that car.
Every car is independent from other cars, and each car has its own destiny.
The first_match is to avoid multiple matches on a sequence, since all matches of an antecedent must comple before an assertion with implication completes. Example:
a ##[1:$]b |-> c // is same as
(a ##1 b) or (a ##2 b) or ... (a ##n b) |-> c
thius assertion can only fail, but cannot pass
first_match(a ##[1:$]b) |-> c // can pass because you do not test all possible combinations of this ORing, all you need is the first one that matches.
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
Thanks Ben for clearing my doubt and also for very nice explanation
In reply to raku:
Thanks for the great solution ben!!
I tried with the first (the one with “first_match”) and now the assertion works fine, but at the end of simulation it remains append because (I guess) no more $fell(a) condition (second of the first part of the assertion) has been found.
But I think it’s sufficient for my checks for now.
thanks again for your help.
In reply to alexkidd84:
Just curious, Does this one work? $fell(a) |=> $stable(b) until $fell(a); // until_with
In reply to aming:
I tried with the first (the one with “first_match”) and now the assertion works fine, but at the end of simulation it remains append because (I guess) no more $fell(a) condition (second of the first part of the assertion) has been found.
If you want just one thread to start, and avoid this problem, you can exclude all others with something like the following
module m;
bit clk, a, b, dist_value;
bit start=1'b1;
always @(posedge clk)
if(!reset_n) start=1'b1;
function void reset_start();
start=1'b0;
endfunction
ap_q: assert property (@(posedge clk) disable iff (!reset_n)
first_match( ($fell(a) && start, reset_start()) ##[1:$] $fell(a)) |-> $stable(dist_value));
//Does this one work? $
fell(a) |=> $stable(b) until_with $fell(a); // until_with
// That assertion has a different meaning, stating that after the fell(a) you gt at next cycle stable(b).
The original requirement stated that after the 2nd fell(a) you get the stable.
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
Hi BEN can you explain , is there any difference between the two properties :-
1)$fell(a) ##0 $fell(a) 2) [b]$fell(a) ##1 $fell(a)
As you have mentioned above that these two are similar.PLease explain how they are similar.
In reply to prashantk:
I strongly suggest that you study SVA either from a book, from videos, or from 1800.
Sorry, but your question implies that you really do not understand the meaning of $fell.
It is trivial for me to answer that question, but it would be more beneficial for you to study SVA and run some tests sot aht you would get a better understanding of the language.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us