diff --git a/xen/arch/x86/domain-builder/core.c b/xen/arch/x86/domain-builder/core.c
index c50eff34fb68..eda7fa7a8ffa 100644
--- a/xen/arch/x86/domain-builder/core.c
+++ b/xen/arch/x86/domain-builder/core.c
@@ -59,6 +59,17 @@ void __init builder_init(struct boot_info *bi)
 
         printk(XENLOG_INFO "  Number of domains: %d\n", bi->nr_domains);
     }
+    else
+    {
+        unsigned int i;
+
+        /* Find first unknown boot module to use as Dom0 kernel */
+        printk("Falling back to using first boot module as dom0\n");
+        i = first_boot_module_index(bi, BOOTMOD_UNKNOWN);
+        bi->mods[i].type = BOOTMOD_KERNEL;
+        bi->domains[0].kernel = &bi->mods[i];
+        bi->nr_domains = 1;
+    }
 }
 
 /*
diff --git a/xen/arch/x86/domain-builder/fdt.c b/xen/arch/x86/domain-builder/fdt.c
index 5793bdc9fd47..bcaee50689a6 100644
--- a/xen/arch/x86/domain-builder/fdt.c
+++ b/xen/arch/x86/domain-builder/fdt.c
@@ -13,6 +13,114 @@
 
 #include "fdt.h"
 
+static int __init hl_module_index(void *fdt, int node, uint32_t *idx)
+{
+    int ret = 0;
+    const struct fdt_property *prop =
+        fdt_get_property(fdt, node, "module-index", &ret);
+
+    /* FDT error or bad idx pointer, translate to -EINVAL */
+    if ( ret < 0 || idx == NULL )
+        return -EINVAL;
+
+    fdt_cell_as_u32((fdt32_t *)prop->data, idx);
+
+    if ( *idx > MAX_NR_BOOTMODS )
+        return -ERANGE;
+
+    return 0;
+}
+
+static int __init dom0less_module_index(
+    void *fdt, int node, int size_size, int address_size, uint32_t *idx)
+{
+    uint64_t size = ~0UL, addr = ~0UL;
+    int ret =
+        fdt_get_reg_prop(fdt, node, address_size, size_size, &addr, &size, 1);
+
+    /* FDT error or bad idx pointer, translate to -EINVAL */
+    if ( ret < 0 || idx == NULL )
+        return -EINVAL;
+
+    /* Convention is that zero size indicates address is an index */
+    if ( size != 0 )
+        return -EOPNOTSUPP;
+
+    if ( addr > MAX_NR_BOOTMODS )
+        return -ERANGE;
+
+    /*
+     * MAX_NR_BOOTMODS cannot exceed the max for MB1, represented by a u32,
+     * thus the cast down to a u32 will be safe due to the prior check.
+     */
+    *idx = (uint32_t)addr;
+
+    return 0;
+}
+
+static int __init process_domain_node(
+    struct boot_info *bi, void *fdt, int dom_node)
+{
+    int node;
+    struct boot_domain *bd = &bi->domains[bi->nr_domains];
+    const char *name = fdt_get_name(fdt, dom_node, NULL) ?: "unknown";
+
+    fdt_for_each_subnode(node, fdt, dom_node)
+    {
+        if ( fdt_node_check_compatible(fdt, node, "multiboot,kernel") == 0 )
+        {
+            unsigned int idx;
+            int ret = 0;
+
+            if ( bd->kernel )
+            {
+                printk(XENLOG_ERR "Duplicate kernel module for domain %s)\n",
+                       name);
+                continue;
+            }
+
+            /* Try hyperlaunch property, fall back to dom0less property. */
+            if ( hl_module_index(fdt, node, &idx) < 0 )
+            {
+                int address_size = fdt_address_cells(fdt, dom_node);
+                int size_size = fdt_size_cells(fdt, dom_node);
+
+                if ( address_size < 0 || size_size < 0 )
+                    ret = -EINVAL;
+                else
+                    ret = dom0less_module_index(
+                            fdt, node, size_size, address_size, &idx);
+            }
+
+            if ( ret < 0 )
+            {
+                printk("  failed processing kernel module for domain %s)\n",
+                       name);
+                return ret;
+            }
+
+            if ( idx > bi->nr_modules )
+            {
+                printk("  invalid kernel module index for domain node (%d)\n",
+                       bi->nr_domains);
+                return -EINVAL;
+            }
+
+            printk("  kernel: boot module %d\n", idx);
+            bi->mods[idx].type = BOOTMOD_KERNEL;
+            bd->kernel = &bi->mods[idx];
+        }
+    }
+
+    if ( !bd->kernel )
+    {
+        printk(XENLOG_ERR "ERR: no kernel assigned to domain\n");
+        return -EFAULT;
+    }
+
+    return 0;
+}
+
 static int __init find_hyperlaunch_node(const void *fdt)
 {
     int hv_node = fdt_path_offset(fdt, "/chosen/hypervisor");
@@ -74,9 +182,19 @@ int __init walk_hyperlaunch_fdt(struct boot_info *bi)
 
     fdt_for_each_subnode(node, fdt, hv_node)
     {
+        if ( bi->nr_domains >= MAX_NR_BOOTDOMS )
+        {
+            printk(XENLOG_WARNING "WARN: more domains defined than max allowed");
+            break;
+        }
+
         ret = fdt_node_check_compatible(fdt, node, "xen,domain");
         if ( ret == 0 )
+        {
+            if ( (ret = process_domain_node(bi, fdt, node)) < 0 )
+                break;
             bi->nr_domains++;
+        }
     }
 
     /* Until multi-domain construction is added, throw an error */
diff --git a/xen/arch/x86/domain-builder/fdt.h b/xen/arch/x86/domain-builder/fdt.h
index f5b89cb54b29..0be4ac771bc4 100644
--- a/xen/arch/x86/domain-builder/fdt.h
+++ b/xen/arch/x86/domain-builder/fdt.h
@@ -3,6 +3,8 @@
 #define __XEN_X86_FDT_H__
 
 #include <xen/init.h>
+#include <xen/libfdt/libfdt.h>
+#include <xen/libfdt/libfdt-xen.h>
 
 #include <asm/bootinfo.h>
 
@@ -10,6 +12,7 @@
 #define HYPERLAUNCH_MODULE_IDX 0
 
 #ifdef CONFIG_DOMAIN_BUILDER
+
 int has_hyperlaunch_fdt(struct boot_info *bi);
 int walk_hyperlaunch_fdt(struct boot_info *bi);
 #else
diff --git a/xen/arch/x86/setup.c b/xen/arch/x86/setup.c
index e1aa9650d22e..71ce9315d3ac 100644
--- a/xen/arch/x86/setup.c
+++ b/xen/arch/x86/setup.c
@@ -1288,11 +1288,6 @@ void asmlinkage __init noreturn __start_xen(void)
 
     builder_init(bi);
 
-    /* Find first unknown boot module to use as Dom0 kernel */
-    i = first_boot_module_index(bi, BOOTMOD_UNKNOWN);
-    bi->mods[i].type = BOOTMOD_KERNEL;
-    bi->domains[0].kernel = &bi->mods[i];
-
     if ( pvh_boot )
     {
         /* pvh_init() already filled in e820_raw */
diff --git a/xen/include/xen/libfdt/libfdt-xen.h b/xen/include/xen/libfdt/libfdt-xen.h
index a5340bc9f4e1..27d23df03af3 100644
--- a/xen/include/xen/libfdt/libfdt-xen.h
+++ b/xen/include/xen/libfdt/libfdt-xen.h
@@ -13,6 +13,82 @@
 
 #include <xen/libfdt/libfdt.h>
 
+static inline int __init fdt_cell_as_u32(const fdt32_t *cell, uint32_t *val)
+{
+    *val = fdt32_to_cpu(*cell);
+
+    return 0;
+}
+
+static inline int __init fdt_cell_as_u64(const fdt32_t *cell, uint64_t *val)
+{
+    *val = ((uint64_t)fdt32_to_cpu(cell[0]) << 32) |
+           (uint64_t)fdt32_to_cpu(cell[1]);
+
+    return 0;
+}
+
+/*
+ * Property: reg
+ *
+ * Defined in Section 2.3.6 of the Device Tree Specification is the "reg"
+ * standard property. The property is a prop-encoded-array that is encoded as
+ * an arbitrary number of (address, length) pairs.
+ */
+static inline int __init fdt_get_reg_prop(
+    const void *fdt, int node, unsigned int asize, unsigned int ssize,
+    uint64_t *addr, uint64_t *size, unsigned int pairs)
+{
+    int ret;
+    unsigned int i, count;
+    const struct fdt_property *prop;
+    fdt32_t *cell;
+
+    /* FDT spec max size is 4 (128bit int), but largest arch int size is 64 */
+    if ( ssize > 2 || asize > 2 )
+        return -EINVAL;
+
+    prop = fdt_get_property(fdt, node, "reg", &ret);
+    if ( !prop || ret < sizeof(u32) )
+        return ret < 0 ? ret : -EINVAL;
+
+    /* Get the number of (addr, size) pairs and clamp down. */
+    count = fdt32_to_cpu(prop->len) / (ssize + asize);
+    count = count < pairs ? count : pairs;
+
+    cell = (fdt32_t *)prop->data;
+
+    for ( i = 0; i < count; i++ )
+    {
+        /* read address field */
+        if ( asize == 1 )
+        {
+            uint32_t val;
+            fdt_cell_as_u32(cell, &val);
+            addr[i] = val;
+        }
+        else
+            fdt_cell_as_u64(cell, &addr[i]);
+
+        /* read size field */
+        cell += asize;
+
+        if ( ssize == 1 )
+        {
+            uint32_t val;
+            fdt_cell_as_u32(cell, &val);
+            size[i] = val;
+        }
+        else
+            fdt_cell_as_u64(cell, &size[i]);
+
+        /* move to next pair */
+        cell += ssize;
+    }
+
+    return count;
+}
+
 static inline int fdt_get_mem_rsv_paddr(const void *fdt, int n,
                                         paddr_t *address,
                                         paddr_t *size)
