Введение
Глава 1. Генерация тестовых программ для микропроцессоров 15
1.1 Проектирование микропроцессоров 15
1.2 Функциональная верификация микропроцессоров 18
1.3 Техники генерации тестовых программ 22
1.4 Инструменты генерации тестовых программ
1.4.1 Инструменты НИИСИ РАН 26
1.4.2 Инструменты ARM 28
1.4.3 Инструменты IBM Research 30
1.4.4 Разработки ИСП РАН 34
1.4.5 Другие разработки 36
1.5 Выводы 40
Глава 2. Автоматизация конструирования генераторов тестовых программ 45
2.1 Метод автоматизации конструирования генераторов тестовых программ 46
2.1.1 Использование формальных спецификаций 46
2.1.2 Описание архитектуры микропроцессора на языке nML 47
2.1.3 Расширение возможностей языка nML 53
2.1.4 Архитектура модели микропроцессора 54
2.2 Язык описания шаблонов тестовых программ 56
2.2.1 Структура тестовых программ 56
2.2.2 Описываемые свойства тестовых программ 57
2.2.3 Концепция языка описания шаблонов тестовых программ 59
2.2.4 Описание последовательностей команд 62
2.2.5 Описание правил выбора регистров 64
2.2.6 Описание тестовых ситуаций 66
2.2.7 Описание инициализирующего кода и встроенных проверок 67
2.2.8 Описание правил рандомизации 72
2.2.9 Описание размещения команд и данных в памяти 74
2.2.10 Описание структуры переходов между тестовыми примерами 75
2.2.11 Расширяемость языка описания шаблонов тестовых программ 76
2.3 Архитектура генераторов тестовых программ 77
2.3.1 Анализатор шаблонов тестовых программ 78
2.3.2 Обработчик внутреннего представления 80
2.3.3 Итератор последовательностей команд 83
2.3.4 Обработчик последовательностей команд 90
2.3.5 Расширяемость генератора тестовых программ 94
2.4 Выводы 94
Глава 3. Реализация предложенного метода 95
3.1 Среда моделирования 96
3.1.1 Модель микропроцессора 96
3.1.2 Анализаторы формальных спецификаций 105
3.1.3 Генераторы кода и библиотеки моделирования 109
3.2 Среда тестирования 111
3.2.1 Анализатор шаблонов тестовых программ 112
3.2.2 Внутреннее представление шаблонов тестовых программ 113
3.2.3 Обработчик внутреннего представления 115
3.2.4 Итератор последовательностей команд 118
3.2.5 Распределитель регистров 120
3.2.6 Обработчик последовательностей команд 121
3.2.7 Исполнитель последовательностей команд 123
3.2.8 Генератор данных 124
3.2.9 Построитель встроенных проверок
3.3 Расширяемость инструмента MicroTESK 126
3.4 Выводы 127
Глава 4. Результаты практического применения 128
4.1 Генератор тестовых программ для архитектуры MIPS64 128
4.1.1 Архитектура MIPS64 128
4.1.2 Спецификации архитектуры MIPS64 129
4.1.3 Генерация тестовых программ для архитектуры MIPS64 131
4.2 Генератор тестовых программ для архитектуры ARMv8 132
4.2.1 Архитектура ARMv8 132
4.2.2 Спецификации архитектуры ARMv8 133
4.2.3 Генерация тестовых программ для архитектуры ARMv8 138
4.2.4 Проверка корректности генерируемых тестовых программ 139
4.3 Генератор тестовых программ для архитектуры PowerPC 140
4.3.1 Архитектура PowerPC 140
4.3.2 Спецификации архитектуры PowerPC 140
4.3.3 Генерация тестовых программ для архитектуры PowerPC 141
4.4 Генератор тестовых программ для архитектуры RISC-V 142
4.4.1 Архитектура RISC-V 142
4.4.2 Спецификации архитектуры RISC-V 142
4.4.3 Генерация тестовых программ для архитектуры RISC-V 145
4.5 Выводы 146
Заключение 148
Список литературы 149
