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 <Chris.Guikema@dornerworks.com> 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