?
An Approach to Test Program Generation Based on Formal Specifications of Caching and Address Translation Mechanisms
Подсистема памяти является одним из ключевых компонентов микропроцессора. Она включает в себя набор запоминающих устройств различного назначения, объединенных в сложную иерархическую структуру. При этом количество возможных состояний подсистемы крайне велико. По этой причине верификация ее функциональной корректности представляет собой нетривиальную задачу. В настоящее время наиболее часто применяемым на практике подходом к функциональной верификации микропроцессоров является генерация и симуляция тестовых программ. Для достижения должного уровня тестового покрытия применяемые методы генерации тестовых программ должны обеспечивать высокий уровень автоматизации и систематичность тестирования. В данной работе предложен метод генерации тестовых программ для функциональной верификации блока управления памятью микропроцессора. В основе метода лежат формальные спецификации инструкций доступа к памяти, а именно инструкций чтения и записи, и устройств памяти, таких как блоки кэш-памяти и буферы трансляции адресов. Использование формальных спецификаций помогает автоматизировать разработку генераторов тестовых программ и обеспечивает систематичность верификации благодаря четкому определению целей тестирования. В предложенном подходе тестовые программы составляются при помощи комбинаторных методов. Т.е. тестовые воздействия (последовательности инструкций чтения и записи) создаются путем перечисления всех возможных комбинаций инструкций, ситуаций (путей выполнения инструкций) и зависимостей (множеств конфликтов между инструкциями). Важно отметить, что тестовые ситуации и зависимости автоматически извлекаются из спецификаций. Данный подход применялся в нескольких промышленных проектах и позволил выявить критические ошибки в механизмах управления памятью.