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

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

Верификация в данной области — это важный процесс, требующий привлечения опытных инженеров. Например, специалист по верификации, работающий над системами с ЦПУ, как правило должен владеть скриптовыми языками и языками командных оболочек (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