Проектирование цифровых систем на языках описания аппаратуры/Лекция 13
- Заголовок
- Верификация с использованием языка PSL.
- Автор
- Ланкевич Ю.Ю.
- Нижний колонтитул
- Проектирование цифровых систем на языках описания аппаратуры/Лекция 13
- Дополнительный нижний колонтитул
- Ланкевич Ю.Ю., 20:25, 9 ноября 2020
Слайд:Введение в PSL
PSL – это аббревиатура от Property Specification Language - язык описания свойств спецификации.
PSL - это язык описания свойств.
! Свойство (property) – это характеристика поведения сигналов проекта.
Свойство описывает взаимоотношения определенных значений выбранного подмножества сигналов проекта во времени на заданных тестовых воздействиях. Свойство может выполняться либо не выполняться на конкретном такте моделирования проекта, либо на конкретном временном интервале (последовательности тактов) времени моделирования, либо на всем сеансе моделирования (на «всем» времени – на всех тактах). В вырожденном случае свойство может быть сформулировано для одного сигнала проекта, одного такта и одного значения сигнала. Тогда свойство может состоять в том, имеет заданный сигнал в данном такте заданное значение. Данное свойство может быть проверено на различных тестах, при этом на одних тестах данное свойство может выполняться, на других – нет. Выполнение либо не выполнение свойства связано с утверждением (ассертом – assert) о данном свойстве, иначе говоря, высказыванием о данном свойстве, которое может быть истинно либо ложно. Если высказывание (утверждение) истинно, то говорят, что свойство выполняется, если ложно, то – не выполняется. Чтобы указать требование выполнения свойства на всем сеансе моделирования, используют ключевое слово always (всегда). Чтобы потребовать противоположное – требование невыполнения свойства, используется ключевое слово never (никогда). Итак, ассерт – это утверждение о том, что проект должен вести себя так, как описано в свойстве. PSL предоставляет и другие директивы, например средства определения ситуаций, которые должны быть покрыты. В дополнение к простым булевым условиям, PSL имеет временные операторы, которые разрешают пользователю описывать отношения по времени. Например, PSL утверждение
assert always (a -> next b);
! Ассерты пропускаются при синтезе.
Ассерты при верификации имеют ряд преимуществ перед другими способами верификации. Во-первых, ассерты помогают обнаружить большее количество функциональных ошибок, обнаружить их на более ранних стадиях и определить наиболее возможную причину их появления. Во-вторых, сам процесс формулирования и написания утверждений о свойствах проекта может дать разработчику возможность лучше понять проект и, следовательно, выявить ошибки в алгоритмах или, иначе говоря, не позволить ошибкам попасть в проект на первых порах.
Слайд:Структура языка PSL
Спецификация (программа) на языке PSL состоит из утверждений относительно свойств проекта под набором допущений. Свойство строится из трех видов элементов:
- булевы выражения, которые описывают поведение в одном такте;
- последовательности (последовательные выражения), которые могут описывать поведение в нескольких тактах;
- временные операторы, которые описывают временные взаимоотношения (в одном либо во многих тактах) между булевыми выражениями и/или последовательностями.
Например, булево (типа boolean) выражение в VHDL
a or b
! Будем говорить, что сигнал выполняется (активен), если он имеет единичное значение.
Последовательное выражение (последовательность) {a;b;c} описывает последовательность тактов, такую, что: a активен в первом такте, b активен во втором такте, c активен в третьем такте. Следующее свойство получается, применяя временные операторы always и |=> к этим выражениям,
always {a;b;c } |=> (x or y);
A |=> B;
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 имеет два кратковременные изменения во втором и пятом такте.
При анализе утверждений о свойствах сигнала sig данный сигнал будет представляться как sig_as.
Кратковременная установка в единичное значение сигнала sig во втором такте, а также кратковременная установка в нуль в пятом такте игнорируется.
На момент начала такта (по переднему фронту сигнала clk) сигнал sig будет иметь нулевое значение в первом, втором и третьем тактах и единичное значение в четвертом и пятом тактах.
В PSL имеются свои средства тактирования, можно использовать для отдельного ассерта свое тактирование, т.е. выбирать некоторый сигнал в качестве синхросигнала и осуществлять для отдельного ассерта свою синхронизацию по выбранному сигналу.
Уровень верификации состоит из директив, которые описывают, каким образом временные свойства должны использоваться программами верификации. Например, утверждение always (req -> next ack); - это директива верификации, которая говорит программе проверить, всегда ли свойство always (req -> next ack); выполняется. Директивы верификации - это инструкции программе, которые поясняют, что делать со свойствами. Смысл директив верификации следующий:
- assert (программа должна попытаться доказать свойство);
- cover (программа должна подсчитать, как часто используется свойство во время моделирования).
vunit first (tstb(BEHAVIOR)) { default clock is rising_edge(clk); property prop1 is always {state=a2; state=a3}; as1: assert prop1; }
Уровень моделирования позволяет дополнительным фрагментам кода из базового языка включаться в свойства и расширять их, что делает возможным использовать PSL отдельно (самостоятельно).
Например, уровень моделирования может использоваться для расчета ожидаемых выходных значений.
Уровень моделирования предоставляет возможности моделирования поведения входов проекта, декларировать и передавать поведение вспомогательным сигналам и переменным.
Уровень моделирования включает некоторые дополнительные языковые конструкции и удобные функции.
Например, функция prev() возвращает значение выражения прошлого цикла.
! Ключевые слова PSL со стилем VHDL не чувствительны к регистру.
Операторы PSL разделяются символом ; (точкой с запятой).
Слайд:Основные PSL операторы
| Оператор, ключевое слово | Смысл, содержание | Типы операндов |
|---|---|---|
|
А |-> В |
Первая последовательность А всегда должна сопровождаться второй последовательностью В с перекрытием в одном цикле (суффиксная импликация) |
|
|
А |=> В |
Первая последовательность А всегда должна сопровождаться второй последовательностью В без перекрытия последовательностей |
|
|
А -> В |
Логическая импликация |
Левый операнд А должен быть булевым |
|
always P |
Всегда. Утверждение P должно выполняться в каждом такте |
|
|
never P |
Никогда. Утверждение P должно не выполняться в каждом такте |
Булев операнд либо последовательность |
|
Assert P |
Утверждение является истинным, если свойство P выполняется |
|
|
next P |
В следующем такте |
|
|
p until q p |
должен быть выполнен в любом такте до такта, в котором выполнен q, при этом нет обязательного значения для p в такте, где q выполнен |
Правый операнд должен быть булевым |
|
p before q |
p должен строго выполняться перед q, если p никогда не выполнится, то q также никогда не выполнится |
Оба операнда должны быть булевыми |
|
[=n] |
Непоследовательное повторение n раз (для последовательностей) |
|
|
[*n] |
Последовательное повторение в n тактах (для последовательностей) |
|
| ! |
Сильный оператор, т.е. должен быть такой такт, в котором выполнится свойство без восклицательного знака |
Булев операнд |
|
Eventually! |
Что-то должно произойти в будущем, без уточнения, когда именно. Будет выдаваться ошибка, если за все время моделирования свойство ни разу не выполнилось |
Булев операнд либо последовательность |
Слайд:Простые свойства и тактирование
Простейшая форма свойства в PSL представляет собой комбинационное булево условие CONDITION, которое должно выполняться в каждом такте: assert always CONDITION; Однако эта форма свойств практически не используется, т.к. сигнал CONDITION может часто меняться даже в течение одного такта. Поэтому сигнал CONDITION проверяется в каждом такте один раз, например по переднему либо заднему фронту сигнала синхронизации. Также возможно определить синхросигнал по умолчанию и, таким образом, избежать потребности в повторении явного оператора синхросигнала @ для каждого отдельного утверждения. Ниже в примере ассерт будет проверяться по переднему фронту сигнала clk синхронизации: -- psl default clock is rising_edge(clk); -- psl assert always CONDITION; Можно или задать проверку ассерта по по заднему фронту -- psl default clock is falling_edge (clk); -- psl assert always CONDITION; Часто для свойств применяется форма импликации, которая включает предварительное условие, которое должно быть выполнено до того, как основное условие будет проверено: assert always PRECONDITION -> CONDITION; Данное утверждение означает, что всякий раз, когда выполняется предусловие PRECONDITION, условие CONDITION должно удовлетворяться в том же цикле. Символ -> обозначает логическую импликацию (см. табл. 1). Для предварительного условия и основного условия, в пределах утверждения, используется форма временной последовательности, заключенной в фигурные скобки: assert always {a;b} |-> {c;d}; Последовательность {a; b} выполняется, если условие a верно в текущем цикле, а условие b - в следующем. Символ |->, находящийся между двумя последовательностями, обозначает суффиксную импликацию (suffix implication), это значит, что если первая последовательность выполняется, то вторая также должна выполняться, причем две последовательности пересекаются в одном цикле. Ассерт может быть задан через свойство, например, в фрагменте PSLкода
-- psl default clock is rising_edge(clk);
-- psl property prop1 is
-- never {state=a2; state=a5};
-- psl as1: assert prop1;
сначала задается по умолчанию проверка свойств по переднему фронту сигнала clk, затем определяется свойство prop1, после чего и записывается утверждение as1. Функция rising_edge(clk) – это функция определения переднего фронта сигнала clk. Свойство prop1 состоит в том, что никогда не должны быть в соседних тактах сначала a2, затем a5. Если будет последовательность {a2, a5}, то утверждение as1 на начало второго такта будет зафиксировано, как ложное. В PSL для ассерта можно записать свое отдельное тактирование, так как в PSL имеются встроенные функции rose, fell тактирования: @rose(clk); – тактирование по переднему фронту сигнала clk; @fell(clk); – тактирование по заднему фронту сигнала clk. Можно для разных ассертов использовать различные сигналы синхронизации: -- psl as1: assert always (b and f) or c @rose(clk1); -- psl as2: assert never (b or f) and c @fell(clk2);
Слайд:Ассерты и директивы покрытия
Директивы покрытия используют ключевое слово cover и собирают информацию о частоте выполнения свойств. Директивы cover отмечают такты и подсчитывают общее число тактов, в которых свойство выполнено.
-- psl default clock is rising_edge(clk); -- psl as1: assert always (a <-> b ); -- psl cov1: cover (a <-> b );
Слайд:Последовательности
Для обозначения перемещения вперед (вправо) на один такт внутри одной последовательности выбран оператор «точка с запятой». Фигурные скобки отмечают начало и конец последовательности. Последовательность (объединение, конкатенация) двух событий a, b обозначается через {a; b}; и понимается так: a выполняется в текущем такте синхросигнала, b выполняется в следующем такте.
Слайд:Компактные обозначения для последовательностей
Для задания повторяющегося события a используются следующие компактные обозначения:
{a[*2]} означает {a;a};
{a[+]} означает {a;a;...;a} с повторением один или более раз;
{a[*]} означает {a;a;...;a} с повторением один или более раз, или не повторяясь вообще;
{[*]} соответствует любой последовательности;
{a[=2]} означает {[*];a;[*];a;[*]}, т. е. непоследовательные повторения;
{a[*1 to 3]} означает {a} или {a;a} или {a;a;a};.
PSL использует последовательности и множества последовательностей.
Из последовательностей могут быть образованы другие последовательности.
Рассмотрим временную диаграмму для перечислимого сигнала sig, который имеет тип state
type state is (a, b); signal sig : state; signal Clk : std_logic := '1'; -- psl default clock is rising_edge(clk); -- psl asp2: assert always {(sig = a);(sig = b[*2])};
Слайд:Примеры операторов неупорядоченного повторения
{a; b[=i]; c} – сигнал b должен появиться i раз (не обязательно в последовательных тактах);
{a; b[=0 to j]; c} – сигнал b должен появиться j раз или меньше на протяжении всей цепочки (также нет ограничения на соседство тактов выполнения);
{a; b[=i to inf]; c} – сигнал b должен появиться как минимум i раз (также нет ограничения на соседство тактов выполнения).
Для операторов [->]:
{a; b[->i]; c} – цепочка повторов b должна завершаться на такте, в котором сигнал занятости b становится активным i-ый раз;
{a; b[->i to j]; c} – количество повторов b должно быть от i до j раз, последний повтор b должен совпадать с окончанием цепочки.
Ключевое PSL слово inf означает максимальное (нефиксированное) значение правой части временного интервала [i to inf], в качестве inf понимается целое число, большее i.
Слайд:Временной PSL оператор next
Временной оператор next (следующий) является одним из важнейших, так как он связывает текущее состояние проекта со следующим состоянием
Различные варианты PSL оператора next
| Оператор | Описание |
|---|---|
| next p | p выполняется в следующем такте, если есть такой такт |
| next! p | p выполняется в следующем такте и такой такт должен быть |
| next[n] p | p выполняется в n-ом такте, если имеется такой такт |
| next![n] p | p выполняется в n-ом такте, и такой такт должен быть |
| next_e[m to n](p) | p выполняется в одном из тактов временного интервала [m to n] |
| next_e | p выполняется в одном из тактов временного интервала [m to n] и такой такт должен быть |
| next_a[m to n](p) | p выполняется во всех тактах временного интервала [m to n] |
| next_a | p выполняется во всех тактах временного интервала [m to n] и должны быть такие такты |
Слайд:Временной PSL оператор until
| Оператор | Смысл |
|---|---|
| p until q | p должен выполняться до выполнения q; если q никогда не выполнится, то p не выполнится до конца моделирования |
| p until! q | p должен выполняться до выполнения q; при этом q в конце концов должно выполниться |
| p until_ q | p должен выполняться до выполнения q (с пересечением выполнения p, q в одном такте); если q никогда не выполнится, то p не выполнится до конца моделирования |
| p until!_ q | p должен выполняться до выполнения q (с пересечением выполнения p, q в одном такте); при этом q в конце концов должно выполниться |
Оператор until*: левый операнд выполняется в любое время до выполнения правого операнда. Ассерт
assert always (b until c);
утверждает, что сигнал b должен быть выполнен (быть в единичном значении) в любом такте до такта, где выполнен сигнал с. При этом нет обязательного значения для сигнала b в такте, где c выполнен (равен 1). Для ассерта
assert always (b until_ c);
единичное значение b и единичное значение сигнала с должны перекрываться в одном такте. Рассмотрим временную диаграмму для ассертов
-- psl default clock is rising_edge(clk); -- psl as1: assert always (b until c); -- psl as2: assert always (b until_ c);
В этом примере в такте 1: с=1, поэтому ассерт as1 выполнен, ибо нет требований к значению сигнала b. В такте 2 сигнал b в единичном значении и сигнал с в единичном значении, ассерт выполнен (b принял значение в любом такте (в том же самом), где с принял единичное значение). Аналогично и для тактов 3, 4. В такте 6 ассерт as1 стартовал (левый операнд выражения «b until c» выполнился, но в следующем 7-ом такте выяснилось, что с не стал равным 1). Поэтому ассерт не выполнился и поэтому в такте 7 стоит два черных треугольника невыполнения ассерта as1. Второй черный треугольник из-за того, что в седьмом такте ассерт тоже стартовал, но не выполнился, проанализировав значения сигналов в седьмом такте. Ассерт as1 выполнился в такте 9, 10, так как в этих тактах значение с=1, а сигнал b принял единичное значение раньше (в такте 6).
Ассерт as2 два раза выполнен, однако в тактах 9, 10 единичные значения сигналов b, c не перекрываются, поэтому ассерт as2 на этих тактах не выполняется. Если же сигнал b везде равен 0, то ассерт as1 на временной диаграмме не изменится, а ассерт as2 ни разу не выполнится – не будет перекрытия тактов с единичными значениями сигналов b, c.
Слайд:Временной PSL оператор before
| Оператор | Описание |
|---|---|
| a before b | a выполнится до того, как выполнится b; если a никогда не выполнится, так же не выполнится и b |
| a before! b | a выполнится до того, как выполнится b; в конце концов a выполняется |
| a before_ b | a выполнится до того как выполнится b (с пересечением выполнения в одном такте); если a никогда не выполнится, так же не выполнится и b |
| a before!_ b | a выполнится до того как выполнится b (с пересечением выполнения в одном такте); в конце концов a выполняется |
Оператор «a before b» требует, чтобы левый операнд a выполнялся строго перед правым операндом b. Подчеркивание всегда обозначает перекрытие в такте, в этом случае перекрытие в операторе before_ означает, что выполнение a и b может перекрыться. Рассмотрим ассерты
-- psl default clock is rising_edge(clk); -- psl as1: assert always (a before b); -- psl as2: assert always (a before_ b);
Сравнение PSL операторов before,before_
| Значение a в одном из строго предыдущих тактов | Значение b в текущем такте | a before b | a before_ b |
|---|---|---|---|
| 0 | 0 | Нет отметки о выполнении либо невыполнении ассерта | Нет отметки о выполнении либо невыполнении ассерта |
| 0 | 1 | Ассерт не выполнен | Ассерт не выполнен |
| 1 | 0 | Ассерт выполнен | Ассерт выполнен |
| 1 | 1 | Ассерт не выполнен | Ассерт выполнен |
