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.

opam install sail

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



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:

ARCH=RV32 make

Executing test binaries

Test binaries like:

./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