Содержание к диссертации
Введение
ГЛАВА 1. Обзор и анализ методов и средств функциональной верификации микропроцессорных вычислительных комплексов 9
1.1. Понятие функциональной верификации и анализ проблемной области 9
1.2. Методы динамической верификации 12
1.3. Методы формальной верификации
1.3.1 Проверка эквивалентности 19
1.3.2 Дедуктивный анализ 20
1.3.3 Проверка модели
1.4. Обзор методов, применяемых при функциональной верификации микропроцессорных вычислительных комплексов 23
1.5. Обзор методов спецификации моделей микропроцессорных вычислительных Комплексов 26
1.6. Обзор технологий построения тестовых систем 30
1.6.1 Технология C++TESK. 31
1.6.2 Универсальная технология верификации
1.7. Анализ текущего состояния 33
1.8. Введение понятия модулей системного обмена 36
1.9. Постановка задачи 39
Глава 2 . Разработка методов и алгоритмов функциональной верификации модулей системного обмена 41
2.1. Разработка концептуальной модели модулей системного обмена 41
2.2. Разработка автоматной модели модулей системного обмена 42
2.3. Разработка методов и алгоритмов динамической верификации модулей системного обмена
2.3.1 Метод генерации воздействий для динамической верификации модулей системного обмена 58
2.3.2 Метод организации устройства проверки для динамической верификации модулей системного обмена. Алгоритм сравнения реакций верифицируемой RTL-модели и эталонной модели 64
2.4. Разработка и адаптация методов и алгоритмов формальной верификации модулей системного обмена 75
2.4.1 Классификация требований к функционированию МСО 77
2.4.2 Разработка семантической модели МСО 78
2.4.3 Адаптация методов редукции числа состояний 81
выводы по главе 82
ГЛАВА 3. Разработка методики комплексной функциональной верификации модулей системного обмена микропроцессорных вычислительных комплексов 84
3.1. Разработка методики и программного обеспечения построения тестовых систем для динамической верификации модулей системного обмена 84
3.1.1 Разработка правил адаптации компонентов моделирующих комплексов для динамической верификации МСО 84
3.1.2 Применение дополнительных механизмов проверки 88
3.1.3 Разработка архитектуры тестовой системы 90
3.1.4 Выбор и обоснование технологии построения тестовых систем 92
3.1.5 Разработка методики построения тестовых систем 97
3.1.6 Разработка средств автоматизации методики построения тестовых систем... 106
3.1.7 Разработка подхода к оценке полноты покрытия 107
3.2. Разработка методики формальной верификации модулей системного обмена 108
3.2.1 Выбор и обоснование способа формализации спецификаций МСО 109
3.2.2 Выбор и обоснование системы автоматизации метода проверки модели ПО
3.2.3 Разработка транслятора диаграмм состояний UML во входной язык верификатора SMV 112
3.3. Разработка методики комплексной функциональной верификации модулей
Системного обмена 117
Выводы по главе 123
Глава 4. Апробация методики комплексной функциональной верификации Модулей системного обмена 125
4.1. Функциональная верификация хост-контроллера МВК «ЭЛЬБРУС-28» 125
4.1.1 Краткое описание хост-контроллера 125
4.1.2 Анализ спецификации хост-контроллера 128
4.1.3 Разработка и формальная верификация автоматной модели хост-контроллера на уровне базовых транзакций 130
4.1.4 Динамическая верификация хост-контроллера 133
4.1.5 Результаты комплексной функциональной верификации хост-контроллера 135
4.2. Результаты применения методики при функциональной верификации модулей системного обмена микропроцессорных вычислительных комплексов 137
Выводы по главе 138
Заключение 140
Список литературы
- Методы динамической верификации
- Обзор методов спецификации моделей микропроцессорных вычислительных Комплексов
- Выбор и обоснование технологии построения тестовых систем
- Разработка и формальная верификация автоматной модели хост-контроллера на уровне базовых транзакций
Введение к работе
Актуальность темы. Современное развитие микропроцессоров и вычислительных комплексов на их основе идет по направлению увеличения числа процессорных ядер в системе и расширения функциональных возможностей, что достигается как повышением уровня микроэлектронной технологии, используемой для производства микропроцессоров, так и применением новых архитектурных и структурных вариантов их реализации. Одним из основных методов обеспечения функциональной надежности микропроцессорных вычислительных комплексов (МВК) является их верификация на этапе разработки. Стоимость исправления ошибок увеличивается в десятки и даже сотни раз при переходе от более ранних этапов маршрута проектирования к более поздним. В связи с этим ошибки необходимо выявлять и исправлять еще на этапе логического проектирования. Для этого применяют функциональную верификацию, объектами которой являются логические модели микропроцессоров уровня регистровых передач (Register Transfer Level, RTL-модели), а также их системные модели и спецификации.
Выделяют два основных уровня функциональной верификации микропроцессоров и МВК: модульный и системный. Развитие модульной функциональной верификации существенно отстает от развития системной верификации, при этом модульная функциональная верификация позволяет обнаруживать и исправлять ошибки на самых ранних стадиях маршрута проектирования МВК. Функциональную верификацию, применяемую для проверки моделей микропроцессоров и МВК, также разделяют на два основных класса: динамическую верификацию, основанную на имитационном тестировании, и формальную верификацию, основанную на статическом анализе формальной модели системы.
Современное состояние области функциональной верификации МВК характеризуется независимым развитием каждого из направлений. Вопросам динамической верификации микропроцессоров и МВК посвящен ряд работ отечественных и зарубежных ученых: Камкина А.С., Чупилко М.М., Белкина В.В., Шаршунова С.Г., Мишра П., Дутта Н., Бергерона Д., Лама В. и других. Проблема формальной верификации программно-аппаратных систем (в том числе МВК) рассматривается в работах Коннова И.В., Карпова Ю.Г., Кларка Э., Харрисона Д., Намьёши К.С. и других. Однако на сегодняшний день отсутствуют методики комплексной функциональной верификации МВК. При этом автономное использование одного из направлений функциональной верификации грозит снижением уровня качества проверки. Большинство существующих работ по функциональной верификации микропроцессоров и МВК посвящено исследованию конвейеризированных модулей управляющей логики, в то время как далеко не все функциональные модули, входящие в состав МВК, имеют конвейеризированную архитектуру. Анализ официальных перечней
ошибок современных микропроцессоров, выпущенных в серийное производство, показал, что около 30% ошибок связаны с неверным функционированием систем поддержки когерентности и обмена данными, имеющих неконвейеризированную архитектуру. Таким образом, разработка методики комплексной функциональной верификации МВК, учитывающей функциональные и архитектурные особенности модулей, организующих системный обмен, является актуальной задачей.
Объектом исследования являются модули системного обмена, входящие в состав МВК, а также процесс их функциональной верификации.
Цель и задачи исследования. Целью диссертационной работы является разработка методики комплексной функциональной верификации модулей системного обмена МВК, обеспечивающей высокий уровень автоматизации разработки тестовых систем и тестов, сокращающей трудозатраты на модульную функциональную верификацию МВК и качественно улучшающей результаты функциональной верификации. Для достижения указанной цели в диссертационной работе поставлены и решены следующие основные задачи:
-
Анализ существующих методов и средств функциональной верификации МВК.
-
Классификация функциональных модулей, входящих в состав МВК, с точки зрения их функциональной верификации. Определение класса модулей системного обмена (МСО), разработка концептуальной модели МСО.
-
Разработка автоматной модели МСО для формального представления МСО на разных уровнях абстракции.
-
Разработка методов, алгоритмов и программного обеспечения для динамической верификации МСО на основе автоматной модели МСО.
-
Разработка и адаптация методов, алгоритмов и программного обеспечения для формальной верификации МСО на основе автоматной модели МСО.
-
Разработка методики комплексной функциональной верификации МСО МВК, основанной на разработанных и адаптированных методах и алгоритмах динамической и формальной верификации МСО.
-
Практическая апробация разработанной методики в промышленных проектах при модульной функциональной верификации современных МВК.
Методы исследования базируются на теоретических и методологических
основах теории множеств, теории графов и методах имитационного
моделирования вычислительных систем. Автоматная модель МСО определена на
основе теории расширенных конечных автоматов. При разработке методов и
средств динамической верификации МСО использовались методы
высокоуровневого моделирования, объектно-ориентированного
программирования, теории алгоритмов.
Научная новизна диссертационной работы заключается в следующем:
-
Впервые выделены и рассмотрены с точки зрения функциональной верификации модули системного обмена как обособленный класс функциональных модулей, входящих в состав современных МВК.
-
Разработаны концептуальная и автоматная модели МСО. Сформулированы критерии принадлежности функционального модуля МВК к классу модулей системного обмена.
-
Предложен новый метод генерации воздействий для динамической верификации МСО, основанный на автоматной модели МСО и позволяющий создавать ортогональные последовательности ограниченно-случайных воздействий на разных уровнях абстракции.
-
Разработан новый алгоритм сравнения последовательностей реакций верифицируемой RTL-модели и эталонной модели уровня базовых транзакций для динамической верификации МСО, учитывающий функциональные особенности соответствующего МСО. На основе данного алгоритма предложен метод организации устройства проверки, позволяющий автоматизировать процедуру проверки реакций и изолировать устройство проверки от генератора воздействий в тестовой системе.
-
Разработана семантическая модель МСО, позволяющая адаптировать формальный метод проверки модели путем трансляции полуформальной автоматной модели МСО в формальную модель, представляющую собой структуру Крипке.
-
Предложена методика комплексной функциональной верификации МСО МВК, базирующаяся на разработанных и адаптированных методах и алгоритмах динамической и формальной верификации МСО и отличающаяся от существующих применением комплексного анализа как спецификаций МСО, так и реализаций в виде RTL-моделей и эталонных программных моделей.
Практическая ценность работы и внедрение ее результатов. На основе предложенных методов динамической верификации модулей системного обмена и универсальной технологии верификации было разработано программное средство автоматизации методики построения тестовых систем, позволяющее более чем на 30% сократить трудозатраты на разработку тестовых систем для динамической верификации МСО.
Разработан транслятор диаграмм состояний UML во входной язык верификатора SMV, реализующий преобразование автоматной модели МСО в структуру Крипке в соответствии с предложенной семантической моделью МСО. Применение транслятора дает возможность полностью автоматизировать процесс формальной верификации спецификаций МСО, представленных в виде диаграмм состояний UML.
Разработанная методика комплексной функциональной верификации модулей системного обмена, а также средства ее автоматизации могут быть использованы при модульной верификации МВК как общего, так и специального
назначения для повышения эффективности функциональной верификации и сокращения сроков ее проведения.
Практическая ценность работы подтверждается эффективностью применения предложенной методики при функциональной верификации микропроцессора «Эльбрус-28», разрабатываемого в ЗАО «МЦСТ». Согласно акту о внедрении, использование разработанных методов динамической верификации МСО и методики комплексной функциональной верификации МСО позволило качественно улучшить верификацию спецификаций и логических моделей микропроцессоров и сократить трудоемкость разработки тестовых систем.
Научные положения диссертационной работы внедрены в учебный процесс на кафедре «Вычислительная техника» МГТУ МИРЭА при проведении лабораторных работ и подготовке лекционного материала по курсам «Проектирование цифровых устройств в САПР», «Моделирование», «Верификация проектов устройств и систем в САПР».
Результаты диссертации использованы в научно-исследовательской работе, выполненной Центром проектирования интегральных схем, устройств наноэлектроники и микросистем МГТУ МИРЭА по проекту №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 таблиц.
Методы динамической верификации
Методы динамической верификации основаны на имитационном моделировании RTL-модели системы, которое подразумевает подачу определенных входных воздействий на исполнимую модель, наблюдение результатов этих воздействий и принятие решения, верны ли результаты. Динамическая верификация осуществляется посредством наблюдения за процессом изменения состояний системы во времени [11].
Первоначально единственным способом проверки на корректность работы являлось интерактивное тестирование (direct testing), включающее в себя создание набора тестовых векторов для проверки всех интересующих ситуаций. Однако при повышении сложности верифицируемых моделей данный метод оказывается слишком медленным. Более того, во многих современных проектах «вручную» создать и перебрать все возможные сценарии оказывается просто невозможно. Верификация на основе тестовых систем является гораздо более сложным и гибким аппаратом для оценки корректности работы некоторого модуля или всего МВК в целом. Верификация на основе тестовых систем требует разработки дополнительного окружения [96]. На рис. 1.2 представлена общая схема динамической функциональной верификации RTL-моделей с использованием тестовых систем. Система моделирования (симулятор САПР)
Общая схема динамической верификации Классическая схема тестирования включает в себя непосредственно верифицируемую RTL-модель, тестовую систему и систему моделирования — систему автоматизированного проектирования (САПР), организующую имитационное моделирование тестовой системы и RTL-модели (среди них наибольшей популярностью пользуются системы VCS (продукт компании Synopsys) [103] и ModelSim (продукт компании Mentor Graphics) [82]). Тестовая система подает на верифицируемую RTL-модель входные воздействия и анализирует выходные реакции. В процессе верификации тестовой системой создается тестовый отчет, используемый для анализа обнаруженных ошибок и оценки полноты покрытия [12].
Тестовая система имитирует окружение, в котором будет в дальнейшем функционировать верифицируемое устройство. В общем случае тестовая система решает три основные задачи [17]: генерацию входных воздействий; проверку правильности выходных реакций; оценку полноты тестирования.
С учетом данных задач обычно детализируют тестовую систему на компоненты: генератор входных воздействий (stimulus generator), устройство проверки (checker), анализатор (scoreboard). На рис. 1.3 представлена архитектура типовой тестовой системы. Такую архитектуру предлагают в своих работах ряд зарубежных и отечественных специалистов в области верификации: Д. Бергерон [48], В. Лам [77], А.С. Камкин и М.С. Чупилко [14]-[17], группа специалистов компании IBM в монографии [А107].
Архитектура классической тестовой системы Генератор входных воздействий создает последовательность входных сигналов, которая может быть как псевдослучайной, так и направленной. Устройство проверки организует сравнение выходных реакций, полученных от верифицируемой RTL-модели, с ожидаемыми реакциями. Анализатор на основании полученной от устройства проверки информации о результатах проверки, а также набора входных воздействий и выходных реакций осуществляет управление тестовой системой, сбор покрытия и генерацию тестовых отчетов.
В зависимости от способа решения основных задач тестовой системы методы динамической верификации можно классифицировать следующим образом:
1. по способу генерации входных воздействий: направленное тестирование (directed testing); случайное тестирование (random testing) ограниченно-случайное тестирование (constrained-random testing);
2. по способу организации устройства проверки: самопроверяющие тестовые системы (self-checking testbench); тестовые системы на основе эталонных моделей (co-simulation);
3. по способу оценки полноты тестирования: тестирование на основе функционального покрытия (coverage-driven verification); тестирование на основе кодового покрытия (code coverage). Далее последовательно рассмотрены более подробно перечисленные подходы.
Направленное тестирование широко используется при проверке особых случаев (corner cases) в работе микропроцессоров или их функциональных модулей, когда достичь желаемого состояния системы другими методами сложно и это требует больших временных затрат. Направленное тестирование также полезно при модульной верификации функциональных блоков микропроцессоров для воспроизведения ошибок, обнаруженных при системной верификации или тестировании с использованием прототипа. Однако применение лишь направленного тестирования для верификации микропроцессора на любом уровне (системном или модульном) сопряжено с колоссальными трудозатратами, так как пространство состояний современных микропроцессоров велико, и вручную создать и перебрать все возможные сценарии оказывается очень сложно.
Случайное тестирование основано на автоматической генерации входных воздействий. Достоинствами случайной генерации является быстрота разработки генератора и возможность быстрого обнаружения простых ошибок (например, неподключенные интерфейсы), а также возможность создания особых ситуаций, неучтенных при направленном тестировании. Однако для полного тестирования современных микропроцессоров таким способом необходимы большие временные затраты, так как получить осмысленные входные воздействия с помощью случайного генератора достаточно сложно.
Ограниченно-случайное тестирование также использует генераторы случайных чисел, но случайными являются не все входные воздействия, а лишь часть параметров тестов. Тест представляет собой шаблон, в котором вместо конкретных значений определенных входных сигналов (типов операций, адресов и тд.) указывается набор ограничений, которым они должны удовлетворять. На основе механизма разрешения ограничений, генератор строит случайные значения параметров. Механизмы разрешения ограничений поддерживаются современными языками моделирования и верификации аппаратуры (SystemVerilog [66], "е" [64] и др.), а также системами моделирования (VCS [103], ModelSim [А82]).
Центральным вопросов при построении тестовых систем для динамической верификации микропроцессоров является способ проверки правильности результатов симуляции. Р. Хо в своей диссертации [62] выделяет два основных подхода: самопроверяющие тесты (self-checking) и сравнение с эталонной моделью (co-simulation).
Обзор методов спецификации моделей микропроцессорных вычислительных Комплексов
При функциональной верификации МВК на практике применяются методы формальной и динамической верификации, рассмотренные в разделах 1.2 - 1.3. Современное состояние области функциональной верификации моделей аппаратуры характеризуется автономных развитием каждого из направлений в сторону повышения автоматизации, масштабируемости, усложнения поддающихся проверке верифицируемых моделей, а также сокращения трудозатрат. Однако как методы динамической, так и методы формальной верификации обладают своими преимуществами и недостатками. Автономное применение одного из направлений функциональной верификации грозит снижением уровня качества проверки. Поэтому столь актуальной становится задача разработки методики комплексной верификации, основанной на использовании двух подходов с возможностью повторного использования разрабатываемых эталонных моделей и формализованных спецификаций.
В данной работе рассматривается модульный уровень верификации МВК, так как на этом уровне верификация может проводиться уже на самых ранних стадиях проектирования, что значительно ускоряет процесс верификации непосредственно и разработки всей системы в целом. Кроме того, как показано в разделе 1.7, развитие модульной функциональной верификации существенно отстает от развития системной верификации.
В качестве объекта функциональной верификации был выбран класс модулей системного обмена. Вопросу функциональной верификации устройств с конвейерной архитектурой посвящен ряд работ отечественных и зарубежных исследователей [2, 3, 17, 52, 79]. МСО впервые выделены в отдельный самостоятельный класс функциональных модулей, входящих в состав МВК, поэтому не существует ни одной методики функциональной верификации, специфицированной для проверки функциональных модулей, обладающих свойствами модулей системного обмена, в то время как критичность ошибок в модулях, организующих взаимодействие в микропроцессорных системах, велика.
Таким образом, целью работы является разработка методики комплексной модульной верификации модулей системного обмена МВК, обеспечивающей высокий уровень автоматизации разработки тестовых систем и тестов и качественно улучшающей результаты функциональной верификации, а также учитывающей специфику модулей системного обмена. Для достижения цели работы основные задачи были уточнены: 1. Разработка автоматной модели МСО МВК для формального представления МСО на разных уровнях абстракции. 2. Разработка метода генерации воздействий для динамической верификации МСО на основе автоматной модели МСО. 3. Разработка алгоритма сравнения последовательностей реакций от верифицируемой RTL-модели и эталонной модели уровня базовых транзакций и метода организации устройства проверки, реализующего данный алгоритм, для динамической верификации МСО. 4. Разработка семантической модели МСО и на ее основе транслятора автоматной модели МСО в структуру Крипке для адаптации метода проверки модели для формальной верификации МСО. 5. Разработка методики и средств автоматизации динамической верификации МСО, основанных на методах генерации воздействий и построения устройства проверки. 6. Разработка методики и средств автоматизации формальной верификации МСО, основанной на трансляции автоматной модели МСО в структуру Крипке и методе проверки модели. 7. Разработка методики комплексной функциональной верификации МСО, базирующейся на разработанных и адаптированных методах, алгоритмах и методиках динамической и формальной верификации МСО. 8. Апробация разработанной методики в промышленных проектах. Глава 2. Разработка методов и алгоритмов функциональной верификации модулей системного обмена 2.1. Разработка концептуальной модели модулей системного обмена При проектировании МСО определяется ряд функций, которые должен выполнять модуль. Такие функции можно разделить на базовые (core), заключающиеся в организации взаимодействия окружения МСО (обмен данными и управляющей информацией) и дополнительные (minor), заключающиеся в поддержке адекватного функционирования МСО (отвечающие за сигналы занятости, сброса, конфигурацию МСО). К базовым функциям МСО, как правило, относятся операции записи (store), чтения (load), установки прерываний (interrupts), передачи запросов (request). Окружением МСО (environment) называются логические модули МВК, взаимодействующие с МСО и не входящие в состав МСО.
Концептуальная модель МСО имеет трехуровневую структуру (рис. 2.1): первый (нижний) уровень представления — уровень интерфейсных сигналов (инициирующих, реагирующих и управляющих); второй — уровень базовых и дополнительных транзакций, образующих домен транзакций МСО; третий (верхний) — уровень базовых и дополнительных операций МСО, образующих домен операций МСО. Первый уровень представлен множеством Z — значений интерфейсных сигналом МСО; второй уровень — множеством {Т} — значений базовых транзакций МСО; третий уровень — множеством {Р} — значений базовый операций МСО. Рис. 2.1. Концептуальная модель МСО
Далее в разделе приведены основные понятия теории расширенных автоматов, на основе которых определена автоматная модель МСО. Расширенные автоматы широко используются для моделирования и верификации коммуникационных протоколов, программных и аппаратных систем, а также дают возможность минимизировать количество состояний формальной модели для решения проблемы «комбинаторного взрыва» в пространстве состояний.
Выбор и обоснование технологии построения тестовых систем
Для решения задачи разработки методики построения тестовых систем для динамической верификации МСО, удовлетворяющей требованиям, сформулированным в разделе 1.7, выделим основные подзадачи: 1. Разработка правил адаптации эталонных программных моделей, являющихся компонентами моделирующих комплексов МВК, и механизмов проверки функциональности МСО, не реализованной в эталонной модели; 2. Разработка и адаптация механизмов проверки темпоральных ограничений выполнения операция для МСО с операциями ограниченной длительности. 3. Разработка архитектуры тестовой системы, поддерживающей разработанные методы генерации воздействий и организации устройства проверки (раздел 2.2) и подходы из пунктов 1-2. 4. Выбор и обоснование технологии построения тестовой системы. 5. Разработка методики построения тестовой системы на основе предложенной архитектуры по выбранной технологии. 6. Разработка программного обеспечения для автоматизации построения тестовых систем. 7. Выбор и обоснование методов оценки полноты покрытия. Далее в разделе более подробно рассмотрены предлагаемые пути решения перечисленных задач.
В качестве эталонных моделей МСО предлагается использовать программные модели, реализованные на языке C++. Существуют также другие решения: поведенческие модели уровня базовых транзакций на языках описания аппаратуры (ЯОА), таких как SystemVerilog [66] и "е" [64]; модели, построенные в соответствие с концепцией TLM-2.0 на языке SystemC [65]. Однако программные модели на языке C++ обладают рядом преимуществ: простотой разработки, широким распространением языка C++, удобством компиляции и отладки, быстродействием, возможностью повторного использования при разработке моделирующих комплексов. Разработка эталонной модели уровня транзакций МСО является достаточно трудоемкой задачей (Приложение 2), поэтому для минимизации трудозатрат на динамическую верификацию МСО перспективным является применение уже готовых функциональных модулей, входящих в состав моделирующих комплексов разрабатываемых МВК. Как отмечают авторы работ [8, 20, 94], моделирующие комплексы, как правило, являются функциональными моделями без учета времени, описанными на языке C++. На функциональном уровне компоненты моделирующих комплексов МВК моделируются как классы с реализованными в них функциями обработки запросов различных типов на уровне транзакций. Выделим два основных подхода к интенсификации процессов разработки моделирующих комплексов и автономной верификации модулей МВК: с одной стороны — это адаптация и внедрение в моделирующий комплекс эталонных моделей, разработанных при динамической верификации микропроцессоров предыдущих поколений (так как ряд функциональных блоков используется повторно при построении микропроцессоров одной архитектуры, но различных версий) или в случае, когда автономная верификации модуля была проведена до начала разработки моделирующего комплекса; с другой — адаптация и использование компонентов моделирующего комплекса разрабатываемого микропроцессора для автономной динамической верификации (разработка моделирующего комплекса, как правило, происходит на более ранних стадиях маршрута проектирования, чем разработка RTL-модели или одновременно с RTL-моделыо).
Первый вариант касается вопросов построения моделирующих комплексов и повторного использования эталонных моделей, созданных для динамической верификации МВК, что выходит за рамки данной работы. Рассмотрим второй вариант, нацеленный на интенсификацию динамической верификации МВК. Модели МСО, входящие в состав моделирующих комплексов, будем называть МСО-компонентами моделирующих комплексов или кратко МСО-компонентами. Пусть Func — множество функций, организующих интерфейс МСО-компонента. Аналогично базовым транзакциям МСО множество всех функций МСО-компонента можно разделить на инициирующие и реагирующие: Func-\Funcinit;Funcг). Множество Func может быть эквивалентно множеству Trans базовых транзакций МСО, но далеко не всегда это условие выполняется. Определим, что функция МСО-компонента эквивалентна базовой транзакции МСО, если при ее вызове с любыми значениями параметров МСО-компонент реализует базовую транзакцию МСО, т.е. значения параметров реагирующих функций МСО-компонента будут соответствовать значениям атрибутов реагирующих транзакций МСО. Ниже приведены разработанные правила адаптации МСО-компонента для его использования в качестве эталонной модели.
Правило 1. Если мощности Func и Trans равны, и каждой базовой транзакции МСО можно сопоставить эквивалентную функцию МСО-компонента, т.е. \Func\ = 7hms = т и V/ = \,т 3/ є {і,/л}: t, « / , /, є Trans, f є Func, то такой МСО-компонент является эталонной моделью МСО уровня базовых транзакций и может быть применен для динамической верификации RTL-модели МСО без дополнительных адаптации.
Правило 2. МСО-компонент является более детальной моделью МСО, чем модель уровня базовых транзакций, если мощность Func больше мощности Trans, и для каждой базовой транзакции МСО существует последовательность вызовов функций МСО-компонента, эквивалентная базовой транзакции МСО:
Разработка и формальная верификация автоматной модели хост-контроллера на уровне базовых транзакций
Следуя разработанной методике комплексной функциональной верификации МСО, после формальной верификации спецификации МСО была проведена динамическая верификация RTL-модели хост-контроллера. В первую очередь был разработан тестовый план, описывающий набор необходимых тестовых сценариев.
Структура тестовой системы представлена на рис. 4.2. Тестовая система построена в соответствии с методикой, представленной в разделе 3.1 и включает в себя следующие компоненты: генератор операций и транзакций (два верхних уровня генератора воздействий host_ctrl_nvm_virtual_sequencer), сериализаторы транзакций (нижний уровень генератора воздействий - host_ctrl_ transaction_name _nvm_agenst), устройство проверки {host_ctrl_avm scoreboard), десериализаторы транзакций (host_ctrl_ transaction_name _nvm_monito? ). Все компоненты тестовой системы построены в соответствии с методикой построения тестовых систем, представленной в разделе 3.1.
В качестве эталонной модели хост-контроллера использована разработанная программная модель с интегрированными в нее компонентами моделирующего комплекса: контролером битовой шкалы и IOMMU. Такая интеграция позволила существенно сократить время разработки и отладки эталонной модели (табл. 4.3).
Функциональных блок Исходный код, строки кода Трудозатраты наразработку/адаптацию,чел.-недели Числообнаруженныхошибок Хост-контроллера безконтроллеров IOMMU ибитовой шкалы 4998 24 73 Контроллер битовой шкалы 1879 4 10 Контроллер IOMMU 2053 3 12
Программная модель является полной эталонной моделью хост-контроллера, поэтому в тестовой системе нет дополнительных механизмов проверки, описанных в разделе 3.1. После разработки тестовой системы и эталонной модели в соответствии с методикой комплексной функциональной верификации МСО (шаги 8, 9) был описан набор тестовых сценариев, состоящий из множества направленных тестов (135 тестовых сценариев), проверяющих исполнение отдельных базовых операций, нагрузочных тестов (13 тестовых сценариев) и случайных динамических тестов (21 тестовый сценарий). В приложении 5 представлено описание разработанных тестовых сценариев.
При верификации хост-контроллера был обнаружен ряд ошибок в RTL-модели и спецификации, связанных с преобразованием форматов данных, обработкой очередей запросов, упорядоченностью данных (приложение 5). Так как для динамической верификации хост-контроллера отдельно создавалась программная эталонная модель и в нее также были интегрированы модели контроллеров битовой шкалы и IOMMU как компоненты моделирующего комплекса, ряд ошибок было обнаружено в реализации эталонной модели (табл. 4.4).
Таким образом, основная доля ошибок приходится на реализацию спецификации хост-контроллера: программную и RTL-модель. Большое число ошибок в реализации программной модели обусловлено тем, что модель создавалась «с нуля», а не использовался готовый МСО-компонент.
Разработанная и отлаженная программная модель в дальнейшем пригодна для применения в моделирующем комплексе.
Ошибки, обнаруженные в спецификации, программной модели, RTL-модели при функциональной верификации хост-контроллера Вид ошибки Доля от общего числаобнаруженныхошибок, % Неточности спецификации (опечатки, неописанные фрагменты) 3,8 Формальные ошибки в спецификации(несоответствия формальным требованиямживости, безопасности, справедливости) 7,1 Ошибки в реализации RTL-модели 27,0 Ошибки в реализации программной модели 47,8 Ошибки в МСО-компоненте - контроллере битовой шкалы 7,0 Ошибки в МСО-компоненте - контроллереюмми 7,3
Для анализа результатов верификации применялся предложенный в методике подход по оценке покрытия. Так как для динамической верификации использовалась полная эталонная программная модель хост-контроллера, то для оценки полноты покрытия использовались метрики покрытия кода RTL-модели и покрытия кода эталонной модели (табл. 4.5). Значения покрытия по некоторым метрикам, не равные 100%, обусловлены использованием неэквивалентных каналов запросов по спецификации хост-контроллера, в то время как при реализации RTL-модели таких каналов используются одинаковые функциональные блоки. Кроме того, в эталонной модели реализованы дополнительные механизмы проверки входных данных, которые могут быть задействованы только при использовании модели в составе моделирующего комплекса.
Представленная в разделе 3.3 методика комплексной верификации функциональной МСО также была применена при верификации модуля доступа к оперативной памяти и контроллера межпроцессорных каналов МВК «Эльбрус-28». Кроме того, методика построения тестовых систем, описанная в разделе 3.1, использовалась для разработки тестовой системы верифицируемого хост-контроллера 2.0 разрабатываемого в ЗАО «МЦСТ» микропроцессорного комплекса «Эльбурс-4С+». По результатам апробации (табл. 4.6), представленным в сводной таблице, можно сделать вывод об эффективности применения системы автоматизации построения шаблонов тестовых систем «UTEG» и компонентов моделирующих комплексов в качестве эталонных моделей. Кроме того, при верификации хост-контроллера 2.0 была применена эталонная модель хост-контроллера 1.0 (хотя данные модули имеют существенные различия в архитектуре и интерфейсах), что доказывает возможность эффективного повторного использования компонентов тестовых систем и эталонных моделей, построенных по разработанной методике.
Результаты апробации методики комплексной функциональной верификации модулей системного обмена показывают ее применимость для сложных промышленным проектов. В главе подробно описан опыт практического применения методики при верификации хост-контроллера МВК «Эльбрус-28», который показал эффективность применения методов генерации воздействий и организации устройства проверки, а также использования компонентов моделирующих комплексов в качестве эталонных моделей МСО. В результате, при комплексной функциональной верификации спецификации и реализации хост-контроллера было выявлено ошибок. Около 7% ошибок было обнаружены при формальной верификации спецификации верифицируемых модулей. Данные ошибки крайне сложно обнаружить какими-либо другими способами, но они могут привести к неверному функционированию всего МВК. В процессе динамической верификации хост-контроллера разработаны 169 тестовых сценариев, включающих в себя 135 сценариев на проверку базовых операций хост-контроллера, 13 нагрузочных тестовых сценария и 21 динамический сценарий, имитирующий работу модуля в реальных условиях.
В главе также приведены результаты функциональной верификации других МСО, входящих в состав МВК «Эльбрус-28» и результаты разработки тестовой системы новой версии хост-контроллера МВК «Эльбрус-4С+». Трудозатраты на разработку тестовых систем существенно отличаются друг от друга, так как не во всех случаях была применена система автоматизации UTEG, позволяющая сократить до 75% трудозатрат. Кроме того, около 70% тестовых сценариев и эталонной модели может быть повторно использовано при изменении исходной спецификации и RTL-модели.
