Подписка на новости

Опрос

Нужны ли комментарии к статьям? Комментировали бы вы?

Реклама

 

2008 №6

Проектирование в условиях временных ограничений: верификация проектов на основе ПЛИС. Часть 3

Михайлов Максим  
Грушвицкий Ростислав  

Авторы продолжают рассмотрение вопросов верификации аппаратуры, и потому включили в данную статью краткий обзор возможностей применения открытой библиотеки верификации OVL (Open Verification Library).

Все статьи цикла:

Открытая библиотека верификации (OVL)

Как уже отмечалось во вступительной статье цикла, структурная и функциональная сложность современных систем весьма внушительна — миллионы логических вентилей, функции сотен и тысяч переменных. Это делает актуальной задачу верификации, то есть подтверждения того, что описание проекта, по которому микросхема будет реализована «в кремнии», полностью соответствует спецификации (техническому заданию) проектируемой системы [1].

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

Отмеченная сложность проектируемых систем означает невозможность «ручного» анализа правильности результатов разработки и указывает на то, что процедура верификации может быть очень длительной. Между тем, в современной электронной промышленности отрезок времени от начала разработки до выхода на рынок — один из наиболее критичных экономических показателей.

Использование в качестве инструмента верификации языка PSL хотя и оказывается эффективным, но все же сопряжено с некоторыми существенными трудностями. Применение языка требует высокой квалификации разработчика и хорошего знания базовых конструкций. При этом объем кода, создаваемого для целей верификации, весьма значителен.

Пожалуй, самым простым и доступным средством повышения скорости и надежности описания верифицируемого проекта являются мониторы утверждений библиотеки OVL, разработанной фирмой Accellera. Существует две версии библиотеки OVL, функциональность которых определяется, прежде всего, особенностями используемых языков описания аппаратуры — VHDL или Verilog. Разработанные фирмой модули покрывают широкий диапазон типовых проблем верификации. Отлаженное функционирование библиотечных элементов облегчает обнаружение ошибок. Полный список всех мониторов, предназначенных для проверки специфических свойств систем, находится в свободном доступе в Интернете по адресу http://www.accellera.org/activities/ovl/. Другим не менее важным ресурсом является сайт пользователей библиотекой OVL — http://www.eda.org/ovl/.

Мониторы утверждений — это объявленные в проекте компоненты, цель использования которых — гарантирование выполнения некоторых условий. Здесь прослеживается явное сходство с понятием утверждение (assertion). Мониторы должны проверять истинность указанных событий и в случае неудачи сообщать об этом проектировщику, а также классифицировать ошибку, в зависимости от серьезности обнаруженного расхождения между предполагаемым и свершившимся событием. При этом допустимо использование мониторов как для моделирования, так и для формальной верификации.

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

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

Обычно каждый монитор утверждений ассоциируется с определенным свойством, которое формулирует потенциальную проблему.

Обязательными параметрами для любого монитора OVL являются:

  • severity_level — определяет уровень важности ошибки, зафиксированной монитором. Конкретные значения этого параметра зависят от используемой САПР. Например, в пакете QuestaSim в библиотеке std описаны следующие возможности: note, warning, error и failure.
  • options — дополнительный параметр, характеризующий специфические свойства мониторов. Также во многом зависит от САПР.
  • msg — строка, отображаемая на экране при срабатывании монитора.

Разные мониторы могут иметь различное количество и назначение портов. Общим является только то, что все эти порты входные.

Ознакомление с применением мониторов OVL удобнее всего начать с анализа конкретного примера. В качестве такового была выбрана модель управления светофором.

Описание системы

Контроллер светофора предназначен для управления дорожным движением на перекрестках путем переключения соответствующих сигналов. Эта задача — достаточно тривиальна и часто описывается в различных источниках для пояснения принципов использования языковых средств. В руководстве по работе с библиотекой OVL [2] приведена реализация подобного алгоритма на языке Verilog. Однако в данной статье прямому заимствованию этого кода авторы предпочли написание собственной модели на языке VHDL. Структурная схема разрабатываемого устройства приведена на рис. 1.

Структурная схема устройства

Назначение отдельных модулей:

  • Автомат управления, он реализует основной алгоритм работы светофора. Граф переходов и выходов автомата приведен на рис. 2.
Граф автомата управления светофором

По сигналу сброса RESET автомат переходит в состояние S0 и остается в нем до появления сигнала CROSSING_REQUEST (пешеход нажал кнопку — запрос на переход перекрестка). При переходе в состояние S1 запускается таймер 1 (fireX[1] <= '1'). При его переполнении активируется сигнал tX[1] и автомат переходит в состояние S2. Аналогичным образом происходит запуск таймера 2, переход в S3, запуск таймера 3, переход в S4. Переключение между состояниями S4–S5 (с периодом, управляемым таймером 0) имитирует мигание зеленого сигнала светофора для пешехода. Длительность мигания определяется таймером 2. Далее через промежуточное состояние S6 автомат возвращается в начальное состояние S0.

Выходные сигналы автомата (TRANSPORT_LIGHT и PEDESTRIAN_LIGHT — сигналы светофора для транспорта и пешеходов соответственно) определяются текущим состоянием автомата. На рис. 2 цвета закодированы следующим образом: G (GREEN)— зеленый, Y (YELLOW) — желтый, R (RED) — красный.

  • Блок таймеров реализует временные задержки сигналов светофора.
  • Модуль верхнего уровня иерархии задает структуру светофора.
  • Блок мониторов утверждения. Текст HDL-программы содержит только один монитор — assert_never, подробная работа которого будет рассмотрена далее.

Назначение отдельных сигналов схемы, приведенной на рис. 1, представлено в таблице.

Таблица. Назначение сигналов
Назначение сигналов

Листинг HDL-программы

Для удобства выполнения практических работ с приведенным далее HDL-кодом он может быть в любое время получен в электронном виде. Для этого достаточно связаться с авторами по указанным адресам электронной почты.

В компоненте DUT реализован testbench для проведения моделирования в среде QuestaSim. Кроме того, здесь же формируется логическое выражение, результат которого (сигнал BOOL) будет отслеживать монитор утверждений, и объявляется сам монитор — both_are_green:

Компонент traffic_light описывает структуру светофора: взаимосвязь контроллера светофора (controller) и четырех таймеров (timerX_inst):

В пакете tl_lib происходит объявление необходимых компонентов, типов, констант и т. д.:

Компонент traffic_light_controller реализует основной алгоритм устройства управления работой светофора (описан с помощью конечного автомата):

Компонент timerX описывает поведение таймера, который используется для реализации временных задержек:

Компонент assert_never реализует монитор утверждения. Данное описание было скопировано с официального сайта фирмы Accellera (заголовок файла, содержащий комментарии, вырезан, так как не представляет особого интереса). Пояснение к работе этого монитора будет приведено после кода:

Файл Ovl_assert.vhd также получен с www.accellera.org. Содержащийся в нем пакет декларирует все существующие мониторы библиотеки OVL и приведен здесь в сокращенном виде, так как для той цели, которую авторы поставили в данной статье, важен только один конкретный монитор:

Монитор assert_never

Для монитора assert_never определены следующие порты:

  • clk — сигнал тактирования, по фронту которого проверяется тестовое выражение test_expr.
  • reset_n — сигнал сброса (активный уровень — '0').
  • test_expr — свойство системы, записанное с помощью булевского выражение. Результат проверки выражения — TRUE или FALSE.

Монитор assert_never позволяет проверить свойство системы, которое никогда не должно быть оценено как истина (TRUE). Применительно к разрабатываемой системе таким свойством, например, может выступать — «сигнал светофора не должен быть зеленым одновременно для транспорта и пешехода». В том случае, если свойство нарушено, произойдет срабатывание монитора (вывод строкового параметра msg на экран). В зависимости от уровня важности ошибки моделирование может быть остановлено или продолжено. Вместе с сообщением в окно моделировщика выводится время срабатывания монитора.

Поддержка САПР

Одним из доказательств простоты применения средства OVL в сравнении с языком PSL является поддержка САПР. Поскольку мониторы утверждений библиотеки OVL построены на основе стандартных языков описания аппаратуры, то для работы с ними подойдет любая САПР, поддерживающая стандарт IEEE-1076 (IEEE Standard VHDL Language Reference Manual). Количество средств моделирования описаний на стандартном языке VHDL явно превышает количество аналогичных продуктов с поддержкой PSL на данный момент. Однако, справедливости ради, стоит отметить, что в последнюю версию стандарта IEEE-1076 язык PSL уже интегрирован [5].

Один из самых распространенных — программный продукт фирмы Mentor GraphicsModelSim. Однако, учитывая основную тематику статьи, лучше ориентироваться на аналогичную по функциональности версию с расширенными возможностями в области верификации — QuestaSim.

Для проведения моделирования с целью изучения принципов использования мониторов утверждений библиотеки OVL необходимо выполнить следующую последовательность действий:

  1. Запустить программу QuestaSim.
  2. Создать новый проект (File > New > Project) и добавить в него файлы:
    • assert_never.vhd (описание монитора утверждения assert_never);
    • ovl_assert.vhd (объявление мониторов утверждения и сигналов);
    • Device_Under_Test.vhd (верхний уровень иерархии при моделировании);
    • Timer.vhd (алгоритм работы таймера);
    • Traffic_Light.vhd (структура светофора);
    • Traffic_Light_Controller.vhd (автомат управления светофором);
    • Traffic_Light_Library.vhd (объявление компонентов, типов, констант и т. д.).
  3. Скомпилировать проект.
  4. Провести моделирование разработанной системы. Убедиться в правильности функционирования светофора.
  5. Изменить в файле Traffic_Light_Controller.vhd для одного из состояний Si значения выходных сигналов TRANSPORT_LIGHT и PEDESTRIAN_LIGHT таким образом, чтобы они одновременно имели значение GREEN (имитация ошибки при написании кода контроллера светофора).
  6. Скомпилировать проект.
  7. Провести моделирование разработанной системы. В окне сообщений (transcript) основного окна QuestaSim наблюдать появление сообщения “TRAFFIC ACCIDENT”.

Искусственное внесение ошибки необходимо для визуализации работы монитора. В противном случае, при условии правильности описанной модели, монитор не сработает в ходе моделирования.

Результат выполнения моделирования HDL-программы с внесенной ошибкой приведен на рис. 3.

Временная диаграмма

Положительный эффект применения монитора верификации в данном случае может показаться сомнительным, ведь состояние, в котором зеленый свет горит в оба направления, отчетливо видно на временной диаграмме. Однако простота рассматриваемого примера не должна вводить в заблуждение. Во-первых, сложность современных систем на порядок превосходит разобранный пример (по числу сигналов, сложности их поведения и т. д.). Во-вторых, анализируемое логическое условие в реальных системах выглядит сложнее, чем просто сравнение значений двух сигналов (для примера был выбран один из самых простых мониторов библиотеки OVL). И, наконец, в-третьих, использование мониторов позволяет в большей степени исключить человеческий фактор из процедуры проверки правильности описания — информация о свойствах системы располагается не в памяти специалиста по верификации (точнее не только в ней), а формально записана в коде устройства.

Лог моделирования

Логическим продолжением рассмотренного примера будет обсуждение вопросов применения мониторов библиотеки OVL и описание их возможностей, а также перспектив развития верификационных средств. Этому будет посвящена следующая статья цикла «Проектирование в условиях временных ограничений: Верификация проектов».

Окончание следует

Литература

  1. Функционально-временная верификация сложных цифровых систем // Открытые системы. 2002. №6.
  2. Assertion Monitor Reference Manual. V. 03.10.14.
  3. Максфилд К. Проектирование на ПЛИС. Архитектура, средства и методы. Курс молодого бойца. М.: Додека-XXI, 2007.
  4. Foster H., Krolnik A., Lacey D. Assertion-Based Design. Kluwer Academic Publisher, 2004.
  5. Accellera Continues to Promote Increased Electronic Design Productivity with Revised VHDL Standard, Oct. 9, 2006. http://www.haifa.ibm.com/projects/verification/sugar/papers/accellera_vhdlVHDL_press_release_psl_inside2006.pdf

Скачать статью в формате PDF  Скачать статью Компоненты и технологии PDF

 


Другие статьи по данной теме:

Сообщить об ошибке