update README

1 files changed, 129 insertions, 131 deletions

diff --git a/README.md b/README.md
index c844f1d..ec962ef 100644
--- a/README.md
+++ b/README.md
@@ -26,8 +26,8 @@ This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_
 [RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review).
 
 
-Sail
-----
+What is Sail?
+-------------
 
 [Sail](https://www.cl.cam.ac.uk/~pes20/sail/) ([repo](https://github.com/rems-project/sail)) is a language for describing the instruction-set architecture
 (ISA) semantics of processors. Sail aims to provide a
@@ -59,30 +59,83 @@ for smaller fragments of IBM POWER and x86.
 
 
 
+Example instruction specifications
+----------------------------------
 
-Directory Structure
--------------------
+These are verbatim excerpts from the main model file, [riscv.sail](https://github.com/rems-project/sail-riscv/blob/master/model/riscv.sail), with a few comments added.
+
+### ITYPE (or ADDI)
+~~~~~
+/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */
+
+union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
+
+/* the encode/decode mapping between AST elements and 32-bit words */
+
+mapping encdec_iop : iop <-> bits(3) = {
+  RISCV_ADDI  <-> 0b000,
+  RISCV_SLTI  <-> 0b010,
+  RISCV_SLTIU <-> 0b011,
+  RISCV_ANDI  <-> 0b111,
+  RISCV_ORI   <-> 0b110,
+  RISCV_XORI  <-> 0b100
+}
+
+mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
+
+/* the execution semantics for the ITYPE instructions */
+
+function clause execute (ITYPE (imm, rs1, rd, op)) = {
+  let rs1_val = X(rs1);
+  let immext : xlenbits = EXTS(imm);
+  let result : xlenbits = match op {
+    RISCV_ADDI  => rs1_val + immext,
+    RISCV_SLTI  => EXTZ(rs1_val <_s immext),
+    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;
+  true
+}
+
+/* the assembly/disassembly mapping between AST elements and strings */
+
+mapping itype_mnemonic : iop <-> string = {
+  RISCV_ADDI  <-> "addi",
+  RISCV_SLTI  <-> "slti",
+  RISCV_SLTIU <-> "sltiu",
+  RISCV_XORI  <-> "xori",
+  RISCV_ORI   <-> "ori",
+  RISCV_ANDI  <-> "andi"
+}
+
+mapping clause assembly = ITYPE(imm, rs1, rd, op)
+                      <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
+~~~~~~
+
+### SRET 
+
+~~~~~
+union clause ast = SRET : unit
+
+mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
+
+function clause execute SRET() = {
+  match cur_privilege {
+    User       => handle_illegal(),
+    Supervisor => if   mstatus.TSR() == true
+                  then handle_illegal()
+                  else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC),
+    Machine    => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
+  };
+  false
+}
+
+mapping clause assembly = SRET() <-> "sret"
+~~~~~
 
-```
-sail-riscv
-- model                   // Sail specification modules
-- generated_definitions   // files generated by Sail, in RV32 and RV64 subdirectories
-  -  c
-  -  ocaml
-  -  lem
-  -  isabelle
-  -  coq
-  -  hol4
-  -  latex
-- prover_snapshots        // snapshots of generated theorem prover definitions
-- handwritten_support     // prover support files
-- c_emulator              // supporting platform files for C emulator
-- ocaml_emulator          // supporting platform files for OCaml emulator
-- doc                     // documentation, including a reading guide
-- test                    // test files
-  - riscv-tests           // snapshot of tests from the riscv/riscv-tests github repo
-- os-boot                 // information and sample files for booting OS images
-```
 
 Sequential execution
 ----------
@@ -107,16 +160,14 @@ platform devices, define the physical memory map, and use command-line
 options to select implementation-specific ISA choices.
 
 
-Use for specification coverage measurement in testing
------------------------------------------------------
+### Use for specification coverage measurement in testing
 
 The Sail-generated C emulator can measure specification branch
 coverage of any executed tests, displaying the results as per-file
 tables and as html-annotated versions of the model source.
 
 
-Use as test oracle in tandem verification
------------------------------------------
+### Use as test oracle in tandem verification
 
 For tandem verification of random instruction streams we support the
 protocols used in [TestRIG](https://github.com/CTSRD-CHERI/TestRIG) to
@@ -133,16 +184,6 @@ implementation choices in Spike that are not mandated by the ISA
 specification.
 
 
-Use in test generation
-----------------------
-
-Our OCaml backend can produce QuickCheck-style random generators for
-types in Sail specifications, which we have used to produce random
-instructions sequences for testing.  The generation of individual
-types can be overridden by the developer to, for example, remove
-implementation-specific instructions or introduce register biasing.
-
-
 Concurrent execution
 --------------------
 
@@ -154,8 +195,8 @@ part of our [RMEM](http://www.cl.cam.ac.uk/users/pes20/rmem) tool.
 It is also integrated with the RISC-V axiomatic concurrency model
  as part of our [isla-axiomatic](https://isla-axiomatic.cl.cam.ac.uk/) tool.
 
-Concurrent testing
-------------------
+## Concurrent testing
+
 
 As part of our concurrency architecture work, we have produced and
 released a library of approximately 7000 [litmus
@@ -169,8 +210,20 @@ FU540 multicore proto board (Freedom Unleashed), kindly on loan from
 Imperas. To date, we see only sequentially consistent behaviour there.
 
 
-Provers
--------
+
+Use in test generation
+----------------------
+
+Our OCaml backend can produce QuickCheck-style random generators for
+types in Sail specifications, which we have used to produce random
+instructions sequences for testing.  The generation of individual
+types can be overridden by the developer to, for example, remove
+implementation-specific instructions or introduce register biasing.
+
+
+
+Generating theorem-prover definitions
+--------------------------------------
 
 With Sail we aim to support the generation of idiomatic theorem prover
 definitions across multiple tools. At present we support Isabelle,
@@ -193,8 +246,35 @@ tool.
 The files under `handwritten_support` provide library definitions for
 Coq, Isabelle and HOL4.
 
-Building the model
-------------------
+
+Directory Structure
+-------------------
+
+```
+sail-riscv
+- model                   // Sail specification modules
+- generated_definitions   // files generated by Sail, in RV32 and RV64 subdirectories
+  -  c
+  -  ocaml
+  -  lem
+  -  isabelle
+  -  coq
+  -  hol4
+  -  latex
+- prover_snapshots        // snapshots of generated theorem prover definitions
+- handwritten_support     // prover support files
+- c_emulator              // supporting platform files for C emulator
+- ocaml_emulator          // supporting platform files for OCaml emulator
+- doc                     // documentation, including a reading guide
+- test                    // test files
+  - riscv-tests           // snapshot of tests from the riscv/riscv-tests github repo
+- os-boot                 // information and sample files for booting OS images
+```
+
+Getting started
+---------------
+
+### Building the model
 
 Install [Sail](https://github.com/rems-project/sail/), either via opam
 or by building Sail from source and setting `SAIL_DIR` in your
@@ -232,8 +312,7 @@ corresponding prover libraries in the Sail directory
 (`$SAIL_DIR/lib/$prover`) are up-to-date and built, e.g. by running
 `make` in those directories.
 
-Executing test binaries
------------------------
+### Executing test binaries
 
 The C and OCaml simulators can be used to execute small test binaries.  The
 OCaml simulator depends on the Device Tree Compiler package, which can be
@@ -256,8 +335,7 @@ A suite of RV32 and RV64 test programs derived from the
 included under [test/riscv-tests/](test/riscv-tests/).  The test-suite
 can be run using `test/run_tests.sh`.
 
-Configuring platform options
-----------------------------
+### Configuring platform options
 
 Some information on additional configuration options for each
 simulator is available from `./ocaml_emulator/riscv_ocaml_sim_<arch>
@@ -268,89 +346,7 @@ Some useful options are: configuring whether misaligned accesses trap
 whether page-table walks update PTE bits (`--enable-dirty-update` for C
 and `-enable-dirty-update` for OCaml).
 
-Booting OS images
------------------
-
-For booting operating system images, see the information under the
-[os-boot/](os-boot/) subdirectory.
-
-
-Example instructions
---------------------
-
-These are verbatim excerpts from the main model file, [riscv.sail](https://github.com/rems-project/sail-riscv/blob/master/model/riscv.sail), with a few comments added.
-
-### ITYPE (or ADDI)
-~~~~~
-/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */
-
-union clause ast = ITYPE : (bits(12), regbits, regbits, iop)
-
-/* the encode/decode mapping between AST elements and 32-bit words */
-
-mapping encdec_iop : iop <-> bits(3) = {
-  RISCV_ADDI  <-> 0b000,
-  RISCV_SLTI  <-> 0b010,
-  RISCV_SLTIU <-> 0b011,
-  RISCV_ANDI  <-> 0b111,
-  RISCV_ORI   <-> 0b110,
-  RISCV_XORI  <-> 0b100
-}
-
-mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
-
-/* the execution semantics for the ITYPE instructions */
-
-function clause execute (ITYPE (imm, rs1, rd, op)) = {
-  let rs1_val = X(rs1);
-  let immext : xlenbits = EXTS(imm);
-  let result : xlenbits = match op {
-    RISCV_ADDI  => rs1_val + immext,
-    RISCV_SLTI  => EXTZ(rs1_val <_s immext),
-    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;
-  true
-}
-
-/* the assembly/disassembly mapping between AST elements and strings */
-
-mapping itype_mnemonic : iop <-> string = {
-  RISCV_ADDI  <-> "addi",
-  RISCV_SLTI  <-> "slti",
-  RISCV_SLTIU <-> "sltiu",
-  RISCV_XORI  <-> "xori",
-  RISCV_ORI   <-> "ori",
-  RISCV_ANDI  <-> "andi"
-}
-
-mapping clause assembly = ITYPE(imm, rs1, rd, op)
-                      <-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_12(imm)
-~~~~~~
-
-### SRET 
-
-~~~~~
-union clause ast = SRET : unit
-
-mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
-
-function clause execute SRET() = {
-  match cur_privilege {
-    User       => handle_illegal(),
-    Supervisor => if   mstatus.TSR() == true
-                  then handle_illegal()
-                  else nextPC = handle_exception(cur_privilege, CTL_SRET(), PC),
-    Machine    => nextPC = handle_exception(cur_privilege, CTL_SRET(), PC)
-  };
-  false
-}
-
-mapping clause assembly = SRET() <-> "sret"
-~~~~~
+### Booting OS images
 
 
 Authors
@@ -379,3 +375,5 @@ This software was developed within the Rigorous
 Engineering of Mainstream Systems (REMS) project, partly funded by
 EPSRC grant EP/K008528/1, at the Universities of Cambridge and
 Edinburgh.
+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).