diff options
| author | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-01-14 18:39:42 -0800 |
|---|---|---|
| committer | Prashanth Mundkur <prashanth.mundkur@gmail.com> | 2019-01-14 19:02:04 -0800 |
| commit | 3fdda1f2e054a01c95ff59593a8d67d85770609a (patch) | |
| tree | ce460b93f6240d98eaef659dbff2442402ee627d /README.md | |
| parent | 3c0168526eb9895292a6f92b42f243fce4fd1a9d (diff) | |
| download | sail-riscv-3fdda1f2e054a01c95ff59593a8d67d85770609a.zip sail-riscv-3fdda1f2e054a01c95ff59593a8d67d85770609a.tar.gz sail-riscv-3fdda1f2e054a01c95ff59593a8d67d85770609a.tar.bz2 | |
Reorganize directory structure.
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 44 |
1 files changed, 35 insertions, 9 deletions
@@ -10,10 +10,36 @@ with a terminal output device. Work on a 32-bit model is ongoing. The model specifies assembly language formats of the instructions, and implements the corresponding encoders and decoders. +Directory Structure +------------------- + +``` +sail-riscv +| ++---- model // Sail specification modules +| ++---- generated_models // Files generated by Sail +| | +| +---- c // C simulator definitions +| +---- ocaml // OCaml simulator definitions +| +---- lem // Lem model +| +---- isabelle // Isabelle model +| +---- coq // Coq model +| +---- hol4 // HOL4 model +| +| // Handwritten files ++---- c // C simulator ++---- ocaml // OCaml simulator ++---- lem // Lem library ++---- coq // Coq library +| ++---- test // unit test files +``` + An outline of the specification ------------------------------- -The model contains the following Sail modules: +The model contains the following Sail modules in the `model` directory: - `prelude.sail` contains useful Sail library functions @@ -51,9 +77,9 @@ your environment pointing to its top-level directory. ``` $ make ``` -will build the OCaml simulator in `platform`, the C simulator in -`riscv_sim`, the Isabelle model in `Riscv.thy`, and the Coq -model in `riscv.v`. +will build the OCaml simulator in `ocaml/platform`, the C simulator in +`c/riscv_sim`, the Isabelle model in `generated_models/isabelle/Riscv.thy`, and the Coq +model in `generated_models/coq/riscv.v`. Executing test binaries ----------------------- @@ -61,11 +87,11 @@ Executing test binaries The C and OCaml simulators can be used to execute small test RV64 binaries. ``` -$ ./platform <elf-file> -$ ./riscv_sim <elf-file> +$ ./ocaml/platform <elf-file> +$ ./c/riscv_sim <elf-file> ``` Some information on additional configuration options for each simulator is available -from `./platform -h` and `./riscv_sim -h`. +from `./ocaml/platform -h` and `./c/riscv_sim -h`. Booting Linux with the C backend -------------------------------- @@ -77,7 +103,7 @@ a DTB (device-tree blob) file describing the platform (say in the file the model should be run as: ``` -$ ./riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & +$ ./c/riscv_sim -t console.log -b spike.dtb bbl > execution-trace.log 2>&1 & $ tail -f console.log ``` The `console.log` file contains the console boot messages. @@ -88,7 +114,7 @@ Booting Linux with the OCaml backend The OCaml model only needs the ELF-version of the BBL, since it can generate its own DTB. ``` -$ ./platform bbl > execution-trace.log 2> console.log +$ ./ocaml/platform bbl > execution-trace.log 2> console.log ``` Generating input files for Linux boot |