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

Версия 12:18, 25 октября 2013

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] имеет нулевое значение.

• The temporal layer consists of temporal properties which describe the relationships between Boolean expressions over time. For example, always (req -> next ack) is a temporal property expressing the fact that whenever (always) signal req is asserted, then (->) at the next cycle (next), 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 always (req -> next ack); is a verification directive that tells the tools to verify that the property always (req -> next ack) 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.

vunit example1 {
  assert never (a and b);
}

vunit example1 {
  assert never (a && b);
}

• 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 a && b in the Verilog flavor belong to the Boolean layer and describe the situation in which both signal a and signal b 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 a and b in the VHDL flavor or a && b 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 (example1). 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 ‘true has been defined to be 1’b1 (i.e., a Verilog expression that holds at every cycle) and that ‘false has been defined to be 1’b0 (i.e., a Verilog expression that does not hold at any cycle).