Which hardware are you trying to run seL4 on? Is it per chance the rocket-chip for the zedboard? If so, that device only has 256MB of RAM. So its physical memory goes from 0x80000000 -> 0x90000000. By default, the kernel gets mapped at a 1GB offset from the physical address base.
[sathya] I am running on Shakti core configured on FPGA. Shakti is an internally developed core based on RV64. Currently, It has memory addressing from 0x80000000 to 0x8fffffff. It has SV39 mmu.
This is actual a nice coincidence. DornerWorks recently uploaded a pull request that makes seL4 functional on the rocket-chip. Essentially it boils down to mapping the kernel window in 2MB blocks instead of 1GB blocks. The commits have just been merged into master this morning.
[sathya] Thanks a lot. I tried your changes on ours. There seems to be some problem with page table mappings.
Essentially when you’re initializing the cmake build system, you simply need to call –DkernelPlatformSpikeRocketChi
[sathya] I did this. I hard-coded the PHY address LOAD to 0x88000000. We are stuck after kernel mapping. The address ranges looked good. Can you please tell, what is your page table configuration (2 level or 3 level) ?
regards,
sathya
Sathya,
Which hardware are you trying to run seL4 on? Is it per chance the rocket-chip for the zedboard? If so, that device only has 256MB of RAM. So its physical memory goes from 0x80000000 -> 0x90000000. By default, the kernel gets mapped at a 1GB offset from the physical address base.
This is actual a nice coincidence. DornerWorks recently uploaded a pull request that makes seL4 functional on the rocket-chip. Essentially it boils down to mapping the kernel window in 2MB blocks instead of 1GB blocks. The commits have just been merged into master this morning.
Essentially when you’re initializing the cmake build system, you simply need to call –DkernelPlatformSpikeRocketChi
p =ON in order to let the kernel know to load at 0x88000000 instead of 0xc0000000. You’ll also need to update the elf-loader to the tip of master, since that also updates the mappings.
Let me know if you have any questions. I’m happy to help.
Chris
From: Devel [mailto:devel-bounces@sel4.
systems ] On Behalf Of Sathya Narayanan N
Sent: Thursday, August 9, 2018 8:33 AM
To: devel@sel4.systems
Subject: Re: [seL4] Porting SEL4 on RISCV FPGA
CAUTION: This email originated from outside the organization. Do no click links or open attachments unless you recognize the sender and know the content is safe.
Hi,
I am porting SEL4 on RISCV FPGA. I am stuck midway in the kernel elf loader.
The function stuck is memcpy. I have added prints and I am not progressing after the last memcpy call in unpack_elf_to_paddr(). All kinds of input appreciated.
Function under review:
static void unpack_elf_to_paddr(void *elf, paddr_t dest_paddr)
/* Parse size/length headers. */
dest_vaddr = elf_getProgramHeaderVaddr(elf, i);
data_size = elf_getProgramHeaderFileSize(
elf, i); data_offset = elf_getProgramHeaderOffset(
elf, i);
/* Load data into memory. */
memcpy((char *)dest_vaddr + phys_virt_offset,
(char *)elf + data_offset, data_size);
printf("loaded data into memory \n"); -----> Stuck Here !
}
}
Can anyone give me a clue on whatsoever to check here ? It worked perfectly in spike simulation.
RISCV FPGA configuration - It supports IMAFD. It has already booted linux. Kernel is loaded at physical address 80 million.
Snap shot
ELF-loader started on
paddr=[80200000..8060dc17]
elfFile->e_phnum = 1
elfFile->e_phnum = 1
elfFile->e_phnum = 1
elfFile->e_phnum = 1
ELF-loading image 'kernel'
paddr=[c0000000..c002dfff]
vaddr=[ffffffff80000000..
ffffffff8002dfff] virt_entry=ffffffff80000000
elf file is valid
image is aligned
phy range valiidngetting size of image
elfFile->e_phnum = 1
elfFile->e_phnum = 1
memset each segment in the elf file
loading each segment in the elf file 2d018
elfFile->e_phnum = 1
loading data into memory
char *)dest_vaddr + phys_virt_offset = ffffffffc0000000 (char *)elf + data_offset, = ffffffff8020a694
----- ?
--
regards,
Sathya