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