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