|
Содержание
СОДЕРЖАНИЕ
Вступление . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 |