An approach to test program generation based on formal specifications of caching and address translation mechanisms

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