Введение
ГЛАВА 1. Обзор и анализ методов и средств функциональной верификации микропроцессорных вычислительных комплексов 9
1.1. Понятие функциональной верификации и анализ проблемной области 9
1.2. Методы динамической верификации 12
1.3. Методы формальной верификации
1.3.1 Проверка эквивалентности 19
1.3.2 Дедуктивный анализ 20
1.3.3 Проверка модели
1.4. Обзор методов, применяемых при функциональной верификации микропроцессорных вычислительных комплексов 23
1.5. Обзор методов спецификации моделей микропроцессорных вычислительных Комплексов 26
1.6. Обзор технологий построения тестовых систем 30
1.6.1 Технология C++TESK. 31
1.6.2 Универсальная технология верификации
1.7. Анализ текущего состояния 33
1.8. Введение понятия модулей системного обмена 36
1.9. Постановка задачи 39
Глава 2 . Разработка методов и алгоритмов функциональной верификации модулей системного обмена 41
2.1. Разработка концептуальной модели модулей системного обмена 41
2.2. Разработка автоматной модели модулей системного обмена 42
2.3. Разработка методов и алгоритмов динамической верификации модулей системного обмена
2.3.1 Метод генерации воздействий для динамической верификации модулей системного обмена 58
2.3.2 Метод организации устройства проверки для динамической верификации модулей системного обмена. Алгоритм сравнения реакций верифицируемой RTL-модели и эталонной модели 64
2.4. Разработка и адаптация методов и алгоритмов формальной верификации модулей системного обмена 75
2.4.1 Классификация требований к функционированию МСО 77
2.4.2 Разработка семантической модели МСО 78
2.4.3 Адаптация методов редукции числа состояний 81
выводы по главе 82
ГЛАВА 3. Разработка методики комплексной функциональной верификации модулей системного обмена микропроцессорных вычислительных комплексов 84
3.1. Разработка методики и программного обеспечения построения тестовых систем для динамической верификации модулей системного обмена 84
3.1.1 Разработка правил адаптации компонентов моделирующих комплексов для динамической верификации МСО 84
3.1.2 Применение дополнительных механизмов проверки 88
3.1.3 Разработка архитектуры тестовой системы 90
3.1.4 Выбор и обоснование технологии построения тестовых систем 92
3.1.5 Разработка методики построения тестовых систем 97
3.1.6 Разработка средств автоматизации методики построения тестовых систем... 106
3.1.7 Разработка подхода к оценке полноты покрытия 107
3.2. Разработка методики формальной верификации модулей системного обмена 108
3.2.1 Выбор и обоснование способа формализации спецификаций МСО 109
3.2.2 Выбор и обоснование системы автоматизации метода проверки модели ПО
3.2.3 Разработка транслятора диаграмм состояний UML во входной язык верификатора SMV 112
3.3. Разработка методики комплексной функциональной верификации модулей
Системного обмена 117
Выводы по главе 123
Глава 4. Апробация методики комплексной функциональной верификации Модулей системного обмена 125
4.1. Функциональная верификация хост-контроллера МВК «ЭЛЬБРУС-28» 125
4.1.1 Краткое описание хост-контроллера 125
4.1.2 Анализ спецификации хост-контроллера 128
4.1.3 Разработка и формальная верификация автоматной модели хост-контроллера на уровне базовых транзакций 130
4.1.4 Динамическая верификация хост-контроллера 133
4.1.5 Результаты комплексной функциональной верификации хост-контроллера 135
4.2. Результаты применения методики при функциональной верификации модулей системного обмена микропроцессорных вычислительных комплексов 137
Выводы по главе 138
Заключение 140
Список литературы
