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 /README.md | |
| parent | c6c9f7c9377d7ec111d4fac4869432454a1f1995 (diff) | |
| download | sail-riscv-97d6a6a302e5969424262cf64f60169e0139a07b.zip sail-riscv-97d6a6a302e5969424262cf64f60169e0139a07b.tar.gz sail-riscv-97d6a6a302e5969424262cf64f60169e0139a07b.tar.bz2 | |
More doc edits.
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 21 |
1 files changed, 15 insertions, 6 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 |