blob: 62c82b19305193268ceb60b22ff934b38b47b6c4 (
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
|
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.
An outline of the specification
-------------------------------
The model contains the following Sail modules:
- `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 `platform`, the C simulator in
`riscv_sim`, the Isabelle model in `Riscv.thy`, and the Coq
model in `riscv.v`.
Executing test binaries
-----------------------
The C and OCaml simulators can be used to execute small test RV64 binaries.
```
$ ./platform <elf-file>
$ ./riscv_sim <elf-file>
```
Some information on additional configuration options for each simulator is available
from `./platform -h` and `./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:
```
$ ./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.
```
$ ./platform 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.
|
