Лаборатория информационных технологий им. М. Г. Мещерякова
Общелабораторный семинар
Дата и время: вторник, 17 ноября 2026 г., в 11:00
Место: комната 310, Лаборатория информационных технологий
им. М. Г. Мещерякова, онлайн в MTS Link
Информация о семинаре в Indico
Тема семинара: «Метод и программные средства статического анализа описаний цифровой аппаратуры для выявления дефектов проектирования»
Докладчик: Ян Чуркин (Институт системного програмирования РАН)
Одним из основных способов описания аппаратуры при проектировании процессоров и систем на кристалле является описание на уровне регистровых передач (RTL) с использованием языков Verilog и SystemVerilog. В крупных проектах объем RTL-описаний достигает сотен тысяч и миллионов строк. Дефекты, внесенные в RTL-описание, нередко обнаруживаются лишь на поздних этапах проектирования, когда их исправление обходится дорого. Статический анализ позволяет выявлять такие дефекты до имитационного моделирования и логического синтеза. Однако промышленные анализаторы закрыты для расширения, а открытые инструменты не поддерживают SystemVerilog в полном объеме и не анализируют конечные автоматы. В докладе представлен метод статического анализа описаний цифровой аппаратуры на основе многоуровневого внутреннего представления, построенного над развернутой моделью проекта. Сформулирован набор из 118 правил, и каждому правилу сопоставлена достаточная для его проверки техника анализа: обход абстрактного синтаксического дерева, анализ путей с интервальными ограничениями, анализ потоков данных с отслеживанием диапазонов значений сигналов и другие. Для разработки детекторов предложен предметно-ориентированный язык сопоставления узлов синтаксического дерева. Разработан метод извлечения конечных автоматов по сети логических элементов, не зависящий от стиля кодирования. Метод выявляет мертвые переходы, недостижимые и тупиковые состояния и взаимоблокировки, которые определяются через терминальные сильно связные компоненты графа автомата. Предложена единая информационная модель, связывающая описание аппаратуры с библиотеками ячеек Liberty, описанием подсистемы питания в формате UPF и SDF-описаниями задержек. На ее основе разработана статическая проверка стратегий изоляции и преобразования уровня напряжения. Методы реализованы в системе статического анализа SVAN. Экспериментальная оценка на десяти открытых проектах общим объемом свыше 1,8 млн строк показала точность детекторов правил 96,3 % и точность анализа конечных автоматов 95,5 %. Разработчики открытых проектов подтвердили 13 из 24 сообщенных им нарушений. Приводится сравнение с коммерческим инструментом SpyGlass и пятью открытыми инструментами.
(По материалам кандидатской диссертации.)