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, циклах включительно.
Оператор next_e![i:j] создает свойство, которое выполняется, если его операнд выполняется, как минимум, на одном цикле начиная с i-го заканчивая j-ым, включительно. Необязательно должно быть j циклов, если операнд выполняется на некотором цикле между i-ым и j-ым. Аналогично, оператор next_event_e!(b)[i:j] создает свойство, которое выполняется, если его второй операнд выполняется, как минимум, на одном вхождении в b, начиная от i-го и заканчивая j-ым. Например, рассмотрим утверждение 4.5b, которое показывает, что запрос (утверждение req) должно быть предопределено (утверждение assertion of ack) на одном из следующих четырех грантах, и в дополнение, тракт не должен заканчиваться до того, как не появится соответствующий грант. Утверждение 4.5b не выполняется на тракте 4.5(i), потому что ни одни из трех показанных грантов не предопределен. Тот факт, что четвертый грант отсутствует неважен, не существует вариантов для четвертого гранта, которые могут изменить наше представление об предопределенности первого, второго и третьего грантов.
Слабая версия утверждения 4.5b выполняется на двух трактах 4.5(i) и Trace 4.5(ii). Существует только один вариант повлиять над слабой версией, показанной в утверждении 4.5a - если бы были четыре гранта, и не один из не был предопределен.
|
|---|
assert always (req -> next_event_e(gnt)[1:4](ack)); (4.5a) assert always (req -> next_event_e!(gnt)[1:4](ack)); (4.5b) |
Рис. 4.5: Слабый next_event_e[i:j] против сильного 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.
