Sail——RISCV-Sail-Model

Learning RISCV Sail Model

Follow the github repository

This repository contains a formal specification of the RISC-V architecture, written in Sail. It has been adopted by the RISC-V Foundations.

Getting started

Building the model

First install Sail via opam

The opam version must be >= 2.0 and we need to check the OCaml version using ocaml -version. If we have OCaml version older than 4.06.1, use opam switch create 4.06.1 (or newer one like 4.10.0). Don't forget to set up the environment for that OCaml version with eval $(opam env) after we change the OCaml version.

Install system dependencies. Finally, intall sail from the opam package and its dependencies. Type this.

1
opam install sail

(If you install sail from source, you need to set SAIL_DIR in the environment pointing to its top-level directory.)

Then:

1
make

One can build either the RV32 or the RV64 model by specifying ARCH=RV32 or ARCH=RV64 on the make line, and using the matching target suffix. RV64 is built by default, but the RV32 model can be built using:

1
ARCH=RV32 make

Executing test binaries

Test binaries like:

1
2
./c_emulator/riscv_sim_RV64 ./test/riscv-tests/rv64ua-p-amoadd_d.elf
./ocaml_emulator/riscv_ocaml_sim_RV64 ./test/risv-tests/rv64ua-p-amoadd.elf