Метод тестирования производительности и корректности микропроцессоров при помощи нацеленных тестовых программ тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат наук Зубковская, Наталья Владимировна

• Зубковская, Наталья Владимировна
• кандидат наук
• 2013

Оглавление диссертации кандидат наук Зубковская, Наталья Владимировна

Содержание

Введение

Глава 1. Анализ и классификация методов функциональной верификации и оценки производительности микропроцессоров

1.1. Функциональная верификация микропроцессоров

1.1.1. Динамическая верификация

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

1.1.3. Верификация, основанная на утверждениях

1.2. Сравнительный анализ методов верификации

1.3. Методы оценки производительности микропроцессора на стадии разработки

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

1.3.2. Аналитические модели

1.3.3. Потактовые эмуляторы

1.3.4. Оценка производительности на стадии ЯТЬ-модели

1.4. Средства повышения скорости моделирования

1.5. Постановка задачи для оценки производительности и функциональности моделей микропроцессоров

Глава 2. Метод исследования и контроля производительности и корректности функционирования микропроцессоров и методика локализации ошибок

2.1. Общая схема процесса разработки и верификации микропроцессоров

2.2. Основные понятия предлагаемого метода

2.2.1. Микротесты

2.2.2. Инициализирующая библиотека

2.2.3. Тестовый шаблон

2.2.4. Определение значимых параметров

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

2.3.1. Первая фаза метода

2.3.2. Вторая фаза метода

2.3.3. Методика построения критериев полноты тестовых воздействий

2.4. Методика локализации ошибок ЯТЬ-модели и КЕТЫ8Т-модели

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

Глава 3. Технологический процесс оценки и контроля производительности моделей микропроцессоров

3.1. Способы определения тестового набора для оценки производительности ЮХ-моделей микропроцессоров

3.1.1 Описание подсистемы памяти

3.1.2 Определение тестового набора для оценки производительности подсистемы памяти

3.1.3 Описание буфера инструкций

3.1.4 Определение тестового набора для оценки производительности буфера инструкций

3.1.5 Описание блока вещественной арифметики

3.1.6 Определение тестового набора для оценки производительности блока вещественной арифметики

3.1.7 Описание параметрической модели ядра микропроцессора

3.2. Организация регрессионного процесса оценки и контроля производительности ЮХ-моделей микропроцессоров

3.3. Визуализация представления результатов оценки производительности

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

Глава 4. Опыт практического применения предлагаемого метода на микропроцессорах 1890ВМ5Ф, 1890ВМ6Я и 1890ВМ8

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

4.2. Результаты оценки производительности буфера инструкций

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

4.4. Результаты оценки производительности параметрической модели ядра микропроцессора

4.5. Микротесты для локализации ошибок готовых микросхем

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

Заключение

ЛИТЕРАТУРА

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

Введение

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

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

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

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

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

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

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

Как правило, для контроля функциональной корректности микропроцессоров используют другие методы построения или генерации тестов, отличные от тестов производительности. Так, для верификации ЯТЬ-моделей микропроцессоров широко применяется имитационное тестирование. Для построения тестовых последовательностей применяют такие методы как ручная разработка на основе типовых сценариев, случайная генерация и генерация тестов на основе конечных автоматов или других систем переходов. Применение совокупности данных методов позволяет уменьшить число логических ошибок, однако, помимо ошибок ЯТЬ-моделей готовая микросхема может содержать ошибки, проявившиеся при переходе на вентильный уровень (КЕТЫБТ). Предлагаемые на рынке средства формальной верификации, позволяющие проверить эквивалентность КЕТЫБТ-модели и ЯТЬ-модели, не дают гарантии отсутствия всех временных нарушений. Поэтому при отладке NETLIST-мoдeли также используют имитационное тестирование. Из-за большей детализации скорость работы тестов на МЕТЫЕТ-модели на несколько порядков замедляется по сравнению со скоростью их работы на ЯТЬ-модели. Следовательно, необходим инструмент, позволяющий прове-

рить все узлы блоков микропроцессора при помощи компактных тестов, не требующих больших временных ресурсов.

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

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

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

Целью диссертационной работы является разработка метода и средств исследования и контроля производительности и корректности функционирования моделей микропроцессоров при помощи нацеленных тестовых программ (микротестов), а также в разработке на основе этих же средств методики локализации ошибок ЮХ-модели и N£^18^ обнаруженных на стадиях тестирования ПЛИС-прототипа, тестового кристалла или готовой СБИС.

В соответствии с этим были определены следующие основные задачи диссертации:

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

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

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

3. Разработка средств генерации микротестов, позволяющих автоматизировать процесс их создания.

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

Научная новизна диссертации

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

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

2. Методика локализации ошибок ЯТЬ-модели и ЫЕТЫЗТ-модели, обнаруженных на стадиях тестирования ПЛИС-прототипа, тестового кристалла или готовой СБИС.

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

Предложенные в работе методы и методики могут использоваться для решения задач оценки производительности и корректности функционирования разрабатываемых микропроцессоров. На основе предложенного метода оценки и контроля производительности и функциональности микропроцессоров была реализована система регрессионного тестирования. Система использовалась при разработке отечественной микросхемы 1890ВМ6Я, выпускаемой серийно, а также продолжает использоваться для разработки микросхем 1890ВМ8 и 1890ВМ9 (на данном этапе разработки получен тестовый кристалл 1890ВМ8).

Проведенные экспериментальные исследования и испытания микросхемы 1890ВМ6Я и тестового кристалла 1890ВМ8 позволили оценить точность результатов исследования производительности на стадии разработки ЯТЬ-

модели, а введенные на этапе проектирования оптимизации позволили повысить производительность микропроцессора.

Апробация диссертации

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

• Научно-техническая конференция «Электроника, микро- и наноэлектроника», 2008 г. (г. Вологда), 2011 г. (г. Суздаль), 2012 г. (г. Суздаль).

• Всероссийская научно-техническая конференция "Проблемы разработки перспективных микро- и наноэлектронных систем", 2005 г. (г. Истра), 2010 г. (г. Истра), 2012 г. (г. Истра).

• Международная конференция «Параллельные вычисления и задачи управления», 2012 г. (г. Москва).

• На семинарах НИИСИ РАН.

Публикации

По теме диссертационной работы опубликованы 17 печатных работ [1]-[17], из них 4 в изданиях по перечню ВАК. Получено 2 патента Российской Федерации на изобретение.

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

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

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

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

при помощи микротестов. Приводится методика построения критериев полноты тестовых воздействий, а также методика локализации ошибок ЯТЬ-модели и КЕТЫБТ-модели, обнаруженных на стадиях тестирования ПЛИС-прототипа, тестового кристалла или готовой СБИС.

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

В четвертой главе приводится опыт применения разработанной методики оценки производительности к ЯТЬ-моделям микропроцессоров ВМ5Ф и ВМ6Я. Также рассматриваются примеры ошибок ЯТЬ-моделей, локализованных в отдельные микротесты, с помощью рассмотренной методики

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

Глава 1. Анализ и классификация методов функциональной верификации и оценки производительности микропроцессоров

Функциональная верификация - это проверка соответствия результатов проектирования функциональным требованиям. В настоящее время существуют различные методики и средства функциональной верификации. Они отличаются как эффективностью работы, так и требуемыми ресурсами (временными, интеллектуальными, финансовыми и так далее). Кроме того, применение тех или иных средств функциональной верификации зависит от этапа проектирования [18].

Помимо функциональной верификации при разработке микропроцессора необходимо проводить оценку его производительности [19]. Применяемые методы и средства также зависят от этапа разработки.

Можно разделить следующие этапы проектирования микропроцессоров и систем на кристалле [20-21]:

• Разработка аналитической модели [22]-[27]. Такие модели значительно быстрее потактовых эмуляторов, хотя и не обеспечивают такую же точность, тем не менее, они могут использоваться для отбраковки архитектурных решений и расчета потребления будущей микросхемы.

в Потактовые эмуляторы [28], [29]. Применяют для исследования и усовершенствования отдельных компонентов архитектуры. Кроме того, это мощный инструмент, используемый в дальнейшем при верификации ЯТЬ-модели.

• Верификация ЯТЬ-модели [30]. На этой стадии проектирования применяется наибольшая часть существующих средств функциональной верификации.

• Тестирование на аппаратном ускорителе [31]. Это удобный инструмент для отладки модели микропроцессора. Хорошая визуализация внутренних сигналов позволяет быстрее обнаружить ошибку. При том не всегда удается протестировать модель микросхемы с полным ее окружением из-за отсутствия полноценных моделей внешних устройств.

• Тестирование ПЛИС-прототипа микропроцессора [32]. Достоинством использования прототипа являются максимально приближенные к реальным условия, в которых функционирует тестируемая микросхема, а также высокая производительность. К недостаткам можно отнести ограниченное количество внутренних сигналов, доступных для логического анализа при отладке.

• Тестирование модели микросхемы транзисторного уровня после топологического проектирования (КЕТЫ8Т) [33]. Основная задача тестов состоит в проверке соблюдения всех временных параметров функционирования микросхемы после перехода на транзисторный уровень и появлении паразитных элементов.

• Валидация тестового кристалла (first-pass silicon validation) [34]. Используется комплект тестов, созданный при разработке модели. Особую значимость приобретает выполнение системного и прикладного ПО на созданных микросхемах. Весьма эффективным является тестирование микросхем сторонними организациями.

• Валидация серийно выпускаемых экземпляров СБИС (post-silicon validation) [35]. На данном этапе поиск ошибок не прекращается, данные об обнаруженных ошибках документируются, предлагаются способы обхода таких ошибок. Воздействия, приводящие к ошибке, локализуются в отдельном тесте, для последующего регрессионного тестирования RTL-моделей микропроцессоров следующего поколения.

1.1. Функциональная верификация микропроцессоров

На сегодняшний день существует три основных типа организации проверки соответствия проектов заданным требованиям [112].

Первый вариант - имитационный или динамический (simulation-based verification) - базируется на проведении серии динамических экспериментов над проверяемым проектом. Второй вариант верификации базируется на формальных методах преобразования спецификации проекта в модель этого проекта. Третий вариант сводится к доказательству эквивалентности моделей (Equivalence Checking of Models).

Помимо этих методов существуют так называемые синтетические или гибридные методы [36], использующие комбинации разных подходов.

1.1.1. Динамическая верификация

Для проведения динамической верификации создается тестовая система (рис. 1) - специализированная программа, которая может быть написана либо на том же языке, что и тестируемый компонент (Verilog, VHDL), либо на языке C/C++, либо на языке верификации аппаратуры (OpenVera [102], SystemVerilog[103], Specman е [104]). Создаваемые тестовые воздействия (стимулы) и саму систему тестирования также называют Test-Bench. Тестовая система, в соответствии с планом верификации, создает тестовые воздействия, осуществляет проверку реакций модели на тестовые воздействия, а также оценивает степень покрытия.

Тестовая система

Генерация стимуловс

RTL-модель

Проверка ^ реакции

Рис. 1. Тестовая система для динамической верификации

В технологии тестирования 11тТЕ8К, разработанной в ИСП РАН [39], [40] архитектура тестовой системы включает такие компоненты, как генератор тестовой последовательности и тестовый оракул (рис.2).

теста

Рис. 2. Структура тестовой системы, применяемая в технологии ЦшТЕ8К

[113]

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

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

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

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

Современные методологии верификации аппаратуры, в частности, OVM (Open Verification Methodology) [41], UVM (Universal Verification Methodology) [104], предлагают более детальное описание тестовой системы, благодаря которому повышается уровень повторного использования тестовых систем при подключении к тестируемому компоненту другого блока RTL-модели или при включении тестируемого компонента в состав вышестоящего по иерархии модуля. Тестовая система в соответствии с методологией UVM представлена на рис 3.

Рис. 3. Структура тестовой системы по методологии UVM

Говоря о динамической верификации, различают модульную (тестированию подвергается отдельный модуль) и системную верификацию (тестированию подвергается система в целом).

Методология UVM хорошо подходит для тестирования на модульном уровне, либо для тестирования IP-блоков (Intellectual Property) устройств, таких как Ethernet, RapidIO и прочее. Для тестирования микропроцессора в сборе чаще используют системную верификацию.

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

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

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

Наиболее известный коммерческий генератор случайных тестов для микропроцессоров - RAVEN, компании Obsidian Software [42]. Также известны генераторы тестовых программ Genesys-Pro (IBM Research) [43], система INTEG (НИИСИ РАН) [44] и MicroTESK (ИСП РАН) [45].

Помимо случайной генерации тестовые программы могут быть построены путем обхода графа состояний автоматной модели тестируемого компонента [45]. Автоматная модель может разрабатываться вручную, строиться на основе статического анализа кода RTL-модели либо на основе формальных спецификаций. На использовании автоматных моделей для построения тестовых последовательностей базируется, в частности, технология UniTESK и поддерживающие ее инструменты.

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

Для ко-симуляции отдельным коллективом разработчиков создается эталонная модель, которая имеет ту же функциональность, но представлена в более абстрактной форме. Как правило, для разработки эталонного эмулятора используют язык С/С++. На ЮХ-модель и эталонную модель подается одна и та же тестовая последовательность, результаты работы ЮХ-модели и эталонной модели сравнивают на соответствие. Расхождения при сравнении поведения двух моделей говорят об ошибке в одной из них. После исправления ошибки тестирование возобновляется. Достоинством ко-симуляции является то, что проверка правильности поведения ЮХ-модели производится автоматически, что снижает трудозатраты на разработку тестовых последовательностей. Для реализации сравнения ЮХ-модель и эталонная модель создают лог-файлы выполненных инструкций, записей в регистровые файлы, обращений в кэш-память и ОЗУ.

Самопроверяющие тесты содержат проверки, которые необходимо провести после или во время воздействия на ЮХ-модель. Достоинством самопроверяющих тестов является то, что при их использовании не нужна эталонная модель. Недостатком является сложность разработки встроенных проверок.

Помимо ЮХ-модели динамической верификации подвергается МЕТЬ-18Т-модель (ЮХ-модель, переведенная в описание на библиотечных элементах). Для динамического тестирования КЕТЫБТ-модели применяют самопроверяющие тесты из-за сложности получения лог-файлов КЕТЫЗТ-модели. Существенной сложностью при динамической верификации КЕТХ-18Т-модели является то, что скорость ее работы на порядок снижается по сравнению со скоростью работы ЮХ-модели.

Для повышения скорости моделирования при верификации ЮХ-модели используют ПЛИС-прототипы. При этом существенно увеличивается объем тестов, которые можно запустить на проекте. Появляется возможность при-

менения метода «встречного» тестирования [110], основанного на использовании приложений под разрабатываемый микропроцессор.

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

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

Формальные методы способствуют повышению уровня качества продукта выше того уровня, который можно обеспечить лишь динамическим моделированием [46]. С помощью формальных методов удается обнаружить дефекты в системах программного обеспечения и аппаратуре, уже прошедших обширное тестирование [47]. Формальная верификация с математической точностью доказывает корректность проекта, то есть верификация, в данном случае, является исчерпывающей и проверяет все возможные варианты поведения системы [114].

Выделяют три основных подхода к формальной верификации, которые используют для проверки микропроцессоров: метод доказательства эквивалентности (Equivalence Checking), проверка моделей (Model Checking) и автоматизированное доказательство теорем (Automated theorem proving).

Метод доказательства эквивалентности моделей (Equivalence Checking of Models) определяет работоспособность той или иной модели проекта, основываясь на ее эквивалентности с другой моделью. При таком подходе не имеет значения, как доказана правильность работы исходной модели. Проверка исходной модели может быть осуществлена ранее проведенным ее тестированием. В наибольшей степени метод применяется для доказательства эквивалентности NETLIST-модели и RTL-модели.

Для проверки эквивалентности используют двоичные диаграммы решений (BDDs, Binary Décision Diagrams) и системы разрешения логических ог-

раничений (SAT-solvers). Основными коммерческими инструментами проверки эквивалентности являются Conformai (от Cadence), Formality (от Synopsys), FormalPro (от Mentor Graphics) и SLEC (от Calypto).

Метод проверки моделей (Model Checking) используется для проверки, удовлетворяет ли система формальной спецификации.

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

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

В основе автоматизированного доказательства теорем (Automated theorem proving) лежит принцип представления описания задачи и относящейся к ней информации в виде логических аксиом и теорем, которые нужно доказать. К недостаткам данного метода можно отнести то, что без участия человека не удается решать сложные задачи. Это связано с тем, что для любой сложной системы можно сгенерировать бесконечное количество теорем, которые можно доказать. Для направления и ограничения количества решаемых теорем разрабатываются эвристики, основанные на оценке синтаксической формы логического выражения. Несмотря на сложность реализации автоматизированное доказательство теорем находит применение в крупных индустриальных проектах таких компаний как IBM, Intel, AMD и Motorola.

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

1.1.3. Верификация, основанная на утверждениях

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

Систему утверждений также используют для оценки покрытия [111] (assertion based coverage). Целью таких утверждений является проверка того, произошло ли описанное в утверждении событие или нет.

Список литературы диссертационного исследования кандидат наук Зубковская, Наталья Владимировна, 2013 год

ЛИТЕРАТУРА

1. Зубковская H.B. Оценка и контроль производительности и работоспособности проектируемых микропроцессоров на базе микротестов // Электроника, микро- и наноэлектроника. Сб. научн. трудов. - М.: МИФИ, 2013. - С. 188-195.

2. Аряшев С.И., Зубковская Н.В., Корниленко A.B., Рогаткин Б.Ю. Имитационное моделирование подсистемы памяти микропроцессора со встроенным системным контроллером // Электроника, микро- и наноэлектроника. Сб. научн. трудов. - М.: МИФИ, 2013. - С. 118-125.

3. Аряшев С.И., Корниленко A.B., Зубковская Н.В., Саяпин П.В. Повышение производительности подсистемы памяти методом буферизации данных // Информационные технологии. - 2013. - №6 - С. 11-17.

4. Пат. 2480820 РФ, МПК G06F 15/00 G06F 12/12. Устройство обработки информации / Аряшев С.И., Корниленко A.B., Николина Н.В., Петров К.А. - Опубл. 27.04.2013. - Бюл. № 12. - 7 С.

5. Пат. 2475817 РФ, МПК G06F9/30. Устройство буферизации потоков данных, считываемых из ОЗУ / Аряшев С.И., Корниленко A.B., Николина Н.В. - Опубл. 20.02.2013. - Бюл. №5.-6 С.

6. Николина Н.В. Микротесты для оценки производительности RTL-моделей микропроцессоров // Программные продукты и системы. - 2012, №3. - С. 103 - 107.

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

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

9. Аряшев С.И., Барских М.Е., Николина Н.В. Оценка производительности буфера инструкций на стадии разработки RTL-модели микропроцессора // Электроника, микро- и наноэлектроника. Сб. научн. трудов. - М.: МИФИ, 2012.-С. 158-165.

10. Аряшев С.И., Корниленко A.B., Николина Н.В., Петров К.А. Повышение сбоеустойчивости и быстродействия подсистемы внешней динамической памяти микропроцессорной системы // Электроника, микро- и наноэлектроника. Сб. научн. трудов. - М.: МИФИ, 2012. - С. 173-178.

11. Рогаткин Б.Ю., Николина Н.В., Аряшев С.И. Проблемы проектирования подсистемы памяти ядра микропроцессора со встроенным системным контроллером / 16-я Международная телекоммуникационная конференция молодых ученых и студентов «Молодежь и наука», 2012.

12. Аряшев С.И., Николина Н.В. Влияние буферизации данных на производительность подсистемы памяти // Электроника, микро- и наноэлектроника. Сб. научн. трудов. - М.: МИФИ, 2011. - С. 164-167.

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

14. Аряшев С.И., Николина Н.В., Чибисов П.А. Этапы тестирования моделей микропроцессора со встроенным системным контроллером. Электроника,

микро- и наноэлектроника. Сборник научных трудов. - М: МИФИ, 2007. -С. 179-182.

15. Аряшев С.И., Зубковский П.С., Николина Н.В., Чибисов П.А. Основные подходы к верификации блока вещественной арифметики. Проблемы разработки перспективных микроэлектронный систем - 2005. Сборник научных трудов. - М: ИППМ РАН, 2005. - С. 269-274.

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

17. Чибисов П.А., Николина Н.В. Функциональная верификация RTL-модели суперскалярных микропроцессоров. Электроника, микро- и наноэлектроника. Сборник научных трудов. - М: МИФИ, 2004. - С. 213— 216.

18. Камкин А. Верификация микропроцессоров: борьба с ошибками и управление качеством // ЭЛЕКТРОНИКА: НТБ №3, 2010. - С. 98-104.

19. Bose P., Abraham J. A., Performance and Functional Verification of Microprocessors. In the IEEE VLSI Design Conference, 2000.

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

21. Бобков С.Г. Методика проектирования микросхем для компьютеров серии «Багет» // Информационные технологии. - 2008, №3. - С. 2 - 7.

22. Joseph P. J., Vaswani К., Thazhuthaveetil М. J. A predictive performance model for superscalar processors // MICRO. - 2006. - P. 161 - 170.

23. Lee В., Brooks D. Efficiency trends and limits from comprehensive microarchitectural adaptivity // ASPLOS. - 2008. - P. 36 - 47.

24. Karkhanis Т., Smith J. Automated design of application specific superscalar processors: An analytical approach // ISCA. - 2007. - P. 402 -411.

25. Taha Т., Wills D. An instruction throughput model of superscalar processors // IEEE Transactions on Computers. - 2008. - P. 389 - 403.

26. Eyerman S., Karkhanis Т., Smith J. A mechanistic performance model for superscalar out-of-order processors // ACM Transactions on Computer Systems, Vol. 27, No. 2, Article 3. - 2009. 37p.

27. P. Joseph, K. Vaswani, and M. J. Thazhuthaveetil. Construction and use of linear regression models for processor performance analysis // Symposium on High Performance Computer Architecture, Austin, Texas, February 2006.

28. Слепов А. Б. Разработка потактовой поведенческой модели системы на кристалле на языке С++ / Сборник научных трудов «Проблемы разработки перспективных микроэлектронных систем - 2010» / Под ред. А.Л. Стемпковского. - М.: ИППМРАН, 2010. - С. 450 - 453.

29. Maturana G., Ball J. L., Gee J., Iyer A., O'Connor J. M. Incas: a cycle accurate model of UltraSPARC // IEEE International Conference on Computer Design (ICCD'95). - 1995. - P. 130 - 135.

30. Bergeron J. Writing Testbenches: Functional Verification of HDL Models. -Kluwer Academic Publishers, 2000.

31. Пеженков А., Радченко Д. Аппаратные эмуляторы на платформе ZeBu // ЭЛЕКТРОНИКА: НТБ №4, 2005. - С. 64-66.

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

33. Rashinkar P., Paterson P., Singh L. System-on-chip verification: Methodology and Techniques. - Kluwer Academic Publishers, 2002. - pp. 122.

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

35. Mitra S., Seshia S., Nicolici N. Post-Silicon Validation: Opportunities, Challenges and Recent Advances. // IEEE/ACM Design Automation Conference.-2010.-P. 12-17.

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

37. Lam W. K. Hardware Design Verification: Simulation and Formal Method-Based Approaches. PrenticeHall PTR, 2005.

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

39. Сайт, посвященный технологии тестирования UniTESK. -www.unitesk.com.

40. Сайт, посвященный исследованиям в области верификации аппаратуры, проводимым в ИСП РАН. - hardware.ispras.ru.

41. Сайт, посвященный методологии OVM. - www.ovmworld.org.

42. Страница, посвященная генератору RAVEN. -www.obsidiansoft.com/products-and-services/inroducing-raven/.

43. Страница, посвященная генератору Genesys-Pro. -www.haifa.ibm.com/projects/verification/genesys_pro/index.shtml.

44. Стохастическое тестирование в системе INTEG / Грибков И.В., Захаров А.В., Кольцов П.П. [и др.] // Програм- мные продукты и системы. 2007. № 2. С. 22-26.

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

46. Новожилов Е. Е. Формальные методы верификации RTL-моделей сверхбольших интегральных схем // Программные продукты и системы. -2008, №4. - С.23-26.

47. S.P., Miller. Formal Verification of the AAMP5 Microprocessor - A Case Study in the Industrial Use of Formal Methods, in Proceedings of the 1995 Workshop on Industrial-Strength Formal Specification Techniques (WIFT'95). Orlando : IEEE Computer Society, 1995.

48. H. Foster, A. Krolnik. Creating Assertion-Based IP. // Springer Science+Business Media, LLC, 2008.

49. Bentley B. Validating the Intel Pentium 4 Microprocessor.- DAC 2001: Design Automation Conference, 2001, p. 244-248.

50. Drechsler R. Advanced Formal Verification. Kluwer Academic Publishers, 2004, - pp. 249.

51. Долинский M. Assertion Based Verification — верификация, основанная на утверждениях // Компоненты и технологии, № 9, 2004. - С.28-33.

52. Linpack. URL: http://www.top500.org/lists/linpack.php/.

53. Standart Performance Evaluation Corporation. URL: http://www.spec.org/.

54. Embedded Benchmark Consortium. URL: http://www.eembc.org/.

55. Cremonesi P., Sansottera A., Turrin R., Predicting SPEC benchmarks values for untested systems, INFQ 2010, pp. 5.

56. Cremonesi P., Bertoli M., Predicting SPEC benchmarks values for untested systems, CMG 2009, pp. 8.

57. Kramer K., Stolze T., Oppelt A. Microprocessor Benchmarks - A Detailed Look at Techniques, Problems and Solutions // ICSENG '11 Proceedings of the 2011 21st International Conference on Systems Engineering. -2011.-P.337-340.

58. Strohmaier E., Shan H. Apex-Map: A Synthetic Scalable Benchmark Probe to Explore Data Access Performance on Highly Parallel Systems // EuroPar2005. -2005.-P. 114-123.

59. Guthaus M., Ringenberg J., Ernst D., Austin T., Mudge T., Brown R. "MiBench: A free, commercially representative embedded benchmark suite,"IEEE International Workshop on Workload Characterization, pp. 3-14, 2 December 2001.

60. McCalpin J. "Stream: Sustainable Memory Bandwidth in High Performance Computers". URL: http://www.cs.virginia.edu/stream/.

61. NAS Parallel Benchmarks. URL: http://www.nas.nasa.gov/Software/NPB/.

62. Stanford Parallel Applications for Shared Memory. URL: http://www-flash.stanford.edu/apps/SPLASH.

63. Eyerman S., Eeckhout L., Karkhanis T., Smith J. E. A Top-Down Approach to Architecting CPI Component Performance Counters // IEEE Micro. 2007. Vol. 27. No. l.P. 84-93.

64. SystemC. URL: http://www.systemc.org.

65. Chang S. F., Hu A. J. Fast Specification of Cycle-Accurate Processor Models // IEEE International Conference on Computer Design (ICCD'Ol). - 2001. - P. 144 - 148.

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

67. L. Van Ertvelde. Workload Generation for Microprocessor Performance Evaluation. PhD thesis, Ghent University, Belgium, 2010.

68. Hristea C., Lenoski D., Keen J. Measuring Memory Hierarchy Performance of Cache-Coherent Multiprocessors Using Micro Benchmarks. In Supercomputing'97, CA, November 1997.

69. Saavedra R., Gaines R., Carlton M. Characterizing the Performance Space of Shared-Memory Machines Using Micro-Benchmarks. In Hot Interconnects'94, CA, August 1994.

70. Strydis C., Kachris C., Gaydadjiev G.N. ImpBench: A novel benchmark suite for biomedical, microelectronic implants. IEEE Xplore. 2008, P 82-91.

71. Материалы компании Intel: «Intel Pentium 4 Processor Specification Update» №249199-059.

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

73. MIPS64 Architecture for Programmers rev. 2.00 vol. I, II, III. - URL: http://www.mips.com.

74. MIPS R10000 Microprocessor. User's Manual. - URL: http://www.mips.com.

75. Cragon H.G. Memory Systems and Pipelined Processors // Jones and Bartlett Publishers. - 1996.-576 p.

76. Burger D.C. Hardware Techniques to Improve the Performance of the Processor Memory Interface // University of Wisconsin-Madison, 1998. -http://citeseer.ist.psu.edu/burger98hardware.html.

77. Zhang Yi., Haga S., Barua R. "Execution history guided instruction prefetching", The Journal of Supercomputing, vol. 27, 2004, p. 129-147.

78. Falcon A., Ramirez A., Valero M. "Effective instruction prefetching via fetch prestaging". Proceedings of the 19th IEEE International Parallel and Distributed Processing Symposium (IPDPS'05), 2005.

79. Hennessy J.L., Patterson D.A. Computer Architecture - a Quantitative Approach. - USA, San Francisco: Morgan Kaufmann Publishers, 2003. - 1072

P-

80. Бобков С.Г., Булгаков В.Ю.. Влияние опережающего считывания из оперативного запоминающего устройства на скорость выполнения программ. - М.: Вопросы кибернетики, 1992. - с 44 — 59.

81. Аряшев с.И., Корниленко А.В. Оптимизация работы с памятью на уровне системного контроллера / Сборник научных трудов «Электроника, микро-и наноэлектроника» / Под ред. В.Я. Стенина. - М.: НИЯУ МИФИ, 2011. -С. 176- 179.

82. Саяпин П. В. Буфер для операций сохранения в кэш-памяти второго уровня с помехоустойчивым кодированием // Научная сессия НИЯУ

МИФИ-2010. XIII Международная телекоммуникационная конференция студентов и молодых ученых «Молодежь и наука». Тезисы докладов. В 3-х частях. Ч. 1.-М.: НИЯУ МИФИ, 2010. С. 79 - 80.

83. J. F. Cantin and М. D. Hill, "Cache Performance for Selected SPEC CPU2000 Benchmarks", Computer Architecture News, Vol. 29, No. 4 -September 2001.

84. Аряшев С.И., Барских M.E., Бычков K.C. Методы повышения производительности суперскалярного RISC-процессора // Проблемы разработки перспективных микроэлектронных систем - 2005. Сб. научных трудов / под общ. ред. A.J1. Стемпковского. - М.: ИППМ РАН, 2005.-С. 214-221.

85. Барских М.Е., Бычков К.С. - Вариант реализации буфера команд и кэшпамяти команд - Электроника, микро- и наноэлектроника. Сборник научных трудов. - М: МИФИ, 2004. - С. 191-195.

86. Столлингс У. Структурная организация и архитектура компьютерных систем, 5-е изд.: пер. с англ. - М.: Издательский дом «Вильяме», 2002. -896 с.

87. Shen J.P., Lipast М.Н.. Modern Processor Design - Fundamentals of Superscalar Processors // McGraw-Hill. - 2003. - 488 p.

88. Аряшев С.И., Барских M.E., Бычков K.C. Поведение RTL-модели буфера инструкций суперскалярного RISC процессора // Электроника, микро- и наноэлектроника. Сборник научных трудов. - М: МИФИ, 2005. - С. 201204.

89. Барских М.Е., Морев С.А. Динамическое предсказание команд условного перехода высокопроизводительного процессора / Сборник научных трудов «Электроника, микро- и наноэлектроника» / Под ред. В.Я. Стенина. - М.: НИЯУ МИФИ, 2011.-С.213-218.

90. IEEE Standard for Binary Floating Point Arithmetic ANSI IEEE Std. 7541985.

91. Numerical Computation Guide. - Sun Microsystems, Inc. Part No. 806-799610 July 2001, Revision A.

92. Vector Signal Image Processing Library URL: http://www.vsipl.org/

93. С.И. Аряшев., Б.Ю.Рогаткин, O.B. Сысоева. Отладка блока преобразования адресов. Проблемы разработки перспективных микроэлектронных систем - 2005. Сборник научных трудов / под общ. Ред. А.Л. Стемпковского. - М.:ИППМ РАН, 205 - 281.

94. Аряшев С. И., Камкин A.C., Рогаткин Б. Ю. Тестирование RTL-модлей аппаратуры с помощью технологии UniTESK на примере блока преобразования адресов микропроцессора. Сб. науч. трудов. - М: МИФИ, 2007.-С. 183-186.

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

96. Стешенко В.Б. ПЛИС фирмы ALTERA: проектирование устройств обработки сигналов. - М.: ДОДЭКА, 2000. -128 с.

97. Cadence Design Systems, Inc. Palladium XP Technical Brief: // URL: http://www.cadence.com/rl/Resources/technical_briefs/palladium_xp_tb.pdf

98. Имитационное моделирование систем. Введение в моделирование с AnyLogic 5. - Издательство: БХВ -Петербург, 2006.-400 с.

99. Максимей И. В. Имитационное моделирование сложных систем. Математические основы. - Минск: БГУ, 2009.-264 с.

100. Sun Grid Engine 5.2.3 Manual. Sun Microsystems, Inc. July 2001. 456p.

101. Trac Integrated SCM & Project Management. URL: http://trac.edgewall.org/.

102. OpenVera Language Reference Manual: Testbench. Version 1.4.3, 2005.

103. IEEE Standard SystemVerilog Language Reference Manual. IEEE Std 18002005.

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

105. И.Б. Бурдонов, A.C. Косачев, B.H. Пономаренко, В.З. Шнитман. Обзор подходов к верификации распределенных систем, Препринт 16. М.: ИСП РАН, 2006. 61 с.

106. http://www.verificationlib.org/

107. http://www.open-vera.com/

108. http://www.accellera.org/

109. "SystemVerilog 3.1: Accellera's Extensions to Verilog/' http://www.eda.org/sv/.

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

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

112. Грушвицкий Р. Михайлов М. Проектирование в условиях временных ограничений: верификация проектов // Компоненты и технологии, №3, 2008, с.96-102.

113. Камкин A.C. , Чупилко М.М. Механизмы поддержки функционального тестирования моделей аппаратуры на разных уровнях абстракции // Труды ИСП РАН, т. 20, М., 2011, ISSN 2079-8156. с. 143-160.

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

115. Методы встречной оптимизации в задачах обработки сигналов // Сборник статей под редакцией академика РАН В.Б. Бетелина // М.:НИИСИ РАН, 2005.