Sail architecture definition language
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
aarch64 Various changes: Dec 10, 2018
arm replaced NIA_LR/CTR/register with NIA_indirect; Feb 8, 2018
cheri Remove cheri and mips specs -- they now have their own repository. Sep 21, 2018
doc C: Add documentation for C compilation in manual.tex Sep 10, 2018
editors Add a test case for various simple boolean properties Dec 12, 2018
etc Added RISC-V fence.tso Dec 22, 2018
language Add separate termination_measure declarations Dec 29, 2018
lib Coq: the division used in smt.sail should be Euclidean Jan 9, 2019
mips Remove cheri and mips specs -- they now have their own repository. Sep 21, 2018
power Merge master branch into sail2 for OCaml 4.06 compatibility Feb 17, 2018
snapshots Update Coq snapshots Jan 9, 2019
src Add options for output directories for the lem and coq backends. Jan 15, 2019
test Coq: avoid putting ambiguous numeric literals in Coq output Dec 27, 2018
x86 replaced NIA_LR/CTR/register with NIA_indirect; Feb 8, 2018
.gitignore RISVC model is now at https://github.com/rems-project/sail-riscv . Re… Dec 20, 2018
.merlin Improvements to latex generation Nov 9, 2018
INSTALL.md Update install instructions. Nov 29, 2018
LICENCE Fix some links and be more clear about licensing May 11, 2018
Makefile RISVC model is now at https://github.com/rems-project/sail-riscv . Re… Dec 20, 2018
README.md update README Jan 13, 2019
descr Add a new SHARE_DIR argument to use when doing opam build. For non-op… Apr 26, 2018
manual.pdf Update manual snapshot Oct 15, 2018
opam Prepare for new release. Dec 14, 2018

README.md

The Sail ISA specification language

Overview

Sail is a language for describing the instruction-set architecture (ISA) semantics of processors. Sail aims to provide a engineer-friendly, vendor-pseudocode-like language for describing instruction semantics. It is essentially a first-order imperative language, but with lightweight dependent typing for numeric types and bitvector lengths, which are automatically checked using Z3. It has been used for several papers, available from http://www.cl.cam.ac.uk/~pes20/sail/.

Given a Sail definition, the tool will type-check it and generate executable emulators, in C and OCaml, theorem-prover definitions for Isabelle, HOL4, and Coq, and definitions to integrate with our RMEM tool for concurrency semantics. This is all work in progress, and some theorem-prover definitions do not yet work for the more complex models; see the most recent papers and the ARMv8.5-A model for descriptions of the current state.

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

Sail ISA Models

Sail is currently being used for ARM, RISC-V, MIPS, CHERI-MIPS, IBM Power, and x86 models, variously ranging from full definitions to core user-mode fragments, and either here or in separate repositories:

The hand-written ARMv8-A, IBM POWER, and x86 models are currently not in sync with the latest version of Sail, which is the (default) sail2 branch on Github. These and the RISC-V model are integrated with our RMEM tool for concurrency semantics.

OPAM Installation

See the following Sail wiki page for how to get pre-built binaries of Sail using OPAM.

Building

See INSTALL.md for full details of how to build Sail from source with all the required dependencies.

Emacs Mode

editors/sail2-mode.el contains an Emacs mode for the most recent version of Sail which provides some basic syntax highlighting. editors/sail-mode.el contains an emacs mode for previous versions of the language.

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, with the exception of the library src/pprint, which is distributed under the CeCILL-C free software licence in src/pprint/LICENSE.

The generated parts of the ASL-derived ARMv8.3 model in aarch64/ are copyright ARM Ltd. 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.