PSL/A Practical Introduction to PSL/Some Philosophy/ru
- Introduction (en)
- Basic Temporal Properties (en)
- Some Philosophy (en)
- Weak vs. Strong Temporal Operators (en)
Содержание |
Some Philosophy
We have seen some basic PSL and gotten a feel for how it is intended to be used. Before we continue, we discuss some of the concepts at the root of PSL.
3.1 Assertions vs. properties
As we have seen, a PSL assertion is made up of the keyword assert plus
the PSL property being asserted, followed by a semi-colon. For example, in
the assertion assert always (a -> next b);, the property is always (a -> next b). A property holds or does not hold on a given trace. It is agnostic
about whether or not holding is a good thing. An assertion, on the other hand,
tells the verification tool that the property being asserted is required to hold.
In the remainder of this book we will be very careful about distinguish-
ing between a property, which merely describes behavior, and an assertion,
which sets a requirement. For example, we might say that an assertion assert always (a -> next b); requires that whenever signal a is asserted, signal
b will be asserted in the next cycle. However, we will never say that about
the property always (a -> next b), for two reasons. First, because if the
property is used in an assumption (assume always (a -> next b);), then
no requirement is being stated. Second, because a property may be used as a
sub-property of a more complicated property, and as such, it does not state a
requirement on its own.
3.2 The notion of time
When a Boolean assertion is embedded in code that is being run, like in the simple assertions of Java and (simulated) VHDL, the notion of time need not be defined – an assertion is checked whenever the statement containing the assertion is executed. For the more complicated assertions of PSL, which first of all stand apart from the code (so that the notion of “execution” is foreign to them) and which second of all span multiple time steps, the notion of time must be given more consideration.
PSL assumes that time is discrete, that is, that time consists of a sequence of evaluation cycles. The meaning of a PSL property is defined relative to such a sequence of cycles. In this book, we will refer to such a sequence of cycles as a trace.
PSL does not dictate how time ticks – that is, it does not dictate how such a sequence of cycles is extracted from a design under verification. This means that the sequence of cycles as seen by two verification tools is not necessarily the same. For example, a cycle-based simulator sees a sequence of signal values calculated cycle-by-cycle, while an event-based simulator running on the same design sees a more detailed sequence of signal values.
Nevertheless, there is a way to ensure that the meaning of a PSL property is not affected by the granularity of time as seen by the verification tool. PSL properties can be modified by using a clock expression to indicate that time should be measured in clock cycles of the clock expression. In the case of a clocked property, the result of a cycle-based tool will be the same as the result of an event-based tool. PSL allows the specification of a default clock, so that the clock does not have to be mentioned explicitly for each and every property. In most of this book we have assumed a singly clocked design under the cycle-based model, and thus most examples omit the explicit mention of the clock. Clocks are discussed in detail in Chapters 6 and 14.
