PSL/A Practical Introduction to PSL/SERE Style
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Стиль SERE
До этого момента, мы видели свойства PSL, построенные на булевых выражениях и временных операторах в стиле LTL. Другой путь построения свойств использует SERE - Последовательные расширения регулярных выражений. SERE по-сути тоже самое, что и регулярные выражения, как те, которые используются для сопоставления во многих приложениях. Отличие лишь в том, что атом SERE - булево выражение, в то время, как атомы стандартного регулярного выражения - отдельные символы.
SERE обычно заключается в фигурные скобки, и атом SERE обычно разделен точкой с запятой. Например, {a;b;c} - это SERE, и SERE 5.1a - это более сложный SERE. SERE 5.1a описывает последовательность циклов, в которых утверждается (req_out && !ack) на первом цикле, далее (busy && !ack) утверждается нуль или более циклов, показанный последовательным оператором повторения [*], и в итоге утверждается ack. Таким образом, SERE 5.1a отмечает последовательность циклов, под лейблом “1” в тракте 5.1(i).
Не поддавайтесь искушению в трактовке SERE более, чем показано здесь: SERE 5.1a показывает последовательность циклов под лейблом “2” в тракте 5.1(i). SERE 5.1a не запрещает утверждения занятости в течение последнего цикла SERE. Если важно исключить такое поведение, занятость может быть явно указана, как показано в SERE 5.1b. SERE 5.1b показывает последовательность циклов под лейблом “1”, показанная на тракте 5.1(i), но не показывает последовательность циклов под лейблом “2” в этом же тракте.
Как использовать SERE? Во-первых, SERE может также быть под-свойством. Например, свойство 5.2a выполняется, если существует утверждение req_in && gnt, далее начиная со следующего цикла, мы видим последовательность циклов отмеченных SERE 5.1a. Свойство 5.2a выполняется на тракте 5.2(i).
Примечание: SERE - это свойство, но свойство это не всегда SERE. Таким образом, пока мы можем использовать SERE, как операнд временного оператора, мы не можем вставить временной оператор, такой как always или next, внутрь SERE.
Сейчас предположим, что у нас есть ситуация похожая на свойство 5.2a, но в которой грант (утверждение сигнала gnt) появляется циклом позже утверждения req_in. Мы можем попробовать заменить булево выражение req_in && gnt временным выражением req_in && next gnt, как в свойстве 5.3a. Однако, вспомним урок раздела 3.4: в свойстве 5.3a текущий цикл лева-ориентированной стороны (req_in && next gnt) тот же самый, что и текущий цикл право-ориентированной стороны (потому что они соединены булевым оператором ->). Таким образом, текущий цикл gnt (который является операндом оператора next) - это тот же текущий цикл для SERE (который также является операндом оператора next). Это немного запутанно, и действительно свойство 5.3а не принадлежит простому подмножеству PSL, которые мы обсуждали в главе 9.
Давайте модифицируем свойство 5.3а, как показано в свойстве 5.3b. Сейчас один оператор next применяется для обоих, gnt и SERE, которые являются операндами оператора ->. Свойство 5.3b эквивалентно свойству 5.3a, но оно из просто подмножества, делая более простым отслеживание временной выборки между gnt и SERE. Если мы подразумеваем, что текущий цикл SERE должен быть циклом позже gnt, мы можем манипулировать свойством 5.3b, добавляя next, как в свойстве 5.3c. Однако, суффиксная импликация операторов предоставляет более простой путь.
|
|---|
| (i) SERE 5.1a отмечает 1 и 2. SERE 5.1b отмечает 1, но не 2. |
{(req_out && !ack) ; (busy && !ack)[*] ; ack} (5.1a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack && !busy} (5.1b)
|
| Рис. 5.1: Два простых SEREs |
|
|---|
| (i) Свойство 5.2a выполняется |
always ((req_in && gnt) -> (5.2a)
next {(req_out && !ack) ; (busy && !ack)[*] ; ack})
|
| Рис. 5.2: SERE - свойство |
always ((req_in && next gnt) -> (5.3a)
next {(req_out && !ack) ; (busy && !ack)[*] ; ack})
always (req_in -> next (gnt -> (5.3b)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}))
always (req_in -> next (gnt -> (5.3c)
next {(req_out && !ack) ; (busy && !ack)[*] ; ack}))
|
| Рис. 5.3: Свойство 5.3a не из простого подмножества. Свойства 5.3b и 5.3c из простого подмножества, но они сложны для чтения. Эти свойства можно выразить проще, используя суффиксную импликацию. |
|---|
5.1 Суффиксная импликация (|-> и |=>)
Операторы суффиксной импликации (|-> и |=>) предоставляют возможность ссылаться на два SERE таким образом, что право-ориентированная сторона начинает работать, когда лева-сторонняя сторона заканчивает работы. Параллельный оператор суффиксной импликации (|->) интерпретирует “когда лева-ориентированная сторона заканчивает работать” также, как “в том же цикле, когда лева-ориентированная сторона заканчивает работать”, в то время как не параллельный оператор суффиксной импликации (|=>) интерпретирует это, как “цикл после цикла, в котором лева-ориентированная сторона завершила работу”. Таким образом, свойство 5.4а эквивалентно свойству 5.3b, и свойство 5.4b эквивалентно свойству 5.3c. Оба свойства 5.4a и 5.4b легче для понимания, чем эквивалентное свойство без суффиксной импликации , и оба принадлежат простому подмножеству из главы 9.
|
|---|
always {req_in;gnt} |-> (5.4a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
always {req_in;gnt} |=> (5.4b)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
|
| Рис. 5.4: Суффиксная импликация |
Напомним, что логический оператор импликации (->) может интерпретироваться, как if-then выражение, с безоговорочно утвержденной else-частью. Суффиксный оператор импликации (|-> and |=>) может восприниматься также. Разница между логическим оператором импликации (->) и суффиксным оператором импликации (|-> and |=>) во временных взаимоотношениях между if- и then-частями. В то время, как текущий цикл then-части для оператора логической импликации
(->) тот же, что и для if-части, текущий цикл then-части суффиксного оператора импликации (|-> or |=>) это первый цикл суффикса тракта, который остается после того, как сменяется if-часть. Это показано для свойств 5.4a и 5.4b в трактах 5.4(i) и 5.4(ii).
|
|---|
| (i) Тракт имеет множественные if-then пары. Свойство 5.5a выполняется. |
always {req_in;gnt} |=> (5.5a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
|
| Рис. 5.5: if-часть другой if-then пары может начаться перед тем, как if-часть или then-часть предыдущей if-then пары выполниться |
В трактах 5.4(i) и 5.4(ii) присутствует единичное утверждение сигнала req_in. Если бы здесь было множественные утверждения req_in, то, конечно же, мы должны были бы идентифицировать множественные if-then пары, как показано в тракте 5.5(i). Отметим, что if-часть другой if-then пары может начинаться, перед завершение выполнения if-части или then-части предыдущей if-then пары. Например, вторая if-then пара начинается в седьмом цикле, перед тем, как выполнится then-часть первой пары. Третья if-then прара начинается в цикле 8, перед тем как выполнятся then-часть первой пары и if-часть второй пары. Мы могли видеть такой вид перекрытия ранее, в трактах 2.2(ii) и 2.3(iii). Отметим, что в тракте 5.5(i) утверждение ack в цикле 16 завершает then-часть второй и третьей if-then пары. Для более глубокого объяснения этого феномена,смотрите раздел 13.4.2.
Свойства 5.6a и 5.6b выполняются в тракте 5.6(i), потому что не существует последовательности циклов согласованных с левой стороной, т.о. else-часть по-умолчанию утверждается в каждом цикле.
|
|---|
| (i) Свойства 5.6a и 5.6b выполняются |
always {req_in;gnt} |-> (5.6a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
always {req_in;gnt} |=> (5.6b)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
|
| Рис. 5.6: else-часть суффиксной импликации по-умолчанию утверждена |
5.2 Слабый и сильный SERE
Как и временные операторы, SERE могут быть слабыми и сильными, и как и временные операторы, сильные версии SERE обозначаются восклицательным знаком (!). Таким образом, свойство 5.7а, правая сторона которого - сильный SERE, выполняется только, если будет достигнут цикл, в котором встречается ack. Другими словами, слабая версия SERE позволяет нам принимать тракт, который является “слишком коротким”, в то время как сильная версия предполагает, что мы должны добраться до конца SERE. Таким образом, в то время как свойство 5.7a выполняется на тракте 5.7(i), также как и на тракте 5.7(ii), свойство 5.7b, сильная версия, выполняется в тракте 5.7(ii), но не в тракте 5.7(i).
|
|---|
always {req_in;gnt} |=> (5.7a)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}
always {req_in;gnt} |=> (5.7b)
{(req_out && !ack) ; (busy && !ack)[*] ; ack}!
|
| Рис. 5.7: Слабый SERE выполняется даже, если тракт “слишком короткий”, в то время как сильный SERE, должен “достигать конца” |
5.3 Оператор never применимый в SERE
Другой способ использования SERE состоит в описании событий, которые никогда не произойдут. Например, утверждение 5.8a показывает, что сигнал req не должен быть утвержден в двух последовательных циклах, и таким образом не выполняется в тракте 5.8(i).
Другой пример, рассмотрим утверждение 5.9a. Оно показывает, что признанный высоко приоритетный запрос (утверждение req вместе с high_pri, следует циклом позже ack) не может быть прерван (утверждение cancel циклом позже ack). Таким образом, оно выполняется на тракте 5.9(i), но не выполняется в тракте 5.9(ii).
|
|---|
| (i) Утверждение 5.8a не выполняется |
assert never {req;req}; (5.8a)
|
| Рис. 5.8: Оператор never |
|
|---|
| (i) Утверждение 5.8a не выполняется |
assert never {req && high_pri ; ack ; cancel}; (5.9a)
|
| Рис. 5.9: Еще об опрераторе never |
5.4 Операторы повторения SERE ([*n], [=n], и [->n])
До теперешнего момента, мы видели основу SERE состоящую из Булевых выражений, разделенных точкой с запятой. В данном разделе мы рассмотрим операторы SERE, которые позволяют вам построить более сложные SERE, используя вариации операторов повторения SERE [*n], [=n] и [->n].
Последовательные операторы повторения предоставляют возможность получения одинаковых под-SERE во времени. Оператор [*n] это аббревиатура для n повторений SERE. Например, вместо того, чтобы писать busy;busy;busy в утверждении 5.10a, мы можем использовать busy[*3], как в утверждении 5.10b. Утверждения 5.10a и 5.10b показывают, что после запроса (утверждения сигнала req), мы ожидаем увидеть предопределение (утверждение сигнала ack) с последующими тремя циклами, в которых утверждается сигнал busy, с последующим утверждением сигнал done. Тракт 5.10(i) пример тракта, в которых выполняются утверждения 5.10a и 5.10b.
|
|---|
assert always {req} |=> {ack;busy;busy;busy;done}; (5.10a)
assert always {req} |=> {ack ; busy[*3] ; done}; (5.10b)
assert always {req} |=> {ack ; busy[*3:5] ; done}; (5.10c)
|
Рис. 5.10: Операторы [*n] и [*i:j]
|
Вместо отдельного написания числа повторений, мы можем определить диапазон, от i до j, вот так: [*i:j]. Таким образом, утверждение 5.10c одинаково с утверждением 5.10b, но вместо точно требуемых трех утверждений сигнала busy, мы требуем между тех и пяти. Утверждение 5.10c выполняются в тракте 5.10(i), также как и в тракте 5.10(ii).
Верхняя граница диапазона может быть бесконечность, которая обозначается $ в SystemVerilog, null в GDL и inf в Verilog, VHDL и SystemC. Например, SERE {b[*5:inf]} предполагает пять или более повторений b.
Мы можем повторять не только Булевы выражения, но и SERE. Например, свойство 5.11а выполняется, если после предопределенного запроса (утверждение сигнала req последует утверждение сигнала ack), мы видим три передачи данных, с последующим утверждение сигнала d_end, где передача данных это утверждение сигнала start, с последующим утверждение сигнала busy, с полседующим утверждением сигнала done. Тракт 5.11(i) это пример тракта, в котором выполняется свойство 5.11a.
Если мы пропустим n, в результате SERE выберет произвольное число повторений Булевого выражения или SERE, которое повторялось. Например, утверждение свойства 5.11b показывает, что после предопределенного запроса, мы ожидаем увидеть некое число передач данных, сопровождаемых утверждением done. Свойство 5.11b выполняется на тракте 5.11(i), также как и трактах 5.11(ii) и 5.11(iii).
[*] предполагает любое количество повторений, в том числе и их отсутствие. Таким образом, свойство 5.11b выполняется на тракте 5.11(iv). Если мы хотим определить любое ненулевое число повторений, нужно использовать [+]. Таким образом, свойство 5.11c аналогично свойству 5.11b, но оно предполагает минимум одну передачу данных перед утверждением сигнала done. Таким образом, свойство 5.11с не выполняется на тракте 5.11(iv), но выполняется на трактах 5.11(i), 5.11(ii) и 5.11(iii).
Вместо того, чтобы опустить n, мы можем опустить Булево выражение или SERE и оставить повторение [*n] в одиночестве. Одинокий [*n] эквивалентен ‘true[*n]. Другими словами, [*n] определяет любые n циклов (потому что ‘true выполняется во всех циклах). Другой вариант восприятия этого, это понимание того, что таким образом мы можем “пропустить” n циклов. Таким образом, свойство 5.12a аналогично свойству Property 5.11b, но вместо подтверждения (утверждение сигнала ack), выполняющегося сразу после запроса (утверждения сигнала req), это происходит четырьмя циклами позже. Свойство 5.12a выполняется на тракте 5.12(i).
Непоследовательный оператор повторения ([=n]) предоставляет возможность описания повторений, которые происходят на непоследовательных циклах. Это может применять только для Булевых выражений. Например, для описания требования, что после запроса (утверждения сигнала req), мы ожидаем увидеть подтверждение (утверждение сигнала ack) в сопровождении некоторого количества циклов, включая три необязательно последовательных утверждения сигнала busy, в сопровождении утверждения сигнала done, утверждение 5.13a. Утверждение 5.13a выполняется на тракте Trace 5.13(i). Обратите внимания на циклы отмеченные “busy[=3]” в тракте 5.13(i). Они не начинаются с утверждением сигнала busy , при этом они не заканчиваются после одного. Непоследовательный оператор повторения [=n] определяет последовательность циклов, в которой n необязательно последовательное повторение Булевого выражения, включая последовательности циклов, в которых “padding” вначале и/или в конце. Другими словами, он определяет любую последовательность циклов, в которой число утверждений Булевого выражения повторится n раз.
Если вы хотите запретить заполнение в конце, используйте оператор повторения goto [->n]. Оператор повторения [->n] идентичен непоследовательному оператору повторения, за исключением того, что последовательность циклов будет описываться с утверждение Булевого выражения, которое должно повторяться, в конце. Другими словами, он показывает последовательность циклов, начиная с текущего цикла и заканчивая после вашего “go to” n-го вхождения в Булево выражение (использование -> предназначено для упоминания, что по стрелки вы переходите к инструкции n). Таким образом утверждение 5.13b не выполняется в тракте 5.13(i), но выполняется в тракте 5.13(ii), потому что третий busy сопровождается утверждением сигнала done.
n может быть опущен для оператора повторения goto, в этом случаи n по-умолчанию равняется 1. Другими словами, b[->] эквивалентно [->1].
Как и последовательные операторы повторения, непоследовательный оператор и оператор goto могут принимать диапазон. Таким образом, утверждение 5.14a требует три - пять не обязательных последовательных утверждений busy, после утверждения сигнала ack и перед утверждением done, в то время как утверждение 5.14b требует тоже самое, и в дополнение, то что утверждение сигнала done появляется, незамедлительно, после 3-го, 4-го или 5-го утверждения сигнала busy. Таким образом, утверждение 5.14a выполняется на трактах 5.14(i) и 5.14(ii), в то время как утверждение 5.14b выполняется на тракте 5.14(ii), но не на тракте 5.14(i).
5.5 Concatenation (;) and fusion (:)
We have already seen the concatenation operator, a semi-colon, which is used to join two SEREs (or two Boolean expressions, or a Boolean expression and a SERE) in such a way that the right-hand SERE starts the cycle after the left-hand SERE ends. The fusion operator, a colon, is used to join two SEREs (or two Boolean expressions, or a Boolean expression and a SERE) in such a way that there is a single cycle of overlap between them: the right-hand SERE starts the same cycle that the left-hand SERE ends.
For example, consider the case that we want to specify the behavior of As- sertion 5.14b, and in addition, following the assertion of signal done, we should see a data transfer, which consists of the assertion of signal data for some num- ber of cycles (might be zero), followed by an assertion of signal d end. Using the concatenation operator, we can write Assertion 5.15a. Trace 5.15(i) is a trace on which Assertion 5.15a holds. The first assertion of signal req gets three cycles of data before the assertion of d end, while the second assertion of signal req sees four cycles of data before seeing d end.
If the data transfer should start the same cycle as signal done is asserted, then we can use the fusion operator as in Assertion 5.16a. Trace 5.16(i) is an example of a trace on which Assertion 5.16a holds. It is similar to Trace 5.15(i), except that the data transfer starts the same cycle as that in which done is asserted, rather than the cycle following the assertion of signal done.
Note that while it may be tempting to understand the concatenation op- erator (;) as a delay, the operator does not necessarily “eat” a cycle. For in- stance, in the case of the SERE {a ; b[*] ; c}, the b[*] may match zero, one, or more cycles, as illustrated in Trace 5.17(i). The first match shown in Trace 5.17(i) is only two cycles long, thus, the second concatenation operator (;) did not “eat” a delay. A better way to think of it is that concatenation gives you an ordered list of things to happen – some of them may consume one cycle, some more, and some no cycles at all.
Further note that fusion requires an overlap of at least one cycle. Thus, while the {b[*]} in {b[*] ; c} may match an empty sequence of cycles, replacing the concatenation operator with the fusion operator like this: {b[*]: c} results in a SERE with at least one assertion of b (otherwise there is nothing to overlap with the assertion of c). In both cases, the match may consist of a single cycle. The difference is that in the case of {b[*] ; c} the single cycle may not include an assertion of b (because there may be zero assertions of b preceding c), while in the case of {b[*] : c}, the single cycle must include an assertion of b (which overlaps with the assertion of c).
5.6 Compound SEREs
Compound SEREs are SEREs built from other SEREs through operations other than concatenation and fusion. The available operators allow you to “and” or “or” together two or more SEREs, as well as to express the situation where a match of one SERE occurs within a sequence of cycles matched by another.
Consider the case that we want to say that signal read complete is as- serted on the last data cycle of every read operation, where we have two kinds of read operations: a short read consists of an assertion of signal short rd fol- lowed by eight not necessarily consecutive assertions of data, and a long read consists of an assertion of signal long rd followed by 32 such assertions. We could code two separate properties, as shown in Properties 5.18a and 5.18b. Alternatively, we could use the SERE “or” operator (|) to “or” the two SEREs together, as in Property 5.18c.
The SERE “and” operator comes in two types: length-matching and non- length-matching. Both the length-matching (&&) and the non-length-matching (&) “and” operators match a sequence of cycles if starting at the current cycle, the left-hand side and the right-hand side are matched. The difference is that in addition, the length-matching “and” operator requires that the lengths of the sequences matched by both the left- and right-hand sides are the same, while the non-length-matching operator matches even if they are different. A length-matching “and” between SEREs R and S is illustrated in Trace 5.19(i), and a non-length-matching “and” between SEREs R and S is illustrated in Traces 5.20(i), 5.20(ii) and 5.20(iii).
When a non-length-matching “and” is used on the left-hand side of a con- catenation or a fusion, the current cycle of the right-hand side of the concate- nation or fusion is determined by the longer of the two subsequences making up the non-length-matching “and”. For instance, in the SERE {{{a;b[*5];c} & {d[*];e}} ; f}, the current cycle of f is the cycle after the cycle in which the longer of the two SEREs {a;b[*5];c} and {d[*];e} completes. This is illustrated in Traces 5.21(i) and 5.21(ii). Note that in each of the traces, sig- nal f is asserted twice: once after the completion of {a;b[*5];c}, and once after the completion of {d[*];e}. However, in each trace, only the assertion of signal f that happens after the completion of the longer of the two SEREs participates in the “match” of SERE {{{a;b[*5];c} & {d[*];e}} ; f}.
NOTE: A length-matching “and” such as {a;b;c} && {d} is legal, but makes no sense (because there is no sequence which is both 3 cycles long to match {a;b;c} and 1 cycle long to match {d}). Many tools will probably issue a warning for such a SERE.
As an example of the use of the length-matching “and”, consider the case that a read request (assertion of signal read req) that is granted (assertion of signal gnt within 5 cycles of the request) should be followed by a data transfer (assertion of signal data start followed by some number of consecutive as- sertions of data, followed by an assertion of data end), unless it is canceled. A cancel is an assertion of signal cancel any time between the assertion of read req and the assertion of gnt, inclusive. We can express this using As- sertion 5.22a. Assertion 5.22a holds on Trace 5.22(i): the first read request is followed by a data transfer, while the second read request is not followed by a data transfer, but is not required to be since it is canceled.
In the case of Assertion 5.22a, we needed the length-matching “and”. To see why, consider what would have happened had we used the non- length-matching “and” as in Assertion 5.22b. In the case of Assertion 5.22b, the left-hand side SERE {{read req ; [*0:4] ; gnt} & {cancel[=0]}} is matched not only by the sequence of cycles starting at cycle 2 and ending at cycle 5, but also by the sequences of cycles starting at cycle 2 and ending at any of the cycles 6 through 16. Thus, Assertion 5.22b requires that we see a data transfer starting not only at cycle 6, but also at cycles 7, 8, 9, 10 and so on. Obviously, this is not what we wanted.
As an example where we want the non-length-matching “and” rather than the length-matching “and”, consider the case that signal global print req indicates that we should see a print on each of printers 1, 2, and 3 (comple- tion of which is indicated by assertions of p1 done, p2 done, and p3 done, respectively), and that following completion of the last print job, we should see an assertion of signal print success. We can express this as shown in Assertion 5.23a. Assertion 5.23a holds on Trace 5.23(i) because following the assertion of signal global print req, we see assertions of each of the signals p1 done, p2 done and p3 done, the last of which is followed by an assertion of print success.
The non-length-matching “and” was needed for Assertion 5.23a. To see why, consider what would have happened if we had used the length-matching “and”, as in Assertion 5.23b. Assertion 5.23b does not hold on Trace 5.23(i) because the use of the length-matching “and” means that p1 done[->], p2 done[->] and p3 done[->] must all have the same length, i.e., that p1 done, p2 done and p3 done must all be asserted at the same time.
The SERE within operator is useful if you want to describe a situation where one SERE occurs within the time frame of another. For instance, sup- pose that the normal behavior of the design is to complete a high priority request first, even if there is a pending low priority request that started be- fore it. However, if signal no nesting is asserted when the low priority re- quest is issued, then this is prohibited. In other words, the situation shown in Trace 5.24(i) is not allowed. We can describe the prohibited situation as shown in Assertion 5.24a. Assertion 5.24a does not hold on Trace 5.24(i) because there is a match of {high pri begin ; high pri end[->]} that is entirely enclosed within the match of {(low pri begin && no nesting) ; low pri end[->]}.
NOTE: If the left and right operands of a within operator are s and t respectively, then the within operator is simply a shorthand for a length- matching “and” between {[*] ; s ; [*]} and {t}. That is, s within t is equivalent to {[*] ; s ; [*]} && {t}.
5.7 More about suffix implication
Up until now, we have seen the suffix implication operators (|-> and |=>) used with SEREs on both the left- and the right-hand sides. While the left- hand side of a suffix implication operator must be a SERE, the right-hand side of a suffix implication operator can be any property. Thus, if we want to express the requirement that whenever we have a request that is acknowledged (assertion of req followed by an assertion of ack) we should see a grant (assertion of signal gnt within three cycles of the acknowledge), we can code as in Assertion 5.25a.
This is illustrated in Trace 5.25(i). In the trace, there are three occurrences of the SERE {req;ack}. The first is followed by an assertion of ack after two cycles, the second after three cycles, and the third after a single cycle. Thus, Assertion 5.25a holds on the trace.
Of course, we could have written Assertion 5.25a entirely in SERE style, as shown in Assertion 5.25b, or entirely without SEREs, as in Assertion 5.25c. Assertions 5.25a, 5.25b and 5.25c are equivalent, thus the issue is purely one of style. Some people prefer using only one style, others find a mix of styles, depending on the particular property, to be easier to understand.
5.8 The built-in function ended()
The built-in function ended() takes a SERE as an argument and returns true in any cycle where that SERE has just ended.1 For example, Trace 5.26(i) has been annotated with a waveform labeled ended({a ; b[*] ; c}) to show the value of the call to ended() at each cycle.
1 - In previous versions of PSL, the role of the built-in function ended() was played by endpoints. Endpoints are no longer a part of the language – use built-in function ended() instead.
How is ended() used? Consider that a complete data transfer consists of an assertion of signal data start followed by some number of assertions of data, followed by an assertion of data end. Consider further that we have a signal data transfer complete that should be asserted when a data trans- fer is completed, and that we would like to specify the correct behavior of this signal. A good start would be Assertion 5.27a. Assertion 5.27a ensures that data transfer complete is asserted at the conclusion of every data transfer. But what about the other direction? That is, what about ensuring that whenever data transfer complete is asserted, a complete data trans- fer has indeed concluded? Assertion 5.27a does not ensure this, and thus it holds on Trace 5.27(i), even though there are “extraneous” assertions of data transfer complete at cycles 6 and 15. We would like an assertion that holds on Trace 5.27(ii) but not on 5.27(i).
In order to check the second direction (that there are no extraneous asser- tions of data transfer complete) we need to switch the direction of the implication: we need to say that if data transfer complete is asserted, then we have just seen the conclusion of a complete data transfer. We could try Assertion 5.27b. However, that doesn’t work. Assertion 5.27b requires that the SERE {data start ; data[*] ; data end} start the same cycle as data transfer complete, while we want it to end that cycle.
This is where the built-in function ended() comes in. Using ended(), we can code what we want as shown in Assertion 5.27c, which states that whenever we see an assertion of data transfer complete, we must have just seen the end of SERE {data start ; data[*] ; data end}, and it does not hold on Trace 5.27(i).
Note that ended() returns a Boolean value. Since the left-hand side of the suffix implication in Assertion 5.27c consists of a single Boolean expression, we could have coded Assertion 5.27c equivalently using logical implication as shown in Assertion 5.27d.
5.9 Overlapping matches of a SERE
Up until now, we have been concentrating on explaining the meaning of each SERE operator, using relatively simple examples. It is now time to introduce some more complex examples, in order to emphasize that like LTL style prop- erties, interpreting a SERE style property on a trace can involve examining overlapping sets of cycles.
Consider Property 5.28a on Traces 5.28(i) and 5.28(ii). There are multiple matches of {a ; b[*] ; c} on Trace 5.28(i), one match ending at cycle 2, one ending at cycle 3, and one ending at cycle 4. Property 5.28a does not hold on Trace 5.28(i), because the matches ending at cycles 2 and 3 do not have associated assertions of signal d at cycles 3 and 4. A suffix implication requires that for every match of the left-hand side, the right-hand side holds. Property 5.28a does hold on Trace 5.28(ii), because signal d is asserted after each match of {a ; b[*] ; c}.
Note that although Property 5.28a contains an always operator, the always operator is not the source of the overlapping matches in this case. Rather, for a single current cycle (cycle 1), there are three separate matches of the SERE {a ; b[*] ; c}, each ending at a different cycle.
The overlapping can happen on the right-hand side of a suffix implication as well. Consider for example Property 5.29a on Trace 5.29(i). There are three matches of {d ; e[*] ; f}, ending at cycles 3, 4, and 5. One match would have been enough to satisfy Property 5.29a, because as long as there exists one match, {d ; e[*] ; f} holds. The fact that there are in fact three matches does not hurt. Thus, Property 5.29a holds on Trace 5.29(i).
We have just explained that we require at least one match of the right-hand side for every match of the left-hand side of a suffix implication, and it might seem that in so doing, we have introduced something new. Actually, the rule could have been deduced from the parallel we have previously drawn between a suffix implication and an if-then statement. SERE {a ; b[*] ; c} can be understood as an infinite “or” between SEREs {a;c}, {a;b;c}, {a;b;b;c}, and so on. So Property 5.28a can be understood as “if {a;c} or {a;b;c} or {a;b;b;c} or ..., then d”, which clearly should hold only if we see a d every time the if-part is matched. And Property 5.29a can be understood as “if c, then {d;f} or {d;e;f} or {d;e;e;f} or ...”, which of course should hold as long as we have seen at least a single match of the then-part.
5.10 How not to use SEREs
