Подходы к применению SVA
Разработка утверждений, которые бы в полной мере проверяли поведение устройства, задача нетривиальная. Одно дело, когда пишутся утверждения для таких распространенных протоколов, как PCI, AMBA, OCP. Зачастую, спецификации к таким протоколам уже содержат описания проверок, которые необходимо реализовать с помощью утверждений, и в дальнейшем требуется только реализация. Если же встала задача разработки утверждений для специфичного устройства, то здесь рекомендуется следующий подход:
- Выделить в своем проекте типовые элементы (автоматы, АЛУ, арбитры, FIFO, памяти). Методика проверки этих блоков с помощью утверждений уже описана. Остается только применить эту методику с учетом особенностей вашего устройства, тем самым, сэкономив время. Реальные проекты редко состоят из одних типовых элементов, и работы по написанию утверждений все равно будет достаточно.
- Проверка всех комбинаций сигналов невозможна и не нужна, поэтому необходимо выделить в своем проекте ключевые функции, операции, состояния для проверки. Как писалось выше, от этого напрямую зависит эффективность верификации на основе утверждений.
- Выбрать место объявления утверждений. SVA могут быть объявлены напрямую в RTL-описании или вынесены в отдельный модуль.
- При тестировании аппаратуры часто встречаются типовые ситуации. Их описание с помощью
утверждений можно ускорить, используя специальные библиотеки, которые содержат утверждения,
наиболее часто используемые разработчиками. Можно выделить следующие библиотеки:
Open Verification Library (OVL) фирмы Accelera, Incisive Assertion Library
(IAL) фирмы Cadence, Questa Verification Library (QVL)
фирмы MentorGraphics и SystemVerilog Assertions Checker Library
фирмы Synopsys. Все эти библиотеки имеют в своем составе схожие наборы утверждений.
Для достижения максимального эффекта рекомендуется использовать библиотечные утверждения настолько полно, насколько это возможно, т.к. эти утверждения уже полностью отлажены и описаны в документации. - На этапе разработки спецификации следует составить план верификации, который содержит список ситуаций для проверки с помощью утверждений. В идеале, в написании утверждений должны принимать участие и команда разработчиков, и команда верификаторов. Это позволяет выявить некоторые ошибки в логике работы устройства. Утверждения, написанные разработчиком, описывают его предположения о работе устройства. Эти предположения могут быть не всегда достоверными, поэтому желательно вовлечь в процесс написания утверждений верификатора. Описать поведение внутренних сигналов может только разработчик, а верификатор проверяет соответствие устройства спецификации. План верификации для схемы на рис.1 представлен в таблице 1.
Таблица 1
План верификации
| Функциональность для проверки | Назначен для написания |
|---|---|
| Ведомый должен выставить сигнал CMD_ACCEPT в течение трех тактов после того, как ведущий выставил команду на шине CMD | Команде разработчиков |
| Адрес и данные не должны меняться, пока не появится сигнал CMD_ACCEPT | Команде разработчиков |
| Адрес не должен меняться, пока на шине CMD стоит команда | Команде верификаторов |
Желательно не пренебрегать написанием плана верификации. Это придает работе наглядность, позволяет найти идентичные утверждения. Все ситуации для проверки невозможно выделить на этапе разработки спецификации, также как и определить, кто будет писать то или иное утверждение, поэтому работа продолжается на этапах создания RTL-модели и верификации. Создание плана занимает некоторое время, но является важным этапом для успешного использования SystemVerilog утверждений.
