seL4/Genode on zynq7000; TTC Timer Component

Johannes Schlatow schlatow at
Tue Oct 29 10:23:58 CET 2019

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


On Mon, 28 Oct 2019 18:05:19 +0100
Alexander Weidinger <alexander.weidinger at> 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].
> [0]:
> [1]:
> [2]:
> [3]:
> [4]:
> _______________________________________________
> Genode users mailing list
> users at

More information about the users mailing list