1.3. Верификация на основе ассерций

Непрерывное увеличение сложности систем на кристаллах привело к тому, что традиционные подходы к верификации уже не могут быть эффективно использованы из-за наличия ограничений, связанных с ухyдшением наблюдаемости и управляемости внутренних линий системы [22].

Верификация на основе ассерций (Assertion-Based Verification, ABV) определена в качестве новой стратегии, обеспечивающей высокое качество изделия и сокращение времени выхода его на рынок [32]. Ассерции используются для захвата информации о поведении проекта во времени. После чего проект может быть верифицирован в отношении ассерций с использованием методов моделирования и/или статической верификации в целях проверки соответствия спецификации.

Верификация ABV получила мощный импульс развития в течение последних лет, о чем свидетельствует рост количества проверенных с помощью ABV проектов, публикаций в данной области и коммерческих предложений. Значительной составляющей этого импульса стал официальный выбор языка PSL [33], основанного на языке Sugar IBM, в качестве промышленного стандарта. В большинстве промышленных предприятий ABV используют как часть традиционной методологии моделирования.

SystemC разработан в качестве платформы для верификации SoC и совместной hardware/software ко-верификации. SystemC представляет собой набор библиотек C++, которые позволяют формировать описания аппаратных модулей на языке C++, и содержит классы, которые имитируют низкоуровневые (регистры) и высокоуровневые (каналы) аппаратные конструкции.

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

PSL состоит из четырех слоев:

1. Булев слой, состоящий из логических выражений, содержит также логические операторы AND, OR, XOR.

2. Временной слой, состоящий из временных выражений или свойств, которые описывают отношения между логическими (булевыми) выражениями во времени.

3. Верификационный слой, состоящий из директив, которые описывают, порядок обработки временных выражений средствами верификации.

4. Слой моделирования, обеспечивающий средства для поведенческого моделирования проекта, позволяет использовать вспомогательные сигналы и переменные.

ANSI-C ассерции в сочетании с testbench могут быть использованы в качестве методологии верификации для определения и тестирования поведения приложения. Каждая отдельная ассерция используется для проверки логических (булевых) выражений в реальном времени, описывающих правильное функционирование приложения. Если выражение принимает значение ложь, ассерция выдает информацию о неудаче в стандартный поток ошибок, указывая имя файла, номер строки, имя функции и выражение, которое «сработало». После чего выполнение программы прерывается [23].

Встроенные ассерции интегрируются в приложение путем генерации единственного модуля проверки и предупреждения для каждой ассерции (рис. 1.4). Модуль проверки ассерции реализует соответствующее булево выражение путем извлечения необходимых и вычисления промежуточных данных. Функция предупреждения сигнализирует о неудаче (ошибке).

Рис. 1.4. Структура ассерций

Функция предупреждения ассерции может работать одновременно с приложением в качестве задачи, ожидающей сообщения об ошибке от модуля проверки ассерции. По существу, задача определена как большой переключательный оператор switch на канал связи, который реализует один вариант для каждой аппаратно отображаемой ассерции.

Один из возможных способов синтеза модуля проверки ассерций заключается в следующем. Семантически ассерция подобна оператору if. Следовательно, модуль может быть синтезирован путем преобразования каждой ассерции в оператор if, условие которого соответствует логическому выражению ассерции. Описанная простая процедура может быть применена в большинстве приложений, но в целом такое преобразование приводит к увеличению накладных расходов. Для решения данной проблемы используются три категории оптимизации, позволяющие улучшить масштабируемость и прозрачность встроенных ассерций [23, 38]:

1) Распараллеливание ассерций. Для обеспечения максимальной прозрачности встроенных ассерций схемы их проверки должны иметь минимальное влияние на производительность исходного приложения. Однако синтез ассерций через прямое преобразование в оператор if изменяет граф управления и конечный автомат, что добавляет произвольную задержку, зависящую от сложности выражения ассерции. Средства высокоуровневого синтеза могут свести к минимуму влияние ассерций на граф управления путем распараллеливания ассерций и исходного приложения. Для этого каждая ассерция преобразуется в отдельную задачу, которая выполняется независимо от задачи исходного приложения. Вместо ожидания результата проверки ассерции приложение передает данные, необходимые для задачи ассерции, и затем продолжает работу. Распараллеливание не может полностью устранить накладные расходы из-за необходимости разделения обще памяти RAM.

2) Дублирование ресурсов. Позволяет минимизировать накладные расходы путем дублирования разделяемых ресурсов (например, портов модулей памяти, которые одновременно используются прикладными и ассерционными задачами). При доступе к памяти из разных источников необходимо мультиплексирование данных по времени для задач, формирующих накладные расходы. Средства высокоуровневого синтеза могут увеличить количество портов путем дублирования разделяемого блока RAM, таким образом, что все экземпляры памяти обновляются одновременно при выполнении каждой задачи. Это гарантирует, что все экземпляры содержат одинаковые данные и отсутствует задержка доступа к информации для исполняемых задач. Дублирование ресурса позволяет снизить накладные расходы за счет увеличения объема служебных данных.

3) Разделение ресурсов. В общем случае цепь проверки ассерции может характеризоваться собственными накладными расходами из-за необходимости проверить условие ассерции. Средства высокоуровневого синтеза могут свести к минимуму указанные накладные расходы за счет разделения ресурсов между ассерциями. При этом возникает проблема, связанная с тем, что ассерции могут затребовать один и тот же ресурс в одно время. Средства высокоуровневого синтеза могут использовать существующие методы разделения ресурсов для ассерций, не относящихся к конвейерным областям отдельной задачи, поскольку они гарантированно не начинаются в одно время. Для решения указанной проблемы средства высокоуровневого синтеза могут имплементировать все ассерции, разделяющие ресурсы, в виде конвейера, запускающего новую ассерцию в каждом цикле. Разделение ресурсов потенциально может быть расширено на произвольное число одновременных ассерций различных задач за счет синтеза конвейерных схем проверки ассерций. Для предотвращения одновременного доступа к разделяемым ресурсам может быть использована буферизация данных различных ассерций с использованием схемы FIFO и последующей их циклической обработкой.