Верификация цифровых схем. Обзор

Моя цель - предложение широкого ассортимента товаров и услуг на постоянно высоком качестве обслуживания по самым выгодным ценам.

image


Я постараюсь в общем рассказать о верификации цифровых схем.


Верификация в данной области — это важный процесс, требующий привлечения опытных инженеров. Например, специалист по верификации, работающий над системами с ЦПУ, как правило должен владеть скриптовыми языками и языками командных оболочек (Tcl, bash, Makefile и т.п.), языками программирования (С, С++, ассемблер), HDL/HDVL (SystemVerilog [10, Appendix C — история языка][11], Verilog, VHDL), современными методологиями и framework’ами (UVM).


Доля времени, затраченного на верификацию, доходит до 70-80% от всего времени проекта. Одна из основных причин такого внимания в том, что к микросхеме нельзя выпустить “патч” после того, как ее отдали в производство, можно только выпустить “silicon errata” (это не касается проектов ПЛИС/FPGA).


Под цифровыми схемами я подразумеваю:


  • сложно-функциональные блоки/intellectual properties (СФБ/IP);
  • специализированные заказные микросхемы/application-specific integrated circuit — (ASIC);
  • проекты программируемых логических интегральных схем/field-programmable gate — array (ПЛИС/FPGA);
  • системы на кристалле/system-on-crystal (СнК/SoC);
  • и т.п.

Актуальные проблемы верификации


О текущем состояние и тенденциях в сфере верификации можно судить по следующим вызовам и проблемам, с которыми она сталкивается [6]:


  • размер объекта верификации (ОВ) постоянно растет. Даже небольшая ИМС типа “микроконтроллер” — это набор из десятков подмодулей, очень часто со сложным функционалом. Большие ИМС — это комплексы, в которых может насчитываться до десятков миллиардов транзисторов, и одна только схема управления электропитанием по сложности может превосходить некоторые процессоры [8];
  • невозможно составить спецификацию на ИМС в начале проекта и в дальнейшем только следовать ей, она постоянно изменяется на протяжении всего процесса разработки (заказчик изменяет требования, технические проблемы или обнаружение более оптимальных решений вынуждают пересматривать подходы и т.д.). Исходя из этого, все процессы должны в динамике воспринимать изменения спецификации и модифицироваться в соответствии с требованиями;
  • часто над верификацией проекта работает несколько удаленных друг от друга команд численность которых может достигать десятков человек;
  • количества отдельных тестов и их типов достигает огромного числа, результаты их надо собирать и анализировать;
  • моделирование даже цифровых систем требует массу машинного времени;
  • полнота установленных для проекта целевых показатели готовности во многом зависит от компетентности и интуиции специалистов по верификации;
  • несмотря на существование показателей охвата проекта тестами (метрик), единственный способ закончить верификацию — это принять решение о ее приостановке, основываясь в основном на следующих заключениях: деньги или время на этап проекта потрачены, необходимо запускать в производство, вроде как достигли покрытия кода в 100%, тестируем уже неделю и ошибок не обнаружили и т.п.

Типы верификации


Верификацию цифровых схем можно разделить на следующие основные типы:


  1. функциональная (functional verification) — название говорит само за себя, вы проверяете правильно ли выполняет свои функции ваша система;
  2. формальная (formal verification) — при такой верификации устанавливается эквивалентность представлений вашей системы на разных стадиях маршрута проектирования или выполнение утверждений, помещенных в исходный код:
    • Equivalence Checking (например, RTL-to-RTL, RTL-to-Gate, Gate-to-Gate);
    • Property Checking (Model Checking) (проверяет свойства(assertions), заданные в коде средствами SVA (например)).
  3. статический анализ кода (static code analysis) — проверка исходного кода по формальным критериям на соблюдения правил использования языка и его конструкций. Очень часто в настроенных правилах проверки идет отсылка на RMM [4]. Программы для такой проверки обычно обозначаются как lint или linter;
  4. физическая верификация — в основном подразумевается DRC, LVS, PERC и пр. проверки, физическое представление системы проверяется на соблюдение технологических норм и соответствия физического и логического представлений и т.д. Состав проверок сильно зависит от технологии. Обычно физическая верификация проводится инженером или командой топологического проектирования.
  5. прототипирование — использование FPGA для функциональной проверки [18].

Функциональная верификация в объеме всех работ наиболее значительна и требует непосредственного участия человека.


Статический анализ кода требуют только первоначальной настройки инструментов, которая соответствует внутренним правилам проектирования, принятым в компании, дальше инструмент занимается тем, что выдает “ценные указания” разработчикам и постоянного присмотра не требует.


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


Примеры инструментов верификации


Примеры инструментов верификации цифровых схем (маршрут digital-on-top):


  • инструменты управления верификацией
    • Mentor Graphics — Questa Verification Management
    • Cadence — vManager
    • Synopsys — Verdi, VC Execution Manager (“ExecMan”)
  • функциональная — как правило это симуляторы
    • Mentor Graphics — ModelSim, QuestaSim
    • Cadence — Incisive, Xcelium
    • Synopsys — VCS
    • свободное ПО независимых разработчиков — симуляторы Verilator, Icarus [5]
  • формальная
    • Mentor Graphics — Formal Pro, Questa Formal Verification
    • Cadence — JasperGold, Conformal LEC, Incisive Formal Verification Platform
    • Synopsys — Formality, VC Formal
  • статический анализ кода
    • Mentor Graphics — Questa AutoCheck
    • Cadence — HAL, JasperGold
    • Synopsys — SpyGlass Lint
  • физическая верификация
    • Mentor Graphics — Calibre
    • Cadence — Pegasus, Physical Verification System,
    • Synopsys — Hercules, IC Validator

Методы функциональной верификации


Функциональная верификация — представляет собой набор тестов, условно позволю себе разбить на три группы (это не догма, это из личного опыта):


  1. Положительные ветки — проверка поведения в штатных ситуациях, регламентируемых спецификацией на устройство или стандартом и т.п. Т.е. проверяем ситуации, когда все идет хорошо.
  2. Отрицательные ветки — проверка отклонений от штатных ситуаций, но в рамках спецификации или стандарта, например — несовпадение контрольной суммы, кол-ва принимаемых данных и т.п. Т.е. когда что-то идет не так, но мы знали, что такое может быть и знаем как в этой ситуации работать.
  3. Нестандартные ситуации — любые случайные ситуации от нарушений протоколов обмена, порядка следования данных, до физических коллизий в интерфейсах, случайных изменений состояний логических элементов и т.п. Т.е. это когда может произойти все, что угодно и надо убедиться, что ОВ выйдет после этого в рабочее состояние.

Первые две стадии поддаются автоматизации с помощью UVC/VIP(Universal Verification Component/Verification IP) и достаточно быстро там можно нарастить объем различных тестов, в том числе — генерируемых автоматически. Третья стадия — это «masterpiece» в верификации, эта стадия требует неординарного подхода и опыта, очень сложно автоматизируется, т.к. большинство ситуаций — это отдельный алгоритм, возможно скрипт для САПР или инструкции для «ручных» проверок.


Типы метрик функциональной верификации


Метрики — это показатели охвата проекта тестами. Они нужны для того, чтобы понять какие еще тесты необходимо разработать для проверки возможных ситуаций и сколько предположительно времени может занять верификация [16].


К сожалению, только один тип метрик оценивается на основании исходного кода проекта, определение критериев для остальных типов — это результат интеллектуального труда.


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


Типы метрик [3]:


  • функциональное покрытие. Показывает на сколько полно проверены функции ОВ. Критерии данного покрытия могут определяться планом тестирования и внедрением специальных конструкций (covergroup [1]) в тестовое окружение и/или ОВ, отслеживающих выполнялась или нет та или иная функция/действие, изменялись ли определенным образом данные и т.п. Информация от конструкций, внедренных в исходный код, может быть автоматически собрана средствами САПР.
  • покрытие кода — изменение состояния конструкций исходного кода в ходе тестов. Собирается автоматически средствами САПР, не требует внесения каких-либо конструкций в исходный код. Например:
    • переключение регистров (Toggle Coverage);
    • активность каждой строки кода (Line Coverage);
    • активность выражений (Statement Coverage), по сути — это Line Coverage, но может отслеживать выражения которые больше, чем одна строка в редакторе;
    • активность участка кода внутри условного оператора или процедуры (Block Coverage), разновидность Statement Coverage;
    • активность всех веток условных операторов таких как if, case, while, repeat, forever, for, loop (Branch Coverage);
    • изменение всех состояний(true, false) составляющих логических выражений (Expression Coverage);
    • состояния конечного автомата (Finite-State Machine Coverage).
  • покрытие утверждений. Утверждения — это специальные языковые конструкции, которые отслеживают различные события и последовательность, и по заданным критериям определяют правомерность их возникновения.

Методы функциональной верификации


Directed Tests Method (DTM)


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


Coverage-Driven Verification, Metric-Driven Verification (CDV, MDV) [17]


Концепция создания тестов, направленная на достижение определенного «тестового покрытия» ОВ. Опираются на метрики, чтобы понять какие тесты необходимо добавить в план верификации, чтобы достигнуть целевых показателей готовности проекта.
Необходимо использовать инструменты анализа покрытия, чтобы посмотреть, что еще добавить в план верификации. По-сути, если начать корректировать план верификации в DTM, опираясь хотя бы на “покрытие кода”, то уже можно считать, что от DTM плавно перешли к CDV.


Constrained Random Verification (CRV)


Верификация подачей случайных воздействий. Это действительно автоматические тесты с генерацией случайных воздействий на ОВ, только их трудно представить без симбиоза с ABV.
Метод очень затратный вначале, т.к. требуется длительное время на подготовку инструментов. После того как начальный этап подготовки пройден, то тестирование может запускаться автоматически, многократно с разными исходными данными. При выявлении несоответствия assertion, команда разработчиков и верификаторов приступает к анализу выявленной ошибки.
В реальном проекте нельзя ограничится только этим методом, т.к. этим методом можно собрать покрытие кода и покрытие утверждений, а они могут ничего не говорить о правильности работы ОВ, т.е. соответствии спецификации. Его необходимо дополнять функциональными тестами.
Для реализации данной методологии требуется:


  1. внедрить “утверждения”(assertion) во всех важных точках исходного кода ОВ и тестового окружения;
  2. разработать генераторы случайных воздействий и сценарии их работы, т.е. воздействия случайны, но имеют ограничения диапазона (все перебрать не успеем), порядок подачи и т.п..

Assertion Based Verification[9] (ABV)


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


Важным вопросом при ABV является как распределить assertions, какие из них лучше поместить в исходные код ОВ, какие нужно иметь в тестовое окружение.


Сразу стоит отметить, что язык Verilog не имеет assertions в своем стандарте (их можно создать с использованием основных конструкций языка, но необходимы директивы для синтезатора, чтобы он не занимался их преобразованием). Аssertions появляются только в стандарте SystemVerilog, а так же они изначально были в стандарте языка VHDL и e.


Предлагаю ознакомиться с рекомендациями специалистов, в том числе Clifford’а Cummings’а [12, статьи про SVA] о распределении работ по их написанию, а также с материалами по ABV на сайте Verification Academy [13].


Список литературы


  1. IEEE Std 1800TM-2012. IEEE Standard for SystemVerilog — Unified Hardware Design, Specification, and Verification Language
  2. Клайв Максфилд. Проектирование на ПЛИС. Архитектура, средства и методы. Курс молодого бойца. ISBN 978-5-94120-147-1 (RUS), ISBN 0-7506-7604-3 (ENG)
  3. Verification Academy. Coverage Cookbook. Про тестовое покрытие
  4. Michael Keating, Pierre Bricaud. Reuse methodology manual for system-on-a-chip designs. Print ISBN 1-4020-7141-8, eBook ISBN 0-306-47640-1
  5. Список лицензируемых и свободно распространяемых САПР
  6. Mentor Graphics. Пример статистики по современному состоянию и сферы верификации
  7. WikiChip. "Википедия" по микросхемам
  8. Wikipedia. Обобщенные данные по количеству транзисторов в ИМС
  9. Harry Foster, Adam Krolnik, David Lacey. Assertion-based design.Print ISBN 1-4020-8027-1, eBook ISBN 1-4020-8028-X
  10. Stuart Sutherland, Simon Davidmann, Peter Flake. SystemVerilog for Design. Print ISBN-10: 0-387-33399-1, eBook ISBN-10: 0-387-36495-1
  11. Chris Spear, Greg Tumbush. SystemVerilog for Verification. Print ISBN: 978-1-4614-0714-0, eBook ISBN: 978-1-4614-0715-7
  12. Sunburst Design. Papers
  13. Verification Academy. ABV course
  14. Doulos. Полезные материалы on-line и справочники
  15. Prakash Rashinkar, Peter Paterson, Leena Singh. System-on-a chip verification. methodology and techniques. Print ISBN: 0-792-37279-4, eBook ISBN: 0-306-46995-2
  16. Verification Academy. Metrics in SoC Verification
  17. Doulos. Coverage-Driven Verification Methodology
  18. Doug Amos, Austin Lesea, Rene Richter. FPGA-Based Prototyping Methodology Manual: Best practices in Design-for-Prototyping (FPMM). Print ISBN: 978-1617300042. Скачать бесплатно с сайта Synopsys
Источник: https://habr.com/ru/post/481542/


Интересные статьи

Интересные статьи

Доброго времени суток, дорогие читатели! В нашем очередном обзоре мы рассмотрим DECT-систему чуть менее масштабную чем предыдущая, но безусловно заслуживающую вашего внимания. Тогда как ...
Недавно в очередном посте о том «как корпоративные редакторы захватили Хабр и совсем не дают вздохнуть свободным авторам», нам поставили в минус, что в нашем блоге слишком много мат...
Качество современных источников света постепенно улучшается и уже стало сравнимо с обычным солнечным светом. Такой источник появился благодаря корейским светодиодам Sunlike, имеющих спектр ка...
Получить трафик для интернет-магазина сегодня не проблема. Есть много каналов его привлечения: органическая выдача, контекстная реклама, контент-маркетинг, RTB-сети и т. д. Вопрос в том, как вы распор...
Эта публикация написана после неоднократных обращений как клиентов, так и (к горести моей) партнеров. Темы обращений были разные, но причиной в итоге оказывался один и тот же сценарий, реализу...