Skip to content

Latest commit

 

History

History
305 lines (233 loc) · 9 KB

Installation.adoc

File metadata and controls

305 lines (233 loc) · 9 KB

Installation Instructions for A Tour of the RISC-V ISA Formal Specification

Contents

1. About this document

This document accompanies the main document for the tutorial “A Tour of the RISC-V ISA Formal Specification”, focusing just on the installation steps needed before starting the tutorial.

Please either take Step A, or take both Steps A and B, depending on your objectives, before starting the tutorial.

Step A

Take this step if you just want to learn how to read and consult the spec. This merely git-clones a certain repository which contains the Sail source code for the RISC-V ISA Formal Spec.

Step B

Take this step if you also want to learn how to execute the spec. This step will compile a RISC-V ISA simulator from the Sail formal spec, which you can use to execute:

  • The standard suite of RISC-V ISA tests

  • The standard RISC-V Compliance Test suite

  • Any RISC-V ELF binary that you create from other source codes

2. Installation Overview

This diagram provides an overview of the various components to be installed.

Fig Installation Overview

3. Step A: Installing for just reading the spec

Ensure you have git installed on your system.

Clone the following repository, which contains the RISC-V ISA Formal Spec in Sail:

    $ git clone https://github.com/rems-project/sail-riscv

What you get:

    $ cd sail-riscv
    $ tree -d
    ├── ...
    ├── ...
    ├── model
    ├── ...
    └── ...

The model directory contains all the spec files.

That’s all you need, for just reading and consulting (not executing) the spec (other than a text editor to view source code)!

4. Step B: Installing for also building executable version of the spec

The tool chain looks like this: opam → OCaml → Sail → Executable version of RISC-V Formal Spec.

  • The RISC-V Formal Spec is written in Sail, a Domain Specific Language (DSL) for ISAs.

  • The compilers that produce executable versions of the spec are written in OCaml, a widely used functional programming language.

  • Opam is the package manager for OCaml

OS requirements

These instructions are for Debian/Ubuntu Linux. If you are running some other OS:

  • You could install a virtual machine running Debian/Linux and follow these instructions.

  • Opam, OCaml and Sail will also install on other OSes. See the Safety net websites (below) for more information.

Safety net: more information on installing opam, OCaml and Sail

The instructions below document are excerpted from:

5. Step B.1: Install opam, the package manager for OCaml

Opam is the OCaml package manager. You can install it using your system’s package manager. E.g., on Ubuntu or Debian:

    $ sudo apt-get install opam

More detailed installation instructions are on the opam website at https://opam.ocaml.org/doc/Install.html.

Your opam version must be >= 2.0.

5.1. Verify successful opam installation

    $ which opam
    /usr/local/bin/opam

    $ opam --version
    2.0.7

6. Step B.2: Install OCaml using opam

6.1. Install OCaml

Environment setup:

    $ opam init
    $ eval $(opam env)

Install specific version of OCaml

    $ opam switch create ocaml-base-compiler.4.06.1
    $ eval $(opam config env)

6.1.1. Verify you’ve got OCaml

    $ which ocaml
    /home/nikhil/.opam/ocaml-base-compiler.4.06.1/bin/ocaml

    $ ocaml -version
    The OCaml toplevel, version 4.06.1
Note

According to https://github.com/rems-project/sail/blob/sail2/INSTALL.md, any version of OCaml from version 4.06.1 or newer is acceptable.

7. Step B.3: Install Sail using opam

7.1. Install Sail

First, please install certain prerequisite libraries needed by Sail (if not already installed on your system):

On Linux (Debian, Ubuntu, …​):

    $ sudo apt-get install build-essential libgmp-dev
    $ sudo apt-get install z3 m4 pkg-config zlib1g-dev
    $ sudo apt-get install git  rsync  unzip
    $ sudo apt-get install device-tree-compiler
    $ sudo apt-get install bubblewrap
Note

The device-tree-compiler is needed by the simulator.

Some people have reported needing bubblewrap on some OSs

Set up opam so it knows where to get Sail:

    $ opam repository add rems https://github.com/rems-project/opam-repository.git

Then, install Sail:

    $ opam install sail

7.2. Verify you’ve got Sail

    $ which sail
    /home/nikhil/.opam/ocaml-base-compiler.4.06.1/bin/sail

    $ sail --help
    Sail 0.13 (sail2 @ opam)
    usage: sail <options> <file1.sail> ... <fileN.sail>

      -o <prefix>                              select output filename prefix
      -i                                       start interactive interpreter
      ...

8. Step B.4: Build RISC-V simulators from the Sail spec

The RISC-V ISA Formal Specification in Sail can be compiled into an executable simulator using which you can execute RISC-V binaries.

Note

The RISC-V specification allows for implementations that simultaneously support both RV32 and RV64, including dynamic switching between these. However, currently the simulators compiled from the Sail Formal Spec must be statically configured for either RV32 or RV64 (this may change in the future).

8.1. Build an RV32 and RV64 RISC-V C-based simulator from the Sail spec

    $ cd sail-riscv
    $ make  ARCH=RV64  csim
    $ make  ARCH=RV32  csim

ARCH=RV64 is the default; you can omit it from the command line.

The make csim command compiles the Sail spec to C and then compiles the C code into the following executabes:

    c_emulator/riscv_sim_RV64
    c_emulator/riscv_sim_RV32

These simulators run fast enough to boot operating systems like FreeRTOS, Linux, FreeBSD, etc. in a few seconds or minutes.

Note

During the builds, you may get some messages about incomplete pattern matches; you can ignore them.
Note

If you omit the csim makefile target, it will build all the targets, which include an OCaml-based simulator and material for Coq, Isabelle, HOL4, …​ (not necessary for this tutorial).

8.1.1. Test-drive your RV64 and RV32 simulators (a smoke test)

Example: executing the rv64ui-p-add standard ISA test in the RV64 simulator:

      $ ./c_emulator/riscv_sim_RV64  test/riscv-tests/rv64ui-p-add.elf
      ...
      tohost located at 0x80001000
      ...
      Running file test/riscv-tests/rv64ui-p-add.elf.
      ELF Entry @ 0x80000000
      ...
      [0] [M]: 0x0000000000001000 (0x00000297) auipc t0, 0
      ...
      [1] [M]: 0x0000000000001004 (0x02028593) addi a1, t0, 32
      ...
      [2] [M]: 0x0000000000001008 (0xF1402573) csrrs a0, zero, mhartid
      ...
      [477] [M]: 0x0000000080000044 (0xFC3F2023) sw gp, 4032(t5)
      ...
      SUCCESS

During execution of the RISC-V binary, it prints out a trace of instructions executed.

Example: executing the rv32ui-p-add standard ISA test in the RV32 simulator:

      $ ./c_emulator/riscv_sim_RV32  test/riscv-tests/rv32ui-p-add.elf
      ...
      tohost located at 0x80001000
      ...
      Running file test/riscv-tests/rv32ui-p-add.elf.
      ELF Entry @ 0x80000000
      ...
      [0] [M]: 0x00001000 (0x00000297) auipc t0, 0
      ...
      [1] [M]: 0x00001004 (0x02028593) addi a1, t0, 32
      ...
      [2] [M]: 0x00001008 (0xF1402573) csrrs a0, zero, mhartid
      ...
      [472] [M]: 0x80000044 (0xFC3F2023) sw gp, 4032(t5)
      ...
      SUCCESS