1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4  *
5  * SPDX-License-Identifier: GPL-2.0-only
6  */
7 
8 #include <config.h>
9 #include <arch/sbi.h>
10 
idle_thread(void)11 void idle_thread(void)
12 {
13     while (1) {
14         asm volatile("wfi");
15     }
16 }
17 
18 /** DONT_TRANSLATE */
halt(void)19 void VISIBLE NO_INLINE halt(void)
20 {
21 #ifdef CONFIG_PRINTING
22     printf("halting...");
23 #endif
24 
25     sbi_shutdown();
26 
27     UNREACHABLE();
28 }
29