Raspberry PI 4 Model B
Serial connection
Serial TX and RX are located at GPIO pins 14 and 15 respectively
U-Boot
Right now, the default U-Boot will not successfully boot an seL4 image on the RPi4 because of cache configuration issues in the seL4 ELFLoader. This problem can be remedied by having U-boot disable caches before loading seL4. Unfortunately, the stock upstream U-boot used to disable caches before loading the kernel image, but as of this patch (https://github.com/u-boot/u-boot/commit/995eab8b5b580b67394312b1621c60a71042cd18), U-boot no longer disables caches.
In order to obtain a U-boot binary that disables caching, you should compile U-Boot from source yourself. You can do this by cloning U-boot from upstream, then reverting commit 995eab8b5b580b67394312b1621c60a71042cd18, and then building it:
git clone https://github.com/u-boot/u-boot.git u-boot
cd u-boot
git revert 995eab8b5b580b67394312b1621c60a71042cd18
make CROSS_COMPILE=aarch64-linux-gnu- rpi_4_defconfig
make CROSS_COMPILE=aarch64-linux-gnu-
This will enable you to get the most up-to-date U-boot which will boot seL4 on the RPi4 successfully.
NOTE: Automatic revert is not going to work if you are using the latest version of u-boot. You need to manually revert the change by looking at the changeset.
SD card setup
The PI boots from the first FAT32 partition on the SD card. Where files are specified, they should be located in the root directory of this partition.
| Stage | Filename | Description | Source |
|---|---|---|---|
| FSBL | - | Mounts SD and loads SSBL | ROM |
| SSBL | bootcode.bin | Loads GPU firmware and boots GPU | https://github.com/raspberrypi/firmware/tree/master/boot |
| GPU firmware | start4.elf | Loads CPU bootloader and boots CPU | https://github.com/raspberrypi/firmware/tree/master/boot |
| Usually the Linux kernel, but could also be u-boot | u-boot.bin | u-boot | Compiled using the instructions above |
| config.txt | u-boot parameters | Add arm_64bit=1, kernel=u-boot.bin, and dtoverlay=disable-bt to the bottom of config.txt |
|
| uboot.env | u-boot saved environment | Generated by u-boot (default environment) bootcmd copied to bootcmd_orig bootcmd and bootdelay removed | |
| bcm2711-rpi-4-b.dtb | RPi4 device tree blob | https://github.com/raspberrypi/firmware/tree/master/boot | |
| overlays/* | Device tree overlays | https://github.com/raspberrypi/firmware/tree/master/boot/overlays |
Getting seL4 onto your Raspberry Pi 4
Because you have applied a device tree overlay to use the UART on GPIO pins 14 and 15,
you will have to update seL4 to use serial0 instead of serial1.
In the kernel at src/plat/bcm2711/overlay-rpi4.dts, you should replace all instances of
serial1 with serial0.
Then, you should then build the kernel, such as in seL4test:
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=rpi4 -DAARCH64=1
# 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.
ninja
Generated binaries can be found in the images/ directory.
The boot method described here is through the SD card. You should set up the files on your SD card as described in the previous section.
Following this, copy your seL4 image (such as an seL4test image) onto the SD card in its root directory. You can now remove the SD card from your PC and re-insert it into the RPi4, and power the RPi4 on.
When the RPi4 boots up, be sure to interrupt the boot process and drop
into the U-boot command prompt. From the U-boot command prompt, type
something like the following: fatls mmc 0. If you don’t see your seL4 image
filename printed out, then you might need to double-check your steps
so far to make sure you didn’t forget something along the way. If you
see your file listed, then do something like:
fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711
bootefi 0x10000000