Consider the following assertion:
assert always req -> eventually! ack;
This asserts that whenever req is true, ack must go true at some future cycle, but there is no upper limit on the time by which ack is required to go true. This is known as a liveness property. Liveness properties are characterised by the fact that they do not possess a finite counter-example, and hence in principle they cannot be disproved by simulation. However, liveness properties can in principle be proved or disproved by static model checking tools. Properties that do possess finite counter-examples are known as safety properties.
Liveness properties are written in PSL using strong operators, all of which include an exclamation mark in their name. There exist strong forms of several temporal operators, including next!, until! and before!. For example:
assert always req -> next (ack until! grant);
This means that whenever req is true, ack is true in the following cycle, ack remains true until the first subsequent cycle in which grant is true and grant must go true eventually.
Non-negated strong operators always create liveness properties, but you might care to ponder the fact that:
not eventually! (not P)
is actually formally equivalent to
always P
Next: Sequences
