Update docs.

2 files changed, 28 insertions, 21 deletions

diff --git a/doc/ExtendingGuide.md b/doc/ExtendingGuide.md
index 82a418d..a13ec94 100644
--- a/doc/ExtendingGuide.md
+++ b/doc/ExtendingGuide.md
@@ -17,14 +17,16 @@ Adding architectural state
 
 Adding registers (such as for floating-point) would involve naming
 them and defining their read and write accessors, as is done for the
-integer registers in `riscv_types.sail`.  For modularity, these new
-definitions can be added in a separate file.  If these registers have
-properties of control-and-status registers (CSRs), or depend on
+integer registers in `riscv_types.sail`, `riscv_reg_type.sail` and
+`riscv_regs.sail`.  For modularity, these new definitions should be
+added in separate files.  If any of these registers are
+control-and-status registers (CSRs), or depend on
 privilege level (such as hypervisor-mode registers), additional access
 control checks would need to be provided as is done for the standard
-CSRs in `riscv_sys_regs.sail` and `riscv_sys_control.sail`.  In addition,
-the bits `mstatus.XS` and `mstatus.SD` may need to be updated or
-extended to handle any extended register state.
+CSRs in `riscv_sys_regs.sail` and `riscv_sys_control.sail`.  Access to
+newly added CSRs can be hooked in `riscv_csr_ext.sail`. In addition,
+the bits `mstatus.XS` and `mstatus.SD` may need to be updated
+or extended to handle any extended register state.
 
 Adding a new privilege level or functionality restricted by privilege
 level will normally be accompanied by defining new exception causes
@@ -40,7 +42,9 @@ An extension that needs to interact closely with exception handling
 may need to capture additional information at the time of an
 exception.  This is supported using the `ext` field in the
 `sync_exception` type in `riscv_sync_exception.sail`, which is where
-the extension can store this information.
+the extension can store this information.  The addresses involved in
+exception handling can be modified by following the interface provided
+in `riscv_sys_exceptions.sail`.
 
 Adding low-level platform functionality
 ---------------------------------------
@@ -71,14 +75,14 @@ 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
+customize the default implementation there to support its metadata
 type.
 
 The actual content of such memory, and its modification, can be
-defined in separate sail files.  This functionality will have access
+defined in separate Sail files.  This functionality will have access
 to any newly defined architectural state.  One can examine how normal
 physical memory access is implemented in `riscv_mem.sail` with helpers
-in `prelude.sail`.
+in `prelude_mem.sail` and `prelude_mem_metadata.sail`.
 
 Virtual memory is implemented in `riscv_vmem.sail`, and defining new
 address translation schemes will require modifying the
@@ -138,8 +142,10 @@ Example
 
 As an example, one can examine the implementation of the 'N' extension
 for user-level interrupt handling.  The architectural state to support
-'N' is specified in `riscv_next_regs.sail`, added control
+'N' is specified in `riscv_next_regs.sail`, added CSR and control
 functionality is in `riscv_next_control.sail`, and added instructions
-are in `riscv_insts_next.sail`.  In addition, privilege transition and
-interrupt delegation logic in `riscv_sys_control.sail` has been
-extended.
+are in `riscv_insts_next.sail`.  Access to the CSRs added by the
+extension are hooked in `riscv_csr_ext.sail`.
+
+In addition, privilege transition and interrupt delegation logic in
+`riscv_sys_control.sail` has been extended.
diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md
index ad09cf0..deda95e 100644
--- a/doc/ReadingGuide.md
+++ b/doc/ReadingGuide.md
@@ -11,23 +11,24 @@ The model contains the following Sail modules in the `model` directory:
   and RV64.  One of them is chosen during the build using the ARCH
   variable.
 
-- `prelude_*.sail` contains useful Sail library functions.  These
+- `prelude_*.sail` contain useful Sail library functions.  These
   files should be referred to as needed.  The lowest level memory
   access primitives are defined in `prelude_mem.sail`, and are
   implemented by the various Sail backends. `prelude_mem.sail`
-  currently depends on the value of `xlen`.
+  depends on the value of `xlen`.
 
 - `riscv_types.sail` contains some basic RISC-V definitions.  This
-  file should be read first, since it provides basic definitions that
+  file should be read first, since these definitions
   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 indices, interrupt and exception definitions
+  and enumerations, 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_regs.sail` contains the base register file, where each
   register is defined as having the `regtype` type defined in
-  `riscv_reg_type.sail`.
+  `riscv_reg_type.sail` and indexed by the indices defined in
+  `riscv_types.sail`.
 
 - `riscv_pc_access.sail` defines functions to access and modify the
   program counter.
@@ -89,7 +90,7 @@ The model contains the following Sail modules in the `model` directory:
   as a variant clause of the `ast` type, and its execution semantics
   are represented as a clause of the `execute` function. `mapping`
   clauses specify the encoding and decoding of each instruction to and
-  from assembly language formats.
+  from their binary representations and assembly language formats.
 
 - `riscv_fetch.sail` contains the instruction fetch function.  It
   supports checking and transformation of the fetch address as