Index: soft/giet_vm/giet_boot/boot.c
===================================================================
--- soft/giet_vm/giet_boot/boot.c	(revision 316)
+++ soft/giet_vm/giet_boot/boot.c	(revision 321)
@@ -22,5 +22,5 @@
 //    - the "map.bin" file contains the hardware architecture description and the
 //      mapping directives. It must be stored in the the seg_boot_mapping segment 
-//      (at address seg_boot_mapping_base).
+//      (at address SEG_BOOT_MAPPING_BASE defined in hard_config.h file).
 //    - the "sys.elf" file contains the kernel binary code and data.
 //    - the various "application.elf" files.
@@ -110,4 +110,16 @@
 #endif
 
+#if !defined(SEG_BOOT_MAPPING_BASE) 
+# error: You must define SEG_BOOT_MAPPING_BASE in the hard_config.h file
+#endif
+
+#if !defined(SEG_BOOT_BUFFER_BASE) 
+# error: You must define SEG_BOOT_BUFFER_BASE in the hard_config.h file
+#endif
+
+#if !defined(SEG_BOOT_BUFFER_SIZE) 
+# error: You must define SEG_BOOT_BUFFER_SIZE in the hard_config.h file
+#endif
+
 #if !defined(NB_PROCS_MAX)
 # error The NB_PROCS_MAX value must be defined in the 'hard_config.h' file !
@@ -157,5 +169,5 @@
 void boot_mapping_check() 
 {
-    mapping_header_t * header = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t * header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
 
     // checking mapping availability
@@ -262,5 +274,5 @@
 mapping_pseg_t *boot_pseg_get(unsigned int seg_id) 
 {
-    mapping_header_t* header = (mapping_header_t*)(&seg_boot_mapping_base);
+    mapping_header_t* header = (mapping_header_t*)SEG_BOOT_MAPPING_BASE;
     mapping_pseg_t * pseg    = _get_pseg_base(header);
 
@@ -396,5 +408,5 @@
     unsigned int verbose = 0;   // can be used to activate trace in add_pte()
 
-    mapping_header_t * header = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t * header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_vspace_t * vspace = _get_vspace_base(header);
     mapping_vseg_t   * vseg   = _get_vseg_base(header);
@@ -523,5 +535,5 @@
 
     // computes vseg alignment constraint
-    mapping_header_t* header    = (mapping_header_t*)&seg_boot_mapping_base;
+    mapping_header_t* header    = (mapping_header_t*)SEG_BOOT_MAPPING_BASE;
     mapping_vobj_t*   vobj_base = _get_vobj_base( header );
     unsigned int      align     = vobj_base[vseg->vobj_offset].align;
@@ -627,5 +639,5 @@
 
     // computes vseg alignment constraint
-    mapping_header_t* header    = (mapping_header_t*)&seg_boot_mapping_base;
+    mapping_header_t* header    = (mapping_header_t*)SEG_BOOT_MAPPING_BASE;
     mapping_vobj_t*   vobj_base = _get_vobj_base( header );
     unsigned int      align     = vobj_base[vseg->vobj_offset].align;
@@ -689,5 +701,7 @@
         _puts(" cannot be mapped on pseg ");
         _puts( pseg->name );
-        _puts("\n");
+        _puts(" in cluster[");
+        _putd( pseg->clusterid );
+        _puts("]\n");
         _exit();
     }
@@ -710,5 +724,5 @@
     unsigned int offset;
 
-    mapping_header_t * header = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t * header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_vobj_t   * vobj   = _get_vobj_base(header);
 
@@ -808,5 +822,5 @@
 void boot_pt_init() 
 {
-    mapping_header_t * header = (mapping_header_t *) &seg_boot_mapping_base;
+    mapping_header_t * header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_vspace_t * vspace = _get_vspace_base(header);
     mapping_vseg_t   * vseg   = _get_vseg_base(header);
@@ -941,5 +955,5 @@
 void boot_vobjs_init() 
 {
-    mapping_header_t* header = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t* header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_vspace_t* vspace = _get_vspace_base(header);
     mapping_vobj_t* vobj     = _get_vobj_base(header);
@@ -1177,5 +1191,5 @@
                            unsigned int* length )
 {
-    mapping_header_t* header = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t* header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_vobj_t*   vobj   = _get_vobj_base(header);
     mapping_vseg_t*   vseg   = _get_vseg_base(header);
@@ -1212,11 +1226,11 @@
 // - In Step 1, it initialises the _schedulers[gpid] pointers array, and scan
 //              the processors to initialise the schedulers, including the
-//              idle_task context (ltid == 14).
-// - In Step 2, it scan all tasks in all vspaces to initialise the tasks contexts, 
-//              as specified in the mapping_info data structure. 
+//              idle_task context (ltid == 14) and HWI / SWI / PTI vectors. 
+// - In Step 2, it scan all tasks in all vspaces to complete the tasks contexts, 
+//              initialisation as specified in the mapping_info data structure. 
 ////////////////////////////////////////////////////////////////////////////////////
 void boot_schedulers_init() 
 {
-    mapping_header_t*  header  = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t*  header  = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_cluster_t* cluster = _get_cluster_base(header);
     mapping_vspace_t*  vspace  = _get_vspace_base(header);
@@ -1231,15 +1245,30 @@
     unsigned int vspace_id;     // vspace index in mapping_info
     unsigned int task_id;       // task index in mapping_info
-
-    // TTY, NIC, CMA, HBA, TIM and DMA channels allocators 
+    unsigned int vobj_id;       // vobj index in mapping_info
+
+    unsigned int lpid;          // local processor index (for several loops)
+
+    // TTY, NIC, CMA, HBA, user timer, and WTI channel allocators to user tasks:
     // - TTY[0] is reserved for the kernel
     // - In all clusters the first NB_PROCS_MAX timers 
     //   are reserved for the kernel (context switch)
-
-    unsigned int alloc_tty_channel = 1;             // TTY channel allocator
-    unsigned int alloc_nic_channel = 0;             // NIC channel allocator
-    unsigned int alloc_cma_channel = 0;             // CMA channel allocator
-    unsigned int alloc_hba_channel = 0;             // HBA channel allocator
-    unsigned int alloc_tim_channel[X_SIZE*Y_SIZE];  // user TIMER allocators
+    unsigned int alloc_tty_channel = 1;              // global
+    unsigned int alloc_nic_channel = 0;              // global
+    unsigned int alloc_cma_channel = 0;              // global
+    unsigned int alloc_hba_channel = 0;              // global
+    unsigned int alloc_tim_channel[X_SIZE*Y_SIZE];   // one per cluster 
+
+    // WTI allocators to processors 
+    // In all clusters, first NB_PROCS_MAX WTIs are for WAKUP
+    unsigned int alloc_wti_channel[X_SIZE*Y_SIZE];   // one per cluster
+
+    // pointers on the XCU and PIC peripherals
+    mapping_periph_t*  xcu = NULL;
+    mapping_periph_t*  pic = NULL;
+
+    // schedulers array base address in a cluster
+    unsigned int          sched_vbase;  
+    unsigned int          sched_length;  
+    static_scheduler_t*   psched;  
 
     /////////////////////////////////////////////////////////////////////////
@@ -1269,4 +1298,5 @@
 #endif
         alloc_tim_channel[cluster_id] = NB_PROCS_MAX;
+        alloc_wti_channel[cluster_id] = NB_PROCS_MAX;
 
         // checking processors number
@@ -1281,12 +1311,8 @@
         }
  
-        static_scheduler_t* psched;  // schedulers array base address in cluster
-
         // no schedulers initialisation if nprocs == 0
         if ( cluster[cluster_id].procs > 0 )
         {
-            // get scheduler array virtual base address and length from mapping
-            unsigned int        sched_vbase;   // schedulers segment virtual base address
-            unsigned int        sched_length;  // schedulers segment length
+            // get scheduler array virtual base address from mapping
             boot_get_sched_vaddr( cluster_id, &sched_vbase, &sched_length );
 
@@ -1303,6 +1329,7 @@
             psched = (static_scheduler_t*)sched_vbase;
 
-            // scan cluster peripherals to find the ICU/XCU 
-            unsigned int found = 0;
+            // scan peripherals to find the ICU/XCU and the PIC component
+
+            xcu = NULL;  
             for ( periph_id = cluster[cluster_id].periph_offset ;
                   periph_id < cluster[cluster_id].periph_offset + cluster[cluster_id].periphs;
@@ -1312,9 +1339,22 @@
                     (periph[periph_id].type == PERIPH_TYPE_ICU) )
                 {
-                    found = 1;
-                    break;
+                    xcu = &periph[periph_id];
+
+                    if ( xcu->arg < cluster[cluster_id].procs )
+                    {
+                        _puts("\n[BOOT ERROR] Not enough inputs for XCU[");
+                        _putd( x );
+                        _puts(",");
+                        _putd( y );
+                        _puts("]\n");
+                        _exit();
+                    }
+                }
+                if( periph[periph_id].type == PERIPH_TYPE_PIC )   
+                {
+                    pic = &periph[periph_id];
                 }
             } 
-            if ( found == 0 )
+            if ( xcu == NULL )
             {         
                 _puts("\n[BOOT ERROR] No ICU / XCU component in cluster[");
@@ -1326,6 +1366,6 @@
             }
 
-            // loop on schedulers for default values initialisation
-            unsigned int lpid;
+            // loop on processors for sechedulers default values
+            // initialisation, including WTI and PTI vectors
             for ( lpid = 0 ; lpid < cluster[cluster_id].procs ; lpid++ )
             {
@@ -1349,5 +1389,5 @@
                 psched[lpid].current = IDLE_TASK_INDEX;
 
-                // initialise HWI / PTI / SWI vectors (valid bit = 0)
+                // default values for HWI / PTI / SWI vectors (valid bit = 0)
                 unsigned int slot;
                 for (slot = 0; slot < 32; slot++)
@@ -1357,4 +1397,8 @@
                     psched[lpid].wti_vector[slot] = 0;
                 }
+
+                // WTI[lpid] <= ISR_WAKUP / PTI[lpid] <= ISR_TICK 
+                psched[lpid].wti_vector[lpid] = ISR_WAKUP | 0x80000000;
+                psched[lpid].pti_vector[lpid] = ISR_TICK  | 0x80000000;
 
                 // initializes the idle_task context in scheduler:
@@ -1373,16 +1417,21 @@
                 psched[lpid].context[IDLE_TASK_INDEX][CTX_VSID_ID]  = 0;
                 psched[lpid].context[IDLE_TASK_INDEX][CTX_RUN_ID]   = 1;
-            }
-
-           
-            // loop on irqs in ICU for actual HWI / PTI / WTI vectors initialisation      
-            for ( irq_id = periph[periph_id].irq_offset ;
-                  irq_id < periph[periph_id].irq_offset + periph[periph_id].irqs ;
+            }  // end for processors
+
+            // scan HWIs connected to local XCU 
+            // for round-robin allocation to processors
+            lpid = 0;
+            for ( irq_id = xcu->irq_offset ;
+                  irq_id < xcu->irq_offset + xcu->irqs ;
                   irq_id++ )
             {
-                unsigned int lpid    = irq[irq_id].dstid;
-                if ( lpid >= cluster[cluster_id].procs )
-                {
-                    _puts("\n[BOOT ERROR] Bad IRQ processor index in cluster[");
+                unsigned int type    = irq[irq_id].srctype;
+                unsigned int srcid   = irq[irq_id].srcid;
+                unsigned int isr     = irq[irq_id].isr & 0xFFFF;
+                unsigned int channel = irq[irq_id].channel << 16;
+
+                if ( (type != IRQ_TYPE_HWI) || (srcid > 31) )
+                {
+                    _puts("\n[BOOT ERROR] Bad IRQ in XCU of cluster[");
                     _putd( x );
                     _puts(",");
@@ -1391,32 +1440,137 @@
                     _exit();
                 }
-                unsigned int type    = irq[irq_id].srctype;
-                unsigned int index   = irq[irq_id].srcid;
-                unsigned int isr     = irq[irq_id].isr;
-                unsigned int channel = irq[irq_id].channel;
-
-                unsigned int entry = ((isr & 0xFFFF)          ) | 
-                                     ((channel & 0x7FFF) << 16) | 
-                                     0x80000000;                    // Valid entry
-
-                if      (type == IRQ_TYPE_HWI) psched[lpid].hwi_vector[index] = entry;
-                else if (type == IRQ_TYPE_PTI) psched[lpid].pti_vector[index] = entry;
-                else if (type == IRQ_TYPE_WTI) psched[lpid].wti_vector[index] = entry;
-
-#if BOOT_DEBUG_SCHED
-_puts("- IRQ : type = ");
-_putd( type );
-_puts(" / index = ");
-_putd( index );
-_puts(" / isr = ");
-_putd( isr );
-_puts(" / channel = ");
-_putd( channel );
-_puts("\n");
-#endif
+
+                psched[lpid].hwi_vector[srcid] = isr | channel | 0x80000000;
+                lpid = (lpid + 1) % cluster[cluster_id].procs; 
 
             } // end for irqs
         } // end if nprocs > 0
     } // end for clusters
+
+    // If there is an external PIC component, we scan HWIs connected to PIC
+    // for Round Robin allocation (as WTI) to processors.
+    // We allocate one WTI per processor, starting from proc[0,0,0], 
+    // and we increment (cluster_id, lpid) as required.
+    if ( pic != NULL )
+    {   
+        unsigned int cluster_id = 0;   // index in clusters array
+        unsigned int lpid       = 0;   // processor local index
+
+        // scan IRQS defined in PIC
+        for ( irq_id = pic->irq_offset ;
+              irq_id < pic->irq_offset + pic->irqs ;
+              irq_id++ )
+        {
+            // compute next values for (cluster_id,lpid)
+            // if no more procesor available in current cluster
+            unsigned int overflow = 0;
+            while ( (lpid >= cluster[cluster_id].procs) ||
+                    (alloc_wti_channel[cluster_id] >= xcu->arg) )
+            {
+                overflow++;
+                cluster_id = (cluster_id + 1) % (X_SIZE*Y_SIZE);
+                lpid       = 0;
+
+                // overflow detection
+                if ( overflow > (X_SIZE*Y_SIZE*NB_PROCS_MAX*32) )
+                {
+                    _puts("\n[BOOT ERROR] Not enough processors for external IRQs\n");
+                    _exit();
+                }
+            }
+
+            unsigned int type    = irq[irq_id].srctype;
+            unsigned int srcid   = irq[irq_id].srcid;
+            unsigned int isr     = irq[irq_id].isr & 0xFFFF;
+            unsigned int channel = irq[irq_id].channel << 16;
+
+            if ( (type != IRQ_TYPE_HWI) || (srcid > 31) )
+            {
+                _puts("\n[BOOT ERROR] Bad IRQ in PIC component\n");
+                _exit();
+            }
+
+            // get scheduler[cluster_id] address
+            unsigned int x          = cluster[cluster_id].x;
+            unsigned int y          = cluster[cluster_id].y;
+            unsigned int cluster_xy = (x<<Y_WIDTH) + y;
+            psched                  = _schedulers[cluster_xy * NB_PROCS_MAX];
+
+            // update WTI vector for scheduler[cluster_id][lpid]
+            unsigned int index = alloc_wti_channel[cluster_id];
+            psched[lpid].wti_vector[index] = isr | channel | 0x80000000;
+            alloc_wti_channel[cluster_id] = index + 1;
+            lpid = lpid + 1;
+
+            // update IRQ fields in mapping for PIC initialisation
+            irq[irq_id].dest_id = index;
+            irq[irq_id].dest_xy = cluster_xy;
+
+        }  // end for IRQs
+    } // end if PIC
+                
+#if BOOT_DEBUG_SCHED
+for ( cluster_id = 0 ; cluster_id < (X_SIZE*Y_SIZE) ; cluster_id++ )
+{
+    unsigned int x          = cluster[cluster_id].x;
+    unsigned int y          = cluster[cluster_id].y;
+    unsigned int cluster_xy = (x<<Y_WIDTH) + y;
+    psched                  = _schedulers[cluster_xy * NB_PROCS_MAX];
+    unsigned int slot;
+    unsigned int entry;
+    for ( lpid = 0 ; lpid < cluster[cluster_id].procs ; lpid++ )
+    {
+        _puts("\n*** IRQS for proc[");
+        _putd( x );
+        _puts(",");
+        _putd( y );
+        _puts(",[");
+        _putd( lpid );
+        _puts("]\n");
+        for ( slot = 0 ; slot < 32 ; slot++ )
+        {
+            entry = psched[lpid].hwi_vector[slot];
+            if ( entry & 0x80000000 ) 
+            {
+                _puts(" - HWI ");
+                _putd( slot );
+                _puts(" / isrtype = ");
+                _putd( entry & 0xFFFF ); 
+                _puts(" / channel = ");
+                _putd( (entry >> 16) & 0x7FFF ); 
+                _puts("\n");
+            }
+        }
+        for ( slot = 0 ; slot < 32 ; slot++ )
+        {
+            entry = psched[lpid].wti_vector[slot];
+            if ( entry & 0x80000000 ) 
+            {
+                _puts(" - WTI ");
+                _putd( slot );
+                _puts(" / isrtype = ");
+                _putd( entry & 0xFFFF ); 
+                _puts(" / channel = ");
+                _putd( (entry >> 16) & 0x7FFF ); 
+                _puts("\n");
+            }
+        }
+        for ( slot = 0 ; slot < 32 ; slot++ )
+        {
+            entry = psched[lpid].pti_vector[slot];
+            if ( entry & 0x80000000 ) 
+            {
+                _puts(" - PTI ");
+                _putd( slot );
+                _puts(" / isrtype = ");
+                _putd( entry & 0xFFFF ); 
+                _puts(" / channel = ");
+                _putd( (entry >> 16) & 0x7FFF ); 
+                _puts("\n");
+            }
+        }
+    }
+}
+#endif
 
     ///////////////////////////////////////////////////////////////////
@@ -1450,5 +1604,5 @@
             // compute gpid (global processor index) and scheduler base address
             unsigned int gpid = cluster_xy * NB_PROCS_MAX + lpid;
-            static_scheduler_t* psched = _schedulers[gpid];
+            psched            = _schedulers[gpid];
 
             // ctx_sr : value required before an eret instruction
@@ -1558,10 +1712,9 @@
             // the task entry point : the start_vector is stored by GCC in the seg_data 
             // segment and we must wait the .elf loading to get the entry point value...
-            mapping_vobj_t* pvobj = &vobj[vspace[vspace_id].vobj_offset + 
-                                     vspace[vspace_id].start_offset];
-            unsigned int ctx_epc = pvobj->vaddr + (task[task_id].startid)*4;
+            vobj_id = vspace[vspace_id].start_vobj_id;     
+            unsigned int ctx_epc = vobj[vobj_id].vaddr + (task[task_id].startid)*4;
 
             // ctx_sp :  Get the vobj containing the stack 
-            unsigned int vobj_id = task[task_id].stack_vobjid + vspace[vspace_id].vobj_offset;
+            vobj_id = task[task_id].stack_vobj_id;
             unsigned int ctx_sp = vobj[vobj_id].vaddr + vobj[vobj_id].length;
 
@@ -1683,5 +1836,5 @@
     unsigned int ok = _fat_read( IOC_BOOT_MODE,
                                  fd_id, 
-                                 (unsigned int*)( &seg_boot_mapping_base), 
+                                 (unsigned int*)SEG_BOOT_MAPPING_BASE, 
                                  nblocks,       
                                  0 );      // offset
@@ -1716,6 +1869,6 @@
 
     // get boot buffer address and size
-    char*             boot_buffer      = (char*)(&seg_boot_buffer_base);
-    unsigned int      boot_buffer_size = (unsigned int)(&seg_boot_buffer_size);
+    char*             boot_buffer      = (char*)SEG_BOOT_BUFFER_BASE;
+    unsigned int      boot_buffer_size = SEG_BOOT_BUFFER_SIZE;
 
 #if BOOT_DEBUG_ELF
@@ -1882,5 +2035,5 @@
 void boot_elf_load()
 {
-    mapping_header_t* header = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t* header = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_vspace_t* vspace = _get_vspace_base( header );
     mapping_vobj_t*   vobj   = _get_vobj_base( header );
@@ -1970,9 +2123,8 @@
 void boot_peripherals_init() 
 {
-    mapping_header_t * header   = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t * header   = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_cluster_t * cluster = _get_cluster_base(header);
     mapping_periph_t * periph   = _get_periph_base(header);
     mapping_vobj_t * vobj       = _get_vobj_base(header);
-    mapping_vspace_t * vspace   = _get_vspace_base(header);
     mapping_coproc_t * coproc   = _get_coproc_base(header);
     mapping_cp_port_t * cp_port = _get_cp_port_base(header);
@@ -2066,5 +2218,5 @@
 #if 0
                     // initialize r_xicu_base & r_xicu_size registers
-                    unsigned int base = (unsigned int)&seg_xcu_base;
+                    unsigned int base = (unsigned int)SEG_XCU_BASE;
 
 #if BOOT_DEBUG_PERI
@@ -2108,9 +2260,7 @@
                           channel_id++ )
                     {
-                        unsigned int hwi_id     = irq[channel_id].srcid;  // HWI index in PIC
-                        unsigned int wti_id     = irq[channel_id].dstid;  // WTI index in XCU
-                        unsigned int x          = irq[channel_id].dstx;   // XCU X coordinate
-                        unsigned int y          = irq[channel_id].dsty;   // XCU Y coordinate
-                        unsigned int cluster_xy = (x<<Y_WIDTH) + y;       // XCU cluster
+                        unsigned int hwi_id     = irq[channel_id].srcid;   // HWI index in PIC
+                        unsigned int wti_id     = irq[channel_id].dest_id; // WTI index in XCU
+                        unsigned int cluster_xy = irq[channel_id].dest_xy; // XCU coordinates
                         unsigned int vaddr;
 
@@ -2126,7 +2276,7 @@
 _putx( vaddr );
 _puts(" in cluster[");
-_putd( x );
+_putd( cluster_xy >> Y_WIDTH );
 _puts(",");
-_putd( y );
+_putd( cluster_xy & ((1<<Y_WIDTH)-1) );
 _puts("]\n");
 #endif
@@ -2163,7 +2313,6 @@
                   cp_port_id++ ) 
             {
-                unsigned int vspace_id = cp_port[cp_port_id].vspaceid;
-                unsigned int vobj_id   = cp_port[cp_port_id].mwmr_vobjid + 
-                                                vspace[vspace_id].vobj_offset;
+                // Get global index of associted vobj
+                unsigned int vobj_id   = cp_port[cp_port_id].mwmr_vobj_id; 
 
                 // Get MWMR channel base address 
@@ -2181,6 +2330,4 @@
 _puts(" / name = ");
 _puts(vobj[vobj_id].name);
-_puts(" / in vspace ");
-_puts(vspace[vspace_id].name);
 _puts("\n"); 
 #endif
@@ -2196,5 +2343,5 @@
 void boot_init() 
 {
-    mapping_header_t*  header     = (mapping_header_t *) & seg_boot_mapping_base;
+    mapping_header_t*  header     = (mapping_header_t *)SEG_BOOT_MAPPING_BASE;
     mapping_cluster_t* cluster    = _get_cluster_base(header);
     unsigned int       gpid       = _get_procid();
@@ -2288,6 +2435,6 @@
     }
 
-    // all processors jump to kernel_init
-    unsigned int kernel_entry = (unsigned int)&seg_kernel_init_base;
+    // all processors jump to kernel_init (address defined in giet_vsegs.ld)
+    unsigned int kernel_entry = (unsigned int)&kernel_init_vbase;
     asm volatile( "jr   %0" ::"r"(kernel_entry) );
 
