Skip to content

Latest commit

 

History

History
84 lines (52 loc) · 13.3 KB

04_rgen.md

File metadata and controls

84 lines (52 loc) · 13.3 KB

Тема 04: RISC-V верификация: сравнение с эталонной моделью

Рекомендуемый материал

Краткое содержание

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

Описание подхода. Часть 1

При подходе, основанном на сравнении c эталонной моделью, используется программная модель процессорного ядра. В настоящее время сообщество RISC-V предоставляет большое количество моделей с открытым исходным кодом, написанных при помощи различных языков программирования, например: Spike, VeeR-ISS, Rust RISC-V Simulator, Pydgin.

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

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

Интерфейс RVFI

Интерфейс RVFI изначально был разработан компанией Symbiotic EDA с целью продвижения формального подхода к верификации RISC-V ядер. Интерфейс содержит набор сигналов, отражающих:

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

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

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

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

Описание подхода. Часть 2

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

Для каждого тестового сценария происходит сравнение лог-файлов процессора и эталонной модели. На основании совпадения или несовпадения формируется результат тестирования.

Для создания тестовых программ в данном подходе используются генераторы случайных инструкций. Благодаря сообществу RISC-V в настоящее время в открытом доступе существует достаточное количество генераторов с открытым исходным кодом и подробной документацией по применению, например RISCV-DV, MicroTESK, AAPG, FORCE-RISCV.

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

На рисунке выше представлена визуализация разбиения полей одного из типов RISC-V инструкций на разделы функционального покрытия (bins) и их пересечение1. В данном примере, например, интервал всех возможных значений поля funct7 разбивается на 64 подинтервала. Если в ходе симуляции выполняется инструкция конкретного типа и значение ее поля funct7 попадает в один из интервалов, а в этот интервал не было попаданий ранее во времени, то процент покрытия увеличивается на 1/64, то есть примерно на 1.6%. Функциональное покрытие инструкций позволяет верификатору убедиться, что все поля всех поддерживаемых ядром инструкций принимали все возможные значения.

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

У представленной методики существует ряд особенностей:

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

Практическое занятие на сравнение с эталонной моделью

Для того, чтобы на практике повторить тестирование процессора при помощи подхода со сравнением с эталонной моделью, перейдите в раздел practice/02_aapg и следуйте инструкциям. Будет интересно!

To be continued...

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

Footnotes

  1. Для ознакомления с функциональным покрытием в SystemVerilog рекомендуется ознакомится с лекцией автора в Школе синтеза цифровых схем: Условия завершения верификации. Модель функционального покрытия