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

Функциональная проверка — это задача проверки соответствия логической конструкции спецификации. ^[1] Функциональная проверка пытается ответить на вопрос: «Делает ли предлагаемая конструкция то, что задумано?» ^[2] Это сложно и отнимает большую часть времени и усилий (до 70% времени проектирования и разработки). ^[1] в большинстве крупных проектов проектирования электронных систем. Функциональная проверка является частью более комплексной проверки проекта , которая, помимо функциональной проверки, учитывает нефункциональные аспекты, такие как время, компоновка и мощность. ^[3]

Предыстория [ править ]

Хотя количество транзисторов росло в геометрической прогрессии согласно закону Мура , увеличение количества инженеров и времени, затрачиваемого на создание проектов, увеличивается только линейно . По мере увеличения сложности транзисторов увеличивается и количество ошибок кодирования. Большинство ошибок в логическом кодировании происходит из-за небрежного кодирования (12,7%), недопонимания (11,4%) и проблем с микроархитектурой (9,3%). ^[1] Таким образом, автоматизации электронного проектирования создаются инструменты (EDA), позволяющие справиться со сложностью проектирования транзисторов. Такие языки, как Verilog и VHDL, представлены вместе с инструментами EDA. ^[1]

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

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

Типы [ править ]

Существует три типа функциональной верификации, а именно: динамическая функциональная, гибридная динамическая функционально-статическая и статическая верификация. ^[1]

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

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

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

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

См. также [ править ]

Ссылки [ править ]

^ Jump up to: ^а ^б ^с ^д ^и Молина, А; Каденас, О (8 сентября 2006 г.). «Функциональная верификация: подходы и проблемы» . Латиноамериканские прикладные исследования . 37 . ISSN 0327-0793 . Архивировано из оригинала 16 октября 2022 года . Проверено 12 октября 2022 г.
^ Резаян, Банафшех. «Методология моделирования и проверки автомобильных ИС смешанных сигналов». CiteSeerX 10.1.1.724.527 .
^ Страуд, Чарльз Э; Изменение, Яо-Чанг (2009). «ГЛАВА 1 – Введение» . Проверка дизайна . стр. 1–38. дои : 10.1016/B978-0-12-374364-0.50008-4 . ISBN 978-0-12-374364-0 . Архивировано из оригинала 12 октября 2022 года . Проверено 11 октября 2022 г. {{cite book}}: |journal= игнорируется ( помогите )

[Molina_2006-1] Jump up to: ^а ^б ^с ^д ^и Молина, А; Каденас, О (8 сентября 2006 г.). «Функциональная верификация: подходы и проблемы» . Латиноамериканские прикладные исследования . 37 . ISSN 0327-0793 . Архивировано из оригинала 16 октября 2022 года . Проверено 12 октября 2022 г.

[Lund-2] Резаян, Банафшех. «Методология моделирования и проверки автомобильных ИС смешанных сигналов». CiteSeerX 10.1.1.724.527 .

[EDA-3] Страуд, Чарльз Э; Изменение, Яо-Чанг (2009). «ГЛАВА 1 – Введение» . Проверка дизайна . стр. 1–38. дои : 10.1016/B978-0-12-374364-0.50008-4 . ISBN 978-0-12-374364-0 . Архивировано из оригинала 12 октября 2022 года . Проверено 11 октября 2022 г. {{cite book}}: |journal= игнорируется ( помогите )

[1]

[2]

[3]