1 /*
2  * Copyright 2020, DornerWorks
3  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
4  * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
5  *
6  * SPDX-License-Identifier: GPL-2.0-only
7  */
8 
9 #include <util.h>
10 #include <api/types.h>
11 #include <arch/types.h>
12 #include <arch/model/statedata.h>
13 #include <arch/object/structures.h>
14 #include <linker.h>
15 #include <plat/machine/hardware.h>
16 
17 /* The top level asid mapping table */
18 asid_pool_t *riscvKSASIDTable[BIT(asidHighBits)];
19 
20 /* Kernel Page Tables */
21 pte_t kernel_root_pageTable[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
22 
23 #if __riscv_xlen != 32
24 pte_t kernel_image_level2_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
25 pte_t kernel_image_level2_dev_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
26 #elif defined(CONFIG_KERNEL_LOG_BUFFER)
27 pte_t kernel_image_level2_log_buffer_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
28 #endif
29 
30 SMP_STATE_DEFINE(core_map_t, coreMap);
31