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
11void idle_thread(void)
12{
13    while (1) {
14        asm volatile("wfi");
15    }
16}
17
18/** DONT_TRANSLATE */
19void VISIBLE NO_INLINE halt(void)
20{
21#ifdef CONFIG_PRINTING
22    printf("halting...");
23#endif
24
25    sbi_shutdown();
26
27    UNREACHABLE();
28}
29