Мы работаем для Вас!

14.апр.2026

Формальная верификация «для богатых»: используем Jasper C2RTL App из Cadence JasperGold

Приве! Меня зовут Андрей, я занимаюсь в YADRO верификацией аппаратного обеспечения. В разработке цифровых устройств (GPU, CPU, AI-ускорители) большое внимание уделяют трактам обработки данных (datapath). Архитекторы создают эталонные модели блоков на языках высокого уровня (C/C++), чтобы быстрее проводить архитектурные исследования и отладку алгоритмов — например, операции с плавающей точкой, полиномы, матричные умножения. Однако конечная реализация выполняется на RTL (Verilog/SystemVerilog).После реализации в виде RTL-кода всегда хочется проверить соответствие итогового дизайна оригинальной модели. В этот момент в мире ASIC-разработки часто начинают думать сразу о UVM, корнер-кейсах и прочих долгих прелюдиях перед оформлением багов.В качестве альтернативы здесь выступает формальная верификация. Если вы работаете в небольшом стартапе, то, скорее всего, вам нужен маршрут формальной верификации, описанный моим коллегой в статье «Формальная верификация „для бедных“: выбираем open-source решение». Но если вам повезло работать в крупной полупроводниковой компании с доступом к коммерческим инструментам формальной верификации, то можно подумать о проверке логической эквивалентности между C и RTL-кодом.Один из популярных инструментов для такой проверки — это Jasper C2RTL App в составе платформы Cadence JasperGold. По механике он очень похож на известные многим инструменты LEC и SEC, но в качестве эталонной реализации здесь выступает код на C.В этой статье мы рассмотрим, как работает C2RTL, из каких этапов состоит процесс верификации с ним, как формируются проверки (ассерты) и с какими ограничениями здесь сталкиваются инженеры. Читать далее
Название: Формальная верификация «для богатых»: используем Jasper C2RTL App из Cadence JasperGold
Ссылка на источник:  https://habr.com/ru/companies/yadro/articles/1022818/?utm_source=habrahabr&utm_medium=rss&utm_campaign=1022818