1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#include <config.h>
8#include <types.h>
9#include <machine/io.h>
10#include <kernel/vspace.h>
11#include <arch/machine.h>
12#include <arch/kernel/vspace.h>
13#include <linker.h>
14
15/* gptcr bits */
16#define EN     0
17#define ENMOD  1
18#define FRR    9
19#define CLKSRC 6
20#define SWR    15
21
22timer_t *gpt = (timer_t *) TIMER_PPTR;
23ticks_t high_bits = 0;
24
25enum IPGConstants {
26    IPG_CLK = 1,
27    IPG_CLK_HIGHFREQ = 2,
28    IPG_CLK_32K = 3
29};
30
31BOOT_CODE void initTimer(void)
32{
33    /* reset the gpt */
34    gpt->gptcr = 0;
35    /* clear the status register */
36    gpt->gptcr = 0x3F;
37    /* software reset */
38    gpt->gptcr = BIT(SWR);
39    /* configure the gpt */
40    gpt->gptcr = BIT(ENMOD) | BIT(FRR) | (IPG_CLK_HIGHFREQ << CLKSRC);
41    /* enable overflow irq */
42    gpt->gptir = BIT(ROV);
43    /* turn it on */
44    gpt->gptcr |= BIT(EN);
45}
46