MicroTESK – реконфигурируемая и расширяемая среда генерации тестовых программ для функциональной верификации микропроцессоров. Позволяет автоматически конструировать генераторы тестовых программ для целевых архитектур микропроцессоров на основе их формальных спецификаций. MicroTESK применим для широкого спектра архитектур (RISC, CISC, VLIW, DSP). Поддерживает онлайн-генерацию тестовых программ. Разработан в Отделе технологий программирования ИСП РАН.

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

MicroTESK – комплекс технологий для промышленного использования, включающий в себя базовую среду моделирования (строит модели микропроцессоров на основе формальных спецификаций) и среду генерации (строит тестовые программы на основе шаблонов). По решаемым задачам близок к мировым аналогам (Genesys Pro и RAVEN), однако отличается от них повышенной производительностью и удобством использования, а также распространением по лицензии открытого исходного кода Apache 2.0.

Выложен в открытом доступе на сайте ИСП РАН: https://forge.ispras.ru/projects/microtesk. Описание технологии доступно на сайте http://www.microtesk.org/.

MicroTESK – это:

  • Использование формальных спецификаций в качестве источников знаний о конфигурации верифицируемого микропроцессора:
  • спецификации архитектуры на nML (регистры, память и режимы адресации, логика инструкций, текстовый/двоичный формат инструкций);
  • дополнительные спецификации подсистемы памяти на mmuSL (свойства буферов памяти (TLB, L1 и L2), логика трансляции адресов и логика операций чтения и записи);
  • потенциальная возможность перехода к формальной верификации, а также генерации набора инструментов для разрабатываемого микропроцессора (дизассемблер, эмулятор и др.)
    • Генерация тестовых программ на основе объектно-ориентированных тестовых шаблонов:
  • тестовые шаблоны на языке Ruby (за счёт чего шаблоны наглядны и удобны в поддержке);
  • возможность одновременного использования различных техник генерации наборов инструкций и тестовых данных (случайная генерация, комбинаторная генерация, генерация на основе разрешения ограничений и др.);
  • масштабируемость среды генерации (возможность разрабатывать сложные шаблоны при небольших затратах за счет повторного использования).
    • Широкий набор поддерживаемых архитектур микропроцессоров:
  • поддержка особенностей различных классов архитектур на уровне среды разработки генераторов (RISC, CISC, VLIW, DSP);
  • разработаны генераторы тестовых программ на основе MicroTESK для таких архитектур, как RISC-V, ARM, MIPS, PowerPC;
  • поддерживается многоядерность целевой микропроцессорной архитектуры.
  • Оперативная настройка среды под новые архитектуры с минимальными затратами и автоматическое извлечение информации о тестовых ситуациях (благодаря формальным спецификациям).
  • Удобный язык разработки тестовых шаблонов, позволяющий быстро описывать сложные сценарии верификации.
  • Поддержка онлайн-генерации тестовых программ для проведения пост-производственной верификации целевого микропроцессора. Онлайн-генерация осуществляется исполняемым генератором, входящим в состав MicroTESK. Он использует текстовый и двоичный форматы инструкций, которые извлекаются из тех же самых формальных спецификаций. Проверка корректности осуществляется с помощью множественного исполнения наборов тестовых последовательностей: оригинальных и с функционально-эквивалентными заменами.

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

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

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

MicroTESK разрабатывается с 2007 года. Использовался в российских и международных проектах по разработке современных индустриальных микропроцессоров (в частности, в промышленных проектах по верификации микропроцессоров ARMv8, MIPS64 и RISC-V).

Схема работы