文件名称：sail:Sail架构定义语言
文件大小：25.8MB
文件格式：ZIP
更新时间：2024-06-01 04:27:31
StandardML
Sail ISA规范语言 概述 Sail是一种用于描述处理器的指令集体系结构（ISA）语义的语言。 Sail的目标是提供一种工程师友好的，类似于供应商伪代码的语言来描述指令语义。 它本质上是一阶命令式语言，但具有轻量级依赖类型的数字类型和位向量长度的键入，可使用Z3自动检查它们。 它已用于几篇论文，可从。 给定Sail定义后，该工具将对其进行类型检查并生成C和OCaml中的可执行仿真器，Isabelle，HOL4和Coq的定理证明者定义，以及与我们的和工具集成的并发语义定义。 这一切都在进行中，某些定理证明者的定义还不适用于更复杂的模型。 有关当前状态的描述，请参见最新论文和ARMv8.5-A模型。 该存储库包含Sail的实现，以及一些Sail规范和相关工具。 带有源代码的手册 （在） Sail源代码（在） 某些ISA模型的已生成Isabelle快照，在 用于生成Isabelle