PSL/A Practical Introduction to PSL/Some Philosophy/ru
- 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 |
