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

• Автор: Стотланд, Ирина Аркадьевна
• Шифр специальности: 05.13.15
• Научная степень: Кандидатская
• Год защиты: 2012
• Место защиты: Москва
• Количество страниц: 225 с. : ил.

ВВЕДЕНИЕ
ГЛАВА 1. ОБЗОР И АНАЛИЗ МЕТОДОВ И СРЕДСТВ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МИКРОПРОЦЕССОРНЫХ ВЫЧИСЛИТЕЛЬНЫХ КОМПЛЕКСОВ.

1.1. ПОНЯТИЕ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ И АНАЛИЗ ПРОБЛЕМНОЙ ОБЛАСТИ

1.2. МЕТОДЫ ДИНАМИЧЕСКОЙ ВЕРИФИКАЦИИ

1.3. Методы формальной верификации

. 3.1 Проверка эквивалентности

1.3.2 Дедуктивны й анализ.

1.3.3 Проверка модели.

1.4. Обзор методов, применяемых при функциональной верификации

МИКРОПРОЦЕССОРНЫХ ВЫЧИСЛИТЕЛЬНЫХ комплексов

1.5. Обзор методов спецификации моделей микропроцессорных вычислительных

комплексов.
1.6. ОБЗОР ТЕХНОЛОГИЙ ПОСТРОНИЯ ТЕСТОВЫХ СИСТЕМ.
. б. 1 Технология СТЕБК
1.6.2 Универсальная технология верификации
1.7. Анализ текущего состояния
1.8. Введение Iюнятия модулей системного обмена.
1.9. Постановка задачи
ГЛАВА 2. РАЗРАБОТКА МЕТОДОВ И АЛГОРИТМОВ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА.
2.1. Разработка концептуальной модели модулей системного обмена.
2.2. Разработка автоматной модели модулей системного обмена.
2.3. Разработка методов и алгоритмов динамической верификации модулей
системного обмена
2.3.1 Метод генерации воздействий для динамической верификации .модулей системного
2.3.2 Метод организации устройства проверки для динамической верификации модулей
системного обмена. Алгоритм сравнения реакций верифицируемой ИТ.модели и эталонной модели
2.4. Разработка и адаптация методов и алгоритмов формальной верификации модулей системного обмена
2.4.1 Классификация требований к функционированию МСО.
2.4.2 Разработка семантической модели МСО.
2.4.3 Адаптация методов редукции числа состояний
Выводы по главе
ГЛАВА 3. РАЗРАБОТКА МЕТОДИКИ КОМПЛЕКСНОЙ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА МИКРОПРОЦЕССОРНЫХ ВЫЧИСЛИТЕЛЬНЫХ КОМПЛЕКСОВ
3.1. Разработка методики и программного обеспечения построения тестовых систем
ДЛЯ ДИНАМИЧЕСКОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА
3.1.1 Разработка правил адаптации компонентов моделирующих комплексов для
динамической верификации МСО.
3.1.2 Применение дополнительных механизмов проверки.
3.1.3 Разработка архитектуры тестовой системы.
3.1.4 Выбор и обоснование технологии построения тестовых систем.
3.1.5 Разработка методики построения тестовых систем
3.1.6 Разработка средств автоматизации методики построения тестовых систем
3.1.7 Разработка подхода к оценке полноты покрытия.
3.2. РАЗРАБОТКА МЕТОДИКИ ФОРМАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА.
3.2.1 Выбор и обоснование способа формализации спецификаций МСО
3.2.2 Выбор и обоснование системы автоматизации метода проверки модели.
3.2.3 Разработка транслятора диаграмм состояний ОМЬ во входной язык
верификатора КМУ
3.3. Разработка методики комплексюй функциональной верификаии модулей
СИСТЕМНОГО ОБМЕНА.1
Выводы по главе
ГЛАВА 4. АПРОБАЦИЯ МЕТОДИКИ КОМПЛЕКСНОЙ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА
4.1. Функциональная верификация хостконтроллера МВК Эльбруса
4.1.1 Краткое описание хостконтроллера
4.1.2 Анализ спецификации хостконтроллера.
4.1.3 Разработка и формальная верификация автоматной модели хостконтроллера на
уровне базовых транзакций.
4.1.4 Динамическая верификация хостконтроллера
4.1.5 Результаты комплексной функциональной верификации хостконтроллера.
4.2. РЕЗУЛЬТАТЫ ПРИМЕНЕНИЯ МЕТОДИКИ ПРИ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА МИКРОПРОЦЕССОРНЫХ ВЫЧИСЛИТЕЛЬНЫХ КОМПЛЕКСОВ
Выводы но главе
ЗАКЛЮЧЕНИЕ
СПИСОК ЛИТЕРАТУРЫ


Выделяют два основных класса метрик тестового покрытия кодовые и функциональные. В их также называют метриками покрытия реализации и метриками покрытия спецификации соответственно. Кодовое покрытие определяет часть кода реализации, которая была выполнена при имитационном тестировании модели. Среди метрик кодового покрытия можно выделить покрытие кода i v, покрытие ветвей v, покрытие выражений ii v, покрытие инструкций v . Как отмечено в стандарте , 0 кодовое покрытие является необходимым, но не достаточным условием завершения процесса верификации, так как кодовое покрытие не связано со спецификацией и часть заложенной в спецификации функциональности может просто отсутствовать в реализации. Функциональное покрытие получают либо на основе кодового покрытия эталонной модели, либо, используя метрики покрытия сценариев и данных при построении тестовых систем класс v. Подробнее данный подход рассмотрен в , , . В Наборе рекомендаций по функциональной верификации виртуальных компонентов V, Vi и СНК, разработанном группой инженеров международной ассоциации ведущих электронных фирм VI i , также представлено разделение метрик функционального покрытия на метрики по входным, выходным, внутренним данным и временным характеристикам. Модель покрытия данных содержит информацию о наборе значений переменных, необходимых для проверки функциональности верифицируемого компонента. Формальная верификация совокупность приемов и методов формального доказательства или опровержения того, что модель системы удовлетворяет заданной формальной спецификации . На основе неформальной спецификации разрабатывается формальная модель системы и набор утверждений, формализующих требования к ее функционированию. Проверка эквивалентности используется для того, чтобы формально доказать, что два различных представления одного и того же компонента являются функционально эквивалентными. Методы проверки эквивалентности широко применяются для доказательства эквивалентности двух представлений системы на разных уровнях абстракции. Для проверки эквивалентности верифицируемые модели представляют в виде двоичных разрешающих диаграмм , i ii i, впервые предложенных Р. Брианом . Проверка эквивалентности двух представлений осуществляется путем применения системы решения задачи выполнимости булевых формул v . Теоретический метод решения задачи проверки эквивалентности применяется в системах автоматизации при верификации микропроцессоров. В работах П. Мишра и Н. Проверка эквивалентности не может обнаружить ошибки, внесенные на ранней стадии проектирования, так как более поздняя модель, как правило, наследует эти ошибки. Таким образом, методы проверки эквивалентности не могут быть использованы автономно для доказательства правильности функционирования системы, что является существенным недостатком данного подхода. Дедукт ивный анализ Дедуктивный аюлиз, основанный на методах автоматизированного доказательства теорем vi, подразумевает применение аксиом и правил вывода для доказательства правильности функционирования системы. Несмотря на многие теоретические ограничения , методы дедуктивного анализа позволяют решить множество сложных, практически значимых задач. Зачастую для верификации применяются интерактивные системы доказательства теорем, которые для своей работы требует участие эксперта. После обнаруженной в микропроцессоре I i ошибки IV , 8 многие компании, разрабатывающие микропроцессоры, стали использовать методы автоматического доказательства теорем для функциональной верификации критичных для системы . Система автоматического доказательства теорем 2, например, использовалась для проверки микропроцессора К5 . Преимущество методов дедуктивного анализа состоит в том, что они могут быть применены к системам с бесконечных числом состояний. Эту задачу можно до определенных пределов автоматизировать. Однако даже в том случае, когда проверяемое свойство действительно выполняется, нельзя наложить никаких ограничений на промежуток времени и объем памяти, необходимый для поиска доказательства, что является недостатком дедуктивного анализа , стр.