отправка...Проектирование в условиях временных ограничений: верификация проектов на основе ПЛИС. Часть 3
Авторы продолжают рассмотрение вопросов верификации аппаратуры, и потому включили в данную статью краткий обзор возможностей применения открытой библиотеки верификации OVL (Open Verification Library).
Все статьи цикла:
- Проектирование в условиях временных ограничений: верификация проектов на основе ПЛИС. Часть 1, (Компоненты и технологии №3’2008)
- Проектирование в условиях временных ограничений: верификация проектов на основе ПЛИС. Часть 2, (Компоненты и технологии №5’2008)
- Проектирование в условиях временных ограничений: верификация проектов на основе ПЛИС. Часть 3, (Компоненты и технологии №6’2008)
- Проектирование в условиях временных ограничений: верификация проектов на основе ПЛИС. Часть 4, (Компоненты и технологии №8’2008)
Открытая библиотека верификации (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 Graphics — ModelSim. Однако, учитывая основную тематику статьи, лучше ориентироваться на аналогичную по функциональности версию с расширенными возможностями в области верификации — QuestaSim.
Для проведения моделирования с целью изучения принципов использования мониторов утверждений библиотеки OVL необходимо выполнить следующую последовательность действий:
- Запустить программу QuestaSim.
- Создать новый проект (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 (объявление компонентов, типов, констант и т. д.).
- Скомпилировать проект.
- Провести моделирование разработанной системы. Убедиться в правильности функционирования светофора.
- Изменить в файле Traffic_Light_Controller.vhd для одного из состояний Si значения выходных сигналов TRANSPORT_LIGHT и PEDESTRIAN_LIGHT таким образом, чтобы они одновременно имели значение GREEN (имитация ошибки при написании кода контроллера светофора).
- Скомпилировать проект.
- Провести моделирование разработанной системы. В окне сообщений (transcript) основного окна QuestaSim наблюдать появление сообщения “TRAFFIC ACCIDENT”.
Искусственное внесение ошибки необходимо для визуализации работы монитора. В противном случае, при условии правильности описанной модели, монитор не сработает в ходе моделирования.
Результат выполнения моделирования HDL-программы с внесенной ошибкой приведен на рис. 3.
Положительный эффект применения монитора верификации в данном случае может показаться сомнительным, ведь состояние, в котором зеленый свет горит в оба направления, отчетливо видно на временной диаграмме. Однако простота рассматриваемого примера не должна вводить в заблуждение. Во-первых, сложность современных систем на порядок превосходит разобранный пример (по числу сигналов, сложности их поведения и т. д.). Во-вторых, анализируемое логическое условие в реальных системах выглядит сложнее, чем просто сравнение значений двух сигналов (для примера был выбран один из самых простых мониторов библиотеки OVL). И, наконец, в-третьих, использование мониторов позволяет в большей степени исключить человеческий фактор из процедуры проверки правильности описания — информация о свойствах системы располагается не в памяти специалиста по верификации (точнее не только в ней), а формально записана в коде устройства.
Логическим продолжением рассмотренного примера будет обсуждение вопросов применения мониторов библиотеки OVL и описание их возможностей, а также перспектив развития верификационных средств. Этому будет посвящена следующая статья цикла «Проектирование в условиях временных ограничений: Верификация проектов».
Окончание следует
Литература
- Функционально-временная верификация сложных цифровых систем // Открытые системы. 2002. №6.
- Assertion Monitor Reference Manual. V. 03.10.14.
- Максфилд К. Проектирование на ПЛИС. Архитектура, средства и методы. Курс молодого бойца. М.: Додека-XXI, 2007.
- Foster H., Krolnik A., Lacey D. Assertion-Based Design. Kluwer Academic Publisher, 2004.
- 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