diff --git a/xen/arch/x86/domain_builder/core.c b/xen/arch/x86/domain_builder/core.c
index a80f3711c306..9335f3a9ebef 100644
--- a/xen/arch/x86/domain_builder/core.c
+++ b/xen/arch/x86/domain_builder/core.c
@@ -56,6 +56,18 @@ void __init builder_init(struct boot_info *bi)
 
         printk(XENLOG_INFO "  Number of domains: %d\n", bi->nr_domains);
     }
+    else
+    {
+        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 ff1ba58b6907..6bf1c4a297fe 100644
--- a/xen/arch/x86/domain_builder/fdt.c
+++ b/xen/arch/x86/domain_builder/fdt.c
@@ -14,6 +14,122 @@
 
 #include "fdt.h"
 
+static inline int __init fdt_get_prop_as_reg(
+    const void *fdt, int node, const char *name, unsigned int ssize,
+    unsigned int asize, uint64_t *size, uint64_t *addr)
+{
+    int ret;
+    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, name, &ret);
+    if ( !prop || ret < sizeof(u32) )
+        return ret < 0 ? ret : -EINVAL;
+
+    /* read address field */
+    cell = (fdt32_t *)prop->data;
+
+    if ( asize == 1 )
+    {
+        uint32_t val;
+        fdt_cell_as_u32(cell, &val);
+        *addr = (uint64_t)val;
+    }
+    else
+        fdt_cell_as_u64(cell, addr);
+
+    /* read size field */
+    cell += asize;
+
+    if ( ssize == 1 )
+    {
+        uint32_t val;
+        fdt_cell_as_u32(cell, &val);
+        *size = (uint64_t)val;
+    }
+    else
+        fdt_cell_as_u64(cell, size);
+
+    return 0;
+}
+
+static int __init dom0less_module_node(
+    void *fdt, int node, int size_size, int address_size)
+{
+    uint64_t size, addr;
+    int ret = fdt_get_prop_as_reg(fdt, node, "reg", size_size, address_size,
+                                  &size, &addr);
+    /* An FDT error value may have been returned, translate to -EINVAL */
+    if ( ret < 0 )
+        return -EINVAL;
+
+    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.
+     */
+    return (int)addr;
+}
+
+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);
+    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 )
+    {
+        printk("  failed processing #address or #size for domain %s)\n",
+               name == NULL ? "unknown" : name);
+        return -EINVAL;
+    }
+
+    fdt_for_each_subnode(node, fdt, dom_node)
+    {
+        if ( fdt_node_check_compatible(fdt, node, "multiboot,kernel") == 0 )
+        {
+            int idx = dom0less_module_node(fdt, node, size_size, address_size);
+            if ( idx < 0 )
+            {
+                printk("  failed processing kernel module for domain %s)\n",
+                       name == NULL ? "unknown" : name);
+                return idx;
+            }
+
+            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(void *fdt)
 {
     int hv_node = fdt_path_offset(fdt, "/chosen/hypervisor");
@@ -74,9 +190,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 84126db208ea..558d00a994fa 100644
--- a/xen/arch/x86/domain_builder/fdt.h
+++ b/xen/arch/x86/domain_builder/fdt.h
@@ -3,6 +3,7 @@
 #define __XEN_X86_FDT_H__
 
 #include <xen/init.h>
+#include <xen/libfdt/libfdt.h>
 
 #include <asm/bootinfo.h>
 
@@ -10,6 +11,22 @@
 #define HYPERLAUNCH_MODULE_IDX 0
 
 #ifdef CONFIG_DOMAIN_BUILDER
+
+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;
+}
+
 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 8041aeb3dcfd..d6e9d4c1769c 100644
--- a/xen/arch/x86/setup.c
+++ b/xen/arch/x86/setup.c
@@ -1280,11 +1280,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 */
