PSL/A Practical Introduction to PSL/Some Philosophy/ru — различия между версиями
Valentin (обсуждение | вклад) (→3.2 The notion of time) |
Valentin (обсуждение | вклад) (→3.5 Reporting a failure) |
||
| (не показаны 5 промежуточных версий 1 участника) | |||
| Строка 41: | Строка 41: | ||
must be given more consideration. | must be given more consideration. | ||
--> | --> | ||
| − | Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении Java или (моделирования) VHDL, понятие времени не нуждается в определении - утверждение проверяется всякий раз, когда заявление, содержащее утверждение выполняется. | + | Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении Java или (моделирования) VHDL, понятие времени не нуждается в определении - утверждение проверяется всякий раз, когда заявление, содержащее утверждение выполняется. Для более сложных утверждений PSL, которые, во-первых, находяться отдельно от кода (таким образом понятие “исполнение” чужое для них), и во-вторых охватывает множество шагов во времени, понятию времени необходими уелить больше внимания. |
| + | <!-- | ||
PSL assumes that time is discrete, that is, that time consists of a sequence | PSL assumes that time is discrete, that is, that time consists of a sequence | ||
of evaluation cycles. The meaning of a PSL property is defined relative to such | of evaluation cycles. The meaning of a PSL property is defined relative to such | ||
a sequence of cycles. In this book, we will refer to such a sequence of cycles | a sequence of cycles. In this book, we will refer to such a sequence of cycles | ||
as a ''trace''. | as a ''trace''. | ||
| + | --> | ||
| + | PSL предполагает, что время дискретно, таким образом, время состоит из последовательности оцененных циклов. Значение свойства PSL определенно по отношению к такой последовательности циклов. В этой книге, мы будем называть такую последовательность циклов ''трактом''. | ||
| + | <!-- | ||
PSL does not dictate how time ticks – that is, it does not dictate how such | PSL does not dictate how time ticks – that is, it does not dictate how such | ||
a sequence of cycles is extracted from a design under verification. This means | a sequence of cycles is extracted from a design under verification. This means | ||
| Строка 54: | Строка 58: | ||
calculated cycle-by-cycle, while an event-based simulator running on the same | calculated cycle-by-cycle, while an event-based simulator running on the same | ||
design sees a more detailed sequence of signal values. | design sees a more detailed sequence of signal values. | ||
| + | --> | ||
| + | PSL не указывает как идет время - т.е. не указывает, как данная последовательность циклов получается из проекта под верификацией. Это значит, что последовательность циклов, для двух программ верификации, необязательно совпадет. Например, симулятор, базирующийся на циклах видит последовательность значений сигнала подсчитанную цикл за циклом, в то время, как симулятор базирующийся на изменениях, запущенный для этого же проекта, видит более детализированную последовательность значений сигнала. | ||
| + | <!-- | ||
Nevertheless, there is a way to ensure that the meaning of a PSL property | Nevertheless, there is a way to ensure that the meaning of a PSL property | ||
is not affected by the granularity of time as seen by the verification tool. PSL | is not affected by the granularity of time as seen by the verification tool. PSL | ||
| Строка 65: | Строка 72: | ||
the cycle-based model, and thus most examples omit the explicit mention of | the cycle-based model, and thus most examples omit the explicit mention of | ||
the clock. Clocks are discussed in detail in Chapters 6 and 14. | the clock. Clocks are discussed in detail in Chapters 6 and 14. | ||
| + | --> | ||
| + | Тем не менее, существует путь гарантировать, что значение свойства PSL не влияет на степень детализации времени, с точки зрения программ верификации. Свойства PSL могут быть модифицированы, используя ''временное выражение'' для того, чтобы показать, что время должно быть получено во временных циклах временного выражения. В случаи временного свойства, результат программы базирующейся на циклах должен быть такой же, как и для программы базирующейся на изменениях. PSL допускает спецификацию ''времени по-умолчанию'', таким образом, что время не должно быть упомянуто отдельно для каждого свойства. Далее в этой книге мы предполагаем однократный тактовый проект под модель, базирующуюся на циклах, таким образом в большинстве примеров опущены явные упоминания о времени. | ||
| − | ===3.3 | + | ===3.3 Проекты и тракты === |
| + | <!-- | ||
The purpose of a PSL property is to describe the desired behavior of a design. | The purpose of a PSL property is to describe the desired behavior of a design. | ||
In order to do so, it is usually convenient to examine individual traces of that | In order to do so, it is usually convenient to examine individual traces of that | ||
| Строка 75: | Строка 85: | ||
The Foundation Language is suitable for both static (formal) and dynamic | The Foundation Language is suitable for both static (formal) and dynamic | ||
(simulation-based) verification. | (simulation-based) verification. | ||
| + | --> | ||
| + | Цель свойства PSL описать желаемое поведение проекта. Как правило, это удобно для проверки отдельных трактов проекта. Фундаментальный язык, который используется в данной книге, применяет данный подход, и таким образом, на протяжении данной книги мы будем интересоваться выполняется ли некое свойство в этом тракте или нет. Фундаментальный язык подходит, как для статической (формальной), так и для динамической (базирующейся на моделировании) верификации. | ||
| + | <!-- | ||
Another approach, used by the Optional Branching Extension (OBE), uses | Another approach, used by the Optional Branching Extension (OBE), uses | ||
a tree structure that represents multiple paths. This approach is applicable | a tree structure that represents multiple paths. This approach is applicable | ||
only to formal verification, and is touched on very briefly in Chapter 11. | only to formal verification, and is touched on very briefly in Chapter 11. | ||
| + | --> | ||
| + | Другой подход, используется дополнительным ветвлением расширения, используется дерево структуры, которое представляет несколько путей. Этот подход подходить только для формальной верификации, и, очень кратко, затрагивается в главе 11. | ||
| + | === 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 | ||
| Строка 98: | Строка 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 | ||
| Строка 111: | Строка 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 | ||
| Строка 120: | Строка 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 | ||
| Строка 133: | Строка 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 | ||
| Строка 142: | Строка 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 | ||
| Строка 152: | Строка 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 | ||
| Строка 159: | Строка 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 | ||
implication may overlap those involved in calculating the right-hand side of | implication may overlap those involved in calculating the right-hand side of | ||
| Строка 169: | Строка 204: | ||
“if” part of a logical implication does not hold, then the “else” part defaults | “if” part of a logical implication does not hold, then the “else” part defaults | ||
to true. | to true. | ||
| − | + | --> | |
| + | Последнее, циклы вовлеченные в в подсчет левой стороны логической импликации могут прекрываться с циклами вовлеченными в подсчет правой стороны логической импликации. Например, рассмотрим утверждение 3.3a на тракте 3.3(i). Утверждение 3.3a выполняется на тракте 3.3(i), потому что под-свойство <code>(a && next[6] (b)) -> (c && next[2] (d))</code> выполняется на всех циклах. Оно выполняется в цикле 2, потому что левая сторона <code>(a && next[6] (b))</code> выполняется и в дополнение правая сторона <code>(c && next[2] (d))</code>, тоже выполняется. Оно выполняется во всех других циклах, потому что, если часть “if” логического исполнения не выполняется, то по-умолчанию часть “else” принимает значение правда | ||
{| align=center | {| align=center | ||
! [[Файл:Psl fig3.2.png]] | ! [[Файл:Psl fig3.2.png]] | ||
|- | |- | ||
| − | !(i) | + | !(i) Утверждение 3.2a и 3.2c выполняются, но 3.2b нет |
|- | |- | ||
|<pre> | |<pre> | ||
| Строка 182: | Строка 218: | ||
</pre> | </pre> | ||
|- | |- | ||
| − | ! | + | ! Рис. 3.2: Важность оператора always |
|} | |} | ||
| Строка 189: | Строка 225: | ||
! [[Файл:Psl fig3.3.png]] | ! [[Файл:Psl fig3.3.png]] | ||
|- | |- | ||
| − | !(i) | + | !(i) Иллюстрация перекрытие левой и правой стороны <br /> |
| − | + | утверждение 3.3a. Утверждение 3.3a выполняется. | |
|- | |- | ||
|<pre> | |<pre> | ||
| Строка 196: | Строка 232: | ||
</pre> | </pre> | ||
|- | |- | ||
| − | ! | + | ! Рис. 3.3: Текущий цикл |
|} | |} | ||
| − | + | <!-- | |
Previously, for example in examining Assertions 2.2a and 2.3b, we have | 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 | seen cases where there is an overlap between the cycles involved in satisfying | ||
| Строка 222: | Строка 258: | ||
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. | ||
| + | --> | ||
| + | Предварительно, например в рассматриваемых утверждениях 2.2а и 2.3b, мы видели случаи, где были перекрытия между циклами вовлеченными в удовлетворение двух разных случаев левой стороны логической импликации. Эти перекрытия вызваны присутствием оператора <code>always</code> в свойстве. Если мы удалим этот оператор, вопрос перекрытия исчезнет из утверждений 2.2a и 2.3b. Перекрытие утверждения 3.3а отличается от перекрытия утверждений 2.2a и 2.3b, и это очень важно: утверждение 3.3a написано таким образом, что циклы вовлеченные в подсчет левой стороны логической импликации перекрываются с циклами правой логической импликации: подсчитывая часть “if” логической вовлекают рассматриваемый текущий цикл, а также “предстоящие” шесть циклов, в то время как подсчет части “then” логической импликации вовлекает рассматриваемый текущий цикл и также “предстоящие” два цикла. Таким образом,перекрытие появляется от самой логической импликации. Такой стиль PSL свойств, обычно, труден для новых пользователей PSL, и вообще это не интуитивный способ использования языка. Поэтому, такие свойства не рекомендуется использовать, и <code>простое подмножество</code> ограничений языка PSL не позволяет использование таких свойств. Мы обсудим простое подмножество в деталях поздней. На данный момент, запомните, что если вы написали свойство, в котором циклы вовлечены в подсчет левой стороны одного оператора перекрываются в течение более одного цикла с циклами вовлеченными для подсчета правой стороны того же оператора, то вы написали свойство не относящиеся к простому подмножеству. | ||
| + | === 3.5 Сообщение об ошибке === | ||
| − | + | <!-- | |
| − | + | ||
Consider Assertion 3.4a on the traces shown in Figure 3.4. Obviously, Assertion | 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, | 3.4a does not hold on them. Now consider four different verification tools, | ||
| Строка 234: | Строка 272: | ||
reports a failure at the end of the trace, and Tool 4 reports a failure at cycle | reports a failure at the end of the trace, and Tool 4 reports a failure at cycle | ||
1, when <code>a</code> is asserted. | 1, when <code>a</code> is asserted. | ||
| + | --> | ||
| + | Рассмотрим утверждение 3.4а на тракте, показаном на рисунке 3.4. Очевидно, утверждение 3.4a не выполняется на нем. Сейчас рассмотрим четыре разных вида инструментов верификации, каждый из которых, выдает сообщение об ошибке утверждения 3.4a, индикаций сигнала, называемого “failure” в трактах 3.4(i), 3.4(ii), 3.4(iii) и 3.4(iv). Инструмент 1 выдал сообщение об ошибке на цикле 4, наиболее ранний выриант,на котором это можно выявить. Инструмент 2 выдал сообщение на цикле 4, а также на цикле 7, когда <code>b</code> утверждается второй раз. Инструмент 3 выдал сообщение в конце тракта, и инструмент 4 выдал сообщение на цикле 11,когда утверждается <code>a</code>. | ||
| + | <!-- | ||
Which tool is correct? The answer is that they all are. PSL defines whether | 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 | or not a property holds on a trace – that is all. It says nothing about when | ||
| Строка 244: | Строка 285: | ||
is concerned, as long as a tool indicates correctly whether or not a property | is concerned, as long as a tool indicates correctly whether or not a property | ||
holds on a trace, it has done its job. | holds on a trace, it has done its job. | ||
| − | + | --> | |
| + | Какой инструмент сработал правильно? Правильный ответ - все они. PSL определяет выполняется ли свойство в тракте - вот и все. ничего не сказано о том, когда инструмент, динамический или статический, должен выдать сообщение по результатам анализов. Таким образом, нету смысла в вопросе - какой инструмент правильный? Все они показали, что свойство не выполняется на тракте, поэтому все они верны. Индикация ошибки показанная на все тракте может пониматься, как помощь для дебага, помогая пользователям понять,где находиться ошибка на тракте. Пока PSL показывает эти ошибки на трактах, он делает свою работу. | ||
{| align=center | {| align=center | ||
| Строка 253: | Строка 295: | ||
</pre> | </pre> | ||
|- | |- | ||
| − | ! | + | ! Рис. 3.4: Четыре инструмент,выдающих сообщение об ошибке утверждения 3.4a на одном и том же тракте |
|} | |} | ||
Текущая версия на 15:04, 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ти следующих циклах.
Последнее, циклы вовлеченные в в подсчет левой стороны логической импликации могут прекрываться с циклами вовлеченными в подсчет правой стороны логической импликации. Например, рассмотрим утверждение 3.3a на тракте 3.3(i). Утверждение 3.3a выполняется на тракте 3.3(i), потому что под-свойство (a && next[6] (b)) -> (c && next[2] (d)) выполняется на всех циклах. Оно выполняется в цикле 2, потому что левая сторона (a && next[6] (b)) выполняется и в дополнение правая сторона (c && next[2] (d)), тоже выполняется. Оно выполняется во всех других циклах, потому что, если часть “if” логического исполнения не выполняется, то по-умолчанию часть “else” принимает значение правда
|
|---|
| (i) Утверждение 3.2a и 3.2c выполняются, но 3.2b нет |
assert a; (3.2a) assert always a; (3.2b) assert next[12] (always a); (3.2c) |
| Рис. 3.2: Важность оператора always |
|
|---|
| (i) Иллюстрация перекрытие левой и правой стороны утверждение 3.3a. Утверждение 3.3a выполняется. |
assert always ((a && next[6](b)) -> (c && next[2](d))); (3.3a) |
| Рис. 3.3: Текущий цикл |
Предварительно, например в рассматриваемых утверждениях 2.2а и 2.3b, мы видели случаи, где были перекрытия между циклами вовлеченными в удовлетворение двух разных случаев левой стороны логической импликации. Эти перекрытия вызваны присутствием оператора always в свойстве. Если мы удалим этот оператор, вопрос перекрытия исчезнет из утверждений 2.2a и 2.3b. Перекрытие утверждения 3.3а отличается от перекрытия утверждений 2.2a и 2.3b, и это очень важно: утверждение 3.3a написано таким образом, что циклы вовлеченные в подсчет левой стороны логической импликации перекрываются с циклами правой логической импликации: подсчитывая часть “if” логической вовлекают рассматриваемый текущий цикл, а также “предстоящие” шесть циклов, в то время как подсчет части “then” логической импликации вовлекает рассматриваемый текущий цикл и также “предстоящие” два цикла. Таким образом,перекрытие появляется от самой логической импликации. Такой стиль PSL свойств, обычно, труден для новых пользователей PSL, и вообще это не интуитивный способ использования языка. Поэтому, такие свойства не рекомендуется использовать, и простое подмножество ограничений языка PSL не позволяет использование таких свойств. Мы обсудим простое подмножество в деталях поздней. На данный момент, запомните, что если вы написали свойство, в котором циклы вовлечены в подсчет левой стороны одного оператора перекрываются в течение более одного цикла с циклами вовлеченными для подсчета правой стороны того же оператора, то вы написали свойство не относящиеся к простому подмножеству.
3.5 Сообщение об ошибке
Рассмотрим утверждение 3.4а на тракте, показаном на рисунке 3.4. Очевидно, утверждение 3.4a не выполняется на нем. Сейчас рассмотрим четыре разных вида инструментов верификации, каждый из которых, выдает сообщение об ошибке утверждения 3.4a, индикаций сигнала, называемого “failure” в трактах 3.4(i), 3.4(ii), 3.4(iii) и 3.4(iv). Инструмент 1 выдал сообщение об ошибке на цикле 4, наиболее ранний выриант,на котором это можно выявить. Инструмент 2 выдал сообщение на цикле 4, а также на цикле 7, когда b утверждается второй раз. Инструмент 3 выдал сообщение в конце тракта, и инструмент 4 выдал сообщение на цикле 11,когда утверждается a.
Какой инструмент сработал правильно? Правильный ответ - все они. PSL определяет выполняется ли свойство в тракте - вот и все. ничего не сказано о том, когда инструмент, динамический или статический, должен выдать сообщение по результатам анализов. Таким образом, нету смысла в вопросе - какой инструмент правильный? Все они показали, что свойство не выполняется на тракте, поэтому все они верны. Индикация ошибки показанная на все тракте может пониматься, как помощь для дебага, помогая пользователям понять,где находиться ошибка на тракте. Пока PSL показывает эти ошибки на трактах, он делает свою работу.
|
|---|
assert always (a -> never b); (3.4a) |
| Рис. 3.4: Четыре инструмент,выдающих сообщение об ошибке утверждения 3.4a на одном и том же тракте |
