2 * (c) 2009 Adam Lackorzynski <adam@os.inf.tu-dresden.de>
3 * economic rights: Technische Universität Dresden (Germany)
4 * This file is part of TUD:OS and distributed under the terms of the
5 * GNU Lesser General Public License 2.1.
6 * Please see the COPYING-LGPL-2.1 file for details.
8 #include <l4/sys/types.h>
9 #include <l4/util/rdtsc.h>
11 l4_uint32_t l4_scaler_tsc_to_us;
12 l4_uint32_t l4_scaler_timer_to_tsc;
15 l4_tsc_init (int constraint, l4_kernel_info_t *kip)
18 l4_scaler_timer_to_tsc = (kip->frequency_cpu * 1000)
19 / (kip->frequency_bus / 4);
20 l4_scaler_tsc_to_us = (kip->frequency_cpu) / 1000;