Content deleted Content added
Line 7:
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{color|orange|request}} should always eventually be {{color|orange|grant}} ed" can be expressed by the PSL formula:
<source lang="text"> always (request -> eventually! grant)
</source>
The property "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a complete {{color|orange|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orange|start}}, ending with signal {{color|orange|end}} in which {{color|orange|busy}} holds at the meantime" can be expressed by the PSL formula:
Line 18:
=== SERE-style operators===
The most commonly used PSL operator is the "suffix-implication" operator (a.k.a. the "triggers" operator), which is denoted by <math> \texttt{|=>} </math>. Its left operand is a PSL regular expression and its right operand is any PSL formula (be it in LTL style or regular expression style). The semantics of <math>\texttt{r |=>p}</math> is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. This is exemplified in the figures on the right.
[[File:The trigger operator - slide 2.jpg|thumb|path satisfying ''r triggers p'' in two non-overlapping ways]]
[[File:The trigger operator - slide 3.jpg|thumb|path satisfying ''r triggers p'' in two overlapping ways]]
Line 75:
|}
Operators for consecutive repetitions are shown in the table below.
Here {{color|orange|s}} is a PSL regular expression.
Line 96:
|}
Operators for non-consecutive repetitions are shown in the table below.
Here {{color|orange|b}} is any PSL Boolean expression.
Line 197:
=== Sampling operator===
Sometimes it is desirable to change the definition of the ''next time-point'', for instance in multiply-clocked designs, or when a higher lever of abstraction is desired. The ''sampling operator'' (a.k.a. ''the clock operator''), denoted {{color|red|@}}, is used for this purpose. The formula {{color|orange| p @ c }} where {{color|orange| p}} is a PSL formula and {{color|orange|c}} a PSL Boolean expressions holds on a given path if {{color|orange| p}} on that path projected on the cycles in which {{color|orange| c}} holds, as exemplified in the figures to the right.
[[File:Need for multiple clocks.jpg|thumb|path and formula showing need for a sampling operator]]
Line 209:
The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].
=== Abort operators ===
| |||