Retrascope – инструмент функциональной верификации модулей цифровой аппаратуры. Retrascope предоставляет автоматизированные средства анализа кода, извлечения формальных моделей и генерации функциональных тестов. В качестве входных данных инструмент принимает описания модулей цифровой аппаратуры на синтезируемых подмножествах языков Verilog и VHDL, а также спецификации поведения. Разработан в Отделе технологий программирования ИСП РАН.
Особенности и преимущества
Retrascope – открытый инструмент функциональной верификации модулей цифровой аппаратуры. Инструмент реализует ряд методов извлечения и анализа формальных моделей, а также генерации функциональных тестов. Модульная архитектура Retrascope позволяет разрабатывать гибридные техники верификации HDL-описаний за счёт комбинирования различных средств анализа формальных моделей. Retrascope доступен на сайте ИСП РАН: https://forge.ispras.ru/projects/retrascope.
Retrascope – это:
- Извлечение формальных моделей из исходного кода:
- граф потока управления;
- решающая диаграмма охраняемых действий;
- высокоуровневая решающая диаграмма;
- расширенный конечный автомат.
- Генерация функциональных тестов:
- случайные тесты;
- выявление недостижимого кода;
- выявление типовых ошибок;
- проверка пользовательских свойств.
- Проверка формальных моделей (model checking) на соответствие спецификациям:
- PSL;
- SystemVerilog Assertions.
- PSL;
- Графический интерфейс на основе Eclipse IDE (также доступен интерфейс командной строки):
- запуск инструмента с параметрами;
- визуализация извлеченных моделей (Zest, GraphML).
- Открытый исходный код (лицензия Apache License Version 2.0).
- Расширяемость на уровне исходного кода:
- добавление новых моделей;
- расширение набора средств анализа.
- Открытые интерфейсы взаимодействия и форматы позволяют использовать различные средства для достижения целей анализа и верификации:
- Проверка формальных моделей (model checking) на соответствие спецификациям:
- SMT-решатели – язык SMT-LIB v2;
- Средства проверки моделей – язык SMV;
- Функциональные тесты – языки VHDL и Verilog, формат VCD.
Системные требования
ОС Windows или ОС на базе ядра GNU/Linux, Java 8.
Схема работы
