Верификация цифровых схем. Обзор | | ДОСТУПНЫЙ ОТДЫХ
Интересное

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

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

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

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

    Читать  Нидерландский фотограф с помощью нейросетей воссоздал внешность исторических личностей и не только (13 фото)

  • внедрить “утверждения”(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
  • Источник

    I heart FeedBurner