Property Specification Language: Difference between revisions

Revision as of 08:56, 26 May 2017

Revision as of 09:00, 26 May 2017

Line 5:

== Syntax and semantics ==

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

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

</source>

The property "every {{color|orangemono|request}} which is immediately followed by an {{color|orangemono|ack}} signal, should be followed by a complete {{color|orangemono|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orangemono|start}}, ending with signal {{color|orangemono|end}} in which {{color|orangemono|busy}} holds at the meantime" can be expressed by the PSL formula:

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

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

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 ( {{color|redmono|!}} ), 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'' ( {{color|redmono|_}} ) is used to differentiate ''inclusive'' vs. ''non-inclusive'' requirements. An {{color|redmono|a_}} and {{color|redmono|e_}} suffixes are used to denote ''universal'' vs. ''existential'' requirements. Exact time windows are denoted by {{color|redmono|[n]}} and flexible by {{color|redmono|[m..n]}}.

=== SERE-style operators===

Line 27:

The trigger operator comes in several variations, shown in the table below.

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

{| class="wikitable"

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

Line 53:

Operators for concatenation, fusion, union, intersection and their variations are shown in the table below.

Here {{color|orangemono|s}} and {{color|orangemono|t}} are PSL regular expressions.

{| class="wikitable"

| <code> s ; t </code>

Line 77:

Operators for consecutive repetitions are shown in the table below.

Here {{color|orangemono|s}} is a PSL regular expression.

{| class="wikitable"

| <code> s[*i] </code>

Line 98:

Operators for non-consecutive repetitions are shown in the table below.

Here {{color|orangemono|b}} is any PSL Boolean expression.

{| class="wikitable"

| <code> b[=i] </code>

Line 134:

Below is a sample of some LTL-style operators of PSL.

Here {{color|orangemono|p}} and {{color|orangemono|q}} are any PSL formulas.

{| class="wikitable"

| always p

Line 197:

=== 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 lever of abstraction is desired. The ''sampling operator'' (a.k.a. ''the clock operator''), denoted {{color|redmono|@}}, is used for this purpose. The formula {{color|orangemono| p @ c }} where {{color|orangemono| p}} is a PSL formula and {{color|orangemono|c}} a PSL Boolean expressions holds on a given path if {{color|orangemono| p}} on that path projected on the cycles in which {{color|orangemono| 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|orangemono|request}} which is immediately followed by an {{color|orangemono|ack}} signal, should be followed by a compete {{color|orangemono|data transfer}}, where a complete data transfer is a sequence starting with signal {{color|orangemono|start}}, ending with signal {{color|orangemono|end}} in which {{color|orangemono|data}} should hold at least 8 times:

<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 {{color|orangemono|clk}} is high.

This is depicted in the second figure in which although the formula

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

uses {{color|orangemono|data[*3]}} and {{color|orangemono|[*n]}} is consecutive repetition, the matching trace has 3 non-consecutive time points where {{color|orangemono|data}} holds, but when considering only the time points where {{color|orangemono|clk}} holds, the time points where {{color|orangemono|data}} hold become consecutive.

[[File:Multiple clocks.jpg|thumb|path and formula showing effect of the sampling operator @]]

Line 214:

PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of the computation). Truncated paths occur in bounded-model checking, due to resets and in many other scenarios. The abort operators, specify how eventualities should be dealt with when a path has been truncated. They rely on the truncated semantics proposed in [1].

Here {{color|orangemono|p}} is any PSL formula and {{color|orangemono|b}} is any PSL Boolean expression.

{| class="wikitable"

| <code> p async_abort b </code>