diff options
-rw-r--r-- | README.md | 64 |
1 files changed, 26 insertions, 38 deletions
@@ -5,10 +5,17 @@ This repository contains a model of the RISCV architecture written in [Sail](https://www.cl.cam.ac.uk/~pes20/sail/). It used to be contained in the [Sail repository](https://github.com/rems-project/sail). -It currently implements enough of RV32IMAC and RV64IMAC to boot a +It currently defines enough of RV32IMAC and RV64IMAC to boot a conventional OS with a terminal output device. The model specifies assembly language formats of the instructions, the corresponding encoders and decoders, and the instruction semantics. +The current status of its +coverage of the prose RISC-V specification is summarized +[here](doc/Status.md). +A [reading guide](doc/ReadingGuide.md) to the model is provided in the +[doc/](doc/) subdirectory, along with a guide on [how to +extend](doc/ExtendingGuide.md) the model. + This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_Public_Review/blob/master/comparison_table.md) compared within the [RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review). @@ -19,48 +26,29 @@ Directory Structure ``` sail-riscv -| -+---- model // Sail specification modules -| -+---- generated_definitions // Files generated by Sail, in RV32 and RV64 subdirectories -| | -| +---- c -| +---- ocaml -| +---- lem -| +---- isabelle -| +---- coq -| +---- hol4 -| +---- latex -| -+---- prover_snapshots // Snapshots of generated theorem prover definitions -| -|---- handwritten_support // Prover support files -| -+---- c_emulator // supporting platform files for C emulator -+---- ocaml_emulator // supporting platform files for OCaml emulator -| -+---- doc // documentation, including a reading-guide -| -+---- test // test files -| | -| +---- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo -| -+---- os-boot // information and sample files for booting OS images +- model // Sail specification modules +- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories + - c + - ocaml + - lem + - isabelle + - coq + - hol4 + - latex +- prover_snapshots // snapshots of generated theorem prover definitions +- handwritten_support // prover support files +- c_emulator // supporting platform files for C emulator +- ocaml_emulator // supporting platform files for OCaml emulator +- doc // documentation, including a reading guide +- test // test files + - riscv-tests // snapshot of tests from the riscv/riscv-tests github repo +- os-boot // information and sample files for booting OS images ``` -Documentation -------------- - -A [reading guide](doc/ReadingGuide.md) to the model is provided in the -[doc/](doc/) subdirectory, along with a guide on [how to -extend](doc/ExtendingGuide.md) the model. The current status of the -coverage of the prose RISC-V specification is summarized -[here](doc/Status.md). - Simulators ---------- -The files in the OCaml and C simulators implement ELF-loading and the +The files in the OCaml and C emulator directories implement ELF loading and the platform devices, define the physical memory map, and use command-line options to select implementation-specific ISA choices. |