Property Specification Language: Difference between revisions

Content deleted Content added
m Task 70: Update syntaxhighlight tags - remove use of deprecated <source> tags
Line 201:
 
The first property states that "every {{mono|request}} which 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 @]]