Previously, in Section 3.4, we saw Assertion 3.3a (repeated here as Assertion 9.1a), in which, if a is asserted at cycle N, we must look ahead to cycle N + 6 to see whether b holds in order to know whether or not we require c to be asserted at N and d to be asserted at N + 2. Such an assertion is not a part of the simple subset of PSL. In the simple subset, time flows from left to right through the property, in the following way: considering each Boolean expression and each SERE as an atomic entity, if we need to know the value of such an entity at cycle M, then the value of everything to the right of the entity need not be known before cycle M.

Figure 9.1: A property not in the simple subset

For a PSL property to be in the simple subset, it must obey the rules shown in Table 9.1. ^[1] All operators not appearing in the table, and in particular the operators always, next, next_a, next_event, next_event_a, and all forms of suffix implication are allowed without restriction in the simple subset.