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

Сегодня, в субботу 26 февраля, на Сколковской Школе Синтеза Цифровых Схем Михаил Коробков проводит занятие по технологиям функциональной верификации: constrain solvers, cover bins и concurrent assertions. Примеры, которые мы подготовили для школы, вращаются вокруг протокола AXI для систем на кристалле, вопросы про который спрашивают например на интервью в хардверное отделение компании Meta и другие.

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

Суть деятельности Verification Engineer заключается в создание фреймворков, которые тестируют хардверные дизайны на прочность, посылая к ним псевдослучайные транзакции и учитывая покрытие интересных сценариев (functional coverage). Базовые элементы этих технологий должен знать и хороший RTL Design Engineer.

Приглашаем присоединяться к трансляции занятия на канале школы в YouTube, в субботу 26 февраля с 12.00 до 15.00:

Как выглядит процесс верификации блока микросхемы, описанного на уровне регистровых передач (Register Transfer Level - RTL):

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

Одна голова - хорошо, а три головы - лучше. Так как корень самых больших ошибок - это неоднозначность в интерпретации функциональной спецификации (fSpec), в промышленности применяется концепция повторной сходимости, reconvergence. Она проверяет интерпретацию спецификации RTL инженера интерпретациями двух других людей - инженера по моделированию и инженера по верификации:

1. Для каждого значительного RTL блока пишется поведенческая или функциональная модель - просто программа, которая на основе вводов и внутреннего состояния, без попыток делать что-либо эффективно, реализует поведение блока по спецификации. Эту программу пишет инженер по моделированию, на основе своего видения fSpec. Программа может быть на SystemVerilog, Си и даже на Питоне, если скорость работы модели на компьютере некритична.

2. Инженер-верификатор, под контролем менеджера-верификатора, составляет план тестирования, на основе своего восприятия fSpec. В плане описываются сценарии работы блока, причем для каждого случая указывается, как его автоматически проверить, сравнивая поведение RTL блока и модели, а также как проверить (тоже автоматически) то, что этот сценарий произошел во время тестирования. Последнее называется "проверка функционального покрытия" (functional coverage).

3. План тестирования проходит ревью, после чего на его основе на языке SystemVerilog пишется тестовое окружение, тесты и специальные конструкции под названием "группы покрытия" (covergroups). Последнее нужно для контроля, что все тесты, обещанные в плане тестирования, были действительно написаны.

4. Многие тесты делаются с ограниченно-случайными данными и ограниченно-случайными последовательностями событий по времени. Для этого в языке SystemVerilog есть встроенный генератор случайных данных на основе правил зависимостей (constraint solver). В комбинации с проверкой функционального покрытия такие тесты дают возможность сгенерировать сценарии, о которых не думал инженер, пишущий тесты. Например у NPU может возникать ситуация, когда транзакции через две независимые AXI шины к многобанковой памяти, в которой лежат веса и поток команд, начинают конфликтовать и вызывать ошибки при дистанции между ними ровно 3 такта, а не 0, не 1 и не 10.

5. Может случиться так, что функциональная спецификация описывает не все аспекты блока, и что RTL инженер дополнил блок на основе устной договоренности с архитектором. Инженер-верификатор может не знать об этой договоренности и не реализовать дополнительные тесты. После этого прогон тестов может выдать в лог "покрыто 100%", хотя это не будет соответствовать действительности (часть реализованной функциональности не будет покрыто тестами). На этот случай в методологии используется страховка в виде автоматической проверки покрытия кода (code coverage) во время симуляции - она выявит RTL код, который не был задействован в процессе тестирования.

Больше деталей и конкретных примеров с кодом - на семинаре.

Картинка отсюда.