ReadingGuide.md

A guide to reading the specification

The model is written in the Sail language. Although specifications in Sail are quite readable as pseudocode, it would help to have the Sail manual handy.

The Sail modules in the model directory have the structure shown below. Arrows indicate a dependency relationship, and italics indicate fragments that are not strictly part of the specification, such as the platform memory map.

• riscv_xlen32.sail and riscv_xlen64.sail define xlen for RV32 and RV64. One of them is chosen during the build using the ARCH variable.

• 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 depends on the value of xlen.

• riscv_types.sail contains some basic RISC-V definitions. This file should be read first, since these definitions are used throughout the specification, such as privilege levels, 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 and indexed by the indices defined in riscv_types.sail.

• riscv_pc_access.sail defines functions to access and modify the program counter.

• 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. riscv_sys_exceptions.sail defines the handling of the addresses involved in exception handling. riscv_sync_exception.sail describes the structure used to capture the architectural information for an exception.

  Since WLRL and WARL fields are intended to capture platform-specific functionality, future versions of the model might separate their handling functions out into a separate platform-defined file. The current implementation of these functions usually implement the same behavior as the Spike emulator.

• riscv_pmp_regs.sail and riscv_pmp_control.sail implement support for physical memory protection (PMP). riscv_pmp_regs handle read and write access to the PMP registers, while riscv_pmp_control implements the permission checking and matching priority.

• riscv_platform.sail contains platform-specific functionality for the model. It contains the physical memory map, the local interrupt controller, and the MMIO interfaces to the clock, timer and terminal devices. Sail extern definitions are used to connect externally provided (i.e. external to the Sail model) platform functionality, such as those provided by the platform support in the C and OCaml emulators. This file also contains the externally selectable options for platform behavior, such as the handling of misaligned memory accesses, the handling of PTE dirty-bit updates during address translation, etc. These platform options can be specified via command line switches in the C and OCaml emulators.

• riscv_mem.sail contains the functions that convert accesses to physical addresses into accesses to physical memory, or MMIO accesses to the devices provided by the platform, or into the appropriate access fault. This file also contains definitions that are used in the weak memory concurrency model.

• The riscv_vmem_*.sail files describe the S-mode address translation. riscv_vmem_types and riscv_vmem_common.sail contain the definitions and processing of the page-table entries and their various permission and status bits. riscv_types_ext, riscv_vmem_sv32.sail, riscv_vmem_sv39.sail, and riscv_vmem_sv48.sail contain the specifications for the corresponding page-table walks, and riscv_vmem_rv32.sail and 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 the base integer instruction set. Each instruction is represented 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 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 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 fetch errors, decodes the fetched value, dispatches the execution of the decoded instruction, and checks for any pending interrupts that may need to be handled. A loop function implements the execute loop, and uses the same HTIF (host-target interface) mechanism as the Spike emulator to detect termination of execution.

• 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.

Structure of the C emulator

The diagram below illustrates how the C emulator is built from the Sail model. The OCaml emulator follows the same approach.

The nodes that are not colored are the handwritten C files for the C emulator. The black arrows indicate dependency relationships, while the red arrow indicates a file generated by the Sail compiler from Sail source files.

riscv_sim is the top level file for the C emulator: it processes command line options, initializes the platform model with any ISA implementation choices if specified, and loads the ELF program or OS image into raw memory, including any ROM firmware such as the Berkeley boot loader and DeviceTree binary blobs, and initializes the memory map.

The generated C model riscv_model_$ARCH is built from the Sail sources by the Sail compiler for the specified architecture $ARCH, either RV32 or RV64. It contains calls to the platform interface riscv_platform for platform-specific information; the latter is typically defined as externally specified in the Sail file riscv_platform.sail.

The Sail system provides a C library for use with its C backend, which provides the low-level details of the implementation of raw memory and bitvectors (typically optimized to use the native machine word representation).