eng
Содержание
СОДЕРЖАНИЕ
Вступление . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
Предисловие . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
Благодарности . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
Об авторах . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
Список сокращений . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
Глава 1. Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.1.
Растущая сложностьва лидации СнК. . . . . . . . . . . . . . . . . . 19.
1.2
Валидация на системном уровне:возможности и проблемы . . . . . 22
1.2.1.
Нисходящий маршрут проектирования и валидации . . . . . . . . . . 23
1.2.2.
Методы валидации СнК . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
1.2.3.
Возможности валидации на системном уровне . . . . . . . . . . . . . . . 31
1.2.4.
Проблемы валидации на системном уровне . . . . . . . . . . . . . . . . . 33
1.3.
Комплексный подход к валидации на системном уровне . . . . . . . . . . . . 35
1.4.
Структура книги. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
Глава 2. Моделирование и спецификации дизайнов СнК . . . . . . . . . . . . . . . . 40
2.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
2.2.
Моделирования сложных систем. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.2.1.
Графовое моделирование . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.2.2.
Моделирование поведения на основе FSM . . . . . . . . . . . . . . . . . 42
2.3.
Спецификация, использующая SystemC TLM . . . . . . . . . . . . . . . . . . . . 43
2.3.1.
Моделирование дизайнов на языке SystemC TLM . . . . . . . . . . . . 44
2.3.2.
Переход от SystemC TLM к механизму управления памятью . . . . 46
2.3.3.
Анализ примера: маршрутизатор . . . . . . . . . . . . . . . . . . . . . . . . . 50
2.4.
Спецификация, использующая диаграммы деятельности UML . . . . . . . 51
2.4.1.
Графические обозначения . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
2.4.2.
Формальное моделирование диаграмм деятельности на UML. . . . 56
2.4.3.
Преобразование диаграммы деятельности UML в SMV . . . . . . . . 59
2.4.4.
Пример: фондовая биржа . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
2.5.
Краткое содержание главы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
Глава 3. Автоматическая генерация направленных тестов. . . . . . . . . . . . . . . . 66
3.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.2.
Обзор сходных работ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
3.3.
Процесс генерации тестов на основе проверки на моделях. . . . . . . . . . . 69
3.4.
Управляемая покрытием генерация свойств . . . . . . . . . . . . . . . . . . . . . 70
3.4.1.
Свойство безопасности и его отрицание . . . . . . . . . . . . . . . . . . . 71
3.4.2.
Адекватностьт естов при проверке на моделях . . . . . . . . . . 7.2 . . . .
3.4.3.
Модели неисправностей . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
3.4.4.
Функциональное покрытие на основе моделей неисправностей . . 76
3.5.
Генерация тестов с использованием методов проверки на модели . . . . . 76
3.5.1.
Генерация тестов с использованием проверки
на неограниченных моделях . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.5.2.
Генерация тестов с использованием проверки
на ограниченной модели . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
3.6.
Практические примеры . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
3.6.1.
Система управления . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
3.6.2.
Система фондовой биржи . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
3.7.
Краткие выводы. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
Глава 4. Уплотнение функциональных тестов . . . . . . . . . . . . . . . . . . . . . . . . 86
4.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
4.2.
Методы сокращения производственных тестов . . . . . . . . . . . . . . . . . . . 87
4.2.1.
Сжатие тестов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
4.2.2.
Уплотнение тестов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
4.2.3.
Сфера применения и ограничения. . . . . . . . . . . . . . . . . . . . . . . . 91
4.3.
Уплотнение функциональных тестов. . . . . . . . . . . . . . . . . . . . . . . . . . . 93
4.3.1.
Модели FSM двоичного формата. . . . . . . . . . . . . . . . . . . . . . . . . 95
4.3.2.
Число состояний и переходов FSM . . . . . . . . . . . . . . . . . . . . . . . 97
4.3.3.
Уплотнение свойств состояний и переходов FSM. . . . . . . . . . . . . 98
4.3.4.
Выбор и генерация тестов, ориентированных
на покрытие состояний FSM. . . . . . . . . . . . . . . . . . . . . . . . . . . 101
4.3.5.
Практический пример . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
4.4.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
Глава 5. Кластеризация свойств и методы обучения . . . . . . . . . . . . . . . . . . . 107
5.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.2.
Обзор сходных работ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
5.3.
Справочная информация: применение решателя булевых формул . . . . 109
5.3.1.
Алгоритм DPLL. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.3.2.
Сообщение о конфликте . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5.4.
Кластеризация свойств . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
5.4.1.
Подобие на основе пересечения структурных характеристик
свойств . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
5.4.2.
Подобие на основе текстового пересечения . . . . . . . . . . . . . . . . 115
5.4.3.
Подобие на основе влияния. . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.4.4.
Подобие на основе пересечения CNF. . . . . . . . . . . . . . . . . . . . . 118
5.4.5.
Определение базового свойства . . . . . . . . . . . . . . . . . . . . . . . . . 118
5.5.
Генерация тестов на основании сообщений о конфликте . . . . . . . . . . . 119
5.5.1.
Методы переадресации сообщений о конфликтах . . . . . . . . . . . . 119
5.5.2.
Замена имен переменных для вычисления пересечений . . . . . . . 121
5.5.3.
Идентификация и повторное использование общих сообщений
о конфликте . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122
5.6.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
5.6.1.
Процессор MIPS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
5.6.2.
Система фондовой биржи . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134
5.7.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138
Глава 6. Порядок принятия решений на основе методов обучения . . . . . . . . . 139
6.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139
6.2.
Обзор сходных работ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140
6.3.
Порядок принятия решений на основе обучения . . . . . . . . . . . . . . . . . 141
6.3.1.
Мотивация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141
6.3.2.
Упорядочивание значений бит . . . . . . . . . . . . . . . . . . . . . . . . . . 143
6.3.3.
Упорядочивание переменных . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
6.3.4.
Гибридное обучение на основе знаний сообщений
о конфликтах и порядке принятия решений . . . . . . . . . . . . . . . 145
6.4.
Генерация тестов с использованием методов упорядочивания
принятия решений . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146
6.4.1.
Генерация тестов для одного свойства . . . . . . . . . . . . . . . . . . . . 147
6.4.2.
Генерация тестов для подобных свойств. . . . . . . . . . . . . . . . . . . 150
6.5.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
6.5.1.
Внутрисвойственное обучение . . . . . . . . . . . . . . . . . . . . . . . . . . 153
6.5.2.
Обучение на основе обмена информацией между
разными свойствами . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157
6.6.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
Глава 7. Синхронизированная генерация направленных тестов . . . . . . . . . . . 162
7.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
7.2.
Обзор работ на сходные темы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
7.3.
Синхронизированная генерация тестов . . . . . . . . . . . . . . . . . . . . . . . . 164
7.3.1.
Корректностьси нхронизированной генерации тестов . . . . . . 1.6 9. .
7.3.2.
Подробности реализации синхронизированной
генерации тестов . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170
7.4.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
7.4.1.
Система фондовой биржи . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171
7.4.2.
Процессор MIPS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175
7.5.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 177
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178
Глава 8. Создание тестов с помощью декомпозиции дизайна и свойств . . . . . 179
8.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179
8.2.
Обзор работ на сходные темы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
8.3.
Декомпозиция дизайна и свойств . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183
8.3.1.
Декомпозиция дизайна . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184
8.3.2.
Декомпозиция свойств. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
8.4.
Генерация тестов после декомпозиции . . . . . . . . . . . . . . . . . . . . . . . . 190
8.4.1.
Генерация тестов с использованием разделения
на уровне модулей. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193
8.4.2.
Генерация тестов с помощью разделения на уровне путей . . . . . 195
8.5.
Слияние частных контрпримеров . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196
8.6.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198
8.6.1.
Декомпозиция на уровне модулей . . . . . . . . . . . . . . . . . . . . . . . 198
8.6.2.
Декомпозиция на уровне группы на основе временного шага . . . 200
8.6.3.
Обсуждение: применимостьи ограничения . . . . . . . . . . .2 0.2 . . . .
8.7.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 203
8
Содержание
Глава 9. Методы ориентированной на обучение декомпозиции свойств . . . . . 206
9.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206
9.2.
Обзор работ на сходные темы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207
9.3.
Ориентированная на обучение декомпозиция свойств . . . . . . . . . . . . . 209
9.3.1.
Пространственная декомпозиция свойств. . . . . . . . . . . . . . . . . . 209
9.3.2.
Временная декомпозиция свойств . . . . . . . . . . . . . . . . . . . . . . . 212
9.4.
Порядок принятия решений на основе методов обучения . . . . . . . . . . 214
9.5.
Генерация тестов с использованием методов декомпозиции и обучения 216
9.6.
Наглядный пример . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217
9.6.1.
Пространственная декомпозиция . . . . . . . . . . . . . . . . . . . . . . . . 217
9.6.2.
Временная декомпозиция . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218
9.7.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
9.7.1.
Процессор MIPS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
9.7.2.
Система фондовой биржи . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221
9.8.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 222
Глава 10. Генерация направленных тестов для многоядерной архитектуры . . . 224
10.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 224
10.2.
Обзор сходных работ. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225
10.3.
Генерация тестов для многоядерных архитектур . . . . . . . . . . . . . . . . . 226
10.3.1.
Корректностьгенерации направленных тестов
для многоядерных архитектур . . . . . . . . . . . . . . . . . . . . . . . . . 231
10.3.2.
Подробности внедрения метода . . . . . . . . . . . . . . . . . . . . . . . 232
10.3.3.
Гетерогенные многоядерные архитектуры . . . . . . . . . . . . . . . . 234
10.4.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 235
10.4.1.
Подробности эксперимента. . . . . . . . . . . . . . . . . . . . . . . . . . . 235
10.4.2.
Результаты эксперимента . . . . . . . . . . . . . . . . . . . . . . . . . . . . 236
10.5.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240
Глава 11. Генерация тестов для валидации согласованности кэшей . . . . . . . . 242
11.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 242
11.2.
Обзор сходных работ. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243
11.3.
Предпосылки и мотивация . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 244
11.4.
Генерация тестов для покрытия переходов . . . . . . . . . . . . . . . . . . . . . 245
11.4.1.
Протокол SI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246
11.4.2.
Протокол MSI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248
Содержание 9
11.4.3.
Протокол MESI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 251
11.4.4.
Протокол MOSI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252
11.5.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253
11.6.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 256
Глава 12. Повторное использование результатов валидации
на системном уровне . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
12.1.
Введение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
12.2.
Обзор работ на сходные темы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 258
12.3.
Генерация тестов при реализации на RTL из спецификации на TLM 259
12.3.1.
Автоматическая генерация тестов на TLM. . . . . . . . . . . . . . . . 260
12.3.2.
Перевод тестов TLM в тесты RTL. . . . . . . . . . . . . . . . . . . . . . 262
12.3.3.
Прототип инструмента для уточнения валидации
TLM-на-RTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 265
12.4.
Практические примеры. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
12.4.1.
Пример маршрутизатора . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 267
12.4.2.
Пример конвейерного процессора. . . . . . . . . . . . . . . . . . . . . . 272
12.5.
Краткие выводы . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 277
Литература . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 277
Глава 13. Заключение . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 280
13.1.
Основные выводы. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 280
13.2.
Будущие направления развития функциональной валидации . . . . . . . 283
Приложение А . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 286
ВСТУПЛЕНИЕ
Задача функциональной верификации в той или иной мере встает перед каж-
дым инженером, занимающимся проектированием электронных систем. Дока-
зательство того, что система функционирует так, как того требует специфика-
ция, с ростом сложности системы требует все больших ресурсов. Причем рост
сложности далеко не линеен.
Современные тенденции в микроэлектронике определяют переход к про-
цессорно-ориентированным системам и совместной разработке аппаратной
части и программного обеспечения. Разработка программного обеспечения до
готовности аппаратной части требует наличия виртуальных прототипов, обес-
печивающих переход на системный уровеньпроектирования.
Требования к росту производительности систем подталкивают к использо-
ванию нескольких процессоров и более сложных шинных архитектур. Появле-
ние аппаратных ускорителей перекладывает верификацию функционала с про-
граммистов на разработчиков аппаратуры.
Некачественная или неполная верификация может привести к некоррект-
ной работе программы уже после начала ее использования потребителем.
В этом случае пострадает в первую очередьрепутация разработчика.
Одновременно с указанными проблемами время выхода на рынок в усло-
виях конкуренции постоянно сокращается, что накладывает дополнительные
ограничения на процесс верификации. Чтобы справиться с возникающими
сложностями, требуются разработка и внедрение новых методов верификации,
более производительных, абстрактных и автоматизированных. Повышенная
производительность может достигаться за счет совершенствования вычисли-
тельных систем, использования более мощных серверов, оптимизации алго-
ритмов, появления новых методик верификации и комбинирования сущест-
вующих. Абстрактностьдостигается за счет использования языка C и его
библиотек (таких как SystemC) с последующей автоматизированной конверта-
цией в языки описания аппаратуры SystemVerilog и VHDL. Автоматизацию
следует проводитьв области генерации тестов.
Попытка описатьметоды решения указанных проблем находит отражение
в книге, которую Вы держите в руках. Она является переводом англоязычной
публикации и ориентирована на русскоговорящих инженеров, занимающихся
верификацией систем-на-кристалле, и может бытьполезна для понимания
сложностей, возникающих в процессе верификации сложных электронных си-
стем, и методов их решения. Надеемся, что каждый найдет для себя в этой
книге что-нибудьполезное.
Генеральный директор ЗАО «СКАН»
Ланцев А.Н.
ПРЕДИСЛОВИЕ
Посвящается нашим семьям
В повседневной жизни мы окружены компьютерами. Мы осознаем сложность
компьютерных систем, поскольку пользуемся настольными компьютерами,
ноутбуками или серверами. Во многих жизненных ситуациях мы взаимодейст-
вуем с системами, которые имеют встроенные компьютеры, например, сото-
вые телефоны, гаджеты и системы мониторинга. В конструкции самолета или
автомобиля много вычислительных устройств, совместная работа которых га-
рантирует, что наше путешествие будет приятным и безопасным. Можем ли
мы с уверенностью сказать, что эти встроенные вычислительные системы
сконструированы и изготовлены правильно и качественно, чтобы смело пола-
гаться на их функции? Простой ответ заключается в том, что никто не может
доказатьих абсолютную непогрешимость. Однако, поскольку у нас нет выбо-
ра, нам остается только расслабиться и наслаждаться жизнью!
Рассмотрим простой сумматор, чтобы понятьтрудности верификации со-
временных компьютерных систем. Сумматор является одним из простейших
вычислительных устройств в калькуляторе. Он складывает два входных значе-
ния и выдает результат. Как правило, входными значениями являются 32-раз-
рядные целые числа. Поэтому, чтобы проверитьтакой сумматор, мы должны
смоделироватьнесколь ко триллионов (232 Ї 232) тестовых векторов. Очевидно,
что слишком дорого применятьтриллионы входных векторов для проверки
сумматора. Фактически, невозможно имитироватьсумматор с использованием
всех возможных входных последовательностей, когда входными значениями
выступают 64-битные целые числа. Если мы не способны полностью верифи-
цироватьпростой сумматор, то как можно надеяться, что мы сможем прове-
ритьсовременные встроенные и гибридные системы, которые состоят из
сложного программного обеспечения и аппаратных средств, включая мульти-
и многоядерные процессоры, память, шины, контроллеры, интерфейсы и т.д.?
Функциональная валидация широко признана как основное узкое место в ме-
тодологии проектирования систем-на-кристалле (SoC—System-on-Chip), по-
этому на нее затрачивается до 70% от общего времени разработки и ресурсов.
Несмотря на стользначитель ные усилия, многие конструкции СнК отказыва-
ют уже при первых тестах (отказ кремниевого кристалла) в связи с функцио-
нальными ошибками. Сложность функциональной валидации, как ожидается,
вырастет еще больше в связи с совокупным влиянием возрастающей сложно-
сти проектирования и сокращением сроков выхода на рынок.
Существующие подходы к валидации используют комбинацию методов
моделирования и формальной верификации. Моделирование является наибо-
лее широко используемой формой валидации с применением генерации слу-
чайных и ограничено-случайных тестов. Например, в случае с сумматором
вместо того, чтобы проверятьвсе возможные комбинации входных данных,
инженеры-валидаторы могут генерироватьтесты для нужных им функцио-
нальных сценариев на основе критериев тестового покрытия и случаев преде-
льного превышения интересующих их параметров. Так как нецелесообразно
создаватьи применятьвсе возможные тесты, валидация на основе моделиро-
вания не гарантирует качество дизайна. С другой стороны, формальные мето-
ды валидации (такие как верификация моделей) не используют входных век-
торов, но исследуют пространство состояний для обеспечения правильности
функционирования. К сожалению, это исследование может привести к расши-
рению пространства состояний в случае валидации больших и сложных проек-
тов. В современных методиках валидации используется эффективное соче-
тание обоих подходов. Для примера, полный дизайн СнК моделируется с
помощью миллиардов тестов, в то время как очень важные компоненты, такие
как контроллеры или конкретные протоколы, полностью верифицируются
формальными методами.
Существуют различные перспективные направления, позволяющие зна-
чительно сократитьобщую трудоемкостьвалидации за счет совместного ис-
пользования моделирования и формальной верификации. Они полезны для
верификации, насколько ее возможно проводить на уровне спецификации
(которая представляет собой оценку порядка величины и потому проще, чем
верификация на уровне реализации, но позволяет исследоватьвсе функцио-
нальные детали) и автоматического повторного использования валидации
высокого уровня для верификации реализации систем низкого уровня. Ана-
логично, они используют направленные тесты для валидации дизайна, так
как подобные тесты позволяют достичьтого же целевого тестового покрытия
с помощью оценки по порядку величины при меньшем количестве тестов по
сравнению с использованием случайных или ограничено-случайных тестов.
В результате моделирование с использованием эффективных направленных
тестов может существенно снизитьобщую трудоемкостьвалидации. Однако
генерация направленных тестов в основном выполняется при вмешательстве
человека. Написанные от руки тесты влекут за собой трудоемкую и отни-
мающую много времени работу инженеров-валидаторов, которые имеют
глубокие знания о конструкциях, проходящих верификацию. Для сложных
конструкций невозможно вручную создатьвсе направленные тесты для до-
стижения всеобъемлющего тестового покрытия. Таким образом, необходимо
разработатьинструменты и методы для автоматической генерации направ-
ленных тестов.
Эта книга описывает инновационные пути объединения моделирования и
формальных методов валидации сложных систем. В ней представлен всесто-
ронний обзор моделирования и методов валидации на системном уровне, на-
правленных на снижение общей трудоемкости валидации и улучшение качест-
ва продукции. Она описывает проблемы, связанные с проверкой сложных
систем и представляет эффективные методы решения этих проблем. В книге
рассматриваются различные методы моделирования на системном уровне,
использующие языки проектирования SystemC, UML (Unified Modeling Language
— унифицированный язык моделирования) и моделирование на уровне
транзакций. Она представляет состояние современных методов для автомати-
ческой генерации направленных тестов с упором на сокращение времени на
генерацию тестов и трудоемкости валидации посредством применения мето-
дов кластеризации, декомпозиции и обучения. Она также описывает новые
пути повторного использования валидации высокого уровня на различных
уровнях абстракции.
Читательэтой книги получит полное понимание задач верификации про-
ектируемых систем и узнает, как валидация на системном уровне может зна-
чительно улучшитькачество проектирования и снизитьобщую стоимостьиз-
делий. В главе 1 представлены преимущества валидации на системном уровне.
Глава 2 описывает, как задатьсложные системы, использующие высокоуров-
невые модели. Глава 3 содержит основные схемы автоматической генерации
направленных тестов. В следующей главе рассказывается, как значительно
уменьшить число тестов без ущерба для целевого тестового покрытия. В главах
5—9 описаны эффективные методы генерации направленных тестов. В следу-
ющих двух главах представлены методы генерации тестов с упором на валида-
цию многоядерных архитектур. Глава 12 описывает инновационные способы
повторного использования сгенерированных тестов и утверждений высокого
уровня для валидации систем на уровне реализации. Наконец, глава 13 завер-
шает книгу кратким обсуждением перспективных направлений исследований.
Мы надеемся, что вам понравится наша книга, в которой вы найдете полез-
ную информацию.
Целевая аудитория
Эта книга предназначена для студентов старших курсов, аспирантов, исследо-
вателей, разработчиков инструментов САПР, проектировщиков и менеджеров,
заинтересованных в развитии эффективных инструментов и методов проекти-
рования и валидации на системном уровне, генерации направленных тестов и
функциональной валидации гетерогенных конструкций СнК.
БЛАГОДАРНОСТИ
Эта книга является результатом десятилетних научных исследований и про-
мышленного сотрудничества многих коллективов. Книга включает в себя опи-
сание методов и представлений о валидации на системном уровне, которые ста-
ли результатом диссертаций профессора Минсон Чэня, доктора Хун-Mo Kу и
доктора Ксяоке Циня. Мы хотели бы поблагодаритьнаших спонсоров за ока-
занную финансовую поддержку в этом исследовании. Эта работа была частично
профинансирована Национальным научным фондом (National Science Foundation
(CAREER Award 0746261, CCF-0903430. and CNS 0905308), Semiconductor
Research Corporation (2009-HJ-1979), Intel Corporation, Фондом докторантуры
Министерства образования Китая 20110076120025 и средствами Государствен-
ного плана Китая по высокотехнологичным разработкам 2011AA010101.
Эта книга несет печатьсотрудничества с многочисленными коллективами.
Мы хотели бы отметитьвклад доктора Магди Абадира (Freescale), доктора
Джаянта Бхадра (Freescale), профессора Никила Датта (UC Irvine), профессора
Масахиро Фуджита (Токийский университет), доктора Хуан Чжо, доктора
Друбайоти Калита (Intel), профессора Тулика Митра (NUS Сингапур) и про-
фессора Абхика Ройчудхури (NUS Сингапур). Мы также благодарны всем чле-
нам CISE Embedded Systems Lab Университета Флориды. В список входят док-
тор Канад Басу, Хади Хаджимири, Камран Рахмани, Камик Шривастава,
Четан Мурти, Сеок-Фан Сеон и доктор Вейксун Ван.
ОБ АВТОРАХ
Минсон Чэньявляется адъюнкт-профессором в Software Engineering Institute
при Восточно-Китайском педагогическом университете. Его исследования на-
правлены на автоматизацию проектирования встроенных систем, разработку
кибер-физических систем, методов моделирования и проверки программного
обеспечения. Он получил степени бакалавра и магистра в Нанкинском уни-
верситете в 2003 и 2006 годах, соответственно, и доктора наук — в Универси-
тете штата Флорида в 2010 году, все в области компьютерных наук. Он опуб-
ликовал множество научных статей в ведущих международных журналах и
материалах международных конференций. Одна из его работ была номиниро-
вана на Best Paper Award Международной конференции по VLSI Design 2009.
В настоящее время его исследования финансируются Национальным научным
фондом Китая, Министерством образования и включены в Государственный
план по высокотехнологичным разработкам. Доктор Чэньработал в качестве
члена оргкомитетов по разработке программ ряда конференций ACM и IEEE,
включая SAC и ICFEM. Он является членом обеих ACM и IEEE.
Ксяоке Циньполучил степени бакалавра и магистра на факультете автома-
тизации Университета Цинхуа в Пекине в 2004 и 2007 годах, соответственно.
Докторскую диссертацию он защищал на факультете компьютерных и инфор-
мационных наук и инженерии Университета штата Флориды в 2012 году. Его
исследовательские интересы лежат в области сжатия кода, верификации моде-
лирования, валидации на системном уровне многоядерных архитектур и пла-
нировании производства встроенных систем в реальном времени. Он опубли-
ковал множество статей в ведущих мировых журналах и материалах
международных конференций. Его работа по валидации согласованности кэша
была номинирована на Best Paper Award в области автоматизации проектиро-
вания и испытаний в Европе (DATE), 2012. Доктор Циньвыступал в качестве
рецензента и обозревателя нескольких конференций и журналов ACM и IEEE.
Хеон-Mo Kу является специалистом по медиаархитектуре в группе парал-
лельной обработки визуальных данных корпорации Intel. Его исследователь-
ские интересы лежат в области проектирования и верификации встраиваемых
систем для медиа-технологий, включая видеокодеки, обработку видео и
машинное распознавание образов. Он получил степени бакалавра и магистра
на факультете электроники и электротехники Национального университета
Kyungpook в Корее в 1993 и 1995 годах, соответственно. До начала работы над
докторской диссертацией он работал в компании LG Electronics Research Center
в течение 8 лет. Он получил докторскую степеньпо вычислительной техни-
ке в Университете Флориды в 2007 году.
Прабхат Мишра является адъюнкт-профессором на кафедре компьютер-
ных и информационных наук в Университете штата Флорида. Его исследова-
тельские интересы включают автоматизацию проектирования встроенных сис-
тем, вычисление энергопотребления, верификацию аппаратных средств и
программного обеспечения и проектирование безопасных систем. Он получил
степеньбакалавра в Университете Джанавпур в Калькутте в 1994 году, степень
магистра по технологии в Индийском технологическом институте в Кхарагпу-
ре в 1996 году и доктора наук в Университете штата Калифорния, Ирвин, в
2004 году, все в области компьютерных наук. До прихода в Университет штата
Флорида он несколько лет работал в различных компаниях, специализирую-
щихся в разработке полупроводниковых приборов и автоматизации проекти-
рования, включая Intel, Motorola, Synopsys и Texas Instruments. Он опублико-
вал четыре книги, был соавтором десяти книг и написал более 100 научных
статей в ведущих мировых журналах и материалах различных конференций.
Его исследования получили несколько наград, включая премию NSF CAREER
от Национального научного фонда, две премии за лучшую статью (VLSI Design
2011 и CODES+ISSS 2003), он имеет несколько номинаций на лучшую
статью и премию EDAA 2004 года за выдающуюся диссертационную работу от
Европейской ассоциации автоматизации проектирования (European Design
Automation Association). В 2007 году он получил премию как Международный
педагог года от инженерного колледжа Университета штата Флорида за значи-
тельный вклад в международные научные исследования и преподавание
компьютерных наук. В настоящее время он работает в качестве помощника
редактора в журналах ACM Transactions on Design Automation of Electronic Systems
(TODAES), IEEE Design & Test of Computers (D&T) и Joumal of Electronic
Testing (JETTA), внештатным редактором в журнале IEEE Transactions on
Computers, а также выступал членом оргкомитета ряда конференций ACM и
IEEE, в том числе ICCAD, DATE, ASPDAC, CODES+ISSS и VLSI Design. Он
занимал должностьгенераль ного председателя на конференции IEEE High-Level
Design Validation and Test (HLDVT) 2010, был руководителем группы по
разработке программы конференции HLDVT 2009 года, информационным
директором ACM TODAES и работал внештатным редактором в издательст-
вах IEEE D&T, Springer JETTA и IJPP. Он является старшим членом в ACM
и IEEE.
СПИСОК СОКРАЩЕНИЙ
ABV — Валидация на основе утверждений
ADL — Язык описания архитектуры
ATE — Автоматическое тестовое оборудование
АТМ — Банкомат (автоматизированный кассовый терминал)
ATPG — Автоматический генератор тестовых векторов
BCP — Булево распространение ограничений
BDD — Двоичные диаграммы решений
BIST — Встроенное самотестирование
BMC — Проверка ограниченной модели
CNF — Конъюнктивная нормальная форма
CSP — Проблема (задача) удовлетворения ограничений
DAG — Направленный ациклический граф
DSE — Исследование пространства проектных параметров
DUV — Валидируемый дизайн
ESL — Уровеньэлектронных систем
FSM — Конечный автомат (автомат с конечным числом состояний)
IC — Интегральная схема
LTL — Линейная временная логика
MоC — Модельв ычислений
MPSoC — Мультипроцессорная система на кристалле
PSL — Язык описания свойств
RTL — Уровеньрегистровых передач
SAT — Выполнимость
SoC — Система на кристалле
SVA — Утверждение SystemVerilog
TLM — Моделирование на уровне транзакций
TRS — Спецификация уточняющих тестов
UMC — Проверка неограниченной модели
UML — Унифицированный язык моделирования
VSIDS — Уменьшение суммы, независимое от состояния переменной
XMI — Обмен метаданными с помощью XML
ГЛАВА 1
Введение
1.1. 1.1. Растущая сложность валидации СнК
Система на кристалле (SoC) включает в себя все необходимые аппаратные ком-
поненты (например, микропроцессоры, блоки памяти и периферийные устрой-
ства) и программные модули (операционные системы, работающие в реальном
времени, и программы контроля), объединяя их в единую интегральную схему с
требуемой функциональностью. Она может выполнять различные вычисления,
в том числе цифровые, аналоговые, а также смешанные цифро-аналоговые.
Рис. 1.1 представляет блок-схему архитектуры типичной многопроцессорной
СнК (MPSoC — Multiprocessor System-on-Chip) [1]. Например, дизайн СнК со-
стоит из четырех RISC-процессоров и различных общих устройств ввода-выво-
да, которые соединены высокопроизводительной шиной (AНB — Advanced
High-Performance Bus) и периферийной шиной (APB — Advanced Peripheral
Bus). СнК широко используются во встраиваемых системах, применяемых в та-
ких областях, как автомобильная электроника, авионика, телекоммуникации,
создание интеллектуальных зданий, портативных устройств и т.д.
В связи с увеличением сложности программных и аппаратных компонентов
сложностьпроектирования современных СнК растет с угрожающей скоростью.
Для размещения новых приложений и удовлетворения вычислительных требо-
ваний современные СнК используют множество сложных архитектурных осо-
бенностей для поддержки синхронизации, обмена данными, динамического ре-
гулирования частоты и напряжения, когерентности кэшей, конвейеризации
Рис. 1.1. Пример дизайна MPSoC: арбитр — устройство разрешения конфликтов
Арбитр
Кон-
троллер
памяти
АНВ/
АРВ-
мост
АНВ-шина
АРВ-шина
межсоединений и т.д. Увеличение сложности дизайна вызывает рост сложности
верификации. Быстрое развитие технологий совместно с жесткой конкуренцией
на рынке поставило разработку СнК перед проблемой: как быстро гарантиро-
вать функциональную правильность СнК? Функциональная верификация СнК
широко признана в качестве основного узкого места. Недопустимо моделиро-
ватьдаже простой двухвходовой сумматор с использованием всех возможных
входных последовательностей, так как это потребует 264 264 входных (тестовых)
векторов, когда каждый вход составляет 64 бита. Верификация комплексных
СнК аналогична верификации миллионов и миллиардов комплексных суммато-
ров, взаимодействующих друг с другом в виде программного обеспечения и/или
аппаратных средств. Серьезными проблемами являются обнаружение всех
функциональных ошибок, а также электротехнических дефектов из-за комби-
нированного воздействия возрастающей сложности и ограничений, накладыва-
емых сокращением времени выхода на рынок.
В соответствии с результатами исследований в области функциональной ве-
рификации, проведенных Ron Collett International (в 2002 и 2004 годах) и Far-
West Research (в 2007 году), функциональные ошибки становятся ведущими
причинами отказов СнК. Около трех четвертей ошибок при проектировании
СнК связаны с функциональными ошибками (багами). Статистика показывает,
что такие ошибки вводятся из-за различных факторов, в том числе небрежного
кодирования, неправильной интерпретации спецификации, микроархитектур-
ной сложности дизайна, случаев превышения допустимых параметров и так да-
лее. Обнаружение ошибок на низком уровне реализации обходится значительно
дороже по сравнению с выполнением верификации на более высоком уровне
абстракции. Например, выявитьошибки легче во время предварительной вали-
дации кремниевого кристалла по сравнению с посткремниевой валидацией, по-
скольку в уже изготовленном кристалле наблюдаемость внутренних сигналов
будет ограничена. Как только причина ошибки будет проанализирована, крис-
талл придется изготавливатьзаново, что стоит оченьдорого. В ином же случае
ошибка может бытьисправлена или скомпенсирована за счет существующих
механизмов. Если ошибки программного обеспечения или аппаратных средств
были выявлены уже на уровне потребителей изделий, это может привести к раз-
личным неприятным сценариям в зависимости от области их применения: как
значительным финансовым потерям товарной продукции, так даже катастрофи-
ческим последствиям при нарушении работы критически важных систем безо-
пасности. Например, в 1994 году процессор Intel Pentium совершил ошибку, ко-
торую называют FDIV bug1, и компании пришлосьзаплатитьогромную сумму
(около полумиллиарда долларов), чтобы заменитьдефектные процессоры. Точ-
1Ошибка Pentium FDIV была одной из самых позорных ошибок микропроцессоров
lntel. Из-за ошибки в справочной таблице определенные операции деления с плавающей
точкой давали неправильные результаты.
но так же, взрыв ракеты-носителя Ariane 51 был вызван ошибкой преобразо-
вания данных в управляющей программе. Поэтому так важно гарантировать
функциональную правильность перед поставкой изделий.
Функциональная валидация (или верификация2) способна выявитьлогиче -
ские/функциональные ошибки в готовых программах и аппаратном обеспече-
нии, которые не соответствуют своим спецификациям.
Графики на рис. 1.2 представляют собой сравнение результатов исследова-
ния, проведенного Far West Research (пунктир) в 2007 году, и данных исследова-
ния Wilson Research Group в 2010 году (сплошная линия), они демонстрируют
важностьверификации в осуществлении различных промышленных проектов с
точки зрения процента от общего времени проектирования, затраченного на
верификацию. Можно отметить, что с 2007 по 2010 год доля верификации в об-
щем времени проектирования значительно возросла в нескольких проектах. Ис-
следование также показывает, что процент времени, затраченного на верифика-
цию, продолжает расти. Таким образом, функциональная валидация, как
Рис. 1.2. Доля общего времени проектирования, затраченного на верификацию изделий
(источник Wilson Research Group and Mentor Graphics, 2010)
В среднем в 2007 г. — 50% В среднем в 2010 г. — 55%
Доля общего времени проектирования, затраченного на верификацию
Процент опрошенных
14 июня 1996 года беспилотная ракета Ariane 5, запущенная Европейским космичес-
ким агентством, взорвалась через несколько секунд после старта.
2«Валидация» выполняется на разных уровнях абстракции, чтобы выявитьдва типа
причин отказов: недостатки спецификации и ошибки реализации. Термин «формальная
верификация» относится к использованию формальных методов для обеспечения того,
чтобы изделия удовлетворяли всем требованиям спецификации. В этой книге термин «ве-
рификация» относится к использованию как валидации на основе моделирования, так и
формальных методов для обнаружения ошибок реализации. Пожалуйста, обратите внима-
ние, что термины «валидация» и «верификация» имеют различные применение и интер-
претацию в различных областях техники.
ожидается, останется серьезной проблемой в методологии проектирования СнК
в обозримом будущем.
Несмотря на значительные усилия по проведению функциональной валида-
ции, большинство конструкций СнК дают отказы уже в самом начале работы
(отказ кремниевого кристалла). Из результатов исследований в области функци-
ональной верификации, проведенных в Collett International Research в 2002 и
2004 годах, а FarWest Research в 2007 году, которые показаны на рис. 1.3, можно
увидетьпостоянную тенденцию роста количества повторных сборок (ре-дизайн
и повторное изготовление) изделий после обнаружения ошибок. Другими сло-
вами, повторная сборка становится все более частым явлением. Очевидно, что
подобные операции повторной сборки стоят оченьдорого и сильно влияют на
сроки выхода изделий на рынок. Таким образом, необходимо развиватьи ис-
пользовать эффективные методы функциональной валидации для уменьшения
общей трудоемкости валидации и улучшения качества продукции.
1.2. Валидация на системном уровне: возможности и проблемы
В этом разделе в первую очередьакцентирована важностьвалидации на сис-
темном уровне и введение понятия традиционного потока нисходящих про-
цессов проектирования и валидации. Далее дан обзор существующих методов
функциональной валидации. В конце раздела обсуждаются проблемы исследо-
ваний в этой области и связанные с ними возможности валидации на систем-
ном уровне.
Рис. 1.3. Отраслевые тенденции в достижении функционально работающих кристаллов (ис-
точники: данные исследований функциональной верификации за 2002 и 2004 го-
ды — Ron Collet Research, за 2007 год — FarWest Research)
Число перевыпусков кристалла
1.2.1. Нисходящий маршрут проектирования и валидации
Предварительное исследование вариантов возможных реализаций (DSE — Design
Space Exploration) требуется для создания наилучшей архитектуры СнК,
которая имеет множество различных конструктивных ограничений, таких как
стоимость, площадь, мощность, энергия, производительность и т.п. Автомати-
зированное исследование является необходимым из-за ограничений сроков
вывода на рынок и тенденции добавления более сложных функций в новые
приложения СнК. Поскольку уровень регистровых передач (RTL — Register
Transfer Level) конструкции содержит более подробную информацию, RTL мо-
делирование является слишком медленным для исследования больших и
сложных конструкций СнК. Для повышения производительности за счет по-
вышения скорости моделирования последние инновации в области проекти-
рования СнК перенесли проектирование на более высокий уровень— уровень
электронных систем (ESL)1. Проектирование на ESL специализируется на со-
здании различных спецификаций системного уровня, которые выполняются
на языках высокого уровня (например, SystemC [3],MATLAB [4], Esterel [5]) и
моделировании (например, Simulink [6], SysML [7], Petri-нетто [8]) на уровне
абстракции. Этот уровеньвыше знакомого RTL в области аппаратных средств
и исходного кода в программном обеспечении2. На таком высоком уровне
спецификации представляют определенную перспективу в описании поведе-
ния на системном уровне и широко используются в исследованиях архитекту-
ры, совместном проектировании и совместной верификации аппаратных
средств и программного обеспечения.
Традиционно проектирование СнК начинается с исследований на систем-
ном уровне и поиска подходящей спецификации архитектуры, а затем специфи-
кация превращается в реализацию на низком уровне. Для ускорения проектиро-
вания СнК были разработаны различные программы автоматизированного
проектирования электронных приборов (EDA — Electronic Design Automation)
(инструменты), которые имеют большую эффективность и производительность.
Как правило, методология нисходящего проектирования аппаратных средств
состоит из следующих уровней абстракции:
системный/архитектурный уровень. Системный уровеньсфокусирован на опи-
сании общей спецификации поведения системы и архитектурных исследованиях;
1В книге, посвященной проектированию и верификации на ESL [2], термин ESL
определяется следующим образом: «Использование соответствующих абстракций для уве-
личения понимания системы и повышения вероятности успешной реализации функцио-
нальности экономически эффективным образом».
2В зависимости от области приложений и уровней абстракции могут применяться раз-
личные типы языков описания спецификаций, например, языки описания архитектуры
(ADL) [9] оченьпопулярны для предварительного исследования и валидации процессора
на кристалле.
уровень регистровых передач. Реализация функций, полученных из специ-
фикаций системного уровня на уровне регистровых передач, использует
язык описания аппаратуры (HDL — Hardware Description Language);
уровень логических элементов. Реализация функциональной конструкции на
уровне логических элементов с использованием САПР логического синтеза;
транзисторный/физический уровень. Реализация логических конструкций с
использованием физических компонентов (например, транзисторов, про-
водников и т.д.) и инструментов их размещения и трассировки.
Проектирование программного обеспечения также имеет аналогичный ни-
сходящий поток. Для обеих конструкций необходима значительная работа по
валидации на каждом уровне проектирования СнК, чтобы гарантироватьпра -
вильность реализации проекта. Поскольку эта книга фокусируется на систем-
ном уровне валидации, мы будем рассматриватьтоль ко два самых высоких
уровня проектирования СнК для программного обеспечения и аппаратных
средств.
Рис. 1.4 представляет собой упрощенную схему проектирования и валида-
ции на первых двух (из четырех рассмотренных выше) уровнях. Различные па-
радигмы моделирования аппаратных средств и программного обеспечения ис-
пользуются для создания спецификации СнК. Двумя наиболее широко
используемыми спецификациями являются моделирование на уровне транзак-
ций (TLM — Transaction Level Modeling) [10, 11] и унифицированный язык
моделирования (UML — Unified Modeling Language) [12]. Они устанавливают
стандарт высокой скорости моделирования и легкую совместимостьмоделей
для совместного проектирования аппаратных средств и программного обеспе-
чения. В целом, TLM является перспективным языком для моделирования ап-
паратных средств, а UML фокусируется на моделировании программного
обеспечения. TLM в основном позволяет моделироватьтранзакции между раз-
24 Глава 1. Введение
Рис. 1.4. Нисходящая последовательность проектирования и валидации СнК
Создание
спецификации
(TLM/UML)
Валидация на уровне спецификации
Валидация на уровне реализации
Реализация
Программное
обеспечение
Аппаратные
средства
Разделение аппаратной и
программной частей проекта
личными аппаратными компонентами системы и обработку данных в каждом
компоненте. UML-модели могут включатькак структурную, так и поведенче-
скую информацию о системе программного обеспечения. Утвержденные спе-
цификации могут бытьисполь зованы в качестве эталонной модели для вали-
дации реализованных программного обеспечения и аппаратных средств.
В зависимости от стиля моделирования спецификации могут включатьразлич -
ный уровеньдетализации функциональной и временной информации. Напри-
мер, TLM предоставляет два вида стилей моделирования: модели, не содержа-
щие информации о времени исполнения транзакций (loosely timed models),
могут быть использованы для моделирования поведения системы с меньшей
временной информацией, а модели, содержащие примерную информацию о
времени, позволяют провести временной анализ поведения системы. Хотя
TLM является перспективным языком для системного уровня моделирования,
все еще трудно точно описатьразличные реализации и датьинформацию о
времени их выполнения. После предварительного исследования и проведения
моделирования на системном уровне RTL подходит для моделирования реали-
зации на поведенческом уровне. В схеме, представленной на рис. 1.4, аппарат-
ная частьреализована с использованием RTL языков, таких как VHDL или
Verilog, а программное обеспечение — с использованием языков программиро-
вания, таких как C или C ++.
В то время как спецификация на системном уровне имеет преимущество
для ранних исследований и валидации, введение нового уровня абстракции
также вносит потенциальные источники ошибок. В соответствии с выводами,
сделанными в работе [13], в настоящее время естьдва ключевых источника от-
казов СнК (приводящих к перевыпуску кристалла): ошибки реализации и спе-
цификации. Было обнаружено, что 82% проектов с перевыпуском в результате
функциональных отказов имели ошибки реализации. Интересно отметить, что
почти 47% проектов, перевыпущенных в результате функциональных отказов,
имели также неправильные или неполные спецификации [13]. Во время поша-
гового уточнения от системного уровня до уровня транзисторов также были
выявлены ошибки системного уровня, которые ранее было труднее обнару-
жить. Кроме того, оченьдорого выявлятьи исправлятьошибки на поздних
стадиях цикла разработки по сравнению с выявлением, проводимым на ран-
них стадиях проектирования. Таким образом, важно гарантироватьправиль -
ностьспецификаций на системном уровне. В последнее десятилетие проводят-
ся многочисленные исследования как на производстве, так и в научных кругах
по разработке методологий валидации на системном уровне [14—16]. Специ-
фикации на системном уровне позволяют повыситьскоростьмоделирования и
упроститьинтерфейс обмена данными. Путем выполнения максимального ко-
личества циклов валидации на ранних стадиях проектирования можно умень-
шитьобщую стоимостьвалидации и повыситькачество реализации. Диапазон
1.2. Валидация на системном уровне: возможности и проблемы 25
проводимых исследований включает работы от изучения методов моделирова-
ния до использования формальных методов. В этой книге мы сосредотачива-
емся на валидации на основе моделирования как спецификаций, так и реали-
зации с использованием эффективных направленных тестов. Особенно
подробно в этой книге рассматриваются различные методы моделирования на
высоком уровне и методы генерации направленных тестов для уменьшения
общей трудоемкости валидации. Следовательно, стоимость генерации тестов и
их качество представляют собой две основные задачи, которые будут рассмот-
рены в следующих главах.
1.2.2. Методы валидации СнК
Методы валидации СнК могут бытьразделены на две категории: формальная
верификация и моделирование. На рис. 1.5 показаны некоторые из широко
используемых методов в этих двух категориях. Далее в этом разделе дается об-
зор этих методов валидации проектирования.
1.2.2.1. Валидация на основе моделирования
Валидация на основе моделирования [17] позволяет обнаружитьошибки про-
ектирования благодаря использованию векторов тестовых последовательно-
стей, состоящих из входных воздействий и ожидаемых выходных результатов
[18—21]. На рис. 1.6 показана схема традиционной валидации на основе мо-
делирования. Валидация состоит из трех основных процедур: 1) генерации
тестовых векторов, 2) моделирования конструкций СнК с использованием тес-
товых векторов, 3) сравнения сгенерированных выходных сигналов с ожидае-
мыми результатами. В процессе валидации тестируемые параметры показыва-
ют, какая частьдизайна не была верифицирована и какие тесты должны быть
добавлены. Для обнаружения различных типов ошибок проектирования на
различных уровнях абстракции дизайна предлагается тестироватьразличные
параметры. Генерация направленных тестов с управляемым тестовым покры-
Рис. 1.5. Методы валидации СнК
Валидация на уровне спецификации
Формальная верификация Подходы на основе моделирования
Проверка
неограниченной модели
Верификация выполнимости
ограниченной модели
Ограниченно-
случайные
тесты
Направленные
тесты
Доказательство
теорем
Верификация
модели
Решение задачи
выполнимости
Случайные
тесты
тием предназначена для активации точки целевого покрытия, что эффективно
сокращает количество тестов по сравнению со случаем применения случайных
тестов. Посредством моделирования эффективностьтестового покрытия ана-
лизируется на предмет того, покрыты ли целевые функции тестами или нет,
таким образом, можно измеритьход валидации. Если найдены пробелы в по-
крытии (т.е. тестирование оказалосьнедостаточным), создаются дополнитель-
ные тесты для их валидации. Если требуется высокая степеньдоверия, мы мо-
жем улучшитьметрику покрытия или использоватьдополнитель ные методы
тестового покрытия. Инженеры-тестировщики могут изменятьобластьи глу-
бину покрытия в течение процесса валидации. Для примера, они могут начать
с простых метрик покрытия на ранней стадии валидации и использовать более
сложные метрики покрытия позже.
Генерация тестов играет важную рольв валидации, управляемой модели-
рованием. Она определяет не только качество тестирования, но также сильно
влияет на время моделирования. Естьтри типа методов генерации тестов:
генерация случайных, ограниченно-случайных и направленных тестов. В теку-
щей производственной практике [22, 23] наиболее широко используются ме-
тоды генерации случайных и ограниченно-случайных тестов, потому что тес-
товые векторы могут бытьполучены автоматически, следовательно, большая
частьошибок дизайна может бытьобнаружена в начале цикла разработки. Тем
не менее, необходимо огромное количество тестов для достижения высокой
степени уверенности в правильности дизайна, поскольку можно легко пропус-
титьсостояния дизайна, в которых наступает отказ (например, состояния кон-
вейера, соотношения тактовых сигналов). По сравнению со случайными мето-
дами тестирования, которые используют миллиарды и триллионы случайных и
псевдослучайных тестов, в традиционном направленном тестировании дизайна
применяется меньше тестов для получения требуемого тестового покрытия
функций, поскольку в данном случае используется информация о структуре
дизайна [24, 25]. Путем применения направленных тестов общая трудоемкость
валидации может бытьумень шена без сокращения целевого тестового покры-
тия. Большинство методов генерации направленных тестов требуют эксперт-
1.2. Валидация на системном уровне: возможности и проблемы 27
Рис. 1.6. Последовательность валидации на основе моделирования
Генерация
тестов
Анализ
тестового
покрытия
Метрики
покрытия
Удовлет-
ворительно
Отчет (ошиб-
ки/тестовое
покрытие)
Выходные
результаты
Сравнение
откликов
с эталоном
Моделирующая
система
Входные
воздействия
Нет
Да
ных знаний валидируемого дизайна (DUV — Design Under Validation). Как
правило, методы генерации направленных тестов являются трудоемкими и
подвержены ошибкам. Из-за неизбежного вмешательства человека невозмож-
на генерация всех направленных тестов для достижения всеобъемлющего це-
левого покрытия в разумные сроки. Эта книга описывает несколько эффек-
тивных методов выполнения автоматической генерации направленных тестов.
Методы моделирования достаточно хорошо работают при валидации слож-
ных конструкций. Легко проверить, активируется ли функциональный сцена-
рий данным тестом при валидации дизайна с многомиллионным количеством
соединений. Тем не менее, достаточно трудно гарантироватьправиль ность
проектирования, используя валидацию на основе моделирования. Например,
чтобы обеспечитьправиль ностьдизайна СнК, требуется проверитьвсе воз-
можные входные стимулы. Однако невозможно сгенерироватьи моделировать
все возможные входные последовательности, так как их число может быть
чрезмерно большим (потенциально бесконечным!). Как правило, используют-
ся триллионы случайных или ограниченно-случайных тестов при моделирова-
нии из-за ограничений сроков выхода на рынок и в силу других причин. Так
как применяются только выборочные входные воздействия (вместо валидации
всех возможных входных последовательностей), валидация не дает уверенно-
сти в правильности дизайна. Нельзя считать, что непротестированный процесс
(функциональность) является корректным или не достижим. Кроме того, су-
ществует нехватка хороших метрик покрытия для количественной оценки сте-
пени доверия и квалификации набора тестов. Поэтому трудно ответитьна во-
прос: «Когда верификация завершена?» из-за сложностей оценки прогресса
верификации и эффективности тестов.
Задача функциональной верификации в той или иной мере встает перед каж-
дым инженером, занимающимся проектированием электронных систем. Дока-
зательство того, что система функционирует так, как того требует специфика-
ция, с ростом сложности системы требует все больших ресурсов. Причем рост
сложности далеко не линеен.
Современные тенденции в микроэлектронике определяют переход к про-
цессорно-ориентированным системам и совместной разработке аппаратной
части и программного обеспечения. Разработка программного обеспечения до
готовности аппаратной части требует наличия виртуальных прототипов, обес-
печивающих переход на системный уровеньпроектирования.
Требования к росту производительности систем подталкивают к использо-
ванию нескольких процессоров и более сложных шинных архитектур. Появле-
ние аппаратных ускорителей перекладывает верификацию функционала с про-
граммистов на разработчиков аппаратуры.
Некачественная или неполная верификация может привести к некоррект-
ной работе программы уже после начала ее использования потребителем.
В этом случае пострадает в первую очередьрепутация разработчика.
Одновременно с указанными проблемами время выхода на рынок в усло-
виях конкуренции постоянно сокращается, что накладывает дополнительные
ограничения на процесс верификации. Чтобы справиться с возникающими
сложностями, требуются разработка и внедрение новых методов верификации,
более производительных, абстрактных и автоматизированных. Повышенная
производительность может достигаться за счет совершенствования вычисли-
тельных систем, использования более мощных серверов, оптимизации алго-
ритмов, появления новых методик верификации и комбинирования сущест-
вующих. Абстрактностьдостигается за счет использования языка C и его
библиотек (таких как SystemC) с последующей автоматизированной конверта-
цией в языки описания аппаратуры SystemVerilog и VHDL. Автоматизацию
следует проводитьв области генерации тестов.
Попытка описатьметоды решения указанных проблем находит отражение
в книге, которую Вы держите в руках. Она является переводом англоязычной
публикации и ориентирована на русскоговорящих инженеров, занимающихся
верификацией систем-на-кристалле, и может бытьполезна для понимания
сложностей, возникающих в процессе верификации сложных электронных си-
стем, и методов их решения. Надеемся, что каждый найдет для себя в этой
книге что-нибудьполезное.
Генеральный директор ЗАО «СКАН»
Ланцев А.Н.
ПРЕДИСЛОВИЕ
Посвящается нашим семьям
В повседневной жизни мы окружены компьютерами. Мы осознаем сложность
компьютерных систем, поскольку пользуемся настольными компьютерами,
ноутбуками или серверами. Во многих жизненных ситуациях мы взаимодейст-
вуем с системами, которые имеют встроенные компьютеры, например, сото-
вые телефоны, гаджеты и системы мониторинга. В конструкции самолета или
автомобиля много вычислительных устройств, совместная работа которых га-
рантирует, что наше путешествие будет приятным и безопасным. Можем ли
мы с уверенностью сказать, что эти встроенные вычислительные системы
сконструированы и изготовлены правильно и качественно, чтобы смело пола-
гаться на их функции? Простой ответ заключается в том, что никто не может
доказатьих абсолютную непогрешимость. Однако, поскольку у нас нет выбо-
ра, нам остается только расслабиться и наслаждаться жизнью!
Рассмотрим простой сумматор, чтобы понятьтрудности верификации со-
временных компьютерных систем. Сумматор является одним из простейших
вычислительных устройств в калькуляторе. Он складывает два входных значе-
ния и выдает результат. Как правило, входными значениями являются 32-раз-
рядные целые числа. Поэтому, чтобы проверитьтакой сумматор, мы должны
смоделироватьнесколь ко триллионов (232 Ї 232) тестовых векторов. Очевидно,
что слишком дорого применятьтриллионы входных векторов для проверки
сумматора. Фактически, невозможно имитироватьсумматор с использованием
всех возможных входных последовательностей, когда входными значениями
выступают 64-битные целые числа. Если мы не способны полностью верифи-
цироватьпростой сумматор, то как можно надеяться, что мы сможем прове-
ритьсовременные встроенные и гибридные системы, которые состоят из
сложного программного обеспечения и аппаратных средств, включая мульти-
и многоядерные процессоры, память, шины, контроллеры, интерфейсы и т.д.?
Функциональная валидация широко признана как основное узкое место в ме-
тодологии проектирования систем-на-кристалле (SoC—System-on-Chip), по-
этому на нее затрачивается до 70% от общего времени разработки и ресурсов.
Несмотря на стользначитель ные усилия, многие конструкции СнК отказыва-
ют уже при первых тестах (отказ кремниевого кристалла) в связи с функцио-
нальными ошибками. Сложность функциональной валидации, как ожидается,
вырастет еще больше в связи с совокупным влиянием возрастающей сложно-
сти проектирования и сокращением сроков выхода на рынок.
Существующие подходы к валидации используют комбинацию методов
моделирования и формальной верификации. Моделирование является наибо-
лее широко используемой формой валидации с применением генерации слу-
чайных и ограничено-случайных тестов. Например, в случае с сумматором
вместо того, чтобы проверятьвсе возможные комбинации входных данных,
инженеры-валидаторы могут генерироватьтесты для нужных им функцио-
нальных сценариев на основе критериев тестового покрытия и случаев преде-
льного превышения интересующих их параметров. Так как нецелесообразно
создаватьи применятьвсе возможные тесты, валидация на основе моделиро-
вания не гарантирует качество дизайна. С другой стороны, формальные мето-
ды валидации (такие как верификация моделей) не используют входных век-
торов, но исследуют пространство состояний для обеспечения правильности
функционирования. К сожалению, это исследование может привести к расши-
рению пространства состояний в случае валидации больших и сложных проек-
тов. В современных методиках валидации используется эффективное соче-
тание обоих подходов. Для примера, полный дизайн СнК моделируется с
помощью миллиардов тестов, в то время как очень важные компоненты, такие
как контроллеры или конкретные протоколы, полностью верифицируются
формальными методами.
Существуют различные перспективные направления, позволяющие зна-
чительно сократитьобщую трудоемкостьвалидации за счет совместного ис-
пользования моделирования и формальной верификации. Они полезны для
верификации, насколько ее возможно проводить на уровне спецификации
(которая представляет собой оценку порядка величины и потому проще, чем
верификация на уровне реализации, но позволяет исследоватьвсе функцио-
нальные детали) и автоматического повторного использования валидации
высокого уровня для верификации реализации систем низкого уровня. Ана-
логично, они используют направленные тесты для валидации дизайна, так
как подобные тесты позволяют достичьтого же целевого тестового покрытия
с помощью оценки по порядку величины при меньшем количестве тестов по
сравнению с использованием случайных или ограничено-случайных тестов.
В результате моделирование с использованием эффективных направленных
тестов может существенно снизитьобщую трудоемкостьвалидации. Однако
генерация направленных тестов в основном выполняется при вмешательстве
человека. Написанные от руки тесты влекут за собой трудоемкую и отни-
мающую много времени работу инженеров-валидаторов, которые имеют
глубокие знания о конструкциях, проходящих верификацию. Для сложных
конструкций невозможно вручную создатьвсе направленные тесты для до-
стижения всеобъемлющего тестового покрытия. Таким образом, необходимо
разработатьинструменты и методы для автоматической генерации направ-
ленных тестов.
Эта книга описывает инновационные пути объединения моделирования и
формальных методов валидации сложных систем. В ней представлен всесто-
ронний обзор моделирования и методов валидации на системном уровне, на-
правленных на снижение общей трудоемкости валидации и улучшение качест-
ва продукции. Она описывает проблемы, связанные с проверкой сложных
систем и представляет эффективные методы решения этих проблем. В книге
рассматриваются различные методы моделирования на системном уровне,
использующие языки проектирования SystemC, UML (Unified Modeling Language
— унифицированный язык моделирования) и моделирование на уровне
транзакций. Она представляет состояние современных методов для автомати-
ческой генерации направленных тестов с упором на сокращение времени на
генерацию тестов и трудоемкости валидации посредством применения мето-
дов кластеризации, декомпозиции и обучения. Она также описывает новые
пути повторного использования валидации высокого уровня на различных
уровнях абстракции.
Читательэтой книги получит полное понимание задач верификации про-
ектируемых систем и узнает, как валидация на системном уровне может зна-
чительно улучшитькачество проектирования и снизитьобщую стоимостьиз-
делий. В главе 1 представлены преимущества валидации на системном уровне.
Глава 2 описывает, как задатьсложные системы, использующие высокоуров-
невые модели. Глава 3 содержит основные схемы автоматической генерации
направленных тестов. В следующей главе рассказывается, как значительно
уменьшить число тестов без ущерба для целевого тестового покрытия. В главах
5—9 описаны эффективные методы генерации направленных тестов. В следу-
ющих двух главах представлены методы генерации тестов с упором на валида-
цию многоядерных архитектур. Глава 12 описывает инновационные способы
повторного использования сгенерированных тестов и утверждений высокого
уровня для валидации систем на уровне реализации. Наконец, глава 13 завер-
шает книгу кратким обсуждением перспективных направлений исследований.
Мы надеемся, что вам понравится наша книга, в которой вы найдете полез-
ную информацию.
Целевая аудитория
Эта книга предназначена для студентов старших курсов, аспирантов, исследо-
вателей, разработчиков инструментов САПР, проектировщиков и менеджеров,
заинтересованных в развитии эффективных инструментов и методов проекти-
рования и валидации на системном уровне, генерации направленных тестов и
функциональной валидации гетерогенных конструкций СнК.
БЛАГОДАРНОСТИ
Эта книга является результатом десятилетних научных исследований и про-
мышленного сотрудничества многих коллективов. Книга включает в себя опи-
сание методов и представлений о валидации на системном уровне, которые ста-
ли результатом диссертаций профессора Минсон Чэня, доктора Хун-Mo Kу и
доктора Ксяоке Циня. Мы хотели бы поблагодаритьнаших спонсоров за ока-
занную финансовую поддержку в этом исследовании. Эта работа была частично
профинансирована Национальным научным фондом (National Science Foundation
(CAREER Award 0746261, CCF-0903430. and CNS 0905308), Semiconductor
Research Corporation (2009-HJ-1979), Intel Corporation, Фондом докторантуры
Министерства образования Китая 20110076120025 и средствами Государствен-
ного плана Китая по высокотехнологичным разработкам 2011AA010101.
Эта книга несет печатьсотрудничества с многочисленными коллективами.
Мы хотели бы отметитьвклад доктора Магди Абадира (Freescale), доктора
Джаянта Бхадра (Freescale), профессора Никила Датта (UC Irvine), профессора
Масахиро Фуджита (Токийский университет), доктора Хуан Чжо, доктора
Друбайоти Калита (Intel), профессора Тулика Митра (NUS Сингапур) и про-
фессора Абхика Ройчудхури (NUS Сингапур). Мы также благодарны всем чле-
нам CISE Embedded Systems Lab Университета Флориды. В список входят док-
тор Канад Басу, Хади Хаджимири, Камран Рахмани, Камик Шривастава,
Четан Мурти, Сеок-Фан Сеон и доктор Вейксун Ван.
ОБ АВТОРАХ
Минсон Чэньявляется адъюнкт-профессором в Software Engineering Institute
при Восточно-Китайском педагогическом университете. Его исследования на-
правлены на автоматизацию проектирования встроенных систем, разработку
кибер-физических систем, методов моделирования и проверки программного
обеспечения. Он получил степени бакалавра и магистра в Нанкинском уни-
верситете в 2003 и 2006 годах, соответственно, и доктора наук — в Универси-
тете штата Флорида в 2010 году, все в области компьютерных наук. Он опуб-
ликовал множество научных статей в ведущих международных журналах и
материалах международных конференций. Одна из его работ была номиниро-
вана на Best Paper Award Международной конференции по VLSI Design 2009.
В настоящее время его исследования финансируются Национальным научным
фондом Китая, Министерством образования и включены в Государственный
план по высокотехнологичным разработкам. Доктор Чэньработал в качестве
члена оргкомитетов по разработке программ ряда конференций ACM и IEEE,
включая SAC и ICFEM. Он является членом обеих ACM и IEEE.
Ксяоке Циньполучил степени бакалавра и магистра на факультете автома-
тизации Университета Цинхуа в Пекине в 2004 и 2007 годах, соответственно.
Докторскую диссертацию он защищал на факультете компьютерных и инфор-
мационных наук и инженерии Университета штата Флориды в 2012 году. Его
исследовательские интересы лежат в области сжатия кода, верификации моде-
лирования, валидации на системном уровне многоядерных архитектур и пла-
нировании производства встроенных систем в реальном времени. Он опубли-
ковал множество статей в ведущих мировых журналах и материалах
международных конференций. Его работа по валидации согласованности кэша
была номинирована на Best Paper Award в области автоматизации проектиро-
вания и испытаний в Европе (DATE), 2012. Доктор Циньвыступал в качестве
рецензента и обозревателя нескольких конференций и журналов ACM и IEEE.
Хеон-Mo Kу является специалистом по медиаархитектуре в группе парал-
лельной обработки визуальных данных корпорации Intel. Его исследователь-
ские интересы лежат в области проектирования и верификации встраиваемых
систем для медиа-технологий, включая видеокодеки, обработку видео и
машинное распознавание образов. Он получил степени бакалавра и магистра
на факультете электроники и электротехники Национального университета
Kyungpook в Корее в 1993 и 1995 годах, соответственно. До начала работы над
докторской диссертацией он работал в компании LG Electronics Research Center
в течение 8 лет. Он получил докторскую степеньпо вычислительной техни-
ке в Университете Флориды в 2007 году.
Прабхат Мишра является адъюнкт-профессором на кафедре компьютер-
ных и информационных наук в Университете штата Флорида. Его исследова-
тельские интересы включают автоматизацию проектирования встроенных сис-
тем, вычисление энергопотребления, верификацию аппаратных средств и
программного обеспечения и проектирование безопасных систем. Он получил
степеньбакалавра в Университете Джанавпур в Калькутте в 1994 году, степень
магистра по технологии в Индийском технологическом институте в Кхарагпу-
ре в 1996 году и доктора наук в Университете штата Калифорния, Ирвин, в
2004 году, все в области компьютерных наук. До прихода в Университет штата
Флорида он несколько лет работал в различных компаниях, специализирую-
щихся в разработке полупроводниковых приборов и автоматизации проекти-
рования, включая Intel, Motorola, Synopsys и Texas Instruments. Он опублико-
вал четыре книги, был соавтором десяти книг и написал более 100 научных
статей в ведущих мировых журналах и материалах различных конференций.
Его исследования получили несколько наград, включая премию NSF CAREER
от Национального научного фонда, две премии за лучшую статью (VLSI Design
2011 и CODES+ISSS 2003), он имеет несколько номинаций на лучшую
статью и премию EDAA 2004 года за выдающуюся диссертационную работу от
Европейской ассоциации автоматизации проектирования (European Design
Automation Association). В 2007 году он получил премию как Международный
педагог года от инженерного колледжа Университета штата Флорида за значи-
тельный вклад в международные научные исследования и преподавание
компьютерных наук. В настоящее время он работает в качестве помощника
редактора в журналах ACM Transactions on Design Automation of Electronic Systems
(TODAES), IEEE Design & Test of Computers (D&T) и Joumal of Electronic
Testing (JETTA), внештатным редактором в журнале IEEE Transactions on
Computers, а также выступал членом оргкомитета ряда конференций ACM и
IEEE, в том числе ICCAD, DATE, ASPDAC, CODES+ISSS и VLSI Design. Он
занимал должностьгенераль ного председателя на конференции IEEE High-Level
Design Validation and Test (HLDVT) 2010, был руководителем группы по
разработке программы конференции HLDVT 2009 года, информационным
директором ACM TODAES и работал внештатным редактором в издательст-
вах IEEE D&T, Springer JETTA и IJPP. Он является старшим членом в ACM
и IEEE.
СПИСОК СОКРАЩЕНИЙ
ABV — Валидация на основе утверждений
ADL — Язык описания архитектуры
ATE — Автоматическое тестовое оборудование
АТМ — Банкомат (автоматизированный кассовый терминал)
ATPG — Автоматический генератор тестовых векторов
BCP — Булево распространение ограничений
BDD — Двоичные диаграммы решений
BIST — Встроенное самотестирование
BMC — Проверка ограниченной модели
CNF — Конъюнктивная нормальная форма
CSP — Проблема (задача) удовлетворения ограничений
DAG — Направленный ациклический граф
DSE — Исследование пространства проектных параметров
DUV — Валидируемый дизайн
ESL — Уровеньэлектронных систем
FSM — Конечный автомат (автомат с конечным числом состояний)
IC — Интегральная схема
LTL — Линейная временная логика
MоC — Модельв ычислений
MPSoC — Мультипроцессорная система на кристалле
PSL — Язык описания свойств
RTL — Уровеньрегистровых передач
SAT — Выполнимость
SoC — Система на кристалле
SVA — Утверждение SystemVerilog
TLM — Моделирование на уровне транзакций
TRS — Спецификация уточняющих тестов
UMC — Проверка неограниченной модели
UML — Унифицированный язык моделирования
VSIDS — Уменьшение суммы, независимое от состояния переменной
XMI — Обмен метаданными с помощью XML
ГЛАВА 1
Введение
1.1. 1.1. Растущая сложность валидации СнК
Система на кристалле (SoC) включает в себя все необходимые аппаратные ком-
поненты (например, микропроцессоры, блоки памяти и периферийные устрой-
ства) и программные модули (операционные системы, работающие в реальном
времени, и программы контроля), объединяя их в единую интегральную схему с
требуемой функциональностью. Она может выполнять различные вычисления,
в том числе цифровые, аналоговые, а также смешанные цифро-аналоговые.
Рис. 1.1 представляет блок-схему архитектуры типичной многопроцессорной
СнК (MPSoC — Multiprocessor System-on-Chip) [1]. Например, дизайн СнК со-
стоит из четырех RISC-процессоров и различных общих устройств ввода-выво-
да, которые соединены высокопроизводительной шиной (AНB — Advanced
High-Performance Bus) и периферийной шиной (APB — Advanced Peripheral
Bus). СнК широко используются во встраиваемых системах, применяемых в та-
ких областях, как автомобильная электроника, авионика, телекоммуникации,
создание интеллектуальных зданий, портативных устройств и т.д.
В связи с увеличением сложности программных и аппаратных компонентов
сложностьпроектирования современных СнК растет с угрожающей скоростью.
Для размещения новых приложений и удовлетворения вычислительных требо-
ваний современные СнК используют множество сложных архитектурных осо-
бенностей для поддержки синхронизации, обмена данными, динамического ре-
гулирования частоты и напряжения, когерентности кэшей, конвейеризации
Рис. 1.1. Пример дизайна MPSoC: арбитр — устройство разрешения конфликтов
Арбитр
Кон-
троллер
памяти
АНВ/
АРВ-
мост
АНВ-шина
АРВ-шина
межсоединений и т.д. Увеличение сложности дизайна вызывает рост сложности
верификации. Быстрое развитие технологий совместно с жесткой конкуренцией
на рынке поставило разработку СнК перед проблемой: как быстро гарантиро-
вать функциональную правильность СнК? Функциональная верификация СнК
широко признана в качестве основного узкого места. Недопустимо моделиро-
ватьдаже простой двухвходовой сумматор с использованием всех возможных
входных последовательностей, так как это потребует 264 264 входных (тестовых)
векторов, когда каждый вход составляет 64 бита. Верификация комплексных
СнК аналогична верификации миллионов и миллиардов комплексных суммато-
ров, взаимодействующих друг с другом в виде программного обеспечения и/или
аппаратных средств. Серьезными проблемами являются обнаружение всех
функциональных ошибок, а также электротехнических дефектов из-за комби-
нированного воздействия возрастающей сложности и ограничений, накладыва-
емых сокращением времени выхода на рынок.
В соответствии с результатами исследований в области функциональной ве-
рификации, проведенных Ron Collett International (в 2002 и 2004 годах) и Far-
West Research (в 2007 году), функциональные ошибки становятся ведущими
причинами отказов СнК. Около трех четвертей ошибок при проектировании
СнК связаны с функциональными ошибками (багами). Статистика показывает,
что такие ошибки вводятся из-за различных факторов, в том числе небрежного
кодирования, неправильной интерпретации спецификации, микроархитектур-
ной сложности дизайна, случаев превышения допустимых параметров и так да-
лее. Обнаружение ошибок на низком уровне реализации обходится значительно
дороже по сравнению с выполнением верификации на более высоком уровне
абстракции. Например, выявитьошибки легче во время предварительной вали-
дации кремниевого кристалла по сравнению с посткремниевой валидацией, по-
скольку в уже изготовленном кристалле наблюдаемость внутренних сигналов
будет ограничена. Как только причина ошибки будет проанализирована, крис-
талл придется изготавливатьзаново, что стоит оченьдорого. В ином же случае
ошибка может бытьисправлена или скомпенсирована за счет существующих
механизмов. Если ошибки программного обеспечения или аппаратных средств
были выявлены уже на уровне потребителей изделий, это может привести к раз-
личным неприятным сценариям в зависимости от области их применения: как
значительным финансовым потерям товарной продукции, так даже катастрофи-
ческим последствиям при нарушении работы критически важных систем безо-
пасности. Например, в 1994 году процессор Intel Pentium совершил ошибку, ко-
торую называют FDIV bug1, и компании пришлосьзаплатитьогромную сумму
(около полумиллиарда долларов), чтобы заменитьдефектные процессоры. Точ-
1Ошибка Pentium FDIV была одной из самых позорных ошибок микропроцессоров
lntel. Из-за ошибки в справочной таблице определенные операции деления с плавающей
точкой давали неправильные результаты.
но так же, взрыв ракеты-носителя Ariane 51 был вызван ошибкой преобразо-
вания данных в управляющей программе. Поэтому так важно гарантировать
функциональную правильность перед поставкой изделий.
Функциональная валидация (или верификация2) способна выявитьлогиче -
ские/функциональные ошибки в готовых программах и аппаратном обеспече-
нии, которые не соответствуют своим спецификациям.
Графики на рис. 1.2 представляют собой сравнение результатов исследова-
ния, проведенного Far West Research (пунктир) в 2007 году, и данных исследова-
ния Wilson Research Group в 2010 году (сплошная линия), они демонстрируют
важностьверификации в осуществлении различных промышленных проектов с
точки зрения процента от общего времени проектирования, затраченного на
верификацию. Можно отметить, что с 2007 по 2010 год доля верификации в об-
щем времени проектирования значительно возросла в нескольких проектах. Ис-
следование также показывает, что процент времени, затраченного на верифика-
цию, продолжает расти. Таким образом, функциональная валидация, как
Рис. 1.2. Доля общего времени проектирования, затраченного на верификацию изделий
(источник Wilson Research Group and Mentor Graphics, 2010)
В среднем в 2007 г. — 50% В среднем в 2010 г. — 55%
Доля общего времени проектирования, затраченного на верификацию
Процент опрошенных
14 июня 1996 года беспилотная ракета Ariane 5, запущенная Европейским космичес-
ким агентством, взорвалась через несколько секунд после старта.
2«Валидация» выполняется на разных уровнях абстракции, чтобы выявитьдва типа
причин отказов: недостатки спецификации и ошибки реализации. Термин «формальная
верификация» относится к использованию формальных методов для обеспечения того,
чтобы изделия удовлетворяли всем требованиям спецификации. В этой книге термин «ве-
рификация» относится к использованию как валидации на основе моделирования, так и
формальных методов для обнаружения ошибок реализации. Пожалуйста, обратите внима-
ние, что термины «валидация» и «верификация» имеют различные применение и интер-
претацию в различных областях техники.
ожидается, останется серьезной проблемой в методологии проектирования СнК
в обозримом будущем.
Несмотря на значительные усилия по проведению функциональной валида-
ции, большинство конструкций СнК дают отказы уже в самом начале работы
(отказ кремниевого кристалла). Из результатов исследований в области функци-
ональной верификации, проведенных в Collett International Research в 2002 и
2004 годах, а FarWest Research в 2007 году, которые показаны на рис. 1.3, можно
увидетьпостоянную тенденцию роста количества повторных сборок (ре-дизайн
и повторное изготовление) изделий после обнаружения ошибок. Другими сло-
вами, повторная сборка становится все более частым явлением. Очевидно, что
подобные операции повторной сборки стоят оченьдорого и сильно влияют на
сроки выхода изделий на рынок. Таким образом, необходимо развиватьи ис-
пользовать эффективные методы функциональной валидации для уменьшения
общей трудоемкости валидации и улучшения качества продукции.
1.2. Валидация на системном уровне: возможности и проблемы
В этом разделе в первую очередьакцентирована важностьвалидации на сис-
темном уровне и введение понятия традиционного потока нисходящих про-
цессов проектирования и валидации. Далее дан обзор существующих методов
функциональной валидации. В конце раздела обсуждаются проблемы исследо-
ваний в этой области и связанные с ними возможности валидации на систем-
ном уровне.
Рис. 1.3. Отраслевые тенденции в достижении функционально работающих кристаллов (ис-
точники: данные исследований функциональной верификации за 2002 и 2004 го-
ды — Ron Collet Research, за 2007 год — FarWest Research)
Число перевыпусков кристалла
1.2.1. Нисходящий маршрут проектирования и валидации
Предварительное исследование вариантов возможных реализаций (DSE — Design
Space Exploration) требуется для создания наилучшей архитектуры СнК,
которая имеет множество различных конструктивных ограничений, таких как
стоимость, площадь, мощность, энергия, производительность и т.п. Автомати-
зированное исследование является необходимым из-за ограничений сроков
вывода на рынок и тенденции добавления более сложных функций в новые
приложения СнК. Поскольку уровень регистровых передач (RTL — Register
Transfer Level) конструкции содержит более подробную информацию, RTL мо-
делирование является слишком медленным для исследования больших и
сложных конструкций СнК. Для повышения производительности за счет по-
вышения скорости моделирования последние инновации в области проекти-
рования СнК перенесли проектирование на более высокий уровень— уровень
электронных систем (ESL)1. Проектирование на ESL специализируется на со-
здании различных спецификаций системного уровня, которые выполняются
на языках высокого уровня (например, SystemC [3],MATLAB [4], Esterel [5]) и
моделировании (например, Simulink [6], SysML [7], Petri-нетто [8]) на уровне
абстракции. Этот уровеньвыше знакомого RTL в области аппаратных средств
и исходного кода в программном обеспечении2. На таком высоком уровне
спецификации представляют определенную перспективу в описании поведе-
ния на системном уровне и широко используются в исследованиях архитекту-
ры, совместном проектировании и совместной верификации аппаратных
средств и программного обеспечения.
Традиционно проектирование СнК начинается с исследований на систем-
ном уровне и поиска подходящей спецификации архитектуры, а затем специфи-
кация превращается в реализацию на низком уровне. Для ускорения проектиро-
вания СнК были разработаны различные программы автоматизированного
проектирования электронных приборов (EDA — Electronic Design Automation)
(инструменты), которые имеют большую эффективность и производительность.
Как правило, методология нисходящего проектирования аппаратных средств
состоит из следующих уровней абстракции:
системный/архитектурный уровень. Системный уровеньсфокусирован на опи-
сании общей спецификации поведения системы и архитектурных исследованиях;
1В книге, посвященной проектированию и верификации на ESL [2], термин ESL
определяется следующим образом: «Использование соответствующих абстракций для уве-
личения понимания системы и повышения вероятности успешной реализации функцио-
нальности экономически эффективным образом».
2В зависимости от области приложений и уровней абстракции могут применяться раз-
личные типы языков описания спецификаций, например, языки описания архитектуры
(ADL) [9] оченьпопулярны для предварительного исследования и валидации процессора
на кристалле.
уровень регистровых передач. Реализация функций, полученных из специ-
фикаций системного уровня на уровне регистровых передач, использует
язык описания аппаратуры (HDL — Hardware Description Language);
уровень логических элементов. Реализация функциональной конструкции на
уровне логических элементов с использованием САПР логического синтеза;
транзисторный/физический уровень. Реализация логических конструкций с
использованием физических компонентов (например, транзисторов, про-
водников и т.д.) и инструментов их размещения и трассировки.
Проектирование программного обеспечения также имеет аналогичный ни-
сходящий поток. Для обеих конструкций необходима значительная работа по
валидации на каждом уровне проектирования СнК, чтобы гарантироватьпра -
вильность реализации проекта. Поскольку эта книга фокусируется на систем-
ном уровне валидации, мы будем рассматриватьтоль ко два самых высоких
уровня проектирования СнК для программного обеспечения и аппаратных
средств.
Рис. 1.4 представляет собой упрощенную схему проектирования и валида-
ции на первых двух (из четырех рассмотренных выше) уровнях. Различные па-
радигмы моделирования аппаратных средств и программного обеспечения ис-
пользуются для создания спецификации СнК. Двумя наиболее широко
используемыми спецификациями являются моделирование на уровне транзак-
ций (TLM — Transaction Level Modeling) [10, 11] и унифицированный язык
моделирования (UML — Unified Modeling Language) [12]. Они устанавливают
стандарт высокой скорости моделирования и легкую совместимостьмоделей
для совместного проектирования аппаратных средств и программного обеспе-
чения. В целом, TLM является перспективным языком для моделирования ап-
паратных средств, а UML фокусируется на моделировании программного
обеспечения. TLM в основном позволяет моделироватьтранзакции между раз-
24 Глава 1. Введение
Рис. 1.4. Нисходящая последовательность проектирования и валидации СнК
Создание
спецификации
(TLM/UML)
Валидация на уровне спецификации
Валидация на уровне реализации
Реализация
Программное
обеспечение
Аппаратные
средства
Разделение аппаратной и
программной частей проекта
личными аппаратными компонентами системы и обработку данных в каждом
компоненте. UML-модели могут включатькак структурную, так и поведенче-
скую информацию о системе программного обеспечения. Утвержденные спе-
цификации могут бытьисполь зованы в качестве эталонной модели для вали-
дации реализованных программного обеспечения и аппаратных средств.
В зависимости от стиля моделирования спецификации могут включатьразлич -
ный уровеньдетализации функциональной и временной информации. Напри-
мер, TLM предоставляет два вида стилей моделирования: модели, не содержа-
щие информации о времени исполнения транзакций (loosely timed models),
могут быть использованы для моделирования поведения системы с меньшей
временной информацией, а модели, содержащие примерную информацию о
времени, позволяют провести временной анализ поведения системы. Хотя
TLM является перспективным языком для системного уровня моделирования,
все еще трудно точно описатьразличные реализации и датьинформацию о
времени их выполнения. После предварительного исследования и проведения
моделирования на системном уровне RTL подходит для моделирования реали-
зации на поведенческом уровне. В схеме, представленной на рис. 1.4, аппарат-
ная частьреализована с использованием RTL языков, таких как VHDL или
Verilog, а программное обеспечение — с использованием языков программиро-
вания, таких как C или C ++.
В то время как спецификация на системном уровне имеет преимущество
для ранних исследований и валидации, введение нового уровня абстракции
также вносит потенциальные источники ошибок. В соответствии с выводами,
сделанными в работе [13], в настоящее время естьдва ключевых источника от-
казов СнК (приводящих к перевыпуску кристалла): ошибки реализации и спе-
цификации. Было обнаружено, что 82% проектов с перевыпуском в результате
функциональных отказов имели ошибки реализации. Интересно отметить, что
почти 47% проектов, перевыпущенных в результате функциональных отказов,
имели также неправильные или неполные спецификации [13]. Во время поша-
гового уточнения от системного уровня до уровня транзисторов также были
выявлены ошибки системного уровня, которые ранее было труднее обнару-
жить. Кроме того, оченьдорого выявлятьи исправлятьошибки на поздних
стадиях цикла разработки по сравнению с выявлением, проводимым на ран-
них стадиях проектирования. Таким образом, важно гарантироватьправиль -
ностьспецификаций на системном уровне. В последнее десятилетие проводят-
ся многочисленные исследования как на производстве, так и в научных кругах
по разработке методологий валидации на системном уровне [14—16]. Специ-
фикации на системном уровне позволяют повыситьскоростьмоделирования и
упроститьинтерфейс обмена данными. Путем выполнения максимального ко-
личества циклов валидации на ранних стадиях проектирования можно умень-
шитьобщую стоимостьвалидации и повыситькачество реализации. Диапазон
1.2. Валидация на системном уровне: возможности и проблемы 25
проводимых исследований включает работы от изучения методов моделирова-
ния до использования формальных методов. В этой книге мы сосредотачива-
емся на валидации на основе моделирования как спецификаций, так и реали-
зации с использованием эффективных направленных тестов. Особенно
подробно в этой книге рассматриваются различные методы моделирования на
высоком уровне и методы генерации направленных тестов для уменьшения
общей трудоемкости валидации. Следовательно, стоимость генерации тестов и
их качество представляют собой две основные задачи, которые будут рассмот-
рены в следующих главах.
1.2.2. Методы валидации СнК
Методы валидации СнК могут бытьразделены на две категории: формальная
верификация и моделирование. На рис. 1.5 показаны некоторые из широко
используемых методов в этих двух категориях. Далее в этом разделе дается об-
зор этих методов валидации проектирования.
1.2.2.1. Валидация на основе моделирования
Валидация на основе моделирования [17] позволяет обнаружитьошибки про-
ектирования благодаря использованию векторов тестовых последовательно-
стей, состоящих из входных воздействий и ожидаемых выходных результатов
[18—21]. На рис. 1.6 показана схема традиционной валидации на основе мо-
делирования. Валидация состоит из трех основных процедур: 1) генерации
тестовых векторов, 2) моделирования конструкций СнК с использованием тес-
товых векторов, 3) сравнения сгенерированных выходных сигналов с ожидае-
мыми результатами. В процессе валидации тестируемые параметры показыва-
ют, какая частьдизайна не была верифицирована и какие тесты должны быть
добавлены. Для обнаружения различных типов ошибок проектирования на
различных уровнях абстракции дизайна предлагается тестироватьразличные
параметры. Генерация направленных тестов с управляемым тестовым покры-
Рис. 1.5. Методы валидации СнК
Валидация на уровне спецификации
Формальная верификация Подходы на основе моделирования
Проверка
неограниченной модели
Верификация выполнимости
ограниченной модели
Ограниченно-
случайные
тесты
Направленные
тесты
Доказательство
теорем
Верификация
модели
Решение задачи
выполнимости
Случайные
тесты
тием предназначена для активации точки целевого покрытия, что эффективно
сокращает количество тестов по сравнению со случаем применения случайных
тестов. Посредством моделирования эффективностьтестового покрытия ана-
лизируется на предмет того, покрыты ли целевые функции тестами или нет,
таким образом, можно измеритьход валидации. Если найдены пробелы в по-
крытии (т.е. тестирование оказалосьнедостаточным), создаются дополнитель-
ные тесты для их валидации. Если требуется высокая степеньдоверия, мы мо-
жем улучшитьметрику покрытия или использоватьдополнитель ные методы
тестового покрытия. Инженеры-тестировщики могут изменятьобластьи глу-
бину покрытия в течение процесса валидации. Для примера, они могут начать
с простых метрик покрытия на ранней стадии валидации и использовать более
сложные метрики покрытия позже.
Генерация тестов играет важную рольв валидации, управляемой модели-
рованием. Она определяет не только качество тестирования, но также сильно
влияет на время моделирования. Естьтри типа методов генерации тестов:
генерация случайных, ограниченно-случайных и направленных тестов. В теку-
щей производственной практике [22, 23] наиболее широко используются ме-
тоды генерации случайных и ограниченно-случайных тестов, потому что тес-
товые векторы могут бытьполучены автоматически, следовательно, большая
частьошибок дизайна может бытьобнаружена в начале цикла разработки. Тем
не менее, необходимо огромное количество тестов для достижения высокой
степени уверенности в правильности дизайна, поскольку можно легко пропус-
титьсостояния дизайна, в которых наступает отказ (например, состояния кон-
вейера, соотношения тактовых сигналов). По сравнению со случайными мето-
дами тестирования, которые используют миллиарды и триллионы случайных и
псевдослучайных тестов, в традиционном направленном тестировании дизайна
применяется меньше тестов для получения требуемого тестового покрытия
функций, поскольку в данном случае используется информация о структуре
дизайна [24, 25]. Путем применения направленных тестов общая трудоемкость
валидации может бытьумень шена без сокращения целевого тестового покры-
тия. Большинство методов генерации направленных тестов требуют эксперт-
1.2. Валидация на системном уровне: возможности и проблемы 27
Рис. 1.6. Последовательность валидации на основе моделирования
Генерация
тестов
Анализ
тестового
покрытия
Метрики
покрытия
Удовлет-
ворительно
Отчет (ошиб-
ки/тестовое
покрытие)
Выходные
результаты
Сравнение
откликов
с эталоном
Моделирующая
система
Входные
воздействия
Нет
Да
ных знаний валидируемого дизайна (DUV — Design Under Validation). Как
правило, методы генерации направленных тестов являются трудоемкими и
подвержены ошибкам. Из-за неизбежного вмешательства человека невозмож-
на генерация всех направленных тестов для достижения всеобъемлющего це-
левого покрытия в разумные сроки. Эта книга описывает несколько эффек-
тивных методов выполнения автоматической генерации направленных тестов.
Методы моделирования достаточно хорошо работают при валидации слож-
ных конструкций. Легко проверить, активируется ли функциональный сцена-
рий данным тестом при валидации дизайна с многомиллионным количеством
соединений. Тем не менее, достаточно трудно гарантироватьправиль ность
проектирования, используя валидацию на основе моделирования. Например,
чтобы обеспечитьправиль ностьдизайна СнК, требуется проверитьвсе воз-
можные входные стимулы. Однако невозможно сгенерироватьи моделировать
все возможные входные последовательности, так как их число может быть
чрезмерно большим (потенциально бесконечным!). Как правило, используют-
ся триллионы случайных или ограниченно-случайных тестов при моделирова-
нии из-за ограничений сроков выхода на рынок и в силу других причин. Так
как применяются только выборочные входные воздействия (вместо валидации
всех возможных входных последовательностей), валидация не дает уверенно-
сти в правильности дизайна. Нельзя считать, что непротестированный процесс
(функциональность) является корректным или не достижим. Кроме того, су-
ществует нехватка хороших метрик покрытия для количественной оценки сте-
пени доверия и квалификации набора тестов. Поэтому трудно ответитьна во-
прос: «Когда верификация завершена?» из-за сложностей оценки прогресса
верификации и эффективности тестов.