Microchip PolarFire Icicle Kit status

Hello!

I have a question about the Microchip PolarFire Icicle Kit board support.

Is the board currently a part of the HW CI?

And are you aware of anyone using it recently (since the page was posted in October 2022)?

It seems to me that there is at least one typo (u-boot.bin in the yaml file should probably be u-boot-dtb.bin), and maybe some instructions are missing (not very clear whether HSS is needed or not).

I don’t have the board yet, and I am evaluating the Renode emulated version, but I am considering using it for one of our projects.

Regards
Michal

It is currently not in CI and is only tested for seL4 releases, not continually (unless Dornerworks has their own CI that tracks the seL4 master branch, but I don’t think so).

We should really add another column to that table that lists the CI status.

I’m not, but @chrisguikema might be.

Some drift in the instructions since Oct’22 does seem quite possible, yes.

Hi all,
so now we have the physical board, as well as a Renode simulated one.

In both cases, I can get as far as this in the kernel boot process:

...
## Booting kernel from Legacy Image at 89300000 ...
   Image Name:   sel4test
   Image Type:   RISC-V Linux Kernel Image (uncompressed)
   Data Size:    4747880 Bytes = 4.5 MiB
   Load Address: 80000000
   Entry Point:  80000000
   Verifying Checksum ... OK
## Flattened Device Tree blob at 88300000
   Booting using the fdt blob at 0x88300000
   Loading Kernel Image
   Using Device Tree in place at 0000000088300000, end 0000000088305b41
Starting kernel ...
sbi_emulate_csr_read: hartid1: invalid csr_num=0x340

Note that I am getting the same error in simulator and on the real board.

A similar SBI related issue popped up here: OpenSBI service in HSS hangs · Issue #185 · riscv-software-src/opensbi · GitHub

Since we are using the latest version of HSS/OpenSBI (either 1.0 or 1.2 I believe), I am wondering if there is anything on the seL4 side that needs to be updated? It looks like the RISCV related code is rather old, see risc-v: add comment about SBI constants · seL4/seL4@6b8cbc9 · GitHub

Perhaps this line? sel4test-manifest/default.xml at master · seL4/sel4test-manifest · GitHub

Note: we changed it to 1.0 but got the same result, so something else is amiss.

Regards
Michal

I believe the default image located in ./images at the end of a sel4test build contains a version of openSBI also. It expects to be loaded via a u-boot running in mmode that jumps into the new image that then sets up a new version of opensbi.
If you are loading via a different flow, eg expecting to load something into smode, then you would want the elfloader image to be what’s given to your opensbi to load.

Hi @kent-mcleod2 !

It expects to be loaded via a u-boot running in mmode

Do you mean u-boot should be in M-mode? Having read through the docs here:
https://u-boot.readthedocs.io/en/latest/board/microchip/mpfs_icicle.html

it looks like u-boot only supports booting in S-mode. Are these docs out of date?

We are following the recommended boot process (HSS → U-Boot → seL4).

@kent-mcleod2 I followed your advice on disabling OpenSBI packaging with the kernel build (commenting out the rootserver config here and then building the kernel with:

../init-build.sh \
		-DPLATFORM=polarfire \
		-DSel4testAllowSettingsOverride=True \
		-DElfloaderImage=elf \
		-DUseRiscVOpenSBI=OFF \
		-DKernelVerificationBuild=OFF && \
	ninja

I boot the board as described in the seL4 icicle kit wiki page.

This doesn’t seem to fix the issue, I am getting the following output which seems to indicate that I in fact need OpenSBI as otherwise the cores are not prepared correctly by u-boot:

[1.372800] HSS_Boot_PMPSetupHandler(): Hart2 setup complete
HSS_OpenSBI_Setup(): MTVEC switching from 20220230 to 20220100
OpenSBI v0.6
   ____                    _____ ____ _____
  / __ \                  / ____|  _ \_   _|
 | |  | |_ __   ___ _ __ | (___ | |_) || |
 | |  | | '_ \ / _ \ '_ \ \___ \|  _ < | |
 | |__| | |_) |  __/ | | |____) | |_) || |_
  \____/| .__/ \___|_| |_|_____/|____/_____|
        | |
        |_|
Platform Name          : Microchip PolarFire SoC
Platform HART Features : RV64ACDFIMS
Platform Max HARTs     : 5
Current Hart           : 2
Firmware Base          : 0x20220000
Firmware Size          : 105 KB
Runtime SBI Version    : 0.2
MIDELEG : 0x0000000000000222
MEDELEG : 0x000000000000b109
PMP0    : 0x0000000020220000-0x000000002023ffff (A)
PMP1    : 0x0000000000000000-0xffffffffffffffff (A,R,W,X)
ELF-loader started on (HART 18446744071562067992) (NODES 1)
  paddr=[80000000..80292037]
Looking for

Does that sound about right?

If so, do you have any other suggestions? Should we try to run a particular bare metal example?

Regards
Michal

We have updated both HSS and the seL4 test manifest to use OpenSBI 1.2 and we are still seeing the invalid csr_num error.

It expects to be loaded via a u-boot running in mmode

Do you mean u-boot should be in m-mode? Having read through the docs here:

https://u-boot.readthedocs.io/en/latest/board/microchip/mpfs_icicle.html

it looks like u-boot only supports booting in s-mode. Are these docs out of date? The seL4 doc here:

https://docs.sel4.systems/Hardware/polarfire.html

also indicates u-boot should be in s-mode.

Thanks!

That looks like you’ve resolved the initial issue and the elfloader is now starting in smode.

This is what the output looks like on the hifive board for example:

  OpenSBI v0.8
     ____                    _____ ____ _____
    / __ \                  / ____|  _ \_   _|
   | |  | |_ __   ___ _ __ | (___ | |_) || |
   | |  | | '_ \ / _ \ '_ \ \___ \|  _ < | |
   | |__| | |_) |  __/ | | |____) | |_) || |_
    \____/| .__/ \___|_| |_|_____/|____/_____|
          | |
          |_|
  
  Platform Name       : SiFive Freedom U540
  Platform Features   : timer,mfdeleg
  Platform HART Count : 4
  Boot HART ID        : 2
  Boot HART ISA       : rv64imafdcsu
  BOOT HART Features  : pmp,scounteren,mcounteren
  BOOT HART PMP Count : 16
  Firmware Base       : 0x80000000
  Firmware Size       : 100 KB
  Runtime SBI Version : 0.2
  
  MIDELEG : 0x0000000000000222
  MEDELEG : 0x000000000000b109
  PMP0    : 0x0000000080000000-0x000000008001ffff (A)
  PMP1    : 0x0000000000000000-0x0000007fffffffff (A,R,W,X)
  ELF-loader started on (HART 1) (NODES 1)
    paddr=[80200000..806be037]
  Looking for DTB in CPIO archive...found at 802dd140.
  Loaded DTB from 802dd140.
     paddr=[84020000..84022fff]
  ELF-loading image 'kernel' to 84000000
    paddr=[84000000..8401ffff]
    vaddr=[ffffffff84000000..ffffffff8401ffff]
    virt_entry=ffffffff84000000
  ELF-loading image 'sel4test-driver' to 84023000
    paddr=[84023000..84429fff]
    vaddr=[10000..416fff]
    virt_entry=1c5cc

The bad HART ID indicates that the a0 argument (which the elfloader expects to contain the hartid) is getting corrupted by the time the print is printed, and then the crash looks like it’s around the time the DTB is accessed (which is also passed through the a1 arg or overridden by the kernel.dtb provided in the cpio archive linked into the elfloader).

Where is main memory of the system located? Normally the Firmware Base starts slightly before the elfloader, and the elfloader expects to start at a value higher than 0x80200000. When I build the polarfire image, the elfloader has a load address of 0x0000000080a1f000 for example, but it’s being loaded at 0x80000000. So one thing you could try next is adding -DIMAGE_START_ADDR=0x80000000 to the init-build.sh arguments which should force the elfloader to expect to be loaded at 0x80000000…

We are still not having much luck with seL4 on the polarfire. We have attempted to boot on both Renode and via direct kernel boot on QEMU polarfire emulation:

https://qemu.readthedocs.io/en/latest/system/riscv/microchip-icicle-kit.html

Neither is working. I built two projects.

First I built sel4tests by following the instructions linked above. We are doing direct kernel boot in QEMU so we only needed this part:

repo init -u https://github.com/seL4/sel4test-manifest.git
repo sync
mkdir cbuild
cd cbuild
../init-build.sh -DPLATFORM=polarfire -DSel4testAllowSettingsOverride=True -DElfloaderImage=binary -DKernelVerificationBuild=OFF
ninja

When I attempt to boot I see the OpenSBI output and nothing else. I checked all 4 serial outputs defined in the dtb:

qemu-system-riscv64 -M microchip-icicle-kit -smp 5 -m 2G     -display none -serial stdio -serial null -serial null -serial null    -kernel /home/esandberg/projects/sel4/repo_sel4/cbuild/images/sel4test-driver-image-riscv-polarfire -dtb /home/esandberg/projects/sel4/repo_sel4/cbuild/kernel/kernel.dtb 

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

Platform Name             : SiFive,FU540G
Platform Features         : medeleg
Platform HART Count       : 5
Platform IPI Device       : ---
Platform Timer Device     : --- @ 0Hz
Platform Console Device   : uart8250
Platform HSM Device       : ---
Platform PMU Device       : ---
Platform Reboot Device    : ---
Platform Shutdown Device  : ---
Firmware Base             : 0x80000000
Firmware Size             : 244 KB
Runtime SBI Version       : 1.0

Domain0 Name              : root
Domain0 Boot HART         : 3
Domain0 HARTs             : 0*,1*,2*,3*,4*
Domain0 Region00          : 0x0000000080000000-0x000000008003ffff ()
Domain0 Region01          : 0x0000000000000000-0xffffffffffffffff (R,W,X)
Domain0 Next Address      : 0x0000000080200000
Domain0 Next Arg1         : 0x00000000bfe00000
Domain0 Next Mode         : S-mode
Domain0 SysReset          : yes

Boot HART ID              : 3
Boot HART Domain          : root
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: 54
Boot HART MHPM Count      : 0
Boot HART MIDELEG         : 0x0000000000000222
Boot HART MEDELEG         : 0x000000000000b109

Second we added the polarfire to the dev fork here:

GitHub - Ivan-Velickovic/microkit: Microkit - A simple operating system framework for the seL4 microkernel

we modified the star64 example to work with the polarfire. Not a lot of changes were required:

  BoardInfo(
        name="polarfire",
        arch=BoardArch.RISCV64,
        gcc_flags = "",
        loader_link_address=0x89300000,
        kernel_options = {
            "KernelIsMCS": True,
            "KernelPlatform": "polarfire",
        },
        examples = {
            "hello": Path("example/polarfire/hello")
        }
    ),

and we copied the star64 example to the polarfire example dir.

When I attempt to boot in QEMU I see the OpenSBI output and then an error about the magic number. I checked all 4 serial outputs defined in the dtb:

qemu-system-riscv64 -M microchip-icicle-kit -smp 5 -m 2G     -display none -serial stdio -serial null -serial null -serial null    -kernel /home/esandberg/projects/sel4/ivan-vel-sel4cp/tmp_build/loader.img     -dtb /home/esandberg/projects/sel4/ivan-vel-sel4cp/build/polarfire/release/sel4/build/kernel.dtb 

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

Platform Name             : SiFive,FU540G
Platform Features         : medeleg
Platform HART Count       : 5
Platform IPI Device       : aclint-mswi
Platform Timer Device     : aclint-mtimer @ 1000000Hz
Platform Console Device   : uart8250
Platform HSM Device       : ---
Platform PMU Device       : ---
Platform Reboot Device    : ---
Platform Shutdown Device  : ---
Firmware Base             : 0x80000000
Firmware Size             : 244 KB
Runtime SBI Version       : 1.0

Domain0 Name              : root
Domain0 Boot HART         : 4
Domain0 HARTs             : 0*,1*,2*,3*,4*
Domain0 Region00          : 0x0000000002000000-0x000000000200ffff (I)
Domain0 Region01          : 0x0000000080000000-0x000000008003ffff ()
Domain0 Region02          : 0x0000000000000000-0xffffffffffffffff (R,W,X)
Domain0 Next Address      : 0x0000000080200000
Domain0 Next Arg1         : 0x00000000bfe00000
Domain0 Next Mode         : S-mode
Domain0 SysReset          : yes

Boot HART ID              : 4
Boot HART Domain          : root
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: 54
Boot HART MHPM Count      : 0
Boot HART MIDELEG         : 0x0000000000000222
Boot HART MEDELEG         : 0x000000000000b109
LDR|INFO: altloader for seL4 starting
LDR|ERROR: mismatch on loader data structure magic number

The loader link address is 0x89300000 which needs to match OpenSBI’s next level starting address which is logged as:

Domain0 Next Address      : 0x0000000080200000

I suggest changing loader_link_address to 0x0000000080200000.

Ultimately this problem you are running into indicates that the documentation is not sufficient. As booting a platform should really be not a hard problem.

At least for the Core Platform, when my development changes are upstreamed I’ll make sure to also include a general guide for porting and starting on a new platform.

Thanks for the help with the loader address. I changed it in sel4cp. I getting further now but hitting an error after dropping to userspace. The OpenSBI portion looks the same as before, the output after that looks like this:

LDR|INFO: region: 0x00000000   addr: 0x0000000084000000   size: 0x000000000002b000   offset: 0x0000000000000000   type: 0x0000000000000001
LDR|INFO: region: 0x00000001   addr: 0x000000008402f000   size: 0x0000000000006ad0   offset: 0x000000000002b000   type: 0x0000000000000001
LDR|INFO: region: 0x00000002   addr: 0x000000008402b000   size: 0x0000000000000910   offset: 0x0000000000031ad0   type: 0x0000000000000001
LDR|INFO: region: 0x00000003   addr: 0x000000008402c000   size: 0x0000000000000298   offset: 0x00000000000323e0   type: 0x0000000000000001
LDR|INFO: region: 0x00000004   addr: 0x000000008402d000   size: 0x0000000000001032   offset: 0x0000000000032680   type: 0x0000000000000001
LDR|INFO: copying region 0x00000000
LDR|INFO: copying region 0x00000001
LDR|INFO: copying region 0x00000002
LDR|INFO: copying region 0x00000003
LDR|INFO: copying region 0x00000004
LDR|INFO: enabling MMU
LDR|INFO: jumping to kernel
Init local IRQ
Bootstrapping kernel
Initializing PLIC...
available phys memory regions: 1
  [80200000..c0000000]
reserved virt address space regions: 2
  [ffffffc084000000..ffffffc08402b000]
  [ffffffc08402f000..ffffffc084036000]
Booting all finished, dropped to user space
MON|INFO: seL4 Core Platform Bootstrap
MON|ERROR: paddr mismatch for untyped region: 0x00000000  expected paddr: 0x000000008402b000  boot info paddr: 0x0000000000000000
FAIL: paddr mismatch

I tried again with sel4test as well. I added -DIMAGE_START_ADDR=0x0000000080200000 to my init-built.sh args but I still get the same lack of output after OpenSBI at runtime.

Okay looks like something is going wrong in seL4CP perhaps. If it’s the same error on QEMU would you mind posting the QEMU command used? I can try debug it.

It was on QEMU. here is the command:

qemu-system-riscv64 -M microchip-icicle-kit -smp 5 -m 2G     -display none -serial stdio -serial null -serial null -serial null    -kernel /home/esandberg/projects/sel4/ivan-vel-sel4cp/tmp_build/loader.img     -dtb /home/esandberg/projects/sel4/ivan-vel-sel4cp/build/polarfire/release/sel4/build/kernel.dtb 

Unfortunately I could not reproduce your issue. For me the QEMU log stops at Booting all finished, dropped to user space and it looks like the monitor does not execute. It looks like the DTS overlay for the CLINT device added in Mark CLINT as reserved device on RISC-V platforms · seL4/seL4@2730e65 · GitHub is causing it to fail, as QEMU is (I assume) expecting some interrupts to be on the DTS node. Applying this change to the kernel:

diff --git a/src/plat/polarfire/overlay-polarfire.dts b/src/plat/polarfire/overlay-polarfire.dts
index 7b90f0429..bcb1b51b5 100644
--- a/src/plat/polarfire/overlay-polarfire.dts
+++ b/src/plat/polarfire/overlay-polarfire.dts
@@ -10,15 +10,4 @@
             &{/soc/clint@2000000},
 		    &{/soc/interrupt-controller@c000000};
 	};
-
-    /*
-     * According to the "PolarFire SoC MSS Technical Reference Manual"
-     * (revision H), the CLINT is mapped from 0x0200_0000 to 0x0200_FFFF.
-     */
-    soc {
-        clint@2000000 {
-            compatible = "riscv,cpu-intc";
-            reg = <0x00000000 0x2000000 0x00000000 0x000010000>;
-        };
-    };
 };
diff --git a/tools/hardware.yml b/tools/hardware.yml
index cf55f22f9..7575ff855 100644
--- a/tools/hardware.yml
+++ b/tools/hardware.yml
@@ -215,6 +215,7 @@ devices:
   # supported platforms.
   - compatible:
       - riscv,cpu-intc
+      - riscv,clint0
     regions:
       - index: 0
         kernel: CLINT_PPTR

does solve the issue, and “hello world” is printed. But I am not sure whether this patch should actually be made to seL4, as the DTB that seL4 produces is (from my understanding) not intended to be a DTB you give to QEMU, Linux, or U-Boot for their booting process.

I tried instead to build U-Boot for the Polarfire and use that DTB instead of seL4’s, but that failed to boot anything.

At least for the seL4CP issue, the issue is to do with the DTB being passed to QEMU, not seL4CP itself.

So, what to do from here? I would compile the seL4 DTS for the Polarfire without the overlay as the overlay is specific to seL4 itself and this device tree is to describe the platform to QEMU. Doing dtc -I dts -O dtb seL4/tools/dts/mpfs_icicle.dts > mpfs_icicle.dtb and using mpfs_icicle.dtb should work, as it does for me. The QEMU command is:

qemu-system-riscv64 -M microchip-icicle-kit -smp 5 -m 2G -display none -serial stdio -serial null -serial null -kernel tmp_build/loader.img -dtb mpfs_icicle.dtb

I would also test the image on hardware to make sure it’s also working there.

If I get the chance I will take a look at the sel4test issue.

What version of QEMU are you using?

qemu-system-riscv64 --version
QEMU emulator version 8.0.3
Copyright (c) 2003-2022 Fabrice Bellard and the QEMU Project developers

@sand7000 did this work for you?

I applied your patch to the master branch of your seL4 fork. rebuilt the SDK and the polarfire example and still didn’t see “hello world”. Is that the correct branch to start with?

I haven’t tried your suggestion of compiling without the overlay yet but will so so shortly.

No I use a different branch called sel4cp-dev. Sorry about the confusion.

Alternatively if you head to “Actions” → Click on the latest commit → Scroll down to “Artifacts” you will see the various development SDKs built by the CI. You can download the (I assume) Linux x86-64 SDK and unpack it. I have added a commit that adds Polarfire support so no changes should be necessary on your part. The hello world example can be found in sel4cp-sdk-1.2.6/board/polarfire/example/hello once unpacking it.