Встречное тестирование высокопроизводительных микропроцессоров тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Чибисов, Петр Александрович

• Чибисов, Петр Александрович
• кандидат наук
• 2013

Оглавление диссертации кандидат наук Чибисов, Петр Александрович

СОДЕРЖАНИЕ

ВВЕДЕНИЕ

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

1.1 Обзор методов функциональной верификации

ЯТЬ-моделей разрабатываемых микропроцессоров

1.2 Обзор методов, применяемых для верификации

с использованием ПЛИС-прототипа

1.3 Обзор методов тестирования СБИС микропроцессоров

и их тестовых кристаллов

1.4 Метрики тестового (функционального) покрытия, применяемые при верификации моделей

1.5 Анализ текущего состояния проблемы

1.6 Постановка задачи для верификации разрабатываемых микропроцессоров повышенной надежности для

ответственных применений

ГЛАВА 2 МЕТОДИКА ТЕСТИРОВАНИЯ МИКРОПРОЦЕССОРОВ И ИХ ЯТЬ-МОДЕЛЕЙ СУЩЕСТВУЮЩИМ ПО ПОЛЬЗОВАТЕЛЯ

ПОД ОС

2.1 Методика тестирования существующим ПО под ОС на

разных уровнях абстракции модели

2.1.1 Этап 1: ЯТЬ-модель ядра микропроцессора

2.1.2 Этап 2: ЯТЬ-модель системы на кристалле

2.1.3 Этап 3: ПЛИС-прототип

2.1.4 Этап 4: тестовый кристалл, серийно выпускаемая

СБИС процессора

2.1.5 Функциональные ошибки микропроцессоров

2.2 Выбор репрезентативного набора тестов

2.3 Динамическое имитационное моделирование

(ко-симуляция) тестовых программ

2.4 Разбиение трасс объемных тестов на подпоследовательности

для параллельного выполнения

2.5 Методика поиска и локализации ошибок в ПЛИС,

тестовом кристалле

ГЛАВА 3 МЕТОД ПОВЫШЕНИЯ КАЧЕСТВА ТЕСТИРОВАНИЯ МИКРОПРОЦЕССОРОВ (ВСТРЕЧНОЕ ТЕСТИРОВАНИЕ) ДЛЯ ВЫДЕЛЕННОГО КЛАССА ЗАДАЧ

3.1 Фазы тестирования

3.2 Классификация и анализ задач пользователя

3.3 Количественное определение полноты тестирования

3.3.1 По графику вероятности возникновения ошибок

3.3.2 По покрытию тестами требований для конкретных

задач пользователя

3.3.3 По значениям функционального покрытия и покрытия кода, получаемым от САПР

3.3.4 Верификация, управляемая метриками тестового покрытия

3.3.5 Критерии готовности проекта к передаче в изготовление

3.4 Методика выбора набора тестов, учитывающая специфику определенного класса задач

3.5 Исследовательская модель пространства покрытия

3.6 Выбор метрик функционального покрытия инструкций МП

3.7 Примеры метрик функционального покрытия для суперскалярного микропроцессора

ГЛАВА 4 РЕЗУЛЬТАТЫ ПРИМЕНЕНИЯ РАЗРАБОТАННЫХ МЕТОДИК НА ПРАКТИКЕ

4.1 Опыт применения разработанных методик на практике

4.2 Спецификация верифицируемых микропроцессоров

4.3 Встречное тестирование микропроцессоров ВМ5, ВМ6, ВМ9

4.4 Результаты применения разработанных методик

ЗАКЛЮЧЕНИЕ

ЛИТЕРАТУРА

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

ВВЕДЕНИЕ

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

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

Непрерывное стремление за повышением производительности вместе с требованием сохранения программной совместимости приводят к неизбежному усложнению микропроцессоров и, соответственно, к появлению всё новых и новых ошибок. Так, по данным на апрель 2005 года у микропроцессора PENTIUM 4 [2] ошибок и несоответствий документации -100, не исправлено - 49, не будут исправляться - 40, неизвестны пути обхода

- 22. В микропроцессоре Intel Core i7-600 на декабрь 2011 г. найдено уже 123 ошибки, из которых не планируется исправлять 118, неизвестны пути обхода

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

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

Верификация проекта до изготовления первого тестового образца основывается, главным образом, на проведении динамического имитационного моделирования на разных уровнях абстракции. Несмотря на высокую степень завершенности проекта на этой стадии и использование колоссальных вычислительных ресурсов, невозможно гарантировать, что все ошибки проекта были исправлены до отправки проекта в производство. Основная причина - относительно небольшое количество функциональных тестовых сценариев, которое может быть выполнено во время верификации ЯТЬ-мод ели. Статистические данные показывают, что 12% пропущенных ошибок в проекте переходят в первые кремниевые прототипы [4], и почти 50% СБИС микропроцессоров требуют дополнительного незапланированного перезапуска в производство [5].

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

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

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

Все методы верификации моделей RTL-уровня можно разделить на формальные и динамические. Формальные методы позволяют математически доказать правильность работы какого-либо блока микропроцессора, но являются крайне трудоемкими. Например, при разработке микропроцессора Pentium 4 фирмой Intel была проведена формальная верификация модуля вещественной арифметики (FPU), модуля декодирования инструкций, а также модуля динамического планирования потока инструкций. При этом на работу было затрачено 60 человеко-лет [6].

Динамические методы верификации (имитационное тестирование) моделей микропроцессоров широко применяются для верификации RTL-моделей. Как правило, качество (полноту) тестирования оценивают по величине покрытия кода разрабатываемой RTL-модели (так называемое структурное покрытие). Однако даже 100% покрытия не гарантирует отсутствие ошибок.

С ростом сложности современных микропроцессоров и систем на кристалле роль, отводимая процессу верификации в маршруте проектирования, очевидно, будет расти. При проектировании микропроцессоров специального назначения процесс разработки аппаратной и программной частей происходит, как правило, одновременно. При этом алгоритмы программ могут оптимизироваться под аппаратуру для повышения реальной (в отличие от пиковой) производительности, и наоборот, создаваемая аппаратура учитывает назначение комплекса и особенности возможных программ пользователей. Такой подход известен как «встречная оптимизация» аппаратно-программных комплексов. Поскольку на начальных

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

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

Объектом исследования является RTL-модель проектируемого микропроцессора, тестовая СБИС микропроцессора, а также процесс их функциональной верификации.

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

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

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

2. разработать методику тестирования микропроцессоров и их RTL-моделей существующим пользовательским программным обеспечением (ПО) под операционной системой (ОС) Linux;

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

для выделенного класса пользовательских задач и повышения производительности микропроцессоров.

Научная новизна исследования

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

1. методика запуска кода готовых приложений под ОС, а также загрузки самой ОС на ранних стадиях проектирования ШЪ-модели;

2. метод тестирования микропроцессора с привлечением контрольных задач от потенциальных пользователей («встречное» тестирование);

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

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

Разработанные автором методы и методики использованы при проектировании в НИИСИ РАН микропроцессоров 1890ВМ5Ф, 1890ВМ6Я, а также успешно используются для выполнения ОКР «Процессор-5» и «Процессор-6» для создания микропроцессоров 1890ВМ8Я и 1890ВМ9Я. Благодаря комплексному применению созданных средств тестирования в серийно выпускаемых вычислительных системах на базе микропроцессоров 1890ВМ5Ф и 1890ВМ6Я не выявлено ни одной ошибки в выделенных областях применения. Результаты работы могут использоваться в НИИ системных исследований РАН, ЗАО «МЦСТ», ФГУП НИИМА «Прогресс», а также в других научных и промышленных организациях, занимающихся разработкой высокопроизводительных микропроцессоров.

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

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

• VI, VII, IX и XIII научно-технические конференции "Электроника, Микро- и Наноэлектроника" (г. Нижний Новгород, 2004, 2005, 2007, 2011 гг.);

« Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС-2005, 2010, 2012, г. Истра Московской области);

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

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

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

Структура и объем работы

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

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

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

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

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

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

Третья глава посвящена предлагаемому автором методу улучшения качества тестирования микропроцессоров («встречное» тестирование) для выделенного класса пользовательских задач. Фактически, метод является развитием подхода ко-верификации для микропроцессоров повышенной

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

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

ГЛАВА 1

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

МИКРОПРОЦЕССОРОВ

1Л Обзор методов функциональной верификации RTL-моделей разрабатываемых микропроцессоров

Разработка микропроцессора - это многоуровневый и многостадийный процесс [21], включающий в себя такие этапы, как: утверждение архитектурной модели, разработка кода RTL-модели (RTL, Register-Transfer Level, модель на уровне регистровых передач) на языке описания аппаратуры (HDL, Hardware Description Language), разработка эталонной модели («golden model», образцовый эмулятор) на языке C/C++, логическое и физическое проектирование, размещение и трассировка, изготовление кристалла СБИС микропроцессора. Проектирование современных высокопроизводительных микропроцессоров проводится по определенному маршруту, при этом от абстрактных текстовых документов, содержащих спецификации архитектуры, техническое задание и прочие требования к создаваемой СБИС, разработчики переходят к менее абстрактным уровням представления проекта. Уровни абстракции воплощаются последовательно в формальной спецификации архитектуры (поведенческое проектирование), в RTL-коде (детальное проектирование), в списке соединений (gate-level net list) (уровень логических вентилей), и в итоге проходят физический синтез (уровень транзисторов), за которым следует изготовление фотошаблона проекта и производство интегральной схемы (рис. 1.1).

Рис. 1.1. Маршрут проектирования современных микропроцессоров

Верификация микропроцессора (или его модели) - это процесс обеспечения соответствия моделей на различных уровнях абстракции. Этап создания ЯТЬ-модели характеризуется минимальной автоматизацией процесса, так как разработчики НЕ)Ь-кода творчески реализуют свои представления о том, как те или иные функции либо технические требования воплотить в виде функциональных блоков кода. Наибольшее количество ошибок вносится в проект именно на этой стадии проектирования (из-за неверной интерпретации спецификации, опечаток в коде, несогласованности интерфейсов блоков, неверно заданных временных характеристик логических сигналов и тому подобное). В связи с этим именно функциональной верификации уделяется большее количество времени, ресурсов, средств.

Современные ЯТЬ-модели микропроцессоров содержат множество одновременно (параллельно) взаимодействующих друг с другом независимых конечных автоматов. Кроме того, сам НЕ)Ь-код в силу своей специфичности обладает высокой степенью параллелизма (все регистровые пересылки, которые должны произойти по фронту тактового сигнала, совершаются одновременно), а также при наличии нескольких различных тактовых сигналов - асинхронностью, что лишь повышает сложность и вместе с тем важность функциональной верификации ЯТЬ-модели проекта.

Функциональная верификация — это процесс установления эквивалентности (соответствия) между реализацией модели и её функциональными требованиями (спецификацией).

Выделяют два основных уровня верификации микропроцессора или его ЯТЬ-модели с точки зрения объекта верификации: модульный и системный. Объектом системной верификации является модель микропроцессора в целом. В качестве входных стимулов используются инструкции из системы команд микропроцессора.

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

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

Вне зависимости от уровня (модульный или системный) методы функциональной верификации, применяемые для проверки моделей, можно разделить на два основных класса: методы динамической верификации, основанные на имитационном тестировании (simulation-based verification) и методы формальной верификации (formal verification). Объектом динамической верификации является RTL-модель разрабатываемой системы. Объектом формальной верификации является формальная статическая модель, построенная на основе формализации спецификаций.

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

Верификация, основанная на динамическом имитационном моделировании

Формальная верификация

property 1

о

Р V О

Проверенные

свойства

О

О sf^

W -(J

|S ^ ^ property 2

lit' О О

Рис. 1.2. Различие в подходах динамической и формальной верификации

Динамическая верификация предполагает проведение имитационного моделирования верифицируемой модели микропроцессора (симуляции) и проверку результатов моделирования на соответствие тем или иным образом описанным требованиям. Для проверки результатов моделирования может быть использован образцовый эмулятор. Обычно создается некоторая автоматизированная тестовая система (testbench), которая создает тестовые воздействия и проверяет реакции модели. Часто динамическую верификацию называют просто тестированием. Таким образом, тестирование - это процесс выполнения тестовой программы с целью обнаружения ошибки; тестирование - это один из видов верификации.

На рис. 1.2 показана принципиальная разница между динамической и формальной верификацией, с подчеркиванием того факта, что при динамическом моделировании происходит проверка отдельных контрольных точек модели (операторов) при изменении входного состояния (при подаче входных векторов), а при формальной верификации проверки происходят на уровне свойств (propertiesj, при этом проверка функциональности осуществляется группами, содержащими множество контрольных точек [22].

Так как тестирование базируется на рассмотрении только небольшого подмножества возможных примеров поведения системы, оно никогда не

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

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

Следует отметить также, что ход работ по функциональной верификации разделяется на этапы до и после создания первого кремниевого кристалла (прототипа) СБИС. Так, на этапе до создания тестового кристалла (pre-silicon verification) в качестве объекта используется RTL-модель, на которой с помощью симуляции запускаются тестовые программы. После создания прототипа в кремнии (тестовый кристалл СБИС) объектом верификации (верификация на кристалле, post-silicon verification) становится тестовый кристалл, на котором проводится тестирование [24].

Помимо термина «верификация», означающего процесс анализа системы или ее компонентов для определения корректности преобразований входного описания на каждой стадии проектирования, в отрасли, связанной с разработкой и созданием микропроцессоров, распространен термин «валидация». Вапидация - это процесс определения работоспособности системы и ее компонентов путём проверки соответствия требованиям спецификации после выполнения каждой стадии проектирования. Взаимосвязь ключевых понятий, связанных с разработкой и верификацией микропроцессоров, показана на рис. 1.3 [25].

Верификация описания

Функциональная верификация

Верификация логического описания

Физическая верификация

Верификация готовой СБИС

С![Логический синтез^}

1 г

Логическое описание

1

С^Физический синтез^

1 г

Топология ИС

1

з гото в л е н ие^^

г

Готовая СБИС

о;

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

Около десяти лет назад функциональная верификация микропроцессора, а также его тестирование, рассматривались как отдельные от процесса разработки стадии (рис. 1.4), к которым приступали после завершения проектирования; в настоящее время процесс верификации интегрирован в процесс разработки и ведётся параллельно на всех стадиях (рис. 1.5).

Архитектурное проектирование

Спецификация * аппаратуры Создание RTL-модели Отладка Синтез Изготовление Лабораторная отладка

Верификация спецификации Верификация тестового окружения и модулей 4 Верификация ¡модульная и системная

Спецификация прикладного ПОл. Разработка программного обеспечения! ' Отладка ПО

Первая интеграция

Рис. 1.4 Независимая разработка аппаратной и программной частей системы на кристалле

Архитектурное проектирование

^JZT С0ГПГТЬ 0™адка Синтез Изготовление аппаратуры модели " Лабораторная отладка

5S - ч ^Верификация модульная и системная

Спецификация прикладного ПО Разработка программного обеспечения Отладка программного обеспечения

Первая интеграция

Финальная интеграция

Рис. 1.5. Совместная разработка аппаратной и программной частей системы на кристалле (ко-верификация)

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

Методы, основанные на имитационном тестировании RTL-модели (simulation-based verification) с помощью программ-симуляторов, являются самыми распространенными на сегодняшний день. Это объясняется в первую очередь относительной простотой первоначальной настройки тестового окружения и гибкостью его использования. Кроме того, на рынке имеется

множество САПР различных фирм (Cadence, Mentor Graphics, Synopsys), поддерживающих стандартные языки описания аппаратуры, таких как Verilog [26] и VHDL [27]. К тому же, в настоящее время многие инструменты поддерживают более высокоуровневые поведенческие модели, описываемые на стандартных языках (ANSI C/C++), либо на языках, расширяющих базовую функциональность с точки зрения возможностей для верификации, таких как SystemC [28], SystemVerilog [29], язык е [30]. Также, в процессе развития данных методов моделирования появились средства для автоматизированного сбора покрытия кода и функционального покрытия с помощью таких расширений, как язык SystemVerilog Assertions (SVA) [31], являющийся подмножеством языка SystemVerilog.

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

Список литературы диссертационного исследования кандидат наук Чибисов, Петр Александрович, 2013 год

ЛИТЕРАТУРА

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

2. Материалы компании Intel. Pentium 4 Processor Specification. Update № 249199-059, 2005.

3. Материалы компании Intel. Intel® Core™ i7-600, i5-500, i5-400 and i3-300 Mobile Processor Series. Specification Update №322814, December 2011.

4. Hakim N. Introduction to Post-silicon Validation, presentation. Intel Corp. 2010.

5. Adir A. et al. A Unified Methodology for Pre silicon Verification and Postsilicon Validation. // In АСМЛЕЕЕ Design, Automation & Test in Europe Conference (DATE), 2011.

6. Bentley B. Validating A Modern Microprocessor // Proc. of 17th International Conference on Computer Aided Verification, 2005. pp. 2-4.

7. Чибисов П.А., Николина H.B. Функциональная верификация RTL-модели суперскалярных микропроцессоров. Электроника, микро- и наноэлектроника // Сборник научных трудов. М.: МИФИ, 2004. С. 213216.

8. Аряшев С.И., Николина Н.В., Чибисов П.А. Тесты аттестации архитектуры RTL-модели 64-разрядного суперскалярного микропроцессора // Проблемы разработки перспективных микроэлектронных систем - 2005. Сборник научных трудов / под общ. ред. А.Л.Стемпковского. М.:ИППМ РАН, 2005. С. 257-262.

9. Аряшев С.И., Краснюк А.А., Чибисов П.А. Адаптация тестов для оценки производительности 64-разрядного универсального суперскалярного микропроцессора // Проблемы разработки перспективных микроэлектронных систем - 2005. Сборник научных трудов / под общ. ред. А.Л.Стемпковского. М.:ИППМ РАН, 2005. С. 263-268.

10. Аряшев С.И., Зубковский П.С., Николина Н.В., Чибисов П.А. Основные подходы к верификации блока вещественной арифметики // Проблемы

разработки перспективных микроэлектронных систем - 2005. Сборник научных трудов / под общ. ред. А.Л.Стемпковского. М.гИППМ РАН, 2005. С. 269-274.

П.Аряшев С.И., Барских М.Е., Чибисов П.А. Оценка покрытия тестами машин состояний RTL-модели процессора // Электроника, микро- и наноэлектроника. Сборник научных трудов/под ред. В.Я.Стенина.-М.:МИФИ, 2007.

12. Аряшев С.И., Николина Н.В., Чибисов П.А. Этапы тестирования моделей микропроцессора со встроенным системным контроллером. // Электроника, микро- и наноэлектроника. Сборник научных трудов. М: МИФИ, 2007.-С. 179-182.

13. Чибисов П.А., Трубицын Д.А., Баранов C.B. Алгоритмы тестирования памяти при проведении радиационных испытаний микропроцессорного модуля // Проблемы разработки перспективных микро- и наноэлектронных систем - 2010. Сборник трудов / под общ. ред. академика А.Л.Стемпковского. М.:ИППМ РАН, 2010. С. 257-260.

14. Николина Н.В., Зубковский П.С., Чибисов П.А. Сопроцессоры вещественной и комплексной арифметики и их тестирование // Проблемы разработки перспективных микро- и наноэлектронных систем - 2010. Сборник трудов / под общ. ред. академика А.Л.Стемпковского. М.:ИППМ РАН, 2010. С. 360-363.

15. Аряшев С.И., Трубицын Д.А., Чибисов П.А. Оптимизация потребляемого тока, частоты функционирования и напряжения питания суперскалярных 64-разрядных микропроцессоров (на примере 1890ВМ5Ф) // Электроника, микро- и наноэлектроника. Сборник научных трудов. М: МИФИ, 2011.

16. Ровинский Е.В., Чибисов П.А. Запуск ОС Linux как этап функционального тестирования микропроцессоров // Проблемы разработки перспективных микро- и наноэлектронных систем - 2012. Сборник трудов / под общ. ред. академика РАН А.Л. Стемпковского. М.: ИППМ РАН, 2012. С. 125-128.

17. Николина Н.В., Чибисов П.А., Аряшев С.И. Современные тенденции оценки и контроля производительности микропроцессоров на стадии их разработки // Проблемы разработки перспективных микро- и наноэлектронных систем - 2012. Сборник трудов / под общ. ред. академика РАН A.JI. Стемпковского. М.: ИППМ РАН, 2012. С. 489-494.

18. Чибисов П.А. Тестирование микропроцессоров и их RTL-моделей приложениями пользователя под ОС Linux. // Программные продукты и системы, № 3, 2012, с. 112-116.

19. Аряшев С. П., Николина Н. В., Чибисов П. А. Организация регрессионного процесса тестирования RTL-моделей микропроцессоров // Параллельные вычисления и задачи управления. Сборник трудов конференции РАСО'2012, с. 231-237.

20. Бобков С.Г., Чибисов П.А. Повышение качества тестирования высокопроизводительных микропроцессоров методами встречного тестирования с анализом функционального тестового покрытия выделенных приложений. // Информационные технологии, №8, 2013, с.26-33.

21. Бобков С.Г. Методика тестирования микросхем для компьютеров серии «Багет». // Программные продукты и системы, 2007, №3, с.2-5.

22. William К. Lam, Hardware Design Verification Simulation and Formal Method-Based Approaches, Prentice Hall PTR, 2005, 624 p.

23.Вельдер С.Э., Лукин M.A., Шалыто A.A., Яминов Б.Р. Верификация автоматных программ. СПб.: Наука. 2011, 242 с.

24.Rotithor Н. Postsilicon Validation Methodology for Microprocessors // IEEE Design and Test of Computers, October-December 2000 Vol. 17, No. 4, pp. 7788.

25.Balakrishnan S. Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs. Master's thesis, Concordia University, 1999.

26. IEEE Standard Verilog Hardware Description Language. IEEE Std 1364-2005.

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

28.IEEE Standard for Standard SystemC Language Reference Manual. IEEE Std 1666-2011.

29.IEEE Standard for SystemVerilog - Unified Hardware Design, Specification, and Verification Language. IEEE Std 1800-2009

30.IEEE Standard for the Functional Verification Language e. IEEE Std 16472011.

31.Foster H., Krolnik A., Lacey D. Assertion-based design- Second edition. Kluwer Academic Publishers. Springer. 2005. 392 p.

32.Brahme D. et al., The Transaction-Based Verification Methodology. Cadence Berkeley Labs, Technical Report # CDNL-TR-2000-0825, 08.2000.

33. K. Shimizu et al., Verification of the Cell Broadband Engine Processor, in Proceedings of the 43rd Design Automation Conference (DAC'06). San Francisco, California, USA, 2006, pp. 338-343.

34. Obsidian Software, "RAVEN Random Architecture Verification Engine" [электронный ресурс]. URL: http://www.arm.com/community/partners/ display_product/rw/ProductId/5171/(flaTa последнего обращения: 28.08.2013).

35.Bin et al. Using a constraint satisfaction formulation and solution techniques for random test program generation. IBM SYSTEMS JOURNAL, VOL 41, NO 3, 2002.

36.Adir A. et al. Genesys-Pro: Innovations in Test Program Generation for Functional Processor Verification. IEEE Design and Test of Computers, 2004 21(2), pp. 84-93.

37.Naveh Y. et al. Constraint-Based Random Stimuli Generation for Hardware Verification // Al MAGAZINE Vol 28, No 3, 2007.

38. F. Corno, F. Cumani, and G. Squillero, "Exploiting Auto-Adaptive jiGP for Highly Effective Test Programs Generation", in ICES2003: The 5th International Conference on Evolvable Systems: From Biology to Hardware. Trondheim, Norway, 2003, pp. 262-273.

39. G. Squillero, "MicroGP - An Evolutionary Assembly Program Generator". Genetic Programming and Evolvable Machines, vol. 6, pp. 247-263, 2005.

40.Гладков JI. А., Курейчик В. В., Курейчик В. М. Генетические алгоритмы: Учебное пособие. - 2-е изд.- М: Физматлит, 2006.- С.320.

41.0rlov М., Sipper М., Hauptman A. Genetic and Evolutionary Algorithms and Programming. Encyclopedia of Complexity and Systems Science. Springer New York, 2009, pp. 4133^145.

42. A. Cheng and C.C. Lim, "System Test Generation for System-on-Chips using Genetic Evolutionary Methods", in 7th International Conference on Optimization: Techniques and Applications (ICOTA7). Kobe, Japan: Universal Academic Press, Inc., 2007, pp. 1-12.

43. A. Cheng Verification of System-on-Chips using Genetic Evolutionary Test Techniques from a Software Applications Perspective, a thesis, The University of Adelaide, 09.2009.

44. Cheng A., Lim C. Optimizing System-on-Chip Verifications with Multi-Objective Genetic Evolutionary Algorithms School of Electrical and Electronic Engineering. CCL ЛМО, The University of Adelaide, Australia, 2012.

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

46. Andrews J., Co-verification of Hardware and Software for ARM. Elsevier Inc, 2005. ISBN-10: 0750677309.

47. Rosenstiel W., Rapid Prototyping, Emulation and Hardware/Software Co-debugging, in "SYSTEM-LEVEL SYNTHESIS" ed. by A. A.Jerraya and J.Mermet, NATO Science Series, Kluwer Academic Publisher, 1999, pp.219262.

48. Andrews J. Modern simulation acceleration and emulation technology. Cadence Design Systems, Incisive verification article, November 2005.

49. Лохов А. Функциональная верификация СБИС в свете решений Mentor Graphics // ЭЛЕКТРОНИКА: Наука, технологии, бизнес. №1 2004 г. , с.58-62.

50. Кравченко В., Радченко Д. Виртуальное прототипирование для аппаратно-программной верификации СБИС // ЭЛЕКТРОНИКА: Наука, технологии, бизнес. №7 2003г, с. 34-37.

51. Материалы компании Cadence "Accelerated hardware/software co-verification" (White Paper) [электронный ресурс]. URL: http://www.cadence.com/rl/Resources/white_papers/Coverification_wp.pdf (дата последнего обращения: 30.08.2013г.).

52. Rashinkar P., Paterson P., Singh L. System-On-A-Chip Verification -Methodology And Techniques // Kluwer Academic Publishers 2002, New York, - 122p.

53. Ilya Wagner, Valeria Bertacco Post-Silicon and Runtime Verification for Modern Processors, Springer, 2011, 224 p.

54. Adir A. et al. Threadmill: a post-silicon exerciser for multi-threaded processors. In DAC, ACM, 2011, pp. 860-865.

55. Piziali A. Functional verification coverage measurement and analysis. New York: Kluwer Academic Publishers, 2004, 216 p.

56. Hayhurst K.J., Veerhusen D.S., Chilenski J.J., and Rierson L.K. A Practical Tutorial on Modified Condition/Decision Coverage. Report NASA/TM-2001-210876, NASA, USA, May 2001.

57. Синицын C.B., Налютин Н.Ю. Верификация программного обеспечения: Курс лекций. - М.: МИФИ (ГУ), 2006. - 158 с.

58. Майерс Г., Баджетт Т., Сандлер К. Искусство тестирования программ, 3-е издание.— М.: «Диалектика», 2012.— 272с.

59. Канер К., Фолк Д., Нгуен Е. Тестирование программного обеспечения. Фундаментальные концепции менеджмента бизнес-приложений. — К.: ДиаСофт, 2001,— 544с.

60. Kumar J., Ahlschlager С., Isberg P. Post-silicon verification methodology on Sun's UltraSPARC T2. HLDVT IEEE Computer Society -2007, p. 47.

61.Foutris N., Gizopoulos D., Psarakis M., Vera X., Gonzalez A., "Accelerating Microprocessor Silicon Validation by Exposing ISA Diversity", IEEE/ACM

International Symposium on Microarchitecture (MICRO), Porto Alegre, Brazil, Dec. 2011.

62.Mitra S., Nicolici N., "Post-Silicon Validation: Opportunities, Challenges and Recent Advances," IEEE/ACM Design Automation Conference, Anaheim, CA, June 2010 (Invited).

63. Balston K., Karimibiuki M., Hu A. J., Ivanov A., Wilton S. Post-Silicon Code Coverage for Multiprocessor System-on-Chip Designs // IEEE Transactions on Computers, vol. 62, no. 2, Feb. 2013, pp. 242-246.

64. Adir A., Nahir A., Ziv A., Meissner C., Schumann J., "Reaching Coverage Closure in Post-silicon Validation", in Proc. Haifa Verification Conference, 2010, pp.60-75.

65. Bojan Т., Arreola M.A., Shlomo E., Shachar Т., "Functional coverage measurements and results in post-Silicon validation of Core™2 duo family", in Proc. HLDVT, 2007, pp. 145-150.

66. Karimibiuki M., Balston K., Hu A.J., Ivanov A. Post-silicon code coverage evaluation with reduced area overhead for functional verification of SoC, In Proceeding HLDVT '11, pp. 92-97.

67. Linux Test Project. [Электронный ресурс] URL: http://ltp.sourceforge.net/ (дата последнего обращения: 30.08.2013г.).

68. SPEC, SPEC CPU2000 and CPU2006. [Электронный ресурс] URL: http://www.spec.org/ (дата последнего обращения: 30.08.2013г.).

69. Phoronix Test Suite [Электронный ресурс]. URL: http://www.phoronix-test-suite.com/ (дата последнего обращения: 30.08.2013г.).

70.Balston К. FPGA Emulation for Critical-Path Coverage Analysis. PhD Thesis. University Of British Columbia, 2012.

71.Francard R, Posner M Verification Methods Applied to the ST Microelectronics GreenSIDE Project. Design And Reuse, 2006. [Электронный ресурс].

URL: http://www.design-reuse.com/articles/7314/verification-methods-applied-to-

the-st-microelectronics-greenside-project.html (дата обращения: 30.08.2013).

72. Райко Г.О., Рогожкин С.А. Тестирование аппаратного обеспечения на основе СПО. Свободное программное обеспечение - 2010 (СПО-2010): Тезисы докладов Всероссийской конференции / 26-27 октября 2010 г., Санкт-Петербург, СПбГПУ, 2010. - 66 с.

73.Gong L., Lu J. Verification-Purpose Operating System for Microprocessor System-Level Functions // IEEE Design & Test of Computers. 2010, pp. 76-85.

74. Taylor S., Quinn M., Brown D., Dohm N., et al. Functional Verification of a Multiple-issue, Out-of-Order, Superscalar Alpha Processor - the DEC Alpha 21264 Microprocessor // Proceedings of the 35th Design Automation Conference, p. 638.

75. Chang, Y., Lee, S., Park, I., Kyung, C. Verification of a microprocessor using real world applications. // In Proceedings DAC 1999, pp. 181-184.

76. Karimibiuki M. Post-Silicon Code Coverage for Functional Verification of Systems-on-Chip. PhD thesis. University of British Columbia, 2012.

77. Balston K., Karimibiuki M., Hu A., Ivanov A., Wilton S. Post-Silicon Code Coverage for Multiprocessor System-on-Chip Designs. // IEEE Trans. Computers 62(2), 2013, pp. 242-246.

78. Xiao Xi Xu Software-centric and interaction-oriented system-on-chip verification. PhD Thesis, University of Adelaide, 2009.

79.Аряшев С., Корниленко А., Подковыров А. Тестирование моделей микропроцессоров с использованием прототипов, реализованных на ПЛИС. Электронные компоненты №12, 2006. - С. 57-61.

80. Quartus II Handbook v. 13.0, Volume 3: Verification, Chapter 13: Design Debugging Using the SignalTap II Logic Analyzer. Altera Corporation 05.2013. [Электронный ресурс] URL: http://www.altera.com/literature/hb/qts/qts_ qii53009.pdf (дата обращения: 30.08.2013).

81. Т. Venton, М. Miller, R. Kalla, A. Blanchard. A Linux-based tool for hardware bring up, Linux development, and manufacturing // IBM Systems Journal, 2005, Volume 44, Number 2, p.319.

82. Dempster D., Stuart M. Verification Methodology Manual: Techniques for Verifying HDL Designs. Teamwork International, 2002, 208p.

83. Larson P. Testing Linux with Linux Test Project. // In Proceedings of the Ottawa Linux Symposium, July 2002, Ottawa Canada, pp.265-273.

84. Larson P., Hinds N., Franke H., Ravindran R. Improving the Linux Test Project with Kernel Code Coverage Analysis // In Proceedings of the Ottawa Linux Symposium, July 2003, Ottawa Canada, pp.275-290.

85. Buildroot [Электронный ресурс] URL: http://buildroot.uclibc.org/ (дата обращения: 30.08.2013).

86. Vasudevan S. Effective Functional Verification, Principles and Processes. Springer, 2006. 256p.

87. В.Б. Бетелин, С.Г. Бобков, С.А. Зендрикова, А.А. Кравченко, А.Г. Кушниренко, В.К. Николаев "Теоретические оценки эффективности суперЭВМ с распределенной памятью" - М.: "НИИСИ РАН", 2003, 180с.

88. Широков И.А. Исследование и разработка методов оценки производительности проектируемых микропроцессоров, процессорных модулей, ЭВМ и систем обработки сигналов: автореф. дис. ... физ.-мат. наук. НИИСИ РАН. - Москва, 2010. - 18 с.

89. J. Sosnowski Software-based self-testing of microprocessors // Journal of Systems Architecture N52, 2006, p. 257-271.

90.Carter H., Hemmady S. Metric Driven Design Verification: An Engineer's and Executive's Guide to First Pass Success. Springer Science+Business Media, LLC, 2007. 361p.

91.Laird, Linda M and Brennan, Carol M; Software Measurement and Estimation: A Practical Approach; John Wiley & Sons, Hoboken, NJ; 2006; ISBN 0-47167622-5.

92. IEEE Recommended Practice on Software Reliability. IEEE Std 1633-2008.

93. Smith G. Verification Bug Metrics. [Электронный ресурс] URL: http://www.testandverification.com/DVClub/24_Jan_2011/Greg_Smith.pdf (дата обращения: 30.08.2013).

94.Alagappan V. Leveraging Defect Prediction Metrics in Software Program Management. // International Journal of Computer Applications, Vol. 50, 2012, p.23.

95.Vladu A., Fagarasan I. On prediction of defect rates // In Proc. IEEE International Conference on Automation, Quality and Testing, Robotics -AQTR 2012, pp. 201 -205.

96. Laird L. In Praise of Defects. Stevens Institute of Technology. [Электронный ресурс] URL: http://www.njspin.org/present/Linda Laird March 2005.pdf

97. Vladu A. Software Reliability Prediction Model Using Rayleigh Function. Politehnica University Scientific Bulletin, Bucharest, Series C, Vol. 73, Iss. 4, 2011, ISSN 1454-234x.

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

99.Wilson R. "Verification metrics: When is enough enough?" [Электронный ресурс]. URL: http://www.edn.com/electronics-news/4326023/Verification-metrics-When-is-enough-enough- (дата обращения: 30.08.2013).

100. В. Bailey "Coverage for functional verification". [Электронный ресурс]. URL:http://www.eetimes.com/electronics-blogs/practical-chip-design/4401929/ Coverage-for-functional-verification (дата обращения: 30.08.2013).

101. RTCA DO-254, Design Assurance Guidance for Airborne Electronic Hardware, RTCA Inc., Washington, DC, 2000.

102. Talesara H., Mullinger N. Accelerating Functional Closure. Synopsys Verification Solutions, Vol. 6, Issue 3, October 2006, pp.3-7.

103. Meyer A. Principles of functional verification. Newnes, 2003. 216p.

104. S. Ur, A. Ziv Off-the-Shelf vs. Custom Made Coverage Models, Which Is the One for You? // Proceedings of 7th Int. Conf. Software Testing Analysis and Rev. (STAR'98), 1998.

105. Рыжов М.П. Опыт реализации системы верификации, управляемой тестовым покрытием. Вопросы Радиоэлектроники. М: «Центральный научно-исследовательский институт «Электроника», № 3, 2011, с. 83-90.

106. Wiemann A. Standardized functional verification. San Carlos: Springer Science+Business Media, LLC, 2008, 275p.

107. Галатенко В.А., Костюхин K.A., Шмырёв H.B. Аппаратная поддержка контролируемого выполнения. // Параллельные вычисления и задачи управления. Сборник трудов конференции РАСО'2010, с. 1105-1112.

108. Emek, R. et al. Quality Improvement Methods for System-level Stimuli Generation // In Proceeding ICCD '04 Proceedings of the IEEE International Conference on Computer Design, pp. 204-206.

109. Ho Kim, J. E. Smith An Instruction Set and Microarchitecture for Instruction Level Distributed Processing // In Proc. of 29th Annual International Symposium on Computer Architecture, 2002, p. 71 - 81.

110. Lachish O., Marcus E., Ur S., Ziv A. Hole analysis for functional coverage data. // In Proc. DAC - 2002, pp. 807-812.

111. Wagner I., Bertacco V., Austin T. Stresstest: an automatic approach to test generation via activity monitors // In proceedings of the IEEE/ACM Design Automation Conference (DAC'05), pp. 783-788.

112. Curtis R. Cook Information Theory Metric For Assembly Language / Software Engineering Strategies Journal, 1993, p. 52-60.

113. J. David Blaine, Richard A. Kemmerer Complexity measures for assembly language programs. // Elsevier Science Inc. N.Y.: Journal of Systems and Software, Vol. 5 Iss. 3, 1985, p.229-245.

114. About CoreMark [Электронный ресурс]. URL: http://www.eembc.org/coremark/about.php (дата обращения: 30.08.2013).