Editing Property Specification Language (section)

=== 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 level of abstraction is desired. The ''sampling operator''  (also known as the ''clock operator''), denoted {{mono|@}}, is used for this purpose. The formula {{mono| p @ c }} where {{mono| p}}  is a PSL formula and {{mono|c}}  a PSL Boolean expressions holds on a given path if {{mono| p}}  on that path projected on the cycles in which {{mono| 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  {{mono|request}} that is immediately followed by an  {{mono|ack}}  signal, should be followed by a complete  {{mono|data transfer}}, where a complete data transfer is a sequence starting with signal {{mono|start}}, ending with  signal {{mono|end}} in which  {{mono|data}} should hold at least 8 times: 
<syntaxhighlight lang="text">  (true[*]; req; ack)  |=> (start; data[=8]; end) </syntaxhighlight>
But sometimes it is desired to consider only the cases where the above signals occur on a cycle where {{mono|clk}} is high. 
This is depicted in the second figure in which although the formula 
<syntaxhighlight lang="text">  ((true[*]; req; ack)  |=> (start; data[*3]; end)) @ clk </syntaxhighlight>
uses  {{mono|data[*3]}} and {{mono|[*n]}} is consecutive repetition, the matching trace has 3 non-consecutive time points where {{mono|data}} holds, but when considering only the time points where {{mono|clk}} holds, the time points where {{mono|data}} hold become consecutive. 
[[File:Multiple clocks.jpg|thumb|path and formula showing effect of the sampling operator @]]

The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2].