Ви є тут

Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций

Автор: 
Камкин Александр Сергеевич
Тип роботи: 
диссертация кандидата физико-математических наук
Рік: 
2008
Кількість сторінок: 
181
Артикул:
14755
179 грн
Додати в кошик

Вміст

Содержание
Введение
1 Функциональная верификация микропроцессоров
1.1 Тестирование микропроцессоров.
1.1.1 Проверка правильности поведения.
1.1.2 Генерация тестовой последовательности.
1.1.3 Оценка полноты тестирования.
1.2 Формальная верификация микропроцессоров.
1.2.1 Проверка эквивалентности
1.2.2 Проверка моделей
1.2.3 Автоматизированное доказательство теорем
1.3 Тестирование и формальная верификация.
1.4 Тестирование микропроцессоров с конвейерной архитектурой
1.4.1 Методы формальной спецификации
1.4.2 Методы модульного тестирования.
1.4.3 Методы системного тестирования.
1.5 Анализ текущего состояния
1.5.1 Методы формальной спецификации
1.5.2 Методы модульного тестирования.
1.5.3 Методы системного тестирования.
1.6 Уточнение задач диссертационной работы
1.7 Краткое введение в предлагаемый метод.
2 Модульное тестирование микропроцессоров
2.1 Введение в метод модульного тестирования микропроцессоров.
2.2 Формальная спецификация конвейера
2.2.1 Вспомогательные понятия.
2.2.2 Модель конвейера без блокировок.
2.2.3 Спецификация конвейера без блокировок
2.2.4 Отношение соответствия
2.2.5 Модель конвейера с блокировками
2.2.6 Спецификация конвейера с блокировками.
2.2.7 Спецификация конвейера с ресурсами .
2.3 Тестирование на основе контрактных спецификаций конвейера.
2.3.1 Проверка правильности поведения
2.3.2 Определение тестового покрытия
2.3.3 Генерация тестовой последовательности.
2.4 Инструментальная поддержка модульного тестирования.
2.4.1 Технология тестирования ишТЕБК.
2.4.2 Тестирование Уег Поймоделей
2.4.3 Тестирование ЭузЬетСмоделей.
2.4.4 Библиотека Р1РЕ
2.5 Результаты главы.
3 Системное тестирование микропроцессоров
3.1 Введение в метод системного тестирования микропроцессоров
3.2 Основные понятия предлагаемого метода
3.2.1 Тестовый шаблон .
3.2.2 Зависимости между инструкциями.
3.2.3 Тестовые ситуации
3.2.4 Тестовые воздействия.
3.3 Формальная спецификация микропроцессора
3.3.1 Формальная спецификация подсистем
3.3.2 Формальная спецификация типов данных.
3.3.3 Формальная спецификация системы команд.
3.4 Метод генерации тестовых программ.
3.4.1 Схема генерации тестовых программ
3.4.2 Подготовка тестовых воздействий
3.4.3 Параметры управления генерацией
3.5 Инструментальная поддержка системного тестирования.
3.5.1 Генератор тестовых программ i..
3.5.2 Примеры описаний тестов и тестовых программ .
3.5.3 Стладка спецификаций и тестов
3.6 Результаты главы.
4 Опыт практического применения предлагаемого метода
4.1 Тестирование буфера трансляции адресом.
4.1.1 Краткое описание тестируемого модуля
4.1.2 Спецификация и тестирование модуля.
4.1.3 Результаты апробации.
4.1.4 Повторное использование спецификаций и тестов
4.2 Тестирование модуля кэшпамяти второго уровня
4.2.1 Краткое описание тестируемого модуля
4.2.2 Спецификация и тестирование модуля.
4.2.3 Результаты апробации.
4.3 Тестирование подсистемы управления памятью.
4.3.1 Краткое описание тестируемой подсистемы .
4.3.2 Спецификация и тестирования подсистемы
4.3.3 Результаты апробации.
4.4 Тестирование микропроцессора Комдив
4.4.1 Краткое описание тестируемого микропроцессора
4.4.2 Спецификация и тестирование микропроцессора
4.4.3 Результаты апробации.
4.5 Тестирование арифметического сопроцессора Комдив8 .
4.5.1 Описание тестируемого сопроцессора.
4.5.2 Спецификация и тестирование сопроцессора.
4.5.3 Результаты апробации.
4.6 Результаты главы.
Заключение
Список литературы