diff options
Diffstat (limited to 'snapshots/coq-riscv/README.md')
| -rw-r--r-- | snapshots/coq-riscv/README.md | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/snapshots/coq-riscv/README.md b/snapshots/coq-riscv/README.md deleted file mode 100644 index 5219c3b8..00000000 --- a/snapshots/coq-riscv/README.md +++ /dev/null @@ -1,14 +0,0 @@ -# Sail RISC-V model for Coq - -This directory contains the Coq files for the Sail RISC-V model, in -`sail/riscv`, along with the Sail Coq library (`sail/lib/coq`) and the -MIT BBV library for bitvector support. The `build` script checks all -of the files, and `clean` removes the generated files. The main model -is in `sail/riscv/riscv.v`. - -The Coq version of the model was generated from the Sail sources -available at <https://github.com/rems-project/sail/tree/sail2/riscv>, -commit `9e9506a582763f7ad4c6c8c57dc514d9fb89b9df`, and were manually -patched to deal with parts of the model that the tool does not fully -deal with, mostly due to recursive functions. The manual changes can -be found in `sail/riscv/coq.patch`. |