Retrascope: инструмент статического анализа hdl-описаний

Retrascope: инструмент статического анализа hdl-описаний

Retrascope – инструмент функциональной верификации модулей цифровой аппаратуры. Retrascope предоставляет автоматизированные средства анализа кода, извлечения формальных моделей и генерации функциональных тестов. В качестве входных данных инструмент принимает описания модулей цифровой аппаратуры на синтезируемых подмножествах языков Verilog и VHDL, а также спецификации поведения.

Особенности и преимущества

Retrascope – открытый инструмент функциональной верификации модулей цифровой аппаратуры. Инструмент реализует ряд методов извлечения и анализа формальных моделей, а также генерации функциональных тестов. Модульная архитектура Retrascope позволяет разрабатывать гибридные техники верификации HDL-описаний за счёт комбинирования различных средств анализа формальных моделей.

Retrascope доступен на сайте ИСП РАН: https://forge.ispras.ru/projects/retrascope.

Retrascope – это:

Извлечение формальных моделей из исходного кода:

• граф потока управления;
• решающая диаграмма охраняемых действий;
• высокоуровневая решающая диаграмма;
• расширенный конечный автомат.

Генерация функциональных тестов:

• случайные тесты;
• выявление недостижимого кода;
• выявление типовых ошибок;
• проверка пользовательских свойств.

Проверка формальных моделей (model checking) на соответствие спецификациям:

• PSL;
• SystemVerilog Assertions.

Графический интерфейс на основе Eclipse IDE (также доступен интерфейс командной строки):

• запуск инструмента с параметрами;
• визуализация извлеченных моделей (Zest, GraphML).

Открытый исходный код (лицензия Apache 2.0).

Расширяемость на уровне исходного кода:

• добавление новых моделей;
• расширение набора средств анализа.

Открытые интерфейсы взаимодействия и форматы позволяют использовать различные средства для достижения целей анализа и верификации:

• SMT-решатели – язык SMT-LIB v2;
• Средства проверки моделей – язык SMV;
• Функциональные тесты – языки VHDL и Verilog, формат VCD.

Для кого предназначен Retrascope?

• Компании, занимающиеся проектированием цифровой аппаратуры.
• Коллективы, проводящие исследования в области функциональной верификации цифровой аппаратуры.

Опыт внедрения

Инструмент находится на стадии исследовательского прототипа, ведётся разработка.

Системные требования

ОС Windows или ОС на базе ядра GNU/Linux, Java 8.

Схема работы

Разработчик/участник

Технологии программирования