The Sail ISA specification language

Overview

Sail is a language for defining the instruction-set architecture (ISA) semantics of processors: the architectural specification of the behaviour of machine instructions. Sail is an engineer-friendly language, much like earlier vendor pseudocode, but more precisely defined and with tooling to support a wide range of use-cases. Given a Sail ISA specification, the tool can:

type-check it, to check e.g. that there are no unintended mismatches of bitvector lengths
generate documentation snippets, using either LaTeX or AsciiDoc, that can be included directly in ISA documents (see e.g. the CHERI ISAv9 spec from p176 for CHERI RISC-V, the CHERIoT spec from p91, and the Sail AsciiDoctor documentation for RISC-V)
generate executable emulators, in C or OCaml, that can be used as an authoritative reference in sequential-code testing and for early software bring-up
show specification coverage, of tests running in that generated C emulator
generate versions of the ISA in the form needed by relaxed memory model tools, isla-axiomatic and RMEM, to compute the allowed behaviour of concurrent litmus tests with respect to architectural relaxed memory models, as an authoritative reference for the concurrency behaviour
support automated instruction-sequence test generation from the specification in ways that get good specification coverage, using the Isla SMT-based symbolic evaluation engine for Sail
generate theorem-prover-definition versions of the ISA specification, in Coq, Isabelle, or HOL4, that support interactive proof in those systems, e.g. that the ISA satisfies intended security properties, such as our proofs for the Arm Morello ISA
(in progress) generate a reference ISA model in SystemVerilog, that can be used as a reference for hardware verification (e.g. using JasperGold)
support interactive proof about sequential binary code, integrating the Isla symbolic evaluator and the Iris program logic in Islaris.

(Not all of these are currently supported for all models - check the current status as needed.)

Sail overview

The language is essentially a first-order imperative language, but with lightweight dependent typing for numeric types and bitvector lengths, which are automatically checked using the Z3 SMT solver.

Sail ISA Models

Sail has been used for Arm-A, Morello (CHERI-Arm), RISC-V, CHERI-RISC-V, CHERIoT, x86, CHERI x86, MIPS, CHERI-MIPS, and IBM Power. In most cases these are full definitions (e.g. able to boot an OS in the Sail-generated emulator), but x86, CHERI x86 and IBM Power are core user-mode fragments, and the last is in an older legacy version of Sail.

Sail Arm-A (from ASL). These are complete ISA specifications for Armv9.4-A, Armv9.3-A, and Armv8.5-A, automatically translated from the Arm-internal ASL reference (as used in the Arm reference manual). They are provided under a BSD 3-Clause Clear license, by agreement with Arm. The older Sail Armv8.3-A model, the "public" model described in our POPL 2019 paper, is still available but is largely superseded. There is also an older handwritten Sail Armv8-A ISA model for a user-mode fragment.
Sail Morello (CHERI-Arm) (from ASL), for the Arm Morello CHERI-enabled prototype architecture. This is similarly automatically translated from the complete Arm-internal ASL definition. It was the basis for our Morello security proofs.
Sail RISC-V. This has been adopted by the RISC-V Foundation.
Sail CHERI RISC-V. This is the specification of the CHERI extensions to RISC-V, developed in the CHERI project.
Sail CHERIoT. This is the Microsoft specification of their CHERIoT ISA design for small embedded cores with CHERI protection.
Sail x86 (from ACL2). This is a version of the X86isa formal model of a substantial part of the x86 ISA in ACL2, by Shilpi Goel, Warren A. Hunt, Jr., and Matt Kaufmann, automatically translated into Sail.
Sail MIPS and CHERI-MIPS. These are specifications of MIPS and CHERI MIPS developed in the first realisation of the CHERI architecture extensions in the CHERI project.
Sail IBM POWER (from IBM XML). This is a specification for a user-mode fragment of the IBM Power ISA, semi-automatically translated from their documentation; it is currently in a legacy version of Sail.
Sail x86 (legacy). This is a handwritten user-mode fragment of x86, also in a legacy version of Sail.

Example

For example, below are excerpts from the Sail RISC-V specification defining the "ITYPE" instructions, for addition, subtraction, etc. First there is the assembly abstract syntax tree (AST) clause for the ITYPE instructions, that are parameterised on a 12-bit immediate value, the source and destination register IDs, and the integer operation:

union clause ast = ITYPE : (bits(12), regbits, regbits, iop)

then the definition of the encode/decode functions between 32-bit opcodes and the AST for these instructions: an ITYPE with immediate imm, source register rs1, destination register rd, and operation op is encoded as the bitvector concatenation on the right.

mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011

Finally the execution semantics for the ITYPE instructions defines how they behave in terms of architectural register reads and writes. This uses local immutable variables for clarity, e.g. immext is the sign-extended immediate value, of type xlenbits, which is a synonym for xlen-wide bitvectors.

function clause execute (ITYPE (imm, rs1, rd, op)) = {
  let rs1_val = X(rs1);                      // read the source register rs1
  let immext : xlenbits = EXTS(imm);         // sign-extend the immediate argument imm
  let result : xlenbits = match op {         // compute the result, case-splitting on op
    RISCV_ADDI  => rs1_val + immext,         // ...for ADDI, do a bitvector addition
    RISCV_SLTI  => EXTZ(rs1_val <_s immext), // ...etc
    RISCV_SLTIU => EXTZ(rs1_val <_u immext),
    RISCV_ANDI  => rs1_val & immext,
    RISCV_ORI   => rs1_val | immext,
    RISCV_XORI  => rs1_val ^ immext
  };
  X(rd) = result;                            // write the result to the destination register
  true                                       // successful termination
}

This repository

This repository contains the implementation of Sail, together with some Sail specifications and related tools.

A manual, doc/manual.html with source (in doc/), currently available online here
The Sail source code (in src/)
Generated Isabelle snapshots of some ISA models, in snapshots/isabelle
Documentation for generating Isabelle and working with the ISA specs in Isabelle in lib/isabelle/manual.pdf
Simple emacs and VSCode modes with syntax highlighting (in editors/)
A test suite for Sail (in test/)

The support library for Coq models is in a separate repository to help our package management.

Installation

See INSTALL.md for how to install Sail using opam.

Editor support

Emacs Mode editors/sail-mode.el contains an Emacs mode for the most recent version of Sail which provides some basic syntax highlighting.

VSCode Mode editors/vscode contains a Visual Studio Code mode which provides some basic syntax highlighting. It is also available on the VSCode Marketplace.

CLion/PyCharm Syntax highlighting editors/vscode/sail contains a Visual Studio Code mode which provides some

Sail

Install / Use

README