Снятся ли венд-машинам электрожуки?
Некоторое время назад в МИЭТ прошёл инженерный хакатон YADRO SoC Design Challenge. Данная статья посвящена треку функциональной верификации, для которого я делал задание. Пройдёмся по тому, что такое верификация и как провести хакатон по этому направлению среди тех, кто никогда с ней не сталкивался. Немного скажу и про сложности, с которыми мы столкнулись и результаты проведения хакатона.
Что такое верификация цифровых устройств
В новостях про микроэлектронику мы часто слышим: «разработано устройство X», «выпущено устройство Y». Человек, читающий новости, но не знакомый с устройством микроэлектронной кухни может решить, что тут все только и занимаются тем, что разрабатывают какие-то устройства, ну или готовят их к производству. Ещё часто мы слышим о разного рода экспертах, фондах, связанных с микроэлектроникой, но уж точно не о верификаторах. Где-то на задворках сознания мы понимаем, что устройство мало разработать, надо, наверное, ещё его проверить, но не придаём этому большого значения. А зря. Приведу пару примеров того, почему проверка устройства важна.
Несмотря на то что в большинстве сценариев использования подобная ошибка могла возникнуть крайне редко (по некоторым оценкам ошибка возникала один раз из девяти миллиардов делений), и в большинстве подобных случаев она давала ошибку в девятом значащем разряде после запятой, в некоторых сценариях ошибка могла возникать чаще и выдавать на порядки большие отклонения (до четвёртого значащего разряда).
Компания Intel была вынуждена признать, что проблема им была известна, и её исправили в будущих ревизиях устройства. Проводить отзывную кампанию и отдавать пользователям новый выпуск процессоров не стали, сославшись на то, что проблема узконаправленная и конечный пользователь вряд ли её обнаружит.
В результате всеобщей критики и поднявшейся шумихи, Intel всё-таки пришлось отозвать всю партию бракованных процессоров и отправить клиентам новые чипы, что вылилось в огромные убытки и репутационный урон.[1]
График демонстрирует одно из проявлений ошибки деления. Каждый отсчёт должен быть выше по оси Y относительно предыдущего примерно на 3.1789×10^-8, однако на отрезке (4195834.4:4195835.9) результат отличается от ожидаемого примерно на 8.14×10^−5.
Здесь важно отметить, что баг не был обнаружен не потому, что Intel ничего не проверяла, просто сам баг проявлялся крайне редко и не попался при верификации. С тех пор микроэлектронная промышленность научилась избегать подобных ошибок альтернативными методами верификации.
Проект «Кассини-Гюйгенс» берёт своё начало в 1982-ом году, когда NASA и ESA (Европейское космическое агентство) сформировали рабочую группу по совместным проектам. Было решено исследовать Сатурн и его спутник Титан. Сатурн планировалось исследовать посредством орбитальной станции («Кассини»), а Титан — с помощью спускаемого аппарата с автоматической станцией «Гюйгенс».
Автоматическая межпланетная станция (АМС) «Кассини-Гюйгенс» была запущена 15 октября 1997 года, а 14 января 2005 года, спускаемый аппарат отделился от орбитальной станции и вошёл в атмосферу спутника Сатурна, Титана, обеспечив мягкую посадку автоматической станции на его поверхность. Программа два раза продлевалась и завершилась в 2017 году. За это время в миссии поучаствовало 27 стран, было собрано 635 ГБ данных, сделано 453 048 фотоснимков и написано 3 948 статей.[2]
Видео спуска аппарата Гюйгенс, смонтированное по переданным им снимкам.
И ещё одно видео, с современной обработкой и комментированием происходящего.
Пара ошибок поставила под угрозу часть успеха этой миссии.
Ещё до того как «Кассини-Гюйгенс» достигла Сатурна, инженеры ESA пришли к выводу, что при проектировании системы приёмника «Кассини» не был должным образом учтён эффект Допплера, связанный со спуском аппарата «Гюйгенс». Орбитальную станцию «Кассини» предполагалось вести прямо позади аппарата «Гюйгенс»: как раз там, где допплеровский сдвиг был бы наибольший. Это означало, что «Гюйгенс» отправлял бы данные с частотой, которую бы не воспринял приёмник на борту «Кассини».
Работая вместе с коллегами из ESA, навигационная команда «Кассини» смогла найти решение. Они изменили траекторию Кассини таким образом, чтобы её расположение оказалось перпендикулярно пути спускаемого аппарата. При таком расположении эффект Допплера оказался минимальным, что позволило продолжить миссию «Гюйгенса».[5]
Вторую ошибку обнаружить заранее, к сожалению, не удалось. В результате учёные из группы по обработке изображений с «Гюйгенса» получили только половину изображений со спуска аппарата. Ожидалось, что за время двух-с-половиной-часового полёта они получат более 700 изображений, однако получили только 350. Данные по эксперименту с эффектом Допплера, во время которого измерялись мельчайшие изменения в скорости ветра, испытываемого «Гюйгенсом» также оказались потеряны. Логичный вопрос, который возникает — как же так вышло?
Во время спуска на Титан, аппарат «Гюйгенс» передавал непрерывный поток данных на орбитальную станцию «Кассини». Та собирала все данные по спуску, прежде чем повернуться в сторону Земли и отправить данные ожидающим их учёных. Передача со стороны «Гюйгенса» шла по двум каналам: А и Б, которые использовали слегка различающиеся частоты СВЧ-диапазона. Большая часть данных дублировалась каждым из каналов подобно двум радиостанциям, транслирующим одну и ту же передачу.
Эта избыточность спасла миссию от провала. На «Кассини» было расположено два различных приёмника для сбора данных с «Гюйгенса», и один из них не работал. Почему один из них не работал? Оказалось, приёмник канала А не был включён. По словам учёных, из группы обработки изображений, приёмнику попросту не отправили такую команду.
Дэвид Саутвуд (научный руководитель ESA) отметил, что не важно, кто именно пропустил критическую инструкцию, поскольку ответственность лежит шире: ошибку должны были найти во время проверок[6].
Изображения не дублировались подобно остальным данным, потому что группа по обработке изображений, пожертвовала избыточной передачей в попытке получить как можно больше данных с Титана. Вместо того, чтобы отправить одни и те же изображения дважды, они чередовали их по обоим каналам. Если бы это сработало, они получили бы 700 изображений.
Вот так из-за ошибок, не выявленных на этапе верификации конечного устройства, может быть поставлен под угрозу дорогостоящий научный проект, над которым работали три поколения астрономов и инженеров.[7]
А какие примеры известных и интересных ошибок знаете вы? Буду рад, если поделитесь в комментариях.
Теперь давайте пройдёмся по самому термину «верификация». В случае цифрового устройства, верификация — это подтверждение того, что устройство соответствует спецификации и делает то, что должно делать, в то же время не делая того, чего не должно.
Стоит отметить, что верификация не является синонимом проверки и вот почему. Вы можете «проверить», что холодильник работает, открыв дверь, увидев, что лампочка загорелась, а внутри холодно. Если вы захотите верифицировать холодильник, то вам придётся ознакомиться с условиями эксплуатации и характеристиками холодильника, провести ряд тестов на то, поддерживает ли холодильник нужную температуру, и что та отклоняется только в допустимых пределах. Что в случае отключения света, холодильник держит температуру на протяжении указанного времени. Что если оставить дверцу холодильника открытой, тот автоматически отключится через какое-то время во избежание поломки. Вам потребуется проверить такие функции, как защиту от обледенения задней стенки (если таковая функция имеется) и т.п. Верификация — это всестороннее исследование объекта верификации на соответствие заявленным характеристикам.
Для проведения верификации инженеру необходимо составить план — документ, описывающий весь объём работ начиная с описания объекта, стратегии, расписания, критериев начала и окончания верификации, и заканчивая необходимым в процессе работы оборудованием, специальными знаниями, а также оценками рисков с вариантами их разрешения.[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).
Непрерывная интеграция (CI) — это процесс автоматизации сборки и запуска тестов каждый раз, когда член команды фиксирует изменения в системе управления версиями.[12]
Как встроить в проверяемые модули конструкции 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, в которой разместили репозиторий-шаблон. Для каждой команды участников на основе этого шаблона был создан приватный репозиторий (чтобы участники не могли видеть работы других участников). В этом репозитории находились:
- Референсный дизайн.
- Модуль-заготовка, в котором необходимо прописать конструкции SVA.
- Тестбенч.
- Readme-файл с руководством по использованию репозитория и инструментов, спецификация и задание.
Участникам предоставлен модуль-заготовка, в котором необходимо прописать конструкции SVA. Входные и выходные сигналы этого модуля — это входные, выходные сигналы проверяемого модуля, а также его архитектурные регистры, описанные в спецификации на устройство. По этим сигналам необходимо написать утверждения, проверить их работоспособность на референсном модуле, после чего закоммитить в свой репозиторий и получить результат автоматизированного запуска тестов — в случае обнаружения ошибок проверить временную диаграмму и, если это не ложноположительное срабатывание зафиксировать обнаружение ошибочного дизайна.
Взаимодействие с репозиторием со стороны участников
На этой странице находился детальный лог по каждому из тестов, в который входят и сообщения о сработавших assertions (в настройках симуляции стоит опция assertion fail -r / -limit 5 отключающая вывод утверждения, сработавшего более пяти раз, чтобы не загромождать лог).
Результаты
По итогам хакатона каждая из команд нашла хотя бы одну ошибку. К сожалению (или счастью), ошибок в референсном дизайне не было обнаружено. Всего участвовало четыре команды — следствие того, что студенты не знают, что это за зверь такой — верификация и не очень торопятся узнать об этом. Это несколько удручает, ведь призовых мест было всего три и фактически выходило так, что определялись не лучшие команды, которые победят, а единственная команда, которая не победит.
Обнаруженные командами ошибки были распределены следующим образом: 9, 7, 6, 1 (всего модулей, содержащих ошибки было 14 из 50). Мне кажется, это отличный результат в плане баланса сложности искусственных ошибок.
Собственная работа над ошибками
Разумеется, многое можно было сделать лучше. В частности, можно было постараться лучше донести, какие именно шаги необходимо предпринять участникам для успешного выполнения задания. Одна из команд пошла не тем путём, и пыталась хакнуть обфусцированный тестбенч. Не знаю уж, чего они пытались добиться, но день был потрачен впустую. Нам, как организаторам, нужно было лучше проработать этот момент.
Кроме того, было необходимо формализовать итоговое выступление по полученным результатам, и предоставить шаблон презентации. Вообще, «я и сам своего рода» участник хакатонов, и по моему опыту презентация результатов — чуть ли не самый важный этап, ведь какую бы ты крутую штуку ни сделал — всё будет впустую, если ты не сможешь её «продать». Возможно, в классических хакатонах подобное ведение за ручку излишне, но поскольку участники впервые столкнулись с верификацией подобная формализация помогла бы им грамотно спланировать ход своей работы: пример того, что участникам было бы полезно рассказать по результатам хакатона:
- Планирование и организация работы;
- Реализация верификационного окружения;
- Количество найденных багов и описание наиболее критичных из них.
Кроме того, появились рекомендации по улучшению спецификации на устройство (самым важным кажется добавление временных диаграмм), а так же весовой градации багов по степени их критичности. В процессе хакатона было обнаружена пара проблем при активном использовании CI, которые были исправлены.
Эпилог, или Материалы для заинтересовавшихся верификацией
В первую очередь верификатор должен уметь писать модули на языке Verilog, поэтому лучше всего начать именно с этого. Если вы уже знакомы с языком Verilog и хотите именно познакомиться с верификацией, то необходимо перейти к изучению SystemVerilog, после чего изучить структуру тестбенча и методологию верификации, после чего перейти к изучению UVM:
- SystemVerilog tutorial for beginners
- SystemVerilog TestBench Architecture
- UVM Tutorial for Candy Lovers
Разумеется, есть множество других материалов, UVM Cookbook, SystemVerilog Assertions Handbook, которые будет полезно изучить после приобретения базового понимания методологии верификации.
Приведённые в статье ссылки:
- Pentium FDIV bug (Wikipedia)
- Cassini-Huygens: Mission to Saturn by the numbers
- Huygens Landing on Titan (Youtube)
- Huygens’s descent to Titan’s surface (Youtube)
- Cassini-Huygens: Spacecraft navigation
- Huygens: the missing data
- Cassini: Unlocking Saturn’s Secrets
- Тест План (План тестирования)
- The Weather Report: 2018 Study On IC/ASIC Verification Trends
- Верификация цифровых схем. Обзор (Habr)
- SystemVerilog Assertions Basics
- Что такое непрерывная интеграция?
- SystemVerilog Assertions Design Tricks and SVA Bind Files
