diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-01-16 18:50:31 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-01-16 19:04:30 -0800 |
| commit | 793643d5879f311f8979cc5046f07020cbb375fd (patch) | |
| tree | fbf83b4b5169016dfa2b361b115ec9114d3734c0 /README.md | |
| parent | 684f431d52c610cc24d12ae3e7b7def9fa0d5317 (diff) | |
| download | sail-riscv-793643d5879f311f8979cc5046f07020cbb375fd.zip sail-riscv-793643d5879f311f8979cc5046f07020cbb375fd.tar.gz sail-riscv-793643d5879f311f8979cc5046f07020cbb375fd.tar.bz2 | |
More reorg.
. move prover files into a single support directory
. generated_models -> generated_definitions
. reset vector -> c_emulator
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 ----------------------- |