1/*
2 * Copyright 2017, 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
13#ifndef __PLAT_MACHINE_DEVICES_H
14#define __PLAT_MACHINE_DEVICES_H
15
16/* These devices are used by the seL4 kernel. */
17#define BUS_ADDR_OFFSET             0x7E000000
18#define PADDR_OFFSET                0x3F000000
19
20#define INTC_BUSADDR                0x7E00B000
21#define UART_BUSADDR                0x7E215000
22#define SDHC_BUSADDR                0x7E300000
23#define USB2_BUSADDR                0x7E980000
24#define SYSTEM_TIMER_BUSADDR        0x7E003000
25#define ARM_TIMER_BUSADDR           0x7E00B000
26
27#define ARM_LOCAL_PADDR             0x40000000
28
29/* We convert from the VC CPU BUS addresses to ARM Physical addresses due to the extra
30    VC (Video controller) MMU */
31#define INTC_PADDR                  (INTC_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
32#define UART_PADDR                  (UART_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
33#define SDHC_PADDR                  (SDHC_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
34#define USB2_PADDR                  (USB2_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
35#define TIMER_PADDR                 (ARM_TIMER_BUSADDR-BUS_ADDR_OFFSET+PADDR_OFFSET)
36
37#endif /* !__PLAT_MACHINE_DEVICES_H */
38