Разработка методики и алгоритмов верификации гетерогенных многоядерных систем на основе графовой модели иерархии когерентной кэш-памяти тема диссертации и автореферата по ВАК РФ 05.13.01, кандидат наук Гаращенко Антон Витальевич

• Гаращенко Антон Витальевич
• кандидат наук
• 2021

Оглавление диссертации кандидат наук Гаращенко Антон Витальевич

ВВЕДЕНИЕ

ГЛАВА 1. АНАЛИЗ СОВРЕМЕННОГО СОСТОЯНИЯ МЕТОДОВ И СРЕДСТВ ВЕРИФИКАЦИИ ГЕТЕРОГЕННЫХ МНОГОЯДЕРНЫХ СИСТЕМ (ГМС)

1.1 Маршрут верификации современных СБИС типа гетерогенных систем на кристалле (СнК)

1.2 Аналитический обзор существующих методов верификации ГМС

1.2.1 Классические методы функциональной верификации

1.2.2 Методы верификации на основе математических моделей

1.2.3 Методы верификации на основе псевдослучайного дополнения шаблонов

1.2.4 Классические методы формальной верификации

1.3 Сравнительный анализ средств формирования верификационных последовательностей для ГМС

1.4 Постановка задач диссертации

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

ГЛАВА 2. ФОРМАЛИЗАЦИЯ ЗАДАЧИ ВЕРИФИКАЦИИ ГМС С ПРИМЕНЕНИЕМ АППАРАТА ТЕОРИИ МНОЖЕСТВ

2.1 Задача верификации ГМС

2.2 Формальное представление задачи верификации ГМС

2.3 Разработка графовой модели иерархии когерентной кэш-памяти ГМС

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

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

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

2.4. Разработка методов формирования верификационных последовательностей для сокращения времени моделирования ЯТЬ-описаний ГМС

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

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

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

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

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

3.2. Разработка генетического алгоритма формирования верификационных последовательностей на основе клеточного автомата для оценки переключательной активности RTL-описания ГМС

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

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

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

ГЛАВА 4. ПРОГРАММНАЯ РЕАЛИЗАЦИЯ РАЗРАБОТАННЫХ РЕШЕНИЙ В ВИДЕ КОМПЛЕКСА ПРОГРАММНЫХ СРЕДСТВ ДЛЯ ВЕРИФИКАЦИИ ГМС

4.1. Разработка структурной схемы КПС для верификации ГМС

4.2. Разработка архитектуры КПС для верификации ГМС на основе предложенной методики формирования верификационных последовательностей

4.3. Программная реализации КПС

4.4. Экспериментальные исследования достоверности предложенных решений (на примере верификации платформы «МУЛЬТИКОР»)

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

ЗАКЛЮЧЕНИЕ

СПИСОК ЛИТЕРАТУРЫ

ПРИЛОЖЕНИЕ

ПРИЛОЖЕНИЕ

ПРИЛОЖЕНИЕ

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

ВВЕДЕНИЕ

Актуальность исследования. Согласно исследованиям ЦНИИ «Электроника», входящего в ГК «Ростех», объём затрат на разработку микроэлектроники в РФ в 2019 году составил 131,3 млрд. рублей, при этом более 70% ресурсов проектирования тратится на верификацию интегральных схем. Это обусловлено высокой комбинаторной сложностью проверки корректности работы как отдельных блоков и вычислительных ядер, так и системы в целом, поэтому этап функциональной верификации становится одним из важнейших и проблемных этапов проектирования.

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

Для функциональной верификации ГМС на этапе RTL-описания необходимо создание верификационных последовательностей из ISA (Instruction set architecture), обеспечивающих полный перебор состояний всех блоков системы. Формирование верификационной последовательности относится к классу задач, сложность которых растет экспоненциально с ростом числа входных данных; однако ее можно свести к задаче дискретной оптимизации. И здесь уже целесообразно использовать эвристические и стохастические подходы.

Вопросы исследования функциональной верификации ГМС широко рассмотрены в ряде научных работ зарубежных авторов (Russinoff D., Eric Smith, Joshy A.M., Strube A.O., Harry Foster, Lionel Bening, John L.K., Xing Hu, William K., Chris S., Clifford E., B. Greene), а также российских ученых (П.П. Пархоменко, В.В, Липаев, Рутковский В. Ю., Юрченко В. Е., Согомонян Е. С., Ф.М. Путря, А.В. Николаев, А.Д. Иванников, А.С. Камкин, В.С. Буренков, В.В. Кулямин, А.К. Петренко и других). От качества и эффективности верификационных последовательностей зависят технические и экономические характеристики верификационного процесса, а значит, и процесса проектирования ГМС в целом.

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

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

Цель диссертационной работы - повышение эффективности процесса верификации ГМС на основе графовой модели когерентной иерархии кэшпамяти за счет разработки методики и алгоритмов увеличения полноты тестового покрытия кода RTL-описания.

Для достижения указанной цели в диссертации решаются следующие задачи:

1) исследование и анализ современных методов и средств верификации

ГМС;

2) формализация задачи верификации ГМС с применением аппарата теории множеств;

3) разработка теоретически обоснованной графовой модели иерархии когерентной кэш-памяти;

4) разработка алгоритмов и методики формирования верификационных последовательностей на основе графовой модели для системного тестирования ГМС;

5) разработка алгоритма оценки энергопотребления RTL-описания

ГМС;

6) программная реализация в виде комплекса программных средств формирования верификационных последовательностей (КПС ВТП) и оценка эффективности предложенных решений.

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

Научная новизна работы состоит в создании совокупности научно обоснованных технических решений, направленных на повышение эффективности процесса верификации ГМС на основе модели когерентной иерархии кэш-памяти за счет разработки методики и алгоритмов увеличения полноты тестового покрытия кода RTL-описания ГМС.

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

1) предложено формализованное представление задачи верификации ГМС с применением аппарата теории множеств, основанная на использовании введенной функции переключательной активности, которая ставит в соответствие каждому элементу из множества всех возможных пакетов инструкций количество сигналов, переключившихся с 0 на 1 или с 1 на 0;

2) разработана графовая модель иерархии когерентной кэш-памяти ГМС на основе алгоритмов построения и решения недетерминированных ситуаций, в том числе:

• узлы, характеризующие состояния кэш-памяти;

• дуги, описывающие связи между состояниями;

3) предложена методика формирования верификационных последовательностей для системного тестирования ГМС на основе графовой модели иерархии когерентной кэш-памяти и алгоритма проверки устройства управления процессорных ядер системы;

4) разработан генетический алгоритм формировании верификационных последовательностей на основе клеточного автомата для оценки переключательной активности RTL-описания ГМС.

Научная ценность полученных в работе результатом подтверждена полученным свидетельством о государственной регистрации программ для ЭВМ №2020666089 "Программа CFSGen формирования верификационных последовательностей для гетерогенных многоядерных структур", зарегистрированном в РОСПАТЕНТ 04.12.2020.

Достоверность полученных результатов. Достоверность разработанных в рамках исследования моделей, алгоритмов и методики подтверждена оценочными критериями, теоретическими расчетами, а также экспериментальными результатами, полученными при использовании КПС ВТП в процессе верификации ГМС (на примере VLIW DSP процессора с архитектурой «ELC0RE50» и системы на кристалле «МУЛЬТИКОР»).

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

Разработанный КПС ВТП, применяемый в маршруте проектирования гетерогенных систем на кристалле и вычислительных DSP-ядер на предприятии АО НПЦ «ЭЛВИС», что подтверждено актом о внедрении, позволил:

1) выявить 16 критичных ошибок иерархии кэш-памяти разрабатываемого VLIW DSP ядра с архитектурой ELC0RE50 (АО НПЦ «ЭЛВИС»);

2) выявить 12 критичных ошибок в DSP ядрах системы на кристалле «МУЛЬТИКОР» (АО НПЦ «ЭЛВИС»);

3) на 10% сократить время, требуемое на верификацию автономных окружений кэш-памятей и процессорных ядер;

4) достичь 97% переключательной активности всех сигналов RTL-описания DSP ядра;

5) достичь 95% тестового покрытия кода RTL-описания DSP ядра.

Личный вклад автора. Все результаты, изложенные в диссертации и

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

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

В результате проведенных исследований получены и выносятся на защиту следующие положения:

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

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

3. Методика формирования верификационных последовательностей для ГМС на основе графовой модели иерархии когерентной кэш-памяти, которая позволяет сократить время верификации автономных окружений кэш-памятей и процессорных ядер на 10%.

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

5. Программная реализация предложенных решений в виде КПС ВТП, внедрение которого в маршрут проектирования ГМС привело к достижению 97% переключательной активности всех сигналов и 95% тестового покрытия кода RTL-описания DSP ядра.

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

1. EIConRus-2020 Conference of Russian Young Researchers in Electrical and Electronic, г. Москва. 2020.

2. 26-я Всероссийская межвузовская научно-техническая конференция студентов и аспирантов «Микроэлектроника и информатика - 2019», г. Москва. 2019.

3. 12-я Всероссийская научно-практическая конференция «Актуальные проблемы информатизации в науке и образовании», г. Москва. 2019.

4. IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering, г. Москва. 2019.

5. Всероссийская научно-техническая конференция «Проблемы разработки перспективных микро- и наноэлектронных систем 2018», г. Москва. 2018.

6. Международная научно-практическая конференция «Актуальные проблемы науковедения, культуры, образования, экономики, информатики и

социальные трансформации», г. Москва, 2017.

9

Публикации. Основное содержание диссертации отражено в 11 работах, в том числе 2 статьи в журналах, входящих в перечень, утвержденный ВАК по специальности 05.13.01, 3 - Scopus; 6 - материалы докладов на всероссийских и международных конференциях.

Структура и объем работы. Диссертация состоит из введения, 4 глав, заключения, списка использованной литературы и приложений, содержащих листинги программ и акты о внедрении результатов работы. Общий объем диссертационной работы - 135 страниц текста, в том числе 6 таблиц и 37 рисунков.

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

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

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

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

В четвертой главе рассмотрены вопросы программной реализации разработанных решений в виде КПС ВТП и подтверждения достоверности

полученных результатов на основе проведенных экспериментов.

10

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

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

ГЛАВА 1. АНАЛИЗ СОВРЕМЕННОГО СОСТОЯНИЯ МЕТОДОВ И СРЕДСТВ ВЕРИФИКАЦИИ ГЕТЕРОГЕННЫХ МНОГОЯДЕРНЫХ

СИСТЕМ (ГМС)

Увеличение производительности вычислительных систем за счет наращивания гетерогенности является одной из важнейших тенденций развития отрасли. Это связано, прежде всего, с известными преимуществами применения разных типов процессоров для выполнения отдельных классов задач. Уменьшение размера полупроводниковых элементов и повышение степени их интеграции позволили создать новые виды СБИС, таких как сети и системы на кристалле. ГМС состоят из ядер общего назначения и специализированных вычислительных ядер с разной архитектурой. Для аппаратной реализации современных систем машинного обучения и искусственного интеллекта необходимы ГМС, содержащие десятки или даже сотни гетерогенных процессорных ядер с быстрым когерентным доступом в память [1].

В первых ГМС выделены отдельные регионы памяти для CPU и GPU, которые в случае ПК могут быть выполнены полностью на разных дискретных микросхемах. В таких системах для обмена данными между CPU и GPU необходимо постоянное копирование из памяти CPU в графическую память со значительными затратами на задержку и энергопотребление. Для обеспечения согласованности данных необходима программная реализация протоколов когерентности за счет отключения и инвалидации кэш-памяти процессоров [2]. В ГМС следующего поколения разработана аппаратная поддержка односторонней когерентности данных (AMBA 4 ACE-Lite) на сигнальном уровне. В системах такого типа GPU ядра способны напрямую читать кэшпамять CPU, обратная операция невозможна (например, ARM Mali-T600). Современные ГМС реализуют полную когерентность памяти между всеми гетерогенными ядрами (например, когерентность между Cortex-A72 и Mali-G71 GPU за счет общей шины CoreLink CCI-550).

1.1 Маршрут верификации современных СБИС типа гетерогенных систем на кристалле (СнК)

Важным и самым длительным этапом разработки СБИС является отладка моделей уровня регистровых передач (RTL) СФ-блоков. Проектирование - это многоэтапный итерационный процесс (рис. 1.1). В связи с архитектурной сложностью RTL-моделей современных многоядерных процессоров [3], применяемых при разработке ГМС, более семидесяти процентов ресурсов проектирования тратится на их верификацию [4]. Это обусловлено высокой комбинаторной сложностью проверки корректности работы как отдельных ядер, так и системы в целом, поэтому функциональная верификация становится одним из важнейших этапов проектирования ГМС.

Производство Рис. 1.1. Маршрут проектирования современных ГМС

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

ГМС. Для этого на этапе верификации RTL-моделей необходимо проверить: правильность подключения как всех СФ-блоков в составе подсистем, так и подсистем в составе ИС; корректность конфигурации всех параметризированных и генерируемых СФ-блоков (третьих сторон и собственных); отсутствие ошибок и клинчей в архитектуре и реализации блоков и протоколов их взаимодействия.

На ранних этапах проектирования возможен визуальный контроль кода при условии вовлечения в процесс анализа сторонних разработчиков, метод становится достаточно эффективным для верификации небольших объёмов кода. На следующем шаге применяется синтаксический и семантический анализ кода — автоматизированная проверка на соответствие правилам синтаксиса языка описания аппаратуры, дополняемая формальной проверкой корректности RTL-кода с использованием средств семантического анализа, выходящая за рамки обычного синтаксического анализа кода (такие инструменты как Cadence HAL и Synopsys SpyGlass). Данная проверка позволяет оперативно найти ошибки в коде до этапов моделирования и синтеза, в том числе проблемы, связанные с переходом между асинхронными доменами (CDC). Данный подход является обязательным для маршрута разработки сложных ГМС по современным проектным нормам и позволяет выявить как опечатки, так и серьёзные проблемы в реализации блока, что в конечном итоге снижает затрачиваемые на верификацию ресурсы. На более поздних этапах применяются высокоуровневые модели блоков и подсистем, среди средств реализации которых используются следующие языки: С++, SystemC/TLM, SystemVerilog. Для проектов типа процессоров или акселераторов наличие полноценной высокоуровневой модели всего блока или устройства является обязательным, поскольку только при наличии такой модели возможно построить полноценный маршрут верификации на базе случайных и направленных тестов. Модель позволяет ускорить процесс разработки тестов за счёт скорости моделирования.

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

Потребность в когерентности кэш-памяти, включая интегрированные сторонние блоки, является неотъемлемой частью современных ГМС. Создание новых типов общих шин и протоколов их функционирования (AMBA 5 CHI), обусловленное, в том числе требованиями систем искусственного интеллекта, увеличило архитектурную сложность ГМС. Тем самым определив необходимость исследования и разработки эффективных алгоритмов и программных средств формирования верификационных последовательностей для иерархии когерентной кэш-памяти. В результате для верификации протокола требуется новая архитектура тестовых окружений и верификационных СФ-блоков, которые поддерживают сложность протокола и обеспечивают необходимую полноту проверки в соответствии со спецификацией. Например, для построения тестового окружения когерентной шины ARM CoreLink CCN-504 (рис. 1.2) на каждом порту необходимо размещение верификационных СФ-блоков, чтобы промоделировать возможный трафик между устройствами ГМС, подключенными через данную шину. В этом примере интерфейс CHI используется для соединения Cortex-A57 и DMC-520. Остальные интерфейсы представляют собой смесь ACE-Lite, AXI4, AHB и APB. После замены верификационных СФ-блоков реальным RTL-описанием компонентов мониторы транзакций переключается в

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

Peripheral address space

Рис. 1.2. Структурная схема шины ARM CoreLink CCN-504

Следующим этапом верификации является прототип в ПЛИС (например, рис. 1.3). На данный момент это самый быстрый с точки зрения временных затрат на исполнение тестов инструмент, доступный при проектировании ГМС. Частота системного тактового сигнала прототипа может достигать десятков мегагерц [3]. Чаще всего прототипирование - это финальная точка подтверждения работоспособности программно-аппаратного комплекса перед изготовлением ИС. На данном этапе возможен запуск прикладных программ, библиотек и операционных систем. Запуск большого объёма прикладного ПО часто выявляет как функциональные проблемы в аппаратуре, так и проблемы, связанные с производительностью. Часто характер реальных данных, обрабатываемых ГМС, отличается от случайных и синтетических паттернов, применяемых на первых этапах верификации блоков. Создание и тестирование сложных краевых сценариев при

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

Рис. 1.3. Платформа (Cadence Protium) для создания прототипов на основе

FPGA 17

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

Симуляция топологического списка цепей системы (GLS) - это последний этап функциональной верификации. На рисунке 1.4 показана схема связи классического имитационного моделирования GLS (например, Incisive Enterprise Simulator) и инструмента STA (например, Cadence Encounter Timing System). Соответственно перед выпуском проекта и передачей GDSII на фабрику выполняется финальный запуск тестов для данного представления.

Рис. 1.4. Схема связи статического временного анализа и GLS моделирования

Статический временной анализ (STA) - метод расчета временных параметров СБИС, не требующий полноценного имитационного моделирования работы ИС [4].

1.2 Аналитический обзор существующих методов верификации ГМС

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

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

Основной проблемой методов динамической верификации на этапе проектирования RTL-описания ГМС является низкая скорость моделирования верификационных последовательностей на целевых ядрах. На этапе натурных испытаний ИС - необходимость создания и использования специальных

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

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

Формирование верификационных последовательностей

Псевдослучайное дополнение шаблона

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

Формальные методы

Проблемные ситуации: краевые ситуации; СФ-блоки; иерархия памяти: многопортовая кэш-память; когерентность памяти; конвейер

Список литературы диссертационного исследования кандидат наук Гаращенко Антон Витальевич, 2021 год

СПИСОК ЛИТЕРАТУРЫ

1. В.В. Степина. Архитектура ЭВМ и вычислительные системы. Учебник. - М.: Курс, Инфра-М, 2017. - 384 с.

2. Дэвид М.Харрис, Сара Л.Харрис. Цифровая схемотехника и архитектура компьютера. - М.: ДМК Пресс, 2017. - 792 с.

3. Бибило, П.Н. Моделирование и верификация цифровых систем на языке VHDL: моногр. / П.Н. Бибило. - Москва: Ленанд, 2017. - 344 c.

4. Буренков В.С. Анализ применимости инструмента SPIN к верификации протоколов когерентности памяти. -«Вопросы радиоэлектроники», сер. ЭВТ, 2013, вып.3, с.126-134.

5. Vigyan Singhal, Starting Formal Right from Formal Test Plannin, Oski Technology, Verification Academy at DAC-2015.

6. David M. Russinoff. Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover.

7. Камкин А.С., Петроченков М.В. «Система поддержки верификации реализаций протоколов когерентности с использованием формальных методов» Вопросы радиоэлектроники», серия ЭВТ, апрель 2014.

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

9. Principles of Verifiable RTL Design: A functional coding style supporting verification processes in Verilog Hardcover, Springer - May 31, 2001

10. The Cortex-A15 Verification Story DVClub Wednesday, December 7, 2011 from 1:00 AM to 1:30 PM (CST) Austin, TX.

11. Тарасик В.П. Математическое моделирование технических систем: учебник для вузов / В.П. Тарасик. М.: Наука, 1997. 600 с.

12. Шеннон Р. Имитационное моделирование систем -искусство и наука / Р. Шеннон. М.: Мир, 1978. 308 с.

13. Синицын, С.В. Верификация программного обеспечения / С.В.

Синицын. - М.: Бином. Лаборатория знаний, 2017. - 463 c.

97

14. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: ModelChecking. М.: МЦНМО, 2002.

15. Apt K. R., Kozen D. C. Limits for the automatic verification of finite-state concurrent systems // Information Processing Letters. 1986/22, pp.307-309.

16. А.Н. Мешков, М. П. Рыжов, В. А. Шмелев (ЗАО «МЦСТ») развитие средств верификации микропроцессора «ЭЛЬБРУС».

17. Шмелёв В.А., Стотланд И.А. Автономная верификация микропроцессоров на ос-новее эталонных моделей разного уровня абстракции. В сб.: Научные труды Всероссийской научно-технической конференции «Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС)»,2012, No1, с. 435-440.

18. Ф.М. Путря. «Применение генераторов случайных программ и случайных фоновых воздействий при функциональной верификации многоядерных систем на кристалле» Материалы Седьмой Международной конференции "Автоматизация проектирования дискретных систем". 16-17 ноября 2010 г., Минск, с. 234 -241.

19. Гаращенко А.В., Гагарина Л.Г., Федотова Е.Л., Высочкин А.В., Зайцев В.В. Разработка генератора верификационных тестов для многоядерных структур // Информатизация и связь. 2017. № 4. - C. 2025.

20. ZakonovA., StepanovO., ShalytoA. GA-Based and Design by Contract Approach to Test Generation for EFSMs /Proceedings of IEEE East-West Design & Test Symposium (EWDTS40). St. Petersburg. 2010, pp.152-155.

21. Камкин А. С., Коцыняк А. М., Смолов С. А., Татарников А. Д., Чупилко М. М., Сортов А. А. Средства функциональной верификации микропроцессоров. Труды Института системного программирования РАН Выпуск № 1 / том 26 / 2014 с. 149-206.

22. Рыжов М.П. Система шаблонной генерации тестов -«Вопросы радиоэлектроники», сер. ЭВТ, 2013, В. 3, с.117-125.

23. Rudell, Richard L.Multiple-Valued Logic Minimization for PLA Synthesis.-140с.

24. Закревский А.Д. Логические основы проектирования дискретных устройств Закревский А.Д., Поттосин Ю.В., Черемисинова Л.Д. М.: ФИЗМАТЛИТ, 2007 г. - 592 с.

25. Sunil P. Khatri, KanupriyaGulati. Advanced techniques in logic synthesis, optimizations and applications. Springer, 2011. - 423 с.

26. Waterman A., Asanov^ K. The RISC-V Instruction Set Manual. Volume II: Privileged Architecture. Version 1.10. University of California, Berkeley. May 7, 2017. 91 P.

27. L. Fournier, Y. Arbetman, and M. Levinger, "FunctionalVerification Methodology for Microprocessors Using theGenesys Test Program Generator: Application to the x86Microprocessors Family," Proc. Design Automation andTest in Europe (DATE 99), IEEE CS Press, 1999, pp.434441.

28. A. Adir et al., "Deeptrans—A Model-Based Approach toFunctional Verification of Address TranslationMechanisms," Proc. 4th Int'l Workshop MicroprocessorTest and Verification: Common Challenges andSolutions, IEEE CS Press, 2003, pp. 3-7.

29. Alan Mishchenko, SatrajitChatterjee, Robert Brayton. DAG-Aware AIG Rewriting. San Francisco, California, USA.: DAC 2006, July 24-28, 20.-532-535с.

30. Alexander Kamkin, Eugene Kornykhin, Dmitry Vorobyev, "Reconfigurable Model-Based Test Program Generator for Microprocessors", Software Testing Verification and Validation Workshops (ICSTW) 2011 IEEE Fourth International Conference on, pp. 47-54, 2011.

31. M. Rimon, Y. Lichtenstein, A. Adir, I. Jaeger, M. Vinov, S. Johnson, D. Jani, "Addressing Test Generation Challenges for Configurable Processor Verification", High-Level Design Validation and Test Workshop 2006.

Eleventh Annual IEEE International, pp. 95-101, 2006.

99

32. Андерсон Дж. Дискретная математика и комбинаторика. — М.: Вильямс, 2006. — 960 с.

33. Prabhat Mishra, Heon-mo Koo, Zhuo Huang, "Language-driven Validation of Pipelined Processors using Satisfiability Solvers", Microprocessor Test and Verification 2005. MTV '05. Sixth International Workshop on, pp. 119126, 2005.

34. E. V. Kornykhin, "Generation of test data for verification of caching mechanisms and address translation in microprocessors", Programming and Computer Software, vol. 36, pp. 28, 2010.

35. A. S. Kamkin, T. I. Sergeeva, S. A. Smolov, A. D. Tatarnikov, M. M. Chupilko, "Extensible environment for test program generation for microprocessors", Programming and Computer Software, vol. 40, pp. 1, 2014.

36. Fedor Putrya, Kirill Zhezlov, Yaroslav Kolbasov, Artyom Nikolaev. Vertical and Horizontal Code Reuse for SoC Functional Verification and Performance Analysis Stages. CDNLive2018, SoC Design and Verification, SVG15.

37. КлебановА.А., СтепановО.Г., ШалытоА.А.Применение шаблонов требований к формальной спецификации и верификации автоматных программ /Труды семинара «Семантика, спецификация и верификация программ: теория и приложения». Казань, 2010, с.124-130.

38. John M. Ludden, Michal Rimon, Bryan G. Hickerson, Allon Adir, Hardware and Software: Verification and Testing, vol. 6504, pp. 146, 2011.

39. Гуров В.С., Мазин М.А., Нарвский А.С., Шалыто А.А. Инструментальное средство для поддержки автоматного программирования // Программирование. 2007. No6, с.65-80.

40. Иванов Б. Н. Дискретная математика. Алгоритмы и программы. — М.: Физматлит, 2007. — 408 с.

41. Статья «Модульное тестирование: 2+2 = 4?»: [сайт]. [2015]. URL:

http://rsdn.ru/article/testing/UnitTesting.xml.

100

42. Миронов А.М., Жуков Д.Ю. Математическая модель и методы верификации программных систем // Интеллектуальные системы. Т.9. 2005. Вып.1-4, с.209-252.

43. Unit Testing Guidelines: [сайт]. [2015]. URL: http ://geosoft.no/devel opment/unittesting .html.

44. Roy Osherove. The Art of Unit Testing, 2009. -320с.

45. ОАО Ангстрем. Базовые матричные кристаллы для полу заказных БИС, 2001. - 4с.

46. Alan Mishchenko. A New Enhanced Approach to Technology Mapping, 2001. - 7с.

47. T. Ibaraki, S. Muroga. Synthesis of Networks with a Minimum Number of Negative Gates. IEEE Transactions on Computers, 1971. - 49-58с.

48. MassoudPedram, Narasimha Bhat. Layout driven technology mapping, 1985. -43с.

49. Гагарина Л.Г., Киселев Д.В., Федотова Е.Л. Разработка и эксплуатация автоматизированных информационных систем Москва 2007, 384 с.

50. Григорий Речистов. Моделирование и оптимизация алгоритмов работы кэшей. - М.: LAP Lambert Academic Publishing, 2011. - 76 с.

51. Аванесов B.C. Теоретические основы разработки заданий в тестовой форме. М.: Исследовательский центр, 1995.

52. Акчурин P.M. Задача автоматизации программирования имитационно диалоговых систем // Программирование. - 1982. - №3.

53. П.А. Головинский. Математические модели. Теоретическая физика и анализ сложных систем. Книга 2. От нелинейных колебаний до искусственных нейронов и сложных систем. - М.: Либроком, 2012. -234 с.

54. Путря Ф.М. Особенности верификации современных систем на кристалле. Микроэлектроника-2015. Интегральные схемы и микроэлектронные модули: проектирование, производство и

применение сборник докладов Международной конференции. 2016. С. 49-57.

55. Поспелов Д. А. Логические методы анализа и синтеза схем. Энергия, 1974. - 368с.

56. Документация на WBQ кэша L2 системы на кристалле «Эльбрус-2S».

57. Проверка параметризованных Promela-моделей протоколов когерентности памяти, труды Института системного программирования РАН, том 28, вып. 4, 2016, стр. 57-76.

58. MIPS R4000PC/SC Errata, Processor Revision 2.2and 3.0. - MIPS Technologies Inc., 1994, May 10.

59. Purify: Fast Detection of Memory Leaks and Access Errors. January 1992.

60. C.V. Ramamoorthy, Siu-BunF. Ho, and W. T. Chen. On the Automated Generation of Program Test Data. IEEE Transactionson Software Engineering, 2(4):293-300,1976.

61. Andrei Tatarnikov, "An approach to instruction stream generation for functional verification of microprocessor designs", East-West Design & Test Symposium (EWDTS) 2016 IEEE, pp. 1-4, 2016.

62. А.С. Камкин, А.С. Проценко, А.Д. Татарников. Метод генерации тестовых программ на основе формальных спецификаций механизмов кэширования. Труды ИСП РАН,том 27, вып. 3, 2015 г., с. 125-138.

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

64. Mehta A.B. (2017) Cache Memory Subsystem Verification: UVM Agent Based. In: ASIC/SoC Functional Design Verification. Springer, Cham.

65. W. Pugh. A Practical Algorithm for Exact Array Dependence Analysis. Communications of the ACM, 35(8): 102- 114, August1992.

66. Rajiv Bhatia, Eyal Bin, Eitan Marcus, Gil Shurek, "An ontology and constraint based approach to cache preloading", High Level Design

Validation and Test Workshop (HLDVT) 2010 IEEE International, pp. 129136, 2010.

67. Калбертсон Р., Браун К., Кобб Г. Быстрое тестирование. - М.: Издательский дом «Вильямс», 2002.

68. Belyayev Andrey Aleksandrovich, Gagarina Larisa Gennadyevna, Koldayev Viktor -Dmitriyevich, Shchagin Anatoliy Vasilyevich and Yanakova Yelena Sergeyevna. - Methods and Techniques for Improving Processing Efficiency of Broadband Signals. - Indian Journal of Science and Technology - 2016. - №9(20). - C.1-8.

69. B.Nichols, D.Buttlar, and J. P. Farrell. Pthreads Programming. O'Reilly, 1998.

70. Жезлов К.А., Колбасов Я.С., Козлов А.О., Николаев А.В., Путря Ф.М., Фролова С.Е. Автоматизация процесса создания тестовых окружений обеспечивающая сквозной маршрут разработки, верификации и исследования сф-блоков и СнК. Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2016. № 2. С. 46-53.

71. Stotland I, Meshkov A., Kutsevol V. Standalone functional verification of multicore microprocessor memory subsystem units based on application of memory subsystem models. Proc. of IEEE East-West Design & Test Symposium (EWDTS 2015), Batumi, Georgia, September 26-29, 2015, pp. 326-330.

72. Petrochenkov M., Stotland I., Mushtakov R. Approaches to Stand~aloneVerification of Multicore Multiprocessor Cores. Trudy ISP RAN/ProculSP RAS, vol. 28, issue3, 2016, pp. 161-172. DOI: 10.155l4/ISPRAS-2ol6-28(3)-I0.

73. А. Камкин Верификация микропроцессоров: борьба с ошибками и управление качеством. Электроника: Наука, Технология, Бизнес, №3, 2010. С. 98-104.

74. Иванников В.П., Камкин А.С., Косачев А.С, Кулямин В.В., Петренко

А.К. использование контрактных спецификаций для представления

103

требований и функционального тестирования моделей аппаратуры. -Программирование, 2007, No5, с. 61.

75. Clifford E. SystemVerilog Assertions. Design Tricks and SVA bind files. SunburstDesign, 2009. 42 p.

76. P. M.Maurer. Generating Test Data with Enhanced Context-Free Grammars. IEEE Software, 7(4):50-55, July1990.

77. Путря Ф.М., Медведев И.А. Верификация коммутационной логики для систем и сетей на кристалле. Вопросы радиоэлектроники. 2012. Т. 1. № 2. С. 56-66.

78. T. O'Malley, D.Richardson, and L.Dillon. Efficient Specification-Based Oracles for Critical Systems. In Proc. Of the California Software Symposium, 1996.

79. A.Pnueli. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46-77, 1977.

80. Кулямин В.В. Методы верификации программного обеспечения, 2008 -www.ispras.ru/~kuliamin/docs/VerMethods-2008-ru.pdf.

81. Xiaoke Qin, Prabhat Mishra, "Automated generation of directed tests for transition coverage in cache coherence protocols", Design Automation & Test in Europe Conference & Exhibition (DATE) 2012, pp. 3-8, 2012.

82. Колдаев В.Д. Основы алгоритмизации и программирования: Учебное пособие / В.Д. Колдаев. Под ред. Гагариной Л.Г... - М.: ИД «ФОРУМ» - ИНФРА-М, 2006, 2009. - 416 с.

83. Putrya F. Method of free c++ code migration between soc level tests and standalone ip-core uvm environments. Proceedings of IEEE East-West Design and Test Symposium, EWDTS 2014.

84. Сайт отдела интегральных микросхем НПК «Технологический центр МИЭТ»: [сайт]. [2015]. URL: http://www.asic.ru/

85. Ю.И. Галушкина, А.Н. Марьямов. Конспект лекций по дискретной математике - 2-е изд., испр. - М.: Айрис-пресс, 2008. - 176 с.

86. Hayes D.P. Digital Logic Design. Addison Wesley. 1993. - 342 с.

87. Korey Sewell, Frank Vahid.Profiling Simple Digital Design Components as Two-Level Implementations using the ESPRESSO logic minimization tool Department of Computer Science and Engineering University of California, Riverside Riverside, 2003.

88. Гаращенко А.В., Гагарина Л.Г. Исследование и разработка методики формирования тестовых последовательностей на основе графовой модели иерархии кэш-памяти // Известия вузов. Электроника. Том 25. - 2020 - №6. - C. 548-557.

89. Гаращенко А.В., Гагарина Л.Г. Исследование и разработка алгоритма формирования тестовой последовательности для оценки энергопотребления RTL-модели процессора // Информационные технологии и вычислительные системы. 2020. № 3. С. 94-100.

90. Garashchenko A.V., Nikolaev A.V., Putrya F.M., Sardaryan S.S. System of combined specialized test generators for the new generation of vliw dsp processors with elcore50 architecture // Проблемы разработки перспективных микро- и наноэлектронных систем (МЭС). 2019. № 2. С. 2-7.

91. Гаращенко А.В., Николаев А.В., Путря Ф.М., Сардарян С.С. Система комбинируемых специализированных генераторов тестов для нового поколения vliw dsp процессоров с архитектурой elcore50 // Проблемы разработки перспективных микро- и наноэлектронных систем (мэс). 2018. № 2. - C. 9-15.

92. Garashchenko A.V., Gagarina L.G, Ye K.Z., Dorogova E., Kochneva M. Development of an Approach to Automatic Test Generation Based on the Graph Model of a Cache Hierarchy // В сборнике: proceedings of the 2020 ieee conference of russian young researchers in electrical and electronic engineering, eiconrus 2020. 2020. - C. 1940-1944.

93. Garashchenko A.V., Putrya F.M., Gagarina L. Automatic test generation

methodology for verification of a cache memory based on the graph model

of cache hierarchy // В сборнике: Proceedings of the 2019 IEEE Conference

105

of Russian Young Researchers in Electrical and Electronic Engineering, ElConRus 2019. 2019. - С. 1876-1879.

94. Gagarina L.G., Garashchenko A.V., Shiryaev A.P., Fedorov A.R. An approach to automatic test generation for verification of microprocessor cores // В сборнике: Proceedings of the 2018 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering, ElConRus 2018. 2018. - С. 1490-1491.

95. Гаращенко А.В. Исследование и разработка графовой модели иерархии кэш-памяти vliw dsp процессоров для генерации тестов // В сборнике: актуальные проблемы информатизации в науке и образовании - 2018. материалы научно-практической конференции: сборник статей. 2018. -C. 31-36.

96. Гаращенко А.В. Исследование и разработка графовой модели подсистемы памяти многоядерных структур для генерации тестов // В сборнике: микроэлектроника и информатика - 2018. материалы научно-технической конференции. сборник статей. 2018. - C. 66-71.

97. Чумаченко П.Ю., Гаращенко А.В. Разработка генератора верификационных тестов для многоядерных структур // В сборнике: сборник научных докладов международной научно-практической конференции "актуальные проблемы науковедения, культуры, образования, экономики, информатики и социальные трансформации -2017". Международная научно-практическая конференция. 2017. - C. 65-71.

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

/

УТВЕРЖДАЮ

Начальник Инженерного Центра АО «РСК «МиГ» тель председателя НТС А.В.Терпугов 2021 г.

АКТ

о практическом применении полученных результатов диссертационного исследования Гаращенко A.B. на тему: «Разработка методики и алгоритмов верификации гетерогенных многоядерных систем на основе графовой модели иерархии когерентной кэш-памяти», представленной на соискание учёной степени кандидата технических наук по специальности 05.13.01 —Системный анализ, управление и обработка информации (приборостроение)

Настоящим актом удостоверяется, что в Инженерном Центре АО «РСК «МиГ» изучены теоретические разработки и практические рекомендации диссертационного исследования Гаращенко A.B. на тему: «Разработка методики и алгоритмов верификации гетерогенных многоядерных систем на основе графовой модели иерархии когерентной кэш-памяти», представленной на соискание учёной степени кандидата технических наук по специальности 05.13.01 — Системный анализ, управление и обработка информации (приборостроение)

Результаты диссертационного исследования обладают высокой актуальностью и представляют практический интерес для Инженерного Центра АО «РСК «МиГ», а именно:

• графовая модель иерархии когерентной кэш-памяти ГМС, которая является базисом методики формирования верификационных последовательностей для ГМС;

• методика формирования верификационных последовательностей для ГМС на основе графовой модели иерархии когерентной кэш-памяти;

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

верификационных последовательностей в совокупности с генетическим алгоритмом их формирования могут найти применение в OA «РСК «МиГ».

Результаты внедрения в маршрут проектирования ГМС могут привести к достижению 97% переключательной активности всех сигналов и 95% тестового покрытия кода RTL-описания DSP ядра.

Заместитель Главного конструктора по техническим средствам обучения и полунатурной отрабо наук

Заместитель Главного конструктора по системам управления, Заслуженный машиностроитель РФ, доктор технических наук

А.В.Пономаренко

УТВЕРЖДАЮ

11роректор МИЭТ по учебной работе доктор технических наук, профессор

И.Г. Игнатова

^ЩМ 16 "._оз

2020 г.

АКТ

внедрения результатов диссертационной работы Гаращенко A.B. на тему «Разработка методики и алгоритмов верификации гетерогенных многоядерных

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

Результаты кандидатской диссертации Гаращенко A.B., посвященной разработке методики и алгоритмов формирования верификационных последовательностей для RTL-описаний гетерогенных многоядерных систем (ГМС). а именно:

• графовая модель иерархии когерентной кэш-памяти ГМС на основе алгоритмов построения и решения недетерминированных ситуаций;

• методика формирования верификационных последовательностей для системного тестирования ГМС на основе графовой модели иерархии когерентной кэш-памяти и алгоритма проверки устройства управления процессорных ядер системы;

• генетический алгоритм формирования верификационных последовательностей на основе клеточного автомата для оценки переключательной активности ИТЪ-описания ГМС.

используются в учебном процессе Института системной и программной инженерии и информационных технологий (СПИИТех) Национального исследовательского университета "МИЭТ" в лекционных и практических занятиях по дисциплинам «Современные проблемы информатики и вычислительной техники», «Компьютерные технологии в науке и образовании».

Директор СПИНТЕх,

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

Л.Г. Гагарина

Ученый секретарь С11И1 ГГех, кандидат технических наук, доцент

В.В. Слюсарь

СВИДЕТЕЛЬСТВО ОБ ИНТЕЛЛЕКТУАЛЬНОЙ СОБСТВЕННОСТИ

ФРАГМЕНТЫ ПРОГРАММ РАЗРАБОТАННОГО КПС

IlHiiuiia.iinauiifl nporpaMMbi

!! !! !!

Invokes generator-program when the generator module is run as a script.

Example: python -m generator check !! !! !!

import random

from optparse import OptionParser

from config import PATH, SEED, AMOUNT_SEQ, PROGSC_PATH, EXCEPTION_EN, MEM_EN, TRACE_FILTER, DEF_VAL, VERSION from config import PROGSC_VLIW1_PATH from program import Program

AMOUNT_INSTR_IN_LOOP = DEF_VAL DEEP_LOOPS = DEF_VAL COUNT LOOP STEP = DEF VAL

def main(): global AMOUNT_INSTR_IN_LOOP global DEEP_LOOPS global COUNT_LOOP_STEP

parser = OptionParser()

parser.add_option("-p", dest-'path", default=PATH) parser.add_option(" -g", dest="progsc_path", default=PROGSC_PATH) parser.add_option(" -v", dest="progsc_vliw1_path", default=PROGSC_VLIW1_PATH)

parser.add_option("-l", dest="amount_seq", type="int", default=AMOUNT_SEQ)

# parser.add_option("-b", dest="amount_subroutine", type="int", default=AMOUNT_SUBROUTINE) parser.add_option("-s", dest="seed", type="int", default=SEED) parser.add_option("-d", dest="DEEP_LOOPS", type="int", default=DEF_VAL) parser.add_option(" -i", dest="AMOUNT_INSTR_IN_LOOP", type="int", default=DEF_VAL)

parser.add_option("-c", dest="COUNT_LOOP_STEP", type="int", default=DEF_VAL)

parser.add_option("-e", dest="exception_en", type="int", default=EXCEPTION_EN) parser.add_option("-m", dest="mem_en", type="int", default=MEM_EN) parser.add_option("-f', dest="trace_filter_en", type="int", default=TRACE_FILTER) (options, args) = parser.parse_args()

random.seed(options.seed)

gen_am_start = min(min(9, options.amount_seq), min(options.amount_seq + 1, abs(options.amount_seq - 10)))

gen_am_end = max(min(10, options.amount_seq), min(options.amount_seq + 1, abs(options.amount_seq - 10))) if gen_am_start == gen_am_end:

gen_am_end += 1 general_amount_seq = random.randrange(gen_am_start, gen_am_end) amount_seq = general_amount_seq

amount_subroutine = options.amount_seq + 1 - general_amount_seq AMOUNT_INSTR_IN_LOOP = options.AMOUNT_INSTR_IN_LOOP - 1 if options.AMOUNT_INSTR_IN_LOOP != DEF_VAL else DEF_VAL DEEP_LOOPS = options.DEEP_LOOPS COUNT_LOOP_STEP = options.COUNT_LOOP_STEP

exc_en = bool(options.exception_en) mem_en = bool(options.mem_en) trace_filter_en = bool(options.trace_filter_en)

progsc_paths = [options.progsc_path, options.progsc_vliw1_path] progsc_body = [None] * len(progsc_paths) progsc_init = [None] * len(progsc_paths)

for i, path in enumerate(progsc_paths): with open(path) as progsc_file: body = progsc_file.readlines()

body_start = body.index("init_finish: nop ; FMT_3m\n") progsc_init[i] = body[body_start - 9: body_start] progsc_body[i] = body[body_start + 1: -13]

# progsc_body = map(lambda e: e.replace("r0", "r2"), progsc_file.readlines()[102:-13])

# print(''.join(progsc_body))

program = Program(amount_seq, amount_subroutine, progsc_body, exc_en, mem_en, progsc_init, trace_filter_en)

print("\ncontrol_flow generator version :: " + VERSION + "\n") print(str(program))

with open(options.path, 'w') as test_file: test_file.write(str(program))

# print(program.reg_values) ## useless because of progsc_gen if exc en and trace filter en:

with open(,7"join(options.path.split('7")[>1]) + '7test_control_flow_filter.txt", 'w') as test_file: test_file.write(program.filter_file)

if_name_== "_main_":

main()

2. Класс Program

!! !! !!

This is the main file. It creates AMOUNT_SEQ_NUMBER a random SEQ

sequences. AMOUNT_SEQ_NUMBER is specified in the

configuration file. !! !! !!

class Program:

def_init_(self, amount_seq, amount_subroutine, progsc_body, exception_en,

mem_en, progsc_init, trace_filter_en): ......Create a test .

:param amount_seq: total number of sequences to generate (control flow base

unit)

:param amount_subroutine: total number of subroutines :param progsc_body: test code that is inserted in subroutines, loops and etc (list - second is prog with vliw=1)

:param exception_en: bool value that enable generating exception and exception handlers

:param mem_en: bool value that enable generating transactions to memory :param progsc_init: additional test code that is inserted in reg_init area (list)

The total test length is counted as amount_seq + amount_subroutine +

amount_exception_handlers. !! !! !!

# if memory mode is enabled excl_regs = [] progsc_init_str = "" self._mem_en = mem_en if mem_en:

progsc_init_str = '\t' + '\t'.join(progsc_init[0])

excl_regs = set(re.findall(r"r([0-9]{1,2})\.l\b", progsc_init_str)) excl_regs = list(map(lambda e: int(e), list(excl_regs)))

self._vadr_reg = VecReg(int(re.fïndall(r", v([0-9]{1,2})\.l", progsc_init[0][-

1])[0]))

# init regs

self._reg_pool = RegPool(excl_regs)

self._reg_init = self._reg_pool.init_pool + progsc_init_str

# create obj for working with stack self._stack = SeqStack(self)

# get progsc_body, create body self._progsc_body = progsc_body[0] self._progsc_body_vliw1 = progsc_body[1] rm.shuffle(self._progsc_body)

filters = Filters(self) self._progsc_vliw_do = filters.vliw_do self._progsc_vliw_jb = filters.vliwjb self._code_body = []

# make and generate exceptions self_trace_filter_en = trace_filter_en self._exc_pool = None self._exc_hndl_pool = None

if exception_en:

self._progsc_body = filters.without_fpe self._exc_hndl_pool = ExcHandlerPool(self)

self._exc_pool = [SeqExc(self, i) for i in range(rm.randint(300, 400))] self._code_body.extend(self._exc_hndl_pool. init_pool) self. _reg_init +=

self._reg_pool.init_EVAR_reg(self._exc_hndl_pool.get_EVAR_adr) self._reg_init += self._reg_pool.init_IMASKR_reg(159) # self._reg_init += self._reg_pool.init_DMASKR_reg(0)

# make and generate subroutines self._subroutine_pool = [SeqSubroutine(self, i) for i in

range(amount_subroutine)]

list(map(lambda e: e.gen_seq(self._subroutine_pool), self._subroutine_pool))

# make and generate sequences

self._code_body.extend([SeqSeq(self, i, i == amount_seq).gen_seq for i in range(amount_seq + 1)])

# add filtered subroutines by call

self._subroutine_pool = list(filter(lambda e: e.is_used, self._subroutine_pool))

self._code_body.extend(list(map(lambda e: e.body, self._subroutine_pool)))

# shuffle program body rm.shuffle(self._code_body)

@property

def reg_values(self):

return "\n".join(map(lambda e: "%2d" % e.number + " " + "0x%08x" % e.value.high + " " + "0x%08x" % e.value.low, self._reg_pool .general_regs))

@property def filter_file(self):

init_f = "reg_init:test_start\n"

exc_list = list(filter(lambda e: e.is_used, self._exc_pool)) gen_filter_list = [] for e in exc_list:

gen_filter = e.gen_filter add_filter_fl = False for code_line in self._code_body: if gen_filter.split(":")[0] in code_line: add_filter_fl = True break if add_filter_fl:

gen_filter_list.append(gen_filter)

return init_f + "\n"join(gen_filter_list) + "\n" + self_exc_hndl_pool.gen_filter

def_str_(self):

return code_header(self._reg_init) + code_stop() + "".join(self_code_body) + NOP.apply()

def code_header(reg_init):

return (".global_start\n"

".global reg_init\n"

".global " + str(LOOP_COUNTER_LABEL) + ".global " + str(HANDLER_DATA_LABEL) + ".global " + str(sTACK_POINTER_LABEL) + ".global test_start\n"

".global " + str(TEST_STOP_LABEL) +

"\n_start:\n"

+ code_data() +

"\n.text\n" ".align 8\n\n" + reg_init + "\ntest_start:\n" "\t b seq_0\n\n")

def code_stop():

stp_com = "stop" if rm.randint(0, 1) == 0 else "stopdi"

return ("test_stop:\n" "\ttrl 0, R0\n" "\t" + stp_com + "\n" + "\tnop\n" "\tnop\n" "\tnop\n" "\tnop\n\n")

def code_data(): return ("\n.data\n" ".align 8\n\n"

+ LOOP_COUNTER_LABEL. mark + "\t.word 0x0\n\n"

+ HANDLER_DATA_LABEL. mark + "\t.word 0x0, 0x0, 0x0, 0x0 \n\n" + STACK_POINTER_LABEL. mark + "\t.word 0x0\n")

3. Класс SeqStack

!! !! !!

This file creates a random sequences of working with stack. !! !! !!

import random as rm

from config import TRL, LDL_A_ADD, ST, LD, ADD, STACK_POINTER_LABEL, LDL_A_SUB, SUB from operand import Imm64, RegImm, Reg64, ReglmmOfs

class SeqStack:

def_init_(self, program):

......Create the sequences of working with stack

:param program: reference on Program object !! !! !!

self._pr = program

def store_reg(self, reg: Reg64): r_pool = self._pr.reg_pool adr_reg = r_pool.read_first

seq = "".join([

TRL.apply([Imm64(STACK_POINTER_LABEL.label_name), r_pool .read_st_pointer_reg], vliw=True),

TRL.apply([Imm64(4), adr_reg]),

LDL_A_ADD.apply([RegImm(r_pool.read_st_pointer_reg),

adr_reg]),

ST.apply([reg, RegImm(adr_reg)], suf="l")

]

if rm.randint(0, 99) < 50 else [

TRL.apply([Imm64(STACK_POINTER_LABEL.label_name), r_pool.read_st_pointer_reg]),

LD.apply([RegImm(r_pool.read_st_pointer_reg), adr_reg],

suf="l"),

ST.apply([reg, RegImm(adr_reg)], suf="l"), ADD.apply([Imm64(4), adr_reg, adr_reg], suf="l"), ST.apply([adr_reg, RegImm(r_pool.read_st_pointer_reg)], suf="l")

])

return seq

def restore_reg(self, reg: Reg64): r_pool = self._pr.reg_pool adr_reg = r_pool.read_first

seq = "".join([])

return seq

4. Файл restore_context.py

!! !! !!

This class describes context restoring for test continuing from any step in traces. !! !! !!

import os

inst_list = [] # instructions list (ELCORE50)

trace = [] # trace list

dis = [] # disassembler list

step_num = 92 # step number

next_step = "step " + str(step_num + 1).zfill(8) # next step

step = "step " + str(step_num).zfill(8) # step format in trace (xxxxxxxx)

step_trace_line = 0 # line index of step in trace

step_asm_i = 0 # line index of step in asm

step_dis_i = 0 # line index of step in disassembler

step_instr = "" # instruction of step

line_num_st = 0 # line number of start label in disassembler

with open(os.environ['WORK_HOME'] + "instructionsELC0RE50.txt") as inst_file: for e in inst_file: inst_list.append(e.split("\t")[1 ] .strip()) inst_list = set(inst_list)

with open(os.environ['WORK_HOME'] + "test_control_flow.s") as asm_file: asm = asm_file.readlines() # assembler list

with open(os.environ['WORK_HOME'] + "test_control_flow.dis") as dis_file: line_count = 0 for e in dis_file: if "Disassembly of section .stab:" in e:

break if e == "\n": continue

if "<_start>:" in e:

line_num_st = line_count

dis.append(e) line_count += 1

with open(os.environ['WORK_HOME'] + "DSP0.log") as trace_file: line_count = 0 for e in trace_file: if next_step in e:

break elif e == "\n":

continue elif step in e:

step_trace_line = line_count

trace.append(e) line_count += 1

step_dis_adr = trace[step_trace_line].split()[2][8:] # step address in dis for i, e in enumerate(dis): if step_dis_adr in e:

step_instr = e.split('\t')[2].split()[0].split('.')[0].strip()

step_dis_i = i

break

reg_init_fl = False

instr_between = step_dis_i - line_num_st for i, e in enumerate(asm): if not reg_init_fl: reg_init_fl = "reg_init:" in e continue

instr_between -= list(map(lambda el: e1.split(".")[0] in inst_list, e.split())).count(True)

if instr_between == 1: step_asm_i = i break

print("from dis :: start :: ", line_num_st, dis[line_num_st].strip()) print("from dis :: step :: ", step_dis_i, dis[step_dis_i].strip()) print("from trace :: step :: ", trace[step_trace_line + 1].strip()) print("from asm :: step :: ", step_asm_i, asm[step_asm_i].strip())

rst_context = [

"restore_context:\n", "\n\tnop\n"

]

asm[18] = "\tb continue trl st_pointer, r0\n" asm.extend(rst_context)

with open(os.environ['WORK_HOME'] + "restored_test_control_flow.s", "w") as asm_file:

asm_file.write("".join(asm))

5. Класс RegPool

!! !! !!

This file describes all regs. !! !! !!

class RegPool:

def_init_(self, excl_regs):

......Create the pool of general (scalar and vector), system and predicate

registers

:param excl_regs: list of excluded registers (registers being used for stack

pointer or other purpose) !! !! !!

allowed_regs_num = list(range(REG_AMOUNT + 1)) excl_regs.append(RETURN_ADR_REG_NUMBER) list(map(lambda e: allowed_regs_num.remove(e), excl_regs)) stack_pointer_reg_number = allowed_regs_num[0] allowed_regs_num.remove(stack_pointer_reg_number)

self._stack_pointer = Reg64(stack_pointer_reg_number) self._return_adr_reg = Reg64(RETURN_ADR_REG_NUMBER) self._true_predicate_reg = PredicateReg(TRUE_PREDICATE_REG_NUMBER) self._inited = False self._predicate_regs = [] self._general_regs = [] self._vector_regs = [] self._loop_regs = {} self._system_regs = { "PC": SysReg("PC"), "IRQR": SysReg("IRQR"), "IMASKR": SysReg("IMASKR"), "EVAR": SysReg("EVAR"), "ERTAR": SysReg("ERTAR"), "IRQ_INDEX": SysReg("IRQ_INDEX"), "DMASKR": SysReg("DMASKR"), "DCSR": SysReg("DCSR"), "CSP": SysReg("CSP")

}

# add loop registers for i in range(4):

self._loop_regs["LA" + str(i)] = SysReg("LA" + str(i)) self._loop_regs["LB" + str(i)] = SysReg("LB" + str(i)) self._loop_regs["LC" + str(i)] = SysReg("LC" + str(i))

# add general regs with allowance for excluded regs

# excl_regs.extend([0, RETURN_ADR_REG_NUMBER]) for i in allowed_regs_num:

if i not in excl_regs:

self._general_regs.append(Reg64(i))

# add vector regs

for i in range(VEC_REG_AMOUNT): self._vector_regs.append(VecReg(i))

# add predicate regs

for i in range(PREDICATE_REG_AMOUNT): if i != TRUE_PREDICATE_REG_NUMBER: self._predicate_regs.append(PredicateReg(i))

@property def init_pool(self): self._inited = True init_list = [

TRL1.apply([Imm64(0), self._stack_pointer], vliw=True), # STACK POINTER REG init

TRL.apply([Imm64(STACK_POINTER_LABEL.label_name), self._stack_pointer], nesting=0),

ADD.apply([Imm64(4), self._stack_pointer, self._return_adr_reg], suf="l"), ST.apply([self._return_adr_reg, RegImm(self._stack_pointer)], suf="l"), TRL1.apply([Imm64(Rand.word()), self._return_adr_reg], vliw=True), # RETURN ADR REG NUMBER init

TRL.apply([Imm64(Rand.word()), self._return_adr_reg], nesting=0)

]

# general regs init

for i, e in enumerate(self._general_regs): vliw = True if i % 2 == 0 else False

init_list.append(TRL 1 .apply([Imm64(Rand.word()), self._general_regs [i] ], nesting=vliw, vliw=True))

init_list.append(TRL.apply([Imm64(Rand.word()), self._general_regs[i]], nesting=0, vliw=vliw))

# general vectors regs init for e in self._vector_regs:

init_list.append(VREPRL.apply([str(self.read_any), e]))

# reset vector accumulator

for i in range(VECTOR_ACC_REG_AMOUNT): init_list.append(VCLRAC.apply(["va" + str(i) + ".d0"]))

# predicate regs init

for i in range(PREDICATE_REG_AMOUNT - 1): # because without TRUE_PREDICATE_REG_NUMBER reg = str(self._general_regs[i]) p_reg = str(self._predicate_regs[i]) init_list.append(TRC.apply([reg + ".l", p_reg]))

init_list.append(TDC.apply([reg + ".d", "v" + p_reg])) # vector predicate regs init

return Label("reg_init").mark + "".join(init_list)

5. Класс SeqSeq

!! !! !!

This file creates a random SEQ sequence. !! !! !!

class SeqSeq:

def_init_(self, program, seq_number, last_seq):

......Create the sequence (base test unit)

:param program: reference on Program object :param seq_number: sequence number for generating sequence label UNIQUE name

:param last_seq: value determines that it is last sequence or not !! !! !!

self._pr = program self._seq_number = seq_number self._label = LabelSeq(seq_number) self._last_seq = last_seq

@property def gen_seq(self): add_command = NOP.apply() if self._pr.trace_filter_en else ""

additional_seq = [ rm.choice(self._pr.subroutine_pool).call, # call a random subroutine

# SeqAlu(self._reg_pool).gen_seq, ## useless because of progsc_gen

# '\t' + '\t'.join(rm.sample(self._pr.progsc_body, rm.randrange(1, 3))), '\t' + rm.choice(self._pr.progsc_body),

'\t' + rm.choice(self._pr.progsc_body), '\t' + rm.choice(self._pr.progsc_body),

SeqLoop(self._pr, self._seq_number, self._pr.subroutine_pool).gen_seq, add_command + SeqExc.exc_call(self._pr.exc_pool) # call a random

exception with a probability ]

rm.shuffle(additional_seq)

seq = [ self._label.mark, "" .join(additional_seq),

SeqBranch(self._pr, (LabelSeq(self._seq_number + 1),

TEST_STOP_LABEL)[self._last_seq]).gen_seq, ]

return ""join(seq)

6. Класс SeqExcHandler

!! !! !!

This file creates a random exception handlers sequences. !! !! !!

class SeqExcHandler:

SEQ_NAME = "seq_exc_handler"

def_init_(self, program, seq_number):

......Create the exceptions handler

:param program: reference on Program object

:param seq_number: exceptions handler number for generating exceptions

handler label UNIQUE name !! !! !!

self._pr = program self._seq_number = seq_number self._label_start = LabelExcHandler(seq_number)

self._label_end = Label(self._label_start.label_name + "_end") # type: Label self._context = []

@property

def gen_handler(self): r_pool = self._pr.reg_pool exc_code_reg = r_pool.read_any reg = r_pool.read_any_other(exc_code_reg) pred = r_pool.get_any_predicate nop = NOP.apply()

label_reset = Label(self._label_start.label_name + "_reset")

# nested exceptions exc_code_list = [

UI_DEC_CODE, BA_DEC_CODE, SYSCALL_DEC_CODE, TRAP_DEC_CODE,

]

rm.shuffle(exc_code_list)

exc_code_list = rm.sample(exc_code_list, rm.randint(0, len(exc_code_list))) nst_exc_lbls = [Label("nested_exc_" + str(self._seq_number) + "_code_" + str(exc_code_list[i]))

for i in range(len(exc_code_list) - 1)]