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 <[email protected]> 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]: > 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 > > _______________________________________________ > Genode users mailing list > [email protected] > https://lists.genode.org/listinfo/users _______________________________________________ Genode users mailing list [email protected] https://lists.genode.org/listinfo/users
