Dear Alex,
the time drift you mentioned is indeed huge and seems odd to me. Have you double-checked all PLL settings and clock dividers in the slcr? The registers may be changed by the bootloader (e.g. uboot) or the debugger. (I was using a Lauterbach debugger once, which used different register values for initialisation.)
What timer(s) is seL4 using already? I assume there should be other hardware timers left.
I'm not familiar with how seL4 integrates into Genode for different platforms, but I can give you a pointer to how the RAM size is configured for different the Zynq-7000 boards that I used with base-hw: The RAM size, clocks etc. are defined in separate header files [1]. Controlled by the specs, the corresponding definitions are used to declare the required symbols in the Board namespace that are needed for compiling core [2] and bootstrap [3].
Best regards Johannes
[1] https://github.com/genodelabs/genode-world/tree/master/include/drivers/defs [2] https://github.com/genodelabs/genode-world/tree/master/src/core/include/spec [3] https://github.com/genodelabs/genode-world/tree/master/src/bootstrap/spec
On Mon, 28 Oct 2019 18:05:19 +0100 Alexander Weidinger alexander.weidinger@tum.de wrote:
Hello Genodians,
we adapted the zynq7000 target to run with Genode/seL4[4], which was done accordingly to the imx6 and imx7 targets already existing in Genode.
Since we are in need for a timer component and the seL4 doesn't provide a "l4_ipc_sleep()" call, like it is used for the generic timer component in Fiasco.OC, we started implementing a timer[1,2] based on the TTC of the Zynq7000[0]. By now we have it up and running but with a high deviation the longer it runs (already 30 seconds deviation after only 2 minutes).
This deviation originates from a few problems we have:
- The timers in TTC only provide a 16 Bit width -> high number of IRQs
when trying to achieve high precision
- The input clock is 133MHz and can only be prescaled by a division of
2^(n+1) with 0 < n <= 16 -> hard to work with?
Currently we implement it similar to the imx6 timer, by generating IRQs when a match in the MATCH0 register is acknowledged.
I'm not very experienced in this topic and any help is appreciated on how to resolve the deviation issues or how to implement it in a better way - e.g. by using a different hardware timer which I didn't discover in the TRM.
Additionally I'd like to know if there is an easy way to configure the maximum RAM of a platform in seL4/Genode apart from limiting it in 'contrib/sel4-*/src/kernel/sel4/include/plat/*/plat/machine/hardware.h'?
Best regards, Alex
PS: As Zynq7000 platform we use the Digilent Zybo[3].
Genode users mailing list users@lists.genode.org https://lists.genode.org/listinfo/users