blob: c50d9fea7ec6d44ac7653881df62a45be7176512 (
plain)
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
RISCV Sail Model
================
This repository contains a model of the RISCV architecture written in
[Sail](https://www.cl.cam.ac.uk/~pes20/sail/). It used to be contained
in the [Sail repository](https://github.com/rems-project/sail).
It currently implements enough of RV64IMAC to boot a conventional OS
with a terminal output device. Work on a 32-bit model is ongoing.
The model specifies assembly language formats of the instructions, and
implements the corresponding encoders and decoders.
Directory Structure
-------------------
```
sail-riscv
|
+---- model // Sail specification modules
|
+---- generated_models // Files generated by Sail
| |
| +---- c // C simulator definitions
| +---- ocaml // OCaml simulator definitions
| +---- lem // Lem model
| +---- isabelle // Isabelle model
| +---- coq // Coq model
| +---- hol4 // HOL4 model
|
| // Handwritten files
|
+---- c_emulator // supporting platform files for C emulator
+---- ocaml_emulator // supporting platform files for OCaml emulator
+---- lem // Lem library
+---- coq // Coq library
|
+---- test // test files
|
+---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
```
An outline of the specification
-------------------------------
The model contains the following Sail modules in the `model` directory:
- `prelude.sail` contains useful Sail library functions
- `riscv_types.sail` contains some basic RISC-V definitions
- `riscv_sys.sail` describes M-mode and S-mode CSRs and exception handling
- `riscv_platform.sail` contains platform-specific functionality
(e.g. physical memory map and clock and terminal device interfaces)
- `riscv_mem.sail` contains the interface to physical memory
- `riscv_vmem.sail` describes the S-mode address translation
- `riscv.sail` captures the instruction definitions and their assembly language formats
- `riscv_step.sail` implements the top-level fetch and execute loop
- `riscv_analysis.sail` is used in the formal operational RVWMO memory model
Simulators
----------
The files in the OCaml and C simulators implement ELF-loading and the
platform devices, define the physical memory map, and use command-line
options to select implementation-specific ISA choices.
Building the model
------------------
Install Sail via Opam, or build Sail from source and have SAIL_DIR in
your environment pointing to its top-level directory.
```
$ make
```
will build the OCaml simulator in `ocaml_emulator/riscv_ocaml_sim`, the C simulator in
`c_emulator/riscv_sim`, the Isabelle model in `generated_models/isabelle/Riscv.thy`, and the Coq
model in `generated_models/coq/riscv.v`.
Executing test binaries
-----------------------
The C and OCaml simulators can be used to execute small test RV64 binaries.
```
$ ./ocaml_emulator/riscv_ocaml_sim <elf-file>
$ ./c_emulator/riscv_sim <elf-file>
```
Some information on additional configuration options for each simulator is available
from `./ocaml_emulator/riscv_ocaml_sim -h` and `./c_emulator/riscv_sim -h`.
Booting Linux with the C backend
--------------------------------
The C model needs an ELF-version of the BBL (Berkeley-Boot-Loader)
that contains the Linux kernel as an embedded payload. It also needs
a DTB (device-tree blob) file describing the platform (say in the file
`spike.dtb`). Once those are available (see below for suggestions),
the model should be run as:
```
$ ./c_emulator/riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 &
$ tail -f console.log
```
The `console.log` file contains the console boot messages.
Booting Linux with the OCaml backend
------------------------------------
The OCaml model only needs the ELF-version of the BBL, since it can generate its
own DTB.
```
$ ./ocaml_emulator/riscv_ocaml_sim bbl > execution-trace.log 2> console.log
```
Generating input files for Linux boot
-------------------------------------
One could directly build Linux and the toolchain using
`https://github.com/sifive/freedom-u-sdk`. The built `bbl`
will be available in `./work/riscv-pk/bbl`. You will need to configure
a kernel that can be booted on Spike; in particular, it should be
configured to use the HTIF console.
The DTB can be generated using Spike and the DeviceTree compiler
`dtc` as:
```
spike --dump-dts . | dtc > spike.dtb
```
(The '.' above is to workaround a minor Spike bug and may not be
needed in future Spike versions.)
Caveats for OS boot
-------------------
- Some OS toolchains generate obsolete LR/SC instructions with now
illegal combinations of `.aq` and `.rl` flags. You can work-around
this by changing `riscv_mem.sail` to accept these flags.
- One needs to manually ensure that the DTB used for the C model
accurately describes the physical memory map implemented in the C
platform. This will not be needed once the C model can generate its
own DTB.
|