Debugging Assertions and Efficiency Considerations - SVA: The Power of Assertions in SystemVerilog - page 424

property p_cover;
logic [3:0] tag;
(

req, tag = req_tag,
$display("[%t] req asserted, tag %0d", $time, tag)

)
##[ * ]
(

ack && tag == ack_tag,
display("[%t] ack asserted, ack_tag %0d", $time, ack_tag)

);
endproperty
c: cover property (p_cover);

t

The additional code stops the assertion at the beginning, starts it for one clock
tick, and then again stops it. We added $display to the assertion to make sure that it
does trigger (and fail) as observed originally. Finally, we added a cover property that
searches for ack with the matching tag indefinitely from the time of the occurrence
of req . The objective is to see whether ack ever arrives.
After running the simulation, we observe that the assertion and the cover
triggered as expected, the assertion failed and the cover matched very quickly
on the next clock tick at time 107. Assuming that the test is generating legal
situations only, it suggests that the assertion missed the arrival of ack associated
with the matching req . By examining the assertion, we can see that in fact the
bounded eventuality starts checking only 2 cycles after the req arrival due to the
one cycle delay introduced by |=> , and then another cycle by the lower bound of 1
in s_eventually . An easy correction is as follows:
Example 19.3.
property p;
logic [3:0] tag;
(req, tag = req_tag)
|=>
s_eventually [0:18] ack && (ack_tag == tag);
endproperty
a: assert property (p);

t

The solution brings out a question: Can the acknowledgment arrive with 0 delay?
The requirement specification did not mention anything about the earliest arrival.
This issue has to be clarified. If the answer is that the acknowledgment can be
generated combinatorially with 0 clock tick delay, then |=> should be replaced by
|-> in the assertion. What should happen if ack arrives at the same time as req and
with the same ack_tag value as the value of req_tag ? If this situation is illegal,
then the assertion should be modified to reject it as shown in the next example.

Example 19.4.
property p;
logic [3:0] tag;
(req, tag = req_tag)