MicroTESK: генератор тестовых программ

MicroTESK: генератор тестовых программ

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

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

MicroTESK – комплекс технологий для промышленного использования, включающий в себя базовую среду моделирования (строит модели микропроцессоров на основе формальных спецификаций) и среду генерации (строит тестовые программы на основе шаблонов). По решаемым задачам близок к мировым аналогам (Genesys Pro и RAVEN), однако отличается от них повышенной производительностью и удобством использования. Распространяется по лицензии Apache 2.0. MicroTESK доступен на сайте ИСП РАН: 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 11.

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

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

Схема работы

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

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