TABLE OF CONTENTS 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.
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 distinguishing 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...
