1.4. Синтез ассерций

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

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

Рис. 1.5. Синтез ассерций при верификации

Современная методология верификации включает сочетание направленного и случайного моделирования на основе ограничений, формальных и полуформальных методов, эмуляции.

Направленное моделирование (directed simulation) использует проверочные устройства в виде черных ящиков, которые тестируют входные и выходные характеристики каждой функции взаимодействия. Данный подход не допускает масштабирования из-за наличия большого количества сложных взаимодействий между функциями.

Случайное моделирование на основе ограничений (constrained random simulation) использует внешнее проверочное устройство для определения ожидаемого поведения тестируемого устройства (Design under Test, DUT). В процессе моделирования выход тестируемого устройства сравнивается с выходом проверочного устройства, и несоответствие фиксируется как ошибка. Проверочное и тестируемое устройства, как правило, разрабатываются независимо друг от друга на основе архитектурной спецификации. Сложно создать проверочное устройство, полностью соответствующее DUT. Поэтому при внешней проверке часто пропускаются свойства и взаимодействия, влияюшие на производительность системы, связанные с исключениями и прерываниями.

Формальная верификация (formal verification) использует математический анализ для доказательства или опровержения определенных свойств системы для всех возможных допустимых входных стимулов. Полная верификация с использованием формальных методов требует определения необходимых свойств для покрытия всех функций проекта.

Эмуляция (emulation) использует специальные аппаратные средства для проверки тестируемого устройства с гораздо большей скоростью, чем при моделировании. Она имеет те же недостатки, что и случайное моделирование на основе ограничений, связанные с использованием внешнего проверяющего устройства. В частности может быть затруднена локализация и отладка ошибок при неудачном завершении эмуляции.

Эффективность всех описанных методов зависит от качества спецификации, в которой определяется сочетание следующих компонентов:

• ассерций в виде прозрачного ящика и проверочного устройства в виде черного ящика для описания поведения проекта на RTL уровне;

• точек функционального покрытия для обеспечения соответствующих тестовых стимулов.

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

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

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

Синтез ассерций – это технология, которая позволяет автоматически генерировать высокоэффективные утверждения для проверки ключевых ограничений и спецификации проекта, атрибутов функционального покрытия, выявляющих пробелы в testbench (рис. 1.6). Синтез ассерций может быть реализован в цифровом проекте так, как показано на рис. 1.7.

Рис. 1.6. Синтез ассерций

Рис. 1.7. Синтез ассерций как часть процесса моделирования, формальной верификации и эмуляции

RTL проект и тестовая информация являются входными данными для синтеза ассерций. Результаты автоматического синтеза формируются в стандартных форматах SVA, PSL и Synthesizable Verilog.