Add extended model from cheri-merge.

3 files changed, 55 insertions, 8 deletions

diff --git a/doc/ExtendingGuide.md b/doc/ExtendingGuide.md
index 8358123..f38130a 100644
--- a/doc/ExtendingGuide.md
+++ b/doc/ExtendingGuide.md
@@ -1,6 +1,17 @@
 Extending the model
 ===================
 
+Changing the register representation
+------------------------------------
+
+One can change the base register representation from an `XLEN`-length
+bitvector by supplying a different definition of the `regtype` type,
+and functions that convert between that type and the default
+`XLEN`-length bitvector.  The interface for this is specified in
+`riscv_reg_type.sail`.  An extension can implement a different
+representation in a file that follows that interface, and use it with
+the rest of the model.
+
 Adding architectural state
 --------------------------
 
@@ -44,10 +55,15 @@ Modifying memory access
 -----------------------
 
 Physical memory addressing and access is defined in `riscv_mem.sail`.
-Any new types of memory (such as scratchpad, tags, or MMIO device
-memory) that are accessible via physical addresses will require
-modifying the `mem_read`, `mem_write_value` or their supporting
-functions `checked_mem_read` and `checked_mem_write`.
+Any new regions of memory that are accessible via physical addresses
+will require modifying the `mem_read`, `mem_write_value` or their
+supporting functions `checked_mem_read` and `checked_mem_write`.
+
+The model supports storing and retrieving metadata along with memory
+values at each physical memory address.  The default interface for
+this is defined in `prelude_mem_metadata.sail`.  An extension can
+customize the default implementation there to support its the metadata
+type.
 
 The actual content of such memory, and its modification, can be
 defined in separate sail files.  This functionality will have access
@@ -62,6 +78,19 @@ virtual addresses and the specifics of the new address translation can be
 specified in a separate file.  This functionality can access any newly
 defined architectural state.
 
+Checking and transforming memory addresses
+------------------------------------------
+
+An extension may wish to perform validity checks and transformations
+on addresses generated by an instruction before a memory access is
+performed with the generated address.  This is supported using the
+types defined in `riscv_addr_checks_common.sail`, with a default
+implementation in `riscv_addr_checks.sail`.
+
+The handling of the memory addresses involved during exception
+handling can be extending using the interface defined in
+`riscv_sys_exceptions.sail`.
+
 Adding new instructions
 -----------------------
 
diff --git a/doc/README.md b/doc/README.md
new file mode 100644
index 0000000..9057e2d
--- /dev/null
+++ b/doc/README.md
@@ -0,0 +1,2 @@
+See the [reading guide](../doc/ReadingGuide.md) to navigate the files
+in this directory.
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