[HOWTO] Build and run seL4 on RISC-V targets

This post gives instructions how to build seL4 to run on RISC-V targets (currently Spike simulator and Rocket Chip/FPGA). The default, and currently only, application is SOS [1] which is a simple operating system running on top of seL4. This means other simple applications can be developed based on this seL4/RISC-V port.

Prerequisites

The development environment is Linux, you need the following tools installed before pursuing with the build/run process:

• riscv32-unknown-elf- [2]
• Spike  [3]
• fesvr [4]
• Python
• git
• gpg

Optional (If you want to build/run seL4 on Rocket Chip/FPGA):

• Xilinx/Vivado 
• Scala
• Chisel

Build/Run seL4/RISC-V

Assuming all the previous packages are installed, the build system (and steps) are exactly the same as of other seL4 projects here [5], but it uses my own repos because the port is not upstream (yet).

1- Get repo

mkdir -p ~/bin
export PATH=~/bin:$PATH
curl https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repo
chmod a+x ~/bin/repo

2- Fetch seL4/RISC-V project
 

The following commands fetche seL4 microkernel, SOS, tools, and all the libraries required to build a complete seL4/RISC-V system (currently SOS project):

mkdir seL4riscv
cd seL4riscv
repo init -u https://github.com/heshamelmatary/sel4riscv-manifest.git

repo sync 

3- Build seL4/RISC-V project
 
The default project is SOS that runs on Spike, RV32 mode, SV32 memory system. First type:

make riscv_defconfig

Make sure ROCKET_CHIP option is  UNCHECKED:

make menuconfig

seL4 kernel > seL4 System

 make

You should find the sos image under images directory.

SOS binary images

 4- Run seL4/RISC-V (SV32) on Spike (and jor1k):

Running SOS on spike is easy, just type the following command and you should see some interesting output (for more details about SOS see [6]):

make simulate-spike

SOS running on seL4 on RISC-V 

seL4/RV32/SV39 (the same image output from the previous steps) can run on jor1k [8], however jor1k for RISC-V is still under development, and may not work properly.

* Build and run seL4/RISC-V (SV39) on Spike/Rocket

Building seL4 for RV64 follows almost the same previous steps, the differences are followed:

1- Assuming you got all the required repos (see steps 1 and 2 above), change the kernel branch to point to sel4Rocket:

cd kernel/
git checkout sel4Rocket
cd ..

2- This time make sure ROCKET_CHIP is CHECKED

make riscv_defconfig
make menuconfig

ROCKET_CHIP config option checked

Save and exit.

3- build and run seL4/RV64/SV39

make 
make simulate-spike64

The same seL4/SV39 image can run on Rocket Chip on FPGA. Just follow the instructions how to build the Rocket Chip on FPGAs [7]. Note that you have to build all the FPGA-related components along with the software tools (zynq-fesvr)  from scratch to get the latest privileged-spec compliant tools (the prebuilt images are not updated).

If you've followed the previous steps and found any issues, just let me know. Your feedback, bug reports, feature-addition requests are welcomed.

References

[1] seL4 on RISC-V is running SOS (Simple Operating System)
[2] https://github.com/riscv/riscv-gnu-toolchain/
[3] https://github.com/riscv/riscv-isa-sim
[4] https://github.com/riscv/riscv-fesvr
[5] http://sel4.systems/Download/
[6] http://www.cse.unsw.edu.au/~cs9242/14/project/framework.shtml
[7] https://github.com/ucb-bar/fpga-zynq
[8] http://jor1k.com/jor1k/demos/riscv.html