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...
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
Hi Alexander,
On Mon, Oct 28, 2019 at 06:05:19PM +0100, Alexander Weidinger 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?
As far as I understood the manual correctly, there are three different reference clocks you can choose from.
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'?
You hard-coded TICKS_PER_MS to "519", according to your comment in [1] Line 88 the prescale value N calculates to: count/2^(N+1) But you set the prescale value to "8". That means count/2^(8+1) = count/512. And 519 * 512 * 1000 ~= 266 MHz, isn't it?
I strongly assume you are working with wrong assumptions regarding your clocking values.
Regards Stefan
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
Hi Johannes, Hi Stefan,
What timer(s) is seL4 using already? I assume there should be other hardware timers left.
I'd assume that seL4 uses the GTC or the cpu private timer(s)? I must admit, that I didn't look into them - I just used the existing imx6 and imx7 targets for comparison. And although both do also have cpu private timer(s), they use different timers (epit and gpt) in the case of seL4/Genode. Therefore I was under the impression, that a dedicated (multi-purpose) timer is necessary.
Apart from the TTC, Zynq7000 offers a system watchdog and cpu watchdogs. Since watchdogs are normally used for the reset of chips/the system, I only looked into the last possibility, the TTC.
Have you double-checked all PLL settings and clock dividers in the slcr? I strongly assume you are working with wrong assumptions regarding your clocking values.
I made sure, that CPU_1x is used as input clock `write<CLK_CNTRL::SRC>(0);` but apart from that I didn't look into any clock settings. As recommended by you two I took a look at the SLCR registers…
My platform (Zybo) contains a 50MHz oscillator which drives all PLLs. I checked that the ARM PLL is used to drive the CPU clock (SRCSEL in ARM_CLK_CTRL -> 0) and read the DIVISOR (-> 2), FDIV (-> 26) and CLK_621 (-> 1) registers.
The CPU_1x clock generation should be as following (chapter 25.3): PS_CLK * PL_FDIV = ARM_PLL freq ARM_PLL freq / DIVISOR = CPU_6x4x CPU_6x4x / 6 or 4 = CPU_1x
Or with exact values: 50 MHz * 26 = 1.300 MHz 1.300 MHz / 2 = 650 MHz 650 MHz / 6 = 108 MHz
My tickrate should therefore be: 108.000 ticks/ms or when using a prescaler value of 2^6=128 => ~1688 ticks/ms Since the prescaler register uses the following formula count/2^(N+1), I set it to 0x5.
When using this calculations, the timer has less deviation but is also 1/2 too slow, e.g. sleeping 10s results in ~4.9s, 20s results in ~9.9s etc. When changing the prescaler value now to 0x6, the /2 problem is gone (of course).
Any ideas where I'm still wrong? And thanks for the hint regarding the clock - this was very helpful! :)
State of the current implementation [0] and [1].
Best regards, Alex
[0]: https://github.com/irgendwie/genode/blob/rtcr-19.08-ttc/repos/base/src/timer... [1]: https://github.com/irgendwie/genode/blob/rtcr-19.08-ttc/repos/base/src/timer...
Output of the registers:
[init -> timer] --- ARM_CLK_CTRL --- [init -> timer] SRCSEL=0 [init -> timer] DIVISOR=2 [init -> timer] ------- SLCR ------- [init -> timer] CLK_621_TRUE=1 [init -> timer] -------------------- [init -> timer] --- ARM_PLL_CTRL --- [init -> timer] PLL_FDIV=26 [init -> timer] --------------------
Hi Alex,
I'd assume that seL4 uses the GTC or the cpu private timer(s)? I must admit, that I didn't look into them - I just used the existing imx6 and imx7 targets for comparison. And although both do also have cpu private timer(s), they use different timers (epit and gpt) in the case of seL4/Genode. Therefore I was under the impression, that a dedicated (multi-purpose) timer is necessary.
I had a brief look at the sel4 source code. in src/plat/zynq7000 there are two dts files which suggest that the standard version uses the private timer whereas the mcs version uses the GTC.
My tickrate should therefore be: 108.000 ticks/ms or when using a prescaler value of 2^6=128 => ~1688 ticks/ms Since the prescaler register uses the following formula count/2^(N+1), I set it to 0x5.
2^6 is actually 64 so maybe this explains why the timer is off by factor 2.
-
Alexander Weidinger -
Johannes Schlatow -
Stefan Kalkowski