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

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

005056500

СТОТЛАНД Ирина Аркадьевна

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

Специальность 05.13.15 -

«Вычислительные машины, комплексы и компьютерные сети»

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата технических наук

Москва 2012

005056500

Работа выполнена на кафедре «Вычислительная техника» Федерального государственного бюджетного образовательного учреждения высшего профессионального образования «Московский государственный технический университет радиотехники, электроники и автоматики» (МГТУ МИРЭА).

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

кандидат технических наук, доцент Деменкова Татьяна Александровна

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

Назаров Александр Викторович

доктор технических наук, профессор МАИ (НИУ), профессор, зав. кафедрой

Басок Борис Моисеевич

кандидат технических наук, доцент МГТУ МИРЭА, доцент

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

ОАО «Научно-исследовательский институт вычислительных комплексов им. М.А. Карцева»

Защита состоится «9» ноября 2012 г. в 14 часов 00 минут на заседании диссертационного совета Д212.131.05 при МГТУ МИРЭА по адресу: г. Москва, пр-т Вернадского, д. 78, ауд. Д-412.

С диссертацией можно ознакомиться в библиотеке МГТУ МИРЭА.

Автореферат разослан «7» октября 2012 г.

Ученый секретарь

диссертационного совета — Е.Г. Андрианова

к.т.н, доцент

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Современное развитие микропроцессоров и вычислительных комплексов на их основе идет по направлению увеличения числа процессорных ядер в системе и расширения функциональных возможностей, что достигается как повышением уровня микроэлектронной технологии, используемой для производства микропроцессоров, так и применением новых архитектурных и структурных вариантов их реализации. Одним из основных методов обеспечения функциональной надежности микропроцессорных вычислительных комплексов (МВК) является их верификация на этапе разработки. Стоимость исправления ошибок увеличивается в десятки и даже сотни раз при переходе от более ранних этапов маршрута проектирования к более поздним. В связи с этим ошибки необходимо выявлять и исправлять еще на этапе логического проектирования. Для этого применяют функциональную верификацию, объектами которой являются логические модели микропроцессоров уровня регистровых передач (Register Transfer Level, RTL-модели), а также их системные модели и спецификации.

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

Современное состояние области функциональной верификации МВК характеризуется независимым развитием каждого из направлений. Вопросам динамической верификации микропроцессоров и МВК посвящен ряд работ отечественных и зарубежных ученых: Камкина A.C., Чупилко М.М., Белкина В.В., Шаршунова С.Г., Мишра П., ДутгаН., БергеронаД., Лама В. и других. Проблема формальной верификации программно-аппаратных систем (в том числе МВК) рассматривается в работах Коннова И.В., Карпова Ю.Г., Кларка Э., Харрисона Д., Намьёши К.С. и других. Однако на сегодняшний день отсутствуют методики комплексной функциональной верификации МВК. При этом автономное использование одного из направлений функциональной верификации грозит снижением уровня качества проверки. Большинство существующих работ по функциональной верификации микропроцессоров и МВК посвящено исследованию конвейеризированных модулей управляющей логики, в то время как далеко не все функциональные модули, входящие в состав МВК, имеют конвейеризированную архитектуру. Анализ официальных перечней

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

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

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

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

МВК.

2. Классификация функциональных модулей, входящих в состав МВК, с точки зрения их функциональной верификации. Определение класса модулей системного обмена (МСО), разработка концептуальной модели МСО.

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

4. Разработка методов, алгоритмов и программного обеспечения для динамической верификации МСО на основе автоматной модели МСО.

5. Разработка и адаптация методов, алгоритмов и программного обеспечения для формальной верификации МСО на основе автоматной модели МСО.

6. Разработка методики комплексной функциональной верификации МСО МВК, основанной на разработанных и адаптированных методах и алгоритмах динамической и формальной верификации МСО.

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

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

программирования, теории алгоритмов.

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

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

2. Разработаны концептуальная и автоматная модели МСО. Сформулированы критерии принадлежности функционального модуля МВК к классу модулей системного обмена.

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

4. Разработан новый алгоритм сравнения последовательностей реакций верифицируемой ЛТЬ-модели и эталонной модели уровня базовых транзакций для динамической верификации МСО, учитывающий функциональные особенности соответствующего МСО. На основе данного алгоритма предложен метод организации устройства проверки, позволяющий автоматизировать процедуру проверки реакций и изолировать устройство проверки от генератора воздействий в тестовой системе.

5. Разработана семантическая модель МСО, позволяющая адаптировать формальный метод проверки модели путем трансляции полуформальной автоматной модели МСО в формальную модель, представляющую собой структуру Крипке.

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

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

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

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

назначения для повышения эффективности функциональной верификации и сокращения сроков ее проведения.

Практическая ценность работы подтверждается эффективностью применения предложенной методики при функциональной верификации микропроцессора «Эльбрус^», разрабатываемого в ЗАО «МЦСТ». Согласно акту о внедрении, использование разработанных методов динамической верификации МСО и методики комплексной функциональной верификации МСО позволило качественно улучшить верификацию спецификаций и логических моделей микропроцессоров и сократить трудоемкость разработки тестовых систем.

Научные положения диссертационной работы внедрены в учебный процесс на кафедре «Вычислительная техника» МГТУ МИРЭА при проведении лабораторных работ и подготовке лекционного материала по курсам «Проектирование цифровых устройств в САПР», «Моделирование», «Верификация проектов устройств и систем в САПР».

Результаты диссертации использованы в научно-исследовательской работе, выполненной Центром проектирования интегральных схем, устройств наноэлектроники и микросистем МГТУ МИРЭА по проекту №2.2.1.1/2411 «Развитие интеграции научной и образовательной деятельности университетского базового центра проектирования на основе работ по созданию высокопроизводительных методов автоматизированного проектирования СБИС, системному и приборному моделированию» АВЦП «Развитие научного потенциала высшей школы (2009-2011 годы)», о чем имеется акт о внедрении.

Апробация работы. Основные положения и результаты диссертационной работы докладывались и обсуждались на 17-ой и 18-ой Всероссийских межвузовских научно-технических конференциях студентов и аспирантов «Микроэлектроника и информатика-2010» и «Микроэлектроника и информатика-2011» (г.Москва, МИЭТ, 2010, 2011); 9-й, 10-ой и 11-ой научно-практических конференциях «Современные информационные технологии в управлении и образовании» (г. Москва, ФГУП НИИ «Восход», 2010-2012); XVII и XVIII Международных научно-практических конференциях студентов и молодых ученых «Современные техника и технологии» — СТТ-2011, СТТ-2012 (г.Томск, 2011, 2012); Международной научно-технической конференции «INTERMATIC-2011» (г. Москва, МГТУ МИРЭА, 2011); 59-ой, 60-ой, 61-ой НТК МИРЭА (г.Москва, МГТУ МИРЭА, 2010-2012); на Международной школе-семинаре «Cooperation of Information Technology between MIREA and RUAS» (Germany, Regensburg - RUAS, 17-19 сентября 2012 г.).

Публикации. По теме диссертации опубликовано 11 работ, в том числе 3 научные статьи в рецензируемых журналах, входящих в перечень рекомендованных ВАК РФ. Разработанный транслятор диаграмм состояний UML во входной язык верификатора SMV зарегистрирован в Отраслевом фонде алгоритмов и программ государственного координационного центра

информационных технологий (Инвентарный номер ВНТИЦ 502001250300 от 20.02.2012).

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка используемой литературы из 108 наименований, 8 приложений, содержащих описания разработанных программных средств, результаты апробации методики и дополнительные примеры и описания, акты о внедрении. Общий объем диссертации (исключая приложения) составляет 152 страницы , включая 20 рисунков и 14 таблиц.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

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

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

функционирования МСО. Логически завершенная последовательность действий, реализующая базовую функцию МСО, названа базовой операцией МСО.

Во второй главе построена концептуальная модель МСО, представляющая собой трехуровневую структуру: первый (нижний) уровень представления — уровень интерфейсных сигналов (инициирующих, реагирующих и управляющих); второй — уровень базовых и дополнительных транзакций МСО; третий — уровень базовых и дополнительных операций МСО. Базовая операция Р модуля системного обмена представляет собой набор инициирующих и реагирующих транзакций, приводящих операцию Р из начального состояния s0 в одно из финальных состояний Sj. Транзакция

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

Определение 1. Автоматной моделью базовой операции МСО называется иерархический расширенный конечный автомат АР = (s,Trans,V,T,Gp,F*j, где S

— множество состояний автомата; Trans — множество транзакций операции АР\ V — множество контекстных переменных, состоящих из подмножества входных параметров инициирующих транзакций Vinil, подмножества параметров реагирующих транзакций Vr и подмножества внутренних контекстных переменных операции Vjmcmal\ Т — множество переходов автомата; Gр — множество глобальных охранных предикатов; Fe5 — множество финальных состояний.

Каждая инициирующая транзакция tim е Trans представляет собой пару (X, I ,g, где Ху , —инициирующее воздействие транзакции /,„„, g,M — локальный охранный предикат транзакции tjnil. Каждая реагирующая транзакция treTrans представляет собой пару где —реакция транзакции tr,

о, — функция выхода транзакции tr.

Определение 2. Автоматной моделью МСО называется параллельная композиция иерархических расширенных конечных автоматов, описывающих базовые операции МСО.

На основе автоматной модели МСО разработаны формальные критерии принадлежности функционального модуля МВК к классу МСО.

Критерий 1Сцелостности транзакций). Пусть дано множество транзакций t = (S,Z,V) базовой операции Р, где Z — множество интерфейсных

сигналов транзакции (Z = {x,\v}), таких что 3 i = (l,N) и 3j = (l,N): ZjnZj ф 0, где inj- идентификаторы транзакций. Транзакция t, допустима в

конфигурации (i,v) Р, тогда и только тогда, когда V/ s(tj)^s'execj, где s\xecjе Ккц ) — состояние графа переходов транзакции в конфигурации (s,v) Р.

Критерий 2 (маркированности операции). Пусть Хр — множество инициирующих интерфейсных сигналов всех инициирующих транзакций базовой операции Р, Yp — множество выходных сигналов всех реагирующих транзакций Р. Тогда операция Р является маркированной, если отображение U: X р -» Yр является биективным.

Критерий 3 (переменной длительности операции). Пусть tp — время выполнения базовой операции Р в тактах сигнала системной частоты, t,j — время между началом выполнения двух транзакций базовой операции в тактах сигнала системной частоты, где i,j = (l,N) — идентификаторы транзакций. Базовая операция является операцией переменной длительности, если t * const и V/,y ts =£const. Если значения tp и Ц \/i,j ограничены сверху, т.е. tp <max_delay и yi,jtij^max_delay_transv, то такая операция называется операцией ограниченной переменной длительности. Если все параметры tn \/i,j не ограничены сверху и tp не ограничено сверху, то операция Р называется операцией неограниченной длительности.

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

В зависимости от способа выполнения потока операций выделены два основных класса МСО: с внеочередным исполнением операций и с упорядоченным исполнением операций.

Критерий 4 (прямой упорядоченности операций). Пусть Р - базовая операция МСО; px(tx) =Р и p2(t2) =Р, где и t2 — моменты выполнения перехода s,0 —> s,exec начальной транзакции Р для эквивалентных базовых операций р; и р2\ {lri} и {tr2j — множество моментов переходов sem —» sf для всех реагирующих транзакций Р. Тогда, если VPeD(MCO) t1 <t2 => Vr £ Transr tri <tr2, МСО является МСО с прямой упорядоченностью операций.

Критерий 5 (связанной упорядоченности операций). Пусть две базовые операции МСО Р и Р' имеют общие группы выходных интерфейсных сигналов, соответствующих реагирующим транзакциям операций Р и Р'; и — моменты выполнения перехода sl0 —»s,exec начальных транзакций Р и Р'; (lrl} и {t,2j — множество моментов переходов smc —> sf для всех реагирующих транзакций Trans \ Р и Рвыполняющихся на общих для Р и Р' группах выходных интерфейсных сигналов. Тогда, Р и Р' являются связанно упорядоченными операциями, если t, ^l2 => Vr S Trans'r trX ^tr2.

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

gen/{P},\\ , 1) => VP genlrans(P,{G}) => Mtrans serialize(trans,{g}), где genp — функция генерации последовательно-параллельного направленного и ограниченно-случайного потока операций МСО; gen,ra„s — функция трансляции базовой операции Р в последовательность базовых и дополнительных транзакций; G — глобальные предикаты транзакций; transjserialize — функция сериализации базовой транзакции trans; g - локальные предикаты транзакций.

Определение 3. Сериализацией транзакции t называется отображение вида 0(t)

' Х ITrans ~~> SBtI Х 1 В« ' (1)

где STlm— конечное множество состояний автомата базовой транзакции МСО на уровне TLM (Transaction Level Model); SBl, — конечное множество состояний автомата базовой транзакции МСО на уровне RTL; lTrans — конечное множество значений атрибутов инициирующей транзакции; 1В„ — конечное множество значений входных интерфейсных сигналов, инициирующих транзакцию t.

Основными компонентами генератора воздействий МСО (рис. 1, стр. 14) являются генератор операций, реализующий функцию genp\ транзакторы базовых операций реализующие функции genlra„s метода путем инкапсулированного преобразования базовых операций МСО в последовательности базовых транзакций; сериализаторы, реализующие функцию serialize метода. С учетом свойства маркированности операций (критерий 2), каждый из транзакторов однозначно идентифицирует реагирующие транзакции, полученные от более низкого уровня генератора воздействий.

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

В ответ на последовательность входных воздействий а'" = (й)'0" эталонная и верифицируемая модели выдают последовательности реакций и wRRTL=(w*TL0,...u)RRTlJ) соответственно. Задача устройства проверки — установить, эквивалентны ли последовательности реакций, полученные от верифицируемой и эталонной моделей.

Определение 4. RTL-модель и эталонная модель уровня базовых транзакций эквивалентны, ест Vcu'" выполняются равенства |iy*ri| = |ctf^| = .$ize

И V/ е {1.....size} 3 j е {l.....size}: а«п [/] = aRM [j\ aRm [/] e coRRTL, afi [/] e <.

Если верифицируемая модель является МСО с упорядоченными операциями, то ' =}■

Алгоритм сравнения последовательностей реакций верифицируемой RTL-модели и эталонной модели:

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

2. При получении реакции от верифицируемой RTL-модели запускается функция поиска модельной реакции в соответствующем буфере модельных реакций. Если МСО удовлетворяет одному из критериев упорядоченности операций (критерии 4-5), то анализируется только нулевой элемент буфера модельных реакций. Иначе, функция поиска последовательно сравнивает полученную реакцию со всеми элементами буфера модельных реакций до тех пор, пока реакции не совпадут или не будет просмотрен весь буфер. Если соответствующая модельная реакция обнаружена в буфере модельных реакций, то функция поиска возвращает значение «истина» и сопоставленная реакция удаляется из буфера модельных реакций, в противном случае функция возвращает «ложь».

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

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

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

Для представления автоматной модели МСО в виде структуры Крипке, являющейся исходной для метода проверки модели, разработана семантическая

модель МСО, необходимая для трансляции автоматной модели МСО в структуру Крипке.

Определение 5. Операционной семантикой иерархического расширенного автомата (ЕНА, Extended Hierarchical Automata) Н называется структура Крипке вида М = (S,S0,Step}, где S=CH — множество состояний структуры Крипке,

соответствующее множеству конфигураций исходного ЕНА; S(1 = Сои G S -

множество начальных состояний структуры Крипке, соответствующее множеству начальных конфигураций исходного ЕНА; Step — отношение переходов.

Определение 6. Для конфигурации расширенного автомата С# и события е е Е множество всех возможных переходов определяется следующим образом:

РТ(СН). ={teT(H)\{SRC(t)}^CH f\eACH\=G(t)},

где Т(Н) — множество всех переходов Н; {SRC(I)} — множество всех исходных состояний перехода /; G(t) — охранный предикат. Тогда множество ЕТ(Сц)е называется множеством допустимых переходов, если удовлетворяются следующие условия:

ЕТ(Сн)е&РТ(Сн)е и Vt,f^ET(CH)e:-Jt!=!t').

Определение 7. Функцией диспетчеризации множества допустимых переходов ЕНА для конфигурации Сн называется функция:

е.если ЕТ(СН )с Ф0;

dispatchf Сн ) =

q. если ЕТ(СН )ц Ф 0

(

3)

О в других случаях.

где s — последовательность переходов внутри Сн, приводящая СИ к стабильному состоянию (имеет наивысший приоритет и возвращается функцией в случае нестабильности конфигурации Сн), a q — последовательность допустимых переходов для конфигурации Сн-

Поведение ЕНА во времени можно определить с помощью двух правил переходов: правила прогресса и правила простоя.

Правило 1 (прогресса). Пусть даны две конфигурации ЕНА С = {g,v,qe,h) и С'= (g'.v',q'e ,h') С,С'е{Ся}. Если dispatch (С)*0, тогда отношение переход из С в С' определяется как С—рг"- ~>л;Гс,,сыс) С'.

Правило 2 (простоя). Пусть даны две конфигурации ЕНА С = (g,v,qe,h) и С' = (g' ,v' ,q't, И) С, С е {С„}. Если dispatch(C) = 0, тогда отношение перехода из С в С' определяется как С———>С'.

Отношение переходов структуры Крипке определяется следующим образом:

>е,если ЕТ(С) Step = ■ p,°*->q, если ЕТ(С)

—¡52—»-О, в других случаях.

slut

В третьей главе приведено описание разработанной методики комплексной функциональной верификации МСО, основанной на предложенных и адаптированных методах и алгоритмах динамической и формальной верификации МСО. Для проверки свойств, не реализованных в эталонной модели МСО, при динамической верификации МСО автором предложены дополнительные механизмы проверки, основанные на применении блока распределенных глобальных и локальных утверждений. Для поддержки метода организации устройства проверки также была разработана технология трансляции данных «BasePort» в виде шаблонного класса языка С++, эмулирующего регистровую организацию данных в языке System Verilog. На основе анализа технологий построения тестовых систем выбрана в качестве базовой универсальная технология верификации, позволяющая строить легко конфигурируемые, высокоуровневые, интероперабельные тестовые системы. Тестовая система, реализующая предложенные методы и механизмы динамической верификации МСО имеет архитектуру, представленную на рис. 1.

В качестве способа описания автоматной модели МСО были выбраны диаграммы состояний UML (UML Statecharts), удовлетворяющие всем сформулированным требованиям к методу спецификации МСО. Для реализации трансляции автоматной модели МСО в структуру Крипке на основе семантической модели МСО был разработан транслятор диаграмм состояний UML во входной язык верификатора SMV. Программа на входном языке верификатора SMV представляет собой формализованное описание структуры Крипке и перечень требований к модели в виде формул темпоральной логики

Методика комплексной функциональной верификации основана на предложенных и адаптированных методах, алгоритмах и средствах динамической и формальной верификации МСО. Основные шаги методики:

Шаг 1. Анализ неформальной текстуальной спецификации модуля на его принадлежность к классу МСО. На данном этапе в соответствии с критериями 4-5 также устанавливается тип МСО.

Шаг 2. Определение доменов базовых операций и транзакций МСО: О/МСО), 0,г(МС0). Для этого определяется множество инициирующих и реагирующих базовых транзакций с атрибутами и управляющими сигналами вида

Шаг 3. Разработка автоматной модели МСО уровня базовых транзакций в виде иМЬ-модели диаграмм состояний.

CTL.

X\Yi={X\Yatll;X\Ycmd}.

Отчет о результатах проверки

Рис. 1. Архитектура тестовой системы для динамической верификации МСО

Шаг 4. Разработка автоматных моделей базовых транзакций МСО уровня регистровых передач в виде иМЬ-моделей диаграмм состояний.

Шаг 5. Трансляция полученных на шагах 3-4 автоматных моделей в соответствующие структуры Крипке с помощью транслятора диаграмм состояний иМЬ во входной язык верификатора 8МУ и их формальная верификация. Анализ результатов.

Шаг 6. Разработка эталонной модели МСО уровня базовых транзакций или адаптация МСО-компонента моделирующего комплекса на основе технологии трансляции данных «ВаБеРоЛ» и правил адаптации компонентов моделирующего комплекса.

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

Шаг 8. Отладка тестовой системы и эталонной модели на направленных тестовых сценариях базовых операций.

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

В условиях временных ограничений на верификацию МСО формальная верификации МСО (шаги 3-5), разработка эталонной модели (шаг 6) и тестовой системы (шаг 7) могут проводиться параллельно. Шаги 1-2 выполняются инженером по верификации и не автоматизированы. Шаги 3-4 могут выполняться с помощью системы разработки иМЬ-моделей инженером-разработчиком ШЪ-модели МСО, архитектором МВК или инженером по верификации. Шаг 5 осуществляется автоматически. Разработкой эталонной модели МСО (шаг 6) занимается инженер-программист. Шаги 6-9 выполняются также инженером по верификации с помощью средств автоматизации и систем моделирования.

В четвертой главе представлены результаты практической апробации предлагаемой методики при функциональной верификации модулей микропроцессоров «Эльбрус-28» и «Эльбрус-4С+», разрабатываемых в ЗАО «МЦСТ». Подробно рассмотрен процесс верификации хост-контроллера микропроцессора «Эльбрус^». При комплексной функциональной верификации хост-контроллера было выявлено 59 ошибок. Около 7% ошибок обнаружено при формальной верификации спецификации. В процессе динамической верификации хост-контроллера разработано 169 тестовых сценариев, включающих в себя 135 сценариев на проверку базовых операций хост-контроллера, 13 нагрузочных тестовых сценария и 21 динамический сценарий. Перечень тестовых сценариев и описание обнаруженных ошибок представлены в приложении к диссертации.

Результаты апробации методики для других модулей микропроцессоров «Эльбрус-25» и «Эльбрус-4С+» (табл. 1) также показали возможность сокращения трудозатрат на разработку тестовых систем при использовании программного средства автоматизации методики построения тестовых систем («иТЕС») на 50-75% и эффективность применения компонентов программных

моделирующих комплексов в качестве эталонных моделей (сокращение трудозатрат на =45% и числа ошибок =35%).

Таблица 1. Результаты апробации методики_

Хост-контроллер 1.0 Модуль доступа к оперативной памяти Хост-контроллер 2.0

Проект «Эльбрус-28» «Эльбрус-28» «Эльбрус-4С+»

Стадия верификации Конечная Поздняя Ранняя

Трудозатраты на разработку и адаптацию эталонной модели, чел.-недель 29 4 Разработка не окончена

Трудозатраты на разработку тестовой системы, чел.-недель 12 6 3

Объем исходный ЯТЬ- модели, строки кода 15956 16364 12398

Способ разработки тестовой системы «вручную» с помощью иТЕО с помощью ШТЮ

Среднее покрытие по коду ЯТЬ-модели, % 97,6 91,2 74,3

Число ошибок в спецификации и ЯТЬ-модели 59 16 8

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

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

ОСНОВНЫЕ ВЫВОДЫ И РЕЗУЛЬТАТЫ РАБОТЫ

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

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

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

метода дает возможность сокращения трудозатрат на разработку и поддержку тестовых систем и эталонных моделей на 10-15% за счет применения высокоуровневых моделей и автоматизации сравнения реакций на уровне базовых транзакций МСО.

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

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

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

СПИСОК РАБОТ, ОПУБЛИКОВАННЫХ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Деменкова Т.А., Певцов Е.Ф., Стотланд И.А. Методика функциональной верификации цифровых устройств // Научно-технический журнал «Электронная техника». Серия 2. Полупроводниковые приборы. Выпуск 2(225). М.: ФГУП НПП «Пульсар», 2011. С. 16-23.

2. Стотланд И.А. Метод динамической верификации модулей системного обмена микропроцессорных вычислительных комплексов. // Научно-технический вестник Поволжья, 2012. №4. Казань: Научно-технический вестник Поволжья. С. 191-196.

3. Шмелев В.А., Стотланд И.А. Автономная верификация микропроцессоров на основе эталонных моделей разного уровня абстракции. // Проблемы разработки перспективных микро- и наноэлектронных систем -2012. Сборник трудов / под общ. ред. академика A.JI. Стемпковского. М.:ИППМ РАН, 2012. С. 48-53.

4. Деменкова Т.А., Стотланд И.А. Применение программных средств для моделирования и верификации СБИС. // Современные информационные

технологии в управлении и образовании. Сб. научн.тр. В 2-х ч. 4.2. М.: ФГУП НИИ «Восход», 2010. С. 23-30.

5. Стотланд И.А., Деменкова Т.А. Об одном подходе к разработке тестовых систем. // Теоретические вопросы вычислительной техники и программного обеспечения: Межвуз. сб. научн. тр. В 2-х т. Т.2. М.: МИРЭА, 2011. С. 102-109.

6. Стотланд И.А. Использование эталонных функциональных моделей для модульной верификации вычислительных систем // XVII Международная научно-практическая конференция студентов, аспирантов и молодых ученых «Современные техника и технологии». Сборник трудов в 3-х томах. Т.2. Томск: Изд-во Томского политехнического университета, 2011. С. 432-433.

7. Стотланд И. А. Методика модульной верификации микропроцессоров на основе высокоуровневых тестовых систем // Современные информационные технологии в управлении и образовании: Сб. научн. трудов. В 3-х ч. 4.2. М.: ООО «Издательство «Проспект», 2011. С. 120-126.

8. Стотланд И.А. Метод автоматизации функционального тестирования моделей аппаратуры // Фундаментальные проблемы радиоэлектронного приборостроения / Материалы международной научно-технической конференции «INTERMATIC-2011», 14-17 ноября 2011 г., Москва / Под. ред. чл.-корр. РАН A.C. Сигова. Ч. 4. М.: МГТУ МИРЭА - ИРЭ РАН, 2011. С. 83-86.

9. Стотланд И.А., Васильев А.Г. Подход к автоматизации формальной верификации модулей системного обмена микропроцессоров // Современные техника и технологии: сборник трудов XVIII Международной научно-практической конференции студентов, аспирантов и молодых ученых. В 3 т. Т. 2. Томск: Изд-во Томского политехнического университета, 2012. С. 407-408.

10. Стотланд И.А., Васильев А.Г., Оленин A.A. Реализация транслятора диаграмм состояний UML в формальную SMV-модель // Современные информационные технологии в управлении и образовании: Сб. научн. трудов. В 3-х ч. 4.2. М.: ООО «Издательство «Проспект», 2012. С. 82-88.

11. Стотланд И.А. Методика комплексной верификации модулей микропроцессорных систем // Современные информационные технологии в управлении и образовании: Сб. научн. трудов. В 3-х ч. 4.2. М.: ООО «Издательство «Проспект», 2012. С. 76-82.

Подписано в печать: 01.10.2012 Объем: 1,0 п.л. Тираж: 100 экз. Заказ № 670 Отпечатано в типографии «Реглет» 119526, г. Москва, пр-т Вернадского, д. 39 (495) 363-78-90; www.reglet.ru

ВВЕДЕНИЕ.

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

1.1. понятие фу! жционллы юй верификации и а11ализ проблем! 10й области.

1.2. Методы динамической верификации.

1.3. Методы формальной верификации.

1.3.1 Проверка эквивалентности.

1.3.2 Дедуктивны й анализ.

1.3.3 Проверка модели.

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

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

1.6. Обзор технологий построения тестовых систем.

1.6.1 Технология С++ТЕБК.

1.6.2 Универсальная технология верификации.

1.7. Анализ текущего состояния.

1.8. Введение понятия модулей системного обмена.

1.9. Постановка задачи.

ГЛАВА 2. РАЗРАБОТКА МЕТОДОВ И АЛГОРИТМОВ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА.

2.1. Разработка концептуальной модели модулей системного обмена.

2.2. разработка автоматной модели модулей системного обмена.

2.3. Разработка методов и алгоритмов динамической верификации модулей систем! юго обмена.

2.3.1 Метод генерации воздействий для динамической верификации модулей системного обмена.

2.3.2 Метод организации устройства проверки для динамической верификации модулей системного обмена. Алгоритм сравнения реакций верифицируемой ЯП-модели и эталонной модели.

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

2.4.1 Классификация требований к функционированию МСО.

2.4.2 Разработка семантической модели МСО.

2.4.3 Адаптация методов редукции числа состояний.

Выводы по главе.

ГЛАВА 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.2.1 Выбор и обоснование способа формализации спецификаций МСО.

3.2.2 Выбор и обоснование системы автоматизации метода проверки модели.

3.2.3 Разработка транслятора диаграмм состояний UML во входной язык верификатора SMV.

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

ГЛАВА 4. АПРОБАЦИЯ МЕТОДИКИ КОМПЛЕКСНОЙ ФУНКЦИОНАЛЬНОЙ ВЕРИФИКАЦИИ МОДУЛЕЙ СИСТЕМНОГО ОБМЕНА.

4.1. функциональная верификация хост-контроллера мвк «эльбрус-28».

4.1.1 Краткое описание хост-контроллера.

4.1.2 Анализ спецификации хост-контроллера.

4.1.3 Разработка и формальная верификация автоматной модели хост-контроллера на уровне базовых транзакций.

4.1.4 Динамическая верификация хост-контроллера.

4.1.5 Результаты комплексной функциональной верификации хост-контроллера.

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

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

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

Одним из основных методов обеспечения функциональной надежности МВК является их верификация на этапе логического проектирования. На каждом этапе маршрута проектирования применяются различные методы и средства верификации, призванные не пропустить неисправности на последующие стадии разработки. Стоимость исправления обнаруженных ошибок увеличивается в десятки и даже сотни раз при переходе от более ранних этапов маршрута проектирования к более поздним. Так, известная ошибка FDIV (ошибка в делении чисел с плавающей запятой) в микропроцессорах Intel Pentium, обнаруженная уже после выпуска 5 микросхемы в серийное производство, привела к замене микропроцессоров, что обошлось компании приблизительно в 475 миллионов долларов [48]. Исходя из вышесказанного, ошибки необходимо выявлять и исправлять еще на этапе логического проектирования системы.

Чтобы убедиться, что система удовлетворяет всем функциональным требованиям, сформулированным в спецификации, применяется функциональная верификация. Задача функциональной верификации — доказать, что разрабатываемое устройство будет работать согласно установленным требованиям (спецификации) [48]. Объектами функциональной верификации МВК являются логические модели уровня регистровых передач (ЯТЬ-модели), а таюке их системные модели и спецификации. Основными направлениями функциональной верификации являются динамическая верификация и формальная верификация. Как методы динамической, так и методы формальной верификации обладают своими преимуществами и недостатками. Автономное применение одного из направлений функциональной верификации грозит снижением уровня качества проверки, в то время как совместное применение независимых методик сопряжено с дополнительными затратами на формализацию спецификаций для разных подходов. Поэтому столь актуальной становится задача разработки методики комплексной верификации, основанной на использовании двух подходов с возможностью повторного использования разрабатываемых моделей и формализованных спецификаций.

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

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

Объектом исследования являются модули системного обмена, входящие в состав МВК, и процесс их функциональной верификации.

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

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

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

2. Классификация функциональных модулей, входящих в состав МВК, с точки зрения их функциональной верификации. Определение класса модулей системного обмена (МСО), разработка концептуальной модели МСО.

3. Разработка автоматной модели МСО МВК для формального представления МСО на разных уровнях абстракции.

4. Разработка методов, алгоритмов и программного обеспечения для динамической верификации МСО МВК на основе автоматной модели МСО.

5. Разработка и адаптация методов, алгоритмов и программного обеспечения формальной верификации МСО на основе автоматной модели МСО.

6. Разработка методики комплексной функциональной верификации МСО МВК, основанной на разработанных и адаптированных методах и алгоритмах динамической и формальной верификации МСО.

7. Апробация разработанной методики в промышленных проектах при модульной функциональной верификации современных МВК.

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

Работа состоит из введения, четырех глав, заключения и 8 приложений.

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

Во второй главе определена концептуальная трехуровневая модель МСО. Разработана автоматная модель МСО на основе теории расширенных конечных автоматов. На основе данных моделей определены формальные критерии принадлежности функционального модуля МВК к классу МСО. Приведено описание разработанных алгоритма сравнения реакций от верифицируемой ЯТЬ-модели и эталонной модели, методов генерации воздействий и организации устройства проверки для динамической верификации МСО. Разработана семантическая модель МСО для трансляции автоматной модели МСО в структуру Крипке для адаптации метода проверки модели для формальной верификации спецификаций МСО.

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

В четвертой главе представлено описание и результаты апробации методики при функциональной верификации микропроцессоров «Эльбрус-28» и «Эльбрус-4С+», разрабатываемых в ЗАО «МЦСТ». Основным результатом главы является практическое обоснование эффективности предложенной методики.

Выводы по главе

Результаты апробации методики комплексной функциональной верификации модулей системного обмена показывают ее применимость для сложных промышленным проектов. В главе подробно описан опыт практического применения методики при верификации хост-контроллера МВК «Эльбрус^», который показал эффективность применения методов генерации воздействий и организации устройства проверки, а также использования компонентов моделирующих комплексов в качестве эталонных моделей МСО. В результате, при комплексной функциональной верификации спецификации и реализации хост-контроллера было выявлено

59 ошибок. Около 7% ошибок было обнаружены при формальной верификации спецификации верифицируемых модулей. Данные ошибки крайне сложно обнаружить какими-либо другими способами, но они могут привести к неверному функционированию всего МВК. В процессе динамической верификации хост-контроллера разработаны 169 тестовых сценариев, включающих в себя 135 сценариев на проверку базовых операций хост-контроллера, 13 нагрузочных тестовых сценария и 21 динамический сценарий, имитирующий работу модуля в реальных условиях.

В главе также приведены результаты функциональной верификации других МСО, входящих в состав МВК «Эльбрус-28» и результаты разработки тестовой системы новой версии хост-контроллера МВК «Эльбрус-4С+». Трудозатраты на разработку тестовых систем существенно отличаются друг от друга, так как не во всех случаях была применена система автоматизации ШТЮ, позволяющая сократить до 75% трудозатрат. Кроме того, около 70% тестовых сценариев и эталонной модели может быть повторно использовано при изменении исходной спецификации и ЯТЬ-модели.

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

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

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

3. Предложен алгоритм сравнения последовательностей реакций от верифицируемой ЯТЬ-модели и эталонной модели, на основе которого разработан метод организации устройства проверки. Предложены механизмы дополнительных проверок и правила адаптации компонентов программных моделирующих комплексов МВК в качестве эталонных моделей, что позволяет существенно сократить сроки разработки и отладки эталонных моделей. Предложена технология «ВазеРоЛ» для организации взаимодействия тестовых систем и эталонных программных моделей.

4. Предложена архитектура и методика построения тестовых систем основе разработанных методов, механизмов, алгоритмов и универсальной технологии верификации ЦУМ. Разработано средство автоматизации построения шаблонов тестовых систем «иТЕв», позволяющее сократить трудозатраты на разработку тестовых систем.

5. Разработана семантическая модель МСО и программное обеспечение «иМЬ28МУ» для трансляции автоматной модели МСО в структуру Крипке для формальной верификации спецификаций МСО. Адаптирован метод проверки модели, разработанный Э. Кларком.

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

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

1. Агошкова Е. Б., Ахлибининский Б. В. Эволюция понятия системы // Вопросы философии, 1998. № 7. С. 170—179.

2. Белкин В.В., Шаршунов С.Г. Разработка функциональных тестов конвейеризованных процессоров на основе высокоуровневых моделей // Приборы и системы. Управление, контроль, диагностика, 2007. №4. С 22-27.

3. Белкин В.В. Построение функциональных диагностических тестов конвейеризированных RISC-процессоров : автореф. дис. . канд. тех. наук. Владивосток, 2008. 17с.

4. Верификация автоматных программ / Вельдер С. Э., Лукин М. А., Шалыто А. А, Яминов Б. Р.: СПбГУ ИТМО, 2011. 242 с.

5. ГОСТ Р ИСО 9000-2001. Государственный стандарт Российской Федерации. Система менеджмента качества. Основные положения и словарь. ИПК Издательство стандартов, 2001. С. 19.

6. Грушвицкий Р., Михайлов М. Проектирование в условиях временных ограничений: верификация проектов. Электронный ресурс. // Компоненты и технологии, 2008. №3. URL: http://www.kit-e.ru (дата обращения 05.09.2012).

7. Грушвицкий Р., Михайлов М. Проектирование в условиях временных ограничений: верификация проектов (продолжение). // Компоненты и технологии, 2008. №5. Электронный ресурс. URL: http://www.kit-e.ru (дата обращения 05.09.2012).

8. Гурин K.JI, Мешков А.Н., Сергин A.B., Якушева М.А. Развитие модели подсистемы памяти вычислительных комплексов серии «Эльбрус» // Вопросы радиоэлектроники, серия ЭВТ, Выпуск 3, 2010, С. 62-70.

9. Деменкова Т.А., Стотланд И.А. Методика проектирования логической модели цифрового устройства. 58 НТК МИРЭА. Информационные технологии и системы. Вычислительная техника. Сб. трудов. 4.1. М.: МИРЭА, 2009.С.32-38.

10. Деменкова Т.А., Певцов Е.Ф., Стотланд И.А. Методика функциональной верификации цифровых устройств // Научно-технический журнал «Электронная техника». Серия 2. Полупроводниковые приборы. Выпуск 2(225). -М.: «ФГУП НПП «Пульсар», 2011. С.16-23.

11. Камкин А., Чупилко М. Обзор современных технологий имитационной верификации аппаратуры. // Программирование, 20011. № 3. С. 42^49.

12. Камкин A.C. Использование контрактных спецификаций для автоматизации функционального тестирования моделей аппаратного обеспечения // Труды института системного программирования РАН, 2007. Т. 13. Ч. 1. С. 123-142.

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

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

15. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.

16. Кларк Э.М., ГрамбергО., ПеледД. Верификация моделей программ: Model Checking. Пер. с англ. / Под ред. Р. Смелянского. М.: МЦНМО, 2002.416 с.

17. Мешков А.Н. Реализация программного комплекса, моделирующего многопроцессорные ВК с архитектурой SPARC V9 // Вопросы радиоэлектроники, серия ЭВТ, 2009. Вып. 3. С. 79-89.

18. Петров И.А. Шерстнёв А.Е. Реализация справочника для аппаратной поддержки когерентности в вычислительном комплексе на базе микропроцессора «Эльбрус-28». -Вопросы радиоэлектроник. -2011. -Выпуск 3. С. 120-130.

19. Средство разработки тестовых систем C++TESK. Электронный ресурс. URL: http://hardware.ispras.ru/HHCTpyMeHTCPPTESK (дата обращения).

20. Стешенко В. Проектирование СБИС. Стили и этапы проекта Электронный ресурс. // Компоненты и технологии, 2003. № 4. URL: http://www.compitech.ru/ (дата обращения 05.09.2012).

21. Стотланд И.А. Метод динамической верификации модулей системного обмена микропроцессорных вычислительных комплексов. // Научно-технический вестник Поволжья, 2012. №4. Казань: Научно-технический вестник Поволжья. С.191-196.

22. Стотланд И.А. Методика комплексной верификации модулеймикропроцессорных систем.// Современные информационные технологии в управлении и образовании: Сб. научн. трудов. В 3-х ч.Ч.2 -М.: ООО «Издательство «Проспект», 2012. С.76-82.

23. Стотланд И.А. Этапы проектирования блока последовательного интерфейса в объеме ПЛИС, методы его диагностики и отладки. Современные информационные технологии в управлении и образовании. Сб. научн. тр.- М.: ФГУП НИИ «ВОСХОД», МИРЭА, 2009.С.118-126.

24. Стотланд И.А., Оленин A.A. Транслятор диаграмм состояний UML во входной язык верификатора SMV. Документ о регистрации программной системы в отраслевом фонде алгоритмов и программ РФ. Инвентарный номер ВНТИЦ 502001250300.

25. СтотландИ.А. Методика модульной верификации микропроцессоров на основе высокоуровневых тестовых систем // Современные информационные технологии в управлении и образовании: Сб. научн. трудов. 4.2. М.: ООО «Издательство «Проспект», 2011. С. 120-126.

26. Стотланд И.А., Деменкова Т.А. Об одном подходе к разработке тестовых систем. // Теоретические вопросы вычислительной техники и программного обеспечения: Межвуз. сб. научн. тр. В 2-х т. Т.2. М.: МИРЭА, 2011. С.102-109.

27. Сызько Э.В. Хост-контроллер ВК «Эльбрус-28». ЗАО «МЦСТ», 2011.

28. Таненбаум Э. Архитектура компьютеров. СПб.: Питер, 2007. 848 с.

29. Хопкрофт Д., Мотвани Р., Ульман Дж. Введение в теорию автоматов, языков и.вычислений. М.: Издательский дом "Вильяме", 2002. 528 с.

30. Чупилко М.М. Динамическая верификация цифровой аппаратуры на основе формальных спецификаций: автореф. дис. . канд. ф-м. наук. М., 2012. 24 с.

31. Чупилко М.М. Разработка тестовых систем для многомодульных моделей аппаратуры. // Программирование, 2012. № 1. С. 47-58.

32. A top-down methodology for validation of microprocessors / Mishra P., DuttN., Krishnamurthy N., AbadirM.S. // IEEE Design & Test, 2004. Vol. 21. No 2. P. 122-131.

33. Accellera. Электронный ресурс. URL: http://www.accellera.org/ (дата обращения 05.09.2012).

34. AVM tutorial. Электронный ресурс. URL: http://www.asicguru.com/methodologies/avm-tutorial (дата обращения 05.09.2012)

35. BaerJ.L. Microprocessor architecture. From simple pipelines to chip multiprocessors. NY: Cambridge University Press, 2010. 383p.

36. Barret G., Mclsaac A. Model Checking in a Microprocessor Design Project // Proc. of 9th International Conference on Computer Aided Verification, 1997. pp. 214-225.

37. Bentley R.M. Validating the Pentium 4 Microprocessor // Proc. of the Int. Conference on Dependable Systems and Networks, 2001. P. 493-498.

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

39. Bryant R.E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 1986. pp. 677-691.

40. Cai L., Gajski D. Transaction level modeling: an overview. // Proc. of CODES+ISSS 2003: The International Conference on Hardware-Software Codesign and System Synthesis, 2003. P. 19-24.

41. Chen J.S. Applying CRV to Microprocessor Verification. Электронный ресурс. URL: http://www.synopsys.com/services/pages/technicalpapers.aspx (дата обращения 05.09.2012)

42. Chupilko M., Kamkin A. Developing cycle-accurate contract specifications for synchronous parallel-pipeline hardware: application to verification // Proc. of ВЕС 2010: The 12th Biennial Baltic Electronics Conference, 2010. P. 185188.

43. Clarke E. M., Emerson E. A., Sistla A. P. Futomatic verification of finite-state146concurrent systems using temporal logic specifications: a practical approach // Proc. of 10th ACM Symp. On Principles of Programming Languages, 1983.

44. Clarke E., Grumberg O., Long O. Model checking and abstraction // ACM Transaction on Programming Languages and Systems, 1994. Vol. 16. No 5. P. 1512-1542.

45. Clarke E., Grumberg O., Peled D. Model checking. The MIT Press, 1999.

46. Clarke E.M., Heinle W. Modular Translation of Statecharts to SMV. // School of Computer Science. Carnegie Mellon University. Pittsburgh, PA 1513, August 3, 2000 -38p.

47. Drechsler R. Advanced formal verification. Kluwer Academic Publishers, 2004.

48. Formal verification of iterative algorithms in microprocessors / Aagaard M.D., Jones R.B., Kaivola R., Kohatsu K.R., Seger C.-J.H. // Proc. of Design Automation Conference, 2000. P. 201-206.

49. Foster H., Krolnic A., Lacey D. Assertion-Based Verification, 2nd ed. Boston: Kluwer Academic Publishers, 2003.

50. Functional Verification Semiconductor Reuse Standard V3.2. Freescale Semiconductor. 2005.

51. Ho R. Validation tools for complex digital designs. PhD thesis, Stanford University, 1996.

52. IEEE Standard for Property Specification Language (PSL). IEEE Std 13642001.1850-2010.

53. IEEE Standard for the Functional Verification Language 'e'. IEEE Std 16472006.

54. IEEE Standard System C Language Reference Manual. IEEE Std 1666-2005.

55. IEEE Standard SystemVerilog Unified Hardware Design, Specification and147

56. Verification Language. IEEE Std 1800-2009.

57. IEEE Standard Verilog Hardware Description Language. IEEE Std 13642001.

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

59. Intel® Core™ i7-900 Desktop Processor Extreme Edition Series and Intel® Core™ 17-900 Desktop Processor Series. Specification Update. May 2011. Электронный ресурс.

60. URL: ftp://download.intel.com/design/processor/specupdt/320836.pdf (дата обращения 05.09.2012)

61. Intel® Core™ 2 Duo Processor E8000 and E7000 Series. Specification Update. December 2010. Электронный ресурс. URL: ftp://download.intel.com/design/processor/specupdt/ 318733.pdf (дата обращения 05.09.2012)

62. Jiang Y, Qiu Z. S2N: Model Transformation from SPIN to NuSMV // Model Checking Software. Lecture Notes in Computer Science, 2012. Vol. 7385. P. 255-260.

63. Jonson N. A Method Is Not A Methodology. Электронный ресурс. URL: http://www.agilesoc.com/articles/a-method-is-not-a-methodology/ (дата обращения 05.09.2012).

64. Kaivola R., Narasimhan N. Formal verification of the Pentium4 floating-point multiplier // Proc. of Design, Automation and Test in Europe Conference, 2002. P. 20-27.

65. Kamkin A. Coverage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications // Proc. of EWDTS 2008: The 6th East-West Design & Test Symposium, 2008. P. 84-87.

66. Kamkin A. Coverage-Directed Verification of Microprocessor Units Based on Cycle-Accurate Contract Specifications // Proc. of EWDTS 2008: The 6th East-West Design & Test Symposium, 2008. P. 84-87.

67. Lam W. Hardware design verification: simulation and formal method-based approaches. New Jersey: Prentice Hall, 2005.

68. Lungu A., Sorin D.J. Verification-aware microprocessor design // Proc. of IEEE 16th International Conference on Parallel Architecture and Compilation Techniques, 2007. P.83-93.

69. Mishra P. A top-down methodology for validation of microprocessors // IEEE Design & Test, 2004. Vol. 21. No 2. P. 122-131.

70. Mishra P., DuttN. A methodology for validation of microprocessors using equivalence checking // Proc. of Microprocessor Test and Verification: Common Challenges and Solutions, 2003. P. 83-88.

71. Mishra P., DuttN. Functional validation of programmable architectures // Proc. of Digital System Design, 2004. P. 12-19.

72. Mishra P., Dutt, N. Automatic functional test program generation for pipelined processors using model checking // Proc. of High-Level Design Validation and Test Workshop, 2002. P. 99-103.

73. ModelSim® User's Manual. Software Version 6.10b, 2012. Электронный ресурс. URL: http://model.com/ (дата обращения).

74. Moore J.S, Lynch T.W., Kaufmann M. A mechanically checked proof of the AMD5K86™ floating-point division program // Computers, IEEE Transactions, 1998. Vol. 47. No 9. P. 913-926.

75. Namjoshi K.S., Kurshan R. P. Syntactic Program Transformations for Automatic Abstraction // Proc. of the 12th International Conference on Computer Aided Verification, 2000. P. 435-449.

76. NuSMV User Manual. Электронный ресурс. URL: http://nusmv.fbk.eu/NuSMV/userman/index-v2.html (дата обращения 05.09.2012).

77. NuSMV: a new symbolic model checker. Электронный ресурс. URL: http://nusmv.fbk.eu/ (дата обращения)

78. OMG Unified Modeling Language (OMG UML), Superstructure. Version 2.3. Электронный ресурс. Режим доступа: http://www.omg.org (дата обращения 05.09.2012)

79. Open Verification library. Электронный ресурс.149

80. URL: http://www.eda-stds.org/ovl/ (дата обращения 05.09.2012)

81. Peng Н. Improving compositional verification through environment synthesis and syntatic model reduction. PhD thesis. Concordia University, Monreal, 2002.

82. Piziali A. Functional Verification Coverage Measurement And Analysis. Kluwer Academic Publishers, 2004.

83. Pnueli A. The temporal logic of program // Proc. of the 18th Anny. Symp. On Foundation of Computer Science, 1977.

84. Price D. Pentium FDIV flaw-lessons learned // IEEE Micro, 1995. Vol. 15. No 2. P. 86.

85. R, Kurshan. Computer-aided verification of coordinating processes. NJ: Princeton Univerisity Press, 1994.

86. Reshadi, M., Mishra, P., Dutt N., Hybrid Compiled Simulation: An Efficient Tehnique for Instruction-Set Architecture Simulation . // ACM Transactions on Embedded Computer Systems, 2009. P. 8(3): 1-27.

87. Revision Guide for AMDAthlon™64 and AMD Opteron™ Processors. Электронный ресурс. URL: http://support.amd.com/us/Processor/ (дата обращения 05.09.2012)

88. Spear С. SystemVerilog for Verification. New York: Springer, 2006.

89. SPIN. Электронный ресурс. URL: http://spinroot.com/ (дата обращения)

90. The SMV System. Электронный ресурс. URL:http://www.cs.cmu.edu/~modelcheck/smv.html (дата обращения)

91. TLM-2.0.1. Электронный ресурс. URL: http://www.accellera.org/ (дата обращения 05.09.2012).

92. UVM/OVM Verification Methodology. Электронный ресурс. URL: http://verificationacademy.com/ (дата обращения 05.09.2012)

93. Van Langenhole S. Towards to correctness of Software Behavior in UML: A Model Checking Approach based on Slicing. PhD thesis. UGent, 2006.

94. Vasudevan S., ViswanathV., Abraham J.A. Efficient Microprocessor Verification using Antecedent Conditioned Slicing // Proc. of VLSI Design, 2007. P. 43-49

95. VCS®/VCSi™ User Guide. Version E-2011.03. March 2011 Электронный ресурс. URL: https://solvnet.synopsys.com (дата обращения 05.09.2012)

96. Verifying hardware in its software context / Kurshan R., Levin V., Minea M., Peled D., Yenigan H. // Proc. of IEEE/ACM international conference on Computer-aided design, 1997. P. 742-749.

97. VMM central. Электронный ресурс. URL: www.vmmcentral.org (дата обращения 05.09.2012 )

98. Wiemann A. Standardized functional verification. San Carlos: Springer Science, 2007.

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

100. Wolfe A. For Intel, it's a case of FPU all over again // Electronic Engineering Times, 1997. No 4. P. 43.

101. Пример генерации воздействий на уровне регистровых передачи уровне транзакций

102. ADDR WRITESTB DATAWR8:0. DATARD[8:0] DATASIZE[2:0] SELLINK[1:0]1. BIG ENDIANi1. TRANS

103. Уровень интерфейсных сигналов0)acOO