Hi Ben, There is a tool in kernel/tools called reciprocal.py. It calculates CLK_MAGIC and CLK_SHIFT from an input frequency like so: ``` ./reciprocal.py --divisor 54000000 magic number is: 5337599559, shift amount is 58 ``` With an input frequency of 31250000 CLK_MAGIC=5337599559, CLK_SHIFT=58. KERNEL_WCET is the worst case execution time of a path through the kernel in microseconds. Without an actual measurement, most platforms configure this to 10us. ________________________________ From: Turner, Ben <ben.turner@roke.co.uk> Sent: Thursday, 20 February 2020 8:14 PM To: Shen, Yanyan (Data61, Kensington NSW) <Yanyan.Shen@data61.csiro.au>; devel@sel4.systems <devel@sel4.systems> Cc: Millar, Curtis (Data61, Kensington NSW) <Curtis.Millar@data61.csiro.au>; Mcleod, Kent (Data61, Kensington NSW) <Kent.Mcleod@data61.csiro.au> Subject: RE: [seL4] Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b Hi Shen, I have managed to confirm that the frequency is 54MHz and the MAX_IRQ is 127. Still no luck finding much on KERNEL_WCET, CLK_MAGIC or CLK_SHIFT so far. I’ll keep digging but any other tips you can throw my way would be appreciated! Thanks, Ben Turner Follow Us: LinkedIn<http://www.linkedin.com/company/roke-manor-research> | Twitter<https://twitter.com/rokemanor> | Facebook<https://www.facebook.com/rokemanor> Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom. Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550. The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. www.roke.co.uk<http://www.roke.co.uk/?utm_source=Roke&utm_medium=Email&utm_content=Company%20Signature&utm_campaign=Roke> ________________________________ From: Shen, Yanyan (Data61, Kensington NSW) <Yanyan.Shen@data61.csiro.au> Sent: 20 February 2020 03:55 To: Turner, Ben <ben.turner@roke.co.uk>; devel@sel4.systems Cc: Millar, Curtis (Data61, Kensington NSW) <Curtis.Millar@data61.csiro.au>; Mcleod, Kent (Data61, Kensington NSW) <Kent.Mcleod@data61.csiro.au> Subject: Re: [seL4] Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b Hi Ben, You could also read the register CNTFRQ_EL0 [https://developer.arm.com/docs/ddi0595/b/aarch64-system-registers/cntfrq_el0] to double check the value. As to the max IRQ, you can read it from the GICD_TYPER [https://developer.arm.com/docs/ihi0048/b/arm-generic-interrupt-controller-ar...]. The ITLinesNumber field indicates the maximum number of interrupts supported by the GIC. Hope that will help. Regards, Yanyan From: "Turner, Ben" <ben.turner@roke.co.uk<mailto:ben.turner@roke.co.uk>> Date: Thursday, 20 February 2020 at 3:06 am To: "Shen, Yanyan (Data61, Kensington NSW)" <Yanyan.Shen@data61.csiro.au<mailto:Yanyan.Shen@data61.csiro.au>>, "devel@sel4.systems<mailto:devel@sel4.systems>" <devel@sel4.systems<mailto:devel@sel4.systems>> Cc: "Millar, Curtis (Data61, Kensington NSW)" <Curtis.Millar@data61.csiro.au<mailto:Curtis.Millar@data61.csiro.au>>, "Mcleod, Kent (Data61, Kensington NSW)" <Kent.Mcleod@data61.csiro.au<mailto:Kent.Mcleod@data61.csiro.au>> Subject: RE: [seL4] Adding Platform Support: CAmkES-ARM-VM: VM_Minimal: Raspberry Pi 3b Hi Shen, Thanks for the advice. I may have found the TIMER_FREQUENCY (although I’m not certain) – the boot log has an entry: arch_timer: cp15 timer(s) running at 54.00MHz This is the only possibly relevant timer reference I can find? I haven’t had any luck with the MAX_IRQ value though. The only value in the boot log that could relate is: NR_IRQS: 16, nr_irqs: 16, preallocated irqs: 16 But 16 seems way lower than I would expect… The value for the RPi3, for example, is 127! Thanks, Ben Turner Follow Us: LinkedIn<http://www.linkedin.com/company/roke-manor-research> | Twitter<https://twitter.com/rokemanor> | Facebook<https://www.facebook.com/rokemanor> Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom. Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550. The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. www.roke.co.uk<http://www.roke.co.uk/?utm_source=Roke&utm_medium=Email&utm_content=Company%20Signature&utm_campaign=Roke>