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
|
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,
the corresponding encoders and decoders, and the instruction semantics.
Directory Structure
-------------------
```
sail-riscv
|
+---- model // Sail specification modules
|
+---- generated_definitions // Files generated by Sail, in RV32 and RV64 subdirectories
| |
| +---- c
| +---- ocaml
| +---- lem
| +---- isabelle
| +---- coq
| +---- hol4
| +---- latex
|
|---- handwritten_support // Prover support files
|
+---- c_emulator // supporting platform files for C emulator
+---- ocaml_emulator // supporting platform files for OCaml emulator
|
+---- doc // documentation, including a reading-guide
|
+---- test // test files
|
+---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
```
Documentation
-------------
A [reading guide](doc/ReadingGuide.md) to the model is provided in the
[doc/](doc/) subdirectory, along with a guide on [how to
extend](doc/ExtendingGuide.md) the 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.
Provers
-------
The files under `handwritten_support` provide library definitions for
Coq, Isabelle and HOL4.
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 64-bit OCaml simulator in
`ocaml_emulator/riscv_ocaml_sim_RV64`, the C simulator in
`c_emulator/riscv_sim_RV64`, the Isabelle model in
`generated_definitions/isabelle/RV64/Riscv.thy`, the Coq model in
`generated_definitions/coq/RV64/riscv.v`, and the HOL4 model in
`generated_definitions/hol4/RV64/riscvScript.sml`.
One can build either the RV32 or the RV64 model by specifying
`ARCH=RV32` or `ARCH=RV64` on the `make` line, and using the matching target suffix. RV64 is built by
default, but the RV32 model can be built using:
```
$ ARCH=RV32 make
```
which creates the 32-bit OCaml simulator in
`ocaml_emulator/riscv_ocaml_sim_RV32`, and the C simulator in
`c_emulator/riscv_sim_RV32`, and the prover models in the
corresponding `RV32` subdirectories.
The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and
`riscv_hol_build` invoke the respective prover to process the definitions. We
have tested Isabelle 2018, Coq 8.8.1, and HOL4 Kananaskis-12.
Executing test binaries
-----------------------
The C and OCaml simulators can be used to execute small test binaries.
```
$ ./ocaml_emulator/riscv_ocaml_sim_<arch> <elf-file>
$ ./c_emulator/riscv_sim_<arch> <elf-file>
```
Some information on additional configuration options for each simulator is available
from `./ocaml_emulator/riscv_ocaml_sim_<arch> -h` and `./c_emulator/riscv_sim_<arch> -h`.
Some useful options are: configuring whether misaligned accesses trap
(--enable-misaligned for C and -enable-misaligned for OCaml), and
whether page-table walks update PTE bits (--enable-dirty-update for C
and -enable-dirty-update for OCaml).
For booting operating system images, see the information under the
[os-boot/](os-boot/) subdirectory.
|
