Content deleted Content added
Pyschobbens (talk | contribs) |
Fixing minor typos |
||
Line 200:
[[File:Need for multiple clocks.jpg|thumb|path and formula showing need for a sampling operator]]
The first property states that "every {{mono|request}} which is immediately followed by an {{mono|ack}} signal, should be followed by a
<source lang="text"> ((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 {{mono|clk}} is high.
Line 232:
===Expressive power===
PSL subsumes the temporal logic [[Linear temporal logic|LTL]] and extends its expressive power to that of the [[omega-regular languages]]. The augmentation in expressive power, compared to that of LTL, which has the expressive power of the star-free ω-regular expressions, can be attributed to the ''suffix implication'', a.k.a. ''triggers'' operator, denoted "|->". The formula ''r |-> f'' where ''r'' is a regular expression and ''f'' is a temporal logic formula holds on a computation ''w'' if any prefix of ''w'' matching ''r'' has a continuation satisfying ''f''. Other non-LTL operators of PSL are the ''@'' operator, for specifying multiply-clocked designs, the ''abort'' operators, for dealing with hardware resets, and ''local variables'' for succinctness.
===Layers===
| |||