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 License Version 2.0).
      • Расширяемость на уровне исходного кода:
        • добавление новых моделей;
        • расширение набора средств анализа.
      • Открытые интерфейсы взаимодействия и форматы позволяют использовать различные средства для достижения целей анализа и верификации:
    • SMT-решатели – язык SMT-LIB v2;
    • Средства проверки моделей – язык SMV;
    • Функциональные тесты – языки VHDL и Verilog, формат VCD.

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

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

Схема работы