1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(GD_GPL)
9 */
10
11#ifndef __ARCH_ARMV7A_MACHINE_H
12#define __ARCH_ARMV7A_MACHINE_H
13
14#include <util.h>
15
16/* See idle_thread for an explanation as to why FORCE_INLINE is required here. */
17static inline void FORCE_INLINE wfi(void)
18{
19    asm volatile("wfi" ::: "memory");
20}
21
22static inline void dsb(void)
23{
24    asm volatile("dsb" ::: "memory");
25}
26
27static inline void dmb(void)
28{
29    asm volatile("dmb" ::: "memory");
30}
31
32static inline void isb(void)
33{
34    asm volatile("isb" ::: "memory");
35}
36
37void lockTLBEntryCritical(unsigned int addr, unsigned int x, unsigned int y);
38
39#endif
40