在 Raspberry Pi 5 上运行

需要购买什么，如何构建和写入 SD 卡，如何读取和检查开发板的串口日志，以及如何在无人值守的情况下在 Pi 5 上运行系统，或在其 HDMI 屏幕上观看用户界面。

Raspberry Pi 5 是 NoWayOS 的参考开发板：成本低、容易买到，也是它首批硬件测试所用的开发板。在 QEMU 中通过测试的系统，会根据开发板的串口日志，在 Pi 上对照同一个预期文件进行检查。

使用开发板的两条规则。 切勿把 5 V 串口适配器连接到 Pi 的 UART：它是 3.3 V 端口。也切勿在开发板上烧写 Pi 的一次性可编程存储器或启用安全启动：两者都不可逆。make sdcard 会拒绝任何会执行其中一项操作、或会改变开发板电压的 config.txt。

您需要准备什么

物品	说明
Raspberry Pi 5	在 16 GB 版本的开发板上开发和测试。每条命令都把开发板命名为 `rpi5b_2gb`：这是 seL4 针对 Pi 5 的配置，使用其前 2 GB 内存，构建会把其中略少于 1 GB 的内存分给 seL4。因此，2 GB、4 GB 和 8 GB 版本的开发板应该无需任何改动，但尚未试过
电源	官方 5 V、5 A USB-C 电源，或同等品质的电源。供电不足的 Pi 5 表现得就像有软件缺陷一样
microSD 卡	用于存放 `make sdcard` 构建的启动分区
Raspberry Pi Debug Probe	它的 UART 线缆可接入 Pi 5 的 3 针调试接口。任何配有合适线缆的 3.3 V USB 转串口适配器也都可以
HDMI 显示器、USB 键盘和鼠标	用于用户界面。请在开机前连接显示器：固件只在启动时设置屏幕。采用 USB 引导协议的键盘和鼠标可以使用；集线器尚不支持

构建 SD 卡

make sdcard BOARD=rpi5b_2gb SYSTEM=hello

这会把 SD 卡的启动分区写入 build/rpi5b_2gb/hello/sdcard/：U-Boot、设备树及其覆盖层、config.txt、seL4 镜像 loader.img、许可证文件，以及一个用于事后检查 SD 卡的 SHA256SUMS。U-Boot 在容器中从源码构建，可重现。

写入 SD 卡

在 macOS 上

用 diskutil list 找到这张卡：它标注为 external, physical，大小与卡的容量一致。下一步会抹掉整张磁盘，所以请仔细核对两遍编号。
格式化它，卷标设为 PIBOOT：

diskutil eraseDisk FAT32 PIBOOT MBRFormat /dev/diskN

复制文件，并检查每个文件是否完整送达（全部匹配时，这些命令不会输出任何内容）：

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$')

用 diskutil eject /dev/diskN 推出它，然后插入 Pi。

在 Linux 上

用 Linux 的工具执行同样的步骤（本项目自己的 SD 卡是在 macOS 上制作的）：

用 lsblk -p 找到这张卡：一个与卡容量相同的磁盘，例如 /dev/sdX 或 /dev/mmcblk0。下一步会抹掉整张磁盘，所以请仔细核对两遍名称，并卸载它的所有分区。
为它创建一个 FAT32 分区，卷标设为 PIBOOT（需已安装 dosfstools 和 parted）：

sudo parted --script /dev/sdX mklabel msdos mkpart primary fat32 1MiB 100% set 1 lba on
sudo mkfs.vfat -F 32 -n PIBOOT /dev/sdX1

复制文件，并检查每个文件是否完整送达（全部匹配时，这些命令不会输出任何内容）：

sudo mount /dev/sdX1 /mnt
sudo cp -r build/rpi5b_2gb/hello/sdcard/. /mnt/
(cd /mnt && sha256sum -c SHA256SUMS | grep -v ': OK$')
sudo umount /mnt

把它插入 Pi。

连接串口控制台

把 Debug Probe 插到 Pi 5 位于两个 HDMI 端口之间的专用 3 针调试接口上，而不是插到 GPIO 引脚上。它的参数是 115200 波特，8N1。探针在 Mac 上显示为 /dev/cu.usbmodem…，在 Linux 上显示为 /dev/ttyACM0 或类似名称（您的用户需要属于 dialout 组）。

请在给 Pi 通电之前开始捕获，每次启动对应一份日志：

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

请像这里一样，把设置和读取放在同一条命令中：在 macOS 上，第二次打开该端口时会退回到 9600 波特。在 Linux 上，用 stty -F /dev/ttyACM0 115200 raw -echo 设置端口，再用 cat /dev/ttyACM0 读取。在最后一行预期输出出现后，按 Ctrl-C 停止。

通电后，U-Boot 会倒数三秒，然后启动卡上的 loader.img。如果想停在它的提示符处，请在倒数期间输入 stopboot。（只有这个词能让它停下，因此未连接的串口线上拾取的噪声永远不会把设备卡在 U-Boot。）

检查日志

按照检查 QEMU 输出的同一套规则，对照系统的预期文件检查开发板的日志：

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

如果某个系统有专门针对 Pi 的预期文件，请加上 BOARD=rpi5b_2gb。

无人值守地运行系统

连接探针后，make pi-run 会在开发板上运行一系列系统，既不用来回插拔 SD 卡，也不需要有人守在开发板旁。请直接在您的机器上运行它，而不是在容器中（在 Mac 上，Podman 的虚拟机看不到 USB 串口设备）。它需要您的机器上装有 Python 3.11 或更高版本，只用到标准库：

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

对于每个系统，它都会在容器中构建镜像、复位开发板、通过串口线发送镜像并检查其是否完整送达、启用开发板的看门狗，然后启动系统。每份日志在接收时即被检查，随后由看门狗复位开发板，以运行下一个系统。它输入的每条命令都会被回显，并在执行前经过检查。日志保存在 build/rpi5b_2gb/pi-run/ 中。

观看用户界面

在开机前连接好显示器，然后运行：

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

这会在 HDMI 屏幕上运行用户界面的脚本化会话，并检查每一帧的哈希值。如果想让某个系统一直运行、供人观看，且不启用看门狗，请使用 make pi-show PI_DEVICE=… SYSTEM=ui-demo；它会一直运行，直到开发板断电重启。

出问题时

先回到上一个能正常工作的镜像，重新检查串口线和启动链，不要一次改动多处。如果在 U-Boot 之前什么都没有出现，请先检查引导加载程序的 BOOT_UART 设置以及卡上 config.txt 中的 enable_uart=1，再怀疑探针或接线。