ANA в 17:03, 31 декабря 2013

2013-12-31T17:03:41Z

ANA: Новая страница: «{{PSL TOC}} =SERE Style= Up until now, we have seen PSL properties that are built of Boolean expres- sions and temporal operators in LTL style. Another way to b…»

2013-12-31T17:02:26Z

Новая страница: «{{PSL TOC}} =SERE Style= Up until now, we have seen PSL properties that are built of Boolean expres- sions and temporal operators in LTL style. Another way to b…»

Новая страница

{{PSL TOC}}

=SERE Style=

Up until now, we have seen PSL properties that are built of Boolean expres-
sions and temporal operators in LTL style. Another way to build properties is
to use SEREs – Sequential Extended Regular Expressions. SEREs are similar
in spirit to standard regular expressions, like those used for pattern matching
in many applications. One difference is that the atoms of a SERE are Boolean
expressions, whereas the atoms of a standard regular expression are single
characters.

A SERE is typically enclosed in curly braces, and the atoms of the SERE
are typically separated by semi-colons. For instance, <code>{a;b;c}</code> is a SERE, and
SERE 5.1a is a more complicated SERE. SERE 5.1a describes a sequence of
cycles in which <code>(req_out && !ack)</code> is asserted on the first cycle, then <code>(busy && !ack)</code>
is asserted for zero or more cycles, indicated by the consecutive
repetition operator <code>[*]</code>, and finally ack is asserted. Thus, SERE 5.1a matches
the sequence of cycles labeled as “1” in Trace 5.1(i).

Don’t be tempted into reading more into a SERE than is actually there:
SERE 5.1a matches the sequence of cycles labeled as “2” in Trace 5.1(i) as well.
SERE 5.1a does not prohibit the assertion of busy during the last cycle of the
SERE. If it is important to exclude such behavior, busy must be mentioned
explicitly, as shown in SERE 5.1b. SERE 5.1b matches the sequence of cycles
labeled as “1” shown in Trace 5.1(i), but does not match the sequence of
cycles labeled as “2” in that trace.

How is a SERE used? First, since a SERE is a property, it can be used
as a sub-property. For example, Property 5.2a holds if whenever there is an
assertion of <code>req_in && gnt</code> then starting on the next cycle we see a sequence
of cycles matching SERE 5.1a. Property 5.2a holds on Trace 5.2(i).

NOTE: A SERE is a property, but a property is not a SERE. Thus, while
you can use a SERE as an operand of a temporal operator, you cannot embed
a temporal operator such as <code>always</code> or <code>next</code> inside of a SERE.

Suppose now that we have a situation similar to that of Property 5.2a, but
in which a grant (assertion of signal <code>gnt</code>) is given the cycle ''after'' the assertion of
<code>req_in</code>. We could try to replace the Boolean expression <code>req_in && gnt</code> with
the temporal expression <code>req_in && next gnt</code>, as in Property 5.3a. However,
remember the lesson of Section 3.4: in Property 5.3a the current cycle of the
left-hand side <tt>(req_in && next gnt)</tt> is the same as the current cycle of the
right-hand side (because they are connected by the Boolean operator <tt>-></tt>).
Thus, the current cycle of <code>gnt</code> (which is the operand of a <code>next</code> operator) is
the same as the current cycle of the SERE (which is also the operand of <code>next</code> operator).
This is slightly confusing, and indeed Property 5.3a is not in
the simple subset of PSL discussed in Chapter 9.

Let’s modify Property 5.3a as shown in Property 5.3b. Now a single <code>next</code>
operator is applied to both <code>gnt</code> and the SERE, which are both operands of
the <code>-></code> operator. Property 5.3b is equivalent to Property 5.3a, but is in the
simple subset, making the timing between <code>gnt</code> and the SERE easier to see. If
we mean that the current cycle of the SERE should be the cycle ''after'' that of
<code>gnt</code>, we can manipulate Property 5.3b by adding a <code>next</code> as in Property 5.3c.
However, the suffix implication operators provide a much easier way.

{| align=center
! [[Файл:Psl fig5.1.png]]
|-
!(i) SERE 5.1a matches both 1 and 2. SERE 5.1b matches 1, but not 2.
|-
|<pre>
{(req_out && !ack) ; (busy && !ack)[*] ; ack} (5.1a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack && !busy} (5.1b)
</pre>
|-
! Fig. 5.1: Two simple SEREs
|}

{| align=center
! [[Файл:Psl fig5.2.png]]
|-
!(i) Property 5.2a holds
|-
|<pre>
always ((req_in && gnt) -> (5.2a)
next {(req_out && !ack) ; (busy && !ack)[*] ; ack})
</pre>
|-
! Fig. 5.2: A SERE is a property
|}

{| align=center width=80%
|<pre>
always ((req_in && next gnt) -> (5.3a)
next {(req_out && !ack) ; (busy && !ack)[*] ; ack})
always (req_in -> next (gnt -> (5.3b)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}))
always (req_in -> next (gnt -> (5.3c)
next {(req_out && !ack) ; (busy && !ack)[*] ; ack}))
</pre>
|-
! Fig. 5.3: Property 5.3a is not in the simple subset. Properties 5.3b and 5.3c are
in the simple subset, but are difficult to read. These properties can be
expressed more easily using suffix implication.
|}

==5.1 Suffix implication (<code>|-></code> and <code>|=></code>)==

The ''suffix implication'' operators (<code>|-></code> and <code>|=></code>) provide a way to link two
SEREs in such a way that the right-hand side starts when the left-hand side
finishes. The overlapping suffix implication operator (<code>|-></code>) interprets “when
the left-hand side finishes” as “at the same cycle as the cycle in which the
left-hand side finishes”, while the non-overlapping suffix implication operator
(<code>|=></code>) interprets it as “the cycle after the cycle in which the left-hand side fin-
ishes”. Thus, Property 5.4a is equivalent to Property 5.3b, and Property 5.4b
is equivalent to Property 5.3c. Both Property 5.4a and Property 5.4b are eas-
ier to grasp than the equivalent property without suffix implication, and both
belong to the simple subset, discussed in Chapter 9.

{| align=center
! [[Файл:Psl fig5.4.png]]
|-
|<pre>
always {req_in;gnt} |-> (5.4a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
always {req_in;gnt} |=> (5.4b)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}

</pre>
|-
! Fig. 5.4: Suffix implication
|}

Recall that the logical implication operator (<code>-></code>) can be understood as an
if-then expression, with the else-part being implicitly true. The suffix implica-
tion operators (<code>|-></code> and <code>|=></code>) can be understood the same way. The difference
between the logical implication operator (<code>-></code>) and the suffix implication op-
erators (<code>|-></code> and <code>|=></code>) is in the timing relationship between the if- and the
then-parts. While the current cycle of the then-part of a logical implication
operator (->) is the same as the current cycle of its if-part, the current cycle
of the then-part of a suffix implication operator (<code>|-></code> or <code>|=></code>) is the first cycle
of the ''suffix'' of the trace that remains once the if-part has been seen. This is
illustrated for Properties 5.4a and 5.4b in Traces 5.4(i) and 5.4(ii).

{| align=center
! [[Файл:Psl fig5.5.png]]
|-
! (i) A trace having multiple if-then pairs. Property 5.5a holds.
|-
|<pre>
always {req_in;gnt} |=> (5.5a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
</pre>
|-
! Fig. 5.5: The if-part of another if-then pair may begin before the if-part or the
then-part of a previous if-then pair has completed
|}

In Traces 5.4(i) and 5.4(ii) there is a single assertion of signal <code>req_in</code>.
If there are multiple assertions of <code>req_in</code>, then of course we will be able to
identify multiple if-then pairs, as shown in Trace 5.5(i). Note that the if-part of
another if-then pair may begin before the if-part or the then-part of a previous
if-then pair has completed. For instance, the second if-then pair starts at cycle
7, before the then-part of the first if-then pair has completed. The third if-
then pair starts at cycle 8, before the then-part of the first if-then pair has
completed, and before the if-part of the second if-then pair has completed.
We have seen this kind of overlapping previously, in Traces 2.2(ii) and 2.3(iii).
Note that in Trace 5.5(i), the assertion of <code>ack</code> at cycle 16 completes the then-
part of the second and of the third if-then pair. For a deeper discussion of this
phenomenon, see Section 13.4.2.

Properties 5.6a and 5.6b hold on Trace 5.6(i) because there is no sequence
of cycles matching the left-hand side, thus the else-parts default to true at
every cycle.

{| align=center
! [[Файл:Psl fig5.6.png]]
|-
! (i) Properties 5.6a and 5.6b both hold
|-
|<pre>
always {req in;gnt} |-> (5.6a)
{(req out && !ack) ; (busy && !ack)[*] ; ack}
always {req in;gnt} |=> (5.6b)
{(req out && !ack) ; (busy && !ack)[*] ; ack}
</pre>
|-
! Fig. 5.6: The else-part of a suffix implication defaults to true
|}

==5.2 Weak and strong SEREs==

@@ Строка 181: / Строка 181: @@
 |-
 |<pre>
-always {req in;gnt} |->                               (5.6a)
+always {req_in;gnt} |->                               (5.6a)
-     {(req out && !ack) ; (busy && !ack)[*] ; ack}
+     {(req_out && !ack) ; (busy && !ack)[*] ; ack}
-always {req in;gnt} |=>                               (5.6b)
+always {req_in;gnt} |=>                               (5.6b)
-     {(req out && !ack) ; (busy && !ack)[*] ; ack}
+     {(req_out && !ack) ; (busy && !ack)[*] ; ack}
 </pre>
 |-

PSL/A Practical Introduction to PSL/SERE Style/ru - История изменений

ANA в 17:03, 31 декабря 2013

ANA: Новая страница: «{{PSL TOC}} =SERE Style= Up until now, we have seen PSL properties that are built of Boolean expres- sions and temporal operators in LTL style. Another way to b…»