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#pragma once
9
10#include <config.h>
11#include <arch/object/structures.h>
12#include <mode/hardware.h>
13
14#ifdef CONFIG_ENABLE_BENCHMARKS
15static inline timestamp_t timestamp(void)
16{
17    return riscv_read_cycle();
18}
19#endif /* CONFIG_ENABLE_BENCHMARK */
20
21