Use the repo tool to get the code from a manifest and start building:
These instructions will download the tools and code required to build the seL4 kernel and the seL4 test suite. This directory will be referred to as the workspace.
The manifest does not, however, install a toolchain to build the code. For this, Data 61 does maintain a Docker image that contains all of the necessary development packages and cross compiling toolchains.
Clone this repository into the
tools directory of your workspace:
If you would also like to build a bootable SD card, the following packages need to be added to the
apt-get command in
extras.dockerfile in order to build u-boot:
and the following line needs to be appended at the end:
I like to create a script in the root of my workspace called
container-env.sh that has the following contents:
I like to open two terminals at this point. In this situation, I can have my container environment in one terminal and my development tools on my host machine accessible in the other. In the terminal that the
container-env.sh file was sourced, run the
start-container command. You should be dropped into a shell prompt, where you should also see the directory structure of your workspace.
Here, we will create a build directory and call the
init-build.sh script to configure and kick off the build:
If you also want to build a bootable SD card, add the following line to the command:
The image will now be located in
<Workspace Root>/build-polarfire/images/sel4test-driver-image-riscv-polarfire. The image that is created is actually the
kernel, and user space
sel4test application all rolled into one. This is not a bootable image just yet though.
To run on the Renode emulator, we have to build a slightly different version of our image. The bootloader used on the board is a little more advanced and not yet directly supported by the seL4 build system. However, the Berkly Bootloader (BBL) is. Create a new build directory and run the same
init-build.sh command as before but this time we will use slightly different options:
Here, we changed the
ElfloaderImage option from
elf and added the
-DUseBootEnv“bbl”= to the options. This will bundle everything we had before into a payload for the BBL. We are now ready to use Renode.
Create a file called
sel4test-polarfire.resc in the root of your workspace and fill it with the following contents:
Make sure that the
dtb variables point to the actual files. You can now run
You should now see the Renode monitor window come up. Type
start here and press Enter. You will see more terminal windows pop up. You should see the kernel printing in one and the user space code in the other.
First we must make a bootable SD card image. This can be done by running the
make_polarfire_sd_card found in the build directory. Insert an SD card and run the script as follows, making sure to change the device path to the path of your SD card:
If the script was successful, you should see a
Success! message at the end. You can now remove the SD card and insert it into the PolarFire SoC board.
First we must make a bootable SD card image. This requires using Yocto. Yocto is out of the scope of this tutorial but follow the directions located at the PolarFire SoC Yocto BSP site. Build the SD card image and follow the instructions for using
dd to write the
wic.gz image to the SD Card. Copy your
sel4test image that you build to the
boot partition as
Ensure that the PolarFire SoC board is configured to boot from an SD Card and insert the SD card. At this point I like to use
tmux to split a terminal into 4 parts and then use
tio to connect each pane to a serial device. I run the following command to achieve this:
When you power on the board, you should see the Hart Software Services boot up in the upper left terminal. This is the software running on the monitor core. The upper right terminal will show the output from U-Boot. Make sure that you are ready with tmux to select this pane. The lower left pane will show the output from the kernel, while the last pane will show the output from the user space seL4 test application suite. When the board powers on be sure to interrupt the U-boot sequence and enter the following
If using the SD card built with the
make_polarfire_sd_card script, use the following
fatload command instead:
You should see debug statements printing on the kernel terminal and test output in the lower right.
A success full test run shows “All is well in the universe” at the end.
We have a few rough edges to sand down here. First, we are working on adding functionality to the build system to make building a bootable image without yocto easy from the current build system. Second, We are working on a timer driver for the PolarFire SoC. Lastly, the platform support for the PolarFire SoC is under review by Data 61 for inclusion upstream. When the patches are accepted upstream, the only difference to these instructions will be the original
sel4test-manifest link that was used.
Created: 2020-09-17 Thu 08:43