There are five signals a,b,c,d,e. I want to check if they are asserted in the order of a,b,c,d and e.
It can be done like this
property valid_packet;
@(posedge clk) disable iff(!rst_n)
$rose(|a) |=> $rose(|b)||=> $rose(|c) |=> $rose(|d)|=> $rose(|e);
endproperty
But the signals don’t change in uniform intervals. For example, after b, c can take any number of cycles to become high. In some cases, c becomes high the next cycle after b becomes high and in other cases, it takes more cycles. How do I do this?
In reply to Lothlorien:
Hi, I guess You’ll have to go with the non-consecutive repetition operator. Along with this, You’ll have to consider one edge case where values of a,b,c,d,e are constant 1. In that case
$rose() will not give the required result.
The following could be the answer :
property valid_packet;
@(posedge clk) disable iff(!rst_n)
a |-> a[=1] ##1 b[=1] ##1 c[=2] ##1 d[=2] ##1 e;
endproperty
It’s just speculation. What’s happening here is when a is 1 from that point it will start searching the first appearance of b as 1. For that, I have used a[=1] .Same theory I have used for the rest of the signals.