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... [1]: https://github.com/irgendwie/genode/blob/rtcr-19.08-ttc/repos/base/src/timer... [2]: https://github.com/irgendwie/genode/blob/rtcr-19.08-ttc/repos/base/src/timer... [3]: https://store.digilentinc.com/zybo-zynq-7000-arm-fpga-soc-trainer-board/ [4]: https://github.com/irgendwie/genode/commit/60ffef31b52d6566f481b3de87b4720f3...