From af5e6e4d11d9df0bd2058ef3cc5b69d877c001ef Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Sun, 13 Jan 2019 09:19:35 +0000 Subject: update README with current model repos --- README.md | 49 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 32 insertions(+), 17 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index f1d9aeed..8917de6a 100644 --- a/README.md +++ b/README.md @@ -4,13 +4,14 @@ The Sail ISA specification language Overview ======== -Sail is a language for describing the instruction semantics of -processors. Sail aims to provide a engineer-friendly, -vendor-pseudocode-like language for describing instruction -semantics. It is an imperative language containing some advanced -features like 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/ +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 +. This repository contains the implementation of Sail, together with some Sail specifications and related tools. @@ -19,10 +20,7 @@ some Sail specifications and related tools. * The Sail source code (in [src/](src/)) -* A Sail specification of ARMv8.3-A generated from ARM's publically - released ASL specification (in [aarch64/](aarch64/)) - -* Generated Isabelle snapshots of the above ISAs in [snapshots/isabelle](snapshots/isabelle) +* Generated Isabelle snapshots of some ISA models, in [snapshots/isabelle](snapshots/isabelle) * Documentation for generating Isabelle and working with the ISA specs in Isabelle in [snapshots/isabelle/Manual.pdf](snapshots/isabelle/Manual.pdf) @@ -31,13 +29,28 @@ some Sail specifications and related tools. * A test suite for Sail (in [test/](test/)) -We also have versions of IBM POWER, a fragment of x86, and a -hand-written fragment of ARMv8-A, but these are currently not up-to-date -with the latest version of Sail, which is the (default) sail2 branch -on Github. +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: + +* [Sail ARMv8.5-A ISA model, automatically generated from the ARM-internal ASL reference, as used in the ARM ARM](https://github.com/rems-project/sail-arm). + +* [Sail ARMv8.3-A ISA model](https://github.com/rems-project/sail/tree/sail2/arm). This is the "public" model described in our [POPL 2019 paper](http://www.cl.cam.ac.uk/users/pes20/sail/sail-popl2019.pdf), now largely superseded by the above. + +* [Sail ARMv8-A ISA model, handwritten](https://github.com/rems-project/sail/tree/sail2/arm). This is a handwritten user-mode fragment. -The mips and cheri-mips specifications that used to be here have moved to -https://github.com/CTSRD-CHERI/sail-cheri-mips . +* [Sail RISC-V ISA model, handwritten](https://github.com/rems-project/sail-riscv). + +* [Sail MIPS and CHERI-MIPS ISA models, handwritten](https://github.com/CTSRD-CHERI/sail-cheri-mips). + +* [Sail IBM POWER ISA model, automatically generated from IBM XML documentation](https://github.com/rems-project/sail/tree/sail2/power). This is a user-mode fragment. + +* [Sail x86 ISA model, handwritten](https://github.com/rems-project/sail/tree/sail2/x86). This is a handwritten user-mode fragment. + +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](http://www.cl.cam.ac.uk/users/pes20/rmem) tool for concurrency semantics. OPAM Installation ================= @@ -81,3 +94,5 @@ 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. \ No newline at end of file -- cgit v1.2.3