PSL/A Practical Introduction to PSL/Introduction/ru - История изменений

Valentin в 09:35, 25 октября 2013

2013-10-25T09:35:29Z

Valentin в 08:18, 25 октября 2013

2013-10-25T08:18:29Z

Valentin в 17:07, 23 октября 2013

2013-10-23T17:07:16Z

ANA: Новая страница: «{{PSL TOC}} PSL is a property specification language. It is a means to express ''properties'' of a design, and in addition to specify how verification tools shou…»

2013-10-09T20:01:58Z

Новая страница: «{{PSL TOC}} PSL is a property specification language. It is a means to express ''properties'' of a design, and in addition to specify how verification tools shou…»

Новая страница

{{PSL TOC}}

PSL is a property specification language. It is a means to express ''properties''
of a design, and in addition to specify how verification tools should use those
properties. For example, a property may be ''asserted'' – this specifies that the
design in question is expected to behave as described by the property. A
property may also be ''assumed'' – this specifies that the design in question
expects its inputs to behave as described by the property. PSL also provides
other directives, for instance a means to specify scenarios that should be
''covered''.

PSL is much more than simply an assertion language. Nevertheless, assertions are at the heart of PSL, and many PSL users will use PSL only for its
assertion capabilities. Thus, before we examine the complete language, a few
words about what exactly a PSL assertion is are in order. Many programming languages (for example Java) and hardware description languages (for
example VHDL) contain assert constructs. An assert construct provides the
user with a way to check at run time or at simulation time that a certain
condition holds, and to report a warning or an error if it does not. PSL assertions are similar in motivation, but much more extensive in their scope. In
addition to simple Boolean conditions, a PSL assertion can contain ''temporal''
operators that allow the user to describe relations over time. For example,
the PSL assertion <code>assert always (a -> next b);</code> specifies that whenever
signal a holds, signal b must hold on the next cycle.

Java and VHDL assertions are designed to be embedded in executable
code, and to be checked whenever execution reaches the point at which they
appear. PSL assertions, on the other hand, typically stand alone, making a
statement ''about'' the code without being a part of it. (While some tools support
embedded PSL assertions, an embedded assertion is still not part of the code
in the sense that there is no way to nest PSL assertions inside of executable
statements. Embedded PSL assertions are located near the code they specify,
but they are still about the code and not a part of it.)

PSL was designed to be mathematically rigorous, with the result that a
PSL specification is both precise and automatically verifiable. Thus, a hardware specification written in PSL is machine readable and can be used as
input to verification tools. In addition, PSL was designed to be easy to read
and write, thus a PSL specification is human readable and can be used for
documentation in order to clarify subtle points of an English specification.

The definitive definition of PSL can be found in IEEE Std 1850-2005. In
this book, our goal is to give a more relaxed, user-friendly introduction to the
language, as well as an in-depth discussion of its fine points. We do cover the
whole of PSL, and for completeness have included as well the BNF and formal
semantics as appendices.

The structure of PSL is based on four layers – the Boolean layer, the
temporal layer, the verification layer and the modeling layer – and comes in
a numbers of flavors, which influence the syntax in a limited way. The four
layers of the language are:

* The ''Boolean layer'' is composed of Boolean expressions, that is, expressions whose value is either true or false. For example, <code>a</code> is a Boolean expression. PSL interprets a high signal as true, and <code>a</code> low signal as false, independent of whether the signal is active-high or active-low. Thus, if signal <code>a</code> is activehigh, the Boolean expression <code>a</code> has the value true when <code>a</code> is asserted, and false when it is deasserted. And if signal b is active-low, the Boolean expression <code>b</code> has the value false when <code>b</code> is asserted and true when it is deasserted. In the remainder of this book, we will assume that all signals are active-high unless stated otherwise. Of course, it is easy to get the active-low versions of the example properties by switching a with <code>!a</code> and vice versa. The Boolean layer consists of any Boolean expression in the underlying flavor. For example, <code>a && !b</code> is a Boolean expression in the Verilog flavor stating that <code>a</code> holds and <code>b</code> does not, <code>a[31:0]==b[31:0]</code> is a Verilog-flavored Boolean expression stating that the 32-bit vectors <code>a[31:0]</code> and <code>b[31:0]</code> are equal, and <code>addr1[127:0]==128’b0</code> is a Verilog-flavored Boolean expression stating that the 128-bit vector <code>addr1[127:0]</code> has the value zero.

* The ''temporal layer'' consists of temporal properties which describe the relationships between Boolean expressions over time. For example, <code>always (req -> next ack)</code> is a temporal property expressing the fact that whenever (<code>always</code>) signal <code>req</code> is asserted, then (<code>-></code>) at the next cycle (<code>next</code>), signal ack is asserted.

* The ''verification layer'' consists of directives which describe how the temporal properties should be used by verification tools. For example, assert <code>always (req -> next ack);</code> is a verification directive that tells the tools to verify that the property <code>always (req -> next ack)</code> holds. Other verification directives include an instruction to assume, rather than verify, that a particular temporal property holds, or to specify coverage criteria. The verification layer also provides a means to group PSL statements into ''verification units''.

{| align=center
|
<source lang="vhdl">
vunit example1 {
assert never (a and b);
}
</source>
|<source lang="vhdl">
vunit example1 {
assert never (a && b);
}
</source>
|-
! (i) VHDL flavor
! (ii) Verilog flavor
|-
!colspan=2| Fig. 1.1: The same vunit in two different flavors
|}

* The ''modeling layer'' provides a means to model behavior of design inputs, and to declare and give behavior to auxiliary signals and variables. This part of the modeling layer is simply a subset of the underlying flavor. For instance, the declaration of auxiliary signals in the Verilog flavor follows Verilog syntax.

The five flavors of PSL correspond to the hardware description languages
Verilog and VHDL, to the language GDL, the environment description language of the RuleBase model checker, and to SystemVerilog and SystemC.
While the flavor has some influence over the syntax – for instance, it affects
the syntax of Boolean expressions – the vast majority of the language is the
same across flavors.

Figure 1.1 shows a PSL specification in the VHDL and Verilog flavors. In
each case, the specification states that signals a and b are mutually exclusive.
While a PSL user typically does not spend a lot of time thinking about the
boundaries between the various layers, we will point them out in this first
example. The Boolean expressions a and b in the VHDL flavor and <code>a && b</code>
in the Verilog flavor belong to the Boolean layer and describe the situation
in which both signal <code>a</code> and signal <code>b</code> are asserted. The keyword never belongs
to the temporal layer and indicates that the Boolean expression is expected
to hold in no cycle. Together, the temporal keyword never and the Boolean
expressions <code>a and b</code> in the VHDL flavor or <code>a && b</code> in the Verilog flavor form
a ''property''. The keyword assert belongs to the verification layer and instructs
the verification tool to check that the property holds in the design under test.
The keyword vunit also belongs to the verification layer and introduces the
name of the verification unit (<code>example1</code>). The modeling layer is not used in
this example.

In the remainder of this book we use the Verilog flavor unless stated otherwise. We focus almost exclusively on the temporal layer, which is the heart of
the language and makes extensive use of the Boolean layer. Chapter 10 briefly
discusses various aspects of the Boolean, modeling and verification layers not
covered elsewhere. Throughout, we will assume that <code>‘true</code> has been defined to
be <code>1’b1</code> (i.e., a Verilog expression that holds at every cycle) and that <code>‘false</code>
has been defined to be <code>1’b0</code> (i.e., a Verilog expression that does not hold at
any cycle).

@@ Строка 70: / Строка 70: @@
 * ''Булевый слой'' состоит из Булевых выражений, это выражения, значения которого могут быть правда или ложь. Например, <code>a</code> Булево выражение. PSL интерпретирует высокий уровень сигнала, как правда, а <code>a</code> низкий уровень, как ложь, независимо от того, какой уровень для сигнала, считается активным. Таким образом, если сигнал <code>a</code> активный-высокий, Булево выражение <code>a</code> имеет значение правда, когда <code>a</code> утверждается, и ложь, когда не утверждается. А если сигнал b активный-низкий, Булево выражение <code>b</code> принимает значение ложь, когда <code>b</code> утверждается, и правда, когда не утверждается. Далее в этой книге, мы будем считать, что все сигналы имеют активный высокий уровень, если не указано иначе. Конечно, проще принять активный низкий уровень для примера свойств за счет перехода a из <code>!a</code> и наоборот. Булевый слой состоит из Булевых выражений определенного варианта. Например, <code>a && !b</code> - это Булево выражение в варианте Verilog, означает, что <code>a</code> утверждается, а <code>b</code> нет, <code>a[31:0]==b[31:0]</code> - это Булево выражение варианта Verilog, означает, что 32-х битные векторы <code>a[31:0]</code> и <code>b[31:0]</code> эквивалентны, и <code>addr1[127:0]==128’b0</code> - это булево выражение варианта Verilog, означает, что 128-и битный вектор <code>addr1[127:0]</code> имеет нулевое значение.
 * The ''temporal layer'' consists of temporal properties which describe the relationships between Boolean expressions over time. For example, <code>always (req -> next ack)</code> is a temporal property expressing the fact that whenever (<code>always</code>) signal <code>req</code> is asserted, then (<code>-></code>) at the next cycle (<code>next</code>), signal ack is asserted.
 * The ''verification layer'' consists of directives which describe how the temporal properties should be used by verification tools. For example, assert <code>always (req -> next ack);</code> is a verification directive that tells the tools to verify that the property <code>always (req -> next ack)</code> holds. Other verification directives include an instruction to assume, rather than verify, that a particular temporal property holds, or to specify coverage criteria. The verification layer also provides a means to group PSL statements into ''verification units''.
@@ Строка 88: / Строка 94: @@
 </source>
 |-
-! (i) VHDL flavor
+! (i) VHDL вариант
-! (ii) Verilog flavor
+! (ii) Verilog вариант
 |-
-!colspan=2| Fig. 1.1: The same vunit in two different flavors
+!colspan=2| Рис. 1.1: Один и тот же vunit в двух различных вариантах
 |}
 * The ''modeling layer'' provides a means to model behavior of design inputs, and to declare and give behavior to auxiliary signals and variables. This part of the modeling layer is simply a subset of the underlying flavor. For instance, the declaration of auxiliary signals in the Verilog flavor follows Verilog syntax.
 The five flavors of PSL correspond to the hardware description languages
 Verilog and VHDL, to the language GDL, the environment description language of the RuleBase model checker, and to SystemVerilog and SystemC.
@@ Строка 102: / Строка 112: @@
 the syntax of Boolean expressions – the vast majority of the language is the
 same across flavors.
 Figure 1.1 shows a PSL specification in the VHDL and Verilog flavors. In
 each case, the specification states that signals a and b are mutually exclusive.
@@ Строка 118: / Строка 131: @@
 name of the verification unit (<code>example1</code>). The modeling layer is not used in
 this example.
 In the remainder of this book we use the Verilog flavor unless stated otherwise. We focus almost exclusively on the temporal layer, which is the heart of
 the language and makes extensive use of the Boolean layer. Chapter 10 briefly
@@ Строка 126: / Строка 142: @@
 has been defined to be <code>1’b0</code> (i.e., a Verilog expression that does not hold at
 any cycle).

@@ Строка 27: / Строка 27: @@
 PSL гораздо больше, чем просто язык утверждений. Тем не менее, утверждения - это сердце PSL, и многие пользователи PSL используют его только из-за возможностей утверждений. Таким образом, перед тем как мы разберем весь язык, пару слов о том, что на самом деле дают нам эти утверждения. Многие языки программирования (например Java) и языки описания аппаратуры (например VHDL) содержат утверждающие конструкции. Утверждающие конструкции предоставляются пользователю возможность во время выполнения или во время моделирования, что нужное условие выполняется и выдать сообщение об ошибке или предупреждении, если оно не выполняется. PSL утверждения похожи по своей сущности, но куда как более масштабные. В дополнение к простым Булевым условиям, PSL условия могут содержат ''временные'' операторы, которые разрешают пользователю описывать отношения по времени. Например, PSL утверждение  <code>assert always (a -> next b);</code> показывает, что когда бы сигнал а не принимал значение, сигнал b должен принять значение в следующем цикле.
 Java and VHDL assertions are designed to be embedded in executable
 code, and to be checked whenever execution reaches the point at which they
@@ Строка 35: / Строка 36: @@
 statements. Embedded PSL assertions are located near the code they specify,
 but they are still about the code and not a part of it.)
 PSL was designed to be mathematically rigorous, with the result that a
 PSL specification is both precise and automatically verifiable. Thus, a hardware specification written in PSL is machine readable and can be used as
@@ Строка 41: / Строка 45: @@
 and write, thus a PSL specification is human readable and can be used for
 documentation in order to clarify subtle points of an English specification.
 The definitive definition of PSL can be found in IEEE Std 1850-2005. In
 this book, our goal is to give a more relaxed, user-friendly introduction to the
@@ Строка 47: / Строка 54: @@
 whole of PSL, and for completeness have included as well the BNF and formal
 semantics as appendices.
 The structure of PSL is based on four layers – the Boolean layer, the
 temporal layer, the verification layer and the modeling layer – and comes in
 a numbers of flavors, which influence the syntax in a limited way. The four
 layers of the language are:
 * The ''Boolean layer'' is composed of Boolean expressions, that is, expressions whose value is either true or false. For example, <code>a</code> is a Boolean expression. PSL interprets a high signal as true, and <code>a</code> low signal as false, independent of whether the signal is active-high or active-low. Thus, if signal <code>a</code> is activehigh, the Boolean expression <code>a</code> has the value true when <code>a</code> is asserted, and false when it is deasserted. And if signal b is active-low, the Boolean expression <code>b</code> has the value false when <code>b</code> is asserted and true when it is deasserted. In the remainder of this book, we will assume that all signals are active-high unless stated otherwise. Of course, it is easy to get the active-low versions of the example properties by switching a with <code>!a</code> and vice versa. The Boolean layer consists of any Boolean expression in the underlying flavor. For example, <code>a && !b</code> is a Boolean expression in the Verilog flavor stating that <code>a</code> holds and <code>b</code> does not, <code>a[31:0]==b[31:0]</code> is a Verilog-flavored Boolean expression stating that the 32-bit vectors <code>a[31:0]</code> and <code>b[31:0]</code> are equal, and <code>addr1[127:0]==128’b0</code> is a Verilog-flavored Boolean expression stating that the 128-bit vector <code>addr1[127:0]</code> has the value zero.
 * The ''temporal layer'' consists of temporal properties which describe the relationships between Boolean expressions over time. For example, <code>always (req -> next ack)</code> is a temporal property expressing the fact that whenever (<code>always</code>) signal <code>req</code> is asserted, then (<code>-></code>) at the next cycle (<code>next</code>), signal ack is asserted.

@@ Строка 1: / Строка 1: @@
 {{PSL TOC}}
 PSL is a property specification language. It is a means to express ''properties''
 of a design, and in addition to specify how verification tools should use those
@@ Строка 9: / Строка 10: @@
 other directives, for instance a means to specify scenarios that should be
 ''covered''.
 PSL is much more than simply an assertion language. Nevertheless, assertions are at the heart of PSL, and many PSL users will use PSL only for its
 assertion capabilities. Thus, before we examine the complete language, a few
@@ Строка 20: / Строка 24: @@
 the PSL assertion <code>assert always (a -> next b);</code> specifies that whenever
 signal a holds, signal b must hold on the next cycle.
 Java and VHDL assertions are designed to be embedded in executable