Add extended model from cheri-merge.

1 files changed, 20 insertions, 4 deletions

diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md
index e6ad5f5..9145ac9 100644
--- a/doc/ReadingGuide.md
+++ b/doc/ReadingGuide.md
@@ -19,15 +19,19 @@ The model contains the following Sail modules in the `model` directory:
 
 - `riscv_types.sail` contains some basic RISC-V definitions.  This
   file should be read first, since it provides basic definitions that
-  are used throughout the specification, such as privilege
-  levels, registers and register access, interrupt and exception
-  definitions and numbering, and types used to define memory accesses.
+  are used throughout the specification, such as privilege levels,
+  registers and register access, interrupt and exception definitions
+  and numbering, and types used to define memory accesses.  The
+  register type is separately defined in `riscv_reg_type.sail` so that
+  extensions of the model can redefine it if required.
 
 - `riscv_sys_regs.sail` describes the privileged architectural state,
   viz. M-mode and S-mode CSRs, and contains helpers to interpret their
   content, such as WLRL and WARL fields.  `riscv_sys_control.sail`
   describes interrupt and exception delegation and dispatch, and the
-  handling of privilege transitions.
+  handling of privilege transitions. `riscv_sys_exceptions.sail`
+  defines the handling of the addresses involved in exception
+  handling.
 
   Since WLRL and WARL fields are intended to capture platform-specific
   functionality, future versions of the model might separate their
@@ -62,6 +66,14 @@ The model contains the following Sail modules in the `model` directory:
   `riscv_vmem_rv64.sail` describe the top-level address translation
   for the corresponding architectures.
 
+- The `riscv_addr_checks_common.sail` and `riscv_addr_checks.sail`
+  contain extension hooks to support the checking and transformation
+  of memory addresses during the execution of an instruction.  The
+  transformed addresses are used for any address translation; however,
+  any memory access exceptions are reported in terms of the original
+  memory address (i.e. the one generated by the instruction, not the
+  hook).
+
 - Files matching `riscv_insts_*.sail` capture the instruction
   definitions and their assembly language formats.  Each file contains
   the instructions for an extension, with `riscv_insts_base.sail` containing
@@ -71,6 +83,10 @@ The model contains the following Sail modules in the `model` directory:
   clauses specify the encoding and decoding of each instruction to and
   from assembly language formats.
 
+- `riscv_fetch.sail` contains the instruction fetch function.  It
+  supports checking and transformation of the fetch address as
+  described above.
+
 - `riscv_step.sail` implements the top-level fetch and execute loop.
   The `fetch` is done in 16-bit granules to handle RVC instructions.
   The `step` function performs the instruction fetch, handles any