«…Труд избавляет человека от трех великих зол: скуки, порока, нужды…»

PSL/A Practical Introduction to PSL/Basic Temporal Properties/ru — различия между версиями

Материал из Wiki
Перейти к: навигация, поиск
(→‎Basic Temporal Properties While)
м (→‎Основные временные свойства While)
 
(не показаны 12 промежуточных версий 2 участников)
Строка 1: Строка 1:
 
{{PSL TOC}}
 
{{PSL TOC}}
−
==Основные временные свойства While==
+
==Основные временные свойства ==
  
 
<!--
 
<!--
Строка 23: Строка 23:
 
transfers we expect to see a tag of <code>i</code>”.
 
transfers we expect to see a tag of <code>i</code>”.
 
-->
 
-->
−
Комбинированием временных операторов различными путями, мы можем установить свойства, такие как “каждый запрос получает подтверждение”, “каждому одтвержденному запросу предоставляется от четырех до семи циклов, в случаи, если запрос не приостановится первым”,  
+
Комбинированием временных операторов различными путями, мы можем установить свойства, такие как “каждый запрос получает подтверждение”, “каждому подтвержденному запросу предоставляется от четырех до семи циклов, в случаи, если запрос не приостановится первым”, “две последовательные записи не должны располагать по одному и тому же адресу” и “когда мы видим запрос на чтение с тэгом i, на следующих четырех передах данных ожидается увидеть тэг <code>i</code>”.
  
 +
<!--
 
The temporal layer is composed of the Foundation Language (FL) and the
 
The temporal layer is composed of the Foundation Language (FL) and the
 
Optional Branching Extension (OBE). The FL is used to express properties
 
Optional Branching Extension (OBE). The FL is used to express properties
Строка 31: Строка 32:
 
“there exists a trace such that ...”, and is used in formal verification. In this
 
“there exists a trace such that ...”, and is used in formal verification. In this
 
book we concentrate on the Foundation Language.
 
book we concentrate on the Foundation Language.
 +
-->
 +
Временной слой состоит из фундаментального языка (FL) и дополнительного расширения ветвления (OBE). FL используется для выражения свойств одного тракта, а также используется для моделирования или формальной верификации. OBE используется для выражения свойств, относящихся к набору трактов, например, “существует тракт, такой как ...”, и также используется для формальной верификации. В этой книге мы сконцентрируемся на фундаментальном языке.   
  
 +
<!--
 
The Foundation Language itself is composed of two complementary styles
 
The Foundation Language itself is composed of two complementary styles
 
– LTL style, named after the temporal logic LTL on which PSL is based, and
 
– LTL style, named after the temporal logic LTL on which PSL is based, and
Строка 38: Строка 42:
 
We provide only a taste – enough to get the basic idea and to give some
 
We provide only a taste – enough to get the basic idea and to give some
 
context to the philosophical issues that we discuss next.
 
context to the philosophical issues that we discuss next.
 +
-->
 +
Фундаментальный язык состоит из двух комплементарных стилей - LTL стиль, названный из-за временной логики LTL, на которой базируется PSL, и SERE стиля, названного из-за последовательного расширения регулярных выражений PSL, или SEREs. В этой главе мы представим основные временные операторы LTL стиля. Мы предоставим то, что будет достаточно для понимания основной идеи, и чтобы дать некий контекст, для философских замечаний,обсуждаемых далее.
  
 +
<!--
 
Throughout this book, we make extensive use of examples. Each example
 
Throughout this book, we make extensive use of examples. Each example
 
property or assertion and its associated timing diagram (which we term a
 
property or assertion and its associated timing diagram (which we term a
Строка 46: Строка 53:
 
number. For instance, Figure 2.1 contains Trace 2.1(i) and Assertions 2.1a,
 
number. For instance, Figure 2.1 contains Trace 2.1(i) and Assertions 2.1a,
 
2.1b, and 2.1c.
 
2.1b, and 2.1c.
 +
-->
 +
В этой книге, мы широко используем примеры. Каждый пример свойства или утверждения связан с временной диаграммой (которую мы называем ''тракт'') сгруппирован вместе на рисунке. Такой рисунок будет содержать один или более трактов, нумерованных в скобках строчными римскими цифрами, одного или более свойств, нумерованных добавление строчной буквы к номеру рисунка. Например, Рисунок 2.1 содержит тракт 2.1(i) и утверждения 2.1а, 2.1b, 2.1c.   
 +
 +
===2.1 Операторы <code>always</code> и <code>never</code> ===
 +
 +
<!--
 +
We have already seen the basic temporal operators <code>always</code> and <code>never</code>. Most
 +
PSL properties will start with one or the other. This is because a “bare”
 +
(Boolean) PSL property refers only to the first cycle of a trace. For example,
 +
Assertion 2.1a requires only that the Boolean expression <code>!(a && b)</code> hold at
 +
the first cycle. Thus, Assertion 2.1a holds on Trace 2.1(i) because the Boolean
 +
expression <code>!(a && b)</code> holds at cycle 0. In order to state that we want it to
 +
hold at every cycle of the design, we must add the temporal operator <code>always</code>
 +
to get Assertion 2.1b. Assertion 2.1b does not hold on Trace 2.1(i) because
 +
the Boolean expression <code>!(a && b)</code> does not hold at cycle 5. Equivalently, we
 +
could have swapped the <code>always</code> operator and the Boolean negation <code>!</code> with
 +
<code>never</code>, to get Assertion 2.1c.
 +
-->
 +
Нам уже встречались основные временные операторы <code>always</code> и <code>never</code>. Большинство свойств PSL начинаются с одного или с другого. Это, потому что “голое” (Булево) PSL свойство относится только к первому циклу тракта. Например, утверждение 2.1a требует только того, чтобы Булево выражение <code>!(a && b)</code> выполнялось в первом цикле. Таким образом, утверждение 2.1а выполняется в тракте 2.1(i), потому что Булево выражение <code>!(a && b)</code> выполняется в цикле 0. Для того, чтобы сформулировать, что мы хотим, чтобы оно выполнялось в каждом цикле проекта, мы должны добавить временной оператор <code>always</code>, и получить утверждение 2.1b. Утверждение 2.1b не поддерживает тракт 2.1(i), потому что Булево выражение <code>!(a && b)</code> не выполняется в цикле 5. Эквивалентно, мы можем поменять оператор <code>always</code> и Булево отрицание <code>!</code> с <code>never</code>, чтобы получить утверждение 2.1с. 
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.1.png]]
 +
|-
 +
!(i) Утверждение 2.1a выполняется, но 2.1b and 2.1c нет
 +
|-
 +
|<pre>
 +
assert !(a && b);              (2.1a)
 +
assert always !(a && b);      (2.1b)
 +
assert never (a && b);        (2.1c)
 +
</pre>
 +
|-
 +
! Рис. 2.1: Операторы always и never
 +
|}
 +
 +
<!--
 +
Both Assertion 2.1b and Assertion 2.1c state that signals a and b are
 +
mutually exclusive. Obviously, anything that can be stated with the <code>always</code>
 +
operator can be stated with the never operator and vice versa, simply by
 +
negating the operand when switching between <code>always</code> and <code>never</code>. PSL provides
 +
both operators for convenience, as sometimes it is more natural to state
 +
the property in the positive (that is, stating what must hold at all cycles)
 +
and sometimes in the negative (that is, what must not hold for any cycle). In
 +
general, there are many ways to state any property in PSL. We will see other
 +
examples throughout the rest of this book.
 +
-->
 +
Оба утверждения 2.1b и 2.1c показывают, что сигналы a и b взаимоисключающиеся. Очевидно, все, что может использоваться с оператором <code>always</code>, может также использоваться с оператором <code>never</code> и наоборот, происходит простое отрицанием операнда, когда происходит переключение между <code>always</code> и <code>never</code>. PSL, для удобства, предоставляет два варианта использования, иногда более удобно описать свойство положительным (если свойство выполняется на всех циклах), а иногда удобней отрицательным (если свойство не выполняется ни в каком цикле). В общем, существует много путей описания свойств в PSL. Мы рассмотрим другие примеры далее.
 +
 +
===2.2 Оператор <code>next</code> ===
 +
 +
<!--
 +
Another temporal operator is the next operator. It indicates that the property
 +
will hold if its operand holds at the next cycle. For instance, Assertion 2.2a
 +
states that whenever a holds, then b should hold in the next cycle. Assertion
 +
2.2a uses another important operator, the logical implication operator
 +
(<code>-></code>). While the logical implication operator is a Boolean and not a temporal
 +
operator (it does not link two sub-properties over time), it plays a very important
 +
role in many temporal properties. A logical implication <code>prop1 -> prop2</code>
 +
holds if either prop1 does not hold or <code>prop2</code> holds. A good way to think of it
 +
is like an if-then expression, with the else-part being implicitly true. That is,
 +
<code>prop1 -> prop2</code> can be understood as “if prop1 then prop2 else true”. Thus,
 +
the sub-property <code>a -> next b</code> in our example holds if either a does not hold
 +
(because then the property defaults to true) or if a holds and also next b
 +
holds. By adding an always operator, we get a property that holds if the
 +
sub-property <code>a -> next b</code> holds at every cycle. Thus, Assertion 2.2a states
 +
that whenever <code>a</code> holds, <code>a</code> must hold at the next cycle. Assertion 2.2a holds on
 +
Trace 2.2(i) because every assertion of signal <code>a</code> is followed by an assertion of
 +
signal <code>b</code>. This is shown in the “if” and “then” annotations on Trace 2.2(ii).
 +
The “additional” assertions of signal <code>b</code> at cycles 1 and 10 are allowed by Assertion
 +
2.2a, because it says nothing about the value of b in cycles other than
 +
those following an assertion of <code>a</code>.
 +
-->
 +
Другой временной оператор - это оператор <code>next</code>. Он показывает, что свойство свойство должно выполняться, если его операнд выполняется в следующем цикле. Например, утверждение 2.2a показывает, что когда бы a не выполнялось, b должно выполниться в следующем цикле. Утверждение 2.2a использует другой важный оператор, логический оператор импликации (<code>-></code>). В то время как оператор логической импликации Булевый, а не временной (он не свяжет два подсвойства по времени), это играет очень важную роль во многих временных свойствах. Логическая импликация <code>prop1 -> prop2</code> выполняется, если prop1 не выполняется или prop2 выполняется. Это хорошо представляется, если принять это, как выражение вида if-then, с частью else. <code>prop1 -> prop2</code> можно понимать, как если prop1, то далее следует prop2, иначе возвращается значение правда. Таким образом, под-свойство <code>a -> next b</code>, в нашем примере, выполняется, если a не выполняется (потому что свойство по умолчание имеет значение правда) или, если a выполняется, а также и next b выполняется. Добавляя оператор always, мы получаем свойство, которое выполняется, если под-свойство <code>a -> next b</code> выполняется в каждом цикле. Таким образом, утверждение 2.2а показывает, что когда бы ни выполнялось <code>a</code>, <code>b</code> должно выполняться в следующем цикле. Утверждение 2.2а выполняется по сигналу <code>b</code>. Это показано в “if” и “then” примечании на тракте 2.2(ii). “Дополнительные” утверждения сигнала <code>b</code> на циклах 1 и 10, спровоцированы утверждение 2.2а, потому что в нем ничего не сказано о значениях b в цикле, кроме того, что следует из из утверждения <code>a</code>.             
 +
 +
<!--
 +
Note that the cycles involved in satisfying one assertion of signal a may
 +
overlap with those involved in satisfying another assertion. For example, consider
 +
Trace 2.2(iii), which is simply Trace 2.2(ii) with the if-then pairs numbered.
 +
There are four assertions of signal <code>a</code> on Trace 2.2(iii), and thus four
 +
associated cycles in which <code>b</code> must be asserted. Each pair of cycles (an assertion
 +
of <code>a</code> followed by an assertion of <code>b</code>) is numbered in Trace 2.2(iii). Consider
 +
pairs 2 and 3. Signal a is asserted at cycle 4 in pair 2, thus signal b needs to
 +
be asserted at cycle 5 in order for Assertion 2.2a to hold. Signal a is asserted
 +
at cycle 5 in pair 3, thus requiring that signal <code>b</code> be asserted at cycle 6. Pairs
 +
2 and 3 overlap, because while we are looking for an assertion of signal <code>b</code> at
 +
cycle 5 in order to satisfy the assertion of <code>a</code> at cycle 4, we see an additional
 +
assertion of signal <code>a</code> that must be considered.
 +
-->
 +
Отметим, что циклы вовлеченные в выполнение одного утверждения сигнала, могут перекрываться с теми,которые вовлечены в выполнение другого утверждения. Например, учитывая тракт 2.2(iii), который является простым трактом 2.2(ii) с if-then пронумерованными парами. Имеем четыре утверждения сигнала <code>a</code> на тракте 2.2(iii), и таким образом четыре связанных цикла, в которых <code>b</code> должен утверждаться. Каждая пара циклов (утверждение <code>a</code> следует из утверждения <code>b</code>) нумерованы в тракте 2.2(iii). Рассматривая пары 2 и 3. Сигнал a утверждается в 4 цикле пары 2, таким образом сигнал b должен утвердиться в 5 цикле, для того, чтобы утверждение 2.2а выполнялось. Сигнал а утверждается в цикле 5 пары 3, таким образом требуется утверждение сигнала b в 6 цикле. Пары 2 и 3 перекрываются, потому что, в то время как мы ищем утверждение сигнала <code>b</code> в 5 цикле, для выполнения утверждения <code>a</code> в 4 цикле, также, мы видим дополнительное утверждение сигнала <code>a</code>, который рассматривается.   
 +
 +
<!--
 +
Assertion 2.2a does not hold on Trace 2.2(iv) because the third assertion
 +
of signal <code>a</code>, at cycle 5, is missing an assertion of signal <code>b</code> at the following cycle.
 +
-->
 +
Утверждение 2.2а не выполняется в тракте 2.2(iv), потому что третье утверждение сигнала <code>a</code>, в цикле 5, т.к. отсутствует утверждение сигнала <code>b</code> в следующем цикле.   
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.2.png]]
 +
|-
 +
|<pre>
 +
assert always (a -> next b);        (2.2a)
 +
</pre>
 +
|-
 +
! Рис.2.2: Операторы next и логическая импликация
 +
|}
 +
 +
=== 2.3 вариации <code>next</code>, включая <code>next_event</code> ===
 +
 +
<!--
 +
A <code>next</code> property holds if its operand holds in the next cycle. Variations on the
 +
<code>next</code> operator allow you to specify the ''n<sup>th</sup>'' next cycle, and ranges of future
 +
cycles. A <code>next[n]</code> property holds if its operand holds in the ''n<sup>th</sup>'' next cycle.
 +
For example, Assertion 2.3a states that whenever signal <code>a</code> holds, signal <code>b</code> holds
 +
three cycles later. Assertion 2.3a holds on Traces 2.3(i), 2.3(iii), and 2.3(iv),
 +
while it does not hold on Traces 2.3(ii) or 2.3(v) because of a missing assertion
 +
of signal <code>b</code> at cycle 7, and does not hold on Trace 2.3(vi) because of <code>a</code> missing
 +
assertion of signal <code>b</code> at cycle 5.
 +
-->
 +
Свойство <code>next</code> выполняется, если его операнд выполняется в следующем цикле. Вариации оператора <code>next</code> позволяют указывать ''n<sup>-й</sup>'' следующий цикл и диапазоны будущих циклов. Свойство <code>next[n]</code> выполняется, если его операнд выполняется в ''n<sup>-й</sup>'' следующий цикл. Например, утверждение 2.3а показывает, что когда бы сигнал <code>a</code> не выполнялся, сигнал <code>b</code> выполниться тремя циклами позже. Утверждение 2.3а выполняется в тактах 2.3(i), 2.3(iii), 2.3(iv), но не выполняется в трактах 2.3(ii) или 2.3(v), потому что отсутствует утверждение сигнала <code>b</code> в цикле 7, и не выполняется в тракте 2.3(vi), потому что отсутствует утверждение сигнала <code>b</code> в цикле 5.
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.3.png]]
 +
|-
 +
!
 +
|-
 +
|<pre>
 +
assert always (a -> next[3] (b)); (2.3a)
 +
assert always (a -> next_a[3:5] (b)); (2.3b)
 +
assert always (a -> next_e[3:5] (b)); (2.3c)
 +
</pre>
 +
|-
 +
! Рис. 2.3: Операторы <code>next[n]</code>, <code>next_a[i:j]</code> и <code>next_e[i:j]</code>
 +
|}
 +
 +
<!--
 +
A next_a[i:j] property holds if its operand holds in ''all'' of the cycles from
 +
the ''i<sup>th</sup>'' next cycle through the ''j<sup>th</sup>'' next cycle, inclusive. For example, Assertion
 +
2.3b states that whenever signal a holds, signal b holds three, four and
 +
five cycles later. It holds on Trace 2.3(iii) and does not hold on Traces 2.3(i),
 +
2.3(ii), 2.3(iv), 2.3(v), or 2.3(vi).
 +
-->
 +
Свойство next_a[i:j] выполняется если его операнд выполняется во ''всех'' циклах от ''i<sup>-го</sup>'' следующего, до ''j<sup>-го</sup>'' следующего цикла включительно. Например, утверждение 2.3b показывает, что когда бы сигнал a не выполнялся, сигнал b выполняется тремя, четырьмя, пятью циклами позже. Выполняется в тракте 2.3(iii) и не выполняется в трактах 2.3(i),
 +
2.3(ii), 2.3(iv), 2.3(v) или 2.3(vi).
 +
 +
<!--
 +
Previously we discussed the fact that the cycles involved in satisfying one
 +
assertion of signal a may overlap those involved in satisfying another assertion
 +
of a. Trace 2.3(iii) has been annotated to emphasize this point for Assertion
 +
2.3b. Signal <code>b</code> must be asserted in cycles 5 through 7 (marked as “1”)
 +
because of the assertion of a at cycle 2, and must be asserted in cycles 7
 +
through 9 (marked as “2”) because of the assertion of a at cycle 4.
 +
-->
 +
Ранее мы обсуждали то факт, что циклы, вовлеченные в выполнение одного утверждения сигнала, могут перекрываться с циклами, вовлеченными для выполнения других утверждений сигнала. Тракт 2.3(iii) был представлен, чтобы с акцентировать это для утверждения 2.3b. Сигнал <code>b</code> должен утверждаться в циклах с 5 до 7 (помечено “1”), в связи с утверждением сигнала a в цикле 2, и должен утверждаться в циклах с 7 до 9 (помечено “2”), в связи с утверждением в цикле 4. 
 +
 +
<!--
 +
A next_e[i:j] property holds if there ''exists'' a cycle from the next <code>i</code>
 +
through the next <code>j</code> cycles in which its operand holds. For example, Assertion
 +
2.3c states that whenever signal <code>a</code> holds, signal <code>b</code> holds either three, four,
 +
or five cycles later. There is nothing in Assertion 2.3c that prevents a single
 +
assertion of signal <code>b</code> from satisfying multiple assertions of signal <code>a</code>, thus it
 +
holds on Trace 2.3(vi) because the assertion of <code>b</code> at cycle 7 comes five cycles
 +
after the assertion of signal <code>a</code> at cycle 2, and three cycles after the assertion
 +
of signal <code>a</code> at cycle 4. We examine the issue of specifying a one-to-one
 +
correspondence between signals in Section 13.4.2.
 +
-->
 +
Свойство next_e[i:j] выполняется, если ''существует'' цикл со следующего <code>i</code> до следующих <code>j</code> циклов, в которых выполняются операнды. Например, утверждение 2.3с показывает, что когда бы сигнал <code>a</code> не выполнялся, сигнал <code>b</code> выполняется тремя, четырьмя или пятью циклами позже. Нету ничего в утверждении 2.3с, что предотвращает единичное утверждение сигнала <code>b</code> из выполнения многочисленных утверждений сигнала <code>a</code>, таким образом это выполняется в тракте 2.3(vi), потому что утверждение сигнала <code>b</code>, в цикле 7, появляется через 5 циклов после утверждения сигнала <code>a</code> в цикле 2, и через три цикла после утверждения сигнала <code>a</code> в цикле 4. 
 +
 +
<!--
 +
Assertion 2.3c also holds on Traces 2.3(i), 2.3(iii), 2.3(iv), and 2.3(v),
 +
since there are enough assertions of signal <code>b</code> at the appropriate times. In
 +
Traces 2.3(i), 2.3(iii), and 2.3(iv) there are more than enough assertions of <code>b</code>
 +
to satisfy the property being asserted (in Trace 2.3(i), the assertion of <code>b</code> at
 +
cycle 7 is enough, because it comes five cycles after the assertion of <code>a</code> at cycle
 +
2, and three cycles after the assertion of <code>a</code> at cycle 4). In Trace 2.3(v) there
 +
are just enough assertions of <code>b</code> to satisfy the requirements of Assertion 2.3c.
 +
-->
 +
Утверждение 2.3с также выполняется на трактах 2.3(i), 2.3(iii), 2.3(iv) и 2.3(v), т.к. есть достаточное количество утверждений сигнала <code>b</code> в соответствующее время. В трактах 2.3(i), 2.3(iii) и 2.3(iv) более, чем достаточно утверждений сигнал <code>b</code> для выполнения утвержденного свойства (в тракте 2.3(i) утверждения сигнала <code>b</code> в цикле 7 достаточно, потому что проходит 5 циклов после утверждения сигнала <code>a</code> в цикле 2, и три цикла после утверждения сигнала <code>a</code> в цикле 4). В тракте 2.3(v) достаточно утверждений сигнала <code>b</code> для выполнения требований утверждения 2.3c. 
 +
 +
<!--
 +
The <code>next_event</code> operator is a conceptual extension of the <code>next</code> operator.
 +
While next refers to the next cycle, <code>next_event</code> refers to the next
 +
cycle in which some Boolean condition holds. For example, Assertion 2.4a
 +
expresses the requirement that whenever a high priority request is received
 +
(signal <code>high_pri_req</code> is asserted), then the next grant (assertion of signal
 +
<code>gnt</code>) must be to a high priority requester (signal <code>high_pri_ack</code> is asserted).
 +
Assertion 2.4a holds on Trace 2.4(i). There are two assertions of signal
 +
<code>high_pri_req</code>, the first at cycle 1 and the second at cycle 10. The associated
 +
assertions of <code>gnt</code> occur at cycles 4 and 11, respectively, and <code>high_pri_ack</code>
 +
holds in these cycles.
 +
-->
 +
Оператор <code>next_event</code> концептуально расширенный оператор <code>next</code>. В то время как <code>next</code> относиться к следующему циклу, <code>next_event</code> относиться к следующему циклу, в котором выполняется некоторое Булево условие. Например, утверждение 2.4а выражает требование того, что когда бы ни принимался запрос с высоким приоритетом (сигнал <code>high_pri_req</code> утвержден), то следующим (утверждение сигнала <code>gnt</code>) должен быть, также, запрос с высоким приоритетом (сигнал <code>high_pri_ack</code> утвержден). Утверждение 2.4а выполняется в тракте 2.4(i). Существует два утверждения сигнала <code>high_pri_req</code>, первое в цикле 1 и второе в цикле 10. Связанные утверждения <code>gnt</code> встречаются в циклах 4 и 11, соответственно, и <code>high_pri_ack</code> выполняется в этих циклах.       
 +
 +
<!--
 +
The <code>next_event</code> operator includes the current cycle. That is, an assertion
 +
of <code>b</code> in the current cycle will be considered the next assertion of <code>b</code> in the
 +
property <code>next_event(b)(p)</code>. For instance, consider Trace 2.4(ii). Trace 2.4(ii)
 +
is similar to Trace 2.4(i) except that there is an additional assertion of
 +
<code>high_pri_req</code> at cycle 8 and two additional assertions of <code>gnt</code> at cycles 8
 +
and 9, one of which has an associated <code>high_pri_ack</code>. Assertion 2.4a holds on
 +
Trace 2.4(ii) because the assertion of <code>gnt</code> at cycle 8 is considered the next
 +
assertion of <code>gnt</code> for the assertion of <code>high_pri_req</code> at cycle 8. If you want to
 +
exclude the current cycle, simply insert a <code>next</code> operator in order to move the
 +
current cycle of the <code>next_event</code> operator over by one, as in Assertion 2.4b.
 +
Assertion 2.4b does not hold on Trace 2.4(ii). Because of the insertion of the
 +
next operator, the relevant assertions of <code>gnt</code> have changed from cycles 4, 8
 +
and 11 for Assertion 2.4a to cycles 4, 9 and 11 for Assertion 2.4b, and at cycle
 +
9 there is no assertion of <code>high_pri_ack</code> in Trace 2.4(ii).
 +
-->
 +
Оператор <code>next_event</code> включает текущие циклы. Это значит, утверждения сигнала <code>b</code> в текущем цикле должно считаться следующим утверждением сигнала <code>b</code> в свойстве <code>next_event(b)(p)</code>. Например, рассмотрим тракт 2.4(ii). Тракт 2.4(ii) так же, как тракт 2.4(i) ожидает, что существуют дополнительные утверждения <code>high_pri_req</code> в цикле 8 и два дополнительных утверждения <code>gnt</code> в циклах 8 и 9, одно из которых связанно с <code>high_pri_ack</code>.  Утверждение 2.4а выполняется на тракте Trace 2.4(ii), потому что утверждение <code>gnt</code> в цикле 8 считается следующим утверждением <code>gnt</code> для утверждения <code>high_pri_req</code> в цикле 8. Если вы хотите исключить текущий цикл, можно вставить оператор <code>next</code> для перемещения текущего цикла оператора <code>next_event</code> на один цикл далее, как в утверждении 2.4b. Утверждение 2.4b не выполняется в тракте 2.4(ii). Потому что вставка оператора <code>next</code> привела к смене циклов утверждений <code>gnt</code>, с циклов 4, 8 и 11 для утверждения 2.4a на циклы 4, 9 и 11 для утверждения 2.4b, а в цикле 9 нету утверждений <code>high_pri_ack</code> в тракте 2.4(ii).         
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.4i.png]]
 +
|-
 +
! (i) Assertions 2.4a and 2.4b hold
 +
|-
 +
! [[Файл:Psl fig 02.4ii.png]]
 +
|-
 +
! (ii) Утверждение 2.4a выполняется, а 2.4b нет
 +
|-
 +
|<pre>
 +
assert always (high_pri_req ->            (2.4a)
 +
  next_event(gnt)(high_pri_ack));
 +
 +
assert always (high_pri_req ->            (2.4b)
 +
  next next_event(gnt)(high_pri_ack));
 +
</pre>
 +
|-
 +
! Рис. 2.4: <code>next_event</code>
 +
|}
 +
 +
<!--
 +
Just as we can use <code>next[i]</code> to indicate the ''i<sup>th</sup>'' next cycle, we can use
 +
<code>next_event(b)[i]</code> to indicate the ''i<sup>th</sup>'' occurrence of <code>b</code>. For example, in order
 +
to express the requirement that every time a request is issued (signal <code>req</code> is
 +
asserted), <code>signal_last</code> ready must be asserted on the fourth assertion of signal
 +
<code>ready</code>, we can code Assertion 2.5a. Assertion 2.5a holds on Trace 2.5(i). For
 +
the first assertion of <code>req</code>, at cycle 1, the four assertions of <code>ready</code> happen
 +
to come immediately and in consecutive cycles. For the second assertion of
 +
<code>req</code>, at cycle 7, the four assertions of <code>ready</code> do not happen immediately and
 +
do not happen consecutively either – they are spread out over seven cycles,
 +
interspersed with cycles in which <code>ready</code> is deasserted. However, the point is
 +
that in both cases, signal <code>last_ready</code> is asserted on the fourth assertion of
 +
<code>ready</code>, thus Assertion 2.5a holds on Trace 2.5(i).
 +
-->
 +
Так как мы можем использовать <code>next[i]</code> для индикации ''i<sup>-го</sup>'' следующего цикла, мы можем использовать <code>next_event(b)[i]</code> для индикации ''i<sup>-го</sup>'' вхождения сигнала <code>b</code>. Например, для выражения требования,что всегда выдается запрос (signal <code>req</code> утвержден), готовность <code>signal_last</code> должна быть утверждена на четвертом утверждении сигнала <code>ready</code>. Утверждение 2.5а выполняется на тракте 2.5(i). Для первого утверждения <code>req</code>, в цикле 1, четыре утверждения <code>ready</code> происходят немедленно в следующих циклах. Для второго утверждения <code>req</code>, в цикле 7, четыре утверждения <code>ready</code> не происходят немедленно  и не происходят последовательно - они распространяются через семь циклов, пресекаясь с циклами, в которых <code>ready</code> не подтвержден. Однако, отметим,что в обоих случаях, сигнал <code>last_ready</code> утверждается на четвертом утверждении <code>ready</code>, таким образом утверждение 2.5a выполняется в тракте 2.5(i).       
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.5.png]]
 +
|-
 +
! (i) Утверждение 2.5a выполняется
 +
|-
 +
|<pre>
 +
assert always (req ->                (2.5a)
 +
  next event(ready)[4](last ready));
 +
</pre>
 +
|-
 +
! Рис. 2.5: next event[n]
 +
|}
 +
 +
 +
<!--
 +
As with <code>next_a[i:j]</code> and <code>next_e[i:j]</code>, the <code>next_event</code> operator also
 +
comes in forms that allow it to indicate ''all'' of a range of future cycles, or the ''existence''
 +
of a future cycle in such a range. The form <code>next_event_a(b)[i:j](f)</code>
 +
indicates that we expect <code>f</code> to hold on all of the ''i<sup>th</sup>'' through ''j<sup>th</sup>'' occurrences
 +
of <code>b</code>. For example, Assertion 2.6a indicates that when we see a read request
 +
(assertion of signal <code>read_request</code>) with tag equal to <code>i</code>, then on the next four
 +
data transfers (assertion of signal <code>data</code>), we expect to see tag <code>i</code>. Assertion 2.6a
 +
uses the <code>forall</code> construct, which we will examine in detail later. For now, suffice
 +
it to say that Assertion 2.6a states a requirement that must hold for all
 +
possible values of the signal <code>tag[2:0]</code>. Assertion 2.6a holds on Trace 2.6(i)
 +
because after the first assertion of signal <code>read_request</code>, where <code>tag[2:0]</code> has
 +
the value 4, the value of <code>tag[2:0]</code> is also 4 on the next four assertions of
 +
signal <code>data</code> (at cycles 5, 9, 10 and 11). Likewise, on the second assertion of
 +
signal <code>read_request</code>, where <code>tag[2:0]</code> has the value 5, the value of <code>tag[2:0]</code>
 +
is also 5 on the next four assertions of signal <code>data</code> (at cycles 17 through 20).
 +
-->
 +
Как и с <code>next_a[i:j]</code> и <code>next_e[i:j]</code>, оператор <code>next_event</code> также появляется в форме, которая позволяет выражать ''весь'' диапазон следующих циклов, или ''наличие'' будущего цикла в этом диапазоне. Форма <code>next_event_a(b)[i:j](f)</code> показывает, что мы ожидаем выполнения <code>f</code> на всех ''i<sup>-х</sup>'' через ''j<sup>-е</sup>'' вхождения <code>b</code>. Например, утверждение 2.6a показывает, что когда мы видим запрос на чтение (утверждение сигнала <code>read_request</code>) с тэгом эквивалентным <code>i</code>, далее на следующих четырех передачах данных (утверждение сигнала <code>data</code>), мы ожидаем увидеть тэг <code>i</code>. Утверждение 2.6а использует конструкцию <code>forall</code>, которую мы рассмотрим в деталях позже. Сейчас достаточно сказать, что утверждение 2.6а показывает требование, что должно выполняться для всех возможных значениях сигнала <code>tag[2:0]</code>. Утверждение 2.6а выполняется в тракте 2.6(i), потому что после первого утверждения сигнала <code>read_request</code>, где значение <code>tag[2:0]</code> 4, значение <code>tag[2:0]</code>, также, 4 на четырех следующих утверждениях сигнала <code>data</code> (в циклах 5, 9, 10 и 11). Более того, на втором утверждении сигнала <code>read_request</code>, где <code>tag[2:0]</code> имеет значение 5, значение <code>tag[2:0]</code>, также, 5 на следующих четырех утверждениях сигнала <code>data</code> (циклы с 17 по 20).   
 +
 +
<!--
 +
In order to indicate that we expect something to happen on one of the next
 +
''i<sup>th</sup>'' to ''j<sup>th</sup>'' cycles, we can use the <code>next_event_e(b)[i:j](f)</code> operator, which
 +
indicates that we expect <code>f</code> to hold on one of the ''i<sup>th</sup>''  through ''j<sup>th</sup>''  occurrences of
 +
<code>b</code>. For example, consider again Assertion 2.4a. It requires that whenever a high
 +
priority request is received, the next grant must be to a high priority requester.
 +
Suppose instead that we require that one of the next ''two'' grants be to a high
 +
priority requester. We can express this using Assertion 2.7a. Assertion 2.7a
 +
holds on Trace 2.7(i) because every time that signal <code>high_pri_req</code> is asserted,
 +
signal <code>high_pri_ack</code> is asserted on one of the next two assertions of <code>gnt</code>.
 +
-->
 +
Для того, чтобы указать, что мы ожидаем чего-либо в одном из следующих циклов с ''i<sup>-го</sup>'' по ''j<sup>-й</sup>'', мы можем использовать оператор <code>next_event_e(b)[i:j](f)</code>, который показывает, что мы ожидаем выполнения <code>f</code> в одном из циклов, с ''i<sup>-го</sup>'' по ''j<sup>-й</sup>'', вхождения <code>b</code>. Например, рассмотри опять утверждение 2.4a. Оно требует того, что когда бы ни приходил запрос высокого приоритета, следующим должен обработаться запрос с высоким приоритетом. Предположим вместо этого, что мы требуем, чтобы один из следующих ''двух'' грантов был для запроса с высоким приоритетом. Мы можем выразить это, используя утверждение 2.7a. Утверждение 2.7a выполняется в тракте 2.7(i), потому что всегда, когда сигнал <code>high_pri_req</code> утверждается, сигнал <code>high_pri_ack</code> утверждается на одном из следующих двух утверждений <code>gnt</code>.     
 +
 +
<!--
 +
The syntax of the range specification for all operators – including those
 +
we have not yet seen – is flavor dependent. In the Verilog, SystemVerilog and
 +
SystemC flavors, it is <code>[i:j]</code>. In the VHDL flavor it is <code>[i to j]</code>. In the GDL
 +
flavor it is <code>[i..j]</code>.
 +
-->
 +
Синтаксис спецификации диапазона для всех операторов, включая тех, которые мы еще не рассматривали, зависит от фундаментального языка. В вариантах Verilog, SystemVerilog и SystemC, это код <code>[i:j]</code>. Для VHDL - это код <code>[i to j]</code>. Для GDL это - <code>[i..j]</code>.
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.6.png|600px]]
 +
|-
 +
! (i) Утверждение 2.6a выполняется
 +
|-
 +
|<pre>
 +
assert forall i in {0:7}:                      (2.6a)
 +
  always ((read_request && tag[2:0]==i) ->
 +
      next_event_a(data)[1:4](tag[2:0]==i));
 +
</pre>
 +
|-
 +
! Рис. 2.6 <code>next_event a[i:j]</code>
 +
|}
 +
 +
=== 2.4 Операторы <code>until</code> и <code>before</code> ===
 +
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.7.png|400px]]
 +
|-
 +
! (i) Утверждение 2.7a выполняется
 +
|-
 +
|<pre>
 +
assert always (high_pri_req ->                (2.7a)
 +
  next_event_e(gnt)[1:2](high_pri_ack));
 +
</pre>
 +
|-
 +
! Рис. 2.7: <code>next_event e[i:j]</code>
 +
|}
 +
 +
<!--
 +
The <code>until</code> operator provides another way to move forward, this time while
 +
putting a requirement on the cycles in which we are moving. For example,
 +
Assertion 2.8a states that whenever signal <code>req</code> is asserted, then, starting at
 +
the next cycle, signal <code>busy</code> must be asserted up until signal <code>done is</code> asserted.
 +
Assertion 2.8a requires that <code>busy</code> will be asserted up to, but not necessarily
 +
including, the cycle where <code>done</code> is asserted. In order to include the cycle where
 +
<code>done</code> is asserted, use the operator <code>until_</code>. The underscore (<code>_</code>) is intended to
 +
represent the extra cycle in which we require that <code>busy</code> should stay asserted,
 +
so Assertion 2.8b states that whenever signal <code>req</code> is asserted, then starting
 +
from the next cycle, <code>busy</code> must be asserted and must stay asserted up until
 +
and including the cycle where done is asserted. For example, Assertion 2.8a
 +
holds on Trace 2.8(i), but Assertion 2.8b does not, because <code>busy</code> is not asserted at cycles 4 and 10. Both Assertions 2.8a and 2.8b hold on Trace 2.8(ii):
 +
Assertion 2.8a does not prohibit the assertion of busy at cycles 4 and 10 – it
 +
just does not require it.
 +
-->
 +
Оператор <code>until</code> предоставляет другой путь движения вперед, здесь накладываются требования на циклы, в которые мы движемся. Например, утверждение 2.8а показывает, что когда бы сигнал <code>req</code> не был утвержден, далее, начиная со следующего цикла, сигнал  <code>busy</code> должен быть утвержден до тех пор, пока не утвердиться сигнал <code>done</code>. Утверждение 2.8а требует, чтобы <code>busy</code> был утвержден до, но необязательно включая, цикла, в котором утверждается <code>done</code>. Для включения этого цикла, используется оператор <code>until_</code>. Подчеркивание (<code>_</code>) служит для того, чтобы указать дополнительный цикл, для которого мы требуем, чтобы <code>busy</code> оставался утвержденным, таким образом утверждение 2.8b показывает, что кода бы сигнал <code>req</code> не утверждался, далее, начиная со следующего цикла, <code>busy</code> должен быть утвержден, и должен оставаться в таком состоянии до цикла, в котором утверждается <code>done</code>, включительно. Например, утверждение 2.8а выполняется на тракте 2.8(i), а утверждение 2.8b нет, потому что <code>busy</code>не утверждается в циклах 4 и 10. Оба утверждения 2.8a и 2.8b выполняются на тракте 2.8(ii): утверждение 2.8a не запрещает утверждения сигнала <code>busy</code>  в циклах 4 и 10 - это просто не требуется.               
 +
 +
<!--
 +
If signal done is asserted the cycle after signal <code>req</code> is asserted, Assertion 2.8a does not require that signal <code>busy</code> be asserted at all, while Assertion 2.8b does. That is, Assertion 2.8a holds on Trace 2.8(iii) – the fact that
 +
done happens immediately after <code>req</code> leaves no cycles on which busy needs to
 +
be asserted. Assertion 2.8b does not hold on Trace 2.8(iii) because of a missing
 +
assertion of <code>busy</code> in the cycle in which <code>done</code> is asserted.
 +
-->
 +
Если сигнал <code>done</code> утверждается на следующем цикле после утверждения <code>req</code>, утверждение 2.8a не требует, чтобы сигнал <code>busy</code>, в принципе, утверждался, в отличие от утверждения 2.8b. То есть, утверждение 2.8а выполняется на тракте 2.8(iii) - факт того, что <code>done</code> утверждается немедленно после утверждения <code>req</code>, не оставляет циклов для утверждения <code>busy</code>. Утверждение 2.8b не выполняется в тракте 2.8(iii), из-за пропущенного утверждения <code>busy</code> в цикле, в котором утверждается <code>done</code>.     
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.8.png|600px]]
 +
|-
 +
!
 +
|-
 +
|<pre>
 +
assert always (req -> next (busy until done));          (2.8a)
 +
assert always (req -> next(busy until_ done));          (2.8b)
 +
</pre>
 +
|-
 +
! Рис. 2.8: Операторы <code>until</code> и <code>until_</code>
 +
|}
 +
 +
<!--
 +
The <code>before</code> family of operators provides an easy way to state that we
 +
require some signal to be asserted before some other signal. For example, suppose that we have a pulsed signal called <code>req</code>, and we have the requirement that
 +
before we can make a second request, the first must be acknowledged. We can
 +
express this in PSL using Assertion 2.9a. We need the <code>next</code> to take us forward
 +
one cycle so that the <code>req</code> in (<code>ack before req</code>) is sure to refer to some other
 +
<code>req</code>, and not the one we have just seen. To understand this, let us examine a
 +
flawed version of the same specification. Consider Assertion 2.9b. It requires
 +
that (<code>ack before req</code>) hold at every cycle in which <code>req</code> holds. Consider,
 +
for example, cycle 1 of Trace 2.9(i). Signal <code>req</code> is asserted. Therefore, (<code>ack before req</code>) must hold at cycle 1. However, it does not, because starting at
 +
cycle 1 and looking forward, we first see an assertion of signal <code>req</code> (at cycle 1),
 +
and only afterwards an assertion of signal <code>ack</code> (at cycle 3) – so <code>req</code> is asserted
 +
before <code>ack</code>, and not the other way around. Assertion 2.9a, on the other hand,
 +
states what we want: at cycle 1, for example, we require <code>next</code> (<code>ack before req</code>) to hold. Therefore, we require that (<code>ack before req</code>) hold at cycle 2.
 +
Starting at cycle 2 and looking forward, we first see an assertion of <code>ack</code> (at
 +
cycle 3), and only afterwards an assertion of <code>req</code> (at cycle 6).
 +
-->
 +
Семейство операторов <code>before</code> предоставляет легкий путь для показания требований, чтобы некоторый сигнал утверждался перед каким-либо другим сигналом. Например, предположим, что у нас есть импульсный сигнал <code>req</code>, и мы имеем требование, что перед тем, как мы сможем сделать второй запрос, первый должен быть определен. Мы можем выразить это в PSL используя утверждение 2.9а. Нам нужен оператор <code>next</code> для передвижения на один цикл вперед, таким образом <code>req</code> в (<code>ack before req</code>) точно будет ссылаться на другие <code>req</code>, а не на тот, который был только что. Чтобы это понять, исследуем недостаточную версию этой спецификации. Рассматривая утверждение 2.9b. Оно требует, чтобы (<code>ack before req</code>) выполнялось на каждом цикле, в котором выполняется <code>req</code>. Например, цикл 1 тракта 2.9(i). Сигнал <code>req</code> утверждается. Поэтому, (<code>ack before req</code>) должен утвердиться в цикле 1. Однако, этого не происходит, потому что, начав с первого цикла и следуя далее, изначально мы увидим утверждения сигнала <code>req</code> (в цикле 1), и только после этого утверждение сигнала <code>ack</code> (в цикле 3) - таким образом <code>req</code> утверждается перед <code>ack</code>, а не наоборот. Утверждение 2.9а, с другой стороны, показывает, что мы хотим: в цикле 1, например, мы требуем выполнения <code>next</code> (<code>ack before req</code>). Поэтому, мы требуем, чтобы (<code>ack before req</code>) выполнлся на цикле 2. Начиная с цикла 2 и двигаясь вперед, изначально мы увидим утверждение <code>ack</code> (на цикле 3), и только после этого утверждение <code>req</code> (в цикле 6).               
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.9.png|600px]]
 +
|-
 +
|<pre>
 +
assert always (req -> next (ack before req)); (2.9a)
 +
assert always (req -> (ack before req)); (2.9b)
 +
assert always (req -> next (ack before_ req)); (2.9c)
 +
assert always (req -> (ack || next (ack before req))); (2.9d)
 +
</pre>
 +
|-
 +
! Рис. 2.9 Операторы <code>before</code> и <code>before_</code>
 +
|}
 +
 +
<!--
 +
The <code>before</code> operator requires that its first operand happen strictly before
 +
its second. In order to specify that something must happen before or at the
 +
same cycle as something else, use <code>before_</code>. The underscore (<code>_</code>) is intended
 +
to represent the cycle in which we allow an overlap between the left and
 +
right sides. For example, in order to specify that behavior like that shown
 +
in Trace 2.9(i) is allowed, and that in addition behavior like that shown in
 +
Trace 2.9(ii) is allowed, use Assertion 2.9c.
 +
-->
 +
Оператор <code>before</code> требует, чтобы первый операнд выполнялся строго перед вторым. Для того, чтобы показать, что что-то должно выполниться перед или в том же цикле, как и что-либо иное, используется оператор <code>before_</code>. Подчеркивание (<code>_</code>) предназначено для представления цикла, в котором мы допускаем прекрытие между левой и правой сторонами. Например,  для того чтобы показать, что поведениее соответствует тем, которые показаны в тракте 2.9(i) и в тракте Trace 2.9(ii), используется утверждение 2.9с.
 +
 +
<!--
 +
What if the assertion of <code>ack</code> is allowed to come, not together with the next
 +
assertion of <code>req</code>, but rather together with the request being acknowledged?
 +
In other words, what if in addition to the behavior shown in Trace 2.9(i), we
 +
want to allow the behavior shown in Trace 2.9(iii)? As we have seen previously,
 +
Assertion 2.9b is not the answer. Rather, we can code Assertion 2.9d.
 +
-->
 +
Что если утверждению <code>ack</code> позволенно выполниться не вместе со следующим утверждением <code>req</code>, но вместе с установленным запросом? Другими словами, что если в дополнение к поведению, показаному в тракте 2.9(i), мы хотим допустить поведение показанное в тракте 2.9(iii)? Как было отмечно ранее, утверждение 2.9b это не ответ. Скорее, мы напишем код утверждения 2.9d.
 +
 +
===2.5 Оператор <code>eventually!</code>===
 +
 +
<!--
 +
The <code>eventually!</code> operator allows you to specify that something must occur in
 +
the future without saying exactly when. For example, Assertion 2.10a states
 +
that every request (assertion of <code>req</code>) must be followed at some time with
 +
an acknowledge (assertion of <code>ack</code>). There is nothing in Assertion 2.10a to
 +
prevent a single acknowledge from satisfying the requirement for multiple
 +
requests, thus Assertion 2.10a holds on Trace 2.10(i). We examine the issue
 +
of specifying a one-to-one correspondence between signals in Section 13.4.2.
 +
-->
 +
Оператор <code>eventually!</code> позволяет показать, что что-либо должно произойти в будущем, без конкретного уточнения когда. Например, утверждение 2.10а показывает, что каждый запрос (утверждение <code>req</code>) должен следовать в то же время, что и установленный (assertion of <code>ack</code>). Нету ничего в утверждении 2.10а, чтобы предотвратить единичного установления из удовлетворяющих требования для множественных запросов, таким образом утверждение 2.10а выполняется на тракте 2.10(i). Мы проверили этот вопрос спецификации взаимно однозначных соответствий между сигналами в разделе 13.4.2.   
 +
 +
<!--
 +
The exclamation point (<code>!</code>) of the <code>eventually!</code> operator indicates that it
 +
is a strong operator. We discuss weak vs. strong temporal operators in detail
 +
in Chapter 4.
 +
-->
 +
Восклицательный знак (<code>!</code>) в операторе <code>eventually!</code> показывает, что это сильный оператор. Обсуждения сильных и слабых оператров пойдет в главе 4.
 +
 +
{| align=center
 +
! [[Файл:Psl fig 02.10.png|600px]]
 +
|-
 +
! (i) Утверждение 2.10a выполняется
 +
|-
 +
|<pre>
 +
assert always (req -> eventually! ack);      (2.10a)
 +
</pre>
 +
|-
 +
! Рис. 2.10: Оператор <code>eventually!</code>
 +
|}

Текущая версия на 23:50, 13 ноября 2013

PSL
Литература
Введение в PSL
* VHDL * OS-VVM * Co-Simulation *

Содержание

Основные временные свойства

В то время как Булевый слой состоит из Булевых выражений, которые выполняются или не выполняются в данном цикле, временной слой предоставляет путь для описания взаимоотношений между Булевыми выражениями по времени. PSL утверждение обычно представлено только в одном направлении - вперед, от первого цикла (также можно двигаться в обратном направлении, используя встроенные функции, такие как prev(), rose() и fell()). Таким образом, простое PSL утверждение assert a; показывает, что a должно утверждаться в самом первом цикле, в то время как PSL утверждение assert always a, показывает, что a должно утверждаться в перовм цикле и в каждом следующем цикле, а это значит, что в каждом цикле.

Комбинированием временных операторов различными путями, мы можем установить свойства, такие как “каждый запрос получает подтверждение”, “каждому подтвержденному запросу предоставляется от четырех до семи циклов, в случаи, если запрос не приостановится первым”, “две последовательные записи не должны располагать по одному и тому же адресу” и “когда мы видим запрос на чтение с тэгом i, на следующих четырех передах данных ожидается увидеть тэг i”.

Временной слой состоит из фундаментального языка (FL) и дополнительного расширения ветвления (OBE). FL используется для выражения свойств одного тракта, а также используется для моделирования или формальной верификации. OBE используется для выражения свойств, относящихся к набору трактов, например, “существует тракт, такой как ...”, и также используется для формальной верификации. В этой книге мы сконцентрируемся на фундаментальном языке.

Фундаментальный язык состоит из двух комплементарных стилей - LTL стиль, названный из-за временной логики LTL, на которой базируется PSL, и SERE стиля, названного из-за последовательного расширения регулярных выражений PSL, или SEREs. В этой главе мы представим основные временные операторы LTL стиля. Мы предоставим то, что будет достаточно для понимания основной идеи, и чтобы дать некий контекст, для философских замечаний,обсуждаемых далее.

В этой книге, мы широко используем примеры. Каждый пример свойства или утверждения связан с временной диаграммой (которую мы называем тракт) сгруппирован вместе на рисунке. Такой рисунок будет содержать один или более трактов, нумерованных в скобках строчными римскими цифрами, одного или более свойств, нумерованных добавление строчной буквы к номеру рисунка. Например, Рисунок 2.1 содержит тракт 2.1(i) и утверждения 2.1а, 2.1b, 2.1c.

2.1 Операторы always и never

Нам уже встречались основные временные операторы always и never. Большинство свойств PSL начинаются с одного или с другого. Это, потому что “голое” (Булево) PSL свойство относится только к первому циклу тракта. Например, утверждение 2.1a требует только того, чтобы Булево выражение !(a && b) выполнялось в первом цикле. Таким образом, утверждение 2.1а выполняется в тракте 2.1(i), потому что Булево выражение !(a && b) выполняется в цикле 0. Для того, чтобы сформулировать, что мы хотим, чтобы оно выполнялось в каждом цикле проекта, мы должны добавить временной оператор always, и получить утверждение 2.1b. Утверждение 2.1b не поддерживает тракт 2.1(i), потому что Булево выражение !(a && b) не выполняется в цикле 5. Эквивалентно, мы можем поменять оператор always и Булево отрицание ! с never, чтобы получить утверждение 2.1с.

Psl fig 02.1.png
(i) Утверждение 2.1a выполняется, но 2.1b and 2.1c нет 
assert !(a && b);              (2.1a)
assert always !(a && b);       (2.1b)
assert never (a && b);         (2.1c)
Рис. 2.1: Операторы always и never

Оба утверждения 2.1b и 2.1c показывают, что сигналы a и b взаимоисключающиеся. Очевидно, все, что может использоваться с оператором always, может также использоваться с оператором never и наоборот, происходит простое отрицанием операнда, когда происходит переключение между always и never. PSL, для удобства, предоставляет два варианта использования, иногда более удобно описать свойство положительным (если свойство выполняется на всех циклах), а иногда удобней отрицательным (если свойство не выполняется ни в каком цикле). В общем, существует много путей описания свойств в PSL. Мы рассмотрим другие примеры далее.

2.2 Оператор next

Другой временной оператор - это оператор next. Он показывает, что свойство свойство должно выполняться, если его операнд выполняется в следующем цикле. Например, утверждение 2.2a показывает, что когда бы a не выполнялось, b должно выполниться в следующем цикле. Утверждение 2.2a использует другой важный оператор, логический оператор импликации (->). В то время как оператор логической импликации Булевый, а не временной (он не свяжет два подсвойства по времени), это играет очень важную роль во многих временных свойствах. Логическая импликация prop1 -> prop2 выполняется, если prop1 не выполняется или prop2 выполняется. Это хорошо представляется, если принять это, как выражение вида if-then, с частью else. prop1 -> prop2 можно понимать, как если prop1, то далее следует prop2, иначе возвращается значение правда. Таким образом, под-свойство a -> next b, в нашем примере, выполняется, если a не выполняется (потому что свойство по умолчание имеет значение правда) или, если a выполняется, а также и next b выполняется. Добавляя оператор always, мы получаем свойство, которое выполняется, если под-свойство a -> next b выполняется в каждом цикле. Таким образом, утверждение 2.2а показывает, что когда бы ни выполнялось a, b должно выполняться в следующем цикле. Утверждение 2.2а выполняется по сигналу b. Это показано в “if” и “then” примечании на тракте 2.2(ii). “Дополнительные” утверждения сигнала b на циклах 1 и 10, спровоцированы утверждение 2.2а, потому что в нем ничего не сказано о значениях b в цикле, кроме того, что следует из из утверждения a.

Отметим, что циклы вовлеченные в выполнение одного утверждения сигнала, могут перекрываться с теми,которые вовлечены в выполнение другого утверждения. Например, учитывая тракт 2.2(iii), который является простым трактом 2.2(ii) с if-then пронумерованными парами. Имеем четыре утверждения сигнала a на тракте 2.2(iii), и таким образом четыре связанных цикла, в которых b должен утверждаться. Каждая пара циклов (утверждение a следует из утверждения b) нумерованы в тракте 2.2(iii). Рассматривая пары 2 и 3. Сигнал a утверждается в 4 цикле пары 2, таким образом сигнал b должен утвердиться в 5 цикле, для того, чтобы утверждение 2.2а выполнялось. Сигнал а утверждается в цикле 5 пары 3, таким образом требуется утверждение сигнала b в 6 цикле. Пары 2 и 3 перекрываются, потому что, в то время как мы ищем утверждение сигнала b в 5 цикле, для выполнения утверждения a в 4 цикле, также, мы видим дополнительное утверждение сигнала a, который рассматривается.

Утверждение 2.2а не выполняется в тракте 2.2(iv), потому что третье утверждение сигнала a, в цикле 5, т.к. отсутствует утверждение сигнала b в следующем цикле.

Psl fig 02.2.png 
assert always (a -> next b);         (2.2a)
Рис.2.2: Операторы next и логическая импликация

2.3 вариации next, включая next_event

Свойство next выполняется, если его операнд выполняется в следующем цикле. Вариации оператора next позволяют указывать n-й следующий цикл и диапазоны будущих циклов. Свойство next[n] выполняется, если его операнд выполняется в n-й следующий цикл. Например, утверждение 2.3а показывает, что когда бы сигнал a не выполнялся, сигнал b выполниться тремя циклами позже. Утверждение 2.3а выполняется в тактах 2.3(i), 2.3(iii), 2.3(iv), но не выполняется в трактах 2.3(ii) или 2.3(v), потому что отсутствует утверждение сигнала b в цикле 7, и не выполняется в тракте 2.3(vi), потому что отсутствует утверждение сигнала b в цикле 5.

Psl fig 02.3.png 
assert always (a -> next[3] (b)); (2.3a)
assert always (a -> next_a[3:5] (b)); (2.3b)
assert always (a -> next_e[3:5] (b)); (2.3c)
Рис. 2.3: Операторы next[n], next_a[i:j] и next_e[i:j]

Свойство next_a[i:j] выполняется если его операнд выполняется во всех циклах от i-го следующего, до j-го следующего цикла включительно. Например, утверждение 2.3b показывает, что когда бы сигнал a не выполнялся, сигнал b выполняется тремя, четырьмя, пятью циклами позже. Выполняется в тракте 2.3(iii) и не выполняется в трактах 2.3(i), 2.3(ii), 2.3(iv), 2.3(v) или 2.3(vi).

Ранее мы обсуждали то факт, что циклы, вовлеченные в выполнение одного утверждения сигнала, могут перекрываться с циклами, вовлеченными для выполнения других утверждений сигнала. Тракт 2.3(iii) был представлен, чтобы с акцентировать это для утверждения 2.3b. Сигнал b должен утверждаться в циклах с 5 до 7 (помечено “1”), в связи с утверждением сигнала a в цикле 2, и должен утверждаться в циклах с 7 до 9 (помечено “2”), в связи с утверждением в цикле 4.

Свойство next_e[i:j] выполняется, если существует цикл со следующего i до следующих j циклов, в которых выполняются операнды. Например, утверждение 2.3с показывает, что когда бы сигнал a не выполнялся, сигнал b выполняется тремя, четырьмя или пятью циклами позже. Нету ничего в утверждении 2.3с, что предотвращает единичное утверждение сигнала b из выполнения многочисленных утверждений сигнала a, таким образом это выполняется в тракте 2.3(vi), потому что утверждение сигнала b, в цикле 7, появляется через 5 циклов после утверждения сигнала a в цикле 2, и через три цикла после утверждения сигнала a в цикле 4.

Утверждение 2.3с также выполняется на трактах 2.3(i), 2.3(iii), 2.3(iv) и 2.3(v), т.к. есть достаточное количество утверждений сигнала b в соответствующее время. В трактах 2.3(i), 2.3(iii) и 2.3(iv) более, чем достаточно утверждений сигнал b для выполнения утвержденного свойства (в тракте 2.3(i) утверждения сигнала b в цикле 7 достаточно, потому что проходит 5 циклов после утверждения сигнала a в цикле 2, и три цикла после утверждения сигнала a в цикле 4). В тракте 2.3(v) достаточно утверждений сигнала b для выполнения требований утверждения 2.3c.

Оператор next_event концептуально расширенный оператор next. В то время как next относиться к следующему циклу, next_event относиться к следующему циклу, в котором выполняется некоторое Булево условие. Например, утверждение 2.4а выражает требование того, что когда бы ни принимался запрос с высоким приоритетом (сигнал high_pri_req утвержден), то следующим (утверждение сигнала gnt) должен быть, также, запрос с высоким приоритетом (сигнал high_pri_ack утвержден). Утверждение 2.4а выполняется в тракте 2.4(i). Существует два утверждения сигнала high_pri_req, первое в цикле 1 и второе в цикле 10. Связанные утверждения gnt встречаются в циклах 4 и 11, соответственно, и high_pri_ack выполняется в этих циклах.

Оператор next_event включает текущие циклы. Это значит, утверждения сигнала b в текущем цикле должно считаться следующим утверждением сигнала b в свойстве next_event(b)(p). Например, рассмотрим тракт 2.4(ii). Тракт 2.4(ii) так же, как тракт 2.4(i) ожидает, что существуют дополнительные утверждения high_pri_req в цикле 8 и два дополнительных утверждения gnt в циклах 8 и 9, одно из которых связанно с high_pri_ack. Утверждение 2.4а выполняется на тракте Trace 2.4(ii), потому что утверждение gnt в цикле 8 считается следующим утверждением gnt для утверждения high_pri_req в цикле 8. Если вы хотите исключить текущий цикл, можно вставить оператор next для перемещения текущего цикла оператора next_event на один цикл далее, как в утверждении 2.4b. Утверждение 2.4b не выполняется в тракте 2.4(ii). Потому что вставка оператора next привела к смене циклов утверждений gnt, с циклов 4, 8 и 11 для утверждения 2.4a на циклы 4, 9 и 11 для утверждения 2.4b, а в цикле 9 нету утверждений high_pri_ack в тракте 2.4(ii).

Psl fig 02.4i.png
(i) Assertions 2.4a and 2.4b hold
Psl fig 02.4ii.png
(ii) Утверждение 2.4a выполняется, а 2.4b нет 
assert always (high_pri_req ->             (2.4a)
   next_event(gnt)(high_pri_ack));

assert always (high_pri_req ->             (2.4b)
   next next_event(gnt)(high_pri_ack));
Рис. 2.4: next_event

Так как мы можем использовать next[i] для индикации i-го следующего цикла, мы можем использовать next_event(b)[i] для индикации i-го вхождения сигнала b. Например, для выражения требования,что всегда выдается запрос (signal req утвержден), готовность signal_last должна быть утверждена на четвертом утверждении сигнала ready. Утверждение 2.5а выполняется на тракте 2.5(i). Для первого утверждения req, в цикле 1, четыре утверждения ready происходят немедленно в следующих циклах. Для второго утверждения req, в цикле 7, четыре утверждения ready не происходят немедленно и не происходят последовательно - они распространяются через семь циклов, пресекаясь с циклами, в которых ready не подтвержден. Однако, отметим,что в обоих случаях, сигнал last_ready утверждается на четвертом утверждении ready, таким образом утверждение 2.5a выполняется в тракте 2.5(i).

Psl fig 02.5.png
(i) Утверждение 2.5a выполняется 
assert always (req ->                (2.5a)
   next event(ready)[4](last ready));
Рис. 2.5: next event[n]


Как и с next_a[i:j] и next_e[i:j], оператор next_event также появляется в форме, которая позволяет выражать весь диапазон следующих циклов, или наличие будущего цикла в этом диапазоне. Форма next_event_a(b)[i:j](f) показывает, что мы ожидаем выполнения f на всех i-х через j-е вхождения b. Например, утверждение 2.6a показывает, что когда мы видим запрос на чтение (утверждение сигнала read_request) с тэгом эквивалентным i, далее на следующих четырех передачах данных (утверждение сигнала data), мы ожидаем увидеть тэг i. Утверждение 2.6а использует конструкцию forall, которую мы рассмотрим в деталях позже. Сейчас достаточно сказать, что утверждение 2.6а показывает требование, что должно выполняться для всех возможных значениях сигнала tag[2:0]. Утверждение 2.6а выполняется в тракте 2.6(i), потому что после первого утверждения сигнала read_request, где значение tag[2:0] 4, значение tag[2:0], также, 4 на четырех следующих утверждениях сигнала data (в циклах 5, 9, 10 и 11). Более того, на втором утверждении сигнала read_request, где tag[2:0] имеет значение 5, значение tag[2:0], также, 5 на следующих четырех утверждениях сигнала data (циклы с 17 по 20).

Для того, чтобы указать, что мы ожидаем чего-либо в одном из следующих циклов с i-го по j-й, мы можем использовать оператор next_event_e(b)[i:j](f), который показывает, что мы ожидаем выполнения f в одном из циклов, с i-го по j-й, вхождения b. Например, рассмотри опять утверждение 2.4a. Оно требует того, что когда бы ни приходил запрос высокого приоритета, следующим должен обработаться запрос с высоким приоритетом. Предположим вместо этого, что мы требуем, чтобы один из следующих двух грантов был для запроса с высоким приоритетом. Мы можем выразить это, используя утверждение 2.7a. Утверждение 2.7a выполняется в тракте 2.7(i), потому что всегда, когда сигнал high_pri_req утверждается, сигнал high_pri_ack утверждается на одном из следующих двух утверждений gnt.

Синтаксис спецификации диапазона для всех операторов, включая тех, которые мы еще не рассматривали, зависит от фундаментального языка. В вариантах Verilog, SystemVerilog и SystemC, это код [i:j]. Для VHDL - это код [i to j]. Для GDL это - [i..j].

Psl fig 02.6.png
(i) Утверждение 2.6a выполняется 
assert forall i in {0:7}:                      (2.6a)
   always ((read_request && tag[2:0]==i) ->
      next_event_a(data)[1:4](tag[2:0]==i));
Рис. 2.6 next_event a[i:j]

2.4 Операторы until и before

Psl fig 02.7.png
(i) Утверждение 2.7a выполняется 
assert always (high_pri_req ->                 (2.7a)
   next_event_e(gnt)[1:2](high_pri_ack));
Рис. 2.7: next_event e[i:j]

Оператор until предоставляет другой путь движения вперед, здесь накладываются требования на циклы, в которые мы движемся. Например, утверждение 2.8а показывает, что когда бы сигнал req не был утвержден, далее, начиная со следующего цикла, сигнал busy должен быть утвержден до тех пор, пока не утвердиться сигнал done. Утверждение 2.8а требует, чтобы busy был утвержден до, но необязательно включая, цикла, в котором утверждается done. Для включения этого цикла, используется оператор until_. Подчеркивание (_) служит для того, чтобы указать дополнительный цикл, для которого мы требуем, чтобы busy оставался утвержденным, таким образом утверждение 2.8b показывает, что кода бы сигнал req не утверждался, далее, начиная со следующего цикла, busy должен быть утвержден, и должен оставаться в таком состоянии до цикла, в котором утверждается done, включительно. Например, утверждение 2.8а выполняется на тракте 2.8(i), а утверждение 2.8b нет, потому что busyне утверждается в циклах 4 и 10. Оба утверждения 2.8a и 2.8b выполняются на тракте 2.8(ii): утверждение 2.8a не запрещает утверждения сигнала busy в циклах 4 и 10 - это просто не требуется.

Если сигнал done утверждается на следующем цикле после утверждения req, утверждение 2.8a не требует, чтобы сигнал busy, в принципе, утверждался, в отличие от утверждения 2.8b. То есть, утверждение 2.8а выполняется на тракте 2.8(iii) - факт того, что done утверждается немедленно после утверждения req, не оставляет циклов для утверждения busy. Утверждение 2.8b не выполняется в тракте 2.8(iii), из-за пропущенного утверждения busy в цикле, в котором утверждается done.

Psl fig 02.8.png 
assert always (req -> next (busy until done));           (2.8a)
assert always (req -> next(busy until_ done));           (2.8b)
Рис. 2.8: Операторы until и until_

Семейство операторов before предоставляет легкий путь для показания требований, чтобы некоторый сигнал утверждался перед каким-либо другим сигналом. Например, предположим, что у нас есть импульсный сигнал req, и мы имеем требование, что перед тем, как мы сможем сделать второй запрос, первый должен быть определен. Мы можем выразить это в PSL используя утверждение 2.9а. Нам нужен оператор next для передвижения на один цикл вперед, таким образом req в (ack before req) точно будет ссылаться на другие req, а не на тот, который был только что. Чтобы это понять, исследуем недостаточную версию этой спецификации. Рассматривая утверждение 2.9b. Оно требует, чтобы (ack before req) выполнялось на каждом цикле, в котором выполняется req. Например, цикл 1 тракта 2.9(i). Сигнал req утверждается. Поэтому, (ack before req) должен утвердиться в цикле 1. Однако, этого не происходит, потому что, начав с первого цикла и следуя далее, изначально мы увидим утверждения сигнала req (в цикле 1), и только после этого утверждение сигнала ack (в цикле 3) - таким образом req утверждается перед ack, а не наоборот. Утверждение 2.9а, с другой стороны, показывает, что мы хотим: в цикле 1, например, мы требуем выполнения next (ack before req). Поэтому, мы требуем, чтобы (ack before req) выполнлся на цикле 2. Начиная с цикла 2 и двигаясь вперед, изначально мы увидим утверждение ack (на цикле 3), и только после этого утверждение req (в цикле 6).

Psl fig 02.9.png 
assert always (req -> next (ack before req)); (2.9a)
assert always (req -> (ack before req)); (2.9b)
assert always (req -> next (ack before_ req)); (2.9c)
assert always (req -> (ack || next (ack before req))); (2.9d)
Рис. 2.9 Операторы before и before_

Оператор before требует, чтобы первый операнд выполнялся строго перед вторым. Для того, чтобы показать, что что-то должно выполниться перед или в том же цикле, как и что-либо иное, используется оператор before_. Подчеркивание (_) предназначено для представления цикла, в котором мы допускаем прекрытие между левой и правой сторонами. Например, для того чтобы показать, что поведениее соответствует тем, которые показаны в тракте 2.9(i) и в тракте Trace 2.9(ii), используется утверждение 2.9с.

Что если утверждению ack позволенно выполниться не вместе со следующим утверждением req, но вместе с установленным запросом? Другими словами, что если в дополнение к поведению, показаному в тракте 2.9(i), мы хотим допустить поведение показанное в тракте 2.9(iii)? Как было отмечно ранее, утверждение 2.9b это не ответ. Скорее, мы напишем код утверждения 2.9d.

2.5 Оператор eventually!

Оператор eventually! позволяет показать, что что-либо должно произойти в будущем, без конкретного уточнения когда. Например, утверждение 2.10а показывает, что каждый запрос (утверждение req) должен следовать в то же время, что и установленный (assertion of ack). Нету ничего в утверждении 2.10а, чтобы предотвратить единичного установления из удовлетворяющих требования для множественных запросов, таким образом утверждение 2.10а выполняется на тракте 2.10(i). Мы проверили этот вопрос спецификации взаимно однозначных соответствий между сигналами в разделе 13.4.2.

Восклицательный знак (!) в операторе eventually! показывает, что это сильный оператор. Обсуждения сильных и слабых оператров пойдет в главе 4.

Psl fig 02.10.png
(i) Утверждение 2.10a выполняется 
assert always (req -> eventually! ack);       (2.10a)
Рис. 2.10: Оператор eventually!
Источник — «http://simhard.com/wiki/index.php?title=PSL/A_Practical_Introduction_to_PSL/Basic_Temporal_Properties/ru&oldid=3273»