diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-20 13:16:10 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-02-20 13:20:54 -0800 |
| commit | 5cb13966646d6d09f2589cd0992f1771cffc72ca (patch) | |
| tree | 047bc85087cfbffdd037849822358860e6e1cac5 | |
| parent | 844feb92ca50901c79fbdd05a0e808d335207ae1 (diff) | |
| download | sail-riscv-5cb13966646d6d09f2589cd0992f1771cffc72ca.zip sail-riscv-5cb13966646d6d09f2589cd0992f1771cffc72ca.tar.gz sail-riscv-5cb13966646d6d09f2589cd0992f1771cffc72ca.tar.bz2 | |
Update docs.
| -rw-r--r-- | README.md | 8 | ||||
| -rw-r--r-- | doc/ReadingGuide.md | 26 |
2 files changed, 24 insertions, 10 deletions
@@ -68,6 +68,14 @@ will build the OCaml simulator in `ocaml_emulator/riscv_ocaml_sim`, the C simula model in `generated_definitions/coq/riscv.v`, and the HOL4 model in `generated_definitions/hol4/riscvScript.sml`. +One can build either the RV32 or the RV64 model by specifying +`ARCH=RV32` or `ARCH=RV64` on the `make` line. RV64 is built by +default, but the RV32 model can be built using: + +``` +$ ARCH=RV32 make +``` + 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. diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md index 1946a9e..e6ad5f5 100644 --- a/doc/ReadingGuide.md +++ b/doc/ReadingGuide.md @@ -7,13 +7,15 @@ manual](https://github.com/rems-project/sail/blob/sail2/manual.pdf) handy. The model contains the following Sail modules in the `model` directory: -- `prelude.sail` contains useful Sail library functions. This file - 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. +- `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. -- `riscv_xlen.sail` contains the `XLEN` definition for the model. It - can be set for either RV32 or RV64. +- `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 @@ -51,10 +53,14 @@ The model contains the following Sail modules in the `model` directory: appropriate access fault. This file also contains definitions that are used in the weak memory concurrency model. -- `riscv_vmem.sail` describes the S-mode address translation. It - contains the definitions and processing of the page-table entries - and their various permission and status bits, the specification of - page-table walks, and the selection of the address translation mode. +- 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. - Files matching `riscv_insts_*.sail` capture the instruction definitions and their assembly language formats. Each file contains |