diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-03-07 10:48:58 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-03-07 10:48:58 -0800 |
| commit | 97d6a6a302e5969424262cf64f60169e0139a07b (patch) | |
| tree | 33aacbcea5e824e0e04950ec11836fcbce1e0a48 | |
| parent | c6c9f7c9377d7ec111d4fac4869432454a1f1995 (diff) | |
| download | sail-riscv-97d6a6a302e5969424262cf64f60169e0139a07b.zip sail-riscv-97d6a6a302e5969424262cf64f60169e0139a07b.tar.gz sail-riscv-97d6a6a302e5969424262cf64f60169e0139a07b.tar.bz2 | |
More doc edits.
| -rw-r--r-- | README.md | 21 | ||||
| -rw-r--r-- | os-boot/README.md | 2 |
2 files changed, 16 insertions, 7 deletions
@@ -77,8 +77,9 @@ will build the 64-bit OCaml simulator 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` 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 @@ -90,8 +91,9 @@ which creates the 32-bit OCaml simulator in 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. +`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 ----------------------- @@ -102,8 +104,15 @@ 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`. + +A suite of RV32 and RV64 test programs derived from the +[`riscv-tests`](https://github.com/riscv/riscv-tests) in included +under [test/riscv-tests/](test/riscv-tests/). The test-suite can be +run using `test/run_tests.sh`. + +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 diff --git a/os-boot/README.md b/os-boot/README.md index bcb220b..a11b39f 100644 --- a/os-boot/README.md +++ b/os-boot/README.md @@ -59,7 +59,7 @@ Caveats for OS boot Sample OS images ---------------- -This directory contains some sample OS images and support files, built +This directory contains some sample OS images and support files built for the basic platform implemented by the model. They were built with toolchains that emitted illegal instructions, and require the model to be patched to boot them: |