PSL/A Practical Introduction to PSL/Introduction/ru

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);
}

• Слой моделирования предоставляет возможности моделирования поведения входов проекта, и декларировать и передавать поведение вспомогательным сигналам и переменным. Эта часть слоя моделирования - просто подмножество какого-либо варианта. Например, декларация вспомогательных сигналов в варианте 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 выражение, которое не выполняется).