diff options
| -rw-r--r-- | doc/ExtendingGuide.md | 80 | ||||
| -rw-r--r-- | doc/ReadingGuide.md | 7 |
2 files changed, 86 insertions, 1 deletions
diff --git a/doc/ExtendingGuide.md b/doc/ExtendingGuide.md new file mode 100644 index 0000000..c3cee02 --- /dev/null +++ b/doc/ExtendingGuide.md @@ -0,0 +1,80 @@ +Extending the model +=================== + +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 +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.sail`. + +Adding a new privilege level will normally be accompanied by defining +new exception causes and their encodings. This will require modifying +and extending the existing definitions for privilege levels and +exceptions in `riscv_types.sail`, and modifying the exception handling +and privilege transition functions in `riscv_sys.sail`. + +Adding low-level platform functionality +--------------------------------------- + +Adding support for new devices such as interrupt controllers and +similar memory-mapped I/O (MMIO) entities strictly falls outside the +purview of the formal model itself, and typically is not done +directly in the Sail model. However, bindings to this external +functionality can be provided to Sail definitions using the `extern` +construct of the Sail language. `riscv_platform.sail` can be examined +for how this is done for the SiFive core-local interrupt (CLINT) +controller, and the HTIF timer and terminal devices. The +implementation of the actual functionality provided by these MMIO +devices would need to be added to the C and OCaml emulators. + +If this functionality requires the definition of new interrupt +sources, their encodings would need to be added to `riscv_types.sail`, +and their delegation and handling to `riscv_sys.sail`. + +Interposing on 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`. + +The actual content of such memory, and its modification, can be +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`. + +Virtual memory is implemented in `riscv_vmem.sail`, and defining new +address translation schemes or will require updating modifying the +top-level `translateAddr` function. Any access control checks on +virtual addresses and the specifics of the address translation can be +specified in a separate file. This functionality can access any newly +defined architectural state. + +Adding new instructions +----------------------- + +This is typically simpler than adding new architectural state or +memory interposition. Each new set of instructions can be specified +in a separate self-contained file, with their instruction encodings, +assembly language specifications and the corresponding encoders and +decoders, and execution semantics. `riscv.sail` can be examined for +examples on how this can done. These instruction definitions can +access any newly defined architectural state and perform virtual or +physical memory accesses as is done in `riscv.sail`. + + +General guidelines +------------------ + +For any new extension, it is helpful to factor it out into the above +items. When specifying and implementing the extension, it is expected +to be easier to implement it in the above listed order. diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md index f5e365b..d60186e 100644 --- a/doc/ReadingGuide.md +++ b/doc/ReadingGuide.md @@ -8,7 +8,9 @@ manual](https://github.com/rems-project/sail/blob/sail2/manual.pdf) handy. The model contains the following Sail modules in the `model` directory: - `prelude.sail` contains useful Sail library functions. This file - should be referred to as needed. + should be referred to as needed. The lowest level memory access + primitives are defined in this file, and are typically implemented + by the various Sail backends. - `riscv_types.sail` contains some basic RISC-V definitions. This file should be read first, since it provides basic definitions that @@ -69,3 +71,6 @@ The model contains the following Sail modules in the `model` directory: - `riscv_analysis.sail` is used in the formal operational RVWMO memory model. + +Note that the files above are listed in dependency order, i.e. files +earlier in the order do not depend on later files. |