PSL/A Practical Introduction to PSL/Basic Temporal Properties/ru
Basic Temporal Properties While
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 ...”, and is used in formal verification. In this book we concentrate on the Foundation Language.
The Foundation Language itself is composed of two complementary styles – LTL style, named after the temporal logic LTL on which PSL is based, and SERE style, named after PSL’s Sequential Extended Regular Expressions, or SEREs. In this chapter we present the basic temporal operators of LTL style. We provide only a taste – enough to get the basic idea and to give some context to the philosophical issues that we discuss next.
Throughout this book, we make extensive use of examples. Each example property or assertion and its associated timing diagram (which we term a trace) are grouped together in a figure. Such a figure will contain one or more traces numbered with a parenthesized lower case Roman numeral, and one or more properties numbered by appending a lower case letter to the figure number. For instance, Figure 2.1 contains Trace 2.1(i) and Assertions 2.1a, 2.1b, and 2.1c.
