Microchip PolarFire Icicle Kit status

New to seL4
21

Thanks so much for your help!

The change to the kernel did work. I saw hello world with no errors or warnings.

Booting with the dtb without the the overlay did not work. I rebuilt the sdk against the the sel4cp-dev branch without your recommended changes and booted in qemu using the dtb I compiled. I saw:

Booting all finished, dropped to user space
seL4 failed assertion 'refill_ready(thread->tcbSchedContext)' at /host/seL4/src/kernel/thread.c:447 in function switchToThread
halting...
Kernel entry via Interrupt, irq 0
22

I recently updated the seL4 kernel that my fork of seL4CP uses to be synced with the current master of the mainline kernel. This includes a commit (Read time directly on RISC-V platforms · seL4/seL4@6904039 · GitHub) by myself that seems to be the culprit, as removing the line set(KernelRiscvUseClintMtime ON) from the Polarfire’s config.cmake causes hello, world to be printed.

I’ll have to investigate more, apologies for the inconvenience. In the meantime if you use the previous version of the SDK Fix QEMU ARM virt hello.system · Ivan-Velickovic/sel4cp@086acc1 · GitHub, everything should work fine.

If you could also test the image that doesn’t work on hardware, that would be great, as it would confirm whether QEMU is the issue.

23

I have three separate questions.

seL4cp for cortex_a53

I tried building and booting the sel4cp for the qemu_virt_arm board and for the zcu102 and boot the resulting files on the generic cortex_a53 emulation in on Renode. The ZCU102 don’t even start to boot. The qemu_virt_arm gets a little ways.

I found that the loader.img file is not recognized by any of the load options in Renode. Instead I tried loading all of the individual ELF files like this:

sysbus LoadELF @/home/esandberg/projects/sel4/hans-sel4/cortex-a53/renode-14/sel4cp/qemu_virt/loader.elf
sysbus LoadSymbolsFrom @/home/esandberg/projects/sel4/hans-sel4/cortex-a53/renode-14/sel4cp/qemu_virt/kernel.elf
sysbus LoadSymbolsFrom @/home/esandberg/projects/sel4/hans-sel4/cortex-a53/renode-14/sel4cp/qemu_virt/kernel.elf

but I am getting this error :

LDR|INFO: altloader for seL4 starting
LDR|ERROR: mismatch on loader data structure magic number

I think that is because I am not specifying the loader link address, but I don’t have the option to do so when I use direct kernel boot instead of u-boot. I tried stripping the elf files into dat files like this:

arm-linux-gnueabi-objcopy -O binary hello.elf hello.bin
arm-linux-gnueabi-objcopy -O binary kernel.elf kernel.bin
arm-linux-gnueabi-objcopy -O binary loader.elf loader.bin

Thinking that might remove references to the loader link address. The conversion causes Renode to no longer recognizes the files. If you have suggestions to try I would like to hear them. Also could point me to where the file format is chosen so I could create an elf file that combines the loader, the kernel and the example? I think an ELF would be better recognized by Renode.

seL4cp for for polarfire in QEMU

I tried the commit you mentioned. Still having trouble in QEMU. I see this now:

Booting all finished, dropped to user space
MON|INFO: seL4 Core Platform Bootstrap
MON|INFO: bootinfo untyped list matches expected list
MON|INFO: Number of bootstrap invocations: 0x00000009
MON|INFO: Number of system invocations:    0x00000021
seL4 failed assertion 'NODE_STATE(ksCurTime) < MAX_RELEASE_TIME' at /host/seL4/include/kernel/thread.h:235 in function updateTimestamp
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 2, Invocation tag: 1

seL4cp for for polarfire on hardware

You asked me to try to boot on the hardware. Perhaps you can advise on how to do that as well. I am able to boot into u-boot and from there I should be able to boot your loader.img. To do so I think I need to convert it to a u-boot image. I tried to adapt the instructions I pointed to above for sel4test on the polarfire:

mkimage -A riscv -O linux -T kernel -C none -a 0x80000000 -e 0x80000000 -n sel4test -d \
images/sel4test-driver-image-riscv-polarfire images/seL4-uImage
cp kernel/kernel.dtb images/

but I am unsure what to use for the load address (-a) and entry point (-e). Would the “Domain1 Next Address” in the below output be the load address? How would I find the entry point?

OpenSBI v1.2
   ____                    _____ ____ _____
  / __ \                  / ____|  _ \_   _|
 | |  | |_ __   ___ _ __ | (___ | |_) || |
 | |  | | '_ \ / _ \ '_ \ \___ \|  _ < | |
 | |__| | |_) |  __/ | | |____) | |_) || |_
  \____/| .__/ \___|_| |_|_____/|____/_____|
        | |
        |_|

Platform Name             : Microchip PolarFire(R) SoC
Platform Features         : medeleg
Platform HART Count       : 5
Platform IPI Device       : aclint-mswi
Platform Timer Device     : aclint-mtimer @ 1000000Hz
Platform Console Device   : mmuart
Platform HSM Device       : mpfs_hsm
Platform PMU Device       : ---
Platform Reboot Device    : mpfs_reset
Platform Shutdown Device  : mpfs_reset
Firmware Base             : 0xa000000
Firmware Size             : 144 KB
Runtime SBI Version       : 1.0

Domain0 Name              : root
Domain0 Boot HART         : 1
Domain0 HARTs             : 1,2,3,4
Domain0 Region00          : 0x0000000002008000-0x000000000200bfff (I)
Domain0 Region01          : 0x0000000002000000-0x0000000002007fff (I)
Domain0 Region02          : 0x000000000a000000-0x000000000a03ffff ()
Domain0 Region03          : 0x0000000000000000-0xffffffffffffffff (R,W,X)
Domain0 Next Address      : 0x0000001000200000
Domain0 Next Arg1         : 0x0000000000000000
Domain0 Next Mode         : S-mode
Domain0 SysReset          : yes

Domain1 Name              : u-boot.bin
Domain1 Boot HART         : 1
Domain1 HARTs             : 1*,2*,3*,4*
Domain1 Region00          : 0x000000000a000000-0x000000000a03ffff ()
Domain1 Region01          : 0x0000000000000000-0xffffffffffffffff (R,W,X)
Domain1 Next Address      : 0x0000001000200000
Domain1 Next Arg1         : 0x0000000000000000
Domain1 Next Mode         : S-mode
Domain1 SysReset          : yes

Boot HART ID              : 1
Boot HART Domain          : u-boot.bin
Boot HART Priv Version    : v1.10
Boot HART Base ISA        : rv64imafdc
Boot HART ISA Extensions  : none
Boot HART PMP Count       : 16
Boot HART PMP Granularity : 4
Boot HART PMP Address Bits: 36
Boot HART MHPM Count      : 2
Boot HART MIDELEG         : 0x0000000000000222
Boot HART MEDELEG         : 0x000000000000b109
24

Renode

I have not looked into using Renode for seL4CP, I am mainly waiting for it to be more mature as I’ve had various issues with it (see GitHub - Ivan-Velickovic/sel4_renode: Simulating seL4 projects with Renode).

You can load binary files in Renode, for example: sysbus LoadBinary @../tmp_build/loader.img 0x70000000. Note that you will also need to set the program counter to where the image is loaded, so in this case cpu PC 0x70000000.

Unfortunately I have Renode working with seL4CP in the non-hypervisor case, but not when hypervisor mode is turned on, which is the default configuration in my seL4CP fork for the QEMU ARM virt platform. I don’t have time to investigate right this moment. But given that QEMU and hardware where seL4 is configured in hypervisor mode work, I suspect either this is a bug in Renode or a misconfiguration on my part.

The full platform description is here:

cpu: CPU.ARMv8A @ sysbus
    cpuType: "cortex-a53"
    genericInterruptController: gic

timer: Timers.ARM_GenericTimer @ cpu
    frequency: 62500000
    EL3PhysicalTimerIRQ -> gic#0@29
    EL1PhysicalTimerIRQ -> gic#0@30
    EL1VirtualTimerIRQ -> gic#0@27
    NonSecureEL2PhysicalTimerIRQ -> gic#0@26
    NonSecureEL2VirtualTimerIRQ -> gic#0@28

gic: IRQControllers.ARM_GenericInterruptController @ {
        sysbus new Bus.BusMultiRegistration { address: 0x8000000; size: 0x010000; region: "distributor" };
        sysbus new Bus.BusMultiRegistration { address: 0x8010000; size: 0x010000; region: "cpuInterface" }
    }
    [0-1] -> cpu@[0-1]
    architectureVersion: IRQControllers.ARM_GenericInterruptControllerVersion.GICv2
    supportsTwoSecurityStates: true

flash: Memory.MappedMemory @ sysbus 0x0
    size: 0x08000000

bl31: Memory.MappedMemory @ sysbus 0x0e000000
    size: 0x01000000

ram: Memory.MappedMemory @ sysbus 0x40000000
    size: 0x80000000

uart0: UART.PL011 @ sysbus 0x09000000
    -> gic@1

The full script is here:

:name: QEMU ARM virt
:description: This script runs QEMU ARM virt seL4CP image on a 64-bit ARM Cortex-A53.

using sysbus
$name?="ARM Cortex-A53"
mach create $name

machine LoadPlatformDescription @qemu_arm_virt.repl

showAnalyzer uart0

macro reset
"""
    uart0 WriteDoubleWord 0x30 0x301
    uart0 WriteDoubleWord 0x2c 0x40
    cpu SetAvailableExceptionLevels true false
    cpu PC 0x70000000
    sysbus LoadBinary @../tmp_build/loader.img 0x70000000
"""
runMacro $reset

I ran Renode with the following command:
renode -e "start @qemu_arm_virt.resc" --console

Polarfire on QEMU

These are the clearest instructions I can produce for getting it working on my end. I am using the same QEMU version as you.

# Current latest SDK
unzip sel4cp-sdk-dev-d509be2-linux-x86-64.zip
tar xf sel4cp-sdk-1.2.6.tar.gz
cd sel4cp-sdk-1.2.6/board/polarfire/example/hello
git clone git@github.com:seL4/seL4.git
dtc -I dts -O dtb seL4/tools/dts/mpfs_icicle.dts > mpfs_icicle.dtb
mkdir build
make BUILD_DIR=build SEL4CP_SDK=../../../../ SEL4CP_BOARD=polarfire SEL4CP_CONFIG=debug
qemu-system-riscv64 -M microchip-icicle-kit -smp 5 -m 2G -display none -serial stdio -serial null -serial null -kernel build/loader.img -dtb mpfs_icicle.dtb

Polarfire on hardware

It is not necessary to convert the loader.img file. By the log it looks like the booting process for Polarfire is OpenSBI → U-Boot → seL4/seL4CP. In this case after U-Boot loads all you need to do is go 0x80200000 after loading the image into memory at address 0x80200000. This can be via TFTP booting or fatload if you have an MMC device.