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

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

.

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

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

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

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

1Pentium — торговая марка нескольких поколений микропроцессоров семейства х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 Управляющей логикой конвейера или просто управляющей логикой называется внутренняя функциональность микропроцессора, отвечающая за планирование и организацию выполнения инструкций.

4NOP или NOOP (No Operation) — специальная инструкция микропроцессора, которая не производит никаких действий и обычно используется для временных задержек и выравнивания памяти.

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

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

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

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

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

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

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

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

Приведенный выше анализ ошибок относится к середине 1990;ых гг., но следует отметить, что ошибки в управляющей логике и по сей день являются одними из самых сложных для обнаружения. Например, список ошибок, датируемый 2006 г., широко используемого в аэрокосмической промышленности микропроцессора TSC695 °F компании 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 г.);

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

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

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

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

.

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

Заключение

.

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

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

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

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

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

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

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

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