Property Specification Language: Difference between revisions

Revision as of 15:34, 3 August 2015

Revision as of 15:37, 3 August 2015

Line 81:

The most commonly used PSL operator is the "suffix-implication" operator (a.k.a the "triggers" operator), which is denoted by {{code|{{!}}->}}. Its left operand is a PSL regular expression and its right operand is any PSL formula (be it in LTL style or regular expression style). The regular expressions of PSL have the common operators for concatenation ({{color|red|;}}), Kleene-closure ({{color|red|*}}), and union ({{color|red|{{code|{{!}}}}}}), as well as operator for fusion ({{color|red|:}}), intersection ({{color|red|&&}}) and a weaker version ({{color|red|&}}), and many variations for counting {{color|red|[*n]}}, {{color|red|[->n]}}, {{color|red|[=n]}}.

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

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

{| class="wikitable"

Line 106 ⟶ 107:

|}

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

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

{| class="wikitable"

Line 129 ⟶ 131:

|}

Operators for consecutive repetitions are shown in the table below.

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

{| class="wikitable"

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

Line 148 ⟶ 152:

|}

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

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

{| class="wikitable"

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

Line 182 ⟶ 188:

==== The Abort Operators ====

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|orange|p}} is any PSL formula and {{color|orange|b}} is any PSL Boolean expression.

{| class="wikitable"

Line 213 ⟶ 220:

===Language compatibility===

Property Specification Language aims tocan be used with multiple electronic system design languages (HDLs) such as:

* [[VHDL]] (IEEE 1076),

* [[Verilog]] (IEEE 1364),