Снятся ли венд-машинам электрожуки?

Некоторое время назад  в МИЭТ прошёл инженерный хакатон YADRO SoC Design Challenge. Данная статья посвящена треку функциональной верификации, для которого я делал задание. Пройдёмся по тому, что такое верификация и как провести хакатон по этому направлению среди тех, кто никогда с ней не сталкивался. Немного скажу и про сложности, с которыми мы столкнулись и результаты проведения хакатона.

---

Что такое верификация цифровых устройств

В новостях про микроэлектронику мы часто слышим: «разработано устройство X», «выпущено устройство Y». Человек, читающий новости, но не знакомый с устройством микроэлектронной кухни может решить, что тут все только и занимаются тем, что разрабатывают какие-то устройства, ну или готовят их к производству. Ещё часто мы слышим о разного рода экспертах, фондах, связанных с микроэлектроникой, но уж точно не о верификаторах. Где-то на задворках сознания мы понимаем, что устройство мало разработать, надо, наверное, ещё его проверить, но не придаём этому большого значения. А зря. Приведу пару примеров того, почему проверка устройства важна.



А какие примеры известных и интересных ошибок знаете вы? Буду рад, если поделитесь в комментариях.

Теперь давайте пройдёмся по самому термину «верификация». В случае цифрового устройства, верификация — это подтверждение того, что устройство соответствует спецификации и делает то, что должно делать, в то же время не делая того, чего не должно.

Стоит отметить, что верификация не является синонимом проверки и вот почему. Вы можете «проверить», что холодильник работает, открыв дверь, увидев, что лампочка загорелась, а внутри холодно. Если вы захотите верифицировать холодильник, то вам придётся ознакомиться с условиями эксплуатации и характеристиками холодильника, провести ряд тестов на то, поддерживает ли холодильник нужную температуру, и что та отклоняется только в допустимых пределах. Что в случае отключения света, холодильник держит температуру на протяжении указанного времени. Что если оставить дверцу холодильника открытой, тот автоматически отключится через какое-то время во избежание поломки. Вам потребуется проверить такие функции, как защиту от обледенения задней стенки (если таковая функция имеется) и т.п. Верификация — это всестороннее исследование объекта верификации на соответствие заявленным характеристикам.

Для проведения верификации инженеру необходимо составить план — документ, описывающий весь объём работ начиная с описания объекта, стратегии, расписания, критериев начала и окончания верификации, и заканчивая необходимым в процессе работы оборудованием, специальными знаниями, а также оценками рисков с вариантами их разрешения.[8]

После составления плана необходимо написать верификационное окружение — несинтезируемый код, который будет формировать и устанавливать тестовые входные воздействия на объект верификации, собирать выходные реакции объекта, сверять результаты с моделью объекта, и собирать данные о набранном тестовом покрытии.

Верификационное окружение часто пишут таким образом, чтобы отдельные его части было возможно использовать повторно в других проектах. Это достигается за счёт применения ООП-подхода при проектировании. Верифицируя разрабатываемые устройства с помощью языка SystemVerilog (надмножеством языка описания аппаратуры Verilog), для ускорения разработки окружения используют универсальную методологию верификации (Universal Verification Methodology, UVM), предоставляющую библиотеку базовых классов для верификационного окружения.

В среднем, на верификацию уходит половина от всего времени, затраченного на весь путь разработки устройства (иногда переваливая и за 80% времени разработки).[9] Чуть подробней о верификации вы можете прочесть здесь.

Для достижения баланса между временем до выхода на рынок, затратами и полнотой проверки устройства, на одного разработчика микросхемы требуется два верификатора. Однако в реальности компании часто стараются выйти хотя бы к отношению 1:1. Связано это с тем, что фактически на эту специальность не учат в вузах, а знания о верификации инженеры пока что получают прямо на производстве. Это означает, что верификаторов не хватает, и если вы ещё не определились со специальностью и читаете эту статью — советую рассмотреть этот вариант. Для создания новых точек входа в данную специальность и был проведён наш хакатон.

Как провести хакатон по верификации среди тех, кто с ней не сталкивался?

Хакатон рассчитан на два дня, которых едва хватит только на то, чтобы обзорно ознакомиться с самой методологией верификации, не то что уж разбираться с библиотекой uvm или написать какое-либо окружение. А ведь нужно ещё адаптироваться к новой обстановке (к нам приезжали студенты и школьники не из МИЭТа), разобраться с самим заданием и не забыть о том, что результаты необходимо ещё и презентовать.

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

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

В качестве проверяемого устройства было решено написать торговый автомат. Подобное устройство часто применяют в качестве примера по разработке конечного автомата. Причём подобное устройство знакомо нам с детства, что позволяет быстро понять описание его работы. Поскольку устройство вполне понятное, было решено написать довольно сложный автомат, в который могли бы закрасться ошибки. В качестве усложнения автомат был максимально приближен к реальному: в нём реализованы опции выдачи сдачи, возврата монет, отслеживания количества товара, проверка условий продажи, а также возврат монет в случае асинхронного сброса во время взаимодействия с автоматом.

Было решено предложить участникам выполнить проверку устройства, написав конструкции SystemVerilog Assertions (SVA).

О SystemVerilog Assertions

Прежде чем говорить об SVA, надо понять, что такое assertion. Переводчик скажет, что assertion — это утверждение. Но для слова «утверждение» можно использовать и argument, point и много других слов, почему именно assertion? Assertion — это утверждение о некотором факте, подразумевающее, что то, о чём вы заявляете, является истиной.

В SVA, когда вы проверяете устройство, то знаете некоторые правила, которые должны выполняться вне зависимости от всего остального. Эти правила являются неотъемлемыми особенностями (свойствами — properties) вашего устройства. Например, вы используете фифо, и дизайн разработан таким образом, что фифо никогда не должно переполниться. В этом случае можно сделать утверждение, что на каждом такте сигнал fifo_is_full не будет равен единице:

fifo_will_never_goes_full: assert property(  
 @(posedge clk) !fifo_is_full  
); 

Ваши правила-свойства могут быть гораздо сложнее, чем описанное выше и действовать на протяжении нескольких тактов. Например, есть память, в которую вы пишите данные data по адресу addr в случае, если по тактовому сигналу clk обнаружен сигнал en (и если не происходит сброс rst). Это значит, что если по тактовому сигналу clk, сигнал en равен 1, то на следующий такт в памяти по адресу addr вы должны обнаружить data:

memory_write: assert property(  
 @(posedge clk) disable iff(reset) 
 en |=> mem[$past(addr)] == $past(data)  
); 

Подробнее про SVA можно прочесть здесь.

Используя конструкции SVA, можно описать некое правило, которое будет проверяться на каждом тактовом синхроимпульсе. Это значит, участникам можно предоставить спецификацию, описание конструкций, операторов и системных функций SVA, и предложить реализовать спецификацию в виде отдельных конструкций. В случае несоответствия устройства той части спецификации, которая была описана, произойдёт срабатывание assertion, о чём узнаёт участник.

Но конструкции SVA будут проверять, только когда с проверяемым устройством что-то начнёт происходить. При этом с самим устройством ничего не начнёт происходить, пока на него не подадут входные воздействия. Поэтому для хакатона был написан тестбенч, формирующий направленные тесты, проверяющий значительную часть возможных воздействий на устройство.

Таким образом, участникам будут даны модули, которые необходимо проверить, и тестбенч, который будет формировать входные воздействия на эти модули, но не будет выполнять никаких проверок выходных сигналов. А участники, написав конструкции SVA, смогут после запуска тестбенча увидеть в логе: были ли найдены какие-либо ошибки или нет.

Обеспечение непрозрачности модулей с ошибками

Итак, участникам необходимо найти модули с ошибками. Такая постановка задачи порождает несколько проблем.

Проблема единственного референсного дизайна

Если у вас одно проверенное устройство, а все остальные устройства с ошибками, то постановка задачи по поиску модулей с ошибками стоит неверно: с высокой вероятностью вы найдёте такой модуль, просто ткнув пальцем в небо. Искать в таком случае надо модуль без ошибок. Но эта задача на порядок сложнее, это значит, что участник должен убедиться в том, что ошибки есть во всех остальных устройствах. В конце концов, исходов у этой задачи два: вы либо нашли правильный модуль, либо не нашли. В задаче поиска ошибочных модулей вы можете найти от одного до n ошибочных модулей, значит, у участников будет больший диапазон результатов, а значит, будет и проще определить победителя хакатона.

Чтобы задача превратилась всё-таки в поиск ошибочных модулей, а не в ловлю шариков голодными бегемотиками, необходимо чтобы модули с ошибками были иголками, а не стогом сена. Для этого их надо спрятать среди множества дизайнов без ошибок. Но написание даже одного модуля, который вы более-менее проверили и уверены в нём, требует значительных усилий. Написать ещё столько, чтобы среди них можно было потерять остальные — неоправданно сложная задача. Значит, необходимо сменить подход. Можно скопировать один модуль несколько десятков раз. В этом случае участнику будет достаточно заметить, что большинство модулей идентично, сложить два и два, и методом исключения найти все модули с ошибками. Для решения этой проблемы можно пытаться обфусцировать модули с разными параметрами, но в связи с другими проблемами, которые опишу ниже, этот подход тоже не был применён. Пока «повесим» проблему в воздухе, и посмотрим, какие сложности есть ещё.

Проблема многократного запуска моделирования

Допустим, у нас есть 50 модулей: часть из них содержат ошибки, часть нет. В процессе проверки ваших assertions от вас потребуется многократно повторять запуск 50 моделирований для этих модулей. Кроме того, в случае такого количества ручных запусков моделирования, высока вероятность каких-либо ошибок, влияющих на дальнейший результат. Очевидно, необходимо озаботиться автоматизацией запуска тестов для участников.

Проблема схожести временных диаграмм

Даже если у вас есть 50 различных по коду модулей, 40 из которых обладают логической эквивалентностью, вы сможете определить их, увидев сходство во временных диаграммах.


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

Принятое решение

Первая и последняя проблемы (проблема исследования исходного кода модулей, а также проблема контроля над ходом запуска моделирования) говорят о том, что у участников хакатона вообще не должно быть доступа к этим сущностям. Моделирование может запускаться на отдельном закрытом от участников сервере. В этом случае нет нужды создавать много новых устройств без ошибок: достаточно запустить несколько тестов с разными сидами над одним и тем же устройством. При этом участникам необходимо предоставить результаты тестов и временные диаграммы, а также организовать приём от участников написанных конструкций SVA. Эти задачи прекрасно решаются инструментами непрерывной интеграции (CI).

Как встроить в проверяемые модули конструкции SVA, если у участника нет доступа к файлам этих модулей?

В SystemVerilog есть конструкция bind, которая позволяет инстанциировать один модуль внутрь другого без какого-либо изменения кода в оригинальном модуле. Например, у вас есть эталонная модель, в которую по вашим бизнес-правилам запрещено вносить какие-либо изменения, но в то же время было бы полезно добавить в неё SVA. Конструкция bind выполнит ровно это. Есть два способа вставки одного модуля внутрь другого с помощью bind:

bind binding_module_name: binding_instance_name bound_module_name 
bound_instance_name(portlist);

Такая конструкция вставит сущность с именем bound_instance_name модуля bound_module_name внутрь сущности binding_instance_name модуля binding_module_name. В случае если порты обоих модулей имеют одинаковые имена, вместо portlist можно указать .*. Подобная запись избыточна. Если вы хотите инстинациировать ваш модуль только в один конкретный экземпляр другого модуля, то можно опустить binding_module_name:. Кроме того, если вы хотите инстанциировать ваш модуль внутрь всех экземпляров другого модуля, вы можете опустить binding_instance_name.[13]

Таким образом, участникам необходимо описать их утверждения в отдельном модуле, который затем будет инстанциироваться в проверяемые модули тестбенчем посредством конструкции bind.

Наше использование CI

Поскольку у нас уже был опыт взаимодействия с работами студентов через github actions с self-hosted сервером, использовали именно этот инструмент.

Была создана организация на github, в которой разместили репозиторий-шаблон. Для каждой команды участников на основе этого шаблона был создан приватный репозиторий (чтобы участники не могли видеть работы других участников). В этом репозитории находились:

1. Референсный дизайн.
2. Модуль-заготовка, в котором необходимо прописать конструкции SVA. 
3. Тестбенч. 
4. Readme-файл с руководством по использованию репозитория и инструментов, спецификация и задание.

Участникам предоставлен модуль-заготовка, в котором необходимо прописать конструкции SVA. Входные и выходные сигналы этого модуля — это входные, выходные сигналы проверяемого модуля, а также его архитектурные регистры, описанные в спецификации на устройство. По этим сигналам необходимо написать утверждения, проверить их работоспособность на референсном модуле, после чего закоммитить в свой репозиторий и получить результат автоматизированного запуска тестов — в случае обнаружения ошибок проверить временную диаграмму и, если это не ложноположительное срабатывание зафиксировать обнаружение ошибочного дизайна.

Взаимодействие с репозиторием со стороны участников

На этой странице находился детальный лог по каждому из тестов, в который входят и сообщения о сработавших assertions (в настройках симуляции стоит опция assertion fail -r / -limit 5 отключающая вывод утверждения, сработавшего более пяти раз, чтобы не загромождать лог).

Результаты

По итогам хакатона каждая из команд нашла хотя бы одну ошибку. К сожалению (или счастью), ошибок в референсном дизайне не было обнаружено. Всего участвовало четыре команды — следствие того, что студенты не знают, что это за зверь такой — верификация и не очень торопятся узнать об этом. Это несколько удручает, ведь призовых мест было всего три и фактически выходило так, что определялись не лучшие команды, которые победят, а единственная команда, которая не победит.

Обнаруженные командами ошибки были распределены следующим образом: 9, 7, 6, 1 (всего модулей, содержащих ошибки было 14 из 50). Мне кажется, это отличный результат в плане баланса сложности искусственных ошибок.

Собственная работа над ошибками

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

Кроме того, было необходимо формализовать итоговое выступление по полученным результатам, и предоставить шаблон презентации. Вообще, «я и сам своего рода» участник хакатонов, и по моему опыту презентация результатов — чуть ли не самый важный этап, ведь какую бы ты крутую штуку ни сделал — всё будет впустую, если ты не сможешь её «продать». Возможно, в классических хакатонах подобное ведение за ручку излишне, но поскольку участники впервые столкнулись с верификацией подобная формализация помогла бы им грамотно спланировать ход своей работы. Пример того, что участникам было бы полезно рассказать по результатам хакатона:

• Планирование и организация работы; 
• Реализация верификационного окружения; 
• Количество найденных багов и описание наиболее критичных из них.

Кроме того, появились рекомендации по улучшению спецификации на устройство (самым важным кажется добавление временных диаграмм), а так же весовой градации багов по степени их критичности. В процессе хакатона было обнаружена пара проблем при активном использовании CI, которые были исправлены.

Эпилог, или Материалы для заинтересовавшихся верификацией

В первую очередь верификатор должен уметь писать модули на языке Verilog, поэтому лучше всего начать именно с этого. Если вы уже знакомы с языком Verilog и хотите именно познакомиться с верификацией, то необходимо перейти к изучению SystemVerilog, после чего изучить структуру тестбенча и методологию верификации, после чего перейти к изучению UVM:

1. SystemVerilog tutorial for beginners 
2. SystemVerilog TestBench Architecture 
3. UVM Tutorial for Candy Lovers

Разумеется, есть множество других материалов, UVM Cookbook, SystemVerilog Assertions Handbook, которые будет полезно изучить после приобретения базового понимания методологии верификации.

Приведённые в статье ссылки:

1. Pentium FDIV bug (Wikipedia)
2. Cassini-Huygens: Mission to Saturn by the numbers
3. Huygens Landing on Titan (Youtube)
4. Huygens's descent to Titan's surface (Youtube)
5. Cassini-Huygens: Spacecraft navigation
6. Huygens: the missing data
7. Cassini: Unlocking Saturn's Secrets
8. Тест План (План тестирования)
9. The Weather Report: 2018 Study On IC/ASIC Verification Trends
10. Верификация цифровых схем. Обзор (Habr)
11. SystemVerilog Assertions Basics
12. Что такое непрерывная интеграция?
13. SystemVerilog Assertions Design Tricks and SVA Bind Files