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

Российская академия наук Институт системного программирования

УДК 519.68

На правах рукописи

Камкин Александр Сергеевич

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

Специальность 05.13.11 -математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Москва 2008

003451308

Работа выполнена в Институте системного программирования РАН.

Научный руководитель: доктор физико-математических наук

Петренко Александр Константинович

Официальные оппоненты: доктор физико-математических наук

Лазутин Юрий Михайлович

доктор технических наук Шнитман Виктор Зиновьевич

Ведущая организация: Московский государственный институт

электроники и математики

Защита диссертации состоится «21 » ноября 2008 г. в 15 часов на заседании диссертационного совета Д.002.087.01 при Институте системного программирования РАН по адресу:

109004, Москва, ул. Б. Коммунистическая, д.25,

Институт системного программирования РАН, конференц-зал (комн. 110).

С диссертацией можно ознакомиться в библиотеке Института системного программирования РАН.

Автореферат разослан «/4 » октября 2008 г.

Ученый секретарь ----------------

диссертационного совета /Прохоров С.П./

канд. физ.-мат. наук ¡У ¡у

Общая характеристика работы

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

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

Микропроцессоры являются сложными электронными устройствами, производство которых можно начать только после тщательного проектирования. Проектирование микропроцессоров выполняется на специализированных языках описания аппаратуры (HDL, Hardware Description Languages). Поскольку исправление ошибок в уже изготовленных микропроцессорах возможно только в исключительных случаях и требует колоссальных затрат, большую часть ошибок крайне желательно выявить и исправить еще на этапе проектирования.

Одним из основных методов обеспечения надежности микропроцессоров является тестирование проектной модели. Такое тестирование называется имитационным (simulation-based verification)^. По различным данным, тестирование микропроцессоров составляет 50-80% от общего объема трудозатрат на их разработку. Для большей эффективности обнаружения ошибок и упрощения их локализации тестирование микропроцессоров включает в себя тестирование модулей по отдельности. Таким образом, тестирование осуществляется на двух основных уровнях: модульном {unit-level) и системном (core-level).

1 Далее для краткости будем называть имитационное тестирование просто тестированием.

Большинство микропроцессоров, разрабатываемых в настоящее время, имеют конвейерную архитектуру. Это означает, что в один и тот же момент времени микропроцессор может обрабатывать сразу несколько инструкций. Выполнение инструкций в таких микропроцессорах разбивается на несколько стадий, при этом разные стадии разных инструкций могут выполняться параллельно. Конвейерная организация значительно усложняет устройство микропроцессора, добавляя в него механизмы планирования и синхронизации выполнения инструкций, которые в совокупности называются управляющей логикой (control logic). Сложная организация и огромное пространство состояний микропроцессоров с конвейерной архитектурой делают их тестирование очень сложной задачей, которую невозможно решить без применения методов автоматизации тестирования.

Анализ ошибок в микропроцессоре MIPS R4000 PC/SC (ревизия 2.2)2, проведенный Ричардом Хо (Richard Но) и др.3, говорит, что большинство ошибок (93.5%) связаны с управляющей логикой конвейера, причем значительную их часть очень сложно обнаружить. Приведенный выше анализ ошибок относится к середине 1990-ых гг., но, следует отметить, что ошибки в управляющей логике и по сей день являются трудно обнаруживаемыми. Список ошибок, датируемый 2006 г., широко используемого в аэрокосмической промышленности микропроцессора TSC695F компании Atmel с архитектурой SPARC v7, включает ошибку (одну из трех), связанную с работой конвейера4.

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

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

3 R.C. Ho, C.H. Yang, M.A. Horowitz, and D.L. Dill. Architecture Validation for Processors. ISCA'1995: International Symposium on Computer Architecture, 1995.

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

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

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

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

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

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

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

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

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

Научная новизна

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

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

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

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

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

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

Практическая значимость работы подтверждается эффективностью применения предложенных методов для тестирования отдельных модулей и

подсистем микропроцессора Комдив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 г.);

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

2007-2008 гг.);

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

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

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

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

Краткое содержание диссертации

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

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

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

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

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

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

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

Исследуется выразительная мощность контрактных спецификаций конвейера. Результатом исследований являются теоремы об адекватности и полноте спецификаций:

Теорема (об адекватности спецификаций). Пусть инициальный расширенный автомат соответствует контрактной спег^фикации конвейера, тогда соответствующий спецификационный подавтомат является автоматной моделью конвейера.

Теорема (о полноте спецификаций). Для любой автоматной модели конвейера существует точно описывающая ее контрактная спецификация конвейера.

На практике распространены модули, имеющие память (набор ресурсов), которую можно адресовать. Для компактного описания таких модулей вводится понятие контрактной спецификации конвейера с ресурсами. Идея состоит в том, что каждая стадия операции параметризуется адресами ресурсов, которые она использует. Адреса ресурсов вычисляются по значениям входных параметров стимула. В состояние управления добавляется информация об адресах ресурсов, используемых в стадиях обрабатываемых операций. Охранные предикаты стимулов и стадий определяются на основе расширенного состояния управления. Семантика контрактной спецификации конвейера с ресурсами определяется с помощью ее преобразования к форме определенной ранее контрактной спецификации конвейера с блокировками. Тем самым, эти формализмы имеют одинаковую выразительную мощность.

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

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

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

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

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

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

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

спецификации конвейера и описания тестового покрытия. Состояниями обобщенной автоматной модели конвейера являются обобщенные состояния, стимулами — стимулы контрактной спецификации конвейера, размеченные тестовыми ситуациями и зависимостями. Показывается, что граф состояний обобщенной автоматной модели конвейера является конечным, детерминированным и сильно-связным, что позволяет применять неизбыточные алгоритмы обхода, исследованные в работах И.Б. Бурдонова, A.C. Косачева, В.В. Куляминаи A.B. Хорошилова.

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

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

В конце главы описывается разработанная автором библиотека PIPE для инструмента CTESK, предназначенная для поддержки создания спецификаций и тестов для модулей с конвейерной организацией.

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

• интерфейс инструкции — описывает операнды инструкции. Для каждого операнда указывается его имя, способ передачи значения (непосредственно или через регистр, в последнем случае также указывается тип регистра), тип данных и информация о том, является операнд входным или выходным;

• предусловие инструкции — определяет ситуации, в которых определено поведение микропроцессора при выполнении данной инструкции. Автоматически создаваемой частью предусловия является проверка совместимости значений входных операндов соответствующим типам данным;

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

• ассемблерный формат инструкции — определяет формат записи инструкции и ее операндов на языке ассемблера.

Совместно с методом можно использовать два способа проверки правильности поведения: с помощью сравнения трасс и используя тесты со встроенными проверками (self-checking tests). Сравнение трасс основано на ко-симуляции, когда сгенерированные тестовые программы выполняются на тестируемой модели микропроцессора и симуляторе. Результатами выполнения программ являются трассы — последовательности событий, каждое из которых включает данные о выполненной инструкции, значениях ее выходных регистров, состоянии счетчика адреса и, возможно, некоторую

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

Как и в описанном методе модульного тестирования метод системного тестирования использует неизбыточное описание тестового покрытия в форме тестовых ситуаций и зависимостей. Тестовые ситуации описывают ограничения на значения входных операндов инструкций и состояние микропроцессора. Зависимости ограничивают значения входных операндов для пары инструкций. В методе выделяется два типа зависимостей: зависимости по регистрам и зависимости по данным. Зависимости по регистрам подразделяются на зависимости типа «определение-использование», когда выходной регистр одной инструкции является входным регистром следующей за ней инструкции5, и зависимости типа «определение-определение», когда выходной регистр одной инструкции также является выходным регистром следующей за ней инструкции.

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

Генерируемые тестовые программы имеют следующую структуру: я = • {(^1, х:[5|, },=!,„ • я8,ор, где:

5 Между зависимыми по регистру инструкциями могут находиться другие инструкции, но эти инструкции не должны переопределять регистр.

• Testait — инициализирующая программа

префикс тестовой программы, который содержит инструкции, предназначенные для инициализации микропроцессора;

• (л;, Xi[s;, d,]) — тестовый вариант (i = 1, ...,n):

о tci — программа подготовки тестового воздействия

последовательность инструкций, осуществляющая

инициализацию регистров и памяти микропроцессора; о Xi[Si, d[] — тестовое воздействие

специально подготовленная последовательность инструкций, предназначенная для тестирования микропроцессора, где s,- — множество тестовых ситуаций, a di — множество зависимостей;

• Тсдар — завершающая программа

постфикс тестовой программы, который содержит инструкции, предназначенные для завершения работы микропроцессора;

• п — размер тестовой программы число тестовых воздействий в программе.

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

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

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

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

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

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

Таблица 1. Данные по методу модульного тестирования.

Показатель Буфер трансляции адресов Модуль кэш-памяти второго уровня

Объем реализации, строк кода 3500 3000

Число тестируемых операций 5 6

Число требований 99 166

Объем спецификаций и тестов, строк кода 3500 4700

Трудоемкость разработки тестов, чел.-мес. 2.5 4

Число найденных ошибок в проектной модели 10 4

Таблица 2. Данные по методу системного тестирования.

Показатель Подсистема управл. памятью Микропроцессор Комдив64 Сопроцессор Комдив128

Число тестируемых инструкций 4 221 109

Объем спецификаций и тестов, строк кода 5560 47190 20610

Трудоемкость разработки тестов, чел.-мес. 2 9 4

Число найден, ошибок в эталонном симуляторе 0 6 5

Число найден, ошибок в проектной модели I 9 Нет данных

Применение метода модульного тестирования в проектах по тестированию буфера трансляции адресов и модуля кэш-памяти второго уровня показывает, что трудоемкость разработки тестов пропорциональна числу требований, накладываемых на тестируемый модуль, и составляет около 2-х требований за 1 человеко-день. Для метода системного тестирования получены данные, что в среднем разработка тестов для 1-ой инструкции микропроцессора занимает 0.7-0.8 человеко-дня. Линейная зависимость трудоемкости разработки тестов от числа требований и инструкций позволяет утверждать, что предлагаемые методы являются масштабируемыми. Данные о трудоемкости разработки тестовых программ

для микропроцессора Комдив64-СМП показывают, что предлагаемый метод автоматизации системного тестирования, позволяет сократить затраты на создание системных тестов в 2-2.5 раза.

В заключении перечисляются основные результаты работы.

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

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

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

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

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

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

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

Работы автора по теме диссертации

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

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

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

т. 10. М., 2006. С. 143-166.

4. Kamkin A. The UniTESK Approach to Specification-Based Validation of Hardware Designs // Proceedings of 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 // Proceedings of SYRCoSE 2007: The 1st Spring Young Researchers Colloquium on Software Engineering, v. 2. 2007.

P. 7-13.

7. Аряшев С.И., Камкин A.C., Рогаткин Б.Ю. Тестирование RTL-моделей аппаратуры с помощью технологии UniTESK на примере блока преобразования адресов микропроцессора // Сборник научных трудов конференции «Электроника, микро- и наноэлектроника - 2007», 2007. С. 183-187.

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

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

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

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

12.Chupilko М., Kamkin A., Vorobyev D. Methodology and Experience of Simulation-Based Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications // Proceedings of SYRCoSE 2008: The 2nd Spring Young Researchers Colloquium on Software Engineering, v. 2.2008. P. 25-31.

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

М.Камкин A.C. Комбинаторная генерация тестовых программ для

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

Подписано в печать 17.10.2008 г.

Печать трафаретная

Заказ № 979 Тираж: 100 экз.

Типография «11-й ФОРМАТ» ИНН 7726330900 115230, Москва, Варшавское ш., 36 (499) 788-78-56 www.autoreferat.ru

Введение

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 страницы.

Заключение

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

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

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

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

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

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

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

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

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.