Hi, The kernel supports and formally verifies bcm2711, but libsel4vm doesn't build for it: gicv2.h has no GIC_PADDR branch, and libsel4vmmplatsupport has no plat_include/bcm2711. I have a small patch (2 lines in gicv2.h, 2 new headers) that I've been using to run VMs on a Raspberry Pi 4B, single-core and 4-core SMP. GIC_PADDR is 0xff840000 — the ARM view of the GIC-400; the rpi4 DTS gives the VideoCore view, and the ARM addresses come from the kernel's generated devices_gen.h. The same value appears in tiiuae's rpi4 branch, derived independently. Before opening a PR I wanted to ask about direction. I see #83 proposes reading these addresses from the device tree, and #58 (GICv3 emulation) has cleanup PRs held back pending it. Is adding another per-platform #elif still acceptable, or would you rather this waited? Two caveats: there's no upstream VM application for this board, so nothing in CI would exercise it; and the vpci.h values are taken from tiiuae's branch — my guests are bare-metal and exercise no PCI path, so I haven't verified them. Happy to rework or drop it. git show bcm2711-platform-support commit ef8f6257ef17a457df075154e81353e6b1eeb39a (HEAD -> bcm2711-platform-support) Author: Shankaraditya N S <shankaradi1511@gmail.com> Date: Tue Sep 8 20:21:58 2026 +0530 libsel4vm/libsel4vmmplatsupport: add BCM2711 (Raspberry Pi 4B) support Signed-off-by: Shankaraditya N S <shankaradi1511@gmail.com> diff --git a/libsel4vm/src/arch/arm/vgic/gicv2.h b/libsel4vm/src/arch/arm/vgic/gicv2.h index c801b88..aa3c831 100644 --- a/libsel4vm/src/arch/arm/vgic/gicv2.h +++ b/libsel4vm/src/arch/arm/vgic/gicv2.h @@ -24,6 +24,8 @@ #define GIC_PADDR 0xc4300000 #elif defined(CONFIG_PLAT_ZYNQMP) #define GIC_PADDR 0xf9000000 +#elif defined(CONFIG_PLAT_BCM2711) +#define GIC_PADDR 0xff840000 #elif defined(CONFIG_PLAT_STM32MP2) #define GIC_PADDR 0x4ac00000 #else diff --git a/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/guest_vcpu_util.h b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/guest_vcpu_util.h new file mode 100644 index 0000000..4ad9935 --- /dev/null +++ b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/guest_vcpu_util.h @@ -0,0 +1,9 @@ +/* + * Copyright 2026, Shankaraditya N S + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#pragma once + +#define PLAT_CPU_COMPAT "arm,cortex-a72" diff --git a/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/vpci.h b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/vpci.h new file mode 100644 index 0000000..07acc59 --- /dev/null +++ b/libsel4vmmplatsupport/plat_include/bcm2711/sel4vmmplatsupport/plat/vpci.h @@ -0,0 +1,23 @@ +/* + * Copyright 2022, Technology Innovation Institute + * + * SPDX-License-Identifier: BSD-2-Clause + */ + +#pragma once + +/* PCI host bridge configuration space */ +#define PCI_CFG_REGION_ADDR 0x100000000ULL +/* PCI host bridge IO space */ +#define PCI_IO_REGION_ADDR 0x101000000ULL +/* Size of PCI configuration space */ +#define PCI_CFG_REGION_SIZE 0x1000000 +/* Size of PCI IO space */ +#define PCI_IO_REGION_SIZE 0x10000 +/* PCI memory space */ +#define PCI_MEM_REGION_ADDR 0x60000000ULL +/* PCI memory space size */ +#define PCI_MEM_REGION_SIZE 0x60000000 + +/* FDT IRQ controller address cells definition */ +#define GIC_ADDRESS_CELLS 0x1 (END)