MicroTESK: среда генерации тестовых программ для микропроцессоров

MicroTESK: среда генерации тестовых программ для микропроцессоров

MicroTESK (Microprocessor TEsting and Specification Kit) — это среда генерации тестовых программ на языке ассемблера для функциональной верификации микропроцессоров. В качестве источника знания о конфигурации верифицируемого микропроцессора выступают формальные спецификации. Задачи генерации описываются на специальном языке, основанном на Ruby, который позволяет формулировать цели верификации в терминах тестовых ситуаций, извлеченных из формальных спецификаций. Такой подход позволяет упростить настройку среды и повысить уровень тестового покрытия. MicroTESK успешно применяется в промышленных проектах по верификации микропроцессоров ARMv8 и MIPS64.

Основной подход к функциональной верификации микропроцессоров – генерация тестовых программ и анализ результатов их выполнения. Функциональная верификация – чрезвычайно трудоемкая задача, на которую отводится свыше 70% от общего объема трудозатрат. Одна из причин этого – сложность настройки существующих генераторов на создание тестов для новых типов микропроцессоров. В большинстве случаев генератор создан под конкретный микропроцессор и при переходе на новую архитектуру его приходится реализовывать заново. Подход, применяемый в среде MicroTESK, позволяет существенно упростить эту задачу. Он применим для широкого спектра микропроцессоров (RISC, CISC, VLIW, DSP) и предполагает автоматизированное конструирование генераторов на основе формальных спецификаций их архитектуры. При этом генератор состоит из двух частей: (1) ядро, которое реализует общие для всех микропроцессоров методы генерации, и (2) модель, которая содержит знание о конкретном микропроцессоре. Генератор позволяет создавать случайные, комбинаторные и нацеленные тесты на основе тестовых шаблонов, описывающих тестовые сценарии на абстрактном уровне.

Шаблоны для нацеленных тестов описываются в терминах тестовых ситуаций, «интересных» для тестирования событий, происходящих во время работы микропроцессора. Информация о них извлекается из спецификаций при построении модели. При этом условия их возникновения задаются в виде ограничений, которые разрешаются в процессе генерации. Гибкая архитектура среды позволяет легко добавлять поддержку пользовательских методов генерации.

Формальные спецификации системы команд создаются на языке nML, который позволяет описать синтаксис и семантику инструкций, абстрагируясь от деталей реализации. Спецификации включают в себя описание следующих сущностей: (1) элементов хранения данных (память, регистры), определяющих состояние микропроцессора; (2) режимов адресации, реализующих абстракцию доступа к элементам хранения данных; (3) инструкций, выполнение которых изменяет состояние микропроцессора. На Рисунке 1 дан пример спецификации инструкции ADD микропроцессора MIPS и используемых ею ресурсов и показано, как спецификация соотносится с описанием этой инструкции в руководстве по архитектуре MIPS.

Рисунок 1. Инструкция ADD микропроцессора MIPS на языке nML.

MicroTESK включает в себя (1) среду моделирования и (2) среду генерации. Первая отвечает за построение модели микропроцессора на основе формальных спецификаций. Задача второй — построение тестовых программ на основе тестовых шаблонов. Компоненты среды MicroTESK показаны на Рисунке 2.

Рисунок 2. Компоненты среды MicroTESK.

Среда моделирования состоит из расширяемого набор анализаторов спецификаций и генераторов кода. Построенная модель включает в себя: (1) метаданные, хранящие информацию о поддерживаемых регистрах и инструкциях; (2) симулятор, позволяющий выполнять инструкции и отслеживать состояние микропроцессора; (3) модель покрытия, содержащая каталог тестовых ситуаций.

Среда генерации строит тестовые программы на основе тестовых шаблонов, которые описывают задачу генерации на абстрактном уровне, когда состав, порядок и операнды инструкций не фиксируются, а выбираются динамически в зависимости от поставленной задачи. Генерация включает следующие стадии:

1. Анализ тестового шаблона и построение абстрактных последовательностей инструкций.

2. Перебор абстрактных последовательностей и осуществление следующих действий для каждой из них:

• конкретизация последовательности: выбор регистров, генерация данных, построение инициализирующего кода;
• выполнение построенных инструкций на симуляторе;
• построение и вставка в последовательность встроенных проверок на основе данных из симулятора;
• добавление последовательности в поток инструкций;

3. Разбиение потока на программы и их печать в ассемблерном формате.

На Рисунке 3 приведен пример шаблона, описывающего пары инструкций ADD и SUB, вызывающие всевозможные комбинации ситуаций IntegerOverflow (исключение целочисленного переполнения) и Normal (отсутствуют исключения), и сгенерированного на его основе тестового воздействия.

Рисунок 3. Тестовый шаблон и построенное тестовое воздействие.

Получить более подробную информацию можно здесь.

Исполнитель

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