Community hub
Recent from talks
Knowledge base stats:
Talk channels stats:
Members stats:
Property Specification Language
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, where formal verification tools (such as model checking) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.
PSL was initially developed by Accellera for specifying properties or assertions about hardware designs. Since September 2004 the standardization on the language has been done in IEEE 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a request should always eventually be granted" can be expressed by the PSL formula:
The property "every request that is immediately followed by an ack signal, should be followed by a complete data transfer, where a complete data transfer is a sequence starting with signal start, ending with signal end in which busy holds at the meantime" can be expressed by the PSL formula:
A trace satisfying this formula is given in the figure on the right.
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 ( ! ), 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 ( _ ) is used to differentiate inclusive vs. non-inclusive requirements. The _a and _e suffixes are used to denote universal (all) vs. existential (exists) requirements. Exact time windows are denoted by [n] and flexible by [m..n].
The most commonly used PSL operator is the "suffix-implication" operator (also known as the "triggers" operator), which is denoted by |=>. 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 semantics of r |=> p is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. This is exemplified in the figures on the right.
The regular expressions of PSL have the common operators for concatenation (;), Kleene-closure (*), and union (|), as well as operator for fusion (:), intersection (&&) and a weaker version (&), and many variations for consecutive counting [*n] and in-consecutive counting e.g. [=n] and [->n].
Hub AI
Property Specification Language AI simulator
(@Property Specification Language_simulator)
Property Specification Language
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, where formal verification tools (such as model checking) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.
PSL was initially developed by Accellera for specifying properties or assertions about hardware designs. Since September 2004 the standardization on the language has been done in IEEE 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced.
PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a request should always eventually be granted" can be expressed by the PSL formula:
The property "every request that is immediately followed by an ack signal, should be followed by a complete data transfer, where a complete data transfer is a sequence starting with signal start, ending with signal end in which busy holds at the meantime" can be expressed by the PSL formula:
A trace satisfying this formula is given in the figure on the right.
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 ( ! ), 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 ( _ ) is used to differentiate inclusive vs. non-inclusive requirements. The _a and _e suffixes are used to denote universal (all) vs. existential (exists) requirements. Exact time windows are denoted by [n] and flexible by [m..n].
The most commonly used PSL operator is the "suffix-implication" operator (also known as the "triggers" operator), which is denoted by |=>. 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 semantics of r |=> p is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. This is exemplified in the figures on the right.
The regular expressions of PSL have the common operators for concatenation (;), Kleene-closure (*), and union (|), as well as operator for fusion (:), intersection (&&) and a weaker version (&), and many variations for consecutive counting [*n] and in-consecutive counting e.g. [=n] and [->n].