Running on a Raspberry Pi 5

The Raspberry Pi 5 is NoWayOS's reference board: low-cost, widely available, and the board its first hardware tests run on. A system that passes in QEMU is checked on the Pi against the same expect file, from the board's serial log.

Two rules for the board. Never connect a 5 V serial adapter to the Pi's UART: it is a 3.3 V port. And never program the Pi's one-time-programmable memory or enable secure boot on a development board: both are irreversible. make sdcard refuses a config.txt that would do either, or that changes the board's voltage.

What you need

Build the SD card

make sdcard BOARD=rpi5b_2gb SYSTEM=hello

This writes the card's boot partition to build/rpi5b_2gb/hello/sdcard/: U-Boot, the device tree and overlays, config.txt, the seL4 image loader.img, the licence files and a SHA256SUMS for checking the card afterwards. U-Boot is built from source in the container, reproducibly.

Write the card (macOS)

1. Find the card with diskutil list: it is external, physical, and the card's size. The next step erases that whole disk, so check the number twice.
2. Format it, labelled PIBOOT:

diskutil eraseDisk FAT32 PIBOOT MBRFormat /dev/diskN

3. Copy the files, and check every one arrived intact (this prints nothing when they all match):

cp -RX build/rpi5b_2gb/hello/sdcard/ /Volumes/PIBOOT/
dot_clean -m /Volumes/PIBOOT
(cd /Volumes/PIBOOT && shasum -a 256 -c SHA256SUMS | grep -v ': OK$')

4. Eject it with diskutil eject /dev/diskN, and put it in the Pi.

Connect the serial console

Plug the Debug Probe into the Pi 5's dedicated 3-pin debug connector, between the HDMI ports, not into the GPIO pins. It runs at 115200 baud, 8N1, and the probe appears on the Mac as /dev/cu.usbmodem….

Start capturing before you power the Pi on, one boot per log:

mkdir -p build/rpi5b_2gb/hello
(stty 115200 raw -echo; cat) < /dev/cu.usbmodemXXXX | tee build/rpi5b_2gb/hello/serial.log

Keep the settings and the read on one command, as here: on macOS a second open of the port falls back to 9600 baud. Stop with Ctrl-C after the last expected line.

At power-on, U-Boot counts down three seconds and then boots the card's loader.img. To stop at its prompt instead, type stopboot during the countdown. (Only that word stops it, so the noise an unconnected serial line picks up can never hold a device at U-Boot.)

Check the log

Check the board's log against the system's expect file, by the same rules QEMU's output is checked by:

make check-serial SYSTEM=hello LOG=build/rpi5b_2gb/hello/serial.log

Add BOARD=rpi5b_2gb for a system with an expect file of its own for the Pi.

Run systems unattended

With the probe attached, make pi-run runs a series of systems on the board with no card to move and nobody at the board. Run it on the Mac itself (Podman's virtual machine cannot see USB serial devices), with Python 3.11 or later:

make pi-run PI_DEVICE=/dev/cu.usbmodemXXXX PI_SYSTEMS="hello ipc-demo isolation-test"

For each system it builds the image in the container, resets the board, sends the image over the serial line and checks it arrived intact, arms the board's watchdog, and starts it. Each log is checked as it arrives, and the watchdog resets the board for the next. Every command it types is echoed back and checked before it is entered. Logs are kept in build/rpi5b_2gb/pi-run/.

Watch the user interface

With the monitor attached before power-on:

make pi-run PI_DEVICE=/dev/cu.usbmodemXXXX PI_SYSTEMS=ui-demo PI_WATCHDOG=15

runs the user interface's scripted session on the HDMI screen and checks a hash of every frame. To leave a system running for a person to watch, with no watchdog, use make pi-show PI_DEVICE=… SYSTEM=ui-demo; it runs until the board is power-cycled.

When something fails

Go back to the last image that worked, and check the serial line and the boot chain again, before changing more than one thing at a time. If nothing at all appears before U-Boot, check the bootloader's BOOT_UART setting and enable_uart=1 in the card's config.txt before suspecting the probe or the wiring.