diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index cdb16f2086..ed290ee31b 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -480,6 +480,139 @@ fail:
           (unsigned long)kinfo->unassigned_mem >> 10);
 }
 
+static bool __init append_static_memory_to_bank(struct domain *d,
+                                                struct membank *bank,
+                                                mfn_t smfn,
+                                                paddr_t size)
+{
+    int res;
+    paddr_t tot_size = size;
+    /* Infer next GFN. */
+    gfn_t sgfn = gaddr_to_gfn(bank->start + bank->size);
+
+    while ( tot_size > 0 )
+    {
+        unsigned int order = get_allocation_size(tot_size);
+
+        res = guest_physmap_add_page(d, sgfn, smfn, order);
+        if ( res )
+        {
+            dprintk(XENLOG_ERR, "Failed map pages to DOMU: %d", res);
+            return false;
+        }
+
+        smfn = mfn_add(smfn, 1UL << order);
+        tot_size -= (1UL << (PAGE_SHIFT + order));
+    }
+
+    bank->size = bank->size + size;
+    return true;
+}
+
+/* Allocate memory from static memory as RAM for one specific domain d. */
+static void __init allocate_static_memory(struct domain *d,
+                                          struct kernel_info *kinfo,
+                                          const struct dt_property *prop,
+                                          u32 addr_cells, u32 size_cells)
+{
+    unsigned int nr_banks, gbank, bank = 0;
+    const uint64_t rambase[] = GUEST_RAM_BANK_BASES;
+    const uint64_t ramsize[] = GUEST_RAM_BANK_SIZES;
+    const __be32 *cell;
+    u32 reg_cells = addr_cells + size_cells;
+    u64 tot_size = 0;
+    paddr_t pbase, psize, gsize;
+    mfn_t smfn;
+
+    /* Start with GUEST_RAM0. */
+    kinfo->mem.nr_banks = 0;
+    gbank = 0;
+    gsize = ramsize[gbank];
+    kinfo->mem.bank[gbank].start = rambase[gbank];
+
+    cell = (const __be32 *)prop->value;
+    nr_banks = (prop->length) / (reg_cells * sizeof (u32));
+    BUG_ON(nr_banks > NR_MEM_BANKS);
+
+    while ( bank < nr_banks )
+    {
+        device_tree_get_reg(&cell, addr_cells, size_cells, &pbase, &psize);
+        tot_size += psize;
+        smfn = maddr_to_mfn(pbase);
+
+        if ( !acquire_domstatic_pages(d, psize >> PAGE_SHIFT, smfn, 0) )
+        {
+            printk(XENLOG_ERR
+                    "%pd: cannot acquire static memory "
+                    "(0x%"PRIpaddr" - 0x%"PRIpaddr").\n",
+                    d, pbase, pbase + psize);
+            goto fail;
+        }
+
+        printk(XENLOG_INFO "%pd: STATIC BANK[%d] %#"PRIpaddr"-%#"PRIpaddr"\n",
+               d, bank, pbase, pbase + psize);
+
+        /*
+         * It shall be mapped to the fixed guest RAM address rambase[i],
+         * And until it exhausts the ramsize[i], it will seek to the next
+         * rambase[i+1].
+         */
+        while ( 1 )
+        {
+            /*
+             * The current physical bank is fully mapped.
+             * Handle the next physical bank.
+             */
+            if ( gsize >= psize )
+            {
+                if ( !append_static_memory_to_bank(d, &kinfo->mem.bank[gbank],
+                                                   smfn, psize) )
+                    goto fail;
+
+                gsize = gsize - psize;
+                bank++;
+                break;
+            }
+            /*
+             * Current guest bank memory is not enough to map.
+             * Check if we have another guest bank available.
+             * gbank refers guest memory bank index.
+             */
+            else if ( (gbank + 2) > GUEST_RAM_BANKS ) {
+                printk("Exhausted the number of guest bank\n");
+                goto fail;
+            }
+            else
+            {
+                if ( !append_static_memory_to_bank(d, &kinfo->mem.bank[gbank],
+                                                   smfn, gsize) )
+                    goto fail;
+
+                psize = psize - gsize;
+                smfn = mfn_add(smfn, gsize >> PAGE_SHIFT);
+                /* Update to the next guest bank. */
+                gbank++;
+                gsize = ramsize[gbank];
+                kinfo->mem.bank[gbank].start = rambase[gbank];
+            }
+        }
+    }
+
+    kinfo->mem.nr_banks = ++gbank;
+    kinfo->unassigned_mem -= tot_size;
+    if ( kinfo->unassigned_mem )
+        printk(XENLOG_ERR
+               "Size of \"memory\" property doesn't match up with the ones "
+               "defined in \"xen,static-mem\".\n");
+
+    return;
+
+fail:
+    panic("Failed to allocate requested static memory for domain %pd."
+          "Fix the VMs configurations.\n",
+          d);
+}
+
 static int __init write_properties(struct domain *d, struct kernel_info *kinfo,
                                    const struct dt_device_node *node)
 {
@@ -2486,8 +2619,8 @@ static int __init construct_domU(struct domain *d,
     if ( !static_mem )
         allocate_memory(d, &kinfo);
     else
-        /* TODO: allocate_static_memory(...). */
-        BUG();
+        allocate_static_memory(d, &kinfo, static_mem_prop,
+                               static_mem_addr_cells, static_mem_size_cells);
 
     rc = prepare_dtb_domU(d, &kinfo);
     if ( rc < 0 )
