Разработка утверждений, которые бы в полной мере проверяли поведение устройства, задача нетривиальная. Одно дело, когда пишутся утверждения для таких распространенных протоколов, как 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 утверждений.