Как я пришел к формальной спецификации RISC-V процессора на F#

Томными зимними вечерами, когда солнце лениво пробегало сквозь пелену дней — я нашел в себе силы заняться реализацией давней мечты: разобраться как же устроены процессоры. Эта мечта привела меня к написанию формально спецификации RISC-V процессора. Проект на Github

Как это было

Подобное желание у меня появилось достаточно давно, когда 20 лет назад я стал заниматься первыми своими проектами. По большей части это были научные исследования, математическое моделирование в рамках курсовых работ и научных статей. Это были времена Pascal и Delphi. Однако уже тогда мой интерес привлек Haskell и функциональное программирование. Прошло время, менялись языки проектов и технологии в которые я был вовлечен. Но с тех пор красной нитью проходил интерес к функциональным языкам программирования, и ими стали: Haskell, Idris, Agda. Однако в последнее время мои проекты были на языке Rust. Более глубокое изучение его меня привело к изучение Embedded устройств.

От Rust к Embedded

Возможности Rust настолько широки, а community настолько активно, что Embedded разработка стала поддерживать широкий спектр устройств. И это был мой первый шаг в более низкоуровневое понимание процессоров.

Первой моей платой стало: STM32F407VET6. Это было погружение в мир микроконтроллеров, от которого я на тот момент был очень далек, и достаточно приблизительно понимал как происходит работа на низком уровне.

Постепенно сюда добавились платы esp32, ATmega328 (в лице платы Ukraino UNO). Погружение в stm32 оказалось достаточно болезненным — информация достаточно обильная и часто не та, которая мне нужна. И оказалось, что разработка, к примеру, на Assembler — достаточно рутинная и неблагодарная задача, с их подмножеством более 1000 инструкций. Однако Rust с этим справлялся бодро, хотя порой возникали трудности с интеграцией для конкретных китайских плат.

Архитектура AVR оказалась заметно проще и прозрачнее. Обильные мануалы мне дали достаточное понимание как работать с таким достаточно ограниченным набором инструкций, и тем не менее иметь возможность создавать очень интересные решения. Тем не менее путь Arduino меня совсем не радовал, но вот написание на Asm/C/Rust оказалось куда увлекательнее.

А где же RISC-V?

И в этот момент возникает логичный вопрос — а где же RISC-V CPU?
Именно минималистичность AVR и достаточная его документирование, меня вернуло к прежней мечте разобраться как же работает процессор. К этому времени у меня появилась FPGA плата и первые реализации для нее в виде взаимодействия с VGA устройствами, вывода графики, взаимодействия с периферией.

Моими проводниками в архитектуру процессоров стали книги:

• John L. Hennessy and David A. Patterson — Computer Architecture: A Quantitative Approach (The Morgan Kaufmann Series in Computer Architecture and Design)
• John L. Hennessy and David A. Patterson — Computer Organization and Design. The Hardware/Software Interface: RISC-V Edition
• Дэвид М. Хэррис и Сара Л. Хэррис — Цифровая схемотехника и архитектура компьютера
• The RISC-V Instruction Set Manual

Зачем это нужно

Казалось бы — уже все давно написано и реализовано.

• RISC-V Cores and SoC Overview
• RISC-V Formal Verification

разнообразные реализации на HDL, и языках программирония. Кстати достаточно интересная реализация RISC-V на Rust.

Однако что может быть интереснее, чем разобраться самому, и создать свое. Свой велосипед? Или внести свой вклад в велосипеда-строение? Кроме личного глубокого интереса у меня возникла идея — а как попробовать популяризировать, заинтересовать. И найти свою форму, свой подход. А это значит представить достаточно скучную документацию по RISC-V ISA в виде официальной спецификации в ином виде. И мне кажется путь формализации в этом смысле достаточно интересен.

Что я понимаю под формализацией? Достаточно обширное понятие. Представление определенного набора данных в формальном виде. В данном случае через описание структур и функционального описания. И в этом смысле функциональные языки программирования обладают своим очарованием. Также задача в том — чтобы человек который не сильно погружен в программирование мог прочитать код как спецификацию, по-возможности минимально вникая в специфику языка, на котором это описано.
Декларативный подход, так сказать. Есть высказывание, а как именно это работает — это уже не существенно. Главное читабельность, наглядность, и конечно же корректность. Соответствие формальных высказываний вкладываемому в них смыслу.

И того — мне действительно любопытно передать свой интерес другим. Есть некая иллюзия того — что интерес движущая сила к поступкам. Через что становится и проявляется индивидуальность. И в этом есть часть самореализации, воплощение творческого начала.
Амбициозно и немного лирики. Что же дальше?

Существующие реализации

Они есть и на данный момент их агрегирует проект: RISC-V Formal Verification.
Список формальных спецификаций (включая мою работу): https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md

Как видно — по большей части это формализации на языке Haskell. Это стало отправной идеей в выборе другого функционального языка. И мой выбор пал на F#.

Почему F#

Так случилось, что про F# мне известно давно, но все как-то в суете повседневности не имел возможности познакомиться ближе. Еще одним фактором была .NET платформа. Беря во внимание что я под Linux-ом, долгое время меня не устраивали IDE, и mono выглядело достаточно сырым. А возвращение в Windows только ради MS Visual Studio — достаточно сомнительная идея.

Однако время не стоит на месте, а звезды на небе не спешат меняться. Но к этому времени Jetbrains Rider — развился до полноценного и удобного инструмента, а .NET Core для Linux не приносит боль при одном взгляде на него.

Стал вопрос — какой функциональный язык выбрать. То что это должен быть именно функциональный язык — в несколько патетическом виде я аргументировал выше.
Haskell, Idris, Agda? F# — с ним я не знаком. Отличный повод узнать новые краски мира функциональных языков.

Да F# не чисто-функциональный. Но что мешает придерживаться "чистоты"? И тут оказалось — что F# документация достаточно подробная и целостная. Читабельная, и я бы даже сказал интересная.

Чем сейчас для меня стал F#? Достаточно гибким языком, с очень удобными IDE (Rider, Visual Studio). Вполне развитыми типами (хотя конечно до Idris очень далеко). И в целом достаточно милым с точки зрения читабельности. Однако как оказалось его функциональная "не чистота" — может приводить код к совершенно невменяемому виду как с точки зрения читабельности, так и логики. Анализ пакетов в Nugget это наглядно показывает.

Еще одной интересной и загадочной особенностью для меня стало открытие, что написать формализацию RISC-V ISA на F# ранее никого не интересовало (официально или в доступном для поиска виде). А это значит, что у меня есть шанс внести новую струю в это сообщество, язык, "экосистему".

Подводные камни, с которыми я столкнулся

Самой сложной частью оказалось реализация Execution flow. Часто оказывалось, что не до конца понятно как инструкция должна работать. К сожалению надежного товарища, которому можно было бы позвонить в 3 часа ночи и взволнованным голосом с придыханием спросить: "А знаешь, BLTU инструкция наверное по-другому signextend-иться..." — у меня нет. В этом смысле иметь квалифицированных товарищей, которые добрым словом, и уместным квалифицированным советом помогут — очень желанно.

Какие были трудности и подводные камни. Попробую тезисно:

• ELF — любопытной задачей стало разобраться как с ним работать, читать секции, инструкции. Скорее всего эта история в рамках текущего проекта не закончена.
• unsigned инструкции периодически меня приводили к ошибкам, которые я выявлял в процессе unit-тестирования
• реализация работы с памятью потребовала подумать над красивым и читабельными алгоритмами компановки байтов.
• годного пакета для работы с битами под int32, int64 не оказалось. Потребовалось время на написание своего пакета и на его тестирование.
  Здесь хочу отметить, что работа с битами в F# таки в разы удобнее чем в Haskell с его Data.Bits
• правильная поддержка битности регистров, с возможностью поддержки x32 и x64 одновременно. Невнимательность привела к тому, что я в некоторых местах использовал int64. Выявить это мне помогли unit-тесты. Но на это потребовалось время.
• простого, лаконичного, удобного лично мне CLI F# пакета я не нашел. Побочным эффектом стало написание минималистичного варианта в функциональном стиле
• на данный момент остается загадкой как правильно реализовать System Instructions: FENCE, ECALL, BREAK
• далеко не весь набор расширений (ISA extensions) из списка: [A, M, C, F, D] на данный момент очевидны. В особенности реализация [F,D] не через soft float.
• на данный момент ясного понимания Privileged Instructions, User Mod, работы с периферией — увы нет. И это путь исследований, проб и ошибок.
• нет черного пояса по написанию Assembler программ под RISC-V. Возможно далеко не часто в этом будет потребность, учитывая сколько языков уже портировано для написания под RISC-V.
• также существенным оказался фактор времени — его достаточно мало в водовороте основной работы, житейских потребностей и океана жизни вокруг. А работы достаточно много, и большая часть не столько в "кодировании" — написания самого кода, сколько в изучении, осваивания материалов.

Как это работает и какие возможности

Теперь пожалуй наиболее техническая часть. Какие возможности на данный момент:

• выполнение набора инструкций rv32i
• возможность выполнения как полноценной программы в качестве RISC-V симулятора — выполнения ELF-файлов.
• поддержка командной строки (CLI) — выбор выполняемой архитектуры, набора инструкций, исполняемых ELF-файлов, режима логирования, справки по командной строке.
• возможность вывода лога выполняемых инструкций, приближенной к objdump виде при дизассемблировании.
• возможность запуска тестов покрывающих весь реализованный набор инструкций.

Работа программы разделена на такие этапы и циклы:

• чтение командной строки
• чтение инструкций из ELF-файла
• чтение конкретной инструкции согласно текущему PC (Program Counter) — счетчику
• декодирование инструкции
• выполнение инструкции
• при наличии непредвиденных ситуаций расставлены ловушки (Trap), позволяющие завершить процесс выполнения, сигнализирующие о проблеме, и предоставляющие необходимые данные
• в случае если программа не в бесконечном цикле — вывод состояния регистров и завершение программы симулирования

Что входит в планы:

• Standard base 64i (почти завершено)
• Standard extension M (integer multiply/divide)
• Standard extension A (atomic memory ops)
• Standard extension C (Compressed 16-bit instructions)
• Standard extension F (Single-precision floating point)
• Standard extension D (Double-precision floating point* Privilege Level M (Machine)
• Privilege Level U (User)
• Privilege Level S (Supervisor)
• Virtual Memory schemes SV32, SV39 and SV48
• host программы
• GPIO — работа с периферией

Как запустить

Для того чтобы запустить программу необходимо наличие .NET Core. Если у вас не установлено, то к примеру, под Ubuntu 16.04 необходимо выполнить такой набор команд:

$ wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb
$ sudo dpkg -i packages-microsoft-prod.deb
$ sudo apt-get update
$ sudo apt-get install apt-transport-https
$ sudo apt-get update
$ sudo apt-get install dotnet-sdk-3.0

Чтобы проверить, что что-то в жизни изменилось — запустите:

$ dotnet --version

И жизнь должна заиграть новыми красками!

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

$ cd some/my/dev/dir
$ git clone https://github.com/mrLSD/riscv-fs
$ cd riscv-fs
$ dotnet build
$ dotnet run -- --help

и ваша консоль должна игриво подмигнуть вам справочным сообщением.
Запуск же:

$ dotnet run

Строгим тоном скажет — что нужны параметры. Поэтому запускаем:

$ dotnet run -- -A rv32i -v myapp.elf

Это тот самый неловкий момент, когда оказывается, что все-таки нам нужна уже готовая ready for execution программа под RISC-V. И тут есть мне чем вам помочь. Однако вам понадобиться GNU toolchain for RISC-V. Его установка пусть будет домашним заданием — в описании к репозиторию достаточно детально описано как это делать.

Далее, для получения заветного тестового ELF-файла, выполняем такие действия:

$ cd Tests/asm/
$ make build32

если у вас RISC-V toolchain есть в наличии то все должно пройти гладко. И файлики должны красоваться в директории:

$ ls Tests/asm/build/
add32  alu32  alui32  br32  j32  mem32  sys32  ui32

и теперь смело, без оглядки пробуем команду:

$ dotnet run -- -A rv32i -v Tests/asm/build/ui32

Важно отметить, что Tests/asm не является тестовыми программами, но их основная цель — это тестовые инструкции и их коды для написания тестов. Поэтому если вам что-то по душе более масштабное и героическое, то в вашей воле меняя мир — найти самостоятельно исполняемый 32-битный ELF файл с поддержкой только rv32i инструкций.

Однако набор инструкций и расширений будет пополняться, набирать обороты и приобретать вес.

Резюме и ссылки

Получилось немного патетическое, приправленное личной историей повествование. Временами техническое, порой субъективное. Однако воодушевленное и с легким налетом энтузиазма.

С моей же стороны мне интересно от вас услышать: отзывы, впечатления, добрые напутствия. А для самых смелых — помощь в поддержании проекта.

Интересен ли вам такой формат повествования и хотели бы вы продолжений?

• сам проект
• список RISC-V формальных спецификаций (включая мой проект)
• RISC-V specifications
• RISC-V toolchain
• Awesome F# (мой проект также включен)
• Ariane — a 6-stage RISC-V CPU based on Verilog

Автор: sfxws2006

Источник