HabrФормальная верификация «для богатых»: используем 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, из каких этапов состоит процесс верификации с ним, как формируются проверки (ассерты) и с какими ограничениями здесь сталкиваются инженеры.
