Формальные методы цифровой проверки значительно продвинулись за последние пару десятилетий, в основном в поддержку проверки в логике управления и передачи данных. Популярное мнение заключалось в том, что логика пути данных не поддается таким методам. Доказательства контроля/транспортировки зависят от проверки собственности; если доказательство найдено в ограниченном пространстве состояний, оно установлено абсолютно. Для больших проектов проверка часто «ограничена» — доказывается правильность до некоторого количества циклов, но не более. У опытных продуктовых команд обычно не возникало проблем с этим ограничением. Большинство электронных продуктов допускают некоторый порог — возможно, 2 недели или месяц — до того, как потребуется сброс. Но для одного класса функций, путей данных, мы не потерпим никаких ошибок. Они требуют совершенно другого подхода к формальной проверке, что оказывается очень важным для ускорителей машинного обучения с интенсивным использованием математики.
Что такое пути данных и почему их трудно проверить?
Путь данных — это часть вычислительного механизма, которая выполняет обработку данных, в частности математическую обработку. Обычно он поддерживает целые числа, числа с фиксированной запятой и числа с плавающей запятой с рядом параметров точности. Операции варьируются от базовой арифметики до экспонент и журналов, триггеров, гиперболических триггеров и многого другого. Наша нетерпимость даже к случайным ошибкам в такой функциональности наиболее печально продемонстрирована ошибкой Pentium FPDIV, которая, по оценкам, возникает только в одной из 9 миллиардов операций, но считается причиной затрат на замену и списание в размере 475 миллионов долларов и значительным синяком под глазом для Intel. . (Справедливости ради стоит отметить, что Intel сейчас лидирует в применении и развитии современных формальных методов для более полных доказательств.)
Верификация Datapath (DPV) намного превосходит возможности моделирования, как показано на рисунке выше. Более быстрые машины и массовый параллелизм почти не повлияли на эти цифры. В таких случаях должны блистать формальные методы. Но проверка свойств быстро иссякает, потому что ограниченные средства проверки моделей (такие как SAT) могут выполнять поиск только через определенное количество циклов, прежде чем экспоненциально расширяющееся пространство состояний проекта станет неуправляемым. Вместо этого формальные методы для путей данных основаны на проверке эквивалентности. Здесь проверяется эквивалентность не между RTL и проектами на уровне шлюза, а между RTL и эталонными моделями C (или C++ или SystemC). Если эталонная модель пользуется широким доверием (например, Soft-float), это сравнение должно обеспечить высокую уверенность в качестве реализации.
VC Formal DPV и процессор Synopsys ARC NPX6 NPU для ИИ
Synopsys недавно провела вебинар по применению своего формального верификатора пути данных, построенного на этих принципах. После ознакомления с инструментом от Neelabja Dutta Шуайю Цзян из группы ARC рассказал, как он использовал VC Formal DPV для проверки логики пути данных для своего модуля нейронной обработки ARC NP6X (NPU IP.
Пример с ускорителем свертки полезен для понимания того, как команда ARC разложила задачу проверки для того, что я считаю стратегией предположения/проверки, хотя здесь она применяется к проверке эквивалентности. Фаза умножения является одним из таких подкомпонентов. Здесь предполагается, что входные данные для ссылки на C и реализации RTL должны быть одинаковыми. Вместо проверки выходных свойств доказательство определяет «лемму», требующую, чтобы выходные данные были одинаковыми. Аналогичный процесс выполняется для каждого компонента в ускорителе свертки с последующей проверкой на верхнем уровне собранных дополнительных доказательств.
Шуайю также рассказывает о приложении к ARC Generic Tensor Ops Accelerator (GTOA). Вкратце, фреймворки ML (TensorFlow, TF-Lite, PyTorch, JAX и т. д.) работают с тензорными объектами — здесь 2D-изображение x глубина цвета x размер выборки для 4D-тензора. Они основаны на больших наборах операторов, несколько уникальных для каждой сети (> 1000 для TF), что препятствует переносимости, единообразию и т. Д. Следуя философии ISA, Arm разработала и выпустила TOSA — архитектуру набора тензорных операторов с примерно 70 базовыми инструкциями. Платформы и платформы логического вывода, совместимые с TOSA, должны устранять такие несоответствия. Хотя Шуайю не прокомментировал этот момент, я предполагаю, что ARC GTOA построен в соответствии с подходом TOSA. ARC ALU для этих операций обязательно требует еще большей математики, чем пример свертки, что делает его даже лучшим примером для доказательств DPV, соответствующим образом разложенных.
Узнать больше
Вы можете зарегистрироваться для просмотра вебинара ВОТ. Также предлагаю вам прочитать второе издание «Как найти свой путь через формальную проверку (второе издание)». Это было обновлено в нескольких областях с тех пор, как Synopsys выпустила первое издание пять лет назад. Теперь есть целая глава, посвященная DPV. Стоит прочитать — я соавтор 😀
Поделитесь этим постом через:
- SEO-контент и PR-распределение. Получите усиление сегодня.
- Платоблокчейн. Интеллект метавселенной Web3. Расширение знаний. Доступ здесь.
- Источник: https://semiwiki.com/artificial-intelligence/322717-formal-datapath-verification-for-ml-accelerators/
