Динамическая верификация цифровой аппаратуры на основе формальных спецификаций

• Автор: Чупилко, Михаил Михайлович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2012
• Место защиты: Москва
• Количество страниц: 127 с. : ил.

СОДЕРЖАНИЕ
ВВЕДЕНИЕ
ГЛАВА 1 ФУНКЦИОНАЛЬНАЯ ВЕРИФИКАЦИЯ ЦИФРОВОЙ АППАРАТУРЫ
1.1 Формальная верификация
1.2 Динамическая верификация
1.2.1 Общая схема тестирования
1.2.2 Уровень сложности тестируемого компонента
1.2.3 Генерация тестовых воздействий
1.2.4 Проверка реакций тестируемого компонента
1.2.5 Оценка полноты тестирования
1.2.6 Технологии создания тестовых систем
1.2.7 Анализ существующих технологий
1.3 Уточнение задач диссертационной работы
1.4 Краткое введение в предлагаемый метод
ГЛАВА 2 МЕТОД ВЕРИФИКАЦИИ АППАРАТУРЫ
2.1 Уровни абстракции эталонной модели
2.2 Архитектура тестовой системы
2.2.1 Архитектура тестового оракула
2.2.2 Генерация стимулов
2.2.3 Способ оценки полноты покрытия
2.2.4 Применение подхода на разных уровнях абстракции
2.2.5 Формализация работы тестового оракула
2.2.6 Соединение нескольких тестовых систем
2.3 Классификация ошибок в аппаратуре
2.4 Результаты главы
ГЛАВА 3 РЕАЛИЗАЦИЯ МЕТОДА ВЕРИФИКАЦИИ АППАРАТУРЫ
3.1 Средства описания тестовых оракулов
3.1.1 Описание сообщений
3.1.2 Описание моделей интерфейсов
3.1.3 Первичные арбитры реакций
3.1.4 Вторичные арбитры реакций
3.1.5 Создание класса модельного окружения и тестового оракула

3.2 Адаптер
3.2.1 Адаптеры моделей входных и выходных интерфейсов
3.2.2 Создание класса адаптера
3.3 Сценарий тестирования
3.3.1 Сценарные функции
3.3.2 Функция получения текущего состояния
3.4 Реализация функционального покрытия
3.5 Реализация объединения нескольких модулей
3.6 Реализация автоматического построения конечных автоматов
3.7 Результаты главы
ГЛАВА 4 РЕЗУЛЬТАТЫ ПРИМЕНЕНИЯ ПОДХОДА
4.1 Коммутатор данных северного моста
4.2 Системный контроллер прерываний
4.3 Устройство аппаратного поиска по таблице страниц
4.4 Буфер команд
4.5 Опыты по автоматическому построению конечных автоматов
4.6 Результаты верификации модулей
4.7 Результаты главы
ЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ
Введение
Актуальность темы
Современная цифровая аппаратура на основе интегральных схем (ИС) представляет собой сложные устройства, проектирование и производство которых требует больших затрат ресурсов. Непосредственное изготовление ИС происходит с использованием наборов фотошаблонов, которые создаются на основе схемы соединений {net list). Схема соединений получается автоматически путем синтеза из модели, созданной на специализированном языке описания аппаратуры. В настоящее время проектирование моделей устройств осуществляется с помощью языков, называемых языками описания аппаратуры {Hardware Description Language, HDL). Такие модели, основанные на HDL-описаниях, часто называют имитационными, так как они допускают их выполнение в специализированной среде имитационного моделирования - симуляторе.
Цена ошибки в аппаратуре может оказаться очень высокой: известный случай замены микропроцессоров Intel Pentium с ошибкой деления обошелся компании приблизительно в 500 миллионов долларов {Wolfe A. For Intel, it's а case of FPU all over again. EE Times, 1997. №5). Так как исправление ошибок в уже готовых микросхемах невозможно, поиск и нахождение функциональных ошибок проводится на этапе проектирования HDL-описания устройства. Подобного рода деятельность, состоящая в проверке соответствия поведения аппаратуры, задаваемого HDL-описанием, его спецификации, называется верификацией. Верификация обычно требует до 70% от общих трудозатрат на создание всего устройства. Это обусловлено следующими причинами: логической сложностью HDL-описаний и ее постоянным увеличением (высокая степень параллелизма, асинхронность и большие размеры), существенной итеративностью процесса разработки HDL-описаний, требующего постоянной модификации тестов и HDL-описаний,

анализ достигнутого покрытия и генерация тестовых шаблонов», что является основными задачами, решаемыми технологией.
Идеей, лежащей в основе подхода, является использование высокоуровневых диаграмм принятия решений (High level decision diagrams, HLDD) для целей симуляции и проверки достигнутого покрытия, а также расширенные временем диаграммы принятия решений (Temporally extended high level decision diagrams, THLDD) для проверки утверждений.
Диаграммы HLDD [63]—[64] - это способ представления дискретных функции с помощью графов, содержащих в вершинах переменные, которые на данном шаге влияют на значение, возвращаемое функцией, а дуги, соединяющие вершины, символизируют значения, принимаемые этими переменными. Когда все необходимые переходы по графу согласно вектору значений переменных, от которых зависит данная дискретная функция сделаны, мы оказываемся в крайней вершине, содержащей возвращаемое функцией значение.
На рисунке 5 представлен пример IILDD-графа для некоторой функции у, значение которой зависит от переменных Х1-Х4, находящихся в вершинах то-гщ. Если, например, вычислять значение, которое функция принимает при подаче тестового вектора, равного {хьХ2,хз,Х4}={4,2
тО ml m2
Рисунок 5 - Пример высокоуровневой диаграммы принятия решений
В [59] отмечается, что НИОО является удобной моделью представления цифровых схем на разных уровнях абстракции: от очень подробного ИОЕ-описания, до абстрактной поведенческой модели за счет того, что в аппаратуре не бывает других функций, кроме дискретных.