search

rems-project / sail

Sail architecture definition language
Other
622 stars 116 forks source link

readme

Sail logo

The Sail ISA specification language

Build and Test

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:

(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.

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.

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 basic syntax highlighting. CLion/PyCharm can also parse the editors/vscode/sail/syntax/sail.tmLanguage.json file and use it to provide basic syntax highlighting. To install open Preferences > Editor > TextMate Bundles. On that settings page press the + icon and locate the editors/vscode/sail directory. This requires the TextMate Bundles plugin.

Vim editors/vim contains support for syntax highlighting in the vim editor, in vim's usual format of an ftdetect directory to detect Sail files and a syntax directory to provide the actual syntax highlighting.<

Logo

etc/logo contains the Sail logo (thanks to Jean Pichon, CC0) )

Licensing

The Sail implementation, in src/, as well as its tests in test/ and other supporting files in lib/ and language/, is distributed under the 2-clause BSD licence in the headers of those files and in src/LICENCE.

The generated parts of the ASL-derived Arm-A and Morello models are copyright Arm Ltd, and distributed under a BSD Clear licence. See https://github.com/meriac/archex, and the README file in that directory.

The hand-written Armv8 model, in arm/, is distributed under the 2-clause BSD licence in the headers of those files.

The x86 model in x86/ is distributed under the 2-clause BSD licence in the headers of those files.

The POWER model in power/ is distributed under the 2-clause BSD licence in the headers of those files.

The models in separate repositories are licensed as described in each.

People

Sail itself is developed by

and previously:

Many others have worked on specific Sail models, including in the CHERI team, in the RISC-V community, and in the CHERIoT team.

Papers

The best starting point is the POPL 2019 paper.

Funding

This work was partially supported by the UK Government Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694). This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No 789108, ELVER). This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous Engineering for Mainstream Systems, an ARM iCASE award, and EPSRC IAA KTF funding. This work was partially supported by donations from Arm and Google. The Sail AsciiDoc backend was supported by RISC-V International. Approved for public release; distribution is unlimited. This research is sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 ("CTSRD") and FA8650-18-C-7809 ("CIFV"). The views, opinions, and/or findings contained in these articles OR presentations are those of the author(s)/presenter(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.