該存儲庫包含用帆編寫的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用戶級規範的附錄），該模型是用於開發RISC的參考模型之一。 -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）的資金。
