1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
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](https://github.com/rems-project/sail/blob/sail2/manual.pdf) handy.
The model contains the following Sail modules in the `model` directory:
- `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` contains 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`.
- `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. 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_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_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_common.sail` contains the definitions and
processing of the page-table entries and their various permission
and status bits. `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 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.
|
