Большие языковые модели приближаются к выполнению одной из самых раздражающих задач верификации проектирования микросхем: преобразованию спецификаций, написанных на естественном языке, в набор формальных свойств, которые можно использовать для оценки корректности реализации RTL. Интервью, проведённые Brian Bailey в Semiconductor Engineering, показывают, что существующие инструменты способны создавать полезный первоначальный черновик, но всё ещё далеки от создания полного набора, который можно было бы принять без тщательной инженерной проверки.
Важность этого развития связана с тем, что написание свойств уже много лет представляет собой узкое место формальной верификации. Свойства SystemVerilog, известные как assertions при включении в среду верификации, используются для описания логических и временных отношений между сигналами, таких как поведение сброса, рукопожатия, условия one-hot и базовые проверки безопасности. Когда эти свойства полны и точны, их можно использовать для сопоставления поведения реализации RTL со спецификацией независимо от способа построения проекта.
Что инструменты умеют делать сегодня?
Инструмент на основе большой языковой модели может прочитать документ со спецификацией, стандарт протокола или даже комментарии внутри RTL, а затем предложить черновик свойств SVA. По словам Ashish Darbari, генерального директора Axiomise, такое применение более реализуемо, когда спецификации опираются на устоявшиеся стандарты, которые не слишком часто меняются. В этом случае инструмент снимает повторяющуюся часть работы по написанию исходного кода, а не берёт на себя весь процесс верификации.
Некоторые методы пытаются повысить точность моделей за счёт создания knowledge graph, то есть графа знаний, в котором хранятся сущности и связи между ними. Узлами могут быть сигнал, модуль, требование или порт, а рёбра описывают такие отношения, как «управляет», «сбрасывает» и «реагирует на». Вместо извлечения фрагментов текста, которые лишь кажутся связанными с запросом, система может обращаться к конкретным фактам и связям, снижая вероятность выдумать имя сигнала или неправильно понять отношение между компонентами проекта. Источник упоминает в этом контексте исследование Cohen и Chibani под названием RAG-SVA in the Landscape of LLM-Based Assertion Generation.
Проблема начинается ещё до искусственного интеллекта
Инструмент не может извлечь то, что изначально не было написано или решено. По словам Ravindra Aneja, директора по инженерии приложений в Synopsys, идеальная спецификация не была доступна на протяжении последних трёх десятилетий: разработка часто начинается до завершения документации, а в некоторых проектах полной спецификации может не существовать вовсе, особенно в производных разработках или когда требования меняются в процессе работы.
Эта проблема связана не только с формулировками, но и с управлением изменениями. Маркетинговая команда может добавить новую функцию или изменить существующее требование, и команде проектирования и верификации необходимо определить влияние этого изменения. Abhi Kolpekwa, старший вице-президент и генеральный директор Siemens EDA, считает, что преобразование спецификации в свойства требует «контекстного интеллекта», который отслеживает историю изменений и их контекст, а не агента, каждый раз генерирующего новый текст.
Опасность ложной уверенности
Главное ограничение современного подхода заключается в том, что свойство может быть синтаксически корректным: оно компилируется, и инструменты верификации успешно доказывают его, но при этом не проверяет фактически требуемое поведение. Darbari предупреждает, что слабое или vacuous-свойство может быть легко доказано, поскольку допускает множество вариантов поведения, использует неправильный сигнал либо содержит отсутствующее или чрезмерно ограниченное предварительное условие. Поэтому «зелёное доказательство» не означает, что проект лишён ошибок: доказательство не может быть сильнее свойства, которое было доказано.
Источник также отмечает, что модели обычно лучше справляются со структурным и синтаксическим покрытием, чем с пониманием архитектурного замысла и причины существования правила. Поэтому неточное прочтение спецификации моделью может превратиться в формальный и строгий на вид фрагмент, скрывающий пробел в требованиях. Если этот пробел перейдёт в такие работы, как FMEDA, документы по безопасности или материалы сертификации, связанные с ISO 26262 и ISO 21434, его последствия могут выйти далеко за пределы первоначального проекта верификации.
Возникает также вопрос разделения проектирования и верификации. Kaye Mao, руководитель направления разработки продуктов в Normal Computing, указывает на необходимость ограничить доступ агентов к материалам проекта, поскольку разрешение агенту использовать сам проект для генерации тестовых случаев может подорвать независимость процесса верификации.
Что меняется на практике?
По словам Darbari, искусственный интеллект может сократить время подготовки первых черновиков с дней до минут, но при этом увеличить объём последующей работы. Каждое сгенерированное свойство требует проверки на соответствие спецификации, анализа покрытия, проверки на vacuity и анализа его связи с сигналами проекта; сбои также могут потребовать анализа временных диаграмм сигналов. Если число свойств увеличится в десять раз, а требуемый уровень проверки каждого из них останется прежним, нагрузка на проверку может превысить выигрыш от быстрого создания.
С точки зрения certi.news, реальное изменение заключается не в замене инженера по верификации, а в переносе центра тяжести с написания свойств на их оценку и отслеживание их источника. Darbari рекомендует рассматривать сгенерированные свойства как черновики, а не как утверждённые результаты, и создавать шлюз проверки перед их включением в regression suite. Следует также фиксировать источник каждого свойства: абзац спецификации, требование или элемент RTL, на основе которого оно было создано, чтобы инженер мог проверить соответствие.
Этот подход может снизить порог входа для инженеров по верификации, желающих использовать formal verification, как говорит Yaron Ilani, инженер решений по верификации в Normal Computing. Однако он не решает вопрос окупаемости инвестиций. Kaye Mao считает, что время проверки результатов работы агента должно учитываться в затратах, тогда как Arvind Srinivasan, главный инженер по решениям в Normal Computing, указывает, что масштабирование связано не только с вычислительными ресурсами, но и с полнотой данных и стоимостью человеческой проверки.
Вывод заключается в том, что большие языковые модели уже способны ускорить автоматическую и повторяющуюся часть формулирования свойств, но пока не решили проблемы полноты спецификации и понимания проектного замысла. Ценность этих инструментов по-прежнему будет зависеть от наличия инженера, понимающего проект, и независимых механизмов измерения покрытия и обнаружения пустых или неподходящих свойств, а не от количества свойств, которые способна создать модель.