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.

    Схема работы

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

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

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

    Перейти к списку всех технологий