Функциональная верификация микропроцессоров. Анализаторы формальных спецификаций. Генераторы кода и библиотеки моделирования. Техники генерации тестовых программ. Спецификации архитектуры, язык описания шаблонов. Размещение команд и данных в памяти.
Аннотация к работе
В отличие от дефектов в программах, которые устраняются сравнительно просто, ошибки в микропроцессорах не могут быть исправлены и для их устранения потребуется повторный выпуск и замена микросхемы или целого блока. На системном уровне (т.е. на уровне устройства в целом) она осуществляется следующим образом: создаются тестовые программы на языке ассемблера; программы запускаются на проектной модели микропроцессора; в результате получаются трассы исполнения, содержащие информацию о событиях, которые произошли в процессе исполнения программ; полученные трассы проверяются на корректность. Общепринятым подходом является генерация на основе шаблонов тестовых программ, описывающих структурные и поведенческие свойства программ. Генераторы должны создавать тестовые программы на языке ассемблера по шаблонам, описывающим структурные и поведенческие свойства этих программ. Разработать метод автоматизации конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций.Тестирование микропроцессоров на системном уровне осуществляется путем генерации тестовых программ на языке ассемблера, которые представляют собой последовательности команд (инструкций) микропроцессора, и анализа результатов их выполнения с целью убедиться, что их поведение соответствует спецификации. Обычно тестирование начинается с HDL-модели и продолжается до выпуска продукции. В моделях первого типа тестовые ситуации связаны непосредственно с кодом HDL-модели или с производными от нее структурами. Т.е. метрики покрытия на основе реализации позволяют оценить, в какой мере код HDL-модели был задействован при выполнении набора тестов. Инструменты, при помощи которых осуществляется генерация, известны как генераторы тестовых программ (TPG, test program generators) или генераторы потока команд (ISG, instruction stream generators).Для всех рассмотренных в этой главе инструментов, независимо от поддерживаемых ими техник, можно выделить два свойства: (1) реконфигурируемость и (2) расширяемость. Другим важным свойством является контролируемость генерации, возможность отслеживать текущее состояние микропроцессора в процессе генерации путем исполнения генерируемых последовательностей команд на эталонной модели, в качестве которой выступает программный эмулятор. Это позволяет гарантировать корректность построенных программ, создавать тесты со встроенными проверками и применять техники генерации, использующие информацию о текущем состоянии микропроцессора. Однако, по сути, они являются частью конфигурации инструмента т.к. используют знание о синтаксисе и семантике команд для их интерпретации. Это объясняется тем, что коммерческие компании занимаются верификацией выпускаемых ими микропроцессоров и создают инструменты для решения текущих задач верификации, а исследовательские институты изобретают новые техники верификации и создают инструменты для их апробации.В данной главе был предложен метод конструирования генераторов тестовых программ для микропроцессоров на основе формальных спецификаций их архитектуры.Модель микропроцессора включает в себя три основных части: (1) метаданные, хранящие информацию о командах, регистрах и памяти микропроцессора; (2) эмулятор, позволяющий программно эмулировать исполнение команд и получать информацию о состоянии микропроцессора; (3) модель тестового покрытия, содержащая информацию о возможных путях исполнения команд. Спецификации на языке NML описывают команды в виде иерархической структуры операций. Например, в спецификации системы команд MIPS, структура которой показана на рисунке 16, команды ADD описывается путем из операции instruction к операции add (другими словами операция instruction параметризована операцией add), которая входит в группы Op и ALU. Параметры описываются следующими атрибутами: (1) имя; (2) тип сущности (операция, режим адресации или непосредственный аргумент); (3) имя сущности (для операций и режимов адресации); (4) тип данных (для режимов адресации и непосредственных аргументов) и (5) тип доступа (чтение, запись). Т.к. спецификации на языке NML не позволяют описать механизмы управления памятью (включая трансляцию адресов), построенный на их основе эмулятор использует упрощенную схему работы с памятью.Инструмент MICROTESK использует предложенный метод для конструирования генераторов тестовых программ с предложенной архитектурой, осуществляющих генерацию на основе шаблонов на предложенном языке.Архитектура MIPS64 описывается в руководстве «MIPSTM Architecture For Programmers», включающем три тома [47, 103, 104], общий объем которых составляет примерно 1000 страниц. Кроме того для модуля арифметики с плавающей точкой определены 32 регистра общего назначения (Floating Point General Purpose Registers, FPRS) размером 64-бит и 32 контрольных регистра (Floating Point Control Registers, FCRS) размером 32-бита для хранения флагов, выставляемых операциями с плавающей точкой.