Overview

Up until now, we have seen PSL properties that are built of Boolean expressions and temporal operators in LTL style. Another way to build properties is to use SEREs Sequential Extended Regular Expressions. SEREs are similar in spirit to standard regular expressions, like those used for pattern matching in many applications. One difference is that the atoms of a SERE are Boolean expressions, whereas the atoms of a standard regular expression are single characters.

A SERE is typically enclosed in curly braces, and the atoms of the SERE are typically separated by semi-colons. For instance, { a;b;c} is a SERE, and SERE 5.1a is a more complicated SERE. SERE 5.1a describes a sequence of cycles in which (req_out && !ack) is asserted on the first cycle, then (busy && !ack) is asserted for zero or more cycles, indicated by the consecutive repetition operator [*], and finally ack is asserted. Thus, SERE 5.1a matches the sequence of cycles labeled as "1" in Trace 5.1(i).

Don't be tempted into reading more into a SERE than is actually there: SERE 5.1a matches the sequence of cycles labeled as "2" in Trace 5.1(i) as well. SERE 5.1a does not prohibit the assertion of busy during the last cycle of the SERE. If it is important to exclude such behavior, busy must be mentioned explicitly, as shown in SERE 5.1b. SERE 5.1b matches the sequence of cycles labeled as "1" shown in Trace 5.1(i), but does...