Major updates since 2015
- - It's now based on seL4's master (rather than experimental) branch, which means it makes use of architecture-independent verified code.
- - Instead of earlier 32-bit support, it's now based on 64-bit RISC-V.
- - Compatible with latest RISC-V priv-1.10 and user-2.2/3 specs.
- - sel4test and libraries are ported and passing 146/146 tests.
- - Tested on Spike and Rocket Chip on FPGA soft-float (also previous version worked with QEMU 1.9.1).
- - Implements seL4's fastpath support.
- - 3 page mappings are supported (Sv39: 4KiB, 2MiB and 1GiB).
- - Relies on SBI from unmodified riscv-pk/bbl to emulate M-mode (same as riscv-linux).
Work in progress
- - Upstreaming seL4/RISC-V port.
- - Multicore support.
- - Research-wise, I've been working on adding CHERI support to RISC-V (Spike) as an extension, and aiming to experiment seL4 on it.
- - Upstream the kernel (and libraries).
- - Add debug and benchmark support.
- - Release sel4bench.
- - Port sel4-tutorial to RISC-V (Start Guide for new comers/learners).
- - External interrupt handling and work with PLIC.
Quick How to
- Install riscv64 tools (priv-1.10)
- Get sel4test/RISC-V (using repo, for more info see )
- $repo init -u email@example.com:heshamelmatary/sel4riscv-manifest.git -m sel4test-03062017.xml
- $make riscv_defconfig && $make
- build riscv-pk/bbl with path to images/sel4test-driver-image-riscv-spike (from 4)
- run spike with bbl image generated from 5.
|sel4test/RISC-V running on Spike|