«Бог не меняет того, что (происходит) с людьми, пока они сами не изменят своих помыслов.» Коран, Сура 12:13

PSL/A Practical Introduction to PSL/Weak vs. Strong Temporal Operators

Материал из Wiki

< 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).


Psl fig4.1.png
(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.


Psl fig4.2.png
(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

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.


Psl fig4.3.png
(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.


Psl fig4.4.png
(i) Assertion 4.4a holds, but 4.4b does not
assert always (high_pri_req ->
    next_event(gnt)(high_pri_ack));    (4.4a)
assert always (high_pri_req ->
    next_event!(gnt)(high_pri_ack));   (4.4b)
Fig. 4.4: Weak vs. strong next_event


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.


Psl fig4.5.png
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.


Psl fig4.6.png
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).


Psl fig4.7.png
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).


Psl fig4.8.png
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.