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

Московский государственный университет имени М. В. Ломоносова

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

Корныхин Евгений Валерьевич

Построение тестовых программ для проверки подсистем управления памяти микропроцессоров

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

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

-7 0КТ 2010

Москва - 2010

004609885

Работа выполнена на кафедре системного программирования факультета вычислительной математики и кибернетики Московского государственного университета имени М. В. Ломоносова.

Научный руководитель:

Официальные оппоненты:

Ведущая организация:

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

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

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

Смелянский Руслан Леонидович;

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

Лацис Алексей Оттпович.

Научно-исследовательский институт системных исследований РАН

Защита состоится 15 октября 2010 года в 11 часов на заседании диссертационного совета Д 501.001.44 Московского государственного университета имени М.В. Ломоносова по адресу: 119991, ГСП-1, Москва. Ленинские горы, МГУ имени М.В.Ломоносова, 2-й учебный корпус, факультет ВМК, ауд. 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМК МГУ. С текстом автореферата можно ознакомиться на официальном сайте ВМК МГУ http://cs.msu.ru в разделе «Наука» — «Работа диссертационных советов» — «Д 501.001.44»

Автореферат разослан «15» сентября 2010 г.

/

Ученый секретарь диссертационного совета профессор

Н.П. Трифонов

Общая характеристика работы Актуальность темы

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

Чем позднее будут обнаружены ошибки в микропроцессорах, тем дороже обойдётся их исправление: сделать это в готовой микросхеме, тем более выпущенной на рынок, практически невозможно. Тем актуальнее становятся методы обнаружения ошибок на ранних этапах разработки микропроцессоров. Цикл разработки микропроцессоров предполагает их подготовку в виде исполнимых программных моделей на языках Verilog или VHDL. Это делает возможным проведение функциональной верификации на таких моделях (т.е. до проихводства самих микропроцессоров) и актуальным исследование методов такой верификации. Целью функциональной верификации программных моделей микропроцессоров является обнаружение ошибок реализации функциональности в программных моделях микропроцессоров.

Выделяют следующие виды функциональной верификации: экспертизу, имитационное тестирование и формальную верификацию. Экспертиза предполагает анализ текстов моделей экспертами с целью оценки их корректности и обнаружения ошибок. Этот вид фукнциональной верификации эффективно применяется на ранних стадиях разработки. Однако ввиду наличия человеческого фактора в результате экспертизы ошибки в микропроцессоре всё же остаются. Методы формальной верификации позволяют дать исчерпывающий ответ на вопрос о корректности отдельных модулей или всего микропроцессора. Однако трудоемкость формальной верификации чрезвычайно велика. Например, при разработке Intel Pentium 4 были формально верифицированы модуль работы с плавающей точкой (FPU), модуль декодирования

инструкции и логика внеочередного выполнения (out-of-order), было найдено порядка 20 новых ошибок, однако трудоемкость этого проекта составила порядка 60 человеко-лет.

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

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

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

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

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

Цель диссертационной работы

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

Для достижения этой цели были поставлены следующие задачи:

1) исследовать описанные в научной литературе методы построения тестовых программ на предмет их применимости для системного тестирования подсистем управления памяти микропроцессоров;

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

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

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

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

2) предложен метод моделирования устройств подсистемы управления памяти, использующий расширенные конечные автоматы с заданным набором операций;

3) предложена формальная модель инструкций, описывающая отдельные пути их выполнения в виде утверждений о свойствах параметров инструкций и модельном состоянии устройств;

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

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

Разработанные модели и методы могут быть использованы коллективами, занимающимися разработкой микропроцессоров, для автоматизации построения тестовых программ. Разработанный прототип системы построения тестовых программ использовался для генерации тестов подсистем управления памяти ряда микропроцессоров архитектуры \HPS64. Результаты работы могут быть использованы в исследованиях, которые ведутся в Институте системного программирования РАН, Московском государственном институте электроники и математики, НИИ системных исследований РАН, Институте точной механики и вычислительной техники им. С.А. Лебедева РАН, Институте проблем информатики РАН и других научных и промышленных организациях.

Апробация работы и публикации

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

1) на втором и третьем весеннем коллоквиуме молодых исследователей в области программной инженерии (SYRCoSE) (2008 и 2009 гг.);

2) на шестнадцатой и семнадцатой международной конференции студентов, аспирантов и молодых ученых «Ломоносов» (2009 и 2010 гг.);

3) на шестнадцатой всероссийской межвузовской научно-технической конференции студентов и аспирантов «Микроэлектроника и информатика - 2009» (2009 г.);

4) на седьмом международном симпозиуме по проектированию и тестированию под эгидой IEEE (EWDTS) (2009 г.);

5) на российско-ирландской летней школе по научным вычислениям (2009

г.);

6) на научной конференции «Тихоновские чтения» (2009 г.);

7) на научной конференции «Ломоносовские чтения» (2010 г.);

8) на объединенном научно-исследовательском семинаре имени М.Р. Шура-Бура (2010 г.);

9) на семинаре Лаборатории вычислительных комплексов факультета вычислительной математики и кибернетики МГУ имени М.В.Ломоносова (2010 г.);

10) на семинаре отдела Технологий программирования института системного программирования РАН (2009, 2010 гг.).

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

Работа состоит из введения, трех глав, заключения, списка литературы и приложений. Общий объем основной части диссертации составляет 125 страниц. Список литературы содержит 71 наименование.

Содержание работы

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

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

В разделе 1.1 дается схема системного тестирования микропроцессора, описываются его отдельные этапы, в том числе и этап построения тестовых программ. Рассматриваются методы псевдослучайного и целенаправленного автоматического построения тестовых программ. В разделе 1.2 кратко описываются функции и типичный состав подсистем управления памяти, способы повышения их эффективности и классы ошибок. В разделе 1.3 сделан обзор методов целенаправленного построения тестовых программ. Выделены методы на основе массовой генерации тестовых программ и методы непосредственного построения тестовых программ. В разделе 1.4 сделан анализ методов целенаправленного построения тестовых программ по применимости этих методов для тестирования подсистемам управления памяти, масштабируемости, возможности «нацеливания» на функциональность. Наиболее перспективными являются методы непосредственного построения тестовых программ по тестовым ситуациям, формализованным в виде тестовых шаблонов — цепочек инструкций с указанием вариантов исполнения инструкций — и методы, включающие разрешение ограничений (constraint satisfaction). В разделе 1.5 уточнены задачи в соответствии с проведенным исследованием методов построения тестовых программ.

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

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

Тестовый шаблон содержит последовательность инструкций, для каждой из которых указан вариант исполнения (т.е. некоторый путь выполнения инструкции). Для алгоритмического построения ограничений и затем тестовых программ варианта инструкций должны быть формализованы в рамках этапа формализации микропроцессора. Раздел 2.2 более детально освещает этот этап . В этом разделе предложены модель функционирования устройств подсистемы управления памяти и модель вариантов инструкций. В рамках этого этапа следует выделить и формализовать те варианты инструкций, которые входят в тестовый шаблон, и задействованные в них устройства подсистемы управления памяти. Моделью состояния устройства подсистемы управления памяти (кэш-памяти, таблицы страниц и т.п.) предлагается последовательность ассоциативных массивов (далее эта последовательность будет называться таблицей, а отдельный ассоциативный массив — регионом). Каждый регион состоит из строк, каждая строка состоит из набора полей, поля делятся на поля ключа и поля данных. Поля ключа задают ключи в ассоциативном массиве, поля данных — значения. В модели устройства определены следующие операции: успешного обращения, успешного обращения с изменением, неуспешного обращения с замещением. На входе операции успешного обращения — выражение, задающие ключ, и выражение, задающее номер ассоциативного массива из состояния устройства. Операция определена на тех входных данных и состоянии модели, при которых в соответствующем ассоциативном массиве есть строка, поля ключей которой соответствуют аргументу-ключу этой операции. Операция возвращает поля данных соответствующей аргументу-ключу строки. Операция успешного обращения с изменением отличается от операции успешного обращения дополнительным аргу-

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

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

телыюсть операторов 4-х видов: оператор утверждения истинности свойства над битовыми строками (assume), оператор введения новой переменной (let), оператор попадания (hit), оператор промаха (miss). С помощью этой последовательности операторов задается набор условий на значения операндов инструкции и для моделей устройств, задействованных в этом варианте инструкции, условия на их состояние и изменение этого состояния в рамках данного варианта. Операторы let и assume имеют ту же семантику, которая используется при формализации императивных языков программирования. Операторы hit и miss специфичны инструкциям, оперирующим с памятью. Оператор nonaflaHHHhit<B>(k;R){loaded(d); [storing(d');] }, гдек, R, d, d' выражения над определенными ранее переменными-битовыми строками, означает, что в данном варианте инструкции должно осуществляться успешное обращение в устройство В по ключу к в массив с номером R, причем ключу соответствуют данные d (если полей данных несколько, то соответствующие выражения для них перечисляются в скобках у loaded). Если указана секция storing, то в варианте инструкции должно осуществляться успешное обращение с изменением на поля данных dJ. Оператор промаха miss<B>(k;R){[replacing(d);]}, где k, R, d — выражения над определенными ранее переменными-битовыми строками, означает, что в данном варианте инструкции должно быть неуспешноеобращение в блок В по ключу к в массив с номером R. Секция replacing задает поля данных d' вытесняющей строки. Если секция replacing отсутствует, изменение состояния устройства В не должно происходить.

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

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

По каждому оператору алгоритм строит свою часть ограничений, которые выражают семантику этого оператора. Операторы обращений в устройства транслируются в ограничения без моделирования состояний устройств, несмотря на то, что определение этих операторов включало состояние устройства. Это позволяет существенно уменьшить количество переменных-битовых строк и размер ограничений и, тем самым, ускорить разрешение ограничений. Специальное представление выбрано и для начального содержимого устройств, а именно, последовательность обращений в это устройство. Поэтому в число переменных в ограничениях входят переменные, задающие аргументы этих, инициализирующих, обращений: ключи, номера ассоциативных массивов. Для операторов hit и miss строятся ограничения на аргументы-ключи к и номера регионов R (эти ограничения должны гарантировать успешное обращение для hit и неуспешное — для miss) и ограничения на аргументы-данные dad1 (обращения по одинаковым адресам должны давать одинаковые данные, если они не были изменены). Ограничения на аргументы-ключи и аргументы-номера регионов строятся согласно следующим определениям операторов: hit(lq;R;) / miss(k; ;Rj) происходит, если

(а) перед ним есть обращение по тому же ключу (к*) в тот же регион (R,),

(Р) после которого и до этого обращения соответствующая строка не была вытеснена / была вытеснена из таблицы.

Трансляция свойства а достаточно очевидна, трансляция свойства /3 рассматривается в разделе 2.5.

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

енные согласно алгоритму, не дают решений, не соответствующих тестовому шаблону, и задают все решения, соответствующие тестовому шаблону. Значение атрибута модели устройства, задающего стратегию вытеснения, равное попе, означает, что при неуспешном обращении в это устройство замещение не производится. Здесь и далее символами ti,t2,...,tm обозначаются аргументы-ключи инициализирующих обращений, ri,r2,...,rm — аргументы-регионы инициализирующих обращений, к\, ..., кп — аргументы-ключи обращений в инструкциях тестового шаблона, Ri, R2,..., Rn аргументы-регионы обращений в инструкциях тестового шаблона, Si, S2,..., Sn — успешности обращений в инструкциях тестового шаблона (Si = hit или Si = miss).

Теорема 1 (Корректность алгоритма генерации ограничений на ключи обращений для таблицы, стратегия вытеснения которой не попе). Если построенная для последовательности обращений в таблицу (S\,ki,R\), (S2, ki, R2), ..., (Sn, кп, Rn) с дополнительным предикатом Р(к\, к^,..., кп, Ri, R2, ■■■, Rn) система ограничений является совместной, то ее решение t\,ti, Гь

Т2, •••) rmi ki,k2,...,kn, Ri, Л2j Rn, удовлетворяет последовательности Si,..., Sn и P при любом начальном состоянии таблицы.

Теорема 2 (Полнота алгоритма генерации ограничений на ключи обращений для таблицы, стратегия вытеснения которой есть попе). Если при данном начальном состоянии таблицы со стратегией вытеснения попе для последовательности обращений в нее (Si,kx,R\), (S2, к2, R2), ■■■, (Sn,k„,Rn) с дополнительным предикатом Р(к\, ¿2, •••, кп, R\, R2, •••> Rn) существует удовлетворяющая ей последовательность ключей, то система ограничений согласно соответствующему алгоритму будет совместной.

Стратегию вытеснения будем называть существенно вытесняющей, если w промахов в один регион полностью вытесняют его предыдущее содержимое (w — значение параметра lines таблицы).

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

со стратегией вытеснения не попе для последоват.ельности обращений в нее (Si,ki,Ri), (S2,k2,R.2), (Sn,kn,R„) с дополнительным предикатом P(k\, k2,-..,kn,R\, R2,...,Rn) существует. удовлетворяющая ей последовательность ключей, то система ограничений согласно соответствующему алгоритму будет совместной, если стратегия вытеснения является «существенно вытесняющейi>.

В разделе 2.3.2 рассматриваются таблицы вытеснения, которые "позволяют формализовать стратегии вытеснения. Таблицы вытеснения были предложены в 2008 году исследователями из Университета Саарланда. С использованием таблиц вытеснения в разделе 2.3.3 сформулированы и доказаны теоремы о том, что стратегии вытеснения LRU, FIFO и Pseudo-LRU являются существенно вытесняющими:

Теорема 4. Стратегия вытеснения LRU является существенно вытесняющей.

Теорема 5. Стратегия вытеснения FIFO является существенно вытесняющей.

Теорема 6. Стратегия вытеснения Pseudo-LRU является существенно вытесняющей.

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

Утверждение 1 (Верхняя оценка количества инициализирующих обращений).

т^п- (п + 2w)

где w — значение параметра lines таблицы, п — количество обращений в таблицу в шаблоне.

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

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

m^n-w + M

где М - количество элементов последовательности Si, S2,..., Sn, равных miss.

В разделе 2.4 предложено новое определение стратегии вытеснения Pseudo-LRU. Обычно при определении Pseudo-LRU предлагают рассматривать для региона упорядоченное бинарное дерево с пометками в нелистовых вершинах, листовым вершинам дерева соответствуют строки региона. Как и прежде, обращения осуществляются к одной из листовых вершин дерева, что приводит к изменению пометок вершин пути в неё из корневой вершины. Вытесняемая строка определяется также на основе пометок вершин дерева. Новое определение задает стратегию вытеснения Pseudo-LRU как изменение битовых векторов (Pseudo-LRU-eemeeit), сопоставленных строкам региона. Это определение позволит сократить количество ограничений и ускорить их разрешение. Сформулирована и доказана теорема, задающее изменение Pseudo-LRU-вет-вей и показывающая эквивалентность нового определения Pseudo-LRU старому (W = log2w, для стратегии вытеснения Pseudo-LRU допустимы лишь те w, которые являются степенями двойки, абсолютная позиция(пли просто, позиция) это номер строки в регионе, относительная позиция позиции i относительно позиции j будем назыаать г ф j и обозначать как 7rj):

Теорема 8 (Инвариантность преобразования Pseudo-LRU-ветвей относительными позициями). Пусть (ai Qa ... aw) ~ Pseudo-LRU-eemeb некоторой позиции i. Тогда изменение этой ветви согласно стратегии вытеснения Pseudo-LRU определяется только относителыюй позицией (относительно i) и происходит следующим образом при обращении к ключу с (абсолютной) позицией j: если ж) € [ft, тргт) для некоторого k = 1,2,..., W, то происходит изменение ai := 0, ai := 0, ..., a^-i := 0, ак := 1; если х} = 0, то

происходит изменение ai := 0, := О, ..., aw '■= 0; вытеснение ключа на позиции i происходит в том случае, когда ац = 1 Л аг = 1 Л ... Л an' = 1.

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

В разделе 2.5.1 предложено и формально обосновано представление свойства «быть вытесненным» для стратегии вытеснения LRU в виде ограничений, составленное по методу полезных обращений («||» — операция битовой конкатенации, выражение [ф] равно 1, если ф истинно, и равно 0 в противном случае):

Теорема 9 (Выражение свойства «быть вытесненным» для LRU). Пусть (ti,ri), (^2]7*2)1 (t,n,I'm) - ключи и регионы инициализирующих обращений, (ki, Ri) - ключ и регион обращения, для которого описывается вытеснение (будем его называть <гвытесняемым»), причем (fc,-||.Rj) € {(ii||fi), ••■, (i.n|jrm), (fci||fli), ...,. МЛ;-!)} u{(fi||ri),...,(tm||rm)} - все разные. Тогда ki не вытеснен из региона Ri согласно определению LRU на перестановках тогда и только тогда, когда

7=1

где последовательность в = ((^Нп),..., (£т||гт), (^Ц/?!),..., (А^ЦЛл)}, R(si) — вторая компонента (регион), а формула полезного обращения

такая:

= $ {sj,...,sm+n}Afli = R{sj) Л sj {sj+b...,s,n+n})

В разделе 2.5.2 предложено и формально обосновано представление свойства «быть вытесненным» для стратегии вытеснения FIFO в виде ограничений, составленное по методу полезных обращений.

В разделе 2.5.3 предложено и формально обосновано представление свойства «быть вытесненным» для стратегии вытеснения Pseudo-LRU в виде ограничений, составленное по методу полезных обращений:

Теорема 10 (Выражение свойства «быть вытесненным» для Pseudo-LRU). Пусть (ii,ri), (¿2jг2)> ••■> (im:rm) - ключи и регионы инициализирующих обращений, (hi, Ri) - ключ и регион обращения, для которого описывается вытеснение (будем его называть «вытесняемым*), причем € {(iilln), ■•v (fj|rm), ..., (Vi|№-i)} u {(til|n),-,(fm||rro)} - все разные. Тогда k не вытеснен из региона R согласно определению на ветвях бинарного дерева тогда и только тогда, когда

m-fn

^КлхЫ) < w i'=i

где последовательность s = ((ii||ri),..., (fm||rm), (fci||i?i),..., (¿„||Я„)), R(si) — вторая компонента s,- (регион), а формула полезного обращения такая:

(ki\№ i {в. Ri = R(sj)

(тГ,'||Я<) 6 {(^||^),(^+1||Д;Ч1),...,(7Гт+п||й,п+п)} m+n

Д (Rj = Rk А *=j+l

P(x, у) = (y > x A x ф у > x)

тг{ определено следующим образом: если 5¿ = hit, то

ate ((fcilli?,-) = M-ñ¿-i)) (Jtí = 7ri_x)

ate ((Ы1Ъ) = M*¡-2)) W = íri-2) ... « = 0);;;..

если S¡ = miss, mo f {тг,-,..., 7Tj}m обозначает подмножество множества позиций от i 'го до j 'го обращения из неуспешных обращений):

ate ((fc¿||fí£) = M-ü-i)) К = 7Г,--г)

ate ((fc¿||ñ¡) = (fc¿-2||i?¿-2)) к = TTi-2 A n'i 6 {7r¡-i}m)

Cite ((Aj||jB¡) = (fcí-sIlHi-s)) (jtí = TTi-a A 7r¡ € {тг;_ь1г;_2}т)

... (я{ = о);;;.. j

7Гг — позиции — дополнительные переменные, для которых надо построить ограничения: конъюнкцию для каждой пары (s¿,7r¿) и (sj,iTj) при j > i ограничений:

• если j'e обращение успешное, то (7r¿||fí(s¡) = tíj\\R(sj) А

7r¿||ü(s¿) i {7Tmi||ñ(smi),7rm2||ñ(sm2),...,7rmJ|ñ(smJ}) s{ = sj

• в противном случае (7r¿||.fi(s¡) = 7r,||ñ(sj) Л

НЖ 7712

где (7rmi, Ä(.smi)), (irm2, R{sm)),..., (тттп, R(smn)) - позиции и регионы неуспешных обращений, расположенных между i 'м и j 'м.

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

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

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

В третьей главе дается оценка предлагаемым методам. В разделах 3.1, 3.2 и 3.3 показывается, что подсистемы управления памяти микропроцессоров архитектур MIPS, PowerPC и IA-32 можно представить в виде набора таблиц и формализовать варианты инструкций, оперирующих с памятью. Причем имеется документация по каждой архитектуре, где эти варианты уже описаны на соответствующем псевдокоде. В разделе 3.4 описана автоматизация некоторых этапов предлагаемого во второй главе подхода: генератор ограничений, решатель ограничений и конструктор текстов тестовых программ. Решатель ограничений это внешний инструмент (Z3) и разрабатывать его для автоматизации подхода не надо, что сильно сокращает трудоемкость автоматизации подхода. Затронут вопрос переиспользования перечисленных компонентов при смене микропроцессора. Был реализован прототип генератора тестовых программ для архитектуры MIPS64. В разделе 3.5 описаны эксперименты над этим прототипом по оценке времени построения тестовых программ и вероятности завершения построения за 60 секунд. Эксперименты показали увеличение допустимого размера тестовых шаблонов до 9-12 инструкций (по сравнению с 2-3 инструкциями в доступных инструментах). В разделе 3.6 проведено сравнение с инструментом Genesys-Pro (IBM): выделены сходства и отличия, преимущества и недостатки предложенных методов по сравнению с Genesys-Pro. В разделе 3.7 проведено сравнение с работами, проводящимися в Intel.

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

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

1) Предложен подход к построению тестовых программ для проверки подсистем управления памяти микропроцессоров на основе формализации документации и техники ограничений.

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

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

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

5) На основе предложенных моделей и методов создан прототип системы построения тестовых программ для проверки подсистем управления памяти микропроцессоров архитектуры М1РБ64 и проведены эксперименты для оценки эффективности разработанного прототипа.

Публикации по теме диссертации

[1] Корныхин, Е. В. Генерация тестовых данных для тестирования арифметических операций центральных процессоров / Е. В. Корныхин // Труды Института Системного Программирования. — 2008. — Т. 15. — С. 107 117.

[2] Корныхин, Е. В. Система генерации тестовых программ с использованием ограничений ТЕСЛА / Е. В. Корныхин // Сборник тезисов конференции Ломоносов. — 2009. — С. 39.

[3] Корныхин, Е. В. Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА / Е. В. Корныхин // Сборник тезисов конференции «Микроэлектроника и информатика». — 2009. — С. 87.

[4] Корныхин, Е. В. Генерация тестовых данных для системного функционального тестирования микропроцессоров с учетом кэширования и трансляции адресов / Е. В. Корныхин // Труды Института Системного Программирования. — 2009. — Т. 17. — С. 145-160.

[5] Корныхин, Е. В. Генерация тестовых данных для системного функционального тестирования АЬ-кэш-памяти микропроцессоров / Е. В. Корныхин // Вычислительные методы и программирование. — 2009. — Т. 10. — С. 107-116.

[6] Корныхин, Е. В. Генерация тестовых данных для тестирования механизмов кэширования и трансляции адресов микропроцессоров / Е. В. Корныхин // Программирование. — 2010. — Т. 36, № 1. — С. 40-49.

[7] Корныхин, Е. В. Метод зеркальной генерации ограничений для построения тестовых программ по тестовым шаблонам / Е. В. Корныхин // Труды Института Системного Программирования. — 2010. — Т. 18. — С. 67-80.

[8] Корныхин, Е. В. Определение стратегии вытеснения pseudolru на ветвях бинарного дерева / Е. В. Корныхин // Сборник тезисов конференции Ломоносов. - 2010. - С. 20-21.

[9] Kornikhin, Е. Test data generation for arithmetic subsystem of cpus mips64 / E. Kornikhin // Proceedings of Spring Young Researchers Colloqium on Software Engineering. - 2008. - Vol. 2. - Pp. 43-46.

[10] Kornikhin, E. Smt-based test program generation for cache-memory testing / E. Kornikhin // Proceedings of East-West D TS.- 2009. - Pp. 124-127.

[11] Kornikhin, E. Test data generation for lru cache-memoTy testing / E. Kornikhin // Proceedings of Spring Young Researchers Colloqium on Software Engineering. - 2009. - Pp. 88-92.

Подписано в печать:

10.09.2010

Заказ № 4093 Тираж - 75 экз. Печать трафаретная. Типография «11-й ФОРМАТ» ИНН 7726330900 115230, Москва, Варшавское ш., 36 (499) 788-78-56 www.autoreferat.ru

Введение

1 Исследование методов построения тестовых программ

1.1 Системное тестирование микропроцессоров.

1.2 Тестирование подсистем управления памяти.

1.3 Методы целенаправленного построения тестовых программ

1.3.1 Методы на основе массовой генерации тестовых программ

1.3.2 Методы непосредственного построения тестовых программ.

1.4 Анализ существующих методов целенаправленного построения тестовых программ.

1.5 Уточненная постановка задачи.

2 Описание предлагаемых методов и моделей

2.1 Подход к генерации тестовых программ.

2.2 Моделирование устройств подсистемы управления памяти и вариантов исполнения инструкций

2.3 Метод построения ограничений.

2.3.1 Алгоритмы.

2.3.2 Таблицы вытеснения.

2.3.3 Существенно вытесняющие стратегии вытеснения

2.4 Новое определение стратегии вытеснения

Pseudo-LRU

2.5 Метод полезных обращений для записи стратегии вытеснения в виде ограничений.

2.5.1 Метод полезных обращений для стратегии вытеснения LRU

2.5.2 Метод полезных обращений для стратегии вытеснения FIFO.

2.5.3 Метод полезных обращений для стратегии вытеснения Pseudo-LRU

2.5.4 Разрешение ограничений, описывающих стратегии вытеснения

2.6 Конструирование текста тестовой программы.

3 Применение предлагаемых методов, сравнение с аналогамиЮЗ

3.1 Генерация тестов для архитектуры MIPS.

3.2 Генерация тестов для архитектуры PowerPC.

3.3 Генерация тестов для архитектуры IA-32.

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

3.5 Эксперименты по оценке допустимой сложности тестовых шаблонов

3.6 Сравнение с Genesys-Pro.

3.7 Сравнение с работами Intel.

Актуальность

Современные микропроцессоры — сложные многокомпонентные системы. Размеры современных микропроцессоров оцениваются как 107 — 108 вентилей[41]. Естественно при разработке таких сложных систем в проекты микропроцессоров вносятся ошибки, порой довольно критичные[20]. Поэтому для обнаружения этих ошибок в цикл разработки микропроцессора в обязательном порядке входят этапы функциональной верификации.

Чем позднее будут обнаружены ошибки в микропроцессорах, тем дороже обойдётся исправление ошибок: сделать это в готовой микросхеме, тем более выпущенной на рынок, практически невозможно. Тем актуальнее становятся методы обнаружения ошибок на ранних этапах разработки микропроцессоров. Цикл разработки предполагает подготовку микропроцессоров в виде исполнимых программных моделей на языках Уеп^ или УНБЬ[19]. Это делает возможным проведение функциональной верификации на таких моделях (т.е. до производства самих микропроцессоров) и актуальным исследование методов такой верификации. Целью функциональной верификации программных моделей микропроцессоров является обнаружение ошибок реализации функциональности в программных моделях микропроцессоров.

Выделяют следующие виды функциональной верификации: экспертизу, имитационное тестирование и формальную верификацию[10]. Экспертиза предполагает анализ текстов моделей экспертами с целью оценки их корректности и обнаружения ошибок. Этот вид функциональной верификации эффективно применяется на ранних стадиях разработки. Однако, ввиду наличия человеческого фактора, после экспертизы ошибки в микропроцессоре всё же остаются. Методы формальной верификации позволяют дать исчерпывающий ответ на вопрос о корректности отдельных модулей и всего микропроцессора. Однако трудоемкость формальной верификации чрезвычайно велика. Например, при разработке Intel Pentium 4 были формально верифицированы модуль работы с плавающей точкой (FPU), модуль декодирования инструкции и логика внеочередного выполнения (out-of-order), было найдено порядка 20 новых ошибок, однако трудоемкость этого проекта составила порядка 60 человеко-лет[20].

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

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

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

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

Цель работы

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

Для достижения этой цели были поставлены следующие задачи:

1) исследовать описанные в научной литературе методы построения тестовых программ на предмет их применимости для системного тестирования подсистем управления памяти микропроцессоров;

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

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

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

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

3) предложена формальная модель инструкций, описывающая отдельные пути их выполнения в виде утверждений о свойствах параметров инструкций и модельном состоянии устройств;

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

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

Разработанные модели и методы могут быть использованы коллективами, занимающимися разработкой микропроцессоров, для автоматизации построения тестовых программ. Разработанный прототип системы построения тестовых программ использовался для генерации тестов подсистем управления памяти ряда микропроцессоров архитектуры М1Р864. Результаты работы могут быть использованы в исследованиях, которые ведутся в Институте системного программирования РАН, Московском государственном институте электроники и математики, НИИ системных исследований РАН, Институте точной механики и вычислительной техники им. С.А. Лебедева РАН, Институте проблем информатики РАН и других научных и промышленных организациях.

Публикации

По материалам диссертации опубликовано одиннадцать работ [3, 5, б, 8, 9, 11-13, 47-49], в том числе одна [11] в издании, входящем в перечень ведущих рецензируемых научных журналов и изданий ВАК.

Структура работы

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

Об обозначениях

Наиболее значимые утверждения помечены как «Теоремы», доказательства большинства из них помещены в приложении А. Менее значимые утверждения помечены как «Утверждения». Обоснования «Утверждений» обычно представлены непосредственно перед формулировкой «Утверждений». Вспомогательные утверждения помечены как «Леммы».

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

1) Предложен подход к построению тестовых программ для проверки подсистем управления памяти микропроцессоров, позволяющий понизить сложность построения некоторого класса тестовых программ. Этот класс состоит из тестовых программ, в которых имеется цепочка длиной от 6 до 12 инструкций обращения к памяти. Понижение сложности обосновано при помощи ряда экспериментов на прототипе программного средства построения тестовых программ. Теоретически обоснована корректность алгоритмов в рамках предложенного подхода к построению тестовых программ. В рамках: предложенного подхода разработаны модели устройств подсистемы управления памяти и модели вариантов исполнения инструкций.

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

Заключение

1. http://wwwлntel.com/design/intaxch/papeгs/cache6.htm.

2. Воробьев, Д. Н. Генерация тестовых программ для подсистемы управления памятью микропроцессоров / Д. Н. Воробьев, А. С. Камкин // Труды Института Системного Программирования РАН. — 2009. — Т. 17.- С. 119-132.

3. Корныхин, Е. В. Генерация тестовых данных для тестирования арифметических операций центральных процессоров / Е. В. Корныхин // Труды Института Системного Программирования. — 2008. — Т. 15. — С. 107-117.

4. Камкин, А. С. Комбинаторная генерация тестовых программ для микропроцессоров на основе моделей / А. С. Камкин // Препринт Института Системного Программирования РАН. — 2008. — Т. 21.

5. Корныхин, Е. В. Система генерации тестовых программ с использованием ограничений ТЕСЛА / Е. В. Корныхин // Сборник тезисов конференции Ломоносов. — 2009. — С. 39.

6. Корныхин, Е. В. Система генерации тестовых данных для системного функционального тестирования микропроцессоров ТЕСЛА / Е. В. Корныхин // Сборник тезисов конференции «Микроэлектроника и информатика». — 2009. — С. 87.

7. Корныхин, Е. В. Генерация тестовых данных для системного функционального тестирования микропроцессоров с учетом кэширования и трансляции адресов / Е. В. Корныхин // Труды Института Системного Программирования. — 2009. — Т. 17. — С. 145-160.

8. Корныхин, Е. В. Генерация тестовых данных для системного функционального тестирования fifo-кэш-памяти микропроцессоров / Е. В. Корныхин // Вычислительные методы и программирование. — 2009. — Т. 10.- С. 107-116.

9. Камкин, А. С. Функциональная верификация микропроцессоров: борьба с ошибками и управление качеством / А. С. Камкин // Электроника: Наука, Технология, Бизнес. — 2010. — по. 3.

10. Корныхин, Е. В. Генерация тестовых данных для тестирования механизмов кэширования и трансляции адресов микропроцессоров / Е. В. Корныхин // Программирование. — 2010. — Т. 36, № 1. — С. 40-49.

11. Корныхин, Е. В. Метод зеркальной генерации ограничений для построения тестовых программ по тестовым шаблонам / Е. В. Корныхин // Труды Института Системного Программирования. — 2010. — Т. 18. — С. 67-80.

12. Корныхин, Е. В. Определение стратегии вытеснения pseudolru на ветвях бинарного дерева /. Е. В. Корныхин // Сборник тезисов конференции Ломоносов. — 2010. — С. 20-21.

13. Томпсон, Б. Управление памятью / Б. Томпсон // Computerworld Россия.— 2001.— № 22.

14. Касперски, К. Техника оптимизации программ. Эффективное использование памяти / К. Касперски. — СПб.: БХВ-Петербург, 2003. — Р. 560.

15. Применение технологии UniTESK для функционального тестирования моделей аппаратного обеспечения / В. П. Иванников, А. С. Камкин,

16. В. В. Кулямин, А. К. Петренко. N0. 8.— М.: Препринт Института системного программирования РАН, 2005. — Р. 26.

17. Apt, K. R. Constraint Logic Programming using Eclipse / K. R. Apt, M. Wallace. — New York, NY, USA: Cambridge University Press, 2007.

18. Ashenden, P. J. The Designer's Guide to VHDL / P. J. Ashenden. — Elsevier, 2008.

19. Bentley, B. Validating the intel pentium 4 processor / B. Bentley, R. Gray // Intel Technology Journal. — 2001.

20. Borger, E. Abstract State Machines: A Method for High-Level System Design and Analysis / E. Borger, R. Stark. — Springer-Verlag, 2003.

21. Clarke, E. M. Model Checking / E. M. Clarke, O. Grumberg, D. A. Peled.— Cambridge, MA: MIT Press, 1999.

22. Evaluation of cardinality constraints on smt-based debugging / A. Sülflow, R. Wille, G. Fey, R. Drechsler // Multiple-Valued Logic, IEEE International Symposium on. — 2009. Vol. 0. - Pp. 298-303.

23. Expression: A . language for architecture exploration through compiler/simulator retargetability. / A. Halambi, P. Grun, V. Ganesh et al. // Proceedings of the European Conference on Design, Automation and Test. 1999. - Pp. 485-490.

24. Fallah, F. A new functional test program generation methodology / F. Fallah, K. Takayama // Proceedings 2001 IEEE International Conference on Computer Design: VLSI in Computers and Processors.— 2001.— Pp. 76-81.

25. Formal verification of backward compatibility of microcode / T. Arons,

26. E. Elster, L. Fix et al. // Lecture Notes in Computer Science. — 2005. — Vol. 3576/2005.-Pp. 185-198.

27. Frey, B. PowerPC Architecture Book / B. Frey. — IBM, 2005.

28. Fully automatic test program generation for microprocessor cores /

29. F. Corno, G. Cumani, S. M. Reorda, G. Squillero // DATE '03: Proceedings of the conference on Design, Automation and Test in Europe. — Washington, DC, USA: IEEE Computer Society, 2003.- P. 11006.

30. Functional verification of the equator maplOOO microprocessor / J. Shen, J. Abraham, D. Baker et al. // DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference. — New York, NY, USA: ACM, 1999. — Pp. 169-174.

31. Functional verification of the hp pa 8000 processor / S. T. Mangelsdorf, R. E Gratias, R. M. Blumberg, R. Bhatia // Hewlett-Packard Journal — 1997. — август. — Pp. 1-13.

32. Genesys-pro: Innovations in test program generation for functional processor verification / A. Adir, E. Almog, L. Fournier et al. // IEEE Design and Test of Computers. — 2004. — Mar/Apr. Vol. 21, no. 2. — Pp. 84-93.

33. Genetic Programming — An Introduction / W. Banzhaf, P. Nordin, R. Keller, F. Francone. — Morgan Kaufmann, 1998.

34. Grund, D. Estimating the performance of cache replacement policies /

35. D. Grund, J. Reineke // 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2008), June 57, 2008, Anaheim, С A, USA. 2008. - Pp. 101-112.

36. Hennenhoefer, E. The Evolution of Processor Test Generation Technology /

37. E. Hennenhoefer, M. Typaldos. — Obsidian Software Inc.

38. Hennessy, J. L. Computer architecture: a quantitative approach / J. L. Hennessy, D. A. Patterson, A. C. Arpaci-Dusseau. — 4 edition.— Morgan Kaufmann, 2007.

39. Ho, C.-M. R. Validation tools for complex digital designs: Tech. rep. / CM. R. Ho: 1996.

40. IA-32 Intel Architecture Software Developer's Manual. — Intel, 2006.

41. Industrial experience with test generation languages for processor verification / A. Adir, E. Almog, L. Fournier et al. // IEEE Design and Test of Computers. — 2004. — Mar./Apr. — Vol. 21, no. 2. — Pp. 84-93.

42. Kohno, K. A new verification methodology for complex pipeline behavior / K. Kohno, N. Matsumoto // Proceedings of the 38st Design Automation Conference (DAC'01). — 2001.

43. Koo, H.-M. Functional test generation using design and property decomposition techniques / H.-M. Koo, P. Mishra // ACM Transactions on Embedded Computer Systems. — 2009. — Vol. 8, no. 4.

44. Kornikhin, E. Test data generation for arithmetic subsystem of cpus mips64 / E. Kornikhin // Proceedings of Spring Young Researchers Colloqium on Software Engineering. — 2008. — Vol. 2. — Pp. 43-46.

45. Kornikhin, E. Smt-based test program generation for cache-memory testing / E. Kornikhin // Proceedings of East-West D T S.— 2009.— Pp. 124-127.

46. Kornikhin, E. Test data generation for lru cache-memory testing / E. Kornikhin // Proceedings of Spring Young Researchers Colloqium on Software Engineering. — 2009. — Pp. 88-92.

47. Maatg: A functional test program generator for microprocessor verification / T. Li, D. Zhu, Y. Guo et al. // Proceedings of the 2005 8th Euromicro conference on Digital System Design (DSD'05). — 2005.

48. McMillan, K. L. Symbolic Model Checking / K. L. McMillan. — Kluwer Acadcmic Publishers, 1993.

49. MIPS Technologies. — MIPS64™ Architecture For Programmers. Volume II: The MIPS64™ Instruction Set, 2001.

50. MIPS Technologies. — MIPS64™ Architecture For Programmers. Volume III: The MIPS64™ Privileged Resource Architecture, 2001.

51. Mishra, P. Automatic functional test program generation for pipelined processors using model checking / P. Mishra, N. Dutt // High-Level Design, Validation, and Test Workshop, IEEE International. — 2002. — Vol. 0. — Pp. 99-103.

52. Mishra, P. Graph-based functional test program generation for pipelined processors / P. Mishra, N. Dutt //In Proceedings of Design Automation and Test in Europe (DATE. 2004. - Pp. 182-187.

53. Mishra, P. Functional coverage driven test generation for validation of pipelined processors / P. Mishra, N. Dutt. — 2005. — Pp. 678-683.

54. On the test of microprocessor ip cores / F. Corno, M. S. Reorda, S. Squillero, M. Violante // DATE '01: Proceedings of the conference on Design, automation and test in Europe. — Piscataway, NJ, USA: IEEE Press, 2001.-Pp. 209-213.

55. Pentium Pro Family Developer's Manual Volume 3: Operating System Writer's Guide. — Intel, 1996.

56. Petters, S. Intel architecture software developer's manual volume 3: System programming: Tech. rep. / S. Petters: 2001.

57. Powerpc g5 user's manual: Tech. rep.: IBM, 2008.

58. The RAISE specification language / C. George, P. Haff, K. Havelund et al. — Prentice Hall Europe, 1992.

59. Shiva, S. G. Computer design and architecture / S. G. Shiva. — 3d edition. — Atlantic/Little, Brown, 2000.

60. Ur, S. Micro architecture coverage directed generation of test programs / S. Ur, Y. Yadin // DAC '99: Proceedings of the 36th annual ACM/IEEE Design Automation Conference.— New York, NY, USA: ACM, 1999.— Pp. 175-180.

61. Using a constraint satisfaction formulation and solution techniques for random test program generation / E. Bin, R. Emek, G. Shurek, A. Ziv // IBM Systems Journal. — 2002. Vol. 41, no. 3. - Pp. 386-402.

62. Wang, L.-T. Electronic Design Automation: Synthesis, Verification, and Test / L.-T. Wang, Y.-W. Chang, K.-T. Cheng. — Morgan Kaufmann, 2009.

63. Wood, B. A. Verifying a multiprocessor cache controller using random test generation / D. A. Wood, G. A. Gibson, R. H. Katz // IEEE Design and Test of Computers. 1990. - Vol. 7. - Pp. 13-25.

64. Yeager, K. C. The mips rlOOOO superscalar microprocessor / K. C. Yeager // IEEE Micro. — 1996. Vol. 16, no. 2. - Pp. 28-40.