Р. А. Баратов, к ф. м н. А. С. Камкин, В. М. Майорова, А. Н. Мешков, А. А. Сортов, М. А. Якушева

Р.А. Баратов, к.ф.-м.н. А.С. Камкин, В.М. Майорова, А.Н. Мешков, А.А. Сортов,
М.А. Якушева (ЗАО «МЦСТ», Институт системного программирования РАН)
R.A. Baratov, A.S. Kamkin, V.M. Mayorova, A.N. Meshkov, A.A. Sortov, M.A. Yakusheva
ТРУДНОСТИ МОДУЛЬНОЙ ВЕРИФИКАЦИИ АППАРАТУРЫ НА ПРИМЕРЕ БУФЕРА КОМАНД МИКРОПРОЦЕССОРА «ЭЛЬБРУС-2S»
DIFFICULTIES OF THE UNIT-LEVEL HARDWARE VERIFICATION ON THE EXAMPLE OF THE INSTRUCTION BUFFER OF THE ELBRUS-2S MICROPROCESSOR
Описывается опыт автономной верификации буфера команд микропроцессора «Эльбрус-2S» с использованием инструмента C++TESK. На этом примере формулируются общие проблемы, возникающие в промышленной верификации аппаратуры, и предлагаются пути их решения. Дается краткое описание буфера команд и его особенностей, затрудняющих верификацию. Рассматриваются применяемые в проекте технические и организационные решения. Многие из затронутых проблем имеют общий характер, что позволяет применять предложенные решения для верификации других устройств.

Ключевые слова: моделирование цифровой аппаратуры, функциональная верификация, тестирование на основе моделей, обратная инженерия.
The experience of standalone verification of the instruction buffer of the Elbrus-2S microprocessor with the C++TESK tool is described. Basing on it, general problems of the industrial hardware verification are identified, and ways to solve them are suggested. A brief description of the instruction buffer and its features that complicate verification is given. Technical and organizational solutions having been applied in the project are discussed. The generality of the problems under consideration allows using the suggested solutions for verifying other devices.

Keywords: Hardware Modeling, Functional Verification, Model-Based Testing, Reverse Engineering.
Введение

Обеспечение корректности работы микропроцессоров и другой аппаратуры является фундаментальной проблемой, для решения которой применяют разные методы функциональной верификации [1, 2]. Суть проблемы состоит в том, что сложность микропроцессоров возрастает быстрее, чем позволяют возможности методов верификации, в результате чего проверка корректности (и так являющаяся самым узким местом процесса проектирования) требует все больше ресурсов. Чтобы повысить эффективность верификации, применяют проверенный принцип «разделяй и властвуй»: микропроцессор декомпозируется на множество относительно простых модулей (устройств), каждый из которых проверяется автономно. Таким образом, помимо обязательной системной верификации, оценивающей работоспособность микропроцессора в целом, применяют еще и модульную верификацию для более тщательной проверки отдельных устройств.

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

В процессе разработки микропроцессора «Эльбрус-2S» применялись оба типа верификации. Статья основана на опыте автономной верификации буфера команд, одного из наиболее критичных компонентов микропроцессора. На наш взгляд, этот опыт показателен: сложное устройство (более 25 000 строк кода на языке Verilog) документировано не достаточно полно. Мы полагаем, что опыт окажется полезным при верификации других устройств и будет способствовать общему повышению качества проектирования аппаратуры.

1. Организация буфера команд

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

Память команд позволяет хранить 512 строк кода размером по 256 байтов. В целях оптимизации она разделена на 8 независимо работающих банков, каждый из которых содержит 512 блоков размером по 32 байта. Память тегов используется для проверки наличия кода в памяти команд и, если код там присутствует, получения адреса, по которому его можно считать. Память тегов представляет собой четырехассоциативный кэш для хранения 512 тегов (ассоциативных признаков, сформированных по виртуальным адресам), разделенный на две независимые части – для четных и нечетных строк. Буфер трансляции адресов отвечает за преобразование виртуальных адресов в физические. Он поддерживает два типа страниц: размером 4 Кбайт (для которых используется четырехассоциативный кэш на 256 позиций) и 2 Мбайт (для которых используется полностью ассоциативный кэш на 8 позиций).

Конвейер буфера команд состоит из четырех стадий (L-A-F0-F1). На стадии L заполняются входные регистры устройства и формируются запросы в буфер трансляции адресов и память тегов (одновременно могут выдаваться четыре запроса – два со стороны основной ветви для четных и нечетных строк и два со стороны ветвей потенциальных переходов.

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

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

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

непоследовательная передача управления между стадиями конвейера. Несмотря на то что в буфере команд всего четыре стадии, поток управления достаточно сложен из-за наличия обходных путей (bypasses) и разнообразных оптимизаций;
нетривиальные зависимости между одновременно выполняемыми процессами обработки запросов: обработка одного запроса может повлиять на обработку другого, в частности, возможна отмена обработки ранее поданного запроса;
использование нестандартных алгоритмов арбитража запросов и вытеснения данных в буферах. Например, для вытеснения в памяти тегов и буфере трансляции адресов применяются две различные модификации алгоритма MPLRU;
большое число ограничений по времени на последовательность запросов (через N тактов после установки сигнала A должен быть установлен входной сигнал B; нельзя устанавливать сигнал С до тех пор, пока не наступит событие D, и т.п.).

2. Используемый подход к верификации

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

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

Сейчас существует несколько методологий создания тестовых систем, включая UVM (Universal Verification Methodology) [4], Incisive Enterprise Specman Elite Testbench [5] и др. В нашей работе использовался инструмент C++TESK, разработанный в Институте системного программирования РАН [6], что было вызвано следующими причинами:

подход к моделированию аппаратуры, принятый в ЗАО «МЦСТ», основывается на языке C++, т.е. на том же языке, который используется в C++TESK для разработки тестовых систем;
в инструменте C++TESK имеются развитые средства построения тестов (рандомизированная генерация стимулов и генерация тестовой последовательности на основе обхода графа состояний устройства) и средства автоматического распараллеливания процесса тестирования на компьютерных кластерах.

Созданная эталонная модель описывает функции буфера команд в терминах выдачи и обработки сообщений. В ее интерфейсе входные и выходные сигналы, объявленные в RTL-описании, разбиты на логически связанные группы, сигналы в которых всегда устанавливаются вместе (одновременно или, в общем случае, с заранее известными задержками друг относительно друга). Для каждой группы входных сигналов в модели отводится интерфейсная функция, принимающая на вход сообщение соответствующего типа; сигналы на выходе выдаются через callback-функцию, вызываемую при формировании модельной реакции. Основные компоненты модели (классы, соответствующие функциональным модулям буфера команд, в целом 20 000 строк кода) взяты без изменений из симулятора микропроцессора «Эльбрус-2S». Наиболее сложная часть проекта (около 10 000 строк кода) заключалась в моделировании конвейера буфера команд, без чего адекватная проверка его поведения не представлялась возможной.

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

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

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

Р
ис. 1. Архитектура тестовой системы
Описание тестов осуществляется в тестовых сценариях, на основе которых инструмент генерирует стимулы и «на лету» подает их как на RTL-модель через адаптер, так и на эталон через модельное окружение. Интерпретация тестовых сценариев и генерация конкретных тестовых последовательностей осуществляются обходчиками – библиотечными компонентами инструмента. Для верификации буфера команд в основном использовалась рандомизированная генерация тестов. Было выделено около 50 параметров, позволяющих задавать вероятности определенных событий (переход на границу страницы, вход в обработчик прерывания и т.п.) и их характеристики (длительность блокировки конвейера, число итераций при повторном выполнении инструкции и т.п.).
3. Организация процесса верификации

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

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

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

Ввиду неполноты имеющихся спецификаций самая трудная часть верификации буфера команд была связана с созданием эталонной модели. Требования к устройству считаются полными, если с их помощью всегда можно сказать, каким – корректным или ошибочным – является поведение устройства. (Заметим, что полнота требований вовсе не означает, что они с потактовой точностью описывают поведение устройства.) Из-за неполноты описания часто (всего более 600 раз) возникали спорные ситуации, когда поведение устройства нельзя было точно классифицировать как корректное или ошибочное. Анализ каждой из них занимал несколько часов, а последующие исправления эталонной модели – до двух недель. Наличие большого числа итераций при уточнении требований к буферу команд привело к тому, что некоторые фундаментальные свойства устройства были выявлены более чем через полгода после начала верификации.

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

Процесс прогона тестов был организован следующим образом. На основе параметров, управляющих генерацией стимулов, были описаны 13 конфигураций тестовой системы с постепенным возрастанием сложности генерируемых воздействий. Перед запуском тестов задавалось ограничение на длительность тестирования в каждой конфигурации (в тактах работы устройства); после прогона фиксировались все обнаруженные расхождения; из двух расхождений больший приоритет получало то, которое было найдено на конфигурации с меньшим номером, т.е. в более простой ситуации. Для каждого запуска измерялся уровень покрытия кода RTL-модели. По мере выполнения работ длительность тестирования постепенно увеличивалась – от 10⁴ до 10⁷ тактов в каждой конфигурации. Для сокращения времени прогона тестов процесс распараллеливался на несколько компьютеров.

4. Статистические данные по верификации буфера команд

На рис. 2 представлены графики, отражающие динамику изменения тестового покрытия кода RTL-модели: верхний график соответствует покрытию строк кода, нижний – покрытию ветвлений. Итоговое покрытие строк кода составило около 95%, покрытие ветвлений – около 90%. В результате инспекции непокрытого кода были выявлены две ошибки. Резкие провалы кривых в конце мая – начале июня вызваны глубокими модификациями эталонной модели, проводимыми в это время.

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

Рис. 2. Динамика изменения уровня тестового покрытия

Рис. 3. Динамика обнаружения ошибок
5. Выводы и рекомендации по итогам проекта

Проблем, связанных с неполнотой документации и большим числом итераций, требуемых для ее уточнения, можно было избежать, если бы специалисты по моделированию и верификации с самого начала вовлекались в процесс проектирования. Перед созданием RTL-модели должно проводиться поведенческое моделирование с использованием языков высокого уровня: универсальных (C, C++) или специализированных (EXPRESSION [7], xMAS [8]). Поведенческие модели и выявленные с их помощью требования имеют огромную ценность и для проектирования устройства, и для его верификации.

Большую трудность вызвали оценка трудоемкости верификации и прогнозирование сроков окончания работ. При наличии единых стандартов качества документации трудоемкость верификации можно достаточно точно оценить по объему кода RTL-модели, однако, если адекватность и полнота документации сильно варьируются, точность прогноза будет невысокой. Частично эти проблемы можно решить путем введения общих правил составления и оформления документации, предполагающих, в частности, применение в ключевых местах аппаратуры стандартных или хорошо специфицированных алгоритмов, а также наличие библиотеки эталонных моделей для типовых узлов, входящих в модели более сложных устройств. Подобный подход позволяет повысить качество и продуктивность разработки за счет повторного использования имеющихся наработок [9].

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

автоматическую группировку сигналов RTL-модели в интерфейсы и автоматическое построение адаптеров;
автоматическую генерацию структурных тестов, нацеленных на покрытие заданных участков кода RTL-модели, и автоматическое обнаружение «мертвого» кода;
автоматический анализ ошибочного поведения RTL-модели на основе модели типичных ошибок;
автоматическую генерацию тестовых последовательностей, сочетающих методы обхода графов состояний и методы рандомизированной генерации (в инструменте C++TESK поддерживаются оба класса методов, однако промежуточные варианты отсутствуют);
автоматическое построение тестовых последовательностей для сокращенного воспроизведения ошибок.

Заключение

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

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

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

Литература

1. W.K. Lam. Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall, 2005.

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

3. А.К. Ким, В.И. Перекатов, С.Г. Ермаков. Микропроцессоры и вычислительные комплексы семейства «Эльбрус». – СПб.: Питер, 2013. 272 с.

4. http://www.uvmworld.org.

5. http://www.cadence.com/products/fv/enterprise_specman_elite.

6. http://forge.ispras.ru/projects/cpptesk-toolkit.

7. http://www.ics.uci.edu/~express.

8. S. Chatterjee, M. Kishinevsky, U. Ogras. xMAS: Quick Formal Modeling of Communication Fabrics to Enable Verification. IEEE Design & Test of Computers, June 2011.

9. M.F. Jacome, H.P. Peixoto. A Survey of Digital Design Reuse. IEEE Design & Test of Computers, 18(3), May 2001.

10. R. Bate, et al. Systems Engineering Capability Maturity Model, Version 1.1. Software Engineering Institute, Carnegie Mellon University, November 1995.

11. В.В. Кулямин, Н.В. Пакулин, О.Л. Петренко, А.А. Сортов, А.В. Хорошилов. Формализация требований на практике. Препринт 13, ИСП РАН, Москва, 2006.

12. G. Perry. Requirements Management is Essential for Today’s Complex Electronics Systems. Chip Design Magazine.