Я постараюсь в общем рассказать о верификации цифровых схем.
Верификация в данной области — это важный процесс, требующий привлечения опытных инженеров. Например, специалист по верификации, работающий над системами с ЦПУ, как правило должен владеть скриптовыми языками и языками командных оболочек (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%, тестируем уже неделю и ошибок не обнаружили и т.п.
Типы верификации
Верификацию цифровых схем можно разделить на следующие основные типы:
- функциональная (functional verification) — название говорит само за себя, вы проверяете правильно ли выполняет свои функции ваша система;
- формальная (formal verification) — при такой верификации устанавливается эквивалентность представлений вашей системы на разных стадиях маршрута проектирования или выполнение утверждений, помещенных в исходный код:
- Equivalence Checking (например, RTL-to-RTL, RTL-to-Gate, Gate-to-Gate);
- Property Checking (Model Checking) (проверяет свойства(assertions), заданные в коде средствами SVA (например)).
- статический анализ кода (static code analysis) — проверка исходного кода по формальным критериям на соблюдения правил использования языка и его конструкций. Очень часто в настроенных правилах проверки идет отсылка на RMM [4]. Программы для такой проверки обычно обозначаются как lint или linter;
- физическая верификация — в основном подразумевается DRC, LVS, PERC и пр. проверки, физическое представление системы проверяется на соблюдение технологических норм и соответствия физического и логического представлений и т.д. Состав проверок сильно зависит от технологии. Обычно физическая верификация проводится инженером или командой топологического проектирования.
- прототипирование — использование 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
Методы функциональной верификации
Функциональная верификация — представляет собой набор тестов, условно позволю себе разбить на три группы (это не догма, это из личного опыта):
- Положительные ветки — проверка поведения в штатных ситуациях, регламентируемых спецификацией на устройство или стандартом и т.п. Т.е. проверяем ситуации, когда все идет хорошо.
- Отрицательные ветки — проверка отклонений от штатных ситуаций, но в рамках спецификации или стандарта, например — несовпадение контрольной суммы, кол-ва принимаемых данных и т.п. Т.е. когда что-то идет не так, но мы знали, что такое может быть и знаем как в этой ситуации работать.
- Нестандартные ситуации — любые случайные ситуации от нарушений протоколов обмена, порядка следования данных, до физических коллизий в интерфейсах, случайных изменений состояний логических элементов и т.п. Т.е. это когда может произойти все, что угодно и надо убедиться, что ОВ выйдет после этого в рабочее состояние.
Первые две стадии поддаются автоматизации с помощью 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, команда разработчиков и верификаторов приступает к анализу выявленной ошибки.
В реальном проекте нельзя ограничится только этим методом, т.к. этим методом можно собрать покрытие кода и покрытие утверждений, а они могут ничего не говорить о правильности работы ОВ, т.е. соответствии спецификации. Его необходимо дополнять функциональными тестами.
Для реализации данной методологии требуется:
- внедрить “утверждения”(assertion) во всех важных точках исходного кода ОВ и тестового окружения;
- разработать генераторы случайных воздействий и сценарии их работы, т.е. воздействия случайны, но имеют ограничения диапазона (все перебрать не успеем), порядок подачи и т.п..
Assertion Based Verification[9] (ABV)
Верификация с помощью утверждений. Наверное, это даже не самостоятельный метод, а некоторый компонент или базовая составляющая вышеупомянутых.
Важным вопросом при ABV является как распределить assertions, какие из них лучше поместить в исходные код ОВ, какие нужно иметь в тестовое окружение.
Сразу стоит отметить, что язык Verilog не имеет assertions в своем стандарте (их можно создать с использованием основных конструкций языка, но необходимы директивы для синтезатора, чтобы он не занимался их преобразованием). Аssertions появляются только в стандарте SystemVerilog, а так же они изначально были в стандарте языка VHDL и e.
Предлагаю ознакомиться с рекомендациями специалистов, в том числе Clifford’а Cummings’а [12, статьи про SVA] о распределении работ по их написанию, а также с материалами по ABV на сайте Verification Academy [13].
Список литературы
- IEEE Std 1800TM-2012. IEEE Standard for SystemVerilog — Unified Hardware Design, Specification, and Verification Language
- Клайв Максфилд. Проектирование на ПЛИС. Архитектура, средства и методы. Курс молодого бойца. ISBN 978-5-94120-147-1 (RUS), ISBN 0-7506-7604-3 (ENG)
- Verification Academy. Coverage Cookbook. Про тестовое покрытие
- 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
- Список лицензируемых и свободно распространяемых САПР
- Mentor Graphics. Пример статистики по современному состоянию и сферы верификации
- WikiChip. "Википедия" по микросхемам
- Wikipedia. Обобщенные данные по количеству транзисторов в ИМС
- Harry Foster, Adam Krolnik, David Lacey. Assertion-based design.Print ISBN 1-4020-8027-1, eBook ISBN 1-4020-8028-X
- Stuart Sutherland, Simon Davidmann, Peter Flake. SystemVerilog for Design. Print ISBN-10: 0-387-33399-1, eBook ISBN-10: 0-387-36495-1
- Chris Spear, Greg Tumbush. SystemVerilog for Verification. Print ISBN: 978-1-4614-0714-0, eBook ISBN: 978-1-4614-0715-7
- Sunburst Design. Papers
- Verification Academy. ABV course
- Doulos. Полезные материалы on-line и справочники
- 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
- Verification Academy. Metrics in SoC Verification
- Doulos. Coverage-Driven Verification Methodology
- Doug Amos, Austin Lesea, Rene Richter. FPGA-Based Prototyping Methodology Manual: Best practices in Design-for-Prototyping (FPMM). Print ISBN: 978-1617300042. Скачать бесплатно с сайта Synopsys
Автор: Dmitriy
