1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: GPL-2.0-only
5  */
6 
7 #pragma once
8 
9 #include <config.h>
10 #include <arch/machine/timer.h>
11 
12 #ifdef CONFIG_KERNEL_MCS
13 #include <types.h>
14 #include <arch/linker.h>
15 
16 /* Read the current time from the timer. */
17 /** MODIFIES: [*] */
18 static inline ticks_t getCurrentTime(void);
19 /* set the next deadline irq - deadline is absolute */
20 /** MODIFIES: [*] */
21 static inline void setDeadline(ticks_t deadline);
22 /* ack previous deadline irq */
23 /** MODIFIES: [*] */
24 static inline void ackDeadlineIRQ(void);
25 
26 /* get the expected wcet of the kernel for this platform */
getKernelWcetTicks(void)27 static PURE inline ticks_t getKernelWcetTicks(void)
28 {
29     return usToTicks(getKernelWcetUs());
30 }
31 #else /* CONFIG_KERNEL_MCS */
32 static inline void resetTimer(void);
33 #endif /* !CONFIG_KERNEL_MCS */
34 
35