seL4/Genode on zynq7000; TTC Timer Component

[Alexander Weidinger]

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]:
https://www.xilinx.com/support/documentation/user_guides/ug585-Zynq-7000-TRM.pdf
[1]:
https://github.com/irgendwie/genode/blob/rtcr-19.08-ttc/repos/base/src/timer/ttc/time_source.cc
[2]:
https://github.com/irgendwie/genode/blob/rtcr-19.08-ttc/repos/base/src/timer/ttc/time_source.h
[3]:
https://store.digilentinc.com/zybo-zynq-7000-arm-fpga-soc-trainer-board/
[4]:
https://github.com/irgendwie/genode/commit/60ffef31b52d6566f481b3de87b4720f3251f6ec