Содержание к диссертации
Введение
1 Функциональная верификация микропроцессоров 13
1.1 Тестирование микропроцессоров 14
1.1.1 Проверка правильности поведения 17
1.1.2 Генерация тестовой последовательности 20
1.1.3 Оценка полноты тестирования 23
1.2 Формальная верификация микропроцессоров 26
1.2.1 Проверка эквивалентности 26
1.2.2 Проверка моделей 27
1.2.3 Автоматизированное доказательство теорем 28
1.3 Тестирование и формальная верификация 29
1.4 Тестирование микропроцессоров с конвейерной архитектурой 31
1.4.1 Методы формальной спецификации 32
1.4.2 Методы модульного тестирования 34
1.4.3 Методы системного тестирования 37
1.5 Анализ текущего состояния 40
1.5.1 Методы формальной спецификации 40
1.5.2 Методы модульного тестирования 42
1.5.3 Методы системного тестирования 43
1.6 Уточнение задач диссертационной работы 44
1.7 Краткое введение в предлагаемый метод 45
2 Модульное тестирование микропроцессоров 47
2.1 Введение в метод модульного тестирования микропроцессоров 48
2.2 Формальная спецификация конвейера 50
2.2.1 Вспомогательные понятия 50
2.2.2 Модель конвейера без блокировок 56
2.2.3 Спецификация конвейера без блокировок 62
2.2.4 Отношение соответствия 6G
2.2.5 Модель конвейера с блокировками 72
2.2.6 Спецификация конвейера с блокировками 75
2.2.7 Спецификация конвейера с ресурсами 81
2.3 Тестирование на основе контрактных спецификаций конвейера 85
2.3.1 Проверка правильности поведения 85
2.3.2 Определение тестового покрытия 87
2.3.3 Генерация тестовой последовательности 93
2.4 Инструментальная поддержка модульного тестирования 102
2.4.1 Технология тестирования UniTESK 103
2.4.2 Тестирование Verilog-моделей 107
2.4.3 Тестирование SystemC-моделей 114
2.4.4 Библиотека PIPE 117
2.5 Результаты главы 127
3 Системное тестирование микропроцессоров 129
3.1 Введение в метод системного тестирования микропроцессоров 130
3.2 Основные понятия предлагаемого метода 131
3.2.1 Тестовый шаблон 132
3.2.2 Зависимости между инструкциями 133
3.2.3 Тестовые ситуации 136
3.2.4 Тестовые воздействия 138
3.3 Формальная спецификация микропроцессора 139
3.3.1 Формальная спецификация подсистем 139
3.3.2 Формальная спецификация типов данных 140
3.3.3 Формальная спецификация системы команд 141
3.4 Метод генерации тестовых программ 142
3.4.1 Схема генерации тестовых программ 143
3.4.2 Подготовка тестовых воздействий 144
3.4.3 Параметры управления генерацией 145
3.5 Инструментальная поддержка системного тестирования 146
3.5.1 Генератор тестовых программ MicroTESK 147
3.5.2 Примеры описаний тестов и тестовых программ 149
3.5.3 Отладка спецификаций и тестов 153
3.6 Результаты главы 154
4 Опыт практического применения предлагаемого метода 155
4.1 Тестирование буфера трансляции адресов 155
4.1.1 Краткое описание тестируемого модуля 155
4.1.2 Спецификация и тестирование модуля 157
4.1.3 Результаты апробации 158
4.1.4 Повторное использование спецификаций и тестов 158
4.2 Тестирование модуля кэш-памяти второго уровня 159
4.2.1 Краткое описание тестируемого модуля 159
4.2.2 Спецификация и тестирование модуля 160
4.2.3 Результаты апробации 161
4.3 Тестирование подсистемы управления памятью 162
4.3.1 Краткое описание тестируемой подсистемы 162
4.3.2 Спецификация и тестирования подсистемы 162
4.3.3 Результаты апробации 163
4.4 Тестирование микропроцессора Комдив64 164
4.4.1 Краткое описание тестируемого микропроцессора 164
4.4.2 Спецификация и тестирование микропроцессора 165
4.4.3 Результаты апробации 165
4.5 Тестирование арифметического сопроцессора Комдив128 167
4.5.1 Описание тестируемого сопроцессора 167
4.5.2 Спецификация и тестирование сопроцессора 168
4.5.3 Результаты апробации 168
4.6 Результаты главы 169
Заключение 171
Список литературы
- Проверка правильности поведения
- Методы формальной спецификации
- Тестирование на основе контрактных спецификаций конвейера
- Повторное использование спецификаций и тестов
Введение к работе
Актуальность темы
Современный мир не мыслим без огромного разнообразия электронных устройств. Мобильные телефоны, цифровые фотокамеры и переносные компьютеры давно стали неотъемлемыми атрибутами жизни многих людей. Специальные устройства управляют работой бытовой техники, контролируют бортовые системы самолетов и космических спутников, регулируют медицинские системы жизнеобеспечения. В основе практически всех этих систем лежат микропроцессоры — программно-управляемые устройства, предназначенные для решения задач цифровой обработки данных.
Неудивительно, что требования к надежности микропроцессоров очень высоки. Ошибки в микропроцессорах могут приводить к некорректной, иногда непредсказуемой, работе вычислительных систем, в состав которых они входят, в то время как число критически важных приложений микропроцессорных систем достаточно велико. Ошибки могут привносить неточность в научно-технические расчеты, причинять вред здоровью людей, ставить под угрозу государственную безопасность. С расширением сфер использования вычислительных систем растет и цена ошибки в микропроцессоре.
На формирование высоких требований к надежности микропроцессоров большое влияние оказывает также следующая особенность полупроводниковой аппаратуры. В отличие от программного обеспечения, в котором исправление ошибки стоит сравнительно дешево, ошибка в микросхеме, обнаруженная несвоевременно, может потребовать перевыпуск и замену продукции, а это сопряжено с очень высокими затратами. Так, известная ошибка в реализации инструкции FDIV микропроцессора Pentium1 [15], заключающаяся в неправильном делении некоторых чисел с плавающей точкой, обошлась компании Intel почти в 475 млн. долларов [16].
В условиях рыночной конкуренции, а конкуренция на рынке микропроцессоров существует [17], важно найти компромисс между многими факторами, включая затраты на разработку и сроки выпуска продукта на рынок. Конкурентоспособный
1Pentium — торговая марка нескольких поколений микропроцессоров семейства x8G, выпускаемых компанией 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 Управляющей логикой конвейера или просто управляющей логикой называется внутренняя
функциональность микропроцессора, отвечающая за планирование и организацию выполнения инструкций.
4NOP или NOOP (No Operation) — специальная инструкция микропроцессора, которая не производит никаких действий и обычно используется для временных задержек и выравнивания памяти.
7 Таблица 1: Статистика ошибок MIPS R4000 PC/SC.
по адресу, содержащемуся в загруженном регистре.
Инструкция перехода — последняя инструкция на странице виртуальной памяти.
Номер следующей страницы не содержится в буфере трансляции адресов (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.
использование позволяет сократить трудоемкость разработки тестов и повысить "глубину" тестирования.
Прямое применение существующих методов автоматизации тестирования на основе формальных спецификаций к промышленным проектам сталкивается с проблемами. Разработка спецификаций и моделей для сложных микропроцессоров и их модулей является трудоемкой задачей, и если метод не предоставляет механизмы эффективной поддержки тестов, то его применение в условиях постоянного уточнения требований, непрерывных доработок интерфейса и реализации, которые имеют место в промышленных проектах, потребует колоссальных затрат. Существующие методы автоматизации тестирования либо не масштабируются на сложные микропроцессоры, либо не устойчивы к изменениям в реализации, что приводит к существенной переработке разработанных описаний даже при небольших изменениях в реализации.
Одна из причин, по которой методы на основе формальных спецификаций не достаточно эффективно применяются в промышленных проектах, состоит в наличии двух независимых описаний: формальной спецификации, которая используется для оценки правильности поведения микропроцессора или его модуля, и модели теста, используемой для генерации тестовых последовательностей и оценки полноты тестирования. Другая причина заключается в неразвитых средствах формальной спецификации микропроцессоров с конвейерной архитектурой, что не позволяет достичь высокого уровня автоматизации тестирования. Представляется перспективным разработать метод формальной спецификации конвейера и метод автоматизации тестирования на его основе спецификаций предлагаемого вида, который был бы лишен указанных недостатков.
Цель и задачи работы
Целью диссертационной работы является разработка метода автоматизации тестирования микропроцессоров на основе формальных спецификаций, который масштабируется на сложные микропроцессоры с конвейерной архитектурой и является пригодным для использования в промышленных проектах. Для достижения цели работы были поставлены следующие задачи:
Провести анализ существующих методов автоматизации тестирования микропроцессоров с конвейерной архитектурой.
Разработать новые методы автоматизации модульного и системного тестирования микропроцессоров с конвейерной архитектурой, которые обеспечивают высокий
уровень автоматизации разработки тестов и повторного использования спецификаций и тестов.
Провести апробацию разработанных методов в промышленных проектах.
Основные результаты работы
Основные научные и практические результаты, полученные в диссертационной работе и выносимые на защиту, состоят в следующем:
разработан метод формальной спецификации модулей микропроцессоров на основе пред- и постусловий стадий выполнения операций, названный контрактной спецификацией конвейера;
разработан метод неизбыточного описания тестового покрытия с помощью тестовых ситуаций и зависимостей;
разработан метод генерации тестовой последовательности на основе обобщенной автоматной модели, построенной по формальной спецификации модуля и описанию тестового покрытия;
разработан метод генерации тестовых программ для системного тестирования микропроцессоров на основе формальной спецификации системы команд микропроцессора и тестового покрытия;
реализованы инструменты, поддерживающие разработанные методы.
Научная новизна работы
Научной новизной обладают следующие результаты работы:
Метод формальной спецификации модулей микропроцессоров на основе пред- и постусловий стадий выполнения операций.
Метод неизбыточного описания тестового покрытия с помощью тестовых ситуаций и зависимостей.
Метод генерации тестовой последовательности на основе обобщенной автоматной модели конвейера, построенной по формальной спецификации модуля и описанию тестового покрытия.
Метод генерации тестовых программ для системного тестирования
микропроцессоров на основе формальной спецификации системы команд и
тестового покрытия.
Практическая значимость
Практическая значимость работы подтверждается результатами применения предложенных методов для тестирования отдельных модулей и подсистем микропроцессора Комдив04-СМП, системного тестирования микропроцессора Комдивб4 и системного тестирования арифметического сопроцессора Комдив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 г.);
По теме диссертации автором опубликованы работы [1]-[14] (из них 1 в изданиях по перечню ВАК), полно отражающие основные результаты диссертации.
Структура и объем диссертации
Работа состоит из введения, четырех глав, заключения и списка литературы (109 наименований). Основной текст диссертации (без приложений и списка литературы) занимает 172 страницы.
Краткое содержание диссертации
Во введении обосновывается актуальность темы работы, определяются ее цели и задачи, раскрывается практическая значимость.
Первая глава содержит обзор методов, которые в настоящее время используются для функциональной верификации микропроцессоров. Наряду с тестированием рассматриваются методы формальной верификации, такие как проверка эквивалентности, проверка моделей и автоматизированное доказательство теорем. Описываются достоинства и ограничения различных методов. Основное внимание уделяется методам модульного и системного тестирования, поскольку это основные методы проверки корректности микропроцессоров и других сложных программных и аппаратных систем. В конце главы делается анализ существующих методов автоматизации тестирования микропроцессоров с конвейерной архитектурой, уточняются цели и задачи диссертационной работы.
Во второй главе описывается предлагаемый автором метод автоматизации модульного тестирования микропроцессоров. В основе подхода лежит метод формальной спецификации модулей микропроцессоров с помощью пред- и постусловий стадий выполнения операций, названный автором контрактной спецификацией конвейера. На основе формализма расширенных автоматов определяется семантика таких спецификаций, исследуются вопросы их выразительной мощности, доказываются теоремы об адекватности и полноте. Показывается, как использовать формальные спецификации предлагаемого вида для решения задач тестирования: проверки правильности поведения, оценки полноты тестирования и генерации тестовой последовательности. Описывается схема проверки правильности поведения модулей,
на основе которой производится классификация ошибок. Для оценки полноты тестирования предлагается метод неизбыточного описания тестового покрытия, который заключается в декомпозиции целей тестирования на тестовые ситуации и зависимости. Предлагаемый метод генерации тестовой последовательности основан на обходе графа состояний обобщенной автоматной модели конвейера, построенной по контрактной спецификации конвейера и описанию тестового покрытия. В конце главы описывается инструментальная поддержка разработки спецификаций и тестов для модулей с конвейерной организацией.
Третья глава посвящена предлагаемому автором методу автоматизации системного тестирования микропроцессоров. ' Метод заключается в автоматической генерации тестовых программ на основе формальной спецификации системы команд и описания тестового покрытия. Как и в методе модульного > тестирования для системного тестирования используется неизбыточное описание тестового покрытия в форме тестовых ситуаций и зависимостей. Предлагаемый метод оперирует с более абстрактными формальными спецификациями, из которых нельзя извлечь точную модель управляющей логики конвейера. В этом случае применяется комбинаторное тестирование, в котором в качестве тестовых воздействий выступают последовательности инструкций микропроцессора, для которых строятся различные комбинации тестовых ситуаций и зависимостей, определенных в тестовом покрытии. В конце главы описывается архитектура разработанного генератора тестовых программ.
В четвертой главе описываются результаты практической апробации предлагаемого автором метода для тестирования промышленных микропроцессоров, их модулей и подсистем, а именно: буфера трансляции адресов, модуля кэшпамяти второго уровня и подсистемы управления памятью микропроцессора Комдив64-СМП, микропроцессора Комдив64 и арифметического сопроцессора Комдив128, разрабатываемых в НИИ системных исследований РАН. В главе приводятся данные о трудоемкости разработки спецификаций и тестов, объеме разработанных описаний и возможности повторного использования спецификаций и тестов для тестирования микропроцессоров с близкой функциональностью. Основным результатом главы является практическое обоснование того, что предлагаемый автором метод автоматизации тестирования микропроцессоров соответствует поставленным в работе целям.
Проверка правильности поведения
Ричард Хо (Richard Но) в своей диссертации (1996 г.) [35] выделяет два основных способа проверки правильности поведения тестируемого компонента. Первый способ — это так называемая ко-симуляция (co-simulation framework), второй — самопроверяющие тесты (self-checking framework). Отдельно можно выделить третий способ, основанный на использовании формальных спецификаций. Рассмотрим последовательно каждый из указанных способов.
Ко-симуляция
Для осуществления ко-симуляции6 отдельно от тестируемого компонента разрабатывается его исполнимая модель, имеющая ту же функциональность, но, как правило, более абстрактная и представленная в более наглядной форме. Такая модель называется эталонной моделью (reference model, golden model). На тестируемый компонент и его эталонную модель подается одна и та же тестовая последовательность (осуществляется ко-симуляция), результаты работы компонента и модели сравниваются на соответствие7. Отметим, что язык, на котором разрабатывается эталонная модель, может отличаться от языка, используемого для разработки тестируемого компонента. В данном способе предполагается, что тестируемый компонент и его эталонная модель разрабатываются независимо друг от друга, поэтому вероятность того, что обе модели содержат одну и ту же ошибку достаточно мала. Другим обоснованием ко-симуляции является то, что эталонная модель является более абстрактной, поэтому потенциально содержит меньшее число ошибок. При нахождении несоответствия между поведением тестируемого компонента и эталонной модели выясняется какая из моделей некорректна; после исправления ошибки тестирование продолжается.
Важным достоинством ко-симуляции является то, что проверка правильности поведения тестируемого компонента может осуществляться автоматически независимо от вида тестовой последовательности. Это избавляет разработчика тестов от необходимости писать отдельные проверки для каждого конкретного теста и позволяет использовать автоматические генераторы тестовых последовательностей, что значительно повышает эффективность тестирования. Однако в некоторых случаях использование ко-симуляции сталкивается со сложностями [35].
Проблемы возникают, когда эталонная модель является более абстрактной. В этом случае между состоянием тестируемого компонента и состоянием эталонной модели бывает сложно установить соответствие. Приведем пример, иллюстрирующий такую ситуацию. Часто при тестировании микропроцессоров с конвейерной архитектурой в качестве эталонной модели используют симуляторы уровня инструкций (instruction-level simulators)8, которые реализуют последовательное выполнение инструкций, никак не отражая состояние конвейера. Для проверки соответствия состояний в этом случае необходимо правильно выбирать точки синхронизации — моменты времени, в которые осуществляется проверка. Для симулятора таким моментом будет завершение выполнение инструкции, а для тестируемой модели микропроцессора — завершение стадии записи результата при выполнении инструкции на конвейере (см. рисунок 1.3). В общем случае определение точек синхронизации является сложной задачей, поскольку современные микропроцессоры могут переупорядочивать инструкции и выполнять несколько инструкций одновременно.
Подводя итоги, можно отметить следующее. Для осуществления ко
симуляции необходима эталонная модель тестируемого компонента. Разработка эталонной модели является сложной задачей, и во многих случаях ее трудоемкость соизмерима с трудоемкостью разработки самого компонента [35]. Наличие эталонной модели позволяет автоматизировать проверку правильности поведения тестируемого компонента и дает возможность использования автоматических генераторов тестов. Недостатком ко-симуляции является большое время, необходимое для получения первых тестов.
Самопроверяющие тесты
Часто, когда тесты нужно получить быстро, вместо ко-симуляции применяют другой подход к тестированию, называемый самопроверяющими тестами. Такое тестирование предполагает, что каждый тест помимо тестовой последовательности содержит проверки, которые необходимо осуществить после оказания воздействия на тестируемый компонент. С одной стороны, при использовании самопроверяющих тестов не нужно разрабатывать эталонную модель, но с другой стороны, требуются ббльшие усилия на разработку тестов, поскольку каждый тест необходимо снабдить соответствующими проверками.
Автоматическая генерация тестовых последовательностей для самопроверяющих тестов практически неосуществима, поэтому этот подход используется преимущественно при ручной разработке тестов, что является его основным недостатком. Другим существенным недостатком самопроверяющих тестов является сложность поддержки. При изменении- тестируемого компонента приходится переделывать все тесты, которые связаны с измененной функциональностью. Наконец, многие проверки приходится дублировать в разных тестах, поскольку если исключить такую избыточность, то теряется полнота проверок, и тесты могут пропустить ошибку.
Для сглаживания последнего недостатка при тестировании часто используют специальные тестовые агенты, называемые снуперами (snoopers), которые осуществляют мониторинг ошибочных ситуаций в процессе симуляции. Снуперы разрабатываются на том же языке, что и тестируемый компонент, обычно в них реализованы относительно простые проверки целостности состояния компонента.
Тестирование на основе формальных спецификаций
Под спецификацией понимается некоторое представление требований к системе. Если спецификация определяется на формальном, машиночитаемом языке, она называется формальной спецификацией. Примером формальной спецификации является эталонная модель, используемая для ко-симуляции, — это исполнимая спецификация тестируемого компонента. Другим видом формальных спецификаций являются декларативные спецификации, которые описывают требования к компоненту в виде набора ограничений, которым должно удовлетворять его поведение9. Примерами декларативных спецификаций являются контрактные спецификации в форме пред-и постусловий; спецификации, основанные на темпоральной логике и др. В данном разделе рассматриваются только декларативные спецификации.
Декларативные спецификации тесно связаны с так называемыми утверждениями (assertions). Под утверждениями понимаются проверки, которые встраиваются в код компонента (снуперы) или описываются отдельно от реализации. В настоящее время существуют специализированные языки и библиотеки для написания утверждений, позволяющие определять требования в виде формул темпоральной логики. Самые известные из них OpenVera Assertions (OVA) [28], SystemVerilog Assertions (SVA) [31], Open Verification Library (OVL) [36] и Property Specification Language (PSL) [37]. Однако следует различать спецификации и утверждения: если первые полно описывают функциональность тестируемого компонента, то последние, как правило, определяют отдельные свойства.
Тестирование на основе формальных спецификаций совмещает в себе достоинства ко-симуляции и самопроверяющих тестов. Поскольку спецификации описывают поведение тестируемого компонента при всевозможных сценариях взаимодействия с ним, тестовую последовательность можно генерировать автоматически. Разработать декларативные спецификации часто бывает проще, чем исполнимую модель, используемую для ко-симуляции. Важно отметить, что декларативные спецификации можно разрабатывать поэтапно, последовательно добавляя утверждения, описывающие еще не специфицированные требования на тестируемый компонент, что сокращает время, необходимое для получения первых тестов.
Методы формальной спецификации
Формальные спецификации имеют большое значение для тестирования, поскольку позволяют автоматизировать проверку правильности поведения тестируемого компонента — чтобы найти ошибку нужно не только построить тестовую последовательность, которая воссоздает ошибочную ситуацию, но и понять на основе анализа поведения тестируемого компонента, что это поведение действительно является ошибочными. Формальные спецификации особенно важны, когда тестируемая система реализует сложное поведение — вынести вердикт в таких случаях бывает довольно трудно и может занять много времени. Именно к таким системам относятся микропроцессоры с конвейерной архитектурой. При их тестировании необходимо учитывать возможность параллельного выполнения стадий разных инструкций и наличие в конвейере блокировок.
Самым часто используемым на практике способом спецификации микропроцессора является его прототипирование на языке программирования. Прототип микропроцессора, полностью реализующий его систему команд, называется симулятором. Симуляторы бывают двух типов: симуляторы уровня инструкций (instruction-level simulators) и потактово точные симуляторы (cycle-accurate simulators). Симуляторы первого типа реализуют последовательное выполнение инструкций микропроцессора, второго — учитывают выполнение инструкций на конвейере. Симуляторы используются на этапе архитектурного проектирования и для проверки правильности поведения микропроцессора при системном тестировании с помощью тестовых программ.
Также для спецификации микропроцессоров используются языки описания архитектуры (ADLs, Architecture Description Languages) [59]. Основным назначением таких языков является проведение исследований альтернатив дизайна (DSE, Design Space Exploration). Их также используют для генерации платформо-зависимых частей компиляторов, отладчиков и компонентов операционных систем. Важной, но реже используемой областью применения таких языков является автоматическая генерация RTL-моделей и симуляторов микропроцессоров.
Языки описания архитектуры разделяются на языки описания структуры (structural ADLs), языки описания поведения (behavioural ADLs) и языки смешанного описания (mixed ADLs). Языки описания структуры описывают архитектуру микропроцессора в терминах компонентов и связей между ними. Языки описания поведения описывают микропроцессор в терминах системы команд. Языки смешанного описания описывают и структуру, и систему команд микропроцессора.
Как правило, языки описания структуры позволяют разрабатывать описания архитектуры микропроцессора, которые можно синтезировать в логическую схему или транслировать в RTL-модель, но они не описывают явно систему команд микропроцессора. Примерами языков описания структуры являются MIMOLA (Machine Independent Microprogramming Language), разработанный в Дортмундском университете (University of Dorthmund) (1976 г.) и UDL/I (Unified Design Language for Integrated circuits), разработанный в Университете о. Кюсю (Kuyshu University) (1990 г.).
Языки описания поведения также называют языками описания системы команд, поскольку они явно описывают инструкции микропроцессора: семантику, ассемблерный формат и отображение в объектный код. Языки данной группы игнорируют структурные детали микропроцессора и не имеют средств детального описания конвейера и процесса выполнения инструкций на нем. Такие языки обычно предназначены для настраиваемой компиляции. Примерами языков описания поведения являются nML, разработанный в Берлинском техническом университете (Technical University of Berlin) (1990 г.) и ISDL (Instruction Set Description Language), разработанный в Массачусетском технологическом институте (Massachusetts Institute of Technology) (1997 г.).
Языки смешанного описания позволяют описывать как структурную, так и поведенческую составляющие микропроцессора, что делает их более универсальными. Языки смешанного описания предназначены для автоматической генерации симуляторов микропроцессоров, они содержат явное описание конвейера с
возможностью определения зависимостей между инструкциями и блокировок. Примерами языков смешанного описания являются EXPRESSION, разработанный в Калифорнийском университете г. Ирвин (University of California, Irvine) (1999 г.) и LISA (Language for Instruction Set Architecture), разработанный в Аахенском технологическом университете ("Rheinisch-Westfalischen Technischen Hochschule" Aachen University of Technology) (1996 г.).
Для формальной спецификации на модульном уровне используются языки программирования и языки утверждений. Языки программирования позволяют разработать программную модель модуля и использовать ее для оценки правильности его поведения. Языки утверждений позволяют описывать отдельные свойства модуля в виде формул темпоральной логики линейного времени (LTL, Linear Temporal Logic) и/или темпоральной логике ветвящегося времени (CTL, Computation Tree Logic) [60]. К таким языкам относятся OpenVera Assertions (OVA) [28], SystemVerilog Assertions (SVA) [31] и Property Specification Language (PSL) [37]. Языки, по крайней мере, по частії спецификации, имеют следующие корни: ForSpec, разработанный в Intel, (для языков, использующих LTL13) [61] и Sugar, разработанный в IBM, (для языков, использующих логику CTL) [62].
Логика CTL используется преимущественно для формальной верификации систем. Для целей симуляции и тестирования больший интерес представляет логика линейного времени LTL. Языки утверждений оперируют с ограниченными по времени последовательностями событий, в которых можно обращаться к прошлому и будущему. Из простых последовательностей можно строить более сложные с помощью логических связок, таких как И и ИЛИ, или используя регулярные выражения. В подходе на основе утверждений упор делается на временную декомпозицию операций. Для каждой операции выделяется ее временная структура — допустимые последовательности событий и задержки между ними.
Многие работы по тестированию модулей микропроцессоров используют статический анализ кода реализации для извлечения информации об управляющей логике модуля. К таким работам относится работа Ричарда Хо (Richard Но), Хана Янга (Han Yang), Марка Хоровица (Mark Horowitz) и Дэвида Дилла (David Dill) из Лаборатории компьютерных систем Стэнфордского Университета (Computer Systems Lab, Stanford University) (1995 г.) [19]. Дополнительную информацию о методе можно найти в работе [63] и диссертации Ричарда Хо (1996 г.) [35]. В работе предлагается Вариант логики LTL, используемый в языке ForSpec, называется FTL (ForSpec Temporal Logic). следующая методология, ориентированная на создание "крайних случаев" в работе микропроцессора. На первом шаге транслятор автоматически преобразует КОД на языке Verilog, снабженный аннотациями пользователя, в автоматную модель на расширении языка Mmtp (называемом Synchronous Миг93). На втором шаге генерируется полный граф состояний автоматной модели. Наконец, на последнем) третьем шаге генерируется тестовая последовательность на основе обхода графа состояний. Если быть более точным, обход разбивается на маршруты, начинающиеся из начального состояния управления, что позволяет распараллелить тестирование # упрощает перезапуск тестов для поверки корректности исправления ошибок. Подход был успешно применен к конвейерному двухканальному (dual-issue) микропроцессору? основанному на архитектуре DLX14, входящему состав контроллера MAGIC (часть проекта "Stanford FLASH Multiprocessor" [64]). В результате было найдено несколько ошибок, возникающих в "крайних случаях". Предлагаемая методология может использоваться как для тестирования отдельных модулей, так и для тестирования; несложных микропроцессоров. Достоинством метода является направленный перебор внутренних взаимодействий внутри тестируемого компонента. Недостатком, как й других подходов на основе статического анализа кода реализации, является сложность масштабирования.
Другими работами, в которых используется статический анализ, являются работы Диноса Мунданоса (Dinos Moundanos), Джэкоба Абрахама (Jacob Abraham) из Университета Техаса г. Остин (University of Texas, Austin) и Ятина Хоскоута (Yatin Hoskote) из компании Intel (1995-1998 гг.) [65]-[67]. Исследователи отмечают, что большинство ошибок на ранних стадиях проекта включают только управляющую логику компонента. Они автоматически извлекают автоматную модель потока управления тестируемого компонента (ECFM, Extracted Control Flow Machine), на основе которой решаются задачи тестирования. Исследователи отмечают, что такое извлечение является сложной задачей, решение которой основано на эвристиках. Полученная модель может использоваться для оценки уровня тестового покрытия, достигаемого существующими тестами; на ее основе можно генерировать тестовые последовательности, покрывающие не достигнутые тестовые ситуации; также с ее помощью можно генерировать тесты, покрывающие все состояния и переходы ECFM. Для генерации тестовой последовательности используются техники проверки моделей (см. раздел "Формальная верификация микропроцессоров ).
Тестирование на основе контрактных спецификаций конвейера
Ниже предлагается метод определения тестового покрытия, который основан на его декомпозиции на тестовые ситуации и зависимости. Метод позволяет описывать тестовое покрытие в неизбыточной форме — определяются лишь базовые элементы покрытия (тестовые ситуации для отдельных операций и зависимости для пар операций), построение всех достижимых ситуаций в работе модуля осуществляется автоматически в процессе тестирования путем композиции базовых элементов покрытия.
Тестовые ситуации и зависимости
Тестовые ситуации представляют собой ограничения на значения входных параметров стимулов и контекст контрактной спецификации конвейера. Зависимости задают ограничения на значения входных параметров для пары стимулов. Основной интерес при тестировании микропроцессорных модулей с конвейерной организацией представляют зависимости, которые влияют на блокировки конвейера. Как правило, блокировки осуществляются при попытке обращения разных операций к одному и тому же ресурсу. Дадим формальные определения тестовой ситуации и зависимости. Определение 70. Тестовой ситуацией для стимула х называется произвольный предикат ф, определенный на множестве Domx х Domusex и не противоречащий предусловию ргех. ш Рассмотрим тактовый стимул т. Поскольку гпТ = 0 и useT = 0, для тактового стимула можно определить одну единственную тестовую ситуацию, тождественно равную true. Определение 71. Зависимостью для пары стимулов (х,у) называется произвольный предикат х определенный на множестве Domx X Domy и не противоречаиі,ий предикату ргех Л ргеу. ш
Заметим, что здесь не рассматриваются контекстные зависимости — зависимости, для определения которых используется контекст. Такого рода зависимости возникают при косвенной адресации, однако на модульном уровне они встречаются редко.
Если рассмотреть произвольную зависимость d для пары стимулов (х,у), то стимул х называется зависимым, а стимул у — определяющим, при этом говорят, что d является зависимостью стимула х от стимула у.
Определение 72. Множество тестовых ситуаций S для стимула х называется ПОЛНЫМ, если РГСХ Л (Vi/ 6 Ф) — Ргех- Полнота множества тестовых ситуаций означает, что оно полностью покрывают область определения стимула, т.е. для любой пары (р, и) Є Domx х Domusej., удовлетворяющей условию ргех(р, и) = true, существует тестовая ситуация -ф, такая что ф(р, и) = true. Определение 73. Множество зависимостей D для пары стимулов (х,у) называется полным, если (ргех Л ргеу) Л (VX6 х) = Ргех Л ргеу. ш Полнота множества зависимостей означает, что для любых двух пар (pi ,v{) Є Domx x DomUSCx и ( 2,) Є Domy x Domusey, удовлетворяющих условию prex(pi,vi) Л ргеу{р2,ь 2) = true, существует зависимость Xi такая что x(Pi P2) = true. Определение 74. Множеством тестовых ситуаций называется отображение S, которое каждому стимулу х ставит в соответствие множество S{x) тестовых ситуаций для этого стимула, и Определение 75. Множеством зависимостей называется отображение D, которое каждой паре стимулов [х, у) ставит в соответствие множество D(x, у) зависимостей для этой пары стимулов, я
В дальнейшем будем использовать обозначение D(x) = \Jyex D(x,y). Множество D(x) называется множеством зависимостей для стимула х. Определение 76. Множество тестовых ситуаций S называется полным, если для любого стимула х множество тестовых ситуаций S(x) является полным, я Определение 77. Множество зависилюстей D называется полным, если для любой пары стимулов (х,у) множество зависимостей D(x,y) является полным, я
Будем считать, что для контрактной спецификации конвейера задано множество тестовых ситуаций S и множество зависимостей D, которые являются полными.
Определение 78. Множеством зависимостей стимула х от состояния управления 7г называется отображение d, которое каждому состоянию обработки (у, к) ТГ ставит в соответствие зависимость d(x,(y,k)) Є D(x,y). я
Множество, состоящее из всевозможных множеств зависимостей стимула х от состояния управления 7Г, будем обозначать символом D(X,TT).
Определение 79. Множеством зависимостей состояния управления тг называется отображение d, которое каждой паре состояний обработки (х, I) ф (у, к) Є тг ставит в соответствие зависимость d((x,l),(y,k)) D(x,y). ш
Множество, состоящее из всевозможных множеств зависимостей состояния управления 7Г, будем обозначать символом D(TT). Очевидно, что каждое множество зависимостей d Є D(TT) можно представить в виде следующего объединения: d= U d\{(x,l)}x(n\{(,x,l)}) (х,г)єтг
Определение 80. Отображение {(а;,()}х(7г\{(а;,0}) называется множеством зависимостей состояния обработки (ж, /) Є 7г от состояния управления ТТ. ш Для краткости отображение {(іс,/)}х(7г\{(х,г)}) будем обозначать символом d(x,l). Введем также следующие обозначения, которые будут использоваться в дальнейшем: D(x,PL) Цг Даг.тг) D(X,PL) dM \JxeXu{T}D{x,PL) D{PL) & \J PLD{-K) Описание тестовых ситуаций и зависимостей
Рассмотрим способ представления тестовых ситуаций и зависимостей, используемый в предлагаемом методе генерации тестовой последовательности. Для удобства описания тестовых ситуаций и зависимостей в нем используются неопределенные значения: предполагается, что домен каждой переменной расширен специально выделенным неопределенным значением ±3. Дадим несколько вспомогательных определений.
Повторное использование спецификаций и тестов
В рассматриваемом методе для генерации тестовых программ используется формальная спецификация микропроцессора. Спецификация является описанием структуры микропроцессора и его системы команд. Описание, будучи формальным, позволяет генератору автоматически анализировать спецификацию и использовать результаты анализа при построении тестовых программ. В процессе генерации спецификация отражает текущее состояние микропроцессора. Состояние спецификации позволяет контролировать предусловия инструкций и корректно подготавливать тестовые ситуации. Заметим также, что состояние спецификации можно использовать для построения самопроверяющих тестов, т.е. тестов, в которых после каждого тестового воздействия располагается тестовый оракул — программа, осуществляющая проверку правильности выполнения тестового воздействия микропроцессором.
Формальная спецификация микропроцессора включает в себя спецификацию подсистем, спецификацию типов данных и спецификацию системы команд. Рассмотрим каждую из перечисленных составляющих.
Спецификация подсистем описывает основные блоки микропроцессора: регистры, буфер трансляции адресов, кэш-память и др. Основное назначение спецификации подсистем заключается в описании структуры состояния микропроцессора — это фундамент, на основе которого осуществляется спецификация системы команд, зависимостей и тестовых ситуаций. Следует отметить, что уровень абстракции, на котором описываются подсистемы микропроцессора, может варьироваться в зависимости от целей тестирования. Например, при описании кэш-памяти можно не включать в спецификацию хранящиеся в кэше данные, а описывать только тэги данных — этого достаточно для того, чтобы проверять и подготвливать такие тестовые ситуации, как попадание или промах в кэш-память.
Важной составной частью спецификации подсистем микропроцессора является спецификация регистров. Спецификация регистров вводит на множестве регистров микропроцессора систему типов: регистры общего назначения, системные регистры, регистры модуля арифметики с плавающей точкой и др. Особая роль этого вида спецификации связана с тем, что регистры являются основным способом передачи значений параметров инструкциям и получения результата их выполнения. При описании инструкций указываются типы их регистров; эта информация используется генератором для автоматического построения зависимостей по регистрам.
Разные инструкции микропроцессора определены над данными разных типов: одни — над 32-х битными словами, другие — над двойными словами; одни инструкции требуют, чтобы значение операнда являлось числом с плавающей точкой, другие — чтобы оно было виртуальным адресом и т.д. Формальная спецификация типов данных описывает множество типов данных микропроцессора и отражает совместимость различных типов данных между собой. Как правило, микропроцессоры имеют достаточно простую систему типов: байт, полуслово, слово, двойное слово, числа с плавающей точкой одинарной и двойной точности, виртуальный адрес и некоторые другие.
При описании инструкций указываются типы данных их операндов. Эта информация используется генератором при построении зависимостей между инструкциями. В частности, зависимость по регистрам типа "определение использование" возможна только в том случае, если типы выходного и входного регистров совместимы. Например, регистр, содержащий результат 32-х битной операции ADD, можно использовать в качестве операнда 64-х битной операции DSUB, но не наоборот.
Формальная спецификация системы команд содержит основную информацию, с которой работает генератор тестовых программ: интерфейс, семантику и ассемблерный формат инструкций микропроцессора. Описание интерфейса используется генератором при построении зависимостей между инструкциями, на основе описания семантики генератор обновляет состояние спецификации; ассемблерный формат используется при отображении внутреннего представления тестовых программ в файлы на языке ассемблера. Описание отдельной инструкции микропроцессора включает в себя следующие составляющие: интерфейс инструкции — описывает операнды инструкции: для каждого операнда указывается его имя, способ передачи значения (непосредственно или через регистр, в последнем случае также указывается тип регистра), тип данных и информация о том, является операнд входным или выходным; предусловие инструкции — определяет ситуации, в которых определено поведение микропроцессора при выполнении данной инструкции. Предопределенной частью предусловия является проверка совместимости значений входных операндов соответствующим типам данным; функция вычисления значений выходных операндов — вычисляет значения выходных операндов инструкции по значениям входных операндов, а также исключения, возникающие при выполнении инструкции; функция обновления состояния микропроцессора — обновляет состояние спецификации на основе значений входных операндов инструкции и текущего состояния; ассемблерный формат инструкции — определяет формат записи инструкции и ее операндов на языке ассемблера.
Отметим, что семантика инструкции описывается двумя функциями: функцией вычисления значений выходных операндов и функцией обновления состояния микропроцессора. Первая функция используется, когда при конструировании тестовой ситуации требуется определить значения зависимых операндов соответствующей инструкции. Эти значения нельзя получить из состояния спецификации, поскольку конструирование тестовой ситуации осуществляется до обновления состояния предшествующими инструкциями тестового воздействия (они будут выполнены только после выполнения программ подготовки тестовых ситуаций всех инструкций тестового воздействия). Вторая функция, как видно из названия, используется для обновления состояния микропроцессора.
Спецификация системы команд микропроцессора разрабатывается на основе анализа документации. Современные руководства содержат детальные описания инструкций, которые могут быть легко формализованы. Для примера, рассмотрим еще раз фрагмент описания инструкции ADD из системы команд MIPS64 [109]
