This is a guide to setting up the 64-bit RISC-V tools and running the seL4 test suite for the Spike platform (the standard RISC-V simulator provided by UC Berkeley), via QEMU.

Running seL4test on RISC-V


Make sure the standard seL4 dependencies are installed.

The following packages are required for the RISC-V tools:

autoconf automake autotools-dev curl libmpc-dev libmpfr-dev libgmp-dev libusb-1.0-0-dev gawk build-essential bison flex texinfo gperf libtool patchutils bc zlib1g-dev device-tree-compiler pkg-config
libglib2.0-dev zlib1g-dev libpixman-1-dev

On Ubuntu, these can be obtained with apt.

Build the tools

  1. Set up a directory for the RISC-V tools, and the RISCV environment variable, which we refer to in future steps.

     mkdir riscv
     cd riscv
     export RISCV=${PWD}
  2. Get the RISC-V tools

     cd ${RISCV}
     git clone https://github.com/riscv/riscv-tools.git
     cd riscv-tools
     git submodule update --init --recursive
  3. Get RISC-V qemu sources, and build them:

     cd ${RISCV}/riscv-tools
     git clone https://github.com/heshamelmatary/riscv-qemu.git
     cd riscv-qemu
     git checkout sfence
     git submodule update --init dtc
     ./configure --target-list=riscv64-softmmu,riscv32-softmmu --prefix=${RISCV}
     make -j8 && make install
  4. Build the 64-bit toolchain, this will take an hour or two.

     cd ${RISCV}/riscv-tools
     sed -i 's/build_project riscv-gnu-toolchain --prefix=$RISCV/build_project riscv-gnu-toolchain --prefix=$RISCV --with-arch=rv64imafdc --with-abi=lp64 --enable-multilib/g' ./build.sh

    If you are using a recent distribution like Ubuntu 18.04 you may need to disable -Wall (turn compiler warning into errors) in riscv-openocd and riscv-isa-sim.

    After it is built, add the $RISCV/bin folder to your path for step 6.

  5. (Optional) Build the 32-bit toolchain, this will also take an hour or two.

     cd ${RISCV}/riscv-tools

Running seL4 test

You will need to make sure that $RISCV/bin has been added to your PATH.

Checkout the sel4test project using repo as per seL4Test

repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync
mkdir cbuild
cd cbuild
../init-build.sh -DPLATFORM=spike -DRISCV64
# The default cmake wrapper sets up a default configuration for the target platform.
# To change individual settings, run `ccmake` and change the configuration
# parameters to suit your needs.
# If your target binaries can be executed in an emulator/simulator, and if
# our build system happens to support that target emulator, then this script
# might work for you:

If you plan to use the ./simulate script, please be sure to add the -DSIMULATION=1 argument when running cmake.

Generated binaries can be found in the images/ directory.

You can also use run the tests on the 32-bit spike platform by
replacing the `-DRISCV64=TRUE` option with `-DRISCV32=TRUE`.

Continuing development

For further development, you only need to rebuild sel4test and rerun qemu, repeating step 6 above.