diff --git a/tools/config.h.in b/tools/config.h.in
index d55173b9a8..478a2ccd40 100644
--- a/tools/config.h.in
+++ b/tools/config.h.in
@@ -14,6 +14,10 @@
    you don't. */
 #undef HAVE_DECL_FDT_NEXT_SUBNODE
 
+/* Define to 1 if you have the declaration of `fdt_property_u32', and to 0 if
+   you don't. */
+#undef HAVE_DECL_FDT_PROPERTY_U32
+
 /* Define to 1 if you have the `fdt_first_subnode' function. */
 #undef HAVE_FDT_FIRST_SUBNODE
 
diff --git a/tools/configure b/tools/configure
index 896d8928f1..9e87e90ceb 100755
--- a/tools/configure
+++ b/tools/configure
@@ -8906,6 +8906,21 @@ cat >>confdefs.h <<_ACEOF
 #define HAVE_DECL_FDT_NEXT_SUBNODE $ac_have_decl
 _ACEOF
 
+
+# The helper fdt_property_u32 is only present in libfdt >= 1.4.0
+# It's an inline function, so only check if the declaration is present
+ac_fn_c_check_decl "$LINENO" "fdt_property_u32" "ac_cv_have_decl_fdt_property_u32" "#include <libfdt.h>
+"
+if test "x$ac_cv_have_decl_fdt_property_u32" = xyes; then :
+  ac_have_decl=1
+else
+  ac_have_decl=0
+fi
+
+cat >>confdefs.h <<_ACEOF
+#define HAVE_DECL_FDT_PROPERTY_U32 $ac_have_decl
+_ACEOF
+
 esac
 
 # Checks for header files.
diff --git a/tools/configure.ac b/tools/configure.ac
index 1a06ddf98d..2886cb5591 100644
--- a/tools/configure.ac
+++ b/tools/configure.ac
@@ -379,6 +379,10 @@ AS_IF([test "x$partial_dt" = "xy" ],
 #   * The prototype exists but the functions are not exposed. Don't ask why...
 AC_CHECK_FUNCS([fdt_first_subnode fdt_next_subnode])
 AC_CHECK_DECLS([fdt_first_subnode, fdt_next_subnode],,,[#include <libfdt.h>])
+
+# The helper fdt_property_u32 is only present in libfdt >= 1.4.0
+# It's an inline function, so only check if the declaration is present
+AC_CHECK_DECLS([fdt_property_u32],,,[#include <libfdt.h>])
 esac
 
 # Checks for header files.
diff --git a/tools/libxl/libxl_arm.c b/tools/libxl/libxl_arm.c
index 4fb5e26fab..f09c860aa6 100644
--- a/tools/libxl/libxl_arm.c
+++ b/tools/libxl/libxl_arm.c
@@ -444,7 +444,9 @@ static int make_gicv3_node(libxl__gc *gc, void *fdt)
     return 0;
 }
 
-static int make_timer_node(libxl__gc *gc, void *fdt, const struct arch_info *ainfo)
+static int make_timer_node(libxl__gc *gc, void *fdt,
+                           const struct arch_info *ainfo,
+                           uint32_t frequency)
 {
     int res;
     gic_interrupt ints[3];
@@ -462,6 +464,9 @@ static int make_timer_node(libxl__gc *gc, void *fdt, const struct arch_info *ain
     res = fdt_property_interrupts(gc, fdt, ints, 3);
     if (res) return res;
 
+    if ( frequency )
+        fdt_property_u32(fdt, "clock-frequency", frequency);
+
     res = fdt_end_node(fdt);
     if (res) return res;
 
@@ -805,7 +810,7 @@ next_resize:
             goto out;
         }
 
-        FDT( make_timer_node(gc, fdt, ainfo) );
+        FDT( make_timer_node(gc, fdt, ainfo, xc_config->clock_frequency) );
         FDT( make_hypervisor_node(gc, fdt, vers) );
 
         if (pfdt)
diff --git a/tools/libxl/libxl_libfdt_compat.h b/tools/libxl/libxl_libfdt_compat.h
index 53a507606d..23230b51b1 100644
--- a/tools/libxl/libxl_libfdt_compat.h
+++ b/tools/libxl/libxl_libfdt_compat.h
@@ -61,6 +61,7 @@
 #define LIBXL_LIBFDT_COMPAT_H
 
 #include "libxl_internal.h"
+#include <libfdt.h>
 
 #if !HAVE_DECL_FDT_FIRST_SUBNODE
 _hidden int fdt_first_subnode(const void *fdt, int offset);
@@ -70,6 +71,14 @@ _hidden int fdt_first_subnode(const void *fdt, int offset);
 _hidden int fdt_next_subnode(const void *fdt, int offset);
 #endif
 
+#if !HAVE_DECL_FDT_PROPERTY_U32
+static inline int fdt_property_u32(void *fdt, const char *name, uint32_t val)
+{
+	uint32_t tmp = cpu_to_fdt32(val);
+	return fdt_property(fdt, name, &tmp, sizeof(tmp));
+}
+#endif
+
 #endif
 
 /*
diff --git a/xen/arch/arm/domain.c b/xen/arch/arm/domain.c
index 24b89380f8..8b1bf5a354 100644
--- a/xen/arch/arm/domain.c
+++ b/xen/arch/arm/domain.c
@@ -593,7 +593,7 @@ int arch_domain_create(struct domain *d, unsigned int domcr_flags,
     if ( (rc = domain_vgic_init(d, config->nr_spis)) != 0 )
         goto fail;
 
-    if ( (rc = domain_vtimer_init(d)) != 0 )
+    if ( (rc = domain_vtimer_init(d, config)) != 0 )
         goto fail;
 
     /*
diff --git a/xen/arch/arm/time.c b/xen/arch/arm/time.c
index ce6d3fd5dc..5ded30c031 100644
--- a/xen/arch/arm/time.c
+++ b/xen/arch/arm/time.c
@@ -42,6 +42,8 @@ uint64_t __read_mostly boot_count;
  * register-mapped time source in the SoC. */
 unsigned long __read_mostly cpu_khz;  /* CPU clock frequency in kHz. */
 
+uint32_t __read_mostly timer_dt_clock_frequency;
+
 static unsigned int timer_irq[MAX_TIMER_PPI];
 
 unsigned int timer_get_irq(enum timer_ppi ppi)
@@ -86,7 +88,10 @@ void __init preinit_xen_time(void)
 
     res = dt_property_read_u32(timer, "clock-frequency", &rate);
     if ( res )
+    {
         cpu_khz = rate / 1000;
+        timer_dt_clock_frequency = rate;
+    }
     else
         cpu_khz = READ_SYSREG32(CNTFRQ_EL0) / 1000;
 
diff --git a/xen/arch/arm/vtimer.c b/xen/arch/arm/vtimer.c
index 685bfea2d6..1418092aeb 100644
--- a/xen/arch/arm/vtimer.c
+++ b/xen/arch/arm/vtimer.c
@@ -60,11 +60,13 @@ static void virt_timer_expired(void *data)
     perfc_incr(vtimer_virt_inject);
 }
 
-int domain_vtimer_init(struct domain *d)
+int domain_vtimer_init(struct domain *d, struct xen_arch_domainconfig *config)
 {
     d->arch.phys_timer_base.offset = NOW();
     d->arch.virt_timer_base.offset = READ_SYSREG64(CNTPCT_EL0);
 
+    config->clock_frequency = timer_dt_clock_frequency;
+
     /* At this stage vgic_reserve_virq can't fail */
     if ( is_hardware_domain(d) )
     {
diff --git a/xen/arch/arm/vtimer.h b/xen/arch/arm/vtimer.h
index 6d2e46efe2..99e81454e5 100644
--- a/xen/arch/arm/vtimer.h
+++ b/xen/arch/arm/vtimer.h
@@ -20,7 +20,8 @@
 #ifndef __ARCH_ARM_VTIMER_H__
 #define __ARCH_ARM_VTIMER_H__
 
-extern int domain_vtimer_init(struct domain *d);
+extern int domain_vtimer_init(struct domain *d,
+                              struct xen_arch_domainconfig *config);
 extern int vcpu_vtimer_init(struct vcpu *v);
 extern int vtimer_emulate(struct cpu_user_regs *regs, union hsr hsr);
 extern int virt_timer_save(struct vcpu *v);
diff --git a/xen/include/asm-arm/time.h b/xen/include/asm-arm/time.h
index 039039a416..d755f36d0b 100644
--- a/xen/include/asm-arm/time.h
+++ b/xen/include/asm-arm/time.h
@@ -22,6 +22,12 @@ enum timer_ppi
     MAX_TIMER_PPI = 4,
 };
 
+/*
+ * Value of "clock-frequency" in the DT timer node if present.
+ * 0 means the property doesn't exist.
+ */
+extern uint32_t timer_dt_clock_frequency;
+
 /* Get one of the timer IRQ number */
 unsigned int timer_get_irq(enum timer_ppi ppi);
 
diff --git a/xen/include/public/arch-arm.h b/xen/include/public/arch-arm.h
index 6f24c5f14f..805483ea80 100644
--- a/xen/include/public/arch-arm.h
+++ b/xen/include/public/arch-arm.h
@@ -311,6 +311,20 @@ struct xen_arch_domainconfig {
     uint8_t gic_version;
     /* IN */
     uint32_t nr_spis;
+    /*
+     * OUT
+     * Based on the property clock-frequency in the DT timer node.
+     * The property may be present when the bootloader/firmware doesn't
+     * set correctly CNTFRQ which hold the timer frequency.
+     *
+     * As it's not possible to trap this register, we have to replicate
+     * the value in the guest DT.
+     *
+     * = 0 => property not present
+     * > 0 => Value of the property
+     *
+     */
+    uint32_t clock_frequency;
 };
 #endif /* __XEN__ || __XEN_TOOLS__ */