Add some initial info about the Sail files to the readme.

1 files changed, 41 insertions, 8 deletions

diff --git a/README.md b/README.md
index fa97fc1..58deaa3 100644
--- a/README.md
+++ b/README.md
@@ -7,10 +7,43 @@ in the [Sail repository](https://github.com/rems-project/sail).
 
 It currently implements enough of RV64IMAC to boot a conventional OS
 with a terminal output device.  Work on a 32-bit model is ongoing.
+The model specifies assembly language formats of the instructions, and
+implements the corresponding encoders and decoders.
 
+A tour of the specification
+---------------------------
 
-Building the model:
--------------------
+The model contains the following Sail modules:
+
+- `prelude.sail` contains useful Sail library functions
+
+- `riscv_types.sail` contains some basic RISC-V definitions
+
+- `riscv_sys.sail` describes M-mode and S-mode CSRs and exception handling
+
+- `riscv_platform.sail` contains platform-specific functionality
+    (e.g. physical memory map and clock and terminal device interfaces)
+
+- `riscv_mem.sail` contains the interface to physical memory
+
+- `riscv_vmem.sail` describes the S-mode address translation
+
+- `riscv.sail` captures the instruction definitions and their assembly language formats
+
+- `riscv_step.sail` implements the top-level fetch and execute loop
+
+- `riscv_analysis.sail` is used in the formal operational RVWMO memory model
+
+
+Simulators
+----------
+
+The files in OCaml and C simulators implement ELF-loading and the
+platform devices, define the physical memory map, and use command-line
+options to select implementation-specific ISA choices.
+
+Building the model
+------------------
 
 Install Sail via Opam, or build Sail from source and have SAIL_DIR in
 your environment pointing to its top-level directory.
@@ -22,8 +55,8 @@ will build the OCaml simulator in ```platform```, the C simulator in
 ```riscv_sim```, and the Isabelle model in ```Riscv.thy```, and the Coq
 model in ```riscv.v```.
 
-Booting Linux with the C backend:
----------------------------------
+Booting Linux with the C backend
+--------------------------------
 
 The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader)
 that contains the Linux kernel as an embedded payload.  It also needs
@@ -40,8 +73,8 @@ The ```console.log``` file contains the console boot messages.  Some
 information on additional configuration options is available from
 ```./riscv_sim -h```.
 
-Booting Linux with the OCaml backend:
--------------------------------------
+Booting Linux with the OCaml backend
+------------------------------------
 
 The OCaml model only needs the ELF-version of the BBL, since it can generate its
 own DTB.
@@ -51,8 +84,8 @@ $ ./platform bbl > execution-trace.log 2> console.log
 Some information on additional configuration options is available from
 ```./platform -h```.
 
-Generating Linux binaries:
---------------------------
+Generating Linux binaries
+-------------------------
 
 One could directly build Linux and the toolchain using
 ```https://github.com/sifive/freedom-u-sdk```.  The built ```bbl```