Формальная спецификация подсистемы управления памятью
На вход генератору тестовых программ подаются формальные спецификации инструкций. Спецификация отдельной инструкции включает в себя описание интерфейса инструкции, функцию выполнения инструкции и ассемблерный формат. В интерфейсе инструкции описываются ее операнды и предусловие. Функция выполнения инструкции вычисляет значения выходных операндов инструкции и обновляет модельное состояние микропроцессора. Ассемблерный формат определяет запись инструкции на языке ассемблера.
Для того чтобы описать семантику инструкций, работающих с памятью, необходимо смоделировать устройства MMU, в частности, буфер трансляции адресов и кэш-память. Все такие устройства могут быть описаны однотипным образом путем задания следующих параметров:
- уровень ассоциативности;
- число множеств;
- функция вычисления тэга;
- функция вычисления индекса;
- структура блока данных;
- управляющие биты;
- стратегия замещения данных при промахе.
В используемом генераторе тестовых программ для разработки формальных спецификаций используется язык программирования Java . Нами разработана библиотека абстрактных классов, позволяющая путем механизма наследования и перегрузки методов (соответствующих указанным выше параметрам) получать спецификации основных устройств MMU. Объекты полученных спецификационных классов можно использовать для определения семантики инструкций, вызывая необходимые интерфейсные методы (чтение, запись и т.п.).
Моделирование подсистемы управления памятью позволяет генератору автоматически строить цепочки инициализирующих инструкций, приводящих микропроцессор в соответствующее тестовой ситуации состояние.