1/*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7typedef unsigned int uint32_t;
8typedef unsigned char uint8_t;
9
10typedef uint32_t paddr_t;
11typedef uint32_t word_t;
12typedef uint8_t hw_asid_t;
13
14word_t x;
15
16/* Address space control */
17/** MODIFIES: x */
18void setCurrentPD(paddr_t addr);
19/** MODIFIES: [*] */
20void setHardwareASID(hw_asid_t hw_asid);
21
22/* TLB control */
23/** MODIFIES: [*] */
24void invalidateTLB(void);
25/** MODIFIES: [*] */
26void invalidateHWASID(hw_asid_t hw_asid);
27/** MODIFIES: [*] */
28void invalidateMVA(word_t mva_plus_asid);
29/** MODIFIES: [*] */
30void lockTLBEntry(word_t vaddr);
31
32void test() {
33  setCurrentPD(0);
34  }
35
36
37