Введение
1 Функциональная верификация микропроцессоров 13
1.1 Тестирование микропроцессоров 14
1.1.1 Проверка правильности поведения 17
1.1.2 Генерация тестовой последовательности 20
1.1.3 Оценка полноты тестирования 23
1.2 Формальная верификация микропроцессоров 26
1.2.1 Проверка эквивалентности 26
1.2.2 Проверка моделей 27
1.2.3 Автоматизированное доказательство теорем 28
1.3 Тестирование и формальная верификация 29
1.4 Тестирование микропроцессоров с конвейерной архитектурой 31
1.4.1 Методы формальной спецификации 32
1.4.2 Методы модульного тестирования 34
1.4.3 Методы системного тестирования 37
1.5 Анализ текущего состояния 40
1.5.1 Методы формальной спецификации 40
1.5.2 Методы модульного тестирования 42
1.5.3 Методы системного тестирования 43
1.6 Уточнение задач диссертационной работы 44
1.7 Краткое введение в предлагаемый метод 45
2 Модульное тестирование микропроцессоров 47
2.1 Введение в метод модульного тестирования микропроцессоров 48
2.2 Формальная спецификация конвейера 50
2.2.1 Вспомогательные понятия 50
2.2.2 Модель конвейера без блокировок 56
2.2.3 Спецификация конвейера без блокировок 62
2.2.4 Отношение соответствия 6G
2.2.5 Модель конвейера с блокировками 72
2.2.6 Спецификация конвейера с блокировками 75
2.2.7 Спецификация конвейера с ресурсами 81
2.3 Тестирование на основе контрактных спецификаций конвейера 85
2.3.1 Проверка правильности поведения 85
2.3.2 Определение тестового покрытия 87
2.3.3 Генерация тестовой последовательности 93
2.4 Инструментальная поддержка модульного тестирования 102
2.4.1 Технология тестирования UniTESK 103
2.4.2 Тестирование Verilog-моделей 107
2.4.3 Тестирование SystemC-моделей 114
2.4.4 Библиотека PIPE 117
2.5 Результаты главы 127
3 Системное тестирование микропроцессоров 129
3.1 Введение в метод системного тестирования микропроцессоров 130
3.2 Основные понятия предлагаемого метода 131
3.2.1 Тестовый шаблон 132
3.2.2 Зависимости между инструкциями 133
3.2.3 Тестовые ситуации 136
3.2.4 Тестовые воздействия 138
3.3 Формальная спецификация микропроцессора 139
3.3.1 Формальная спецификация подсистем 139
3.3.2 Формальная спецификация типов данных 140
3.3.3 Формальная спецификация системы команд 141
3.4 Метод генерации тестовых программ 142
3.4.1 Схема генерации тестовых программ 143
3.4.2 Подготовка тестовых воздействий 144
3.4.3 Параметры управления генерацией 145
3.5 Инструментальная поддержка системного тестирования 146
3.5.1 Генератор тестовых программ MicroTESK 147
3.5.2 Примеры описаний тестов и тестовых программ 149
3.5.3 Отладка спецификаций и тестов 153
3.6 Результаты главы 154
4 Опыт практического применения предлагаемого метода 155
4.1 Тестирование буфера трансляции адресов 155
4.1.1 Краткое описание тестируемого модуля 155
4.1.2 Спецификация и тестирование модуля 157
4.1.3 Результаты апробации 158
4.1.4 Повторное использование спецификаций и тестов 158
4.2 Тестирование модуля кэш-памяти второго уровня 159
4.2.1 Краткое описание тестируемого модуля 159
4.2.2 Спецификация и тестирование модуля 160
4.2.3 Результаты апробации 161
4.3 Тестирование подсистемы управления памятью 162
4.3.1 Краткое описание тестируемой подсистемы 162
4.3.2 Спецификация и тестирования подсистемы 162
4.3.3 Результаты апробации 163
4.4 Тестирование микропроцессора Комдив64 164
4.4.1 Краткое описание тестируемого микропроцессора 164
4.4.2 Спецификация и тестирование микропроцессора 165
4.4.3 Результаты апробации 165
4.5 Тестирование арифметического сопроцессора Комдив128 167
4.5.1 Описание тестируемого сопроцессора 167
4.5.2 Спецификация и тестирование сопроцессора 168
4.5.3 Результаты апробации 168
4.6 Результаты главы 169
Заключение 171
Список литературы
