Property Specification Language: Difference between revisions

Revision as of 13:47, 22 March 2020

Revision as of 18:22, 11 May 2020

Line 6:

PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a {{mono|request}} should always eventually be {{mono|grant}} ed" can be expressed by the PSL formula:

<sourcesyntaxhighlight lang="text"> always (request -> eventually! grant)

</syntaxhighlight>

</source>

The property "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|busy}} holds at the meantime" can be expressed by the PSL formula:

<sourcesyntaxhighlight lang="text"> (true[*]; req; ack) |=> (start; busy[*]; end) </sourcesyntaxhighlight>

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 <sourcesyntaxhighlight lang="text">(true[*]; req; ack) |=> (start; busy[*]; end)</sourcesyntaxhighlight>]]

PSL's temporal operators can be roughly classified into ''LTL-style'' operators and ''regular-expression-style'' operators. Many PSL operators come in two versions, a strong version, indicated by an exclamation mark suffix ( {{mono|!}} ), and a weak version. The ''strong version'' makes eventuality requirements (i.e. require that something will hold in the future), while the ''weak version'' does not. An ''underscore suffix'' ( {{mono|_}} ) is used to differentiate ''inclusive'' vs. ''non-inclusive'' requirements. An {{mono|_a}} and {{mono|_e}} suffixes are used to denote ''universal'' (all) vs. ''existential'' (exists) requirements. Exact time windows are denoted by {{mono|[n]}} and flexible by {{mono|[m..n]}}.

Line 29:

Here {{mono|s}} and {{mono|t}} are PSL-regular expressions, and {{mono|p}} is a PSL formula.

{| class="wikitable"

| <sourcesyntaxhighlight lang="text"> s |=> t! </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the cycle after s ends,

*the match of t must reach to its end

|-

| <sourcesyntaxhighlight lang="text"> s |-> t! </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the same cycle that s ends,

*the match of t must reach to its end

|-

| <sourcesyntaxhighlight lang="text"> s |=> t </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the cycle after s ends,

*the match of t may "get stuck" in the middle

|-

| <sourcesyntaxhighlight lang="text"> s |-> t </sourcesyntaxhighlight>

| if there is a match of s, then there is a match of t on the suffix of the trace,

*t starts the same cycle that s ends,

Line 61:

| match of s followed by a match of t, t starts the same cycle that s ends

|-

| <sourcesyntaxhighlight lang="text" inline>s | t </sourcesyntaxhighlight>

| match of s or match of t

|-

Line 104:

*equivalent to (!b[*];b)[*i]; !b[*]

|-

| <sourcesyntaxhighlight lang="text" inline> b[=i..j] </sourcesyntaxhighlight>

| at least i and no more than j not necessarily consecutive repetitions of b,

*equivalent to (!b[*];b)[*i..j]; !b[*]

Line 112:

*equivalent to (!b[*];b)[*i..]; !b[*]

|-

| <sourcesyntaxhighlight lang="text" inline> b[->m] </sourcesyntaxhighlight>

| m not necessarily consecutive repetitions of b ending with b,

*equivalent to (!b[*];b)[*m]

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:

<sourcesyntaxhighlight lang="text"> ((true[*]; req; ack) |=> (start; data[=8]; end) </sourcesyntaxhighlight>

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

<sourcesyntaxhighlight lang="text"> ((true[*]; req; ack) |=> (start; data[*3]; end) @ clk </sourcesyntaxhighlight>

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 @]]