Практическая апробация подхода
Мы применили описанный подход для тестирования подсистемы управления памятью MIPS64-совместимого микропроцессора. В качестве тестовых воздействий использовались всевозможные пары, составленные из четырех инструкций: lb (загрузка байта), ld (загрузка двойного слова), sb (сохранение байта) и sd (сохранение двойного слова). Структура используемых тестовых ситуаций и зависимостей была близка к описанной в статье, но были дополнительно учтены управляющие биты в TLB и наличие микро-TLB — промежуточного буфера, содержащего записи, по которым были последние обращения.
В результате тестирования было найдено несколько критических ошибок в подсистеме управления кэш-памятью, которые не были обнаружены с помощью тестовых программ, сгенерированных случайно.
