< PSL
Это снимок страницы. Он включает старые, но не удалённые версии шаблонов и изображений.
Литература
Введение в PSL
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
|
|
NOTE: A weak temporal operator is lenient even about ‘false, and a
strong temporal operator is strict even about ‘true. Thus, Assertion 4.2a
holds on Trace 4.2(i) because ‘false is treated as something that could happen in the future, and Assertion 4.2b does not hold on Trace 4.2(i) because ‘true is not treated as a sure thing.
|
|
| (i) Assertion 4.2a holds, but 4.2b does not
|
assert always(a -> next[3] (‘false)); (4.2a)
assert always(a -> next![3] (‘true)); (4.2b)
|
Fig. 4.2: A weak temporal operator is lenient even about ‘false,
and a strong temporal operator is strict even about ‘true
|
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
|
|
|
|
| Fig.
|
|
|
|
|
| Fig.
|
|
|
|
|
| Fig.
|
|
|
|
|
| Fig.
|
|
|
|
|
| Fig.
|
|
|
|
|
| Fig.
|
