PSL/A Practical Introduction to PSL/Introduction/ru — различия между версиями
Материал из Wiki
Valentin (обсуждение | вклад) |
Valentin (обсуждение | вклад) |
||
| (не показана 1 промежуточная версия 1 участника) | |||
| Строка 27: | Строка 27: | ||
PSL гораздо больше, чем просто язык утверждений. Тем не менее, утверждения - это сердце PSL, и многие пользователи PSL используют его только из-за возможностей утверждений. Таким образом, перед тем как мы разберем весь язык, пару слов о том, что на самом деле дают нам эти утверждения. Многие языки программирования (например Java) и языки описания аппаратуры (например VHDL) содержат утверждающие конструкции. Утверждающие конструкции предоставляются пользователю возможность во время выполнения или во время моделирования, что нужное условие выполняется и выдать сообщение об ошибке или предупреждении, если оно не выполняется. PSL утверждения похожи по своей сущности, но куда как более масштабные. В дополнение к простым Булевым условиям, PSL условия могут содержат ''временные'' операторы, которые разрешают пользователю описывать отношения по времени. Например, PSL утверждение <code>assert always (a -> next b);</code> показывает, что когда бы сигнал а не принимал значение, сигнал b должен принять значение в следующем цикле. | 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 | Java and VHDL assertions are designed to be embedded in executable | ||
code, and to be checked whenever execution reaches the point at which they | 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, | statements. Embedded PSL assertions are located near the code they specify, | ||
but they are still about the code and not a part of it.) | but they are still about the code and not a part of it.) | ||
| + | --> | ||
| + | Java и VHDL утверждения встраиваются в исполняемый код, и должны быть проверены, когда достигается точка выполнения,на которой они появляются. PSL утверждения, с другой стороны, типично располагаются отдельно, и делают утверждения ''о'' коде, не являясь его частью. (Пока некоторые программы поддерживают встроенные PSL утверждения, встроенное утверждение по-прежнему не является частью кода, в том смысле, что нет возможности поместить PSL утверждение внутрь исполняемого утверждения. Встроенные PSL утверждения располагаются рядом с кодом и они определены, но не являются частью кода.) | ||
| + | <!-- | ||
PSL was designed to be mathematically rigorous, with the result that a | 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 | 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 | 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. | documentation in order to clarify subtle points of an English specification. | ||
| + | --> | ||
| + | PSL был создан, чтобы быть математически строгим, с результатом таким, что спецификация PSL точная и автоматически русифицируемая. Таким образом, аппаратная спецификация написанная на PSL читается машиной и может использоваться как вход для программ верификации. В дополнение, PSL был создам для легкого чтения и записи, таким образом PSL спецификация читается человеком и используется для документации, в целях уточнения спорных моментов из английской спецификации. | ||
| + | <!-- | ||
The definitive definition of PSL can be found in IEEE Std 1850-2005. In | 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 | 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 | whole of PSL, and for completeness have included as well the BNF and formal | ||
semantics as appendices. | semantics as appendices. | ||
| + | --> | ||
| + | Окончательное определение PSL можно найти в IEEE Std 1850-2005. В этой книге, нашей целью является получить более спокойное, легко воспринимаемое представление языка, а также углубиться в изучение его тонкостей. Мы покроем весь PSL, а также, для полноты, включим BNF и формальную семантику, в качестве приложений. | ||
| + | <!-- | ||
The structure of PSL is based on four layers – the Boolean layer, the | 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 | 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 | a numbers of flavors, which influence the syntax in a limited way. The four | ||
layers of the language are: | layers of the language are: | ||
| + | --> | ||
| + | Структура языка PSL базируется на четырех слоях - Булевый слой, временной слой, слой верификации и слой моделирования - и представляются в нескольких вариантах, что влияет на синтаксис в ограниченной форме. Четыре слоя это: | ||
| + | <!-- | ||
* 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 ''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. | ||
| + | --> | ||
| + | * ''Булевый слой'' состоит из Булевых выражений, это выражения, значения которого могут быть правда или ложь. Например, <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 ''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. | ||
| + | --> | ||
| + | * ''Временной слой'' состоит из временных свойств, которые описывают взаимоотношения между Булевыми выражениями по времени. Например, <code>always (req -> next ack)</code> временное свойство, выражающее, что когда бы ни (<code>always</code>) не утверждался сигнал <code>req</code>, далее (<code>-></code>) в следующем цикле (<code>next</code>), утверждается сигнал <code>ack</code>. | ||
| + | <!-- | ||
* 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''. | * 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''. | ||
| + | --> | ||
| + | * слой верификации состоит из директив, которые описывают, как временные свойства должны использоваться программами верификации. Например, утверждение <code>always (req -> next ack);</code> - это директива верификации, которая говорит программе верифицировать, что свойство <code>always (req -> next ack);</code> выполняется. Другая директива верификации включает инструкцию предположения, а не верификации, того что конкретное временное свойство выполняется или определяет критерий зоны покрытия. Слой верификации также предоставляет возможность группировать PSL утверждения в ''verification units''. | ||
| Строка 73: | Строка 94: | ||
</source> | </source> | ||
|- | |- | ||
| − | ! (i) VHDL | + | ! (i) VHDL вариант |
| − | ! (ii) Verilog | + | ! (ii) Verilog вариант |
|- | |- | ||
| − | !colspan=2| | + | !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 ''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. | ||
| + | --> | ||
| + | * ''Слой моделирования'' предоставляет возможности моделирования поведения входов проекта, и декларировать и передавать поведение вспомогательным сигналам и переменным. Эта часть слоя моделирования - просто подмножество какого-либо варианта. Например, декларация вспомогательных сигналов в варианте Verilog предполагает синтаксис Verilog. | ||
| + | <!-- | ||
The five flavors of PSL correspond to the hardware description languages | 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. | Verilog and VHDL, to the language GDL, the environment description language of the RuleBase model checker, and to SystemVerilog and SystemC. | ||
| Строка 87: | Строка 112: | ||
the syntax of Boolean expressions – the vast majority of the language is the | the syntax of Boolean expressions – the vast majority of the language is the | ||
same across flavors. | same across flavors. | ||
| + | --> | ||
| + | Пять вариантов PSL соответствуют языкам описания аппаратуры Verilog и VHDL, языку GDL, языку описания среды RuleBase, и SystemVerilog и SystemC. Т.к. все варианты имеют некоторое влияние на синтаксис - например, это влияет на синтаксис Булевых выражений - большинство языков имеют схожий синтаксис. | ||
| + | <!-- | ||
Figure 1.1 shows a PSL specification in the VHDL and Verilog flavors. In | 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. | each case, the specification states that signals a and b are mutually exclusive. | ||
| Строка 103: | Строка 131: | ||
name of the verification unit (<code>example1</code>). The modeling layer is not used in | name of the verification unit (<code>example1</code>). The modeling layer is not used in | ||
this example. | this example. | ||
| + | --> | ||
| + | Рисунок 1.1 показывает спецификацию PSL для VHDL и Verilog вариантов. В каждом случаи, в спецификации говориться, что сигналы a и b взаимоисключающиеся. Пока PSL пользователь не проводит много времени, думая о границах между слоями, мы будем указывать на них в первом примере. Булевы выражения <code>a and b</code> в VHDL варианте и <code>a && b</code> в Verilog варианте, принадлежать Булевому слою и описывают ситуацию, в которой оба сигнала <code>a</code> и <code>b</code> утверждаются. Ключевое слово never относиться к временному слою и показывает, что Булево выражение не ожидает своего выполнения в цикле. Вместе, ключево слово never и Булевы выражения <code>a and b</code> в VHDL варианте или <code>a && b</code> в Verilog варианте, формируют ''свойство''. Ключевое слово assert принадлежит слою верификации и инструктирует программу верификации на проверку того, что свойство выполняется в ходе тестирования проекта. Ключевое слово vunit также принадлежит слою верификации и представляет имя юнита верификации (<code>example1</code>). Слой, моделирования в данном примере, не используется. | ||
| + | <!-- | ||
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 | 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 | the language and makes extensive use of the Boolean layer. Chapter 10 briefly | ||
| Строка 111: | Строка 142: | ||
has been defined to be <code>1’b0</code> (i.e., a Verilog expression that does not hold at | has been defined to be <code>1’b0</code> (i.e., a Verilog expression that does not hold at | ||
any cycle). | any cycle). | ||
| + | --> | ||
| + | Далее в книге, и\мы будем использовать Verilog вариант, если не указано иное. В основном мы сфокусируем наше внимание на временном слое, который является сердцем языка, и будем широко использовать Булевый слой. В глава 10 кратко обговорим различые аспекты Булевого слоя, слоя моделирования и слоя верификации, не затронутые в других главах. Также, мы сделаем предположение, что <code>‘true</code> был определен, как <code>1’b1</code> (т.е. Verilog выражение, которое выполняется в каждом цикле) и, что <code>‘false</code> опреден, как <code>1’b0</code> (т.е. Verilog выражение, которое не выполняется). | ||
Текущая версия на 13:35, 25 октября 2013
Литература
Введение в PSL
- 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, также, предоставляет другие директивы, например средства определения сценариев, которые должны быть покрыты.
PSL гораздо больше, чем просто язык утверждений. Тем не менее, утверждения - это сердце PSL, и многие пользователи PSL используют его только из-за возможностей утверждений. Таким образом, перед тем как мы разберем весь язык, пару слов о том, что на самом деле дают нам эти утверждения. Многие языки программирования (например Java) и языки описания аппаратуры (например VHDL) содержат утверждающие конструкции. Утверждающие конструкции предоставляются пользователю возможность во время выполнения или во время моделирования, что нужное условие выполняется и выдать сообщение об ошибке или предупреждении, если оно не выполняется. PSL утверждения похожи по своей сущности, но куда как более масштабные. В дополнение к простым Булевым условиям, PSL условия могут содержат временные операторы, которые разрешают пользователю описывать отношения по времени. Например, PSL утверждение assert always (a -> next b); показывает, что когда бы сигнал а не принимал значение, сигнал b должен принять значение в следующем цикле.
Java и VHDL утверждения встраиваются в исполняемый код, и должны быть проверены, когда достигается точка выполнения,на которой они появляются. PSL утверждения, с другой стороны, типично располагаются отдельно, и делают утверждения о коде, не являясь его частью. (Пока некоторые программы поддерживают встроенные PSL утверждения, встроенное утверждение по-прежнему не является частью кода, в том смысле, что нет возможности поместить PSL утверждение внутрь исполняемого утверждения. Встроенные PSL утверждения располагаются рядом с кодом и они определены, но не являются частью кода.)
PSL был создан, чтобы быть математически строгим, с результатом таким, что спецификация PSL точная и автоматически русифицируемая. Таким образом, аппаратная спецификация написанная на PSL читается машиной и может использоваться как вход для программ верификации. В дополнение, PSL был создам для легкого чтения и записи, таким образом PSL спецификация читается человеком и используется для документации, в целях уточнения спорных моментов из английской спецификации.
Окончательное определение PSL можно найти в IEEE Std 1850-2005. В этой книге, нашей целью является получить более спокойное, легко воспринимаемое представление языка, а также углубиться в изучение его тонкостей. Мы покроем весь PSL, а также, для полноты, включим BNF и формальную семантику, в качестве приложений.
Структура языка PSL базируется на четырех слоях - Булевый слой, временной слой, слой верификации и слой моделирования - и представляются в нескольких вариантах, что влияет на синтаксис в ограниченной форме. Четыре слоя это:
- Булевый слой состоит из Булевых выражений, это выражения, значения которого могут быть правда или ложь. Например,
aБулево выражение. PSL интерпретирует высокий уровень сигнала, как правда, аaнизкий уровень, как ложь, независимо от того, какой уровень для сигнала, считается активным. Таким образом, если сигналaактивный-высокий, Булево выражениеaимеет значение правда, когдаaутверждается, и ложь, когда не утверждается. А если сигнал b активный-низкий, Булево выражениеbпринимает значение ложь, когдаbутверждается, и правда, когда не утверждается. Далее в этой книге, мы будем считать, что все сигналы имеют активный высокий уровень, если не указано иначе. Конечно, проще принять активный низкий уровень для примера свойств за счет перехода a из!aи наоборот. Булевый слой состоит из Булевых выражений определенного варианта. Например,a && !b- это Булево выражение в варианте Verilog, означает, чтоaутверждается, аbнет,a[31:0]==b[31:0]- это Булево выражение варианта Verilog, означает, что 32-х битные векторыa[31:0]иb[31:0]эквивалентны, иaddr1[127:0]==128’b0- это булево выражение варианта Verilog, означает, что 128-и битный векторaddr1[127:0]имеет нулевое значение.
- Временной слой состоит из временных свойств, которые описывают взаимоотношения между Булевыми выражениями по времени. Например,
always (req -> next ack)временное свойство, выражающее, что когда бы ни (always) не утверждался сигналreq, далее (->) в следующем цикле (next), утверждается сигналack.
- слой верификации состоит из директив, которые описывают, как временные свойства должны использоваться программами верификации. Например, утверждение
always (req -> next ack);- это директива верификации, которая говорит программе верифицировать, что свойствоalways (req -> next ack);выполняется. Другая директива верификации включает инструкцию предположения, а не верификации, того что конкретное временное свойство выполняется или определяет критерий зоны покрытия. Слой верификации также предоставляет возможность группировать PSL утверждения в verification units.
vunit example1 { assert never (a and b); } |
vunit example1 { assert never (a && b); } |
| (i) VHDL вариант | (ii) Verilog вариант |
|---|---|
| Рис. 1.1: Один и тот же vunit в двух различных вариантах | |
- Слой моделирования предоставляет возможности моделирования поведения входов проекта, и декларировать и передавать поведение вспомогательным сигналам и переменным. Эта часть слоя моделирования - просто подмножество какого-либо варианта. Например, декларация вспомогательных сигналов в варианте Verilog предполагает синтаксис Verilog.
Пять вариантов PSL соответствуют языкам описания аппаратуры Verilog и VHDL, языку GDL, языку описания среды RuleBase, и SystemVerilog и SystemC. Т.к. все варианты имеют некоторое влияние на синтаксис - например, это влияет на синтаксис Булевых выражений - большинство языков имеют схожий синтаксис.
Рисунок 1.1 показывает спецификацию PSL для VHDL и Verilog вариантов. В каждом случаи, в спецификации говориться, что сигналы a и b взаимоисключающиеся. Пока PSL пользователь не проводит много времени, думая о границах между слоями, мы будем указывать на них в первом примере. Булевы выражения a and b в VHDL варианте и a && b в Verilog варианте, принадлежать Булевому слою и описывают ситуацию, в которой оба сигнала a и b утверждаются. Ключевое слово never относиться к временному слою и показывает, что Булево выражение не ожидает своего выполнения в цикле. Вместе, ключево слово never и Булевы выражения a and b в VHDL варианте или a && b в Verilog варианте, формируют свойство. Ключевое слово assert принадлежит слою верификации и инструктирует программу верификации на проверку того, что свойство выполняется в ходе тестирования проекта. Ключевое слово vunit также принадлежит слою верификации и представляет имя юнита верификации (example1). Слой, моделирования в данном примере, не используется.
Далее в книге, и\мы будем использовать Verilog вариант, если не указано иное. В основном мы сфокусируем наше внимание на временном слое, который является сердцем языка, и будем широко использовать Булевый слой. В глава 10 кратко обговорим различые аспекты Булевого слоя, слоя моделирования и слоя верификации, не затронутые в других главах. Также, мы сделаем предположение, что ‘true был определен, как 1’b1 (т.е. Verilog выражение, которое выполняется в каждом цикле) и, что ‘false опреден, как 1’b0 (т.е. Verilog выражение, которое не выполняется).
