Index: soft/giet_vm/sys/vm_handler.c
===================================================================
--- soft/giet_vm/sys/vm_handler.c	(revision 228)
+++ soft/giet_vm/sys/vm_handler.c	(revision 238)
@@ -8,8 +8,4 @@
 // They contains the kernel data structures and functions used to dynamically
 // handle the iommu page table.
-// 
-// TODO : We must transfer here the functions used to statically build
-// the page tables associated to the various vspaces (now in boot_handler.c)
-// 
 ///////////////////////////////////////////////////////////////////////////////////
 
@@ -18,4 +14,5 @@
 #include <common.h>
 #include <giet_config.h>
+#include <drivers.h>
 
 /////////////////////////////////////////////////////////////////////////////
@@ -88,65 +85,55 @@
 // Returns 0 if success, 1 if PTE1 or PTE2 unmapped
 //////////////////////////////////////////////////////////////////////////////
-unsigned int _v2p_translate(
-        page_table_t * pt,
-        unsigned int vpn,
-        unsigned int * ppn,        
-        unsigned int * flags) {
-    unsigned int ptba;
-    register unsigned int * pte2;
-    register unsigned int flags_value;
-    register unsigned int ppn_value;
+unsigned int _v2p_translate( page_table_t*   pt,
+                             unsigned int    vpn,
+                             unsigned int*   ppn,        
+                             unsigned int*   flags ) 
+{
+    paddr_t                 ptba;
+    paddr_t                 pte2;
+
+    register unsigned int   pte2_msb;
+    register unsigned int   pte2_lsb;
+    register unsigned int   flags_value;
+    register unsigned int   ppn_value;
 
     unsigned int ix1 = vpn >> 9;
     unsigned int ix2 = vpn & 0x1FF;
-    /*
-       _puts("\n\n********************** entering v2p_translate");
-       _puts("\n - pt    = ");
-       _putx( (unsigned int)pt );
-       _puts("\n - vpn   = ");
-       _putx( vpn << 12 );
-       _puts("\n - ptba  = ");
-       _putx( pt->pt1[ix1] << 12 ) ;
-       _puts("\n - &pte2 = ");
-       _putx( (pt->pt1[ix1] << 12) + 8*ix2 );
-       _puts("\n - flags = ");
-       _putx( *(unsigned int*)((pt->pt1[ix1] << 12) + 8*ix2) );
-       _puts("\n");
-       */
+
     // check PTE1 mapping
-    if ((pt->pt1[ix1] & PTE_V) == 0) {
-        return 1;
-    }
-    else {
+    if ((pt->pt1[ix1] & PTE_V) == 0) return 1;
+    else 
+    {
         // get physical addresses of pte2 
-        ptba = pt->pt1[ix1] << 12;
-        pte2 = (unsigned int *) (ptba + 8 * ix2);
+        ptba     = (paddr_t)(pt->pt1[ix1] & 0x0FFFFFFF) << 12;
+        pte2     = ptba + 8*ix2;
+        pte2_lsb = (unsigned int)pte2;
+        pte2_msb = (unsigned int)(pte2 >> 32);
 
         // gets ppn_value and flags_value, after temporary DTLB desactivation
         asm volatile (
-                "li      $27,    0xFFFFFFFE  \n"     /* Mask for IE bits     */
-                "mfc0    $26,    $12         \n"     /* save SR              */ 
-                "and     $27,    $26,    $27 \n"
-                "mtc0    $27,    $12         \n"     /* disable Interrupts   */
+                "li      $2,     0xFFFFFFFE  \n"     /* Mask for IE bits     */
+                "mfc0    $4,     $12         \n"     /* $4 <= SR             */ 
+                "and     $2,     $2,    $4   \n"
+                "mtc0    $2,     $12         \n"     /* disable Interrupts   */
 
-                "li      $27,    0xB         \n"     
-                "mtc2    $27,    $1          \n"     /* DTLB unactivated     */ 
+                "li      $3,     0xB         \n"     
+                "mtc2    $3,     $1          \n"     /* DTLB unactivated     */ 
 
-                "move    $27,    %2          \n"     /* $27 <= pte2          */
-                "lw      %0,     0($27)      \n"     /* read flags           */ 
-                "lw      %1,     4($27)      \n"     /* read ppn             */
+                "mtc2    %2,     $24         \n"     /* PADDR_EXT <= msb     */
+                "lw      %0,     0(%3)       \n"     /* read flags           */ 
+                "lw      %1,     4(%3)       \n"     /* read ppn             */
+                "mtc2    $0,     $24         \n"     /* PADDR_EXT <= 0       */
 
-                "li      $27,    0xF         \n" 
-                "mtc2    $27,    $1          \n"     /* DTLB activated       */
+                "li      $3,     0xF         \n" 
+                "mtc2    $3,     $1          \n"     /* DTLB activated       */
 
-                "mtc0    $26,    $12         \n"     /* restore SR           */
+                "mtc0    $4,     $12         \n"     /* restore SR           */
                 : "=r" (flags_value), "=r" (ppn_value)
-                : "r" (pte2)
-                : "$26","$27","$8");
+                : "r" (pte2_msb), "r" (pte2_lsb)
+                : "$2","$3","$4");
 
         // check PTE2 mapping
-        if ((flags_value & PTE_V) == 0) {
-            return 1;
-        }
+        if ((flags_value & PTE_V) == 0)  return 1; 
 
         // set return values 
