«Случай — это псевдоним Бога, когда Он не хочет подписываться своим собственным именем.» А. Франс

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

Материал из Wiki
Перейти к: навигация, поиск
(Новая страница: «{{PSL TOC}} == Some Philosophy == We have seen some basic PSL and gotten a feel for how it is intended to be used. Before we continue, we discuss some of the …»)
 
(→‎3.5 Reporting a failure)
 
(не показаны 9 промежуточных версий 2 участников)
Строка 2: Строка 2:
  
  
−
== Some Philosophy ==
+
== Немного философии ==
−
 
+
  
 +
<!--
 
We have seen some basic PSL and gotten a feel for how it is intended to be
 
We have seen some basic PSL and gotten a feel for how it is intended to be
 
used. Before we continue, we discuss some of the concepts at the root of PSL.
 
used. Before we continue, we discuss some of the concepts at the root of PSL.
 +
-->
 +
Мы рассмотрели немного основ PSL и получили ощущение того, как используется. Перед тем как продолжить, мы обсудим некоторые концепции в корне PSL.
  
 +
=== 3.1 Утверждения против свойств ===
  
−
=== 3.1 Assertions vs. properties ===
+
<!--
−
 
+
 
As we have seen, a PSL assertion is made up of the keyword assert plus
 
As we have seen, a PSL assertion is made up of the keyword assert plus
 
the PSL ''property'' being asserted, followed by a semi-colon. For example, in
 
the PSL ''property'' being asserted, followed by a semi-colon. For example, in
Строка 25: Строка 27:
 
sub-property of a more complicated property, and as such, it does not state a
 
sub-property of a more complicated property, and as such, it does not state a
 
requirement on its own.
 
requirement on its own.
 +
-->
 +
Как мы уже видели, утверждения PSL состоят из ключевого слова assert плюс ''свойства'' PSL для утверждения, разделенных точкой с запятой. Например, в утверждении <code>assert always (a -> next b);</code>, свойство - <code>always (a -> next b)</code>. Свойство выполняется или не выполняется в данном тракте. Утверждение, с другой стороны, указывает программе верификации, что свойство было утверждено, и требуется выполнение. Далее в книге мы будем внимательно рассматривать отличия между свойствами, которые просто описывают поведения, и утверждения,которые устанавливают требования. Например, мы можем сказать, что утверждение <code>assert always (a -> next b);</code> требует, чтобы когда бы сигнал <code>a</code> не утверждался, сигнал <code>b</code> должен будет утвердиться в следующем цикле. Однако, мы никогда не скажем такого о свойстве <code>always (a -> next b)</code>, по двум причинам. Первая - потому что если свойство используется в предположении (<code>assume always (a -> next b);</code>), то нету никаких требований. Вторая - потому что свойство может использоваться, как под-свойство более сложного свойства, и если так, то не может исходить требований от него самого.
  
 +
=== 3.2 Понятие времени ===
  
−
=== 3.2 The notion of time ===
+
<!--
−
 
+
 
When a Boolean assertion is embedded in code that is being run, like in the
 
When a Boolean assertion is embedded in code that is being run, like in the
 
simple assertions of Java and (simulated) VHDL, the notion of time need not
 
simple assertions of Java and (simulated) VHDL, the notion of time need not
Строка 36: Строка 40:
 
to them) and which second of all span multiple time steps, the notion of time
 
to them) and which second of all span multiple time steps, the notion of time
 
must be given more consideration.
 
must be given more consideration.
 +
-->
 +
Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении 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
Строка 48: Строка 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
Строка 59: Строка 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 Проекты и тракты ===
 +
 +
<!--
 +
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
 +
design. The Foundation Language (FL), which we focus on in this book, uses
 +
this approach, and thus throughout most of this book we shall be interested
 +
in whether or not a particular PSL property holds on a particular trace.
 +
The Foundation Language is suitable for both static (formal) and dynamic
 +
(simulation-based) verification.
 +
-->
 +
Цель свойства PSL описать желаемое поведение проекта. Как правило, это удобно для проверки отдельных трактов проекта. Фундаментальный язык, который используется в данной книге, применяет данный подход, и таким образом, на протяжении данной книги мы будем интересоваться выполняется ли некое свойство в этом тракте или нет. Фундаментальный язык подходит, как для статической (формальной), так и для динамической (базирующейся на моделировании) верификации. 
 +
 +
<!--
 +
Another approach, used by the Optional Branching Extension (OBE), uses
 +
a tree structure that represents multiple paths. This approach is applicable
 +
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
 +
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
 +
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
 +
current cycle of an assertion is 0. The current cycle of a sub-property of some
 +
enclosing property depends on its use in the enclosing property. The operands
 +
of a Boolean operator have the same current cycle as the parent property.
 +
The operands of a temporal operator have a current cycle that is related to
 +
the current cycle of the parent property in a way dictated by the temporal
 +
operator. For example, the next operator increases the current cycle by one,
 +
the always operator creates “multiple instances” of the sub-property, each of
 +
which has a current cycle that corresponds either to the current cycle or to
 +
some future cycle, etc.
 +
-->
 +
Предполагая, что циклы тракта нумеруются, начиная с 0, текущий цикл утверждения - 0. Текущий цикл под-свойства, какого-нибудь вшитого свойства, зависит от своего использования во вшитом свойстве. Операнды Булевого оператора получают такой же текущий цикл, как и родительское свойство. Операнды временных операторов получают текущий цикл, который связан с текущим циклом родительского свойства, в случаи, если это указано временным оператором. Например, оператор next увеличивает текущий цикл на один, оператор always создает “несколько экземпляров” под-свойства, каждый из которых получает текущий цикл, который соответствует текущему циклу или некоторому будущему циклу.   
 +
 +
<!--
 +
NOTE: It is very important to understand that the term “multiple instances”
 +
is intended to convey an intuition which is useful in understanding
 +
the <code>always</code> operator. It is ''not'' intended to hint that any actual instantiation
 +
is taking place; neither does it imply that a tool implementing PSL needs to
 +
create multiple instances of an assertion checker, spawn multiple instances of
 +
a process, or in any other way cause the words “multiple instances” to correspond
 +
to actual instances of anything whatsoever. On the contrary, there are
 +
many efficient implementations of PSL in which the <code>always</code> operator does not
 +
create, spawn, or in any other way generate actual multiple instances. Still,
 +
the term “multiple instances” is a good way to gain intuition about how the
 +
<code>always</code> operator works, and a naive and inefficient implementation may well
 +
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
 +
not <code>always (a -> next b)</code> holds at cycle 0 depends on whether or not the
 +
sub-property <code>(a -> next b)</code> holds at every cycle from 0 onwards. The current
 +
cycle for a particular evaluation of the sub-property <code>(a -> next b)</code> will be
 +
some cycle ''N''. Finally, in order to determine whether or not sub-property
 +
<code>(a -> next b)</code> holds at cycle ''N'', we will need to evaluate sub-properties a
 +
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.
 +
-->
 +
Возвращаясь к нашему основному пункту рассмотрения, рассмотрим утверждение <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
 +
3.1a, on Trace 3.1(i). Signal a holds in cycles 4 and 8. Signal <code>b</code> holds in
 +
cycle 5, and therefore <code>next b</code> holds in cycle 4. This is shown in Trace 3.1(ii),
 +
an annotated version of Trace 3.1(i). Since a holds in cycles 4 and 8, and <code>next b</code>
 +
holds in cycle 4, we get that <code>(a -> next b)</code> holds in all cycles but cycle 8,
 +
as shown in Trace 3.1(ii). (Remember that the else-part defaults to true, so <code>(a -> next b)</code>
 +
holds in all cycles where <code>a</code> does not hold, and in addition in all
 +
cycles where <code>a</code> holds and <code>next b</code> does too.) The entire property <code>always (a -> next b)</code>
 +
therefore holds in cycles 9, 10, 11, 12 and 13 (because in these
 +
cycles, <code>(a -> next b)</code> holds “now” and in all future cycles). Thus, Assertion
 +
3.1a does not hold on Trace 3.1(i) (because it does not hold on cycle 0 –
 +
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
 +
! [[Файл:Psl fig3.1.png]]
 +
|-
 +
|<pre>
 +
assert always (a -> next b);          (3.1a)
 +
</pre>
 +
|-
 +
! Рис. 3.1: Конкретный пример
 +
|}
 +
 +
 +
<!--
 +
The above explanation seems straightforward. However, the idea of modularity
 +
hides some subtle points – for example, that the value of the property
 +
<code>a</code> is dependent only on the current cycle. Thus, Assertion 3.2a holds on
 +
Trace 3.2(i), because signal <code>a</code> holds in cycle 0. If you want to express the fact
 +
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).
 +
-->
 +
Приведенное выше описание кажется простым. Однако, идея модульности скрывает некоторые тонкие моменты, например, что значение свойства <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
 +
without holding on the trace itself. Thus, the property <code>always a</code> holds on
 +
the sub-traces of Trace 3.2(i) starting at cycles 12, 13, and 14. This would
 +
be important if we used the property <code>always a</code> as a sub-property of some
 +
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.
 +
-->
 +
Другой тонкий момент, что свойство может выполняться в суффиксе тракта,а не на самом тракте. Таким образом, свойство <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
 +
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 <code>(a && next[6] (b)) -> (c && next[2] (d))</code>
 +
holds at all cycles. It holds at cycle 2 because
 +
the left-hand side <code>(a && next[6] (b))</code> holds and in addition the right-hand
 +
side <code>(c && next[2] (d))</code> 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.
 +
-->
 +
Последнее, циклы вовлеченные в в подсчет левой стороны логической импликации могут прекрываться с циклами вовлеченными в подсчет правой стороны логической импликации. Например, рассмотрим утверждение 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
 +
! [[Файл:Psl fig3.2.png]]
 +
|-
 +
!(i) Утверждение 3.2a и 3.2c выполняются, но 3.2b нет
 +
|-
 +
|<pre>
 +
assert a;                      (3.2a)
 +
assert always a;                (3.2b)
 +
assert next[12] (always a);    (3.2c)
 +
</pre>
 +
|-
 +
! Рис. 3.2: Важность оператора always
 +
|}
 +
 +
 +
{| align=center
 +
! [[Файл:Psl fig3.3.png]]
 +
|-
 +
!(i) Иллюстрация перекрытие левой и правой стороны  <br />
 +
утверждение 3.3a. Утверждение 3.3a выполняется.
 +
|-
 +
|<pre>
 +
assert always ((a && next[6](b)) -> (c && next[2](d)));      (3.3a)
 +
</pre>
 +
|-
 +
! Рис. 3.3: Текущий цикл
 +
|}
 +
 +
<!--
 +
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 <code>always</code> 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
 +
<code>simple subset</code> 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.
 +
-->
 +
Предварительно, например в рассматриваемых утверждениях 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
 +
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 <code>b</code> 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 <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
 +
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.
 +
-->
 +
Какой инструмент сработал правильно? Правильный ответ - все они. PSL определяет выполняется ли свойство в тракте - вот и все. ничего не сказано о том, когда инструмент, динамический или статический, должен выдать сообщение по результатам анализов. Таким образом, нету смысла в вопросе - какой инструмент правильный? Все они показали, что свойство не выполняется на тракте, поэтому все они верны. Индикация ошибки показанная на все тракте может пониматься, как помощь для дебага, помогая пользователям понять,где находиться ошибка на тракте. Пока PSL показывает эти ошибки на трактах, он делает свою работу. 
  
−
===3.3 Designs and traces===
+
{| align=center
 +
! [[Файл:Psl fig3.4.png]]
 +
|-
 +
|<pre>
 +
assert always (a -> never b);    (3.4a)
 +
</pre>
 +
|-
 +
! Рис. 3.4: Четыре инструмент,выдающих сообщение об ошибке утверждения 3.4a на одном и том же тракте
 +
|}

Текущая версия на 15:04, 25 ноября 2013

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


Содержание

Немного философии

Мы рассмотрели немного основ 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 - первом цикле тракта).

Psl fig3.1.png 
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” принимает значение правда

Psl fig3.2.png
(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


Psl fig3.3.png
(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 показывает эти ошибки на трактах, он делает свою работу.

Psl fig3.4.png 
assert always (a -> never b);     (3.4a)
Рис. 3.4: Четыре инструмент,выдающих сообщение об ошибке утверждения 3.4a на одном и том же тракте
Источник — «http://www.simhard.com/wiki/index.php?title=PSL/A_Practical_Introduction_to_PSL/Some_Philosophy/ru&oldid=3441»