Рассмотрена тестовая система на основе эталонной модели, используемая для верификации протокола когерентности микропроцессора «Эльбрус-2S». Описаны методы ее использования в гибридной системе вместе с RTL-моделью процессора и механизм генерации универсальных входных воздействий для разнородных составных частей.
Подсистема памяти микропроцессора, которая соединяет функциональные модули с физической памятью, является одной из самых сложных его составляющих, обладающей большой комбинаторикой состояний. Помимо основной функции доступа в память она отвечает за связь с другими процессорами и за когерентность системы, т.е. согласованность данных в случае многопроцессорных конфигураций. В связи с этим очень важна ее тщательная и всесторонняя верификация.
Одним из подходов, применяющихся в проектах ЗАО «МЦСТ», является системная верификация с использованием функциональной модели всего процессора в качестве эталона [1, 2]. Однако в рассматриваемом случае такая модель оказывается непригодной по ряду причин. С одной стороны, с точки зрения работы некоторых неиспользуемых подсистем – арифметико-логических устройств, прерываний и др. – она является слишком детальной. С другой стороны, в общей модели работа подсистемы памяти упрощена – не используются кэши, нет поддержки когерентности.
Объем вычислительных ресурсов, затрачиваемых на моделирование многопроцессорной системы, увеличивается пропорционально количеству входящих в нее процессоров. При этом моделирование процессора RTL-описанием значительно более затратно, чем использование его поведенческой модели. Для минимизации занятых ресурсов было решено верифицировать протокол поддержания когерентности памяти на «гибридном» кластере. В нем один из процессоров представляет собой RTL-описание процессора и является верифицируемым устройством, а поведение остальных трех моделируется созданной в рамках этого проекта системой E2S_MU, реализованной на языке C++. Взаимодействие между частями системы обеспечивает модуль связи.
Сложность подсистемы памяти процессора «Эльбрус-2S» исключает возможность ее формальной верификации [3]. Для функциональной верификации протокола, поддерживающего когерентность памяти, следует моделировать поведение многопроцессорной конфигурации. В случае процессора «Эльбрус-2S» такой конфигурацией является кластер – система, организованная по принципу Non-Uniform Memory Access (NUMA) [4], состоящая из четырех процессоров, соединенных между собой с помощью межпроцессорных линков по схеме «каждый с каждым» .
Кроме того, дополнительная экономия ресурсов достигается при повторном запуске тестов, когда можно исключить затратное по моделированию RTL-описание из тестовой системы, используя вместо этого снятую трассу воздействий и ответных реакций на них.
Подробнее... Загрузить файл 
Содержание:
Введение
1. Модель E2S_MU
2. Модуль связи
3. Генераторы воздействий
4. Результаты
Заключение
Литература