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.

Схема работы