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 /README.md | |
| parent | 844feb92ca50901c79fbdd05a0e808d335207ae1 (diff) | |
| download | sail-riscv-5cb13966646d6d09f2589cd0992f1771cffc72ca.zip sail-riscv-5cb13966646d6d09f2589cd0992f1771cffc72ca.tar.gz sail-riscv-5cb13966646d6d09f2589cd0992f1771cffc72ca.tar.bz2 | |
Update docs.
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 8 |
1 files changed, 8 insertions, 0 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. |