Hello

Thank you for the answer. I simply adjusted the values in kernel/tools/dts/am335x.dts for now and kept the seL4DTBHardware connection.

I have more questions:
1) There are 2 implementations of low_level_init
     - projects/global-components/components/PicoServer/src/eth_interface.c
     - projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c
     What decides which one to invoke? or is the in beaglebone.c not necessary at all?

2) How is projects/camkes/picoserver/ethdriver_seL4Ethdriver_0.c generated?
    I am debugging my current implementation which gets stuck before ethriver_mac().

Sincerely,
Benjamin
Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au]
Gesendet: Dienstag, 18. Juni 2019 03:36
An: KAP Benjamin; devel@sel4.systems
Betreff: Re: Beaglebone Black: failed to find device frame

Hi,

The problem is that there isn't any untyped memory available to make a 4K page at address 0x4a101200 (if you notice carefully, this address isn't page aligned).

The seL4DTBHardware connector doesn't support the AM335x board as the format of the interrupt fields in the DTS doesn't follow that of the ARM GIC.

The page alignment problem is also a problem that I didn't encounter when developing the seL4DTBHardware connector, so thanks for the alert.

So to resolve your problem you will have to use the seL4HardwareMMIO connector and ask it to make a 4K mapping at 0x4a100000 and 0x4a101000.

You will also need to use the seL4HardwareInterrupt connector to generate the interrupts.

Sincerely,
Damon
From: Devel <devel-bounces@sel4.systems> on behalf of KAP Benjamin <benjamin.kap.001@student.uni.lu>
Sent: Tuesday, 18 June 2019 4:10 AM
To: devel@sel4.systems
Subject: [seL4] Beaglebone Black: failed to find device frame
 
Hello

I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file:
projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h.

Current contents of this file (I am creating it step by step, thus it might be incomplete):

#pragma once

#define HARDWARE_ETHERNET_COMPONENT

#define HARDWARE_ETHERNET_INTERFACES                                                \
    consumes Dummy EthDriver;                                                                                     \
    emits Dummy dummy_source;

#define HARDWARE_ETHERNET_COMPOSITION                                            \
    connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver);

#define HARDWARE_ETHERNET_CONFIG                                                  \
    EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" });                     \
    EthDriver.generate_interrupts = 1;


I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error:

ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2
  paddr=[82000000..8262e037]
No DTB found!
Looking for DTB in CPIO archive...
Found dtb at 820c1b84
Loaded dtb from 820c1b84
   paddr=[80034000..8003cfff]
ELF-loading image 'kernel'
  paddr=[80000000..80033fff]
  vaddr=[f0000000..f0033fff]
  virt_entry=f0000000
ELF-loading image 'capdl-loader'
  paddr=[8003d000..8059afff]
  vaddr=[10000..56dfff]
  virt_entry=1e4dc
ELF loader relocated, continuing boot...
Enabling MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
Booting all finished, dropped to user space
create_object@main.c:726  device frame/untyped, paddr = 0x48040000, size = 12 bits

create_object@main.c:726  device frame/untyped, paddr = 0x48042000, size = 12 bits

create_object@main.c:726  device frame/untyped, paddr = 0x4a100000, size = 12 bits

create_object@main.c:726  device frame/untyped, paddr = 0x4a101200, size = 12 bits

create_object@main.c:730 [Cond failed: err != seL4_NoError]
        Failed to find device frame/untyped at paddr = 0x4a101200

seL4 root server abort()ed
Debug halt syscall from user thread 0xffefd600 "rootserver"
halting...
Kernel entry via Unknown syscall, word: 65


The am335x.dtb contains the following line in ethernet@4a100000:
reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>;



If I am correct the hardware block isn't enabled but I don't know exactly how to do this.
Could anyone help me out here or give me some hints?

Best Regards,

Kap Benjamin