[CAUTION: Non-UBC Email]
Hello Sid,
On 2023-08-08 05:20, Sid Agrawal wrote:
1. Looking at the DTS files for tqma8xqp-1gb in the seL4 repo. I see
one big file and another overlay. Why are there two for the same
board? I would have understood if one was for the SoC and another
for the board.
- tools/dts/tqma8xqp1gb.dts
- src/plat/tqma8xqp1gb/overlay-tqma8xqp1gb.dts
See Ivan's answer. As I was involved with the tqma port, I can confirm
that tools/dts/tqma8xqp1gb.dts is the de-compiled Linux DTB that came
on the SD card with the STKa8Xx dev board, see:
https://www.tq-group.com/en/products/tq-embedded/arm-architecture/stka8xx/
Specifically, I think it's based on version 25 of the SDK:
https://support.tq-group.com/en/arm/tqma8xx/linux/yocto/overview
The reason there is no board DTS file is because tqma is a module
which exposes almost all pins, so there are very few module hardware
choices made. And seL4 only uses on-chip peripherals, so nothing
board specific is left. In hindsight the tqma8xqp1gb platform would
have been better named imx8qxp, with configurable UART and memory
amount.
2. I see that the VMM example
(https://github.com/Ivan-Velickovic/sel4cp_vmm), as well as the sDDF
example (https://github.com/lucypa/sDDF/tree/main/echo_server), uses
the iMX8MM-EVK board.
- How different are iMX8MM-EVK and tqma8xqp1gb?
Very different for SoCs in the same product range, the iMX8MM-EVK
is based on the i.MX8M Mini SoC. But most changes aren't really
software visible.
The imx8qxp SoC is very complex and annoying because of the SCU.
If you don't need ECC memory, GPU, multiple displays and Ethernet
ports, go for a different SoC without SCU. That said, if U-Boot
configures the SCU correctly for your needs, you can ignore the
whole SCU mess for a while.
- What is the preferred board for the sel4cp effort at Trustworthy
Systems? This way, I will just get that board, and it would be easier
for me to follow your efforts along the way and maybe even contribute
:)
I don't know what board they use, but STKa8Xx, the tqma dev board,
used to be very expensive.
3. For the VMM example in particular.
- Is it correct to say that there are two dts files at play, one
needed by seL4(which we get from the seL4 repo) and the other needed
by the Linux Guest, which we get from the sel4cp_vmm repo?
The seL4 one describes all hardware peripherals so that all
the device untyped memory regions can be created. Assuming it
correctly describes the SoC, it never needs to be changed or
updated.
The VMM one is needed to tell the Linux VM what hardware and
memory it can actually use. Not all boards have all peripherals
connected, so the sel4cp_vmm DTS file is also the board file
describing the actual hardware available.
Greetings,
Indan
