Проектирование цифровых систем на языках описания аппаратуры/Лекция 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 операторы
Слайд:Простые свойства и тактирование
Простейшая форма свойства в 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 );