Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 100

Of course, this assumes that we verify the property on an infinite trace, hence
in FV. In that case it is not difficult to see that the opposite is also true: Assertion a1
implies the required behavior. Indeed, if req goes high in some clock tick i , it will
remain high until granted by definition. The attempt of the property starting

s_eventually req -> gnt
in clock i guarantees that this req is granted.
Discussion: This property is a special case of property always s_eventually p
described in Example 5.13 . Assertion a1 is standalone, and therefore it has an
implicit always operator. Its performance in simulation may be poor if req is
asserted and no gnt is asserted for a long time (if ever). Simulation performance
efficiency is discussed in detail in Sect. 19.3 .
In this example, we assumed that the request remains pending until granted.
Example 6.23 describes the case of an arbitrary, not necessarily pending request.

t

Fairness.

Example 5.15. A device must be available infinitely many times. The device
availability is indicated by high value of the ready signal.
Solution:

a1: assert property (@( posedge clk) s_eventually ready);

Discussion: This assertion is standalone, hence there is an implicit top-level always
operator. t

The property always s_eventually e is very important for verifying liveness
properties in FV. It expresses the notion of fairness . Fairness indicates that some
resource eventually becomes available, as in Example 5.15 . The absence of fairness
is called starvation , the situation when the requested resource is never available:
Imagine a car waiting at an intersection forever on the red light when the traffic
lights are broken. We get back to the notions of fairness and starvation in Chap. 21 .
In simulation, of course, this assertion cannot be verified (it cannot fail) because
simulation will end in a finite number of clock ticks.

5.5 Basic Boolean Property Connectives

The following Boolean connectives between properties exist in SVA:

￿ not —negation
not p is true iff p is false.
￿ and —conjunction
p and q is true iff both p and q are true.