KnowHow
Free Technical Resources

The temporal operators of the foundation language provide syntactic sugaring on top of the LTL operators. These temporal operators include always, never, next, until and before, amongst others. The meaning of these operators is quite intuitive, but there are a few surprises.

The always operator holds if its operand holds in every single cycle, whilst the never operator holds if its operand fails to hold in every single cycle. The next operator holds if its operand holds in the cycle that immediately follows. Hence the assertion

assert always req -> next grant;

means that whenever the HDL signal req is true, the HDL signal grant must be true in the following cycle. The meaning of a cycle will typically be specified either by defining a default clock or by including the clocking operator @ within the property. Note that when req is true, this assertion says nothing about the value of grant in any cycle other than the immediately following cycle. Also, it says nothing about the value of grant when req is false. It only says that whenever req is true, it must be the case that grant is true in the very next cycle.

The next operator can take a number of cycles as an argument, enclosed in square brackets, as in:

assert always req -> next[2] (grant);

This means that whenever req is true, grant must be true two cycles later. It says nothing about the value of grant one cycle after req is true. An interesting feature of this assertion is that it must hold in every single cycle, such that if req were true for three consecutive cycles, say, so must grant be true for three consecutive cycles, but with a latency of two cycles. If this assertion is implemented as a simulation check, it would be re-triggered every time req is true, such that concurrent invocations of the simulation check are effectively pipelined.

The meaning of the until operator is a bit more subtle:

assert always req -> next (ack until grant);

This asserts that whenever req is true, ack is true in the following cycle and ack remains true until the first subsequent cycle in which grant is true. There is no obligation on the value of ack in the cycle in which grant goes true, nor in any subsequent cycles (unless the check is re-triggered by req going true once more). If req goes true and then grant goes true in the following cycle, ack need not go true at all. On the other hand, there is no obligation for grant to ever go true following a req, in which case ack would have to remain true indefinitely.

The cycle in which the left-hand operand to until is first required to hold is determined by the context in which that operator appears. In the example above, the obligation for ack to be true begins in the cycle after req is true. Once again, the always operator requires that the temporal expression shall hold in every cycle, and hence concurrent invocations of the check are pipelined.

Finally, the before operator:

assert always req -> next (ack before grant);

This asserts that whenever req is true, ack must be true at least once in the period starting in the following cycle and ending in the last cycle before grant is true. There are no obligations on the value of ack in the cycle in which req goes true, nor in the cycle in which grant goes true. There is no obligation for grant to ever go true following a req, in which case ack need not go true either. In other words, following a req both ack and grant could remain false indefinitely.

 

Next: Strong Operators and Liveness Properties