Embedded Virtualization on RISC-V with seL4

Embedded virtualization is a key enabler for system designers to meet SWaP-C requirements for mission critical systems that execute various military, aerospace, medical, and commercial applications. The demand is now on the software designer to implement high assurance software that can reliably satisfy safety and time critical requirements. This article presents the first public implementation of the formally proven microkernel, seL4, on the RISC-V hypervisor using H-extension v0.6.1. This implementation uses the Rocketchip softcore executing in the FPGA fabric of a Zynq UltraScale+MPSoC ZCU102.