Функциональная проверка - Functional verification

В автоматизация проектирования электроники, функциональная проверка является задачей проверки того, что логический дизайн соответствует спецификации. Говоря обыденным языком, функциональная проверка пытается ответить на вопрос: «Делает ли предлагаемая конструкция то, что задумано?» Это сложная задача, которая требует много времени и усилий в большинстве крупных проектов по проектированию электронных систем. Функциональная проверка является частью более всеобъемлющего проверка конструкции, который, помимо функциональной проверки, учитывает нефункциональные аспекты, такие как время, компоновка и мощность.

Функциональная проверка очень сложна из-за огромного количества возможных тестовых примеров, которые существуют даже в простом проекте. Часто существует более 10 ^ 80 возможных тестов для всесторонней проверки конструкции - число, которое невозможно достичь за весь срок службы. Это усилие эквивалентно проверка программы, и является NP-жесткий или даже хуже - и не было найдено решения, которое бы хорошо работало во всех случаях. Однако его можно атаковать многими методами. Ни один из них не идеален, но каждый может быть полезен в определенных обстоятельствах:

  • Логическое моделирование имитирует логику до ее построения.
  • Ускорение моделирования применяет специальное оборудование к задаче логического моделирования.
  • Эмуляция строит версию системы, используя программируемую логику. Это дорого и все же намного медленнее, чем реальное оборудование, но на порядки быстрее, чем моделирование. Его можно использовать, например, для загрузки операционной системы на процессоре.
  • Формальная проверка попытки математически доказать, что определенные требования (также выраженные формально) выполняются или что определенные нежелательные поведения (например, тупик) не могут возникнуть.
  • Интеллектуальная проверка использует автоматизацию для адаптации тестовой среды к изменениям в зарегистрировать уровень передачи код.
  • Специфичные для HDL версии ворсинок, и другие эвристики, используются для поиска общих проблем.

Проверка на основе моделирования (также называемая 'динамическая проверка ') широко используется для «моделирования» конструкции, поскольку этот метод очень легко масштабируется. Предоставляется стимул для тренировки каждой строчки кода HDL. Испытательный стенд создан для функциональной проверки проекта, предоставляя содержательные сценарии для проверки того, что при определенных входных данных проект соответствует спецификации.

Среда моделирования обычно состоит из нескольких типов компонентов:

  • В генератор генерирует входные векторы, которые используются для поиска аномалий, существующих между намерением (спецификациями) и реализацией (HDL-код). Этот тип генератора использует NP-полный тип SAT Solver, который может быть дорогостоящим в вычислительном отношении. К другим типам генераторов относятся вручную созданные векторы, собственные генераторы графических генераторов (GBM). Современные генераторы создают направленные случайные и случайные стимулы, которые управляются статистически для проверки случайных частей дизайна. Случайность важна для достижения высокого распределения доступных входных стимулов в огромном пространстве. С этой целью пользователи этих генераторов намеренно занижают требования к созданным тестам. Задача генератора - случайным образом заполнить этот пробел. Этот механизм позволяет генератору создавать входные данные, которые выявляют ошибки, которые не ищутся непосредственно пользователем. Генераторы также смещают стимулы в сторону угловых вариантов дизайна, чтобы еще больше подчеркнуть логику. Смещение и случайность служат разным целям, и между ними есть компромиссы, поэтому разные генераторы имеют разное сочетание этих характеристик. Поскольку входные данные для дизайна должны быть действительными (законными) и должны поддерживаться многие цели (например, смещение), многие генераторы используют проблема удовлетворения ограничений (CSP) для решения сложных задач тестирования. Смоделирована законность исходных данных и арсенал смещения. Генераторы, основанные на моделях, используют эту модель для создания правильных стимулов для целевого дизайна.
  • В водители преобразуйте стимулы, создаваемые генератором, в фактические входные данные для проверяемого проекта. Генераторы создают входные данные на высоком уровне абстракции, а именно в виде транзакций или языка ассемблера. Драйверы преобразуют эти входные данные в фактические входные данные проекта, как определено в спецификации интерфейса проекта.
  • В симулятор производит выходные данные проекта на основе текущего состояния проекта (состояния триггеров) и введенных входов. В симуляторе есть описание сетевого списка дизайна. Это описание создается путем синтеза HDL в список цепей низкого уровня шлюза.
  • В монитор преобразует состояние дизайна и его выходы на уровень абстракции транзакции, чтобы его можно было сохранить в базе данных «табло» для последующей проверки.
  • Проверяющий проверяет, является ли содержание «табло» законным. Бывают случаи, когда генератор создает ожидаемые результаты в дополнение к входным данным. В этих случаях средство проверки должно проверить соответствие фактических результатов ожидаемым.
  • Арбитражный менеджер управляет всеми вышеуказанными компонентами вместе.

Разные покрытие метрики определены для оценки того, что проект был должным образом отработан. К ним относятся функциональное покрытие (были ли реализованы все функциональные возможности проекта?), Покрытие операторов (выполнялась ли каждая строка HDL?) И покрытие ветвей (было ли выполнено каждое направление каждой ветви?).

Инструменты

Смотрите также

Рекомендации