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


Метод генерации тестовых программ на основе формальных спецификаций механизмов кэширования и трансляции адресов

А.С. Камкин, А.С. Проценко, А.Д. Татарников

Аннотация

Подсистема памяти является одним из ключевых компонентов микропроцессора. Она состоит из запоминающих устройств разного назначения (буферов инструкций, буферов трансляции адресов, многоуровневой кэш-памяти, основной памяти и других), объединенных в сложную иерархическую структуру. Число возможных состояний подсистемы памяти крайне велико, что делает ее функциональную верификацию чрезвычайно трудоемкой задачей. В настоящее время основным подходом к функциональной верификации микропроцессоров на системном уровне является имитационное моделирование с использованием автоматически сгенерированных тестовых программ. В данной работе предлагается метод генерации тестовых программ для функциональной верификации модулей управления памятью микропроцессоров. В основе предложенного метода лежат формальные спецификации инструкций доступа к памяти, а именно инструкций чтения и записи, и формальные спецификации устройств памяти, таких как модули кэш-памяти и буферы трансляции адресов. Использование формальных спецификаций позволяет автоматизировать разработку генераторов тестовых программ и обеспечивает систематичность функциональной верификации за счет четкого определения целей тестирования. В предложенном подходе тестовые программы конструируются с помощью комбинаторных техник, то есть тестовые воздействия (последовательности инструкций чтения и записи) создаются путем перебора всех возможных комбинаций инструкций, ситуаций (путей исполнения инструкций) и зависимостей (множеств конфликтов между инструкциями). Важной особенностью метода является то, что тестовые ситуации и зависимости автоматически извлекаются из формальных спецификаций. Предложенный подход применялся в нескольких промышленных проектах по верификации микропроцессоров архитектуры MIPS и позволил выявить критические ошибки в механизмах управления памятью.

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

микропроцессоры; управление памятью; кэширование; трансляция адресов; функциональная верификация; формальные спецификации; генерация тестовых программ; генерация потока инструкций.

Издание

Труды Института системного программирования РАН, том 27, вып. 3, 2015, стр. 125-138.

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

DOI: 10.15514/ISPRAS-2015-27(3)-9

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