PSL/A Practical Introduction to PSL/Some Philosophy/ru — различия между версиями
Valentin (обсуждение | вклад) (→3.3 Designs and traces) |
Valentin (обсуждение | вклад) (→3.4 Current cycle, sub-traces, and modularity) |
||
| Строка 95: | Строка 95: | ||
Другой подход, используется дополнительным ветвлением расширения, используется дерево структуры, которое представляет несколько путей. Этот подход подходить только для формальной верификации, и, очень кратко, затрагивается в главе 11. | Другой подход, используется дополнительным ветвлением расширения, используется дерево структуры, которое представляет несколько путей. Этот подход подходить только для формальной верификации, и, очень кратко, затрагивается в главе 11. | ||
| − | === 3.4 | + | === 3.4 Текущий цикл, субтракты, модульность === |
| + | <!-- | ||
When a PSL property composed of two or more sub-properties is checked on | When a PSL property composed of two or more sub-properties is checked on | ||
a trace, it is sometimes necessary to decide the meaning of the sub-properties | a trace, it is sometimes necessary to decide the meaning of the sub-properties | ||
on a sub-trace. The ''current cycle'' is the name we give to the first cycle of a | on a sub-trace. The ''current cycle'' is the name we give to the first cycle of a | ||
trace or a sub-trace on which we are evaluating a property or a sub-property. | trace or a sub-trace on which we are evaluating a property or a sub-property. | ||
| + | --> | ||
| + | Когда свойство PSL состоит из двух и больше под-свойств, оно проверяется на тракте, иногда это необходимо для понятия значения под-свойств на субтрактах. ''Текущий цикл'' это имя мы дали первому циклу тракта или субтракта, на котором мы оцениваем свойство или под-свойство. | ||
| + | <!-- | ||
Assuming that the cycles of a trace are numbered starting from 0, the | Assuming that the cycles of a trace are numbered starting from 0, the | ||
current cycle of an assertion is 0. The current cycle of a sub-property of some | current cycle of an assertion is 0. The current cycle of a sub-property of some | ||
| Строка 112: | Строка 116: | ||
which has a current cycle that corresponds either to the current cycle or to | which has a current cycle that corresponds either to the current cycle or to | ||
some future cycle, etc. | some future cycle, etc. | ||
| + | --> | ||
| + | Предполагая, что циклы тракта нумеруются, начиная с 0, текущий цикл утверждения - 0. Текущий цикл под-свойства, какого-нибудь вшитого свойства, зависит от своего использования во вшитом свойстве. Операнды Булевого оператора получают такой же текущий цикл, как и родительское свойство. Операнды временных операторов получают текущий цикл, который связан с текущим циклом родительского свойства, в случаи, если это указано временным оператором. Например, оператор next увеличивает текущий цикл на один, оператор always создает “несколько экземпляров” под-свойства, каждый из которых получает текущий цикл, который соответствует текущему циклу или некоторому будущему циклу. | ||
| + | <!-- | ||
NOTE: It is very important to understand that the term “multiple instances” | NOTE: It is very important to understand that the term “multiple instances” | ||
is intended to convey an intuition which is useful in understanding | is intended to convey an intuition which is useful in understanding | ||
| Строка 125: | Строка 132: | ||
<code>always</code> operator works, and a naive and inefficient implementation may well | <code>always</code> operator works, and a naive and inefficient implementation may well | ||
generate multiple instances of a checker or of a process. | generate multiple instances of a checker or of a process. | ||
| + | --> | ||
| + | Примечание: Очень важно понять, что термин “несколько экземпляров” предназначен для смысла, который используется для понимания оператора <code>always</code>. ''Не'' предназначем показать, что каждый экземпляр существует; причем это не значит, что программе реализации PSL надо создать много экземпляров проверки утверждения, порождение нескольких экземпляров процесса или в любом другом случаи слова “несколько экземпляров” означают актуальные экземпляры чего-либо. Наоборот, существуют множество эффективных реализаций PSL, в которых оператор <code>always</code> не создает нескольких экземпляров. Термин “несколько экземпляров” - это хороший способ усилить понятие того, как работает оператор <code>always</code>, наивная и неэффективная реализация могжет также реализовывать несколько экземпляров проверки или процесса. | ||
| + | <!-- | ||
Getting back to our main point, consider the assertion <code>assert always (a -> next b);</code>. The current cycle of <code>always (a -> next b)</code> is 0. Whether or | Getting back to our main point, consider the assertion <code>assert always (a -> next b);</code>. The current cycle of <code>always (a -> next b)</code> is 0. Whether or | ||
not <code>always (a -> next b)</code> holds at cycle 0 depends on whether or not the | not <code>always (a -> next b)</code> holds at cycle 0 depends on whether or not the | ||
| Строка 134: | Строка 144: | ||
and next b with a current cycle of ''N'', which means that we need to evaluate | and next b with a current cycle of ''N'', which means that we need to evaluate | ||
sub-property b with a current cycle of ''N'' + 1. | sub-property b with a current cycle of ''N'' + 1. | ||
| + | --> | ||
| + | Возвращаясь к нашему основному пункту рассмотрения, рассмотрим утверждение <code>assert always (a -> next b);</code>. Текущий цикл <code>always (a -> next b)</code> - 0. Выполнение <code>always (a -> next b)</code> в цикле 0, зависит от выполнения под-свойства <code>(a -> next b)</code> в каждом цикле с нулевого. Текущий цикл для частной оценки под-свойства <code>(a -> next b)</code> будет некий цикл ''N''. В итоге, для того, чтобы определить действительно ли под-свойство <code>(a -> next b)</code> выполняется в цикле ''N'', мы должны оценить под-свойство a и следующий b с текущим циклом ''N'', что значит, что нам надо оценить под-свойство b с текущим циклом ''N'' + 1. | ||
| + | <!-- | ||
To make the discussion more concrete, let’s consider our assertion, Assertion | To make the discussion more concrete, let’s consider our assertion, Assertion | ||
3.1a, on Trace 3.1(i). Signal a holds in cycles 4 and 8. Signal <code>b</code> holds in | 3.1a, on Trace 3.1(i). Signal a holds in cycles 4 and 8. Signal <code>b</code> holds in | ||
| Строка 147: | Строка 160: | ||
3.1a does not hold on Trace 3.1(i) (because it does not hold on cycle 0 – | 3.1a does not hold on Trace 3.1(i) (because it does not hold on cycle 0 – | ||
the first cycle of the trace). | the first cycle of the trace). | ||
| − | + | --> | |
| + | Для того чтобы сделать обсуждения конкретней, давайте рассмотрим наше утверждение, утверждение 3.1а на тракте 3.1(i). Сигнал а выполняется в циклах 4 и 8. Сигнал b выполняется в цикле 5, <code>next b</code> выполняется в цикле 4. Это показано в тракте 3.1(ii), аннотированная версия тракта 3.1(i). В то время, как а выполняется в циклах 4 и 8, и <code>next b</code> выполняется в цикле 4, мы получаем, что <code>(a -> next b)</code> выполняется во всех циклах, а цикл 8,как показано на тракте 3.1(ii). (Запомните, что в других частях по умолчанию справедливо, что <code>(a -> next b)</code> выполняется во всех циклах, где <code>a</code> не выполняется, и в дополнение во всех циклах где <code>a</code> выполняется и <code>next b</code> тоже.) Все свойство <code>always (a -> next b)</code> выполняется в циклах 9, 10, 11, 12, 13 (потому что в этих циклах <code>(a -> next b)</code> выполняется “сейчас” и во всех следующих циклах). Таким образом, утверждение 3.1a не выполняется на тракте 3.1(i) (потому что оно не выполняется в цикле 0 - первом цикле тракта). | ||
{| align=center | {| align=center | ||
| Строка 156: | Строка 170: | ||
</pre> | </pre> | ||
|- | |- | ||
| − | ! | + | ! Рис. 3.1: Конкретный пример |
|} | |} | ||
| + | <!-- | ||
The above explanation seems straightforward. However, the idea of modularity | The above explanation seems straightforward. However, the idea of modularity | ||
hides some subtle points – for example, that the value of the property | hides some subtle points – for example, that the value of the property | ||
| Строка 166: | Строка 181: | ||
that <code>a</code> should hold in every cycle, you must use the <code>always</code> operator, as in | that <code>a</code> should hold in every cycle, you must use the <code>always</code> operator, as in | ||
Assertion 3.2b. Assertion 3.2b does not hold on Trace 3.2(i). | Assertion 3.2b. Assertion 3.2b does not hold on Trace 3.2(i). | ||
| + | --> | ||
| + | Приведенное выше описание кажется простым. Однако, идея модульности скрывает некоторые тонкие моменты, например, что значение свойства <code>a</code> зависит только от текущего цикла. Таким образом, утверждение 3.2а выполняется нна тракте 3.2(i), потому что сигнал <code>a</code> выполняется в цикле 0. Если вы хотите выразить тот факт, что <code>a</code> должен выполняться в каждом цикле, вы должны использовать оператор <code>always</code>, как в утверждении 3.2b. Утверждение 3.2b не выполняется на тракте 3.2(i). | ||
| + | <!-- | ||
Another subtle point is that a property can hold on a suffix of a trace | Another subtle point is that a property can hold on a suffix of a trace | ||
without holding on the trace itself. Thus, the property <code>always a</code> holds on | without holding on the trace itself. Thus, the property <code>always a</code> holds on | ||
| Строка 173: | Строка 191: | ||
other property. For example, Assertion 3.2c holds on Trace 3.2(i) because the | other property. For example, Assertion 3.2c holds on Trace 3.2(i) because the | ||
property <code>always a</code> holds on the 12<sup>''th''</sup> next cycle. | property <code>always a</code> holds on the 12<sup>''th''</sup> next cycle. | ||
| + | --> | ||
| + | Другой тонкий момент, что свойство может выполняться в суффиксе тракта,а не на самом тракте. Таким образом, свойство <code>always a</code> выполняется на субтракте тракта 3.2(i), начиная с циклов 12, 13, 14. Это будет важно, если мы используем свойство <code>always a</code>, как под-свойство какого-либо друо свойства. Например, утверждение 3.2c выполняется на тракте 3.2(i), потому что свойство <code>always a</code> выполняется на 12<sup>''ти''</sup> следующих циклах. | ||
Finally, the cycles involved in calculating the left-hand side of a logical | Finally, the cycles involved in calculating the left-hand side of a logical | ||
| Строка 236: | Строка 256: | ||
with those involved in calculating the right-hand side of the same operator, | with those involved in calculating the right-hand side of the same operator, | ||
you have not written a property that is in the simple subset. | you have not written a property that is in the simple subset. | ||
| − | |||
=== 3.5 Reporting a failure === | === 3.5 Reporting a failure === | ||
Версия 13:29, 25 ноября 2013
- 1. Introduction (en)
- 2. Basic Temporal Properties (en)
- 3. Some Philosophy (en)
- 4. Weak vs. Strong Temporal Operators (en)
- 5. SERE Style (en)
Содержание |
Немного философии
Мы рассмотрели немного основ PSL и получили ощущение того, как используется. Перед тем как продолжить, мы обсудим некоторые концепции в корне PSL.
3.1 Утверждения против свойств
Как мы уже видели, утверждения PSL состоят из ключевого слова assert плюс свойства PSL для утверждения, разделенных точкой с запятой. Например, в утверждении assert always (a -> next b);, свойство - always (a -> next b). Свойство выполняется или не выполняется в данном тракте. Утверждение, с другой стороны, указывает программе верификации, что свойство было утверждено, и требуется выполнение. Далее в книге мы будем внимательно рассматривать отличия между свойствами, которые просто описывают поведения, и утверждения,которые устанавливают требования. Например, мы можем сказать, что утверждение assert always (a -> next b); требует, чтобы когда бы сигнал a не утверждался, сигнал b должен будет утвердиться в следующем цикле. Однако, мы никогда не скажем такого о свойстве always (a -> next b), по двум причинам. Первая - потому что если свойство используется в предположении (assume always (a -> next b);), то нету никаких требований. Вторая - потому что свойство может использоваться, как под-свойство более сложного свойства, и если так, то не может исходить требований от него самого.
3.2 Понятие времени
Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении Java или (моделирования) VHDL, понятие времени не нуждается в определении - утверждение проверяется всякий раз, когда заявление, содержащее утверждение выполняется. Для более сложных утверждений PSL, которые, во-первых, находяться отдельно от кода (таким образом понятие “исполнение” чужое для них), и во-вторых охватывает множество шагов во времени, понятию времени необходими уелить больше внимания.
PSL предполагает, что время дискретно, таким образом, время состоит из последовательности оцененных циклов. Значение свойства PSL определенно по отношению к такой последовательности циклов. В этой книге, мы будем называть такую последовательность циклов трактом.
PSL не указывает как идет время - т.е. не указывает, как данная последовательность циклов получается из проекта под верификацией. Это значит, что последовательность циклов, для двух программ верификации, необязательно совпадет. Например, симулятор, базирующийся на циклах видит последовательность значений сигнала подсчитанную цикл за циклом, в то время, как симулятор базирующийся на изменениях, запущенный для этого же проекта, видит более детализированную последовательность значений сигнала.
Тем не менее, существует путь гарантировать, что значение свойства PSL не влияет на степень детализации времени, с точки зрения программ верификации. Свойства PSL могут быть модифицированы, используя временное выражение для того, чтобы показать, что время должно быть получено во временных циклах временного выражения. В случаи временного свойства, результат программы базирующейся на циклах должен быть такой же, как и для программы базирующейся на изменениях. PSL допускает спецификацию времени по-умолчанию, таким образом, что время не должно быть упомянуто отдельно для каждого свойства. Далее в этой книге мы предполагаем однократный тактовый проект под модель, базирующуюся на циклах, таким образом в большинстве примеров опущены явные упоминания о времени.
3.3 Проекты и тракты
Цель свойства PSL описать желаемое поведение проекта. Как правило, это удобно для проверки отдельных трактов проекта. Фундаментальный язык, который используется в данной книге, применяет данный подход, и таким образом, на протяжении данной книги мы будем интересоваться выполняется ли некое свойство в этом тракте или нет. Фундаментальный язык подходит, как для статической (формальной), так и для динамической (базирующейся на моделировании) верификации.
Другой подход, используется дополнительным ветвлением расширения, используется дерево структуры, которое представляет несколько путей. Этот подход подходить только для формальной верификации, и, очень кратко, затрагивается в главе 11.
3.4 Текущий цикл, субтракты, модульность
Когда свойство PSL состоит из двух и больше под-свойств, оно проверяется на тракте, иногда это необходимо для понятия значения под-свойств на субтрактах. Текущий цикл это имя мы дали первому циклу тракта или субтракта, на котором мы оцениваем свойство или под-свойство.
Предполагая, что циклы тракта нумеруются, начиная с 0, текущий цикл утверждения - 0. Текущий цикл под-свойства, какого-нибудь вшитого свойства, зависит от своего использования во вшитом свойстве. Операнды Булевого оператора получают такой же текущий цикл, как и родительское свойство. Операнды временных операторов получают текущий цикл, который связан с текущим циклом родительского свойства, в случаи, если это указано временным оператором. Например, оператор next увеличивает текущий цикл на один, оператор always создает “несколько экземпляров” под-свойства, каждый из которых получает текущий цикл, который соответствует текущему циклу или некоторому будущему циклу.
Примечание: Очень важно понять, что термин “несколько экземпляров” предназначен для смысла, который используется для понимания оператора always. Не предназначем показать, что каждый экземпляр существует; причем это не значит, что программе реализации PSL надо создать много экземпляров проверки утверждения, порождение нескольких экземпляров процесса или в любом другом случаи слова “несколько экземпляров” означают актуальные экземпляры чего-либо. Наоборот, существуют множество эффективных реализаций PSL, в которых оператор always не создает нескольких экземпляров. Термин “несколько экземпляров” - это хороший способ усилить понятие того, как работает оператор always, наивная и неэффективная реализация могжет также реализовывать несколько экземпляров проверки или процесса.
Возвращаясь к нашему основному пункту рассмотрения, рассмотрим утверждение assert always (a -> next b);. Текущий цикл always (a -> next b) - 0. Выполнение always (a -> next b) в цикле 0, зависит от выполнения под-свойства (a -> next b) в каждом цикле с нулевого. Текущий цикл для частной оценки под-свойства (a -> next b) будет некий цикл N. В итоге, для того, чтобы определить действительно ли под-свойство (a -> next b) выполняется в цикле N, мы должны оценить под-свойство a и следующий b с текущим циклом N, что значит, что нам надо оценить под-свойство b с текущим циклом N + 1.
Для того чтобы сделать обсуждения конкретней, давайте рассмотрим наше утверждение, утверждение 3.1а на тракте 3.1(i). Сигнал а выполняется в циклах 4 и 8. Сигнал b выполняется в цикле 5, next b выполняется в цикле 4. Это показано в тракте 3.1(ii), аннотированная версия тракта 3.1(i). В то время, как а выполняется в циклах 4 и 8, и next b выполняется в цикле 4, мы получаем, что (a -> next b) выполняется во всех циклах, а цикл 8,как показано на тракте 3.1(ii). (Запомните, что в других частях по умолчанию справедливо, что (a -> next b) выполняется во всех циклах, где a не выполняется, и в дополнение во всех циклах где a выполняется и next b тоже.) Все свойство always (a -> next b) выполняется в циклах 9, 10, 11, 12, 13 (потому что в этих циклах (a -> next b) выполняется “сейчас” и во всех следующих циклах). Таким образом, утверждение 3.1a не выполняется на тракте 3.1(i) (потому что оно не выполняется в цикле 0 - первом цикле тракта).
|
|---|
assert always (a -> next b); (3.1a) |
| Рис. 3.1: Конкретный пример |
Приведенное выше описание кажется простым. Однако, идея модульности скрывает некоторые тонкие моменты, например, что значение свойства a зависит только от текущего цикла. Таким образом, утверждение 3.2а выполняется нна тракте 3.2(i), потому что сигнал a выполняется в цикле 0. Если вы хотите выразить тот факт, что a должен выполняться в каждом цикле, вы должны использовать оператор always, как в утверждении 3.2b. Утверждение 3.2b не выполняется на тракте 3.2(i).
Другой тонкий момент, что свойство может выполняться в суффиксе тракта,а не на самом тракте. Таким образом, свойство always a выполняется на субтракте тракта 3.2(i), начиная с циклов 12, 13, 14. Это будет важно, если мы используем свойство always a, как под-свойство какого-либо друо свойства. Например, утверждение 3.2c выполняется на тракте 3.2(i), потому что свойство always a выполняется на 12ти следующих циклах.
Finally, the cycles involved in calculating the left-hand side of a logical
implication may overlap those involved in calculating the right-hand side of
a logical implication. For example, consider Assertion 3.3a on Trace 3.3(i).
Assertion 3.3a holds on Trace 3.3(i) because the sub-property (a && next[6] (b)) -> (c && next[2] (d))
holds at all cycles. It holds at cycle 2 because
the left-hand side (a && next[6] (b)) holds and in addition the right-hand
side (c && next[2] (d)) holds. It holds at all other cycles because if the
“if” part of a logical implication does not hold, then the “else” part defaults
to true.
|
|---|
| (i) Assertions 3.2a and 3.2c hold, but 3.2b does not |
assert a; (3.2a) assert always a; (3.2b) assert next[12] (always a); (3.2c) |
| Fig. 3.2: The importance of the always operator |
|
|---|
| (i) An illustration of the overlap between the left- and right-hand sides of Assertion 3.3a. Assertion 3.3a holds. |
assert always ((a && next[6](b)) -> (c && next[2](d))); (3.3a) |
| Fig. 3.3: The current cycle |
Previously, for example in examining Assertions 2.2a and 2.3b, we have
seen cases where there is an overlap between the cycles involved in satisfying
two different occurrences of the left-hand side of a logical implication. These
overlaps are caused by the presence of the always operator in the property.
If we remove the always operator, the issue of overlap disappears from Assertions
2.2a and 2.3b. The overlap of Assertion 3.3a is different from the overlap
of Assertions 2.2a and 2.3b in a very important way: Assertion 3.3a is written
in such a way that the cycles involved in calculating the left-hand side of the
logical implication overlap those involved in calculating the right-hand side of
the logical implication: calculating the “if” part of the logical implication involves
examining the current cycle and also “looking ahead” six cycles, while
calculating the “then” part of the logical implication involves examining the
current cycle and also “looking ahead” two cycles. Thus the overlap results
from the logical implication itself. This style of PSL property is usually very
confusing to new users of PSL, and indeed it is not an intuitive way to use
the language. For this reason, such properties are not recommended, and the
simple subset of PSL restricts the language in such a way that such properties
are not allowed. We discuss the simple subset in more detail later. For now,
remember that if you have written a property in which the cycles involved in
calculating the left-hand side of an operator overlap for more than one cycle
with those involved in calculating the right-hand side of the same operator,
you have not written a property that is in the simple subset.
3.5 Reporting a failure
Consider Assertion 3.4a on the traces shown in Figure 3.4. Obviously, Assertion
3.4a does not hold on them. Now consider four different verification tools,
each of which reports the failure of Assertion 3.4a as indicated by the signal
called “failure” in Traces 3.4(i), 3.4(ii), 3.4(iii) and 3.4(iv). Tool 1 reports a
failure at cycle 4, the earliest that it can be detected. Tool 2 reports a failure
at cycle 4, but also at cycle 7, when b is asserted for a second time. Tool 3
reports a failure at the end of the trace, and Tool 4 reports a failure at cycle
1, when a is asserted.
Which tool is correct? The answer is that they all are. PSL defines whether or not a property holds on a trace – that is all. It says nothing about when a tool, dynamic or static, should report on the results of the analysis. Thus, there is no meaning in asking whether Tool 1, 2, 3 or 4 is correct. All of them indicate that the property fails on the trace, so all are correct. The failure indications shown along the trace can be thought of as debugging aids, hinting to the user where to look along the trace for the failure. As far as PSL is concerned, as long as a tool indicates correctly whether or not a property holds on a trace, it has done its job.
|
|---|
assert always (a -> never b); (3.4a) |
| Fig. 3.4: Four different tools reporting the failure of Assertion 3.4a on the same trace |
