unsigned int irqbase);
 extern void gic_clocksource_init(unsigned int);
 extern cycle_t gic_read_count(void);
+extern unsigned int gic_get_count_width(void);
 extern cycle_t gic_read_compare(void);
 extern void gic_write_compare(cycle_t cnt);
 extern void gic_write_cpu_compare(cycle_t cnt, int cpu);
 
 
 void __init gic_clocksource_init(unsigned int frequency)
 {
-       unsigned int config, bits;
-
-       /* Calculate the clocksource mask. */
-       GICREAD(GIC_REG(SHARED, GIC_SH_CONFIG), config);
-       bits = 32 + ((config & GIC_SH_CONFIG_COUNTBITS_MSK) >>
-               (GIC_SH_CONFIG_COUNTBITS_SHF - 2));
-
        /* Set clocksource mask. */
-       gic_clocksource.mask = CLOCKSOURCE_MASK(bits);
+       gic_clocksource.mask = CLOCKSOURCE_MASK(gic_get_count_width());
 
        /* Calculate a somewhat reasonable rating value. */
        gic_clocksource.rating = 200 + frequency / 10000000;
 
        return (((cycle_t) hi) << 32) + lo;
 }
 
+unsigned int gic_get_count_width(void)
+{
+       unsigned int bits, config;
+
+       GICREAD(GIC_REG(SHARED, GIC_SH_CONFIG), config);
+       bits = 32 + 4 * ((config & GIC_SH_CONFIG_COUNTBITS_MSK) >>
+                        GIC_SH_CONFIG_COUNTBITS_SHF);
+
+       return bits;
+}
+
 void gic_write_compare(cycle_t cnt)
 {
        GICWRITE(GIC_REG(VPE_LOCAL, GIC_VPE_COMPARE_HI),