Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов.

Авторы

А.С. Камкин, М.В. Петроченков.

Аннотация

Описывается подход к разработке тестовых систем, предназначенных для верификации RTL-реализаций протоколов когерентности памяти. На основе анализа проблем, возникающих при верификации механизмов работы с памятью многоядерных микропроцессоров, предлагается архитектура тестовой системы, рассчитанной на эту специфику. Существенное внимание уделяется проблеме детерминированного воспроизведения тестов, построенных с помощью формальных методов. Рассматривается опыт применения предложенного подхода для микропроцессора «Эльбрус-2S».

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

консистентность памяти, протоколы когерентности, верификация, тестирование, проверка моделей, детерминированное воспроизведение.

Издание

Вопросы радиоэлектроники, серия ЭВТ, №3, 2014. С. 27-38.

Научная группа

Технологии программирования

Все публикации за 2014 год

Все публикации