Hardware Reference
In-Depth Information
req
gnt
Fig. 6.8
Two requests corresponding to the same grant
Solution:
a1: assert property (@( posedge clk) req |=> s_eventually gnt);
Discussion: This assertion does not distinguish between grants to different requests.
For example, there may be the same grant for several requests, as shown in Fig. 6.8 .
This example reflects the fact that the normal semantics of assertions is global,
and not pipelined: there is no easy way to distinguish between different attempts
(transactions) of the same assertion. The pipelined semantics in our case means
that each request should have its own grant. Chapter 15 explains how to implement
pipelined semantics in assertions using local variables.
t
Example 6.24. After request req has been sent, acknowledgment ack should come
before data ( data_ready ).
Solution:
a1: assert property (@( posedge clk)
req |-> !data_ready until_with ack);
Discussion: In this implementation, the acknowledgment is allowed to be issued
in the same clock tick as the request; see Exercise 6.5 for the case when the
acknowledgment is expected to come strictly after the request. If the request is never
acknowledged - there is neither acknowledgment nor data—the assertion passes.
t
6.4.3
Vacuous Execution
The definition of the suffix implication states that the consequent is checked starting
from the moment of every nonempty match of the antecedent. It follows that in the
case when the antecedent does not have a match, the suffix implication holds. This
case is called vacuous execution of the implication.
If an assertion is continuously monitored, it is natural that many of its attempts
terminate vacuously. For instance, if in Example 6.22 each attempt is nonvacuous
then the request is always active, which is not likely to happen in practice. But if all
the assertion attempts pass vacuously, it indicates a serious problem in validation.
What would you say about a civil engineer who constructed a bridge, and to the
question “Will this bridge withstand if a heavy truck crosses it?” he will answer
Search WWH ::




Custom Search