diff --git a/xen/arch/arm/domain_build.c b/xen/arch/arm/domain_build.c
index 30b55588b7..9f662313ad 100644
--- a/xen/arch/arm/domain_build.c
+++ b/xen/arch/arm/domain_build.c
@@ -437,6 +437,50 @@ static bool __init allocate_bank_memory(struct domain *d,
     return true;
 }
 
+/*
+ * #ram_index and #ram_index refer to the index and starting address of guest
+ * memory kank stored in kinfo->mem.
+ * Static memory at #smfn of #tot_size shall be mapped #sgfn, and
+ * #sgfn will be next guest address to map when returning.
+ */
+static bool __init allocate_static_bank_memory(struct domain *d,
+                                               struct kernel_info *kinfo,
+                                               int ram_index,
+                                               paddr_t ram_addr,
+                                               gfn_t* sgfn,
+                                               mfn_t smfn,
+                                               paddr_t tot_size)
+{
+    int res;
+    struct membank *bank;
+    paddr_t _size = tot_size;
+
+    bank = &kinfo->mem.bank[ram_index];
+    bank->start = ram_addr;
+    bank->size = bank->size + tot_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;
+        }
+
+        *sgfn = gfn_add(*sgfn, 1UL << order);
+        smfn = mfn_add(smfn, 1UL << order);
+        tot_size -= (1ULL << (PAGE_SHIFT + order));
+    }
+
+    kinfo->mem.nr_banks = ram_index + 1;
+    kinfo->unassigned_mem -= _size;
+
+    return true;
+}
+
 static void __init allocate_memory(struct domain *d, struct kernel_info *kinfo)
 {
     unsigned int i;
@@ -480,6 +524,116 @@ fail:
           (unsigned long)kinfo->unassigned_mem >> 10);
 }
 
+/* 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)
+{
+    int nr_banks, _banks = 0;
+    size_t ram0_size = GUEST_RAM0_SIZE, ram1_size = GUEST_RAM1_SIZE;
+    paddr_t bank_start, bank_size;
+    gfn_t sgfn;
+    mfn_t smfn;
+
+    kinfo->mem.nr_banks = 0;
+    sgfn = gaddr_to_gfn(GUEST_RAM0_BASE);
+    nr_banks = d->arch.static_mem.nr_banks;
+    ASSERT(nr_banks >= 0);
+
+    if ( kinfo->unassigned_mem <= 0 )
+        goto fail;
+
+    while ( _banks < nr_banks )
+    {
+        bank_start = d->arch.static_mem.bank[_banks].start;
+        smfn = maddr_to_mfn(bank_start);
+        bank_size = d->arch.static_mem.bank[_banks].size;
+
+        if ( !alloc_domstatic_pages(d, bank_size >> PAGE_SHIFT, bank_start, 0) )
+        {
+            printk(XENLOG_ERR
+                    "%pd: cannot allocate static memory"
+                    "(0x%"PRIx64" - 0x%"PRIx64")",
+                    d, bank_start, bank_start + bank_size);
+            goto fail;
+        }
+
+        /*
+         * By default, it shall be mapped to the fixed guest RAM address
+         * `GUEST_RAM0_BASE`, `GUEST_RAM1_BASE`.
+         * Starting from RAM0(GUEST_RAM0_BASE).
+         */
+        if ( ram0_size )
+        {
+            /* RAM0 at most holds GUEST_RAM0_SIZE. */
+            if ( ram0_size >= bank_size )
+            {
+                if ( !allocate_static_bank_memory(d, kinfo,
+                                                  0, GUEST_RAM0_BASE,
+                                                  &sgfn, smfn, bank_size) )
+                    goto fail;
+
+                ram0_size = ram0_size - bank_size;
+                _banks++;
+                continue;
+            }
+            else /* bank_size > ram0_size */
+            {
+                if ( !allocate_static_bank_memory(d, kinfo,
+                                                  0, GUEST_RAM0_BASE,
+                                                  &sgfn, smfn, ram0_size) )
+                    goto fail;
+
+                /* The whole RAM0 is consumed. */
+                ram0_size -= ram0_size;
+                /* This bank hasn't been totally mapped, seeking to RAM1. */
+                bank_size = bank_size - ram0_size;
+                smfn = mfn_add(smfn, ram0_size >> PAGE_SHIFT);
+                sgfn = gaddr_to_gfn(GUEST_RAM1_BASE);
+            }
+        }
+
+        if ( ram1_size >= bank_size )
+        {
+            if ( !allocate_static_bank_memory(d, kinfo,
+                                              1, GUEST_RAM1_BASE,
+                                              &sgfn, smfn, bank_size) )
+            goto fail;
+
+            ram1_size = ram1_size - bank_size;
+            _banks++;
+            continue;
+        }
+        else
+            /*
+             * If RAM1 still couldn't meet the requirement,
+             * no way to seek for now.
+             */
+            goto fail;
+    }
+
+    if ( kinfo->unassigned_mem )
+        goto fail;
+
+    for( int i = 0; i < kinfo->mem.nr_banks; i++ )
+    {
+        printk(XENLOG_INFO "%pd BANK[%d] %#"PRIpaddr"-%#"PRIpaddr" (%ldMB)\n",
+               d,
+               i,
+               kinfo->mem.bank[i].start,
+               kinfo->mem.bank[i].start + kinfo->mem.bank[i].size,
+               /* Don't want format this as PRIpaddr (16 digit hex) */
+               (unsigned long)(kinfo->mem.bank[i].size >> 20));
+    }
+
+    return;
+
+fail:
+    panic("Failed to allocate requested domain memory."
+          /* Don't want format this as PRIpaddr (16 digit hex) */
+          " %ldKB unallocated. Fix the VMs configurations.\n",
+          (unsigned long)kinfo->unassigned_mem >> 10);
+}
+
 static int __init write_properties(struct domain *d, struct kernel_info *kinfo,
                                    const struct dt_device_node *node)
 {
@@ -2497,8 +2651,7 @@ static int __init construct_domU(struct domain *d,
     d->arch.type = kinfo.type;
 #endif
     if ( static_mem )
-        /* allocate_static_memory(d, &kinfo); */
-        BUG();
+        allocate_static_memory(d, &kinfo);
     else
         allocate_memory(d, &kinfo);
 
