В электронной автоматизации проектирования , функциональная проверка является задача проверки того, что логика проектирования Соответствует спецификации. Говоря обыденным языком, функциональная проверка пытается ответить на вопрос: «Делает ли предлагаемая конструкция то, что предполагается?» Это сложная задача, которая требует много времени и усилий в большинстве крупных проектов проектирования электронных систем. Функциональная проверка - это часть более всеобъемлющей проверки проекта , которая, помимо функциональной проверки, рассматривает нефункциональные аспекты, такие как синхронизация, компоновка и мощность.
Функциональная проверка очень сложна из-за огромного количества возможных тестовых примеров, которые существуют даже в простом проекте. Часто существует более 10 ^ 80 возможных тестов для всесторонней проверки конструкции - число, которое невозможно достичь за весь срок службы. Эти усилия эквивалентны верификации программы и являются NP-трудными или даже хуже - и не было найдено решения, которое бы хорошо работало во всех случаях. Однако его можно атаковать многими методами. Ни один из них не идеален, но каждый может быть полезен в определенных обстоятельствах:
- Логическое моделирование имитирует логику до ее построения.
- Ускорение моделирования применяет специальное оборудование к задаче логического моделирования.
- Эмуляция создает версию системы с использованием программируемой логики. Это дорого и все же намного медленнее, чем реальное оборудование, но на порядки быстрее, чем моделирование. Его можно использовать, например, для загрузки операционной системы на процессоре.
- Формальная проверка пытается математически доказать, что определенные требования (также выраженные формально) выполняются или что определенные нежелательные поведения (такие как тупик) не могут возникнуть.
- Интеллектуальная проверка использует автоматизацию для адаптации тестовой среды к изменениям кода уровня передачи регистров .
- Специфичные для HDL версии lint и другие эвристики используются для поиска распространенных проблем.
Проверка на основе моделирования (также называемая « динамической проверкой ») широко используется для «моделирования» проекта, поскольку этот метод очень легко масштабируется. Предоставляется стимул для тренировки каждой строчки HDL-кода. Испытательный стенд создан для функциональной проверки проекта путем предоставления значимых сценариев для проверки того, что при определенных входных данных проект соответствует спецификации.
Среда моделирования обычно состоит из нескольких типов компонентов:
- Генератор генерирует входные векторы, которые используются для поиска аномалий , которые существуют между намерением (спецификации) и реализацию (HDL кода). Этот тип генератора использует NP-полный тип SAT Solver, который может быть дорогостоящим в вычислительном отношении. Другие типы генераторов включают вручную созданные векторы, собственные генераторы на основе графов (GBM). Современные генераторы создают направленные случайные и случайные стимулы, которые статистически управляются для проверки случайных частей дизайна. Случайность важна для достижения высокого распределения доступных входных стимулов в огромном пространстве. С этой целью пользователи этих генераторов намеренно занижают требования к созданным тестам. Задача генератора - случайным образом заполнить этот пробел. Этот механизм позволяет генератору создавать входные данные, которые выявляют ошибки, которые не ищутся непосредственно пользователем. Генераторы также смещают стимулы в сторону угловых вариантов дизайна, чтобы еще больше подчеркнуть логику. Смещение и случайность служат разным целям, и между ними есть компромиссы, поэтому разные генераторы имеют разное сочетание этих характеристик. Поскольку входные данные для проектирования должны быть действительными (законными) и должны поддерживаться многие цели (например, смещение), многие генераторы используют метод задачи удовлетворения ограничений (CSP) для решения сложных требований тестирования. Смоделирована законность исходных данных и арсенал смещения. Основанные на модели генераторы используют эту модель для создания правильных стимулов для целевого дизайна.
- В водителях переводят стимулы , полученные с помощью генератора в фактические входы для разработки под контролем. Генераторы создают входные данные на высоком уровне абстракции, а именно в виде транзакций или языка ассемблера. Драйверы преобразуют эти входные данные в фактические входные данные проекта, как определено в спецификации интерфейса проекта.
- Тренажер производит выходы конструкции, основанные на текущем состоянии конструкции ( в состоянии триггеров) и инъекционные входы. В симуляторе есть описание сетевого списка дизайна. Это описание создается путем синтеза HDL в список цепей низкого уровня шлюза.
- Монитор преобразует состояние конструкции и ее выходы на уровень транзакций абстракции , поэтому он может быть сохранен в базе данных A «SCORE-бордах» , чтобы быть проверен позже.
- Проверяющий проверяет, что содержимое «табло» является допустимым. Бывают случаи, когда генератор создает ожидаемые результаты в дополнение к входным данным. В этих случаях средство проверки должно проверить соответствие фактических результатов ожидаемым.
- Арбитражный менеджер управляет всеми вышеперечисленными компонентами вместе.
Определены различные метрики покрытия для оценки того, что дизайн был должным образом отработан. К ним относятся функциональное покрытие (были ли реализованы все функциональные возможности проекта?), Покрытие операторов (выполнялась ли каждая строка HDL?) И покрытие ветвей (было ли выполнено каждое направление каждой ветви?).
Инструменты
- Альдек
- Стрелочные устройства
- Avery Design Systems: SimCluster (для параллельного логического моделирования) и Insight (для формальной проверки)
- Breker Verification Systems, Inc .: Trek (инструмент генерации тестов на основе моделей для сложных SoC)
- Системы дизайна Cadence
- EVE / ZeBu
- Наставник Графика
- Nusym Technology
- Программное обеспечение Obsidian
- Решения OneSpin
- Synopsys
- Valtrix Systems : Sting (универсальный инструмент проверки дизайна для сложных реализаций SoC / CPU)