Hi Tuo,

Can you send a log of what your build process is, including Cmake steps and elfloader output?

The kernel should have a BUILD_ROCKET_CHIP_ZEDBOARD option, which can be initialized with the –DkernelPlatformSpikeRocketChip flag in Cmake. Can you also look at the “kernel/gen_config/kernel/gen_config.h” file to see if CONFIG_BUILD_ROCKET_CHIP_ZEDBOARD is being set.

Chris Guikema

DornerWorks Ltd.

From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Tuo Li
Sent: Sunday, September 2, 2018 11:10 PM
To: devel@sel4.systems
Subject: [seL4] issues in running sel4test on RISC-V rocket-chip FPGA

CAUTION: This email originated from outside the organization. Do not click links or open attachments unless you recognize the sender and know the content is safe.

Hi guys,

I have ported rocket chip (github.com/ucb-bar/fpga-zynq) on a ZCU102 FPGA board and it successfully runs riscv-linux. It's RV64G RISC-V.

I am trying to run sel4test on the same hardware system. So far, the system gives no output after "Jumping to kernel-image entry point..." and seems to be stuck there.

The same code has been tested on qemu simulator targeting spike 1.10 with the same device tree, following the online guide (https://docs.sel4.systems/Hardware/RISCV.html). No problem.

I have seen this thread (http://sel4.systems/pipermail/devel/2018-August/002069.html), and used the solution provided for modifying the paddr range.

I tried to add a few printf statements and even a fail statement in the boot.c file in kernel/src/arch/riscv/kernel/, which I guess is the first function executed after head.S. Same problem happens. 

Any suggestions? Thanks.

Best regards,
Tuo