I work on getting seL4 virtualization on Raspberry Pi 4 and I had to add few modifications to get the rpi4 in 64bit compiling, booting and passing the official test suite project.
Good new, it’s working, but I needed to relax a restriction (among other thing) in the parsing of dtb file (memory mapping) which seems stricter than necessary.
Explanation: In order to get closer to the final dtb, I retrieved the dynamic dtb from the Linux boot process and used it to get the sel4test test binary on rpi4 with 64bit.
Is there a reason for keeping strictly non overlapping memory region in the dtb mem region parsing?
Second question, would it be interesting for the community to publish the cmake modification we’ve done to get rpi4 running?