Temporal Assertions

Temporal assertions are statements in temporal logic that define a temporal relationship between variables and/or predicates of the program. For example a temporal statement can be

“if a =1 then eventually b=1”.

Notice the operator eventually which makes this assertion temporal. Another example is

“if a =1 then next b=1”.

In this case the temporal operator next refers to a next time point. This implicitly assumes that time points in this context are discrete and that there is some global method to distinguish in between them.

Temporal assertions are a very effective way to describe correct execution of a program. Examples are (temporal operators highlighted):

  1. If the elevator is moving up and I press a button on one of the floors above the elevator will go to that floor before it goes to the floors below.
  2. If I enter a subroutine and afterwards allocate a resource. Then I will release that resource before I exit the subroutine.
  3. If I I send a request I will be serviced between 1 to 4 time steps.
  4. etc.

There are a few languages for temporal assertions including PSL (Property Specification Language). PSL is IEEE standard 1850. It was chartered by the Functional Verification Technical Committee of Accellera. After a process in which donations from a number of sources were evaluated, the Sugar language from IBM was chosen as the basis for PSL. The Language Reference Manual for PSL version 1.01 was released in April 2003. The PSL standard is currently owned by Accellera. The PSL/Sugar Consortium is a complementary organisation that exists to facilitate the adoption of PSL by the user community.