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

Слабые временные операторы против сильных временных операторов

Временные операторы могут быть слабыми или сильными. Сильны временной оператор, такой как eventually! показан восклицательным знаком, как частью своего имени. Оператор без восклицательного , такой как next, слабый. До этого времени мы видели только по одной версии каждого оператора, но много операторов, которых мы видели до того, могут иметь слабую и сильную версии. Различие между слабыми и сильными операторами очень важны, когда путь “слишком короткий”, чтобы определить, действительно все ли произошло для удовлетворения свойства. ¹ Например, рассматривая спецификацию “каждое утверждения сигнала 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^-го до j^th, циклах включительно.

Оператор 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 Операторы until и until!

Ранее мы видели утверждения подобные утверждению 4.6a, который показывает, что когда бы не утверждался a, далее, начиная со следующего цикла, b должен утвердиться до утверждения c. Например, утверждения 4.6a выполняется в тракте 4.6(i). Но, что касается тракта, подробного Trace 4.6(ii), где c никогда не появляется? Выполняется утверждение 4.6a на тракте 4.6(ii) или нет? Оно выполняется. Суть в том, что оператор until - слабый оператор.

Если мы хотим выразить требования утверждения 4.6a, но в дополнение присутствует c, мы должны использовать сильный оператор. Утверждение 4.6b, которое использует сильный оператор, не выполняется в тракте 4.6(ii).

Оператор until!_ сильная версия оператора until_. Оператор until!_ выполняется только, если его левый операнд остается утвержденным до конца, включая цикл, где его правый операнд утвержден, и в дополнение его правый операнд выполняется в конечном итоге.

assert always(a -> next (b until c)); (4.6a) assert always(a -> next (b until! c)); (4.6b)
Fig. 4.6: Сильный until против слабого until

4.4 операторы before! и before!_

Акцент, сильной версии оператора before, заключается в его лева-направленности операндов. Например, утверждения 4.7a показывает, что следуя утверждению req, утверждения gnt необходимо, чтобы req утверждался до этого, но будучи слабым выполняется не только в тракте 4.7(ii), но также на тракте 4.7(i), в котором после второго запроса ни грант, ни третий запрос не появляются. Сильная версия, показанная в утверждение 4.7b, требует появления гранта, но не обязательно, что был другой запрос. Таким образом, утверждения 4.7b не выполняется на тракте 4.7(i), но выполняется на 4.7(ii).

assert always (req -> next (gnt before req)); (4.7a) assert always (req -> next (gnt before! req)); (4.7b)
Fig. 4.7: Слабый before против сильного before

Оператор before!_ сильная версия оператора before_. Таким образом, утверждение 4.8a выполняется на тракте 4.8(i), в котором первый запрос (утверждение сигнала req) предоставляется (утверждением сигнала gnt), но не второй. Сильная версия утверждения 4.8a, показанная в утверждении 4.8b, не выполняется на тракте Trace 4.8(i), потому что второй запрос не предоставляется. Оба утверждения 4.8а и 4.8b выполняются на тракте 4.8(ii).

assert always (req -> next (gnt before_ req)); (4.8a) assert always (req -> next (gnt before!_ req)); (4.8b)
Fig. 4.8: Слабый before_ против сильного before_

4.5 Операторы без слабых или сильных версий

Мы видели слабые и сильные версии многих операторов. Оператор eventually! не является сильной версий какого-либо оператора. Другими словами, не существует слабой версии eventually!. Смысл в том, что значение другого сильного оператора может быть широко описано, как требование того, чтобы ничего непредвиденного не должно случиться пока не появится условие прекращения, и в дополнении, в конечном счете условие окончание должно выполниться. Слабая версия далее отказывает требованию, что условие окончание выполнено, оставляя только требование, что ничего не предвиденного не произошло. Оператор eventually!, однако, не содержит идею “чего-либо” непредвиденного, только условия окончания. Более того, не существует вариантов ослабления оператора, без освобождения его значения.

Так как нету слабой версии оператора eventually!, нету сильной версии операторов always и never, для противоположного смысла. В случаи always и never, не существует условия окончания.