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 */
18asid_pool_t *riscvKSASIDTable[BIT(asidHighBits)];
19
20/* Kernel Page Tables */
21pte_t kernel_root_pageTable[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
22
23#if __riscv_xlen != 32
24pte_t kernel_image_level2_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
25pte_t kernel_image_level2_dev_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
26#elif defined(CONFIG_KERNEL_LOG_BUFFER)
27pte_t kernel_image_level2_log_buffer_pt[BIT(PT_INDEX_BITS)] ALIGN_BSS(BIT(seL4_PageTableBits));
28#endif
29
30SMP_STATE_DEFINE(core_map_t, coreMap);
31