seL4 doesn't detect memory at runtime. The physical memory is specified in the
DTS file, in this case,
kernel/tools/dts/spike.dts
seL4 build system extracts the memory info from this file, generates platform
headers,
kernel/gen_headers/plat/machine/devices_gen.h
If you'd like to use smaller memory, simply modify the memory section in the
DTS file.
________________________________________
From: Devel <[email protected]> on behalf of Porter, Jeremy
<[email protected]>
Sent: Saturday, 14 November 2020 6:57 AM
To: [email protected]
Subject: Re: [seL4] QEMU vs Spike on RISC-V Debugging
OK, this worked perfectly. Thank you!
Is there a reason we need so much memory? I've got the command you sent working
with -m size=1025M, but I can't go lower. I've looked at machine.c code for the
platform (spike) but that seems to adjust to the size provided by hardware.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
