Various fixes and improvements to RPi4 docs

Hardware/Rpi4.md

@@ -1,7 +1,7 @@
 ---
 arm_hardware: true
 cmake_plat: rpi4
-xcompiler_arg: -DAARCH64=1
+xcompiler_arg: -DAARCH64=1 -DRPI4_MEMORY=<1024,2048,4096,8192>
 platform: Raspberry Pi 4B
 arch: ARMv8A
 virtualization: ARM HYP
@@ -18,79 +18,73 @@ SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
 # Raspberry Pi 4 Model B
 
 ## Serial connection
-Serial TX and RX are located at GPIO pins 14 and 15 respectively
+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:
+In order to build U-Boot for the Raspberry Pi 4B, run the following commands:
 ```bash
 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-
 ```
 
+More information regarding U-Boot support for the Raspberry Pi can be found [here](https://u-boot.readthedocs.io/en/latest/board/broadcom/raspberrypi.html).
+
 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.
+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 |
+|Usually the Linux kernel, but could also be u-boot |u-boot.bin |U-Boot binary| 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`.
+The final step to test that you have setup your RPi4 correctly is to build and run the
+seL4test project.
 
-Then, you should then build the kernel, such as in seL4test:
+You will see that the `init-build.sh` command contains the flag
+`-DRPI4_MEMORY`, this specifies how much RAM exists on the Raspberry Pi that will run
+the final seL4 image. Since seL4 needs to know the physical memory layout of the hardware
+at build time, and the RPi4 has multiple models with different amounts of RAM, we have to
+specify how much RAM the system will have when we build seL4.
 
 {% include sel4test.md %}
 
-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.
+Now that we have a bootable image, we can run it on your RPi4. The following instructions describe
+how to use a microSD card to boot seL4, using the seL4test image as well as the files mentioned
+in the previous section.
+
+The first step is to copy the seL4 image onto the microSD card to the root directory. After
+removing the card from your computer and insterting into your RPi4, you can power on the RPi4.
+
+Once the RPi4 boots up, you will something like the following text from U-Boot:
+```
+Hit any key to stop autoboot:  2
+```
+
+At this point you want to interrupt the U-Boot booting process by pressing any key.
+
+You will now be in the U-Boot command prompt, type the following command:
+```
+fatls mmc 0
+```
 
-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.
+You should see the seL4test image you just placed on your microSD card.
 
-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:
+From here, you can load and boot the image using:
 ```
 fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711
 go 0x10000000