Методика комплексной функциональной верификации модулей системного обмена микропроцессорных вычислительных комплексов тема диссертации и автореферата по ВАК РФ 05.13.15, кандидат технических наук Стотланд, Ирина Аркадьевна

• Стотланд, Ирина Аркадьевна
• кандидат технических наук
• 2012

Оглавление диссертации кандидат технических наук Стотланд, Ирина Аркадьевна

ВВЕДЕНИЕ.

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

1.1. понятие фу! жционллы юй верификации и а11ализ проблем! 10й области.

1.2. Методы динамической верификации.

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

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

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

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

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

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

1.6. Обзор технологий построения тестовых систем.

1.6.1 Технология С++ТЕБК.

1.6.2 Универсальная технология верификации.

1.7. Анализ текущего состояния.

1.8. Введение понятия модулей системного обмена.

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 Разработка транслятора диаграмм состояний UML во входной язык верификатора SMV.

3.3. Разработка методики комплексной функциональной верификации модулей системного обмена. выводы по главе.

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

4.1. функциональная верификация хост-контроллера мвк «эльбрус-28».

4.1.1 Краткое описание хост-контроллера.

4.1.2 Анализ спецификации хост-контроллера.

4.1.3 Разработка и формальная верификация автоматной модели хост-контроллера на уровне базовых транзакций.

4.1.4 Динамическая верификация хост-контроллера.

4.1.5 Результаты комплексной функциональной верификации хост-контроллера.

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

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

Актуальность темы

Основными направлениями развития микропроцессоров и вычислительных комплексов на их основе являются увеличение их производительности и расширение функциональных возможностей, что достигается как повышением уровня микроэлектронной технологии, используемой для производства микропроцессоров, так и применением новых архитектурных и структурных вариантов их реализации [21]. Задача расширения применения микропроцессоров и вычислительных комплексов на их основе для решения все более широкого спектра сложных задач не всегда затруднительна из-за недостаточного быстродействия и неудовлетворительных вычислительных возможностей, а, главных образом, из-за ограниченности надежностных характеристик разрабатываемых систем. Постоянное усложнение создаваемых микропроцессорных вычислительных комплексов (МВК) приводит к неравномерному распределению появления и удаления логических ошибок по различных этапам проектирования. Как показано в [6] Дж. Бергероном, 70% ошибок возникает на начальных этапах проектирования, и только на этапе отладки готовой системы удается устранить порядка 70% ранее внесенных ошибок. Значительные усилия прилагаются для изменения отмеченной тенденции путем применения различных методов и средств функциональной верификации.

Одним из основных методов обеспечения функциональной надежности МВК является их верификация на этапе логического проектирования. На каждом этапе маршрута проектирования применяются различные методы и средства верификации, призванные не пропустить неисправности на последующие стадии разработки. Стоимость исправления обнаруженных ошибок увеличивается в десятки и даже сотни раз при переходе от более ранних этапов маршрута проектирования к более поздним. Так, известная ошибка FDIV (ошибка в делении чисел с плавающей запятой) в микропроцессорах Intel Pentium, обнаруженная уже после выпуска 5 микросхемы в серийное производство, привела к замене микропроцессоров, что обошлось компании приблизительно в 475 миллионов долларов [48]. Исходя из вышесказанного, ошибки необходимо выявлять и исправлять еще на этапе логического проектирования системы.

Чтобы убедиться, что система удовлетворяет всем функциональным требованиям, сформулированным в спецификации, применяется функциональная верификация. Задача функциональной верификации — доказать, что разрабатываемое устройство будет работать согласно установленным требованиям (спецификации) [48]. Объектами функциональной верификации МВК являются логические модели уровня регистровых передач (ЯТЬ-модели), а таюке их системные модели и спецификации. Основными направлениями функциональной верификации являются динамическая верификация и формальная верификация. Как методы динамической, так и методы формальной верификации обладают своими преимуществами и недостатками. Автономное применение одного из направлений функциональной верификации грозит снижением уровня качества проверки, в то время как совместное применение независимых методик сопряжено с дополнительными затратами на формализацию спецификаций для разных подходов. Поэтому столь актуальной становится задача разработки методики комплексной верификации, основанной на использовании двух подходов с возможностью повторного использования разрабатываемых моделей и формализованных спецификаций.

Большинство существующих работ по функциональной верификации МВК посвящено исследованию конвейеризированных модулей управляющей логики, в то время как далеко не все функциональные блоки, входящие в состав МВК, имеют конвейеризированную архитектуру. Анализ официальных перечней ошибок современных микропроцессоров, выпущенных в серийное производство, показал, что около 30% ошибок связаны с неверным функционированием систем поддержки когерентности и обмена данными. При этом критичность ошибок в модулях, организующих и 6 поддерживающих взаимодействие в МВК, велика, поэтому актуальной также является задача разработки методики комплексной функциональной верификации МВК, учитывающей функциональные и архитектурные особенности таких модулей.

Объект исследования

Объектом исследования являются модули системного обмена, входящие в состав МВК, и процесс их функциональной верификации.

Цель и задачи исследования

Целью диссертационной работы является разработка методики комплексной функциональной верификации модулей системного обмена МВК, обеспечивающей высокий уровень автоматизации разработки тестовых систем и тестов, сокращающей трудозатраты на модульную функциональную верификацию МВК и качественно улучшающей результаты функциональной верификации, а также учитывающей специфику модулей системного обмена. Для достижения указанной цели в диссертационной работе поставлены и решены следующие основные задачи:

1. Анализ существующих методов и средств функциональной верификации микропроцессоров.

2. Классификация функциональных модулей, входящих в состав МВК, с точки зрения их функциональной верификации. Определение класса модулей системного обмена (МСО), разработка концептуальной модели МСО.

3. Разработка автоматной модели МСО МВК для формального представления МСО на разных уровнях абстракции.

4. Разработка методов, алгоритмов и программного обеспечения для динамической верификации МСО МВК на основе автоматной модели МСО.

5. Разработка и адаптация методов, алгоритмов и программного обеспечения формальной верификации МСО на основе автоматной модели МСО.

6. Разработка методики комплексной функциональной верификации МСО МВК, основанной на разработанных и адаптированных методах и алгоритмах динамической и формальной верификации МСО.

7. Апробация разработанной методики в промышленных проектах при модульной функциональной верификации современных МВК.

Структура работы

Работа состоит из введения, четырех глав, заключения и 8 приложений.

В первой главе проведен обзор и анализ существующих методов и средств функциональной верификации микропроцессоров и вычислительных комплексов на их основе. Описано понятие и объекты функциональной верификации МВК. Рассмотрен маршрут проектирования современных МВК и установлено, что функциональная верификация применяется на трех из семи основных стадий маршрута проектирования МВК. Приведена классификация функциональных модулей МВК и выделен класс модулей системного обмена. В конце главы приводится уточнение основных задач работы.

Во второй главе определена концептуальная трехуровневая модель МСО. Разработана автоматная модель МСО на основе теории расширенных конечных автоматов. На основе данных моделей определены формальные критерии принадлежности функционального модуля МВК к классу МСО. Приведено описание разработанных алгоритма сравнения реакций от верифицируемой ЯТЬ-модели и эталонной модели, методов генерации воздействий и организации устройства проверки для динамической верификации МСО. Разработана семантическая модель МСО для трансляции автоматной модели МСО в структуру Крипке для адаптации метода проверки модели для формальной верификации спецификаций МСО.

В третьей главе на основе разработанных и адаптированных методов и алгоритмов предложены методика построения тестовых систем для динамической верификации МСО и методика формальной верификации, в основе которой лежит трансляция полуформального описания автоматной модели МСО в виде диаграмм состояний иМЬ во входной язык верификатора 8МУ и дальнейшая автоматизированная формальная верификация полученной 8МУ-модели методом проверки модели. В главе также описаны разработанные средства автоматизации динамической и формальной верификации МСО. На основе разработанных методов, алгоритмов и методик разработана методика комплексной функциональной верификации МСО.

В четвертой главе представлено описание и результаты апробации методики при функциональной верификации микропроцессоров «Эльбрус-28» и «Эльбрус-4С+», разрабатываемых в ЗАО «МЦСТ». Основным результатом главы является практическое обоснование эффективности предложенной методики.

Заключение диссертации по теме «Вычислительные машины и системы», Стотланд, Ирина Аркадьевна

Выводы по главе

Результаты апробации методики комплексной функциональной верификации модулей системного обмена показывают ее применимость для сложных промышленным проектов. В главе подробно описан опыт практического применения методики при верификации хост-контроллера МВК «Эльбрус^», который показал эффективность применения методов генерации воздействий и организации устройства проверки, а также использования компонентов моделирующих комплексов в качестве эталонных моделей МСО. В результате, при комплексной функциональной верификации спецификации и реализации хост-контроллера было выявлено

59 ошибок. Около 7% ошибок было обнаружены при формальной верификации спецификации верифицируемых модулей. Данные ошибки крайне сложно обнаружить какими-либо другими способами, но они могут привести к неверному функционированию всего МВК. В процессе динамической верификации хост-контроллера разработаны 169 тестовых сценариев, включающих в себя 135 сценариев на проверку базовых операций хост-контроллера, 13 нагрузочных тестовых сценария и 21 динамический сценарий, имитирующий работу модуля в реальных условиях.

В главе также приведены результаты функциональной верификации других МСО, входящих в состав МВК «Эльбрус-28» и результаты разработки тестовой системы новой версии хост-контроллера МВК «Эльбрус-4С+». Трудозатраты на разработку тестовых систем существенно отличаются друг от друга, так как не во всех случаях была применена система автоматизации ШТЮ, позволяющая сократить до 75% трудозатрат. Кроме того, около 70% тестовых сценариев и эталонной модели может быть повторно использовано при изменении исходной спецификации и ЯТЬ-модели.

Основные полученные научные и практические результаты работы состоят в следующем:

1. Выделен новый класс функциональных модулей МВК — модулей системного обмена. Разработаны концептуальная и автоматная модели МСО, определены критерии принадлежности функционального модуля МВК к классу МСО. Рассмотрены различные типы МСО и определены формальные критерии принадлежности МСО к одному из типов.

2. Разработан новый метод генерации воздействий для динамической верификации МСО на основе автоматной модели МСО, позволяющий инкапсулировать реализации базовых операций МСО и создавать направленные и ограниченно-случайные последовательности воздействий.

3. Предложен алгоритм сравнения последовательностей реакций от верифицируемой ЯТЬ-модели и эталонной модели, на основе которого разработан метод организации устройства проверки. Предложены механизмы дополнительных проверок и правила адаптации компонентов программных моделирующих комплексов МВК в качестве эталонных моделей, что позволяет существенно сократить сроки разработки и отладки эталонных моделей. Предложена технология «ВазеРоЛ» для организации взаимодействия тестовых систем и эталонных программных моделей.

4. Предложена архитектура и методика построения тестовых систем основе разработанных методов, механизмов, алгоритмов и универсальной технологии верификации ЦУМ. Разработано средство автоматизации построения шаблонов тестовых систем «иТЕв», позволяющее сократить трудозатраты на разработку тестовых систем.

5. Разработана семантическая модель МСО и программное обеспечение «иМЬ28МУ» для трансляции автоматной модели МСО в структуру Крипке для формальной верификации спецификаций МСО. Адаптирован метод проверки модели, разработанный Э. Кларком.

6. Предложена методика комплексной функциональной верификации МСО МВК, базирующаяся на разработанных и адаптированных методах и алгоритмах динамической и формальной верификации МСО, соответствующая поставленным в работе целям и задачам.

7. Проведена апробация методики, результаты которой показали ее применимость для сложных промышленных проектов.

Список литературы диссертационного исследования кандидат технических наук Стотланд, Ирина Аркадьевна, 2012 год

1. Агошкова Е. Б., Ахлибининский Б. В. Эволюция понятия системы // Вопросы философии, 1998. № 7. С. 170—179.

2. Белкин В.В., Шаршунов С.Г. Разработка функциональных тестов конвейеризованных процессоров на основе высокоуровневых моделей // Приборы и системы. Управление, контроль, диагностика, 2007. №4. С 22-27.

3. Белкин В.В. Построение функциональных диагностических тестов конвейеризированных RISC-процессоров : автореф. дис. . канд. тех. наук. Владивосток, 2008. 17с.

4. Верификация автоматных программ / Вельдер С. Э., Лукин М. А., Шалыто А. А, Яминов Б. Р.: СПбГУ ИТМО, 2011. 242 с.

5. ГОСТ Р ИСО 9000-2001. Государственный стандарт Российской Федерации. Система менеджмента качества. Основные положения и словарь. ИПК Издательство стандартов, 2001. С. 19.

6. Грушвицкий Р., Михайлов М. Проектирование в условиях временных ограничений: верификация проектов. Электронный ресурс. // Компоненты и технологии, 2008. №3. URL: http://www.kit-e.ru (дата обращения 05.09.2012).

7. Грушвицкий Р., Михайлов М. Проектирование в условиях временных ограничений: верификация проектов (продолжение). // Компоненты и технологии, 2008. №5. Электронный ресурс. URL: http://www.kit-e.ru (дата обращения 05.09.2012).

8. Гурин K.JI, Мешков А.Н., Сергин A.B., Якушева М.А. Развитие модели подсистемы памяти вычислительных комплексов серии «Эльбрус» // Вопросы радиоэлектроники, серия ЭВТ, Выпуск 3, 2010, С. 62-70.

9. Деменкова Т.А., Стотланд И.А. Методика проектирования логической модели цифрового устройства. 58 НТК МИРЭА. Информационные технологии и системы. Вычислительная техника. Сб. трудов. 4.1. М.: МИРЭА, 2009.С.32-38.

10. Деменкова Т.А., Певцов Е.Ф., Стотланд И.А. Методика функциональной верификации цифровых устройств // Научно-технический журнал «Электронная техника». Серия 2. Полупроводниковые приборы. Выпуск 2(225). -М.: «ФГУП НПП «Пульсар», 2011. С.16-23.

11. Камкин А., Чупилко М. Обзор современных технологий имитационной верификации аппаратуры. // Программирование, 20011. № 3. С. 42^49.

12. Камкин A.C. Использование контрактных спецификаций для автоматизации функционального тестирования моделей аппаратного обеспечения // Труды института системного программирования РАН, 2007. Т. 13. Ч. 1. С. 123-142.

13. Камкин A.C., Чупилко М.М. Механизмы поддержки функционального тестирования моделей аппаратуры на разных уровнях абстракции // Труды ИСП РАН, т. 20, М., 2011, ISSN 2079-8156. с. 143-160.

14. Камкин A.C. Метод автоматизации имитационного тестирования микропроцессоров с конвейерной архитектурой на основе формальных спецификаций: дис. . канд. ф-м. наук. М., 2009. 181 с.

15. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.

16. Кларк Э.М., ГрамбергО., ПеледД. Верификация моделей программ: Model Checking. Пер. с англ. / Под ред. Р. Смелянского. М.: МЦНМО, 2002.416 с.

17. Мешков А.Н. Реализация программного комплекса, моделирующего многопроцессорные ВК с архитектурой SPARC V9 // Вопросы радиоэлектроники, серия ЭВТ, 2009. Вып. 3. С. 79-89.

18. Петров И.А. Шерстнёв А.Е. Реализация справочника для аппаратной поддержки когерентности в вычислительном комплексе на базе микропроцессора «Эльбрус-28». -Вопросы радиоэлектроник. -2011. -Выпуск 3. С. 120-130.

19. Средство разработки тестовых систем C++TESK. Электронный ресурс. URL: http://hardware.ispras.ru/HHCTpyMeHTCPPTESK (дата обращения).

20. Стешенко В. Проектирование СБИС. Стили и этапы проекта Электронный ресурс. // Компоненты и технологии, 2003. № 4. URL: http://www.compitech.ru/ (дата обращения 05.09.2012).

21. Стотланд И.А. Метод динамической верификации модулей системного обмена микропроцессорных вычислительных комплексов. // Научно-технический вестник Поволжья, 2012. №4. Казань: Научно-технический вестник Поволжья. С.191-196.

22. Стотланд И.А. Методика комплексной верификации модулеймикропроцессорных систем.// Современные информационные технологии в управлении и образовании: Сб. научн. трудов. В 3-х ч.Ч.2 -М.: ООО «Издательство «Проспект», 2012. С.76-82.

23. Стотланд И.А. Этапы проектирования блока последовательного интерфейса в объеме ПЛИС, методы его диагностики и отладки. Современные информационные технологии в управлении и образовании. Сб. научн. тр.- М.: ФГУП НИИ «ВОСХОД», МИРЭА, 2009.С.118-126.

24. Стотланд И.А., Оленин A.A. Транслятор диаграмм состояний UML во входной язык верификатора SMV. Документ о регистрации программной системы в отраслевом фонде алгоритмов и программ РФ. Инвентарный номер ВНТИЦ 502001250300.

25. СтотландИ.А. Методика модульной верификации микропроцессоров на основе высокоуровневых тестовых систем // Современные информационные технологии в управлении и образовании: Сб. научн. трудов. 4.2. М.: ООО «Издательство «Проспект», 2011. С. 120-126.

26. Стотланд И.А., Деменкова Т.А. Об одном подходе к разработке тестовых систем. // Теоретические вопросы вычислительной техники и программного обеспечения: Межвуз. сб. научн. тр. В 2-х т. Т.2. М.: МИРЭА, 2011. С.102-109.

27. Сызько Э.В. Хост-контроллер ВК «Эльбрус-28». ЗАО «МЦСТ», 2011.

28. Таненбаум Э. Архитектура компьютеров. СПб.: Питер, 2007. 848 с.

29. Хопкрофт Д., Мотвани Р., Ульман Дж. Введение в теорию автоматов, языков и.вычислений. М.: Издательский дом "Вильяме", 2002. 528 с.

30. Чупилко М.М. Динамическая верификация цифровой аппаратуры на основе формальных спецификаций: автореф. дис. . канд. ф-м. наук. М., 2012. 24 с.

31. Чупилко М.М. Разработка тестовых систем для многомодульных моделей аппаратуры. // Программирование, 2012. № 1. С. 47-58.

32. A top-down methodology for validation of microprocessors / Mishra P., DuttN., Krishnamurthy N., AbadirM.S. // IEEE Design & Test, 2004. Vol. 21. No 2. P. 122-131.

33. Accellera. Электронный ресурс. URL: http://www.accellera.org/ (дата обращения 05.09.2012).

34. AVM tutorial. Электронный ресурс. URL: http://www.asicguru.com/methodologies/avm-tutorial (дата обращения 05.09.2012)

35. BaerJ.L. Microprocessor architecture. From simple pipelines to chip multiprocessors. NY: Cambridge University Press, 2010. 383p.

36. Barret G., Mclsaac A. Model Checking in a Microprocessor Design Project // Proc. of 9th International Conference on Computer Aided Verification, 1997. pp. 214-225.

37. Bentley R.M. Validating the Pentium 4 Microprocessor // Proc. of the Int. Conference on Dependable Systems and Networks, 2001. P. 493-498.

38. Bergeron J. Writing testbenches: functional verification of HDL models. Boston: Kluwer Academic Publishers, 2003.

39. Bryant R.E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986. pp. 677-691.

40. Cai L., Gajski D. Transaction level modeling: an overview. // Proc. of CODES+ISSS 2003: The International Conference on Hardware-Software Codesign and System Synthesis, 2003. P. 19-24.

41. Chen J.S. Applying CRV to Microprocessor Verification. Электронный ресурс. URL: http://www.synopsys.com/services/pages/technicalpapers.aspx (дата обращения 05.09.2012)

42. Chupilko M., Kamkin A. Developing cycle-accurate contract specifications for synchronous parallel-pipeline hardware: application to verification // Proc. of ВЕС 2010: The 12th Biennial Baltic Electronics Conference, 2010. P. 185188.

43. Clarke E. M., Emerson E. A., Sistla A. P. Futomatic verification of finite-state146concurrent systems using temporal logic specifications: a practical approach // Proc. of 10th ACM Symp. On Principles of Programming Languages, 1983.

44. Clarke E., Grumberg O., Long O. Model checking and abstraction // ACM Transaction on Programming Languages and Systems, 1994. Vol. 16. No 5. P. 1512-1542.

45. Clarke E., Grumberg O., Peled D. Model checking. The MIT Press, 1999.

46. Clarke E.M., Heinle W. Modular Translation of Statecharts to SMV. // School of Computer Science. Carnegie Mellon University. Pittsburgh, PA 1513, August 3, 2000 -38p.

47. Drechsler R. Advanced formal verification. Kluwer Academic Publishers, 2004.

48. Formal verification of iterative algorithms in microprocessors / Aagaard M.D., Jones R.B., Kaivola R., Kohatsu K.R., Seger C.-J.H. // Proc. of Design Automation Conference, 2000. P. 201-206.

49. Foster H., Krolnic A., Lacey D. Assertion-Based Verification, 2nd ed. Boston: Kluwer Academic Publishers, 2003.

50. Functional Verification Semiconductor Reuse Standard V3.2. Freescale Semiconductor. 2005.

51. Ho R. Validation tools for complex digital designs. PhD thesis, Stanford University, 1996.

52. IEEE Standard for Property Specification Language (PSL). IEEE Std 13642001.1850-2010.

53. IEEE Standard for the Functional Verification Language 'e'. IEEE Std 16472006.

54. IEEE Standard System C Language Reference Manual. IEEE Std 1666-2005.

55. IEEE Standard SystemVerilog Unified Hardware Design, Specification and147

56. Verification Language. IEEE Std 1800-2009.

57. IEEE Standard Verilog Hardware Description Language. IEEE Std 13642001.

58. IEEE Standard VHDL Language Reference Manual. IEEE Std 1076-2008.

59. Intel® Core™ i7-900 Desktop Processor Extreme Edition Series and Intel® Core™ 17-900 Desktop Processor Series. Specification Update. May 2011. Электронный ресурс.

60. URL: ftp://download.intel.com/design/processor/specupdt/320836.pdf (дата обращения 05.09.2012)

61. Intel® Core™ 2 Duo Processor E8000 and E7000 Series. Specification Update. December 2010. Электронный ресурс. URL: ftp://download.intel.com/design/processor/specupdt/ 318733.pdf (дата обращения 05.09.2012)

62. Jiang Y, Qiu Z. S2N: Model Transformation from SPIN to NuSMV // Model Checking Software. Lecture Notes in Computer Science, 2012. Vol. 7385. P. 255-260.

63. Jonson N. A Method Is Not A Methodology. Электронный ресурс. URL: http://www.agilesoc.com/articles/a-method-is-not-a-methodology/ (дата обращения 05.09.2012).

64. Kaivola R., Narasimhan N. Formal verification of the Pentium4 floating-point multiplier // Proc. of Design, Automation and Test in Europe Conference, 2002. P. 20-27.

65. Kamkin A. Coverage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications // Proc. of EWDTS 2008: The 6th East-West Design & Test Symposium, 2008. P. 84-87.

66. Kamkin A. Coverage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications // Proc. of EWDTS 2008: The 6th East-West Design & Test Symposium, 2008. P. 84-87.

67. Lam W. Hardware design verification: simulation and formal method-based approaches. New Jersey: Prentice Hall, 2005.

68. Lungu A., Sorin D.J. Verification-aware microprocessor design // Proc. of IEEE 16th International Conference on Parallel Architecture and Compilation Techniques, 2007. P.83-93.

69. Mishra P. A top-down methodology for validation of microprocessors // IEEE Design & Test, 2004. Vol. 21. No 2. P. 122-131.

70. Mishra P., DuttN. A methodology for validation of microprocessors using equivalence checking // Proc. of Microprocessor Test and Verification: Common Challenges and Solutions, 2003. P. 83-88.

71. Mishra P., DuttN. Functional validation of programmable architectures // Proc. of Digital System Design, 2004. P. 12-19.

72. Mishra P., Dutt, N. Automatic functional test program generation for pipelined processors using model checking // Proc. of High-Level Design Validation and Test Workshop, 2002. P. 99-103.

73. ModelSim® User's Manual. Software Version 6.10b, 2012. Электронный ресурс. URL: http://model.com/ (дата обращения).

74. Moore J.S, Lynch T.W., Kaufmann M. A mechanically checked proof of the AMD5K86™ floating-point division program // Computers, IEEE Transactions, 1998. Vol. 47. No 9. P. 913-926.

75. Namjoshi K.S., Kurshan R. P. Syntactic Program Transformations for Automatic Abstraction // Proc. of the 12th International Conference on Computer Aided Verification, 2000. P. 435-449.

76. NuSMV User Manual. Электронный ресурс. URL: http://nusmv.fbk.eu/NuSMV/userman/index-v2.html (дата обращения 05.09.2012).

77. NuSMV: a new symbolic model checker. Электронный ресурс. URL: http://nusmv.fbk.eu/ (дата обращения)

78. OMG Unified Modeling Language (OMG UML), Superstructure. Version 2.3. Электронный ресурс. Режим доступа: http://www.omg.org (дата обращения 05.09.2012)

79. Open Verification library. Электронный ресурс.149

80. URL: http://www.eda-stds.org/ovl/ (дата обращения 05.09.2012)

81. Peng Н. Improving compositional verification through environment synthesis and syntatic model reduction. PhD thesis. Concordia University, Monreal, 2002.

82. Piziali A. Functional Verification Coverage Measurement And Analysis. Kluwer Academic Publishers, 2004.

83. Pnueli A. The temporal logic of program // Proc. of the 18th Anny. Symp. On Foundation of Computer Science, 1977.

84. Price D. Pentium FDIV flaw-lessons learned // IEEE Micro, 1995. Vol. 15. No 2. P. 86.

85. R, Kurshan. Computer-aided verification of coordinating processes. NJ: Princeton Univerisity Press, 1994.

86. Reshadi, M., Mishra, P., Dutt N., Hybrid Compiled Simulation: An Efficient Tehnique for Instruction-Set Architecture Simulation . // ACM Transactions on Embedded Computer Systems, 2009. P. 8(3): 1-27.

87. Revision Guide for AMDAthlon™64 and AMD Opteron™ Processors. Электронный ресурс. URL: http://support.amd.com/us/Processor/ (дата обращения 05.09.2012)

88. Spear С. SystemVerilog for Verification. New York: Springer, 2006.

89. SPIN. Электронный ресурс. URL: http://spinroot.com/ (дата обращения)

90. The SMV System. Электронный ресурс. URL:http://www.cs.cmu.edu/~modelcheck/smv.html (дата обращения)

91. TLM-2.0.1. Электронный ресурс. URL: http://www.accellera.org/ (дата обращения 05.09.2012).

92. UVM/OVM Verification Methodology. Электронный ресурс. URL: http://verificationacademy.com/ (дата обращения 05.09.2012)

93. Van Langenhole S. Towards to correctness of Software Behavior in UML: A Model Checking Approach based on Slicing. PhD thesis. UGent, 2006.

94. Vasudevan S., ViswanathV., Abraham J.A. Efficient Microprocessor Verification using Antecedent Conditioned Slicing // Proc. of VLSI Design, 2007. P. 43-49

95. VCS®/VCSi™ User Guide. Version E-2011.03. March 2011 Электронный ресурс. URL: https://solvnet.synopsys.com (дата обращения 05.09.2012)

96. Verifying hardware in its software context / Kurshan R., Levin V., Minea M., Peled D., Yenigan H. // Proc. of IEEE/ACM international conference on Computer-aided design, 1997. P. 742-749.

97. VMM central. Электронный ресурс. URL: www.vmmcentral.org (дата обращения 05.09.2012 )

98. Wiemann A. Standardized functional verification. San Carlos: Springer Science, 2007.

99. Wile B, Goss J, Roesner W. Comprehensive functional verification the complete industry cycle. Morgan Kaufmann Publishers, 2005.

100. Wolfe A. For Intel, it's a case of FPU all over again // Electronic Engineering Times, 1997. No 4. P. 43.

101. Пример генерации воздействий на уровне регистровых передачи уровне транзакций

102. ADDR WRITESTB DATAWR8:0. DATARD[8:0] DATASIZE[2:0] SELLINK[1:0]1. BIG ENDIANi1. TRANS

103. Уровень интерфейсных сигналов0)acOO