PSL/A Practical Introduction to PSL/Weak vs. Strong Temporal Operators
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Содержание |
Слабые временные операторы против сильных временных операторов
Временные операторы могут быть слабыми или сильными. Сильны временной оператор, такой как eventually! показан восклицательным знаком, как частью своего имени. Оператор без восклицательного , такой как next, слабый. До этого времени мы видели только по одной версии каждого оператора, но много операторов, которых мы видели до того, могут иметь слабую и сильную версии. Различие между слабыми и сильными операторами очень важны, когда путь “слишком короткий”, чтобы определить, действительно все ли произошло для удовлетворения свойства. 1 Например, рассматривая спецификацию “каждое утверждения сигнала a должно происходить на три цикла раньше утверждения сигнала b” на тракте 4.1(i). Выполняется спецификация или нет? Утверждение сигнала a в цикле 2 удовлетворяется утверждением сигнала b на цикле 5. Но, что можно сказать про утверждение сигнала a на цикле 9? Это предполагает утверждение сигнала b на цикле 12, но тракт заканчивает до достижения 12-го цикла. Слабые и сильные временные операторы позволяют нам различать случаи, в которых мы можем сказать,что наша спецификация выполняется на тракте 4.1(i), и в которых мы можем сказать, что она не выполняется.
1 - В этой главе мы рассмотрим конечные пути, т.к. как они выглядят с точки зрения моделирования. Для бесконечных путях, т.к. они представлены в формальной верификации, также существует разница между слабыми и сильными операторами. Это мы обсудим в главе 11.
Слабы временной оператор податливый - в случаи, когда тракт заканчивается “слишком быстро”, свойство, использующее слабый оператор, будет выполнятся до тех пор, пока что-нибудь не пойдет ни так. Если бы мы продолжили ход верификации в тракте 4.1(i) еще на несколько циклов, мы могли бы обнаружить, что сигнал b утверждается в цикле 12. Такое может случится. Таким образом, утверждение 4.1а, которое использует слабый оператор next, выполняется в тракте 4.1(i).
Сильный оператор строгий - в случаи, когда тракт заканчивается “слишком быстро”, свойство, использующее сильный оператор, не будет выполняться, даже если ничего плохого не происходит. Не существует пути узнать, что бы случилось, если бы мы продолжили ход верификации, показанный в тракте 4.1(i), еще несколько циклов, и мы не можем сказать, что свойство выполняется, не имея всей информации. Таким образом, утверждение 4.1b, которое использует сильный оператор next!, не выполняется на тракте 4.1(i).
|
|---|
| (i) Утверждение 4.1a выполняется, but 4.1b не выполняется |
assert always(a -> next[3] (b)); (4.1a) assert always(a -> next![3] (b)); (4.1b) |
| Рис. 4.1: Тракт иллюстрирует идею слабого и сильного оператора |
{{Слабый временной оператор податливый, даже при ‘false, а сильный временной оператор строгий, даже при ‘true. Таким образом, утверждение 4.2а выполняется на тракте 4.2(i), потому что ‘false трактуется, как что-то, что может случится в будущем, а утверждение 4.2b не выполняется на тракте 4.2(i), потому что ‘true безусловно не трактуется.}}
|
|---|
| (i) Утверждение 4.2a выполняется, но 4.2b нет |
assert always(a -> next[3] (‘false)); (4.2a) assert always(a -> next![3] (‘true)); (4.2b) |
Рис. 4.2: Слабый временной оператор податливый, даже при ‘false, а сильный временной оператор строгий, даже при ‘true
|
Ниже мы покажем семейства сильных операторов, в том же порядке, в котором в котором были представлены их слабые аналоги, а также контраст слабых и сильных версий.
4.1 Оператор next!
Утверждение 4.3а показывает, что когда бы a не утверждался, b должен утвердиться в следующем цикле. Используя сильную версию оператора next, мы получим утверждение 4.3b, которое дополнительно требует be a в следующем цикле. Например, пока утверждение 4.3а выполняется на тракте 4.3(i), утверждение 4.3b нет, потому что, даже хотя b утверждается после первых двух утверждений a, тракт заканчивается слишком быстро по отношению к третьему утверждению a.
|
|---|
| (i) Утверждение 4.3a выполняется, но 4.3b нет |
assert always (a -> next b); (4.3a) assert always (a -> next! b); (4.3b) |
| Рис. 4.3: слабый next против сильного next |
4.2 Вариации на next!, включая next_event!
Сильный оператор next_event! связан с его слабой версией next_event, также как сильный оператор next! связан со своей слабой версией next. Например, утверждение 4.4b не выполняется на тракте 4.4(i), потому что не хватает грантов. Однако, слабая версия, утверждения 4.4а, не выполняется на том же тракте. Оператор next![n] позволяет вам показать, что как минимум n следующих циклов необходимы, и оператор next_event!(b)[n] позволяет вам показать, что как минимум n вхождений в булево событие b необходимы.
|
|---|
| (i) Утверждение 4.4a выполняется, но 4.4b нет |
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)
|
Рис. 4.4: Слабый next_event против сильного next_event
|
Вы должны уже сейчас догадываться о значениях операторов next_a![i:j] и next_event_a!(b)[i:j]. Оператор next_a![i:j] выполняется, если существуют минимум j дополнительных циклов, и его операнд выполняется от i-го до j-ого включительно. Оператор next_event_a!(b)[i:j] выполняется, если существует минимум j дополнительных циклов, на которых выполняется b, и второй оператор выполняется на всех, от i-го до jth, циклах включительно.
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.
