1/*
2 * Copyright 2018, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
8 * See "LICENSE_GPLv2.txt" for details.
9 *
10 * @TAG(DATA61_GPL)
11 */
12#ifndef __MACHINE_TIMER_H
13#define __MACHINE_TIMER_H
14
15#include <types.h>
16#include <arch/linker.h>
17#include <arch/machine/timer.h>
18
19/* Read the current time from the timer. */
20/** MODIFIES: [*] */
21static inline ticks_t getCurrentTime(void);
22/* set the next deadline irq - deadline is absolute */
23/** MODIFIES: [*] */
24static inline void setDeadline(ticks_t deadline);
25/* ack previous deadline irq */
26/** MODIFIES: [*] */
27static inline void ackDeadlineIRQ(void);
28
29/* get the expected wcet of the kernel for this platform */
30static PURE inline ticks_t
31getKernelWcetTicks(void)
32{
33    return usToTicks(getKernelWcetUs());
34}
35
36#endif /* __MACHINE_TIMER_H */
37