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
11#define TIMER_CLOCK_HZ ULL_CONST(@CONFIGURE_TIMER_FREQUENCY@)
12#define CLK_MAGIC @CONFIGURE_CLK_MAGIC@
13#define CLK_SHIFT @CONFIGURE_CLK_SHIFT@
14#define TIMER_PRECISION @CONFIGURE_TIMER_PRECISION@
15
16enum IRQConstants {
17    maxIRQ                      = @CONFIGURE_MAX_IRQ@
18} platform_interrupt_t;
19
20#define IRQ_CNODE_SLOT_BITS (@CONFIGURE_IRQ_SLOT_BITS@)
21
22#include <@CONFIGURE_INTERRUPT_CONTROLLER@>
23#include <@CONFIGURE_TIMER@>
24
25#cmakedefine CONFIGURE_SMMU <@CONFIGURE_SMMU@>
26#if (defined(CONFIGURE_SMMU) && defined(CONFIG_TK1_SMMU))
27#include CONFIGURE_SMMU
28#endif
29
30#cmakedefine CONFIGURE_SMMU <@CONFIGURE_SMMU@>
31#if (defined(CONFIGURE_SMMU) && defined(CONFIG_ARM_SMMU))
32#include CONFIGURE_SMMU
33
34#define SMMU_MAX_SID  @CONFIGURE_MAX_SID@
35#define SMMU_MAX_CB  @CONFIGURE_MAX_CB@
36
37#endif
38
39#ifdef CONFIG_KERNEL_MCS
40static inline CONST time_t getKernelWcetUs(void)
41{
42    return @CONFIGURE_KERNEL_WCET@;
43}
44#endif
45