+/* Read the time stamp counter */
+static inline uint64_t rdtsc(void)
+{
+ uint32_t high, low;
+ __asm__ __volatile__("rdtsc" : "=a" (low), "=d" (high));
+ return (((uint64_t)high) << 32) | low;
+}
+
+/* board/... */
+void timer_set_tsc_base(uint64_t new_base);
+uint64_t timer_get_tsc(void);
+