void
tsc_init(void)
{
    uint64_t	busFreq;
    uint64_t	busFCvtInt;
    uint32_t	cpuModel;
    uint32_t	cpuFamily;
    uint32_t	xcpuid[4];

    /*
     * Get the FSB frequency and conversion factors.
     */
    busFreq = EFI_FSB_frequency();
    if (busFreq != 0) {
	busFCvtt2n = ((1 * Giga) << 32) / busFreq;
	busFCvtn2t = 0xFFFFFFFFFFFFFFFFULL / busFCvtt2n;
	busFCvtInt = tmrCvt(1 * Peta, 0xFFFFFFFFFFFFFFFFULL / busFreq); 
    } else {
	panic("rtclock_init: EFI not supported!\n");
    }
	
    kprintf(" BUS: Frequency = %6d.%04dMHz, "
	    "cvtt2n = %08X.%08X, cvtn2t = %08X.%08X, "
	    "cvtInt = %08X.%08X\n",
	    (uint32_t)(busFreq / Mega),
	    (uint32_t)(busFreq % Mega), 
	    (uint32_t)(busFCvtt2n >> 32), (uint32_t)busFCvtt2n,
	    (uint32_t)(busFCvtn2t >> 32), (uint32_t)busFCvtn2t,
	    (uint32_t)(busFCvtInt >> 32), (uint32_t)busFCvtInt);

    do_cpuid(1, xcpuid);
    cpuFamily = ( xcpuid[eax] >> 8 ) & 0xf;
    /*
     * Get the extended family if necessary.
     */
    if (cpuFamily == 0x0f)
	cpuFamily += (xcpuid[eax] >> 20) & 0x00ff;

    cpuModel = ( xcpuid[eax] >> 4 ) & 0xf;
    /*
     * Get the extended model if necessary.
     */
    if (cpuFamily == CPUID_FAMILY_686
	|| cpuFamily == CPUID_FAMILY_EXTENDED)
	cpuModel += ((xcpuid[eax] >> 16) & 0xf) << 4;

    /*
     * Get the TSC increment.  The TSC is incremented by this
     * on every bus tick.  Calculate the TSC conversion factors
     * to and from nano-seconds.
     */
    if (cpuFamily == CPUID_FAMILY_686) {
	if (cpuModel == CPUID_MODEL_CORE || cpuModel == CPUID_MODEL_CORE2) {
	uint64_t	prfsts;
	
	prfsts = rdmsr64(IA32_PERF_STS);
	tscGranularity = (uint32_t)(prfsts >> BusRatioShift) & BusRatioMask;
	} else {
	    panic("rtclock_init: unknown CPU model: 0x%X\n",
	      cpuModel);
	}
    } else {
	panic("rtclock_init: unknown CPU family: 0x%X\n",
	      cpuFamily);
    }
	
    tscFCvtt2n = busFCvtt2n / (uint64_t)tscGranularity;
    tscFreq = ((1 * Giga)  << 32) / tscFCvtt2n;
    tscFCvtn2t = 0xFFFFFFFFFFFFFFFFULL / tscFCvtt2n;

    kprintf(" TSC: Frequency = %6d.%04dMHz, "
	    "cvtt2n = %08X.%08X, cvtn2t = %08X.%08X, gran = %d\n",
	    (uint32_t)(tscFreq / Mega),
	    (uint32_t)(tscFreq % Mega), 
	    (uint32_t)(tscFCvtt2n >> 32), (uint32_t)tscFCvtt2n,
	    (uint32_t)(tscFCvtn2t >> 32), (uint32_t)tscFCvtn2t,
	    tscGranularity);

    /*
     * Calculate conversion from BUS to TSC
     */
    bus2tsc = tmrCvt(busFCvtt2n, tscFCvtn2t);
}