PSL/A Practical Introduction to PSL/Weak vs. Strong Temporal Operators
Материал из Wiki
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Содержание |
Weak vs. Strong Temporal Operators
Temporal operators can be weak or strong. A strong temporal operator such as
eventually!
is indicated by an exclamation point (!
) as part of its name. An
operator without an exclamation point, such as next
, is weak. Up until now
we have seen only one version of each operator, but many of the operators we
have seen previously come in both weak and strong versions. The difference
between weak and strong operators is important when the path is “too short”
to determine whether or not everything that needs to happen to satisfy a
property has indeed happened.1 For instance, consider the specification “every
assertion of signal a must be followed three cycles later by an assertion of signal
b
”, on Trace 4.1(i). Does the specification hold or not? The assertion of signal
a at cycle 2 is satisfied by the assertion of signal b at cycle 5. But what about
the assertion of signal a at cycle 9? It requires an assertion of signal b at cycle
12, but the trace ends before cycle 12 is reached. Weak and strong temporal
operators allow us to distinguish between the case where we would like to say
that our specification holds on Trace 4.1(i), and the case where we would like
to say that it does not.
1 - In this chapter we assume finite paths such as those seen in simulation. On infinite paths, such as those seen in formal verification, there is also a difference between weak and strong operators. We discuss this issue in Chapter 11.
A weak temporal operator is lenient – in the case that a trace ends “too soon”, a property using a weak temporal operator will hold as long as nothing else has gone wrong. If we were to continue the verification run shown in Trace 4.1(i) for a few more cycles, we might find out that signal b is asserted in cycle 12. It could happen. Thus, Assertion 4.1a, which uses the weak next operator, holds on Trace 4.1(i).
A strong temporal operator is strict – in the case that a trace ends “too
soon”, a property using a strong operator will not hold, even if nothing else
has gone wrong. There is no way to know what will happen if we continue the
verification run shown in Trace 4.1(i) for a few more cycles, and we shouldn’t
say that a property holds without having all the information. Thus, Assertion 4.1b, which uses the strong next!
operator, does not hold on Trace 4.1(i).
![]() |
---|
(i) Assertion 4.1a holds, but 4.1b does not |
assert always(a -> next[3] (b)); (4.1a) assert always(a -> next![3] (b)); (4.1b) |
Fig. 4.1: A trace illustrating the idea behind weak and strong operators |
Below we present the families of strong operators, in the same order in
which their weak cousins were presented, and contrast the weak and strong
versions.
4.1 The next! operator
Assertion 4.3a states that whenever a holds, then b should hold in the next
cycle. Using the strong version of the next
operator, we get Assertion 4.3b
which requires that in addition, there be a next cycle. For example, while
Assertion 4.3a holds on Trace 4.3(i), Assertion 4.3b does not, because even
though b
is asserted after the first two assertions of a
, the trace ends too soon
with regards to the third assertion of a
.
![]() |
---|
(i) Assertion 4.3a holds, but 4.3b does not |
assert always (a -> next b); (4.3a) assert always (a -> next! b); (4.3b) |
Fig. 4.3: Weak vs. strong next |
4.2 Variations on next!
including next_event!
The strong next_event!
operator is related to its weak version next_event
in
the same way that the strong next!
operator is related to next
. For example,
Assertion 4.4b does not hold on Trace 4.4(i), because there are not enough
grants. However, the weak version, Assertion 4.4a, does hold on the same
trace.
The next![n]
operator allows you to indicate that at least n
next cycles
are needed, and the next_event!(b)[n]
operator allows you to indicate that
at least n
occurrences of the Boolean event b
are needed.
You should by now be able to guess the meaning of the next_a![i:j]
and next_event_a!(b)[i:j]
operators. The next_a![i:j]
operator holds if
there are at least j additional cycles, and its operand holds on all of the ith
through jth of them, inclusive. The next_event_a!(b)[i:j]
operator holds if
there are at least j additional cycles on which b
holds, and the second operand
holds on all of the ith through jth of them, inclusive.
The next_e![i:j]
operator creates a property that holds if its operand
holds on at least one of the ith through jth next cycles, inclusive. There
do not have to be j cycles if the operand holds on some cycle between the
ith and the jth, inclusive. Similarly, the next_event_e!(b)[i:j]
operator
creates a property that holds if its second operand holds on at least one of
the ith through j th next occurrences of b
, inclusive. There do not have to be
j occurrences if the second operand holds on some occurrence between the ith
and the jth, inclusive. For example, consider Assertion 4.5b, which states that
a request (assertion of req
) must be acknowledged (assertion of ack
) on one of
the next four grants, and that in addition, the trace must not end before there
is an appropriate grant. Assertion 4.5b does not hold on Trace 4.5(i) because
none of the three grants shown is acknowledged. However, it does hold on
Trace 4.5(ii) because at least one of the first, second, third or fourth grants
is acknowledged. The fact that the fourth grant does not occur is immaterial
– there is no way for a fourth grant to change the fact that we know for sure
that one of the first, second, third or fourth grants is acknowledged.
The weak version of Assertion 4.5b holds on both Trace 4.5(i) and Trace 4.5(ii). The only way to violate the weak version shown in Assertion 4.5a is for there to be four grants, none of which are acknowledged.
![]() |
---|
assert always (req -> next_event_e(gnt)[1:4](ack)); (4.5a) assert always (req -> next_event_e!(gnt)[1:4](ack)); (4.5b) |
Fig. 4.5: Weak vs. strong next_event_e[i:j]
|
4.3 The until! and until! operators
We have previously seen assertions like Assertion 4.6a, which states that whenever a
is asserted, then starting the next cycle b
should be asserted until c
is
asserted. For example, Assertion 4.6a holds on Trace 4.6(i). But what about
a trace like that shown in Trace 4.6(ii), where c
never arrives? Does Assertion 4.6a hold on Trace 4.6(ii) or not? It does. The reason is that the until
operator is a weak operator.
If we want to express the requirement of Assertion 4.6a, but in addition
insist that c
eventually occur, we need to use a strong operator. Assertion 4.6b,
which uses a strong operator, does not hold on Trace 4.6(ii).
The until!_
operator is the strong version of the until_
operator. The
until!_
operator holds only if its left operand stays asserted up to and including
the cycle where its right operand is asserted, and in addition its right
operand eventually holds.
![]() |
---|
assert always(a -> next (b until c)); (4.6a) assert always(a -> next (b until! c)); (4.6b) |
Fig. 4.6: Weak vs. strong until |
4.4 The before!
and before!_
operators
The emphasis of the strong versions of the before
operators is on their lefthand operand. For example, Assertion 4.7a states that following an assertion
of req
, an assertion of gnt
is required before req
can be asserted again, but
being weak holds not only on Trace 4.7(ii), but also on Trace 4.7(i), in which
after the second request neither a grant nor a third request ever arrives. The
strong version, shown in Assertion 4.7b, requires that a grant eventually be
given, but not necessarily that another request be seen. Thus, Assertion 4.7b
does not hold on Trace 4.7(i), but holds on Trace 4.7(ii).
![]() |
---|
assert always (req -> next (gnt before req)); (4.7a) assert always (req -> next (gnt before! req)); (4.7b) |
Fig. 4.7: Weak vs. strong before |
The before!_
operator is the strong version of the before_
operator. Thus,
Assertion 4.8a holds on Trace 4.8(i), in which the first request (assertion of
signal req
) is granted (assertion of signal gnt
) but the second is not. The
strong version of Assertion 4.8a, shown in Assertion 4.8b, does not hold on
Trace 4.8(i) because the second request is not granted. Both Assertion 4.8a
and 4.8b hold on Trace 4.8(ii).
![]() |
---|
assert always (req -> next (gnt before_ req)); (4.8a) assert always (req -> next (gnt before!_ req)); (4.8b) |
Fig. 4.8: Weak vs. strong before_
|
4.5 Operators without weak or strong versions
We have seen weak and strong versions of many operators. The eventually!
operator is not a strong version of some other operator. In other words, there
is no weak version of eventually!
. The reason is that the meaning of other
strong operators can be broadly described as requiring that nothing bad must
happen up until some terminating condition, and in addition, the terminating condition must eventually occur. The weak versions then waive the requirement that the terminating condition eventually occur, leaving only the requirement that nothing bad must happen. The eventually!
operator, however, contains no idea of a bad “something”, only a terminating condition.
Therefore, there is no way to weaken it without emptying it completely of
meaning.
Just as there is no weak version of eventually!
, there is no strong version
of the operators always
and never
, for the opposite reason. In the case of
always
and never
, there is no terminating condition to waive.