该存储库包含用帆编写的RISC-V架构的正式规范。它已被RISC-V基金会采用。
该模型指定指令的汇编语言格式，相应的编码器和解码器以及指令语义。该模型的阅读指南在DOC/ SubDirectory中提供了有关如何扩展模型的指南。
可以从适合包含参考文档包含的模型中生成乳胶或ASCIIDOC定义。还有RISC-V的较新的Asciidoctor文档支持。
帆是一种描述处理器的说明集架构（ISA）语义的语言：机器指令行为的体系结构规范。 SAIL是一种对工程师友好的语言，就像早期的供应商伪代码一样，但更精确地定义并且具有支持广泛用例的工具。
鉴于帆规范，该工具可以键入检查，生成文档片段（在乳胶或asciidoc中），生成可执行模拟器，显示规范覆盖范围，生成ISA的版本，用于放松的存储器模型工具，支持自动化指令序列测试生成，为交互式证明（在Isabelle，hol4和coq中）生成定理 - 透明的定义，支持有关二进制代码（ISLARIS）的支持证明，并（在进行中）在SystemVerilog中生成一个可以用于正式硬件验证的SystemVerilog中的参考ISA模型。
SAIL用于多个ISA描述，包括ARM-A的顺序行为的完整版本（自动源自权威的ARM-内部规范，并在ARM许可的BSD透明许可下发布），RISC-V，cheri- RISC-V，Cheriot，Mips和Cheri-Mips；所有这些都足够完整，可以引导各种操作系统。还有用于IBM Power和X86较小片段的帆模型，包括自动翻译的ACL2 X86型号的版本。
安装帆。在Linux上，您可以下载二进制版本（强烈推荐），也可以使用OPAM从源安装。然后：
$ make
将在c_emulator/riscv_sim_RV64中构建模拟器。
如果您收到一条错误消息，说sail: unknown option '--require-version'.这是因为您的帆编译器太老了。您需要0.18版或更高版本。
可以通过在make线上指定ARCH=RV32或ARCH=RV64 ，并使用匹配目标后缀来构建RV32或RV64模型。 RV64默认构建，但可以使用以下方式构建RV32模型。
$ ARCH=RV32 make
在c_emulator/riscv_sim_RV32中创建模拟器。
MakeFile的目标是riscv_isa_build ， riscv_coq_build和riscv_hol_build调用相应的供体来处理定义并生成Isabelle模型，以生成generated_definitions/isabelle/RV64/Riscv.thy中的generated_definitions/coq/RV64/riscv.v /coq ferv 64分别在generated_definitions/hol4/RV64/riscvScript.sml中的模型。我们已经测试了Isabelle 2018，COQ 8.8.1和Hol4 Kananaskis-12。构建这些目标时，请确保帆名录中的相应供摊位库（ $SAIL_DIR/lib/$prover ）是最新的，并在这些目录中make 。
模拟器可用于执行小型测试二进制文件。
$ ./c_emulator/riscv_sim_<arch> <elf-file>
在测试/ riscv-tests测试中，包括RV32和RV64测试程序的RV32和RV64测试程序。可以使用test/run_tests.sh运行测试套件。
有关模拟器的配置选项的信息，可从./c_emulator/riscv_sim_<arch> -h获得。
一些有用的选项是：配置未对准的访问是否陷阱（ --enable-misaligned ），以及页面桌walks是否更新PTE位（ --enable-dirty-update ）。
有关启动操作系统图像，请参见OS-Boot/ SubDirectory下的信息。
很少有帆的发行版可能无法满足您的需求。如果您需要尚未发布的帆版本中的错误修复或新功能，或者您正在积极地驾驶帆，则可能会发生这种情况。在这种情况下，您可以告诉sail-riscv Makefile ，通过将SAIL_DIR设置在帆船仓库的根源上，以使用当地的make 。另外，您可以使用opam pin从帆仓库的本地结帐中安装帆，如帆安装说明中所述。
这些是来自包含基本说明的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"
该模型构建了一个可以执行RISC-V ELF文件的C模拟器，并且两个模拟器都提供了足以引导Linux，FreeBSD和SEL4的平台支持。 C模拟器可以与尖峰模拟器链接，用于执行，并通过指导串联验证。
对于Linux启动的C模拟器，目前在Intel I7-7700上以大约300 kips运行（当禁用详细的每个指导跟踪时），并且有很多机会进行未来的优化（帆MIPS模型以大约1 MIPS运行）。这使一个人可以在大约4分钟内引导Linux，并在大约2分钟内freeBSD。启动Linux时C模拟器的内存使用率约为140MB。
C模拟器目录中的文件实现ELF加载和平台设备，定义物理内存映射，并使用命令行选项选择特定于实现的ISA选择。
帆生成的C模拟器可以测量任何执行测试的规范分支覆盖范围，以每文件表显示结果，并以模型源的HTML宣布版本显示。
为了进行随机指令流的串联验证，工具支持Testrig中使用的协议直接将指令注入C模拟器并以RVFI格式生成跟踪信息。这已用于针对Spike和BluesPec SystemVerilog编写的RVBS规范进行交叉测试。
C仿真器也可以直接链接到Spike，该Spike提供了精灵二进制（包括OS靴子）的串联验证。当已知在Spike上工作时，这通常可用于调试模型中的操作系统启动问题。在ISA规范中未规定的SPIKE中检测特定于平台的实现选择也很有用。
ISA模型与RISC-V放松内存模型RVWMO的操作模型集成（如RISC-V用户级规范的附录中所述），该模型是RISC-V的开发中使用的参考模型之一。 -v并发架构；这是RMEM工具的一部分。它也与RISC-V公理并发模型集成在一起，作为ISLA轴工具的一部分。
作为剑桥大学/ Inria并发架构工作的一部分，这些群体生产并发布了大约7000个石蕊测试的库。这些测试的操作和公理RISC-V并发模型是同步的，而且它们与共同测试的相应ARM架构行为一致。
这些测试也已在RISC-V硬件上进行，这是在sifive RISC-V FU540多核心原始板上（自由释放），并从Impleas借来。迄今为止，在那里仅观察到依次一致的行为。
SAIL旨在支持多种工具跨多种工具的惯用定理私人定义的产生。目前，它支持Isabelle，Hol4和Coq，并且prover_snapshots目录提供了生成的定理鄙分定义的快照。
这些定理式翻译可以靶向多个单子出于不同的目的。第一个是一个具有非确定性和例外情况的状态单，适用于在连续环境中推理的情况，假设有效表达式在没有中断的情况下执行并独家访问状态。
为了推理并发性的推理，指令在投机上执行异常，并且在非原子上执行，因此在内存操作的效果数据类型上有一个免费的单调。通过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的Prashanth Mundkur撰写，并由其他人，特别是剑桥大学的研究人员撰写。
有关完整的作者列表，请参见LICENCE和GIT责任。
该软件是由以上在剑桥和爱丁堡大学的EPSRC Grant EP/K008528/1资助的主流系统（REMS）项目中开发的。
该软件是由SRI International和剑桥大学计算机实验室（计算机科学技术系）根据DARPA/AFRL合同FA8650-18-C-7809（“ CIFV”）开发的，根据DARPA合同HR0011-18-C-- 0016（“ ECAT”）作为DARPA SSITH研究计划的一部分。
该项目已从欧盟的Horizon 2020研究与创新计划（授予协议789108，Elver）获得了欧洲研究委员会（ERC）的资金。
