Overview

While the Boolean layer consists of Boolean expressions that hold or do not hold at a given cycle, the temporal layer provides a way to describe relationships between Boolean expressions over time. A PSL assertion typically looks in only one direction forwards from the first cycle (although it is possible to look backwards using built-in functions such as prev(), rose() and fell()). Thus, the simple PSL assertion assert a; states that a should hold at the very first cycle, while the PSL assertion assert always a; states that a should hold at the first cycle and at every cycle following the first cycle that is, at every cycle.

By combining the temporal operators in various ways we can state properties such as "every request receives an acknowledge", "every acknowledged request receives a grant within four to seven cycles unless the request is canceled first", "two consecutive writes should not be to the same address", and "when we see a read request with tag equal to i, then on the next four data transfers we expect to see a tag of i".

The temporal layer is composed of the Foundation Language (FL) and the Optional Branching Extension (OBE). The FL is used to express properties of single traces, and can be used in either simulation or formal verification. The OBE is used to express properties referring to sets of traces, for example "there exists a trace such that