Re: [seL4] QEMU vs Spike on RISC-V Debugging

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 on behalf of Porter, Jeremy Sent: Saturday, 14 November 2020 6:57 AM To: devel@sel4.systems 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.