SAIL ISA规范语言

SAIL是一种用于描述处理器的指令集体系结构(ISA)语义的语言。SAIL的目标是提供一种工程师友好的、类似于供应商伪代码的语言来描述指令语义。它本质上是一种一阶强制语言，但是对于数值类型和位向量长度(使用Z3自动检查)具有轻量级依赖类型。它已用于多篇论文，可从http://www.cl.cam.ac.uk/~pes20/sail/.获得。

给定一个SAIL定义，该工具将对其进行类型检查，并生成C和OCaml的可执行仿真器、Isabelle、HOL4和Coq的定理证明器定义，以及与我们的RME和Isla-axiomatictools工具集成以实现并发语义的定义。这都是正在进行的工作，一些定理证明器的定义还不适用于更复杂的模型；有关当前状态的描述，请参阅最新的论文和ARMv8.5-A模型。

SAIL目前用于ARM、RISC-V、MIPS、CHERI-MIPS、IBM Power和x86型号，范围从完整定义到核心用户模式片段，并且可以在此处或单独的存储库中使用：

SAIL ARMv8.3-A ISA型号。这就是我们的POPL 2019年论文中描述的公共模式，现在基本上已经被上面的模式所取代。

手写的ARMv8-A、IBM POWER和x86模型目前与最新版本的Sail不同步，最新版本是(默认的)sail2分支Github。这些和RISC-V模型与我们用于并发语义的RMEM工具集成在一起。

SAIL 32位RISC-V型号，部分手写，部分生成。它目前实现了RV32IM的机器模式(-M)规范的一个片段。(独立于REMS项目的完整RISC-V型号开发。)。

请参见BUILDING.md，了解如何使用所有必需的依赖项从源构建Sail的完整详细信息。

Editor/sail-mode.el包含最新版本的Sail的Emacs模式，该模式提供了一些基本的语法突出显示。

编辑器/vscode包含一个Visual Studio代码模式，该模式提供一些基本的语法突出显示。它也可以在VSCode市场上买到。

Editor/vscode/sail包含一个Visual Studio Codemode，它提供了一些基本的语法突出显示。Clion/PyCharm还可以增强editors/vscode/sail/syntax/sail.tmLanguage.jsonfile并使用它来提供基本语法突出显示。要安装打开的首选项编辑器>；TextMate捆绑包，请执行以下操作。在该设置页面上，按+图标并找到Editor/vscode/saildirectory。

Src/中的SAIL实现，以及它在test/和lib/和language/中的其他支持文件中的测试，都是根据2条款BSD许可在这些文件的头部和src/license中分发的。

Aarch64/arecopyright arm Ltd中基于asl派生的ARMv8.3模型的生成部分。请参阅https://github.com/meriac/archex，和该目录中的自述文件。

在ARM/中手写的ARMv8模型在2条款BSD许可下在这些文件的标题中分发。

X86/中的x86模型按照2条款BSD许可在这些文件的标题中分发。

POWER/中的POWER模型根据2条款BSD许可在这些文件的标题中分发。

这项工作得到了EPSRC赠款EP/K008528/1REMS：主流系统的严格工程(ARM ICASE奖)和EPSRC IAA KTF基金的部分支持，该项目已获得欧洲研究理事会根据欧盟2020年地平线研究和创新计划(赠款协议编号789108)提供的资金。

批准公开发布；分发不受限制。这项研究由国防高级研究计划局(DARPA)和空军研究实验室(AFRL)赞助，合同为FA8750-10-C-0237(#34；CTSRD&34；)和FA8650-18-C-7809("；CIFV&34；)。这些文章或演示文稿中包含的观点、意见和/或结论是作者/演讲者的观点、观点和/或结论，不应解释为代表国防部或美国政府的官方观点或政策。