Content deleted Content added
moved the history to a history section. I think it is more interesting to start with what PSL is about, rather than the circumstances in which it was created. |
corrected formulas and text relating to the added figures |
||
Line 6:
</source>
The property "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a compete {{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
<source> ((true[*]; req; ack) |=> (start;
A trace satisfying this formula is given in the figure on the right.
[[File:The trigger operator - slide 1.jpg|thumb|a simple trace satisfying <source>(true[*]; req; ack) |=> (start;
===Operators===
Line 194:
==== The Sampling
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]]
The first property states that "every {{color|orange|request}} which is immediately followed by an {{color|orange|ack}} signal, should be followed by a compete {{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|data}} should hold at least 8 times:
<source> ((true[*]; req; ack) |=> (start; data[=8]; end) </source>
But sometimes it is desired to consider only the cases where the above signals occur on a cycle where {{color|orange|clk}} is high.
This is depicted in the second figure in which although the formula
<source> ((true[*]; req; ack) |=> (start; data[*3]; end) @ clk </source>
uses {{color|orange|data[*3]}} and {{color|orange|[*n]}} is consecutive repetition, the matching trace has 3 non-consecutive time points where {{color|orange|data}} holds, but when considering only the time points where {{color|orange|clk}} holds, the time points where {{color|orange|data}} hold become consecutive.
[[File:Multiple clocks.jpg|thumb|path and formula showing effect of the sampling operator @]]
| |||