Merge remote-tracking branch 'origin/sail2' into asl_flow2

1 files changed, 45 insertions, 22 deletions

diff --git a/README.md b/README.md
index d1a5bc32..f3c877a4 100644
--- a/README.md
+++ b/README.md
@@ -4,13 +4,28 @@ 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
+<http://www.cl.cam.ac.uk/~pes20/sail/>.
+<p>
+
+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 
+<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a> 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.
+<p>
+
+  <img src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png">
+<p>
 
 This repository contains the implementation of Sail, together with
 some Sail specifications and related tools.
@@ -19,10 +34,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 +43,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
 =================
@@ -76,14 +103,10 @@ copyright ARM Ltd. See https://github.com/meriac/archex, and the
 The hand-written ARMv8 model, in arm/, is distributed under the
 2-clause BSD licence in the headers of those files.
 
-The MIPS and CHERI models, in mips/ and cheri/, are 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 RISC-V model in riscv/ model is also distributed under the
-2-clause BSD licence.
+The models in separate repositories are licensed as described in each. 
\ No newline at end of file