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

￿ Properties ending with open-ended intervals such as
##[M:$] s and s_eventually p .
An open-ended interval in a property implies that the tool will be searching for
satisfying the arguments s and p , till the end of evaluation. If it cannot be satisfied in
simulation it will run till the end. Depending on the strength of the operator, it will
report a success (weak property) or failure (strong property). That is, the property
cannot fail (if at all) until the end of simulation. If the evaluation of such an open-
ended operator is repeatedly retriggered, this will cause accumulation of attempts
and threads. In simulation, open-ended intervals should be replaced by a reasonably
bounded range, while in FV, open ranges are much preferred because they add only
few states to the automaton.
Exercises
19.1. Assertion a: assert property (en ##1 !y[+] |-> x) had attempts start
at 1, 2, 3, 4 all of which succeeded at time 5, but the attempt that started at time 5
failed at time 6. What could be the problem? Is it a problem in the design or in the
assertion formulation? Explain each of the cases.
19.2. Assertion a: assert property (trig |-> s_eventually (sig)) ; failed
at the end of simulation for several attempts. What is the reason for the failure and
what could be the remedy(ies)?
19.3. The example in Chap. 17 ,Fig. 17.14 fails. How would you debug the failure
in simulation?
19.4. If a checker like the assert_handshake in Chap. 24 fails, how could you
approach debugging the failure (a) if you have access to the source code of the
checker, and (b) if you do not have access to the source code.
19.5. Suppose that the assertion in Exercise 19.1 failed in formal verification by
model checking. What means you may have to debug it?
19.6. Will property req |-> s_eventually ack be efficiently evaluated in simu-
lation if it is required to provide full attempt information (start and fail/success
times)? Does it depend on the protocol? That is, when req is a single clock tick
pulse vs. when req should hold asserted until and including the assertion of ack ?
How would it perform in formal verification?
19.7. In the preceding problem, if req is to remain asserted until ack is asserted, is
it important to you that an assertion using the preceding property reports all the start
times of attempts that succeeded at the same time when ack is asserted? Should it
report the earliest or the latest such start time only?