diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-01-22 16:48:10 +0000 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-01-22 16:48:10 +0000 |
| commit | b5b365d881f270c143d69734fc4cf9ff39bf92a7 (patch) | |
| tree | 7cde8a7fe93e499104bc311d8f0dd9b6d0ec03e1 /README.md | |
| parent | 3ecb42213976ac3eaaef8ae0b5bc17c1e40bb3bf (diff) | |
| download | sail-riscv-b5b365d881f270c143d69734fc4cf9ff39bf92a7.zip sail-riscv-b5b365d881f270c143d69734fc4cf9ff39bf92a7.tar.gz sail-riscv-b5b365d881f270c143d69734fc4cf9ff39bf92a7.tar.bz2 | |
Mention versions of tested provers
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 9 |
1 files changed, 7 insertions, 2 deletions
@@ -82,8 +82,13 @@ your environment pointing to its top-level directory. $ make ``` will build the OCaml simulator in `ocaml_emulator/riscv_ocaml_sim`, the C simulator in -`c_emulator/riscv_sim`, the Isabelle model in `generated_definitions/isabelle/Riscv.thy`, and the Coq -model in `generated_definitions/coq/riscv.v`. +`c_emulator/riscv_sim`, the Isabelle model in `generated_definitions/isabelle/Riscv.thy`, the Coq +model in `generated_definitions/coq/riscv.v`, and the HOL4 model in +`generated_definitions/hol4/riscvScript.sml`. + +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 ----------------------- |