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: LinkedInhttp://www.linkedin.com/company/roke-manor-research | Twitterhttps://twitter.com/rokemanor | Facebookhttps://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.ukhttp://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.ukmailto:ben.turner@roke.co.uk> Date: Thursday, 20 February 2020 at 3:06 am To: "Shen, Yanyan (Data61, Kensington NSW)" <Yanyan.Shen@data61.csiro.aumailto:Yanyan.Shen@data61.csiro.au>, "devel@sel4.systemsmailto:devel@sel4.systems" <devel@sel4.systemsmailto:devel@sel4.systems> Cc: "Millar, Curtis (Data61, Kensington NSW)" <Curtis.Millar@data61.csiro.aumailto:Curtis.Millar@data61.csiro.au>, "Mcleod, Kent (Data61, Kensington NSW)" <Kent.Mcleod@data61.csiro.aumailto: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: LinkedInhttp://www.linkedin.com/company/roke-manor-research | Twitterhttps://twitter.com/rokemanor | Facebookhttps://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.ukhttp://www.roke.co.uk/?utm_source=Roke&utm_medium=Email&utm_content=Company%20Signature&utm_campaign=Roke