TABLE OF CONTENTS In this chapter, we discuss some common errors that beginning users of PSL tend to make, and provide some guidelines for avoiding them.
As we have seen, the logical implication ( ->) and suffix implication operators ( -> and =>) are very useful for stating if-then kinds of properties in a concise manner. However, beginning users often misuse them. In this section we examine various ways in which beginning users abuse logical and suffix implications.
Both logical implications and suffix implications can be thought of as if-then expressions, with the else-part defaulting to true. The difference is in the current cycle of the then-part. The current cycle of the then-part of a logical implication is the same as the current cycle of its if-part. The current cycle of the then-part of a suffix implication is the first cycle of the suffix of the trace that remains once the if-part has been seen. Suppose, for instance, that we want to state that once we see a request (assertion of req) followed by an acknowledge (assertion of ack) followed by a grant (assertion of gnt), we expect to see a complete data transfer (assertion of data for four cycles followed by an assertion of dataend). A beginner might code Assertion 13.1a. This is a mistake! The reason is that Assertion 13.1a uses a logical implication, and therefore requires that...
