«Бог не меняет того, что (происходит) с людьми, пока они сами не изменят своих помыслов.» Коран, Сура 12:13

Проектирование цифровых систем на языках описания аппаратуры/Лекция 13

Материал из Wiki
Перейти к: навигация, поиск
Лекции ПЦСЯОА

Лекции

Практические

Доп. материалы

Заголовок
Верификация с использованием языка PSL.
Автор
Ланкевич Ю.Ю.
Нижний колонтитул
Проектирование цифровых систем на языках описания аппаратуры/Лекция 13
Дополнительный нижний колонтитул
Ланкевич Ю.Ю., 20:25, 9 ноября 2020


Слайд:Введение в PSL

PSL – это аббревиатура от Property Specification Language - язык описания свойств спецификации. PSL - это язык описания свойств. ! Свойство (property) – это характеристика поведения сигналов проекта.

Свойство описывает взаимоотношения определенных значений выбранного подмножества сигналов проекта во времени на заданных тестовых воздействиях. Свойство может выполняться либо не выполняться на конкретном такте моделирования проекта, либо на конкретном временном интервале (последовательности тактов) времени моделирования, либо на всем сеансе моделирования (на «всем» времени – на всех тактах). В вырожденном случае свойство может быть сформулировано для одного сигнала проекта, одного такта и одного значения сигнала. Тогда свойство может состоять в том, имеет заданный сигнал в данном такте заданное значение. Данное свойство может быть проверено на различных тестах, при этом на одних тестах данное свойство может выполняться, на других – нет. Выполнение либо не выполнение свойства связано с утверждением (ассертом – assert) о данном свойстве, иначе говоря, высказыванием о данном свойстве, которое может быть истинно либо ложно. Если высказывание (утверждение) истинно, то говорят, что свойство выполняется, если ложно, то – не выполняется. Чтобы указать требование выполнения свойства на всем сеансе моделирования, используют ключевое слово always (всегда). Чтобы потребовать противоположное – требование невыполнения свойства, используется ключевое слово never (никогда). Итак, ассерт – это утверждение о том, что проект должен вести себя так, как описано в свойстве. PSL предоставляет и другие директивы, например средства определения ситуаций, которые должны быть покрыты. В дополнение к простым булевым условиям, PSL имеет временные операторы, которые разрешают пользователю описывать отношения по времени. Например, PSL утверждение

assert always (a -> next b);

показывает, что когда бы сигнал а не принимал единичное значение, сигнал b должен принять единичное значение в следующем (next) такте. Написание утверждений можно выполнять одновременно с разработкой модели цифровой системы. Ассерты помещаются в требуемых местах VHDL-кодов, что значительно облегчает процесс верификации. ! Ассерты пропускаются при синтезе.

Ассерты при верификации имеют ряд преимуществ перед другими способами верификации. Во-первых, ассерты помогают обнаружить большее количество функциональных ошибок, обнаружить их на более ранних стадиях и определить наиболее возможную причину их появления. Во-вторых, сам процесс формулирования и написания утверждений о свойствах проекта может дать разработчику возможность лучше понять проект и, следовательно, выявить ошибки в алгоритмах или, иначе говоря, не позволить ошибкам попасть в проект на первых порах.

Слайд:Структура языка PSL

Спецификация (программа) на языке PSL состоит из утверждений относительно свойств проекта под набором допущений. Свойство строится из трех видов элементов:

  • булевы выражения, которые описывают поведение в одном такте;
  • последовательности (последовательные выражения), которые могут описывать поведение в нескольких тактах;
  • временные операторы, которые описывают временные взаимоотношения (в одном либо во многих тактах) между булевыми выражениями и/или последовательностями.

Например, булево (типа boolean) выражение в VHDL

a or b

описывает цикл, в котором, по крайней мере, один из сигналов a и b активен (выполняется). Для сигналов других типов (std_logic, bit и др.) будет указано, какие значения будут интерпретироваться как единичные.
! Будем говорить, что сигнал выполняется (активен), если он имеет единичное значение.
Последовательное выражение (последовательность) {a;b;c} описывает последовательность тактов, такую, что: a активен в первом такте, b активен во втором такте, c активен в третьем такте. Следующее свойство получается, применяя временные операторы always и |=> к этим выражениям,

always {a;b;c } |=> (x or y);

это значит, что всегда (в каждом такте), если встречается последовательность {a;b;c}, то либо сигнал x, либо сигнал y должен быть активен в течение такта после окончания последовательности {a; b; c}. Смысл оператора

A |=> B;

состоит в том, что после окончания последовательности A в следующем такте должна начинаться последовательность B. Добавляя директиву assert, получаем:

assert always {a;b;c } |=> (x or y);

Этим завершается спецификация, указывая, что это свойство требуется проверить (верифицировать). Язык PSL в соответствии со стандартом структурирован в четыре отдельных уровня:

  • булевый уровень (boolean),
  • временной уровень (temporal),
  • уровень верификации (verification)
  • уровень моделирования (modelling).

Уровень верификации и временной уровень имеют свой собственный синтаксис, в то время как уровень моделирования и булевый уровень заимствуют синтаксис из лежащего в основе HDL. Таким образом, говорят, что PSL сочетает три стиля («окраски» - flavour): VHDL, Verilog и GDL. Например, ниже показаны два стиля: (a & b)) == 0 // Verilog flavour (a and b)) = ‘0’ -- VHDL flavour Стиль («окраска») напрямую определяет синтаксис, используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня. Булевый уровень используется для создания выражений, которые, в свою очередь, используются другими уровнями.
! Выражения булевого уровня выполняются в одном (одиночном) такте.
Ввыражения булевого уровня оцениваются на истинность (true) либо ложность (false) в определенный момент времени (в определенном такте). Временной уровень является основой языка PSL, он используется для описания свойств проекта и называется временным, потому что, в дополнение к простым свойствам он может также описывать свойства, включающие сложные временные отношения между сигналами. Для временных свойств важны моменты времени, в которых проверяются эти свойства. Моменты времени привязываются к тактам синхросигнала.
! Чаще всего будем считать, что состояния проекта в каждом такте будут фиксироваться по переднему фронту синхросигнала.
Если сигнал проекта изменился (с дельта-задержкой) после установления переднего фронта синхросигнала, то значение сигнала в такте определяется до изменения, а именно, на момент времени установления переднего фронта синхросигнала. Временной уровень может включать в себя как выражения из булева уровня, так и временные операторы и последовательности.
! Язык PSL предназначен для верификации синхронных схем.
Заметим, что за время одного такта синхросигнала состояние проекта может многократно измениться, однако следующим состоянием проекта будем считать состояние, соответствующее следующему переднему фронту синхросигнала. Далее в книге все ассерты будут рассматриваться по переднему фронту сигнала синхронизации. Для ассертов важны будут значения сигналов строго в моменты переднего фронта сигнала. Если будет кратковременное изменение сигнала во время одного такта, то это изменение ассертами не будет учитываться. Например, сигнал sig имеет два кратковременные изменения во втором и пятом такте.