I may need to get assertion based on below scenario, help how to do it?
X, Y and Z are the signals from RTL.
Whenever X comes, Y should go high (may be in couple of clk cycles); Z should only high when both X and Y is High (may be in N no of clk cycles); and X should go down once Z comes.
My code look like below:
property my_seq;
($rose(X) ##[0:5] Y ##[0:5] Z ##[0:1] $fell(X));
endproperty
assert property @posedge(clk) my_seq;
But, here the boundaries are not fixed. Y and Z can happen in any N no of cycles.
Asserting a sequence has little meaning since the sequence can only hold at specific points in time, and you will get failures at all other times even though the design behaviour is correct.
Is it not better to write this as a single assertion with multiple implications. Otherwise, the above solution is checking each of the conditions independently. For example, we might want Z to be only asserted if X and Y asserted where-as as per above approach, if z is asserted, it would only check that x is de-asserted, which might not be correct as per the protocol. Again, as mpreyer mentioned, it all depends on the specification of this interface …
As per your protocol , Below I have written assertion.
property my_seq;
($rose(X)) |-> ##[0:$] Y ##0 X |-> ##[0:$] Z |-> ($fell(X))
endproperty
You need to be careful about multiple matches. The above assertion can never succeed because all the threads of antecedents must complete; and that is impossible because of the infinite number of threads cause by the ##[0:$] . Looking at the structure only, rather than the accuracy of the property, the above property is best written as:
Manish,
We generally recommend write several simple assertions, which when seen together fulfills your requirement as a whole. Rationale:
It is much easier to understand, decipher and debug smaller ones
Formal tools like smaller assertions and converge faster on them, than the end-to-end ones.
As my co-author Ben mentioned, you need to worry about multiple matches etc. while writing long ones - though that understanding is a must for simple ones too.
So I suggest you better break it down like MPreyer has shown.
Before answering the question, let me first assert that you do not need a first_match in the consequent because when the first match of the consequent succeed, the assertion is done.
You need a first_match in the antecedent because all threads of the antecedent must be tested before the determination of the assertion is determined, unless the assertion fails in one of those threads (at which point that attempt for the evaluation of assertion ends). Thus,
property my_seq;
($rose(X)) |-> first_match( ##[0:$] Y ##0 X) ##0 first_match(##[0:$] Z) ##0 ($fell(X));
endproperty
// should be written as
property my_seq;
$rose(X)) |-> ##[0:$] Y ##0 X ##[0:$] Z ##0 $fell(X);
endproperty
Now, to your question on multiple implications:
Instead of using multiple implication can I use single implication? I am more interested in understanding the reason to persuade multiple implication.
The simple answer is that at the evaluation each antecedent of an implication, if that antecedent evaluates to false, then the evaluation of that assertion for that attempt is vacuous. So the answer is vacuity vs failure, and vacuity is of importance in your definition of the assertion. Consider the following example:
$rose(req) |-> first_match(##[1:3] rdy) |=> ack;
In this case, if rdy is not true within 1 to 3 cycles after a new req, then the assertion is vacuous.
However, for
$rose(req) |-> ##[1:3] rdy ##1 ack;
if rdy is not true within 1 to 3 cycles after a new req, then the assertion fails
… And that is the difference as to why you may or many not want multiple implications.