Объект верификации (ОВ) часто называют DUT (Design Under Test).

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

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

• Функциональная верификация (Functional Verification) – проверка всех функциональных параметров и характеристик СБИС на логическом уровне. Если моделирование не дает корректных результатов, то этап логического проектирования (исправление ошибок проектирования) повторяется до достижения успеха. Функциональная верификация в объеме всех работ наиболее значительна и требует непосредственного участия человека.
• Формальная верификация (Formal Verification) - устанавливается эквивалентность представлений системы на разных стадиях маршрута проектирования или выполнение утверждений, помещенных в исходный код; инструменты формальной верификации часто тоже весьма самостоятельны, требует только внимательного анализа отчетов, которые они генерируют.
• Cтатический анализ кода (static code analysis) — проверка исходного кода по формальным критериям на соблюдения правил использования языка и его конструкций. Программы для такой проверки обычно обозначаются как lint или linter; требуют только первоначальной настройки инструментов, которая соответствует внутренним правилам проектирования, принятым в компании, дальше данный инструмент можно использовать без дополнительных трудозатрат.
• Прототипирование — использование FPGA для функциональной проверки.
• Физическая верификация — в основном подразумевается DRC, LVS, PERC и пр. проверки, физическое представление системы проверяется на соблюдение технологических норм и соответствия физического и логического представлений и т.д. Состав проверок сильно зависит от технологии. Обычно физическая верификация проводится инженером или командой топологического проектирования

Directed Tests Method (DTM)
Прямые, осмысленные тесты. План верификации составляется из тестов направленных на проверку поведения устройства в конкретных интересующих точках (состояниях). Проверить все возможные ситуации, особенно в сложных проектах, почти не возможно. При этом проблемы, которые могут возникнуть в ситуациях не покрытых тестами не обнаруживаются до того, как устройство начинают использовать в реальных условиях. Обычно в этих тестах используются метрики функционального покрытия.
Coverage-Driven Verification, Metric-Driven Verification (CDV, MDV)
Концепция создания тестов, направленная на достижение определенного «тестового покрытия» DUT. Опираются на метрики, чтобы понять какие тесты необходимо добавить в план верификации, чтобы достигнуть целевых показателей готовности проекта. Необходимо использовать инструменты анализа покрытия, чтобы посмотреть, что еще добавить в план верификации. По-сути, если начать корректировать план верификации в DTM, опираясь хотя бы на “покрытие кода”, то уже можно считать, что от DTM плавно перешли к CDV.
Constrained Random Verification (CRV)
Верификация подачей случайных воздействий. Это действительно автоматические тесты с генерацией случайных воздействий на DUT. Метод очень затратный вначале, т.к. требуется длительное время на подготовку инструментов. После того как начальный этап подготовки пройден, то тестирование может запускаться автоматически, многократно с разными исходными данными. При выявлении несоответствия проверок или утверждений (checkers or assertions), команда разработчиков и верификаторов приступает к анализу выявленной ошибки. Этим методом можно собрать покрытие кода и покрытие утверждений, а они могут ничего не говорить о правильности работы DUT, т.е. соответствии спецификации. Его необходимо дополнять функциональными тестами. Для реализации данной методологии требуется:

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

Assertion Based Verification (ABV)
Верификация с помощью утверждений. Наверное, это даже не самостоятельный метод, а некоторый компонент или базовая составляющая вышеупомянутых. Важным вопросом при ABV является как распределить assertions, какие из них лучше поместить в исходные код DUT, какие нужно иметь в тестовом окружении.

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

Типы метрик:

• функциональное покрытие. Показывает на сколько полно проверены функции устройства. Критерии данного покрытия могут определяться планом тестирования и внедрением специальных конструкций (covergroup) в тестовое окружение и/или в объект верификации, отслеживающих выполнялась или нет та или иная функция/действие, изменялись ли определенным образом данные и т.п. Информация от конструкций, внедренных в исходный код, может быть автоматически собрана средствами САПР.
• покрытие кода — изменение состояния конструкций исходного кода в ходе тестов. Собирается автоматически средствами САПР, не требует внесения каких-либо конструкций в исходный код. Например:
  • переключение регистров/сигналов (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 (FSM) Coverage).
• покрытие утверждений (assertions). Утверждения — это специальные языковые конструкции, которые отслеживают различные события и последовательности, и по заданным критериям определяют правомерность их возникновения.

В системе ModelSim при моделировании можно задать следующие опции покрытия кода.

• Enable Statement coverage – покрытие операторов.
• Enable Branch coverage – подсчитывается число выполнений условий типа «if/then/else» и «case».
• Enable Condition coverage – анализируется выборы, сделанные в условиях "if" и "case"; данная опция является расширением Branch coverage.
• Enable Expression coverage – покрытие выражений в правой части оператора назначения сигнала.
• Enable 0/1 Toggle coverage – покрытие переходов логического сигнала из одного состояния в другое; учитываются только переходы из 0 в 1 и обратно.
• Enable State Machine coverage – в VHDL-коде выделяется описание конечного автомата, подсчитываются покрытые переходы между внутренними состояниями, в которые попадает автомат.

Чтобы увидеть, какие строки кода конкретного модуля отмечены как покрытые (непокрытые), требуется открыть текст этого модуля.
Отчет о покрытии строки можно получить, выполнив View -->Coverage --> Details.
Результирующие отметки о покрытии кода

Рассмотрим покрытие выражений на примере оператора назначения сигнала

Y <= a and b and c;

при моделировании на наборе тестов {101, 011, 111}, сигналы a, b, c имеют тип std_logic и являются входными сигналами данного выражения. Первый набор 101 соответствует значениям a=1, b=0, c=1; для набора 011: a=0, b=1, c=1; для набора 111: a=1, b=0, c=1. Предполагается, что при моделировании установлен флаг (опция покрытия) Enable Expression coverage.
Полное покрытие выражения

a and b and c

означает, что в процессе моделирования каждый из сигналов a, b, c изменил свое значение из нуля в единицу и из единицы в нуль. Однако на рассматриваемом тесте сигнал c остается неизменным и равным 1. В отчете ниже (так называемой FEC-таблице, FEC – Focused Expression Coverage) выборочно для каждого входного сигнала выражения записываются входные наборы, обеспечивающие переключения данного сигнала в нуль либо в единицу:

# Input Term Covered Reason for no coverage Hint
# ----------- -------- ----------------------- -------
# a Y
# b Y
# c N '_0' not hit Hit '_0'
# Rows: Hits FEC Target Matching input patterns
# --------- --------- -------------------- -----------
# Row 1: 1 a_0 { 011 }
# Row 2: 1 a_1 { 111 }
# Row 3: 1 b_0 { 101 }
# Row 4: 1 b_1 { 111 }
# Row 5: ***0*** c_0 { 110 }
# Row 6: 1 c_1 { 111 }
#
# NOTE:
# * Order of matching input pattern values: {a,b,c}

указано, что для сигнала c нет установки в значение 0.

1. c N '_0' not hit Hit '_0'

Символ Y (Yes) свидетельствует о покрытии, символ N (No) - о том, что сигнал не покрыт. Символы '_0' сообщают в этой строке о том, что нет установки (hit) в значение 0. Заметим, что установка сигнала в единицу соответствует '_1'.
Далее в отчете строки

# Row 1: 1 a_0 { 011 }
# Row 2: 1 a_1 { 111 }

сообщают о том, что имеются тестовые векторы для установки сигнала a в нуль и единицу, соответственно. Далее две строки

# Row 3: 1 b_0 { 101 }
# Row 4: 1 b_1 { 111 }

указывают такие векторы 101, 111 имеются при моделировании для сигнала b. Следующая строка

# Row 5: ***0*** c_0 { 110 }

показывает, что тестовым вектором для установки сигнала с в нуль мог бы быть вектор 110. Однако такого вектора нет – моделирование осуществляется только для тестовых наборов из множества {101, 011, 111}. Строка

# Row 6: 1 c_1 { 111 }

показывает вектор 111, позволяющий установить сигнал c в единицу.
Покрытие выражения сводится к покрытию всех значений каждого сигнала по отдельности. Однако при таком покрытии не перебираются все восемь возможных комбинаций значений трех логических сигналов a, b, c.

Условные переходы в VHDL программах осуществляются с помощью операторов if, case. Рассмотрим покрытие ветвей на примерах различных вариантов записи оператора if. Так как оператор if может проверять много условий, то к организации тестирования таких операторов с целью покрытия всех ветвей следует относиться внимательно.

if C1 then Oper1;
elsif C2 then Oper2;
elsif C3 then Oper3;
elsif CN then Oper4;
else Oper5;
end if;

Приведем пример, показывающий различие покрытия ветвей для оператора if с частью else и частью elsif. Целью является демонстрация того факта, что оператор if с частью else обеспечивает полное покрытие ветвей (branch), а оператор if с частью elsif может не обеспечить полное покрытие ветвей при тех же тестирующих наборах.

После проведения моделирования VHDL-кода получаем следующий отчет

By file
File: B:/projects/VHDL/Cov_Ex/top.vhd
Line: 14
Branch Coverage for:
   if A
Active: 3, True Hits: 1, AllFalse: 0

из которого следует, что для строки 14 ни разу не была пройдена ветвь, когда A равно false. Однако сигналу A в тестирующей программе было присвоено это значение, но ветвь по такому значению сигнала ни разу не была пройдена. Всё потому, что во втором операторе if отсутствует фраза else. Нет фразы else - нет и ветви для альтернативного значения условия (А=false). Этот пример иллюстрирует факт того, что при записи операторов if без частей else нельзя добиться покрытия всех ветвей.