diff --git a/xen/arch/arm/include/asm/mmu/mm.h b/xen/arch/arm/include/asm/mmu/mm.h
index 7f4d59137d..819fe923a4 100644
--- a/xen/arch/arm/include/asm/mmu/mm.h
+++ b/xen/arch/arm/include/asm/mmu/mm.h
@@ -69,8 +69,6 @@ static inline void *maddr_to_virt(paddr_t ma)
  */
 static inline void *maddr_to_virt(paddr_t ma)
 {
-    ASSERT((mfn_to_pdx(maddr_to_mfn(ma)) - directmap_base_pdx) <
-           (DIRECTMAP_SIZE >> PAGE_SHIFT));
     return (void *)(XENHEAP_VIRT_START -
                     (directmap_base_pdx << PAGE_SHIFT) +
                     maddr_to_directmapoff(ma));
diff --git a/xen/arch/arm/mmu/mm.c b/xen/arch/arm/mmu/mm.c
index 69617a4986..e24fca8c70 100644
--- a/xen/arch/arm/mmu/mm.c
+++ b/xen/arch/arm/mmu/mm.c
@@ -25,6 +25,7 @@ init_frametable_chunk(unsigned long pdx_s, unsigned long pdx_e)
     base_mfn = alloc_boot_pages(chunk_size >> PAGE_SHIFT, 32 << (20 - 12));
 
     virt = (unsigned long)pdx_to_page(pdx_s);
+    printk("DEBUG %s %d virt=%lx base_mfn=%lx pfn_start=%lx pfn_end=%lx\n",__func__,__LINE__,(unsigned long)virt,mfn_x(base_mfn),mfn_x(pdx_to_mfn(pdx_s)),mfn_x(pdx_to_mfn(pdx_e)));
     rc = map_pages_to_xen(virt, base_mfn, chunk_size >> PAGE_SHIFT,
                           PAGE_HYPERVISOR_RW | _PAGE_BLOCK);
     if ( rc )
@@ -51,12 +52,9 @@ void __init init_frametable(void)
 
     max_pdx = pfn_to_pdx(max_page - 1) + 1;
 
-    if ( max_pdx > FRAMETABLE_NR )
-        panic("Frametable too small\n");
-
     max_idx = DIV_ROUND_UP(max_pdx, PDX_GROUP_COUNT);
 
-    for ( sidx = (frametable_base_pdx / PDX_GROUP_COUNT); ; sidx = nidx )
+    for ( sidx = 0; ; sidx = nidx )
     {
         eidx = find_next_zero_bit(pdx_group_valid, max_idx, sidx);
         nidx = find_next_bit(pdx_group_valid, max_idx, eidx);
@@ -64,6 +62,7 @@ void __init init_frametable(void)
         if ( nidx >= max_idx )
             break;
 
+        printk("DEBUG %s %d start=%lx end=%lx\n",__func__,__LINE__,mfn_x(pdx_to_mfn(sidx * PDX_GROUP_COUNT)),mfn_x(pdx_to_mfn(eidx * PDX_GROUP_COUNT)));
         init_frametable_chunk(sidx * PDX_GROUP_COUNT, eidx * PDX_GROUP_COUNT);
     }
 
diff --git a/xen/arch/arm/setup.c b/xen/arch/arm/setup.c
index c9ad6bbab6..1f5c1866c4 100644
--- a/xen/arch/arm/setup.c
+++ b/xen/arch/arm/setup.c
@@ -291,6 +291,7 @@ void __init init_pdx(void)
         bank_size = mem->bank[bank].size;
         bank_end = bank_start + bank_size;
 
+        printk("DEBUG %s %d start=%lx end=%lx\n",__func__,__LINE__,bank_start,bank_end);
         set_pdx_range(paddr_to_pfn(bank_start),
                       paddr_to_pfn(bank_end));
     }