Hi Chris, I just updated the sel4test today. And the problem seems to be gone. Now the processor can jump to kernel entry and finish the sel4test. The only issue now is I have to execute init_build.sh and ninja twice to make "-DKernelPlatformSpikeRocketChip" flag effective. Perhaps I didn't do it correctly, since I am not very familiar with cmake. init_build.sh file is modified to initilize cmake with -DKernelPlatformSpikeRocketChip: # Initialize cmake cmake -DKernelPlatformSpikeRocketChip=ON -DCMAKE_TOOLCHAIN_FILE=${SCRIPT_PATH}/kernel/gcc.cmake -G Ninja $@ ${SCRIPT_PATH} && cmake ${SCRIPT_PATH} && cmake ${SCRIPT_PATH} Executing init_build.sh && ninja once does not set CONFIG_BUILD_ROCKET_CHIP_ZEDBOARD in kernel/gen_config/kernel/gen_ config.h. And, elf_loader loads kernel to paddr=[c0000000..c0026fff], which is out of 256M memory space. Cmake log: -- The C compiler identification is GNU 7.2.0 -- The CXX compiler identification is GNU 7.2.0 -- Check for working C compiler: /home/lituo/workspace/riscv/sel4test/riscv-tools/bin/riscv64-unknown-elf-gcc -- Check for working C compiler: /home/lituo/workspace/riscv/sel4test/riscv-tools/bin/riscv64-unknown-elf-gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /home/lituo/workspace/riscv/sel4test/riscv-tools/bin/riscv64-unknown-elf-g++ -- Check for working CXX compiler: /home/lituo/workspace/riscv/sel4test/riscv-tools/bin/riscv64-unknown-elf-g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /home/lituo/workspace/riscv/sel4test/riscv-tools/bin/riscv64-unknown-elf-gcc -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FAILED -- Performing test SOFTFP_FLOAT with flags -mfloat-abi=softfp -- Test SOFTFP_FLOAT FAILED CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) -- Configuring done -- Generating done -- Build files have been written to: /home/lituo/workspace/riscv/sel4test/build-riscv -- Configuring done -- Generating done -- Build files have been written to: /home/lituo/workspace/riscv/sel4test/build-riscv -- Configuring done -- Generating done -- Build files have been written to: /home/lituo/workspace/riscv/sel4test/build-riscv elfloader output: bbl loader ELF-loader started on paddr=[80200000..805cbe7f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 What I did is executing init_build.sh && ninja twice. This seems to make -DKernelPlatformSpikeRocketChip flag effective. elfloader output: bbl loader ELF-loader started on paddr=[80200000..805cc27f] ELF-loading image 'kernel' paddr=[88000000..88027fff] vaddr=[ffffffff80000000..ffffffff80027fff] virt_entry=ffffffff80000000 ELF-loading image 'sel4test-driver' paddr=[88028000..8838efff] vaddr=[10000..376fff] virt_entry=3a8ee Jumping to kernel-image entry point... Thanks, Tuo On Tue, Sep 4, 2018 at 10:58 PM Chris Guikema wrote:

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