Генератор тестовых программ для архитектуры ARMv8 на основе инструмента MicroTESK

ARM - это семейство микропроцессорных архитектур, разработанных в одноименной компании. Новейшая архитектура этого семейства, ARMv8, содержит большое число команд разных типов и отличается сложной организацией виртуальной памяти (включающей аппаратную поддержку многоуровневой трансляции адресов и виртуализации); все это делает функциональную верификацию микропроцессоров этой архитектуры крайне трудной технической задачей. Неотъемлемой частью верификации микропроцессора является генерация тестовых программ - программ на языке ассемблера, создающих разнообразные ситуации (исключения, блокировки конвейера, неверные предсказания переходов, вытеснения данных из кэш-памяти и т.п.). В статье описываются требования, предъявляемые к промышленным генераторам тестовых программ, и представляется генератор для микропроцессоров архитектуры ARMv8, разработанный с использованием инструмента MicroTESK (Microprocessor TEsting and Specification Kit). Генератор поддерживает подмножество команд, характерное для мобильных приложений (около 400 команд) и состоит из двух основных частей: (1) архитектурно независимого ядра и (2) формальной спецификации ARMv8 (точнее, модели, автоматически построенной по формальным спецификациям). При такой организации процесс разработки генератора тестовых программ состоит преимущественно в создании формальных спецификаций, что экономит усилия за счет повторного использования архитектурно независимых компонентов. Архитектура описывается на языках nML и mmuSL: первый язык позволяет описывать регистры микропроцессора, синтаксис и семантику команд; второй - устройство подсистемы памяти (адресные пространства, разного рода буферы и таблицы, алгоритмы трансляции адресов и т.п.). В статье приводятся характеристики разработанного генератора и делается сравнение с существующими аналогами.