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

Ссылки сюда (17) →

Лекции ПЦСЯОА

• Чеклист

---

Лекции

Лекция 1 Лекция 2 Лекция 3 Лекция 4 Лекция 5 Лекция 6 Лекция 7 Лекция 8 Лекция 9 Лекция 10 Лекция 11 Лекция 12

Лекция 13 Лекция 14 Лекция 15 Лекция 16 Лекция 17 Лекция 18 Лекция 19 Лекция 20 Лекция 21 Лекция 22 Лекция 23 Лекция 24

---

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

• Тест 1 - Основы VHDL
• Тест 2 - Вопросы по VHDL (простой уровень)

---

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

• Ссылки
• Книги
• Софт
  • Редактор Emacs
  • ModelSim
  • ISE
  • LeonardoSpectrum

---

• Форум
• Журнал
• План сдачи заданий
• Экзамен

Slide Show

Заголовок

Верификация с использованием языка 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);