Этот репозиторий содержит формальную спецификацию архитектуры RISC-V, написанную в парусе. Он был принят Фондом RISC-V.
Модель определяет форматы языка сборки инструкций, соответствующие кодеры и декодеры, а также семантику инструкций. Руководство по чтению модели приведено в DOC/ Subercectory, а также руководство по расширению модели.
Определения латекса или Asciidoc могут быть получены из модели, которая подходит для включения в справочную документацию. Существует также более новая поддержка документации Asciidoctor Sail для RISC-V.
SAIL-это язык для описания семантики процессоров с архитектурой инструкций (ISA): архитектурная спецификация поведения машинных инструкций. SAIL-это дружелюбный язык, очень похожий на более ранний псевдокод поставщика, но более точно определяемый и с инструментами для поддержки широкого спектра использования.
Учитывая спецификацию SAIL, инструмент может проверить его, генерировать фрагменты документации (в латексном или Asciidoc), генерировать исполняемые эмуляторы, показать охват спецификации, генерировать версии ISA для инструментов модели с расслабленной памятью, поддержки автоматизированной тест-последовательности Создайте определения теоремы для интерактивного доказательства (в Isabelle, Hol4 и CoQ), подтверждение поддержки о двоичном коде (в Islaris) и (в процессе) генерируют эталонную модель ISA в SystemVerilog, которую можно использовать для формальной проверки оборудования.
Парус используется для нескольких описаний ISA, в том числе по существу полных версий последовательного поведения ARM-A (автоматически полученное из авторитетной индивидуальной спецификации и выпускается по четкой лицензии BSD с разрешения ARM), RISC-V, Cheri- RISC-V, хериот, MIPS и Cheri-Mips; Все они достаточно полны, чтобы загрузить различные операционные системы. Существуют также парусные модели для небольших фрагментов IBM Power и X86, включая версию модели ACL2 X86, автоматически переведенную из этого.
Установить парус. На Linux вы можете скачать двоичный релиз (настоятельно рекомендуется), или вы можете установить из источника с помощью Opam. Затем:
$ make
Будет построить симулятор в c_emulator/riscv_sim_RV64 .
Если вы получите сообщение об ошибке, в котором говорится sail: unknown option '--require-version'. Это потому, что ваш парусник слишком стар. Вам нужна версия 0,18 или более поздней версии.
Можно построить либо модель RV32, либо RV64, указав ARCH=RV32 или ARCH=RV64 на линии make и, используя соответствующий целевой суффикс. RV64 строится по умолчанию, но модель RV32 может быть построена с помощью:
$ ARCH=RV32 make
который создает симулятор в c_emulator/riscv_sim_RV32 .
Makefile Targets riscv_isa_build , riscv_coq_build и riscv_hol_build вызывают соответствующий повернут для обработки определений и создания модели Исабель в generated_definitions/isabelle/RV64/Riscv.thy , модель COQ в generated_definitions/coq/RV64/riscv.v RV64/rscv. Модель в generated_definitions/hol4/RV64/riscvScript.sml соответственно. Мы протестировали Isabelle 2018, COQ 8.8.1 и HOL4 Kananaskis-12. При создании этих целей, пожалуйста, убедитесь, что соответствующие библиотеки Prover в каталоге SAIL ( $SAIL_DIR/lib/$prover ) были в курсе и построены, например, make в этих каталогах.
Симулятор может использоваться для выполнения небольших тестовых двоичных файлов.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
Набор программ тестовых программ RV32 и RV64, полученных из тестирования riscv-tests , включен в тестирование/RISCV-тесты/. Теста можно запустить с помощью test/run_tests.sh .
Информация об параметрах конфигурации для симулятора доступна от ./c_emulator/riscv_sim_<arch> -h .
Некоторые полезные параметры: настройка того, является ли разветвленная ловушка Accesses ( --enable-misaligned ) и обновление PTE PAGE TABLE WALKS ( --enable-dirty-update ).
Для загрузки изображений операционной системы см. Информацию в рамках OS-Boot/ Subercectory.
Редко, выпускная версия SAIL может не удовлетворить ваши потребности. Это может произойти, если вам нужно исправление ошибки или новая функция, которая еще не в выпущенной версии Sail, или вы активно работаете над парусом. В этом случае вы можете указать Makefile sail-riscv использовать локальную копию SAIL, установив SAIL_DIR в корень оформления репо паруса, когда вы вызываете make . В качестве альтернативы, вы можете использовать opam pin для установки паруса с локальной проверки Sail Repo, как описано в инструкциях по установке SAIL.
Это дословные выдержки из модельного файла, содержащего базовые инструкции, RISCV_INSTS_BASE.SAIL, с несколькими комментариями добавлены.
/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */
union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
/* the encode/decode mapping between AST elements and 32-bit words */
mapping encdec_iop : iop <-> bits(3) = {
RISCV_ADDI <-> 0b000,
RISCV_SLTI <-> 0b010,
RISCV_SLTIU <-> 0b011,
RISCV_ANDI <-> 0b111,
RISCV_ORI <-> 0b110,
RISCV_XORI <-> 0b100
}
mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
/* the execution semantics for the ITYPE instructions */
function clause execute (ITYPE (imm, rs1, rd, op)) = {
let rs1_val = X(rs1);
let immext : xlenbits = sign_extend(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
};
X(rd) = result;
RETIRE_SUCCESS
}
/* the assembly/disassembly mapping between AST elements and strings */
mapping itype_mnemonic : iop <-> string = {
RISCV_ADDI <-> "addi",
RISCV_SLTI <-> "slti",
RISCV_SLTIU <-> "sltiu",
RISCV_XORI <-> "xori",
RISCV_ORI <-> "ori",
RISCV_ANDI <-> "andi"
}
mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
union clause ast = SRET : unit
mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute SRET() = {
let sret_illegal : bool = match cur_privilege {
User => true,
Supervisor => not(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
Machine => not(extensionEnabled(Ext_S))
};
if sret_illegal
then { handle_illegal(); RETIRE_FAIL }
else if not(ext_check_xret_priv (Supervisor))
then { ext_fail_xret_priv(); RETIRE_FAIL }
else {
set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_SUCCESS
}
}
mapping clause assembly = SRET() <-> "sret"
Модель создает эмулятор C, который может выполнять файлы RISC-V ELF, и оба эмулятора обеспечивают поддержку платформы, достаточную для загрузки Linux, FreeBSD и SEL4. Эмулятор C может быть связан с эмулятором Spike для выполнения с помощью тандемной проверки для внедрения.
Эмулятор C, для загрузки Linux, в настоящее время работает примерно на 300 п. ) Это позволяет загружать Linux примерно через 4 минуты, а Freebsd - примерно через 2 минуты. Использование памяти для эмулятора C при загрузке Linux составляет приблизительно 140 МБ.
Файлы в каталоге C-эмулятора реализуют загрузку ELF и устройства платформы, определяют карту физической памяти и используют параметры командной строки для выбора специфического для реализации вариантов ISA.
Сгенерированный парусным эмулятором C может измерять охват спецификации ветвей любых выполненных тестов, отображая результаты в виде таблиц для файлов и в виде HTML-версий источника модели.
Для проверки тандемных потоков инструкций инструменты поддерживают протоколы, используемые в Testrig для непосредственного ввода инструкций в эмулятор C и создавать трассировку в формате RVFI. Это было использовано для перекрестного тестирования против Спайка и спецификации RVBS, написанной в Bluespec SystemVerilog.
Эмулятор C также может быть непосредственно связан с Spike, который обеспечивает проверку тандем на двоичных файлах ELF (включая ботинки ОС). Это часто полезно при отладке проблем с загрузкой ОС в модели, когда станет известна, работая над Spike. Также полезно обнаружить выбор реализации, специфичный для платформы в Spike, которые не предписываются спецификацией ISA.
Модель ISA интегрирована с оперативной моделью модели RISC-V смягченной памяти RVWMO (как описано в приложении спецификации пользовательского уровня RISC-V), которая является одной из контрольных моделей, используемых при разработке RISC -V Архитектура параллелизма; Это часть инструмента RMEM. Он также интегрирован с моделью аксиоматической параллелизма RISC-V как часть оси ISLA-оси.
В рамках архитектурной работы по параллелизму Кембриджского университета/ INRIA эти группы произвели и выпустили библиотеку с приблизительно 7000 лакмусовых тестов. Операционные и аксиоматические модели параллелизма RISC-V находятся в синхронизации для этих тестов, и они, кроме того, согласны с соответствующим архитективным поведением ARM для общих тестов.
Эти тесты также проводились на оборудовании RISC-V на многоядерном протосовом совете Sifive RISC-V FU540 (Freedom Deleashed), любезно по ссуде от Imperas. На сегодняшний день там наблюдалось только последовательное поведение.
SAIL стремится поддержать генерацию идиоматических определений пошлин теоремы в нескольких инструментах. В настоящее время он поддерживает Isabelle, HOL4 и COQ, а в каталоге prover_snapshots предоставляется снимки сгенерированных определений ProVerme.
Эти переводы по производству теорема могут нацелиться на несколько монадов для разных целей. Первое - это государственная монада с нетерминизмом и исключениями, подходящим для рассуждения в последовательных условиях, предполагая, что эффективные выражения выполняются без перерывов и с исключительным доступом к государству.
Для рассуждения о параллелизме, где инструкции выполняют вне порядка, спекулятивно и неатомически, существует бесплатная монада на эффект данных действий памяти. Эта монада также используется как часть вышеупомянутой поддержки параллелизма с помощью инструмента RMEM.
Файлы в разделе handwritten_support предоставляют определения библиотеки для Coq, Isabelle и Hol4.
sail-riscv
- model // Sail specification modules
- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories
- c
- lem
- isabelle
- coq
- hol4
- latex
- prover_snapshots // snapshots of generated theorem prover definitions
- handwritten_support // prover support files
- c_emulator // supporting platform files for C emulator
- doc // documentation, including a reading guide
- test // test files
- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
- os-boot // information and sample files for booting OS images
Модель предоставляется доступной по лицензии BSD с двумя направлениями в лицензии.
Первоначально написанный Прашант Мундкур в SRI International и дополнительно разработал другие, особенно исследователи из Кембриджского университета.
Смотрите LICENCE и вину Git для полного списка авторов.
Это программное обеспечение было разработано в рамках вышеупомянутого проекта по строгому проектированию основных систем (REMS), частично финансируемого грантом EPSRC EP/K008528/1, в университетах Кембриджа и Эдинбурга.
Это программное обеспечение было разработано SRI International и Кембриджской компьютерной лабораторией (Департамент компьютерных наук и техники) в соответствии с DARPA/AFRL Contract FA8650-18-C-7809 («CIFV») и согласно контракту DARPA HR0011-18-C- 0016 ("eCats") как часть исследовательской программы DARPA SSITH.
Этот проект получил финансирование от Европейского исследовательского совета (ERC) в рамках Программы исследований и инноваций Европейского Союза Horizon 2020 (грант 789108, Elver).
