diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 33 |
1 files changed, 16 insertions, 17 deletions
@@ -16,27 +16,26 @@ Directory Structure ``` sail-riscv | -+---- model // Sail specification modules ++---- model // Sail specification modules | -+---- generated_models // Files generated by Sail ++---- generated_definitions // Files generated by Sail | | -| +---- c // C simulator definitions -| +---- ocaml // OCaml simulator definitions -| +---- lem // Lem model -| +---- isabelle // Isabelle model -| +---- coq // Coq model -| +---- hol4 // HOL4 model +| +---- c +| +---- ocaml +| +---- lem +| +---- isabelle +| +---- coq +| +---- hol4 +| +---- latex | -| // Handwritten files +|---- handwritten_support // Prover support files | -+---- c_emulator // supporting platform files for C emulator -+---- ocaml_emulator // supporting platform files for OCaml emulator -+---- lem // Lem library -+---- coq // Coq library ++---- c_emulator // supporting platform files for C emulator ++---- ocaml_emulator // supporting platform files for OCaml emulator | -+---- test // test files ++---- test // test files | - +---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo + +---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo ``` An outline of the specification @@ -81,8 +80,8 @@ 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_models/isabelle/Riscv.thy`, and the Coq -model in `generated_models/coq/riscv.v`. +`c_emulator/riscv_sim`, the Isabelle model in `generated_definitions/isabelle/Riscv.thy`, and the Coq +model in `generated_definitions/coq/riscv.v`. Executing test binaries ----------------------- |