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

• Автор: Камкин, Александр Сергеевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Москва
• Количество страниц: 181 с. : ил.

Содержание
Введение

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 Результаты главы.
Заключение
Список литературы


Методы верификации, используемые на разных уровнях, могут отличаться друг от друга, например, для модулей микропроцессора может использоваться формальная верификация, в то время, как для микропроцессора в целом — тестирование. На рисунке 1. Под тестируемым компонентом здесь понимается либо тестируемый микропроцессор, либо его модуль. В дальнейшем для краткости будем называть имитационное тестирование микропроцессора просто тестированием, хотя под тестированием обычно понимается проверка готовой микросхемы (post-silicon testing). Возможны и другие уровни верификации, например, в компании IBM выделяют блочную верификацию (block-level verification), в которой верификация осуществляется на уровне блоков — небольших модулей или фрагментов модулей, как правило, созданных одним разработчиком (); в компании Intel выделяют верификацию на уровне кластеров — логически связанных модулей микропроцессора (clustcr-Icvcl verification) [j. Рис. Общая схема имитационного тестирования. HVL, Hardware Verification Language)'1, например, на OpcriVera |]-|| или SysfcemVerilog [, |. Работа тестовой системы и тестирумого компонента осуществляется в симуляторе — программном средстве, выполняющем программы на соответствующем языке моделирования. Тестовая система последовательно подает на тестируемый компонент тестовые воздействия (входные сигналы) и осуществляет проверку правильности реакций на них (выходные сигналы). В процессе тестирования тестовой системой создается тестовый отчет, который используется для анализа ошибок и оценки полноты тестирования. В общем случае тестоная система решает три основные задачи: генерация тестовой последовательности, проверка правильности поведения тестируемого компонента, оценка полноты тестирования. С учетом такого разбиения задачи тестирования па подзадачи обычно детализируют архитектуру тестовой системы, различая в ней такие компоненты, как генератор тестовой последоиательности и тестовый оракул (см. Такая архитектура тестовой системы является общеупотребительной как для аппаратного, так и для программного обеспечения |2, |5. Некоторые языки, например, SystemVeriiog, используются как для описания, так и для верификации аппаратуры. Такие языки называют языками описания и иерификации аппаратуры (IIDVLs, Hardware Description and Verification Languages). RB конкретных реализациях данной архитектуры компоненты тестовой системы могут иметь другие названии, например, тестопый оракул часто называют монитором (monitor) или программой проверки (checker). Рис. Детализированная архитектура тестовой системы. РАН. В процессе тестирования проверяется, что тестируемый компонент работает в соответствии с зафиксированными требованиями к его поведению. Для этого на все входы тестируемого компонента в начале каждого такта подаются некоторые сигналы, а в конце каждого такта его выходные сигналы считываются с выходов. Генератор тестовой последовательности создает последовательность входных сигналов, па которой проверяется поведение тестирэ'емого компонента. Он же отвечает за симуляцию работы генератора тактового сигнала, создавая и подавая на соответствующий вход тестируемого компонента периодически изменяющийся сигнал. В начале каждого такта генератор тестовой последовательности передает очередной набор входных сигналов на входы тестируемого компонента и на входы тестового оракула. Генератор тестовой последовательности разрабатывается таким образом, чтобы он реализовывал разные допустимые сценарии работы тестируемого компонента. Тестовый оракул оценивает соответствие поведения тестируемого компонента в ходе тестирования требованиям к нему и выносит вердикт о их соответствии или несоответствии. Входные сигналы, получаемые тестируемым компонентом в начале такта, выходные сигналы, выдаваемые им в конце такта, а также свой вердикт об их корректности оракул записывает в тестовый отчет. Если оракул обнаруживает некорректные результаты работы тестируемого компонента, он, помимо записи и отчет, сигнализирует об этом и генератору тестовой последовательности, чтобы остановить тестирование.