Сборники трудов ИСП РАН


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

А.С. Камкин (ИСП РАН, Москва, Россия, МГУ, Москва, Россия, МФТИ, Долгопрудный, Россия)
А.М. Коцыняк (ИСП РАН, Москва, Россия)
А.Д. Татарников (ИСП РАН, Москва, Россия)
М.М. Чупилко (ИСП РАН, Москва, Россия)

Аннотация

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

Ключевые слова

микропроцессоры, спецификация системы команд, функциональная верификация, генерация тестовых программ, ARM, nML, MicroTESK

Издание

Труды Института системного программирования РАН, том 28, вып. 6, 2016, стр. 87-102.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(6)-6

Полный текст статьи в формате pdf Вернуться к содержанию тома