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


Подходы к автономной верификации кэш-памятей многоядерных микропроцессоров

М.В. Петроченков (АО «МЦСТ», Москва, Россия)
И.А. Стотланд (АО «МЦСТ», Москва, Россия)
Р.Е. Муштаков (АО «МЦСТ», Москва, Россия)

Аннотация

В статье приведен обзор методов, применяемых при проверке корректности поведения кэш-памятей многоядерных микропроцессоров. Описаны общие свойства устройств подсистемы памяти микропроцессора, а также свойства, специфичные для кэш-памятей, и метод поддержки согласованности состояния памяти в системе на основании протокола когерентности. Представлены подходы к проектированию тестовой системы, генерации корректных тестовых воздействий и проверке правильности поведения тестируемого устройства. Предложены модификации общего подхода к генерации тестовых воздействий для устройств с внеочередным исполнением инструкций. Приведены способы разработки тестовых систем на различных уровнях абстракции. В статье описан основной способ проверки поведения устройства на уровне транзакций — разработка эталонной поведенческой модели для последующего сравнения реакций устройства с эталонными; расхождения в реакциях сигнализируют об ошибке. Выделены критерии применимости данного подхода. Описаны методы верификации устройств, поведение которых функционально не детерминировано на уровне транзакций: метод «серого ящика», базирующийся на анализе внутренних интерфейсов устройства, для устранения возникающей неопределенности в поведении устройства. Кроме того, приведен новый метод, основанный на динамическом уточнении поведенческой модели на основе реакции устройства. Также рассмотрены преимущества использования утверждений утверждения в генераторе тестовых воздействий в качестве дополнительных методов обнаружения ошибок. В работе приведен метод, позволяющий упростить проверку поведения устройств с внеочередным исполнением инструкций, основанный формировании эталонной очереди их выполнения. В заключение представлены результаты применения предложенных подходов к верификации кэш-памятей многоядерных микропроцессоров архитектуры «Эльбрус» и «SPARC-V9».

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

многоядерный микропроцессор, кэш-память, внеочередное исполнение, тестовая система, недетерминированное поведение, верификация на основе эталонных моделей, автономная верификация, «SPARC-V9», микропроцессор «Эльбрус»

Издание

Труды Института системного программирования РАН, том 28, вып. 3, 2016, стр. 161-172.

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

DOI: 10.15514/ISPRAS-2016-28(3)-10

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