← All repos

sail

Sail architecture definition language

GitHub
Browse cluster: OCaml Systems and Utilities →
6,627commits
89contributors
20languages

Tech stack & purpose

Sail is a language for defining instruction-set architecture (ISA) semantics—the formal specification of how processor machine instructions behave—developed by researchers at the University of Cambridge, University of Edinburgh, and other institutions. Given a Sail ISA specification, the toolchain can type-check it using the Z3 SMT solver, generate executable emulators in C or OCaml, produce documentation in LaTeX or AsciiDoc, create theorem-prover definitions in Coq, Isabelle, or HOL4, and support symbolic evaluation and concurrent testing through integration with tools like Isla. The language itself is a first-order imperative language with lightweight dependent typing for numeric types and bitvector lengths, and Sail specifications have been created for numerous processor architectures including Arm, RISC-V, MIPS, x86, IBM Power, and CHERI-extended variants of several of these.

Community & reference links

Languages

OCaml
43.1%
Sail
42.1%
Rocq Prover
4.7%
Lean
3.6%
C
2.9%
Isabelle
1.6%
Python
0.8%
Standard ML
0.5%
Shell
0.3%
Makefile
0.1%
Emacs Lisp
0.1%
SystemVerilog
0.1%
CSS
0.0%
TeX
0.0%
Dune
0.0%
Rust
0.0%
Vim Script
0.0%
Perl
0.0%
JavaScript
0.0%
C++
0.0%

Contributors (top 30 of 89)