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

• Камкин, Александр Сергеевич
• кандидат физико-математических наук
• 2008

Оглавление диссертации кандидат физико-математических наук Камкин, Александр Сергеевич

Введение

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 Технология тестирования UniTESK.

2.4.2 Тестирование Verilog-моделей

2.4.3 Тестирование SystemC-моделей.

2.4.4 Библиотека PIPE.

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 Генератор тестовых программ MicroTESK.

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 Тестирование микропроцессора Комдив64.

4.4.1 Краткое описание тестируемого микропроцессора.

4.4.2 Спецификация и тестирование микропроцессора.

4.4.3 Результаты апробации.

4.5 Тестирование арифметического сопроцессора Комдив

4.5.1 Описание тестируемого сопроцессора.

4.5.2 Спецификация и тестирование сопроцессора.

4.5.3 Результаты апробации.

4.6 Результаты главы.

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

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

Современный мир не мыслим без огромного разнообразия электронных устройств. Мобильные телефоны, цифровые фотокамеры и переносные компьютеры давно стали неотъемлемыми атрибутами жизни многих людей. Специальные устройства управляют работой бытовой техиики, контролируют бортовые системы самолетов н космических спутников, регулируют медицинские системы жизнеобеспечения. В основе практически всех этих систем лежат микропроцессоры — программно-унравляемые устройства, предназначенные для решения задач цифровой обработки данных.

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

На формирование высоких требований к надежности микропроцессоров большое влияние оказывает также следующая особенность полупроводниковой аппаратуры. В отличие от программного обеспечения, в котором исправление ошибки стоит сравнительно дешево, ошибка в микросхеме, обнаруженная несвоевременно, может потребовать перевыпуск и замену продукции, а это сопряжено с очень высокими затратами. Так, известная ошибка в реализации инструкции FDIV микропроцессора Pentium1 [15], заключающаяся в неправильном делении некоторых чисел с плавающей точкой, обошлась компании Intel почти в 475 млн. долларов [16].

В условиях рыночной конкуренции, а конкуренция на рынке микропроцессоров существует [17], важно найти компромисс между многими факторами, включая затраты на разработку и сроки выпуска продукта на рынок. Конкурентоспособный

1 Pentium — торговая марка нескольких поколений микропроцессоров семейства х86, выпускаемых компанией Intel с 22 марта 1993 г. микропроцессор должен отвечать запросам пользователей и, прежде всего, быть надежным. При этом важно не затягивать процессы разработки и выпустить микропроцессор на рынок своевременно, пока он не потерял актуальность и на него имеется спрос.

Основным методом обеспечения надежности микропроцессоров, как и других технических систем, является тестирование. Как правило, тестирование осуществляется не для готовой микросхемы, а для проектной модели, разработанной на специальном языке описания аппаратуры (HDL, Hardware Description Language). Такое тестирование называется имитационным (simulation-based verification)2. По различным данным, тестирование микропроцессоров составляет 50-80% от общего объема трудозатрат на их разработку. Развивающиеся методы тестирования, с одной стороны, нацелены на повышение надежности производимых микропроцессоров, с другой, — на сокращение длительности цикла разработки.

Большинство микропроцессоров, разрабатываемых в настоящее время, имеют конвейерную архитектуру. В общих словах это означает, что параллельно, в один момент времени микропроцессор может обрабатывать сразу несколько инструкций [18[. Выполнение инструкций разбивается на несколько стадий, при этом разные стадии разных инструкций могут выполняться параллельно. Часто в конвейерных микропроцессорах применяются специальные механизмы, направленные на повышение производительности: кэширование, предсказание переходов, спекулятивное выполнение и многие другие. Все это делает тестирование микропроцессоров с конвейерной архитектурой невероятно сложной задачей, которую невозможно решить без применения методов автоматизации тестирования [19].

Анализ ошибок в микропроцессоре MIPS R4000 PC/SC (ревизия 2.2) [20], проведенный в работе [19], говорит, что большинство ошибок (93.5%) связаны с управляющей логикой конвейера3 (см. таблицу 1), причем для обнаружения большей части таких ошибок должны одновременно выполняться несколько условий. Например, одна из ошибок микропроцессора проявлялась только в следующей ситуации (см. пункты 4 и 14 списка ошибок [20]):

• Инструкция загрузки данных в регистр вызывает промах в кэше данных.

• За ней через одну инструкцию NOP4 следует инструкция безусловного перехода

2В дальнейшем для краткости называть имитационное тестирование просто тестированием.

3Управляющей логикой конвейера или просто управляющей логикой называется внутренняя функциональность микропроцессора, отвечающая за планирование и организацию выполнения инструкций. aNOP или NOOP (No Operation) — специальная инструкция микропроцессора, которая не производит никаких действий и обычно используется для временных задержек и выравнивания памяти.

Таблица 1: Статистика ошибок MIPS R4000 PC/SC.

Класс ошибок Число ошибок Процент ошибок

Ошибки обработки данных 3 6.5%

Ошибки в управляющей логике (одно услопие) 17 37.0%

Ошибки в управляющей логике (несколько условий) 26 56.5%

Всего ошибок 40 100,0% по адресу, содержащемуся в загруженном регистре.

• Инструкция перехода — последняя инструкция на странице виртуальной памяти.

• Номер следующей страницы не содержится в буфере трансляции адресов (TLB, Translation Lookaside Buffer).

Приведенный выше анализ ошибок относится к середине 1990-ых гг., но следует отметить, что ошибки в управляющей логике и по сей день являются одиими из самых сложных для обнаружения. Например, список ошибок, датируемый 2006 г., широко используемого в аэрокосмической промышленности микропроцессора TSC695F компании Atmel с архитектурой SPARC v75, включает ошибку (одну из трех), связанную с работой конвейера (см. пункт 3 списка ошибок [21]).

Для большей эффективности обнаружения ошибок и упрощения их локализации тестирование микропроцессора включает в себя тестирование его модулей по отдельности. Для определения правильности выдаваемых модулем результатов используется не техническое задание на микропроцессор в целом, а проектные документы, описывающие функции именно этого модуля. Таким образом, тестирование микропроцессора обычно осуществляется на двух уровнях: модульном (unit-level) и системном (core-level).

В последнее время определенный прогресс в автоматизации модульного и системного тестирования микропроцессоров достигнут в исследованиях в области тестирования на основе формальных спецификаций (specification-based testing, model-based testing). Основная идея этого направления заключается в том, что в процесс разработки тестов включаются формальные спецификации тестируемого компонента и формальные модели тестов. Спецификации и модели используются для автоматической проверки правильности поведения, автоматической генерации тестовых последовательностей и оценки полноты тестирования. Их

5SPARC (Scalable Processor Architecture) — архитектура RISC-микропроцессоров, первоначально разработанная в 1985 г. компанией Sun Microsystems. использование позволяет сократить трудоемкость разработки тестов и повысить "глубину" тестирования.

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

Одна из причин, по которой методы на основе формальных спецификаций не достаточно эффективно применяются в промышленных проектах, состоит в наличии двух независимых описаний: формальной спецификации, которая используется для оценки правильности поведения микропроцессора или его модуля, и модели теста, используемой для генерации тестовых последовательностей и оценки полноты тестирования. Другая причина заключается в неразвитых средствах формальной спецификации микропроцессоров с конвейерной архитектурой, что не позволяет достичь высокого уровня автоматизации тестирования. Представляется перспективным разработать метод формальной спецификации конвейера и метод автоматизации тестирования на его основе спецификаций предлагаемого вида, который был бы лишен указанных недостатков.

Цель и задачи работы

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

• Провести анализ существующих методов автоматизации тестирования микропроцессоров с конвейерной архитектурой.

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

• Провести апробацию разработанных методов в промышленных проектах.

Основные результаты работы

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

• разработан метод формальной спецификации модулей микропроцессоров на основе пред- и постусловий стадий выполнения операций, названный контрактной спецификацией конвейера;

• разработан метод неизбыточиого описания тестового покрытия с помощью тестовых ситуаций и зависимостей;

• разработан метод генерации тестовой последовательности на основе обобщенной автоматной модели, построенной по формальной спецификации модуля и описанию тестового покрытия;

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

• реализованы инструменты, поддерживающие разработанные методы.

Научная новизна работы

Научной новизной обладают следующие результаты работы:

• Метод формальной спецификации модулей микропроцессоров на основе пред- и постусловий стадий выполнения операций.

• Метод неизбыточного описания тестового покрытия с помощью тестовых ситуаций и зависимостей.

• Метод генерации тестовой последовательности на основе обобщенной автоматной модели конвейера, построенной по формальной спецификации модуля и описанию тестового покрытия.

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

Практическая значимость

Практическая значимость работы подтверждается результатами применения предложенных методов для тестирования отдельных модулей и подсистем микропроцессора Комдив64-СМП, системного тестирования микропроцессора Комдив64 и системного тестирования арифметического сопроцессора Комдив128, разрабатываемых в НИИ системных исследований РАН.

Результаты работы могут быть использованы в исследованиях, которые ведутся в Институте системного программирования РАН, Московском государственном институте электроники и математики, НИИ системных исследований РАН, Институте точной механики и вычислительной техники им. С.А. Лебедева РАН, Институте проблем информатики РАН и других научных и промышленных организациях.

Доклады и публикации

Основные положения работы докладывались на следующих конференциях и семинарах:

• Научной конференции "Тихоновские чтения", проводимой на факультете ВМиК МГУ им М.В. Ломоносова (г. Москва, 2005 г.);

• Международном симпозиуме по усиливающим приложениям формальных методов, верификации и валидации (ISoLA: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, г. Пафос, 2006 г.);

• Первом весеннем коллоквиуме молодых исследователей в области программной инженерии (SYRCoSE: Spring Young Researchers Colloquium on Software Engineering, г. Москва, 2007 г.);

• Международном симпозиуме "Восток-Запад: проектирование и тестирование" (EWDTS: East-West Design & Test Symposium, г. Ереван, 2007 г. и г. Львов, 2008 г.);

• Форуме аспирантов, проводимом в рамках международной конференции "Проектирование, автоматизация и тестирование в Европе" (DATE: Design, Automation & Test in Europe, г. Мюнхен, 2008 г.);

• Семинарах Института системного программирования РАН (г. Москва, 20072008 гг.);

• Семинаре НИИ системных исследований РАН (г. Москва, 2008 г.);

По теме диссертации автором опубликованы работы [1]-[14] (из них 1 в изданиях но перечню ВАК), полно отражающие основные результаты диссертации.

Структура и объем диссертации

Работа состоит из введения, четырех глав, заключения и списка литературы (109 наименований). Основной текст диссертации (без приложений и списка литературы) занимает 172 страницы.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Камкин, Александр Сергеевич

Заключение

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

• Разработан метод формальной спецификации модулей микропроцессоров на основе пред- и постусловий стадий выполнения операций, названный контрактной спецификацией конвейера. Формальные спецификации предлагаемого вида могут использоваться для автоматизации проверки правильности поведения конвейерных модулей, на их основе можно определять тестовое покрытие и оценивать полноту тестирования. Разработанный метод позволяет строить формальные спецификации для модулей со сложной управляющей логикой, которая допускает блокировки конвейера.

• Разработан метод неизбыточного описания тестового покрытия с помощью тестовых ситуаций и зависимостей, который позволяет декомпозировать сложную структуру целей тестирования на набор относительно простых описаний, определяемых для отдельных операций или пар операций. Разработанный метод позволяет сократить трудоемкость разработки тестов и увеличить эффективность их поддержки.

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

• Разработан метод генерации тестовых программ на основе формальных спецификаций системы команд микропроцессора и описания тестового покрытия, состоящий в целенаправленном переборе всевозможных сочетаний тестовых ситуаций и зависимостей для последовательностей инструкций ограниченной длины и использовании дополнительных эвристик для сокращения размера тестов. Метод позволяет генерировать тестовые программы со встроенными проверками, что делает возможным их использование для проверки готовых микросхем.

• Реализованы инструменты, поддерживающие предложенные методы.

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

Благодарности. Автор выражает благодарность А.С. Косачеву и В.В. Кулямину за ценные замечания, которые способствовали улучшению качества работы. Особую благодарность автор выражает своим коллегам по Институту, которые вместе с ним участвовали в апробации предложенных методов: Д. Воробьеву, Я. Губенко, К. Козлову, А. Проценко и М. Чупилко, а также партнерам из НИИ системных исследований РАН, в тесном взаимодействии с которыми эта апробация осуществлялась.

Список литературы диссертационного исследования кандидат физико-математических наук Камкин, Александр Сергеевич, 2008 год

1. Иванников В.П., Камкин А.С., Косачев А.С., Кулямин В.В., Петренко А.К. Использование контрактных спецификаций для представления требований и (функционального тестирования моделей аппаратуры // Программирование, К- 5, 2007. С. 47-61.

2. Иванников В.П., Камкин А.С., Кулямин В.В., Петренко А.К. Применение технологии UniTESK для функционального тестирования моделей аппаратного обеспечения. Препринт № 8. М.: Институт системного программирования РАН, 2005. 26 с.

3. Камкин А.С. Тестирование в условиях неполной информации. Подход к разработке спецификаций и генерации тестов // Труды Института системного программирования РАН, т. 10, 2006. С. 143-166.

4. Kamkin A. The UniTESK Approach to Specification-Based Validation of Hardware Designs // ISoLA 2006: The 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, 2006. P. 52-58.

5. Камкин А.С. Использование ф>ормальных спецификаций для функционального тестирования модулей микропроцессоров / / Тезисы конференции "Микроэлектроника и информатика 2007", 2007. С. 188.

6. Kamkin A. Contract Specification of Pipelined Designs: Application to Testbench Automation // SYRCoSE 2007: The 1st Spring Young Researchers Colloquium on Software Engineering, v. 2. 2007. P. 7-13.

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

8. Kamkin A. Testbench Automation for Pipelined Designs Based on Contract Specifications // EWDTS 2007: The 5th East-West Design & Test Symposium, 2007. P. 348-353.

9. Камкин А.С., Чупилко M.M. Тестирование модулей арифметики над числами с плавающей точкой микропроцессоров на соответствие стандарту IEEE 754 // Труды Института системного программирования РАН, т. 14, ч. 2. 2008. С. 7-22.

10. Камкин А.С. Генерация тестовых программ для микропроцессоров // Труды Института системного программирования РАН, т. 14, ч. 2. 2008. С. 23-63.

11. Kamkin А. С overage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications // EWDTS 2008: The 6th East-West Design & Test Symposium, 2008. P. 84-87.

12. Камкин А.С. Комбинаторная генерация тестовых программ для, микропроцессоров на основе моделей. Препринт № 21. М.: ИСП РАН, 2008. 18 с.

13. Statistical Analysis of Floating Point Flaw in the Pentium Processor. Intel Corporation, November 1994. (http://www.intel.com/support/processors/pentium/fdiv/wp/)

14. Beizer B. The Pentium Bug — An Industry Watershed // Testing Techniques Newsletter, TTN Online Edition, September 1995.

15. Дудкин А. Борьба противоположностей, или Микропроцессоры 2004 II Экспресс-Электроника, №3, 2004.http://www.citforum.ru/hardware/microcon/cpu2004/)

16. Patterson D., Hennesy J. Computer Organization and Design: The Hardware/Software Interface. 3rd Edition. The Morgan Kaufmann Series in Computer Architecture and Design, 2005. 621 p.

17. Ho R.C., Yang C.H., Horowitz M.A., Dill D.L. Architecture Validation for Processors II ISCA 1995: International Symposium on Computer Architecture, 1995. P. 404-413.

18. MIPS R4000PC/SC Errata, Processor Revision 2.2 and 3.0. MIPS Technologies Inc., May 10, 1994.

19. TSC695 Errata Sheet. Atmel Corporation, July, 2006.

20. IEEE Standard Hardware Description Language Based on the Verilog Hardware Description Language. IEEE Std 1364-1995.

21. IEEE Standard VHDL Language Reference Manual. IEEE Std 1076-1987.

22. IEEE Standard SystemC Language Reference Manual. IEEE Std 1666-2005.25. http://www.systemc.org — сайт, посвященный языку SystemC.

23. Bentley B. Validating the Intel Pentium 4 Microprocessor // DAC 2001: Design Automation Conference, 2001. P. 244-248.

24. OpenVera Language Reference Manual: Assertions. Version 1.4.1, 2004.

25. OpenVera Language Reference Manual: Testbench. Version 1.4.3, 2005.30. http://www.open-vera.com — сайт, посвященный языку OpenVera.

26. IEEE Standard SystemVerilog Language Reference Manual. IEEE Std 1800-2005.32. http://www.systemverilog.org — сайт, посвященный языку SystemVerilog.

27. Но R. Validation Tools for Complex Digital Designs. PhD Thesis, 1996. 113 p.36. http://www.eda.org/ovl/ — страница, посвященная библиотеке OVL.

28. Property Specification Language Reference Manual. Version 1.1, June 9, 2004

29. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Использование конечных автоматов для тестирования программ // Программирование, 2000, №2. С. 12-28

30. Бурдонов И.Б., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай // Программирование,2003, №5, С. 11-30.

31. Бурдонов И.В., Косачев А.С., Кулямин В.В. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай // Программирование,2004, т, С. 4-24.

32. Хорошилов А.В. Спецификация и тестирование систем с асинхронгшм интерфейсом. Препринт № 12. М.: Институт системного программирования РАН, 2006. 140 с.

33. Ur S., Yadin Y. Micro Architecture Coverage Directed Generation of Test Programs // DAC 1999: Design Automation Conference, 1999. P. 175-180.

34. Ur S., Yadin Y. Coverage Driven Processor Test Generation: Proof of Concept. 1997. 16 p. (http://www.research.ibm.com/pics/verification/ps/dac.ps)

35. Clark D.W. Bugs are Good: A Problem-Oriented Approach to the Management of Design Engineering // Research Technology Management, v. 33, № 3, May-June 1990. P. 23-27.

36. Tasiran S., Keutzer K. Coverage Metrics for Functional Validation of Hardware Designs fj IEEE Design h Test, v. 18, № 4, July 2001. P. 36-45.

37. Jou J.-Y., Liu C.-N. Coverage Analysis Techniques for HDL Design Validation j/ APCHDL 1999: The 6Lh Asia Pacific Conference on Chip Design Languages, 1999. (Invited Paper).

38. Piziali A. Functional Verification Coverage Measurement and Analysis. Kluwer Academic Publishers, 2004. 237 p.

39. Brock В,, Kaufmann М., Moore J.S. ACL2 Theorems About Commerical Microprocessors // FMCAD 1996: Formal Methods on Computer-Aided Design, 1996. P. 275-293.

40. Clarke E., German S., Zhao X. Verifying the SRT Division Algorithm Using Theorem Proving Techniques // Formal Methods in System Design, 1999. P. 7-44.

41. Rushby J. Formal Specification and Verification of a Fault-Masking and Transient-Recovery Model for Digital Flight-Control Systems // Formal Techniques in Real-Time and Fault-Tolerant Systems, 1992. 99 p.

42. Kapur D., Subramaniam M. Mechanically Verifying a Family of Multiplier Circuits // CAV 1996: Conference on Computer Aided Verification, 1996. P. 135-146.

43. Harrison J. Floating-Point Verification // FM 2005: Formal Methods / International Symposium of Formal Methods Europe, Springer LNCS 3582, 2005. P. 529-532.

44. Kumar R., Tahar S. Formal Verification of Pipeline Conflicts in RISC Processors // EURO-DAC 1994: European Design Automation Conference, 1994. P. 285-289.

45. Hunt W.A., Brock B.C. A Formal HDL and Us Use in the FM9001 Verification // Mechanized Reasoning and Hardware Design, Prentice Hall, 1992. P. 35-47.

46. Qadeer S., Tasiran S. Promising Directions in Hardware Design Verification // ISQED 2002: The 3rd International Symposium on Quality Electronic Design, 2002. P. 381-387.

47. Bhadra J., Abadir M., Ray S., Wang L. A Survey of Hybrid Techniques for Functional Verification // IEEE Design & Test, v. 24, № 22, March 2007. P. 112-122.

48. Mishra P., Dutt N. Architecture Description Languages for Programmable Embedded Systems // IEE Proceedings — Computers and Digital Techniques, v. 152, № 3, May 2005. P. 285-297.

49. Edwards S. Design and Verification Languages. Technical Report, New York, Columbia University, 2004. 18 p.

50. Beer I., Ben-David S., Eisner C., Fisman D., Gringauze A., Rodeh Y. The Temporal Logic Sugar // Lecture Notes in Computer Science, 2001. P. 363-367.

51. Ho R., Horowitz M. Validation Coverage Analysis for Complex Digital Designs // IC-CAD 1996: International Conference on Computer-Aided Design, 1996. P. 146-151.

52. Hoskote Y., Moundanos D., Abraham J. Automatic Extraction of the Control Flow Machine and Application to Evaluating Coverage of Verification Vectors // ICCD 1995: International Conference of Computer Design, 1995. P. 532-537.

53. Moundanos D., Abraham J., Hoskote Y. A Unified Framework for Design Validation and Manufacturing Test // ITC 1996: International Test Conference, 1996. P. 875-884.

54. Moundanos D., Abraham J., Hoskote Y. Abstraction Techniques for Validation Coverage Analysis and Test Generation // IEEE Transactions on Computers, v. 47, JV2 1, 1998. P. 2-14.

55. Shen J., Abraham J. An RTL Abstraction Technique for Processor Microarchitecture Validation and Test Generation // Journal of Electronic Testing, v. 16, № 1-2, February 1999. P. 67-81.

56. Geist D., Farkas M., Landver A., Lichtenstein Y., Ur S., Wolfsthal Y. Coverage Directed Test Generation Using Symbolic Techniques // FMCAD 1996: Formal Methods in Computer Aided Design, LNCS 1166, 1996. P. 143-158.

57. Fournier L., Arbetman Y., Levinger M. Functional Verification Methodology for Microprocessors Using the Genesys Test Program Generator: Application to the x86 Microprocessors Family // DATE 1999: Design Automation and Test in Europe, 1999. P. 434-441.

58. Mishra P., Dutt N. Automatic Functional Test Program Generation for Pipelined Processors Using Model Checking 11 HLDVT 2002: Proceedings of the 1th IEEE International High-Level Design Validation and Test Workshop, 2002. P. 99-103.

59. Mishra P., Dutt N. Architecture Description Language Driven Functional Test Program Generation for Microprocessors Using SMV. CECS Technical Report 02-26, September 13, 2002. 18 p.

60. Mishra P., Dutt N. Graph-Based Functional Test Program Generation for Pipelined Processors // DATE 2004: Design, Automation and Test in Europe Conference and Exhibition, 2004. P. 182-187.

61. Mishra P., Dutt N., Krishnamurthy N., Abadir M.S. A Top-Down Methodology for Validation of Microprocessors // IEEE Design h Test, v. 21, № 2, March-April 2004. P. 122-131.

62. Mishra P., Dutt N. Functional Coverage Driven Test Generation for Validation of Pipelined Processors // DATE 2005: Design, Automation and Test in Europe, Vol. 2, 2005. P. 678-683.

63. Koo H.M., Mishra P. Test Generation Using SAT-based Bounded Model Checking for Validation of Pipelined Processors // ACM Great Lakes Symposium on VLSI, 2006. P. 362-365

64. Koo H.M., Mishra P. Functional Test Generation Using Property Decomposition for Validation of Pipelined Processors // DATE 2006: Design, Automation and Test in Europe, 2006. P. 1240-1245.

65. Grun P., Halambi A., Khare A., Ganesh V., Dutt N., Nicolau A. EXPRESSION: An ADL for System Level Design Exploration // Technical Report 1998-29, University of California, Irvine, 1998. 28 p.

66. Lewin D., Lorenz D., Ur S. A Methodology for Processor Implementation Verification // FMCAD 1996: Formal Methods in Computer Aided Design, LNCS 1166, 1996. P. 126142.

67. Kohno K, Matsumoto N. A New Verification Methodology for Complex Pipeline Behavior 11 DAC 2001: Design Automation Conference, 2001. P. 816-821.

68. Corno F., Sonza Reorda M., Squillero G., Violante M. A Genetic Algorithm-based System . for Generating Test Programs for Microprocessor IP Cores // ICTAI 2000: The 12th

69. EE International Conference on Tools with Artificial Intelligence, 2000. P. 195-198.

70. Corno F., Sonza Reorda M., Squillero G., Violante M. On the Test of Microprocessor IP Cores 11 DATE 2001: IEEE Design, Automation & Test in Europe Conference, 2001. P. 209-213.

71. Corno F., Cumani G., Sonza Reorda M., Squillero G. Automatic Test Program Generation from RT-Level Microprocessor Descriptions // ISQED 2002: The 3rd International Symposium on Quality Electronic Design, 2002. P. 120-125.

72. Corno F., Cumani G., Sonza Reorda M., Squillero G. Efficient Machine-Code Test-Program Induction // CEC 2002: Congress on Evolutionary Computation, 2002. R 1486-1491.

73. Corno F., Cumani G., Sonza Reorda M., Squillero G. Evolutionary Test Program Induction for Microprocessor Design Verification // ATS 2002: IEEE Asian Test Symposium,2002. P. 368-373.

74. Corno F., Cumani G., Sonza Reorda M., Squillero G. Fully Automatic Test Program Generation for Microprocessor Cores // DATE 2003: Design, Automation and Test in Europe, 2003. P. 1006-1011.

75. Corno F., Sonza Reorda M., Squillero G. Automatic Test Program Generation for Pipelined Processors // SAC 2003: The 18t/l Annual ACM Symposium on Applied Computing, 2003. P. 736-740.

76. Corno F., Squillero G. Exploiting Auto-Adaptive GP for Highly Effective Test Programs Generation // ICES 2003: The 5th International Conference on Evolvable Systems: From Biology to Hardware, 2003. P. 262-273.

77. Corno F., Squillero G. An Enhanced Framework for Microprocessor Test-Program Generation II EUROGP 2003: The GLh European Conference on Genetic Programming,2003. P. 307-315.

78. Corno F., Sanchez E., Sonza Reorda M., Squillero G. Automatic Test Program Generation: a Case Study // IEEE Design & Test, Special issue on Functional Verification and Testbench Generation, v. 21, № 2, March-April 2004. P. 102-109.

79. Corno F., Sanchez E., Sonza Reorda M., Squillero G. Code Generation for Functional Validation of Pipelined Microprocessors // Journal of Electronic Testing: Theory and Applications, v. 20, № 3, June 2004. P. 269-278.

80. Lindsay W., Sanchez E., Sonza Reorda M., Squillero G. Automatic Test Programs Generation Driven by Internal Performance Counters // MTV 2004: The bih International Workshop on Microprocessor Test and Verification, 2004. P. 8-13.

81. Squillero G. MicroGP — An Evolutionary Assembly Program Generator // Genetic Programming and Evolvable Machines, v. 6, № 3, 2005. P. 247-263.

82. Бурдонов И.Б. Теория конформности для функционального тестирования программных систем на основе формальных моделей. Диссертация на соискание ученой степени д.ф.-м.н., 2008. 436 с.

83. Meyer В. Applying "Design by Contract" // IEEE Computer, v. 25, № 10, October 1992. P. 40-51.

84. Bourdonov I., Kossatchev A., Kuliamin V., Petrenko A. UniTESK Test Suite Architecture j j FM 2002: Formal Methods / International Symposium of Formal Methods Europe, LNCS 2391, Springer-Verlag, 2002. P. 77-88.

85. Кулямин В.В., Петренко А.К., Косачев А.С., Бурдонов И.Б. Подход UniTESK к разработке тестов // Программирование, № 6, 2003. С. 25-43.

86. Sutherland S. The Verilog PLI Handbook: A User's Guide and Comprehensive Reference on the Verilog Programming Language Interface. Springer, 2002. 798 p.

87. Bourdonov I., Kossatchev A., Petrenko A., Gaiter D. KVEST: Automated Generation of Test Suites from Formal Specifications // FM 1999: Formal Methods / International Symposium of Formal Methods Europe, LNCS 1708, Springer-Verlag, 1999. P. 608-621.

88. The RAISE Language Group. The RAISE Specification Language. Prentice-Hall BCS Practitioner Series. Prentice-Hall, Inc., 1993. 397 p.

89. RM7000 Family User Manual. Issue 1, May 2001.

90. MIPS64™ Architecture For Programmers. Revision 2.0. MIPS Tecnologies Inc., June 9, 2003.