Index: soft/giet_vm/xml/xml_parser.c
===================================================================
--- soft/giet_vm/xml/xml_parser.c	(revision 232)
+++ soft/giet_vm/xml/xml_parser.c	(revision 238)
@@ -49,16 +49,16 @@
 ///////////////////////////////////////////////////////////////////////////////////
 
-mapping_header_t * header;
-mapping_cluster_t * cluster[MAX_CLUSTERS];  // cluster array
-mapping_pseg_t * pseg[MAX_PSEGS];           // pseg array
-mapping_vspace_t * vspace[MAX_VSPACES];     // vspace array
-mapping_vseg_t * vseg[MAX_VSEGS];           // vseg array
-mapping_vobj_t * vobj[MAX_VOBJS];           // vobj array
-mapping_task_t * task[MAX_TASKS];           // task array
-mapping_proc_t * proc[MAX_PROCS];           // proc array
-mapping_irq_t * irq[MAX_IRQS];              // irq array
-mapping_coproc_t * coproc[MAX_COPROCS];     // coproc array
-mapping_cp_port_t * cp_port[MAX_CP_PORTS];  // coproc port array
-mapping_periph_t * periph[MAX_PERIPHS];     // peripheral array
+mapping_header_t *   header;
+mapping_cluster_t *  cluster[MAX_CLUSTERS];  // cluster array
+mapping_pseg_t *     pseg[MAX_PSEGS];        // pseg array
+mapping_vspace_t *   vspace[MAX_VSPACES];    // vspace array
+mapping_vseg_t *     vseg[MAX_VSEGS];        // vseg array
+mapping_vobj_t *     vobj[MAX_VOBJS];        // vobj array
+mapping_task_t *     task[MAX_TASKS];        // task array
+mapping_proc_t *     proc[MAX_PROCS];        // proc array
+mapping_irq_t *      irq[MAX_IRQS];          // irq array
+mapping_coproc_t *   coproc[MAX_COPROCS];    // coproc array
+mapping_cp_port_t *  cp_port[MAX_CP_PORTS];  // coproc port array
+mapping_periph_t *   periph[MAX_PERIPHS];    // peripheral array
 
 // Index for the various arrays
@@ -95,55 +95,39 @@
 
 
-/////////////////////////
-// found peripheral
-/////////////////////////
+//////////////////////////////
+// for replicated peripheral
+//////////////////////////////
 char found_timer = 0;
 char found_icu = 0;
-char found_xicu = 0;
 char found_dma = 0;
 
 
-//////////////////////////////////
-//needed to generate map_config.ld
-//////////////////////////////////
-unsigned int cluster_y            = 0;
-unsigned int cluster_x            = 0; 
-unsigned int nb_proc_max          = 0; // max number of processors per cluste 
-
-unsigned int nb_tasks_max         = 0; // max number of tasks (for all vspaces)
-unsigned int nb_timer_channel_max = 0; // max number of user timer
-unsigned int nb_dma_channel_max   = 0;
-unsigned int nb_tty_channel       = 0;
-unsigned int nb_ioc_channel       = 0;
-unsigned int nb_nic_channel       = 0;
-unsigned int io_mmu_active        = 0;
-unsigned int use_xicu             = 0xFFFFFFFF;
-
-
-//////////////////////////////////
-//needed to generate giet_vseg.ld
-//////////////////////////////////
-
-//kernel and boot code
-unsigned int kernel_code_base    = 0x80000000; /* kernel code */
-unsigned int kernel_data_base    = 0x80010000; /* system cacheable data */
-unsigned int kernel_uncdata_base = 0x80080000; /* system uncacheable data */
-unsigned int kernel_init_base    = 0x80090000; /* system init entry */ 
-
-unsigned int boot_code_base      = 0xBFC00000; /* boot code */
-unsigned int boot_stack_base     = 0xBFC08000; /* boot temporary stack */ 
-unsigned int boot_mapping_base   = 0xBFC0C000; /* mapping_info blob */
-
-//periphs
-unsigned int tim_base_offset = 0xFFFFFFFF;
-unsigned int tty_base_offset = 0xFFFFFFFF;
-unsigned int dma_base_offset = 0xFFFFFFFF;
-unsigned int ioc_base_offset = 0xFFFFFFFF;
-unsigned int nic_base_offset = 0xFFFFFFFF;
-unsigned int fbf_base_offset = 0xFFFFFFFF;
-unsigned int icu_base_offset = 0xFFFFFFFF;
-unsigned int gcd_base_offset = 0xFFFFFFFF;
-unsigned int iob_base_offset = 0xFFFFFFFF;
-
+////////////////////////////////////////////////////////////////////
+// These variables are used to generate the hard_config.h file
+////////////////////////////////////////////////////////////////////
+
+unsigned int cluster_y        = 0; // number of clusters in a column
+unsigned int cluster_x        = 0; // number of clusters in a row
+unsigned int nb_proc_max      = 0; // max number of processors per cluster
+unsigned int nb_tasks_max     = 0; // max number of tasks (for all vspaces)
+
+unsigned int tim_channels     = 0; // max number of user timers per cluster
+unsigned int dma_channels     = 0; // max number of DMA channels per cluster
+
+unsigned int tty_channels     = 0; // total number of terminals in first TTY 
+unsigned int ioc_channels     = 0; // total number of channels in first IOC 
+unsigned int nic_channels     = 0; // total number of channels in first NIC 
+unsigned int cma_channels     = 0; // total number of channels in first CMA
+
+unsigned int io_mmu_active    = 0; // using IOB component
+unsigned int use_xicu         = 0; // using XICU (not ICU)
+
+
+////////////////////////////////////////////////////////////////
+// These variables are used to generate the giet_vseg.ld file
+////////////////////////////////////////////////////////////////
+
+unsigned int periph_vbase_array[PERIPH_TYPE_MAX_VALUE] 
+         = { [0 ... (PERIPH_TYPE_MAX_VALUE - 1)] = 0xFFFFFFFF };
 
 //////////////////////////////////////////////////////////////////////
@@ -153,5 +137,6 @@
 // once all the vspace have been parsed.
 /////////////////////////////////////////////////////////////////////
-typedef struct vobj_ref_s {
+typedef struct vobj_ref_s 
+{
     char vspace_name[32];
     char vobj_name[32];
@@ -162,25 +147,34 @@
 
 //////////////////////////////////////////////////
-unsigned int getIntValue(xmlTextReaderPtr reader, const char * attributeName, unsigned int * ok) {
+unsigned int getIntValue( xmlTextReaderPtr reader, 
+                          const char * attributeName, 
+                          unsigned int * ok) 
+{
     unsigned int value = 0;
     unsigned int i;
     char c;
 
-    char * string = (char *) xmlTextReaderGetAttribute(reader, (const xmlChar *) attributeName);
-
-    if (string == NULL) {
+    char * string = (char *) xmlTextReaderGetAttribute(reader, 
+                                (const xmlChar *) attributeName);
+
+    if (string == NULL) 
+    {
         // missing argument
         *ok = 0;
         return 0;
     }
-    else {
-        if ((string[0] == '0') && ((string[1] == 'x') || (string[1] == 'X'))) {
+    else 
+    {
+        if ((string[0] == '0') && ((string[1] == 'x') || (string[1] == 'X'))) 
+        {
             // Hexa
-            for (i = 2 ; (string[i] != 0) && (i < 10) ; i++) {
+            for (i = 2 ; (string[i] != 0) && (i < 10) ; i++) 
+            {
                 c = string[i];
                 if      ((c >= '0') && (c <= '9')) { value = (value << 4) + string[i] - 48; }
                 else if ((c >= 'a') && (c <= 'f')) { value = (value << 4) + string[i] - 87; }
                 else if ((c >= 'A') && (c <= 'F')) { value = (value << 4) + string[i] - 55; }
-                else {
+                else 
+                {
                     *ok = 0;
                     return 0;
@@ -188,10 +182,13 @@
             }
         }
-        else {
+        else 
+        {
             // Decimal
-            for (i = 0; (string[i] != 0) && (i < 9); i++) {
+            for (i = 0; (string[i] != 0) && (i < 9); i++) 
+            {
                 c = string[i];
                 if ((c >= '0') && (c <= '9')) value = (value * 10) + string[i] - 48;
-                else {
+                else 
+                {
                     *ok = 0;
                     return 0;
@@ -204,18 +201,71 @@
 } // end getIntValue()
 
-
-///////////////////////////////////////////////
-char * getStringValue(xmlTextReaderPtr reader, const char * attributeName, unsigned int * ok) {
-    char * string = (char *) xmlTextReaderGetAttribute(reader, (const xmlChar *) attributeName);
-
-
-    if (string == NULL) {
+////////////////////////////////////////////////
+paddr_t getPaddrValue( xmlTextReaderPtr reader, 
+                       const char * attributeName, 
+                       unsigned int * ok) 
+{
+    paddr_t value = 0;
+    unsigned int i;
+    char c;
+
+    char * string = (char *) xmlTextReaderGetAttribute(reader, 
+                                (const xmlChar *) attributeName);
+
+    if (string == NULL) 
+    {
+        // missing argument
+        *ok = 0;
+        return 0;
+    }
+    else 
+    {
+        if ((string[0] == '0') && ((string[1] == 'x') || (string[1] == 'X'))) 
+        {
+            // Hexa
+            for (i = 2 ; (string[i] != 0) && (i < 18) ; i++) 
+            {
+                c = string[i];
+                if      ((c >= '0') && (c <= '9')) { value = (value << 4) + string[i] - 48; }
+                else if ((c >= 'a') && (c <= 'f')) { value = (value << 4) + string[i] - 87; }
+                else if ((c >= 'A') && (c <= 'F')) { value = (value << 4) + string[i] - 55; }
+                else 
+                {
+                    *ok = 0;
+                    return 0;
+                }
+            }
+        }
+        else 
+        {
+            // Decimal not supported for paddr_t
+            *ok = 0;
+            return 0;
+        }
+        *ok = 1;
+        return value; 
+    }
+} // end getPaddrValue()
+
+////////////////////////////////////////////////
+char * getStringValue( xmlTextReaderPtr reader, 
+                       const char * attributeName, 
+                       unsigned int * ok ) 
+{
+    char * string = (char *) xmlTextReaderGetAttribute(reader, 
+                               (const xmlChar *) attributeName);
+
+
+    if (string == NULL) 
+    {
         // missing argument
         *ok = 0;
         return NULL;
     }
-    else {
+    else 
+    {
         //we read only string smaller than 32 byte
-        if (strlen(string) > 32) {
+        if (strlen(string) > 32) 
+        {
             printf("[XML ERROR] all strings must be less than 32 bytes\n");
             exit(1);
@@ -227,13 +277,34 @@
 } // end getStringValue()
 
-
-///////////////////////////////////////
-int getPsegId(unsigned int cluster_id, char * pseg_name) {
+///////////////////////////////////////////////////////
+void set_periph_vbase_array( unsigned int vseg_index )
+{
+    unsigned int vbase  = vseg[vseg_index]->vbase;  // peripheral vbase address
+    unsigned int psegid = vseg[vseg_index]->psegid; // pseg global index
+    unsigned int type;                              // peripheral type
+    unsigned int periph_id; 
+
+    for ( periph_id = 0 ; periph_id < header->periphs ; periph_id++)
+    {
+        if( periph[periph_id]->psegid == psegid )
+        {
+            type = periph[periph_id]->type;
+            if ( periph_vbase_array[type] == 0xFFFFFFFF ) 
+                 periph_vbase_array[type] = vbase;    
+        }
+    }
+}  // end set_periph_vbase_array()
+
+////////////////////////////////////////////////////////
+int getPsegId(unsigned int cluster_id, char * pseg_name) 
+{
     unsigned int pseg_id;
     unsigned int pseg_min = cluster[cluster_id]->pseg_offset;
     unsigned int pseg_max = pseg_min + cluster[cluster_id]->psegs;
 
-    for (pseg_id = pseg_min; pseg_id < pseg_max; pseg_id++) {
-        if (strcmp(pseg[pseg_id]->name, pseg_name) == 0) {
+    for (pseg_id = pseg_min; pseg_id < pseg_max; pseg_id++) 
+    {
+        if (strcmp(pseg[pseg_id]->name, pseg_name) == 0) 
+        {
             return pseg_id;
         }
@@ -242,11 +313,13 @@
 }
 
-
-////////////////////////////////////////////
-int getVspaceId(char * vspace_name) {
+///////////////////////////////////
+int getVspaceId(char * vspace_name) 
+{
     unsigned int vspace_id;
 
-    for (vspace_id = 0; vspace_id < vspace_index; vspace_id++) {
-        if (!strcmp(vspace[vspace_id]->name, vspace_name)) {
+    for (vspace_id = 0; vspace_id < vspace_index; vspace_id++) 
+    {
+        if (strcmp(vspace[vspace_id]->name, vspace_name) == 0) 
+        {
             return vspace_id;
         }
@@ -255,7 +328,7 @@
 }
 
-
-////////////////////////////////////////////
-int getVobjLocId(unsigned int vspace_id, char * vobj_name, unsigned int vspace_max) {
+///////////////////////////////////////////////////////////////////////////////////
+int getVobjLocId(unsigned int vspace_id, char * vobj_name, unsigned int vspace_max) 
+{
     unsigned int vobj_id;
     unsigned int vobj_min = vspace[vspace_id]->vobj_offset;
@@ -272,19 +345,19 @@
 
 /////////////////////////////////////////
-void taskNode(xmlTextReaderPtr reader) {
+void taskNode(xmlTextReaderPtr reader) 
+{
     unsigned int ok;
     unsigned int value;
     char * str;
 
-    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) {
-        return;
-    }
-
-    if (task_index >= MAX_TASKS) {
+    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) { return; }
+
+    if (task_index >= MAX_TASKS) 
+    {
         printf("[XML ERROR] The number of tasks is larger than %d\n", MAX_TASKS);
     }
 
 #if XML_PARSER_DEBUG
-    printf("   task %d\n", task_loc_index);
+printf("   task %d\n", task_loc_index);
 #endif
 
@@ -293,11 +366,13 @@
     ////////// get name attribute
     str = getStringValue(reader, "name", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      name = %s\n", str);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      name = %s\n", str);
 #endif
         strncpy( task[task_index]->name, str, 31 );
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <name> attribute for task (%d,%d)\n", 
                 vspace_index, task_loc_index);
@@ -307,9 +382,11 @@
     ///////// get clusterid attribute
     value = getIntValue(reader, "clusterid", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      clusterid = %x\n", value);
-#endif
-        if (value >= header->clusters) {
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      clusterid = %x\n", value);
+#endif
+        if (value >= header->clusters) 
+        {
             printf("[XML ERROR] <clusterid> too large for task (%d,%d)\n",
                     vspace_index, task_loc_index);
@@ -318,5 +395,6 @@
         task[task_index]->clusterid = value;
     }  
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <clusterid> attribute for task (%d,%d)\n",
                 vspace_index, task_loc_index);
@@ -326,9 +404,11 @@
     ////////// get proclocid attribute
     value = getIntValue(reader, "proclocid", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      proclocid = %x\n", value);
-#endif
-        if (value >= cluster[task[task_index]->clusterid]->procs) {
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      proclocid = %x\n", value);
+#endif
+        if (value >= cluster[task[task_index]->clusterid]->procs) 
+        {
             printf("[XML ERROR] <proclocid> too large for task (%d,%d)\n",
                     vspace_index, task_loc_index);
@@ -337,5 +417,6 @@
         task[task_index]->proclocid = value;
     }  
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <locprocid> attribute for task (%d,%d)\n", 
                 vspace_index, task_loc_index);
@@ -345,14 +426,17 @@
     ////////// get stackname attribute
     str = getStringValue(reader, "stackname" , &ok);
-    if (ok) {
+    if (ok) 
+    {
         int index = getVobjLocId(vspace_index, str , vobj_loc_index);
-        if (index >= 0) {
-#if XML_PARSER_DEBUG
-            printf("      stackname = %s\n", str);
-            printf("      stackid   = %d\n", index);
+        if (index >= 0) 
+        {
+#if XML_PARSER_DEBUG
+printf("      stackname = %s\n", str);
+printf("      stackid   = %d\n", index);
 #endif
             task[task_index]->stack_vobjid = index;
         }
-        else {
+        else 
+        {
             printf("[XML ERROR] illegal or missing <stackname> for task (%d,%d)\n", 
                     vspace_index, task_loc_index);
@@ -360,5 +444,6 @@
         }
     }  
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <stackname> for task (%d,%d)\n", 
                 vspace_index, task_loc_index);
@@ -368,19 +453,24 @@
     ////////// get heap attribute
     str = getStringValue(reader, "heapname", &ok);
-    if (ok) {
+    if (ok) 
+    {
         int index = getVobjLocId(vspace_index, str, vobj_loc_index);
-        if (index >= 0) {
-#if XML_PARSER_DEBUG
-            printf("      heapname = %s\n", str);
-            printf("      heapid   = %d\n", index);
+        if (index >= 0) 
+        {
+#if XML_PARSER_DEBUG
+printf("      heapname = %s\n", str);
+printf("      heapid   = %d\n", index);
 #endif
             task[task_index]->heap_vobjid = index;
         }
-        else {
-            printf("[XML ERROR] illegal or missing <heapname> for task (%d,%d)\n", vspace_index, task_loc_index);
+        else 
+        {
+            printf("[XML ERROR] illegal or missing <heapname> for task (%d,%d)\n", 
+                   vspace_index, task_loc_index);
             exit(1);
         }
     }  
-    else {
+    else 
+    {
         task[task_index]->heap_vobjid = -1;
     }
@@ -389,11 +479,13 @@
     ////////// get startid  attribute
     value = getIntValue(reader, "startid", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      startid = %x\n", value);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      startid = %x\n", value);
 #endif
         task[task_index]->startid = value;
     }  
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <startid> attribute for task (%d,%d)\n", 
                 vspace_index, task_loc_index);
@@ -403,49 +495,43 @@
     /////////// get usetty  attribute (optionnal : 0 if missing)
     value = getIntValue(reader, "usetty", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      usetty = %x\n", value);
-#endif
-        task[task_index]->use_tty = value;
-    }  
-    else {
-        task[task_index]->use_tty = 0;
-    }
+#if XML_PARSER_DEBUG
+printf("      usetty = %x\n", value);
+#endif
+    task[task_index]->use_tty = (ok)? value : 0;
 
     /////////// get usenic  attribute (optionnal : 0 if missing)
     value = getIntValue(reader, "usenic", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      usenic = %x\n", value);
-#endif
-        task[task_index]->use_nic = value;
-    }  
-    else {
-        task[task_index]->use_nic = 0;
-    }
-
-    /////////// get usetimer attribute (optionnal : 0 if missing)
-    value = getIntValue(reader, "usetimer", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      usetimer = %x\n", value);
-#endif
-        task[task_index]->use_timer = value;
-    }  
-    else {
-        task[task_index]->use_timer = 0;
-    }
-
-    /////////// get usefbdma  attribute (optionnal : 0 if missing)
-    value = getIntValue(reader, "usefbdma", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      usefbdma = %x\n", value);
-#endif
-        task[task_index]->use_fbdma = value;
-    }
-    else {
-        task[task_index]->use_fbdma = 0;
-    }
+#if XML_PARSER_DEBUG
+printf("      usenic = %x\n", value);
+#endif
+    task[task_index]->use_nic = (ok)? value : 0;
+
+    /////////// get usetim attribute (optionnal : 0 if missing)
+    value = getIntValue(reader, "usetim", &ok);
+#if XML_PARSER_DEBUG
+printf("      usetim = %x\n", value);
+#endif
+    task[task_index]->use_tim = (ok)? value : 0;
+
+    /////////// get usedma  attribute (optionnal : 0 if missing)
+    value = getIntValue(reader, "usedma", &ok);
+#if XML_PARSER_DEBUG
+printf("      usedma = %x\n", value);
+#endif
+    task[task_index]->use_dma = (ok)? value : 0;
+
+    /////////// get useioc  attribute (optionnal : 0 if missing)
+    value = getIntValue(reader, "useioc", &ok);
+#if XML_PARSER_DEBUG
+printf("      useioc = %x\n", value);
+#endif
+    task[task_index]->use_ioc = (ok)? value : 0;
+
+    /////////// get usecma  attribute (optionnal : 0 if missing)
+    value = getIntValue(reader, "usecma", &ok);
+#if XML_PARSER_DEBUG
+printf("      usecma = %x\n", value);
+#endif
+    task[task_index]->use_cma = (ok)? value : 0;
 
     task_index++;
@@ -454,21 +540,21 @@
 
 
-//////////////////////////////////////////
-void vobjNode(xmlTextReaderPtr reader) {
+//////////////////////////////////////
+void vobjNode(xmlTextReaderPtr reader) 
+{
     unsigned int ok;
     unsigned int value;
     char * str;
 
-    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) {
-        return;
-    }
-
-    if (vobj_index >= MAX_VOBJS) {
-        printf("[XML ERROR] The number of vobjs is larger than %d\n", MAX_VSEGS);
-        exit(1);
-    }
-
-#if XML_PARSER_DEBUG
-    printf("      vobj %d\n", vobj_loc_index);
+    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) { return; }
+
+    if (vobj_index >= MAX_VOBJS) 
+    {
+        printf("[XML ERROR] The number of vobjs is larger than %d\n", MAX_VOBJS);
+        exit(1);
+    }
+
+#if XML_PARSER_DEBUG
+printf("      vobj %d\n", vobj_loc_index);
 #endif
 
@@ -477,11 +563,13 @@
     ///////// get name attribute
     str = getStringValue(reader, "name", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("        name = %s\n", str);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("        name = %s\n", str);
 #endif
         strncpy(vobj[vobj_index]->name, str, 31);
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <name> attribute for vobj (%d,%d)\n", 
                 vseg_index, vobj_loc_index);
@@ -492,26 +580,32 @@
     str = getStringValue(reader, "type", &ok);
 #if XML_PARSER_DEBUG
-    printf("        type = %s\n", str);
-#endif
-    if (ok && (strcmp(str, "ELF") == 0)) {
+printf("        type = %s\n", str);
+#endif
+    if (ok && (strcmp(str, "ELF") == 0)) 
+    {
         vobj[vobj_index]->type = VOBJ_TYPE_ELF;
 
-        //check that this vobj is the first in vseg
-        if (vobj_count != 0) {
-            printf("[XML ERROR] an ELF vobj must be alone in a vseg (%d,%d)\n", 
-                    vspace_index, vobj_loc_index);
-            exit(1);
-        }
-    }
-    else if (ok && (strcmp(str, "BLOB")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_BLOB; }
-    else if (ok && (strcmp(str, "PTAB")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_PTAB; }
-    else if (ok && (strcmp(str, "PERI")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_PERI; }
-    else if (ok && (strcmp(str, "MWMR")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_MWMR; }
-    else if (ok && (strcmp(str, "LOCK")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_LOCK; }
-    else if (ok && (strcmp(str, "BUFFER")   == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_BUFFER; }
-    else if (ok && (strcmp(str, "BARRIER")  == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_BARRIER; }
-    else if (ok && (strcmp(str, "CONST")    == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_CONST; }
+        assert( (vobj_count == 0) && "[XML ERROR] an ELF vobj must be alone in a vseg");
+    }
+    else if (ok && (strcmp(str, "PERI")     == 0)) 
+    { 
+        vobj[vobj_index]->type = VOBJ_TYPE_PERI;     
+
+        assert( (vobj_count == 0) && "[XML ERROR] a PERI vobj must be alone in a vseg");
+
+        // fill the peripheral base address array 
+        set_periph_vbase_array( vseg_index );
+    }
+    else if (ok && (strcmp(str, "BLOB")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_BLOB;     }
+    else if (ok && (strcmp(str, "PTAB")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_PTAB;     }
+    else if (ok && (strcmp(str, "MWMR")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_MWMR;     }
+    else if (ok && (strcmp(str, "LOCK")     == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_LOCK;     }
+    else if (ok && (strcmp(str, "BUFFER")   == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_BUFFER;   }
+    else if (ok && (strcmp(str, "BARRIER")  == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_BARRIER;  }
+    else if (ok && (strcmp(str, "CONST")    == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_CONST;    }
     else if (ok && (strcmp(str, "MEMSPACE") == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_MEMSPACE; }
-    else {
+    else if (ok && (strcmp(str, "SCHED")    == 0)) { vobj[vobj_index]->type = VOBJ_TYPE_SCHED;    }
+    else 
+    {
         printf("[XML ERROR] illegal or missing <type> attribute for vobj (%d,%d)\n", 
                 vspace_index, vobj_loc_index);
@@ -523,5 +617,5 @@
     if (ok) {
 #if XML_PARSER_DEBUG
-        printf("        length = %d\n", value);
+printf("        length = %d\n", value);
 #endif
         vobj[vobj_index]->length = value;
@@ -537,5 +631,5 @@
     if (ok) {
 #if XML_PARSER_DEBUG
-        printf("        align = %d\n", value);
+printf("        align = %d\n", value);
 #endif
         vobj[vobj_index]->align = value;
@@ -549,5 +643,5 @@
     if (ok) {
 #if XML_PARSER_DEBUG
-        printf("        binpath = %s\n", str);
+printf("        binpath = %s\n", str);
 #endif
         strncpy(vobj[vobj_index]->binpath, str, 63);
@@ -559,16 +653,19 @@
     ////////// get init attribute (mandatory for mwmr and barrier)
     value = getIntValue(reader, "init", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("        init  = %d\n", value);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("        init  = %d\n", value);
 #endif
         vobj[vobj_index]->init = value;
     }  
-    else {
+    else 
+    {
         if ((vobj[vobj_index]->type == VOBJ_TYPE_MWMR) || 
-                (vobj[vobj_index]->type == VOBJ_TYPE_BARRIER) ||
-                (vobj[vobj_index]->type == VOBJ_TYPE_CONST)) {
+            (vobj[vobj_index]->type == VOBJ_TYPE_BARRIER) ||
+            (vobj[vobj_index]->type == VOBJ_TYPE_CONST)) 
+        {
             printf("[XML ERROR] illegal or missing <value> attribute for vobj (%d,%d). \
-                    All MWMR or BARRIER vobj must have a init value \n", 
+                    All MWMR or BARRIER or CONST vobj must have a init value \n", 
                     vspace_index, vobj_loc_index);
             exit(1);
@@ -583,6 +680,7 @@
 
 
-//////////////////////////////////////////
-void vsegNode(xmlTextReaderPtr reader) {
+//////////////////////////////////////
+void vsegNode(xmlTextReaderPtr reader) 
+{
     unsigned int ok;
     unsigned int value;
@@ -591,9 +689,8 @@
     vobj_count = 0;
 
-    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) {
-        return;
-    }
-
-    if (vseg_index >= MAX_VSEGS) {
+    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) { return; }
+
+    if (vseg_index >= MAX_VSEGS) 
+    {
         printf("[XML ERROR] The number of vsegs is larger than %d\n", MAX_VSEGS);
         exit(1);
@@ -601,5 +698,5 @@
 
 #if XML_PARSER_DEBUG
-    printf("    vseg %d\n", vseg_loc_index);
+printf("    vseg %d\n", vseg_loc_index);
 #endif
 
@@ -608,17 +705,20 @@
     ////////// set vobj_offset attributes
     vseg[vseg_index]->vobj_offset = vobj_index;
-#if XML_PARSER_DEBUG
-    printf("      vobj_offset = %d\n", vobj_index);
+
+#if XML_PARSER_DEBUG
+printf("      vobj_offset = %d\n", vobj_index);
 #endif
 
     ///////// get name attribute
     str = getStringValue(reader, "name", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      name = %s\n", str);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      name = %s\n", str);
 #endif
         strncpy( vseg[vseg_index]->name, str, 31);
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <name> attribute for vseg (%d,%d)\n", 
                 vspace_index, vseg_loc_index);
@@ -628,11 +728,13 @@
     ////////// get ident attribute (optional : 0 if missing)
     value = getIntValue(reader, "ident", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      ident = %d\n", value);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      ident = %d\n", value);
 #endif
         vseg[vseg_index]->ident = value;
     }  
-    else {
+    else 
+    {
         vseg[vseg_index]->ident = 0;
     }
@@ -640,11 +742,13 @@
     /////////// get vbase attribute
     value = getIntValue(reader, "vbase", &ok);
-    if (ok) {
-#if XML_PARSER_DEBUG
-        printf("      vbase = 0x%x\n", value);
+    if (ok) 
+    {
+#if XML_PARSER_DEBUG
+printf("      vbase = 0x%x\n", value);
 #endif
         vseg[vseg_index]->vbase = value;
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] illegal or missing <vbase> attribute for vseg (%d,%d)\n", 
                 vspace_index, vseg_loc_index);
@@ -654,5 +758,6 @@
     ////////// get clusterid and psegname attributes
     value = getIntValue(reader, "clusterid", &ok);
-    if (ok == 0) {
+    if (ok == 0) 
+    {
         printf("[XML ERROR] illegal or missing <clusterid> for vseg %d\n", 
                 vseg_loc_index);
@@ -660,5 +765,6 @@
     }
     str = getStringValue(reader, "psegname", &ok);
-    if (ok == 0) {
+    if (ok == 0) 
+    {
         printf("[XML ERROR] illegal or missing <psegname> for vseg %d\n", 
                 vseg_loc_index);
@@ -668,13 +774,15 @@
     /////////// set psegid field
     int index = getPsegId(value, str);
-    if (index >= 0) {
-#if XML_PARSER_DEBUG
-        printf("      clusterid = %d\n", value);
-        printf("      psegname  = %s\n", str);
-        printf("      psegid    = %d\n", index);
+    if (index >= 0) 
+    {
+#if XML_PARSER_DEBUG
+printf("      clusterid = %d\n", value);
+printf("      psegname  = %s\n", str);
+printf("      psegid    = %d\n", index);
 #endif
         vseg[vseg_index]->psegid = index;
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] pseg not found for vseg %d / clusterid = %d / psegname = %s\n", 
                 vseg_loc_index, value, str );
@@ -685,5 +793,5 @@
     str = getStringValue(reader, "mode", &ok);
 #if XML_PARSER_DEBUG
-    printf("      mode = %s\n", str);
+printf("      mode = %s\n", str);
 #endif
     if      (ok && (strcmp(str, "CXWU") == 0)) { vseg[vseg_index]->mode = 0xF; }
@@ -714,10 +822,9 @@
         const char * tag = (const char *) xmlTextReaderConstName(reader);
 
-        if (strcmp(tag, "vobj")     == 0 ) {
-            vobjNode(reader);
-        }
+        if      (strcmp(tag, "vobj")     == 0 ) { vobjNode(reader); }
         else if (strcmp(tag, "#text"  )  == 0 ) { }
         else if (strcmp(tag, "#comment") == 0 ) { }
-        else if (strcmp(tag, "vseg")     == 0 ) {
+        else if (strcmp(tag, "vseg")     == 0 ) 
+        {
             vseg[vseg_index]->vobjs = vobj_count;
             vseg_index++;
@@ -756,5 +863,5 @@
 
 #if XML_PARSER_DEBUG
-    printf("\n  vspace %d\n", vspace_index);
+printf("\n  vspace %d\n", vspace_index);
 #endif
 
@@ -765,5 +872,5 @@
     if (ok) {
 #if XML_PARSER_DEBUG
-        printf("  name = %s\n", str);
+printf("  name = %s\n", str);
 #endif
         strncpy(vspace[vspace_index]->name, str, 31);
@@ -936,15 +1043,15 @@
 
 
-///////////////////////////////////////////
-void periphNode(xmlTextReaderPtr reader) {
+////////////////////////////////////////
+void periphNode(xmlTextReaderPtr reader) 
+{
     char * str;
     unsigned int value;
     unsigned int ok;
 
-    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) {
-        return;
-    }
-
-    if (periph_index >= MAX_PERIPHS) {
+    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) { return; }
+
+    if (periph_index >= MAX_PERIPHS) 
+    {
         printf("[XML ERROR] The number of periphs is larger than %d\n", MAX_PERIPHS);
     }
@@ -955,9 +1062,9 @@
 
     periph[periph_index] = (mapping_periph_t *) malloc(sizeof(mapping_periph_t));
-
 
     ///////// get channels attribute (optionnal : 1 if missing)
     value = getIntValue(reader, "channels", &ok);
-    if (ok) {
+    if (ok) 
+    {
 #if XML_PARSER_DEBUG
         printf("      channels = %d\n", value);
@@ -965,5 +1072,6 @@
         periph[periph_index]->channels = value;
     }
-    else {
+    else 
+    {
         periph[periph_index]->channels = 1;
     }
@@ -971,5 +1079,6 @@
     /////////// get psegname attribute 
     str = getStringValue(reader, "psegname", &ok);
-    if (ok == 0) {
+    if (ok == 0) 
+    {
         printf("[XML ERROR] illegal or missing <psegname> for coproc %d in cluster %d\n", 
                 coproc_index, cluster_index);
@@ -979,5 +1088,6 @@
     /////////// set psegid attribute
     int index = getPsegId(cluster_index, str);
-    if (index >= 0) {
+    if (index >= 0) 
+    {
 #if XML_PARSER_DEBUG
         printf("      clusterid = %d\n", cluster_index);
@@ -989,5 +1099,6 @@
                 "peripheral psegname attribute must refer to a pseg of type PERI" );
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] pseg not found for periph %d / clusterid = %d / psegname = %s\n", 
                 periph_loc_index, cluster_index, str );
@@ -995,8 +1106,8 @@
     }  
 
-
     /////////// get type attribute 
     str = getStringValue(reader, "type", &ok);
-    if (ok) {
+    if (ok) 
+    {
 #if XML_PARSER_DEBUG
         printf("      type     = %s\n", str);
@@ -1004,119 +1115,147 @@
         unsigned int error = 0;
 
-        // The TTY, IOC, NIC, FBF and IOB peripherals cannot be replicated
-        // one per architecture
-        if (strcmp(str, "IOC") == 0) {
+        // The TTY, IOC, NIC, FBF, CMA and IOB peripherals are not replicated in all clusters
+        // but can be replicated in two different clusters for fault tolerance
+        // In case of replication, the number of channels must be the same
+        if (strcmp(str, "IOC") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_IOC;
-            if (header->ioc_clusterid == 0xFFFFFFFF) {
-                header->ioc_clusterid = cluster_index;
-            }
-            else {
+            if (header->ioc_cluster == 0xFFFFFFFF)
+            {
+                header->ioc_cluster  = cluster_index; 
+                ioc_channels = periph[periph_index]->channels;
+            }
+            else if (header->ioc_cluster_bis == 0xFFFFFFFF) 
+            {
+                header->ioc_cluster_bis = cluster_index;
+            }
+            else
+            {
                 error = 1;
             }
-
-            ioc_base_offset = pseg[periph[periph_index]->psegid]->base;
-            nb_ioc_channel = periph[periph_index]->channels;
         } 
-        else if (strcmp(str, "TTY") == 0) {
+        else if (strcmp(str, "TTY") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_TTY;
-            if (header->tty_clusterid == 0xFFFFFFFF) {
-                header->tty_clusterid = cluster_index;
-            }
-            else  {
+            if (header->tty_cluster == 0xFFFFFFFF) 
+            {
+                header->tty_cluster = cluster_index;
+                tty_channels = periph[periph_index]->channels;
+            }
+            else if (header->tty_cluster_bis == 0xFFFFFFFF) 
+            {
+                header->tty_cluster_bis = cluster_index;
+            }
+            else  
+            {
                 error = 1;
             }
-
-            tty_base_offset = pseg[periph[periph_index]->psegid]->base;
-            nb_tty_channel = periph[periph_index]->channels;
-        }
-        else if (strcmp(str, "FBF") == 0) {
+        }
+        else if (strcmp(str, "FBF") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_FBF;
-            if (header->fbf_clusterid == 0xFFFFFFFF) {
-                header->fbf_clusterid = cluster_index;
-            }
-            else {
+            if (header->fbf_cluster == 0xFFFFFFFF)  
+            {
+                header->fbf_cluster = cluster_index; 
+            }
+            else if (header->fbf_cluster_bis == 0xFFFFFFFF) 
+            {
+                header->fbf_cluster_bis = cluster_index; 
+            }
+            else  
+            {
                 error = 1;
             }
-            fbf_base_offset = pseg[periph[periph_index]->psegid]->base;
-        }
-        else if (strcmp(str, "NIC") == 0) {
+        }
+        else if (strcmp(str, "NIC") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_NIC;
-            if (header->nic_clusterid == 0xFFFFFFFF) {
-                header->nic_clusterid = cluster_index;
-            }
-            else {
+            if (header->nic_cluster == 0xFFFFFFFF)  
+            {
+                header->nic_cluster = cluster_index;
+                nic_channels = periph[periph_index]->channels;
+            }
+            else if (header->nic_cluster_bis == 0xFFFFFFFF) 
+            {
+                header->nic_cluster_bis = cluster_index;
+            }
+            else  
+            {
                 error = 1;
             }
-            nic_base_offset = pseg[periph[periph_index]->psegid]->base;
-            nb_nic_channel = periph[periph_index]->channels;
-        }
-        else if (strcmp(str, "IOB") == 0) {
+        }
+        else if (strcmp(str, "CMA") == 0) 
+        {
+            periph[periph_index]->type = PERIPH_TYPE_CMA;
+            if (header->cma_cluster == 0xFFFFFFFF)  
+            {
+                header->cma_cluster = cluster_index;
+                cma_channels = periph[periph_index]->channels;
+            }
+            else if (header->nic_cluster_bis == 0xFFFFFFFF) 
+            {
+                header->cma_cluster_bis = cluster_index;
+            }
+            else  
+            {
+                error = 1;
+            }
+        }
+        else if (strcmp(str, "IOB") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_IOB;
-            iob_base_offset = pseg[periph[periph_index]->psegid]->base;
-
-            if (io_mmu_active) {
+            io_mmu_active = 1;
+            if (header->iob_cluster == 0xFFFFFFFF)  
+            {
+                header->iob_cluster = cluster_index; 
+            }
+            else if (header->iob_cluster_bis == 0xFFFFFFFF) 
+            {
+                header->iob_cluster_bis = cluster_index; 
+            }
+            else  
+            {
                 error = 1;
             }
-            io_mmu_active = 1;
-        }
-        // The TIM, ICU, XICU, DMA and IOB peripherals can be replicated in several clusters
-        // one per cluster
-        else if (strcmp(str, "TIM") == 0 ) {
+        }
+        // The TIM, ICU, XICU, DMA peripherals are replicated in all clusters
+        // but only one component per cluster
+        else if (strcmp(str, "TIM") == 0 ) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_TIM;
-            if (found_timer) {
-                error = 1;
-            }
+            if (found_timer || use_xicu)  error = 1; 
             found_timer = 1;
-
-            if (tim_base_offset == 0xFFFFFFFF) {
-                tim_base_offset = pseg[ periph[periph_index]->psegid ]->base;
-            }
-
-            if (nb_timer_channel_max < periph[periph_index]->channels) {
-                nb_timer_channel_max = periph[periph_index]->channels;
-            }
-        }
-        else if (strcmp(str, "ICU") == 0) {
+            if (tim_channels < periph[periph_index]->channels) 
+            {
+                tim_channels = periph[periph_index]->channels;
+            }
+        }
+        else if (strcmp(str, "ICU") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_ICU;
-            if (found_icu) {
-                error = 1;
-            }
+            if (found_icu)  error = 1; 
             found_icu = 1;
-
-            if (icu_base_offset == 0xFFFFFFFF) {
-                icu_base_offset = pseg[periph[periph_index]->psegid]->base;
-            }
-        }
-        else if (strcmp(str, "XICU") == 0) {
-            periph[periph_index]->type = PERIPH_TYPE_XICU;
-            if (found_xicu) {
-                error = 1;
-            }
-            found_xicu = 1;
-
-            //'icu' since we can't have both xicu and icu in an arch
-            if (icu_base_offset == 0xFFFFFFFF) {
-                icu_base_offset = pseg[ periph[periph_index]->psegid ]->base;
-            }
-
-            if (nb_timer_channel_max == 0) {
-                nb_timer_channel_max = 32;
-            }
-        }
-        else if (strcmp(str, "DMA") == 0) {
+        }
+        else if (strcmp(str, "XICU") == 0) 
+        {
+            periph[periph_index]->type = PERIPH_TYPE_ICU;
+            if (found_icu || found_timer)  error = 1; 
+            found_icu = 1;
+            if (tim_channels == 0) 
+            { 
+                tim_channels = 32; 
+            }
+            use_xicu = 1;
+        }
+        else if (strcmp(str, "DMA") == 0) 
+        {
             periph[periph_index]->type = PERIPH_TYPE_DMA;
-            if (found_dma) {
-                error = 1;
-            }
+            if (found_dma)  error = 1; 
             found_dma = 1;
-
-            if (dma_base_offset == 0xFFFFFFFF) {
-                dma_base_offset = pseg[periph[periph_index]->psegid]->base;
-            }
-            if (nb_dma_channel_max < periph[periph_index]->channels) {
-                nb_dma_channel_max = periph[periph_index]->channels;
-            }
-        }
-        else {
+            if (dma_channels < periph[periph_index]->channels)
+                dma_channels = periph[periph_index]->channels;
+        }
+        else 
+        {
             printf("[XML ERROR] illegal <type> for peripheral %d in cluster %d\n",
                     periph_loc_index, cluster_index);
@@ -1124,5 +1263,6 @@
         }
 
-        if (error) {
+        if (error) 
+        {
             printf("[XML ERROR] illegal <type> for peripheral %d in cluster %d\n",
                     periph_loc_index, cluster_index);
@@ -1130,10 +1270,10 @@
         }
     }
-    else {
+    else 
+    {
         printf("[XML ERROR] missing <type> for peripheral  %d in cluster %d\n",
                 periph_loc_index, cluster_index);
         exit(1);
     }
-
 
     periph_index++;
@@ -1403,5 +1543,5 @@
 void psegNode(xmlTextReaderPtr reader) {
     unsigned int ok;
-    unsigned int value;
+    paddr_t      ll_value;
     char * str;
 
@@ -1450,10 +1590,10 @@
 
     //////// get base attribute
-    value = getIntValue(reader, "base", &ok);
-#if XML_PARSER_DEBUG
-    printf("      base = 0x%x\n", value);
+    ll_value = getPaddrValue(reader, "base", &ok);
+#if XML_PARSER_DEBUG
+    printf("      base = 0x%llx\n", ll_value);
 #endif
     if (ok) {
-        pseg[pseg_index]->base = value;
+        pseg[pseg_index]->base = ll_value;
     }
     else {
@@ -1464,10 +1604,10 @@
 
     //////// get length attribute
-    value = getIntValue(reader, "length", &ok);
-#if XML_PARSER_DEBUG
-    printf("      length = 0x%x\n", value);
+    ll_value = getPaddrValue(reader, "length", &ok);
+#if XML_PARSER_DEBUG
+    printf("      length = 0x%llx\n", ll_value);
 #endif
     if (ok) {
-        pseg[pseg_index]->length = value;
+        pseg[pseg_index]->length = ll_value;
     }  
     else {
@@ -1485,6 +1625,7 @@
 
 
-/////////////////////////////////////////////
-void clusterNode(xmlTextReaderPtr reader) {
+/////////////////////////////////////////
+void clusterNode(xmlTextReaderPtr reader) 
+{
     unsigned int ok;
     unsigned int value;
@@ -1510,5 +1651,4 @@
     found_timer = 0;
     found_icu = 0;
-    found_xicu = 0;
     found_dma = 0;
 
@@ -1552,5 +1692,6 @@
     int status = xmlTextReaderRead(reader);
 
-    while (status == 1) {
+    while (status == 1) 
+    {
         const char * tag = (const char *) xmlTextReaderConstName(reader);
 
@@ -1561,33 +1702,29 @@
         else if (strcmp(tag, "#text")    == 0) { }
         else if (strcmp(tag, "#comment") == 0) { }
-        else if (strcmp(tag, "cluster")  == 0) {
-
-            if (use_xicu == 0xFFFFFFFF) {
-                use_xicu = found_xicu;
-            }
-
-            ////////////////// peripherals checks ////////////////////
-            if ((found_timer  && use_xicu) || (!found_timer  && !use_xicu)) {
+        else if (strcmp(tag, "cluster")  == 0) 
+        {
+
+            ////////////////// peripherals checks /////////////////////////
+            if ((found_timer  && use_xicu) || (!found_timer  && !use_xicu)) 
+            {
                 printf("[XML ERROR] illegal or missing timer peripheral in cluster %d\n", cluster_index);
                 exit(1);
             }
 
-            if ((found_icu && use_xicu) || (!found_icu && !use_xicu)) {
+            if (!found_icu) 
+            {
                 printf("[XML ERROR] illegal or missing icu peripheral in cluster %d\n", cluster_index);
                 exit(1);
             }
 
-            if (!found_xicu && use_xicu) {
+            if (!found_dma) 
+            {
                 printf("[XML ERROR] illegal or missing dma peripheral in cluster %d\n", cluster_index);
                 exit(1);
             }
 
-            if (!found_dma) {
-                printf("[XML ERROR] illegal or missing dma peripheral in cluster %d\n", cluster_index);
-                exit(1);
-            }
-
-
-            if (nb_proc_max < cluster[cluster_index]->procs) {
+
+            if (nb_proc_max < cluster[cluster_index]->procs) 
+            {
                 nb_proc_max = cluster[cluster_index]->procs;
             }
@@ -1609,8 +1746,7 @@
 
 //////////////////////////////////////////////
-void clusterSetNode(xmlTextReaderPtr reader) {
-    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) {
-        return;
-    }
+void clusterSetNode(xmlTextReaderPtr reader) 
+{
+    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) { return; }
 
 #if XML_PARSER_DEBUG
@@ -1619,20 +1755,23 @@
 
     int status = xmlTextReaderRead(reader);
-    while (status == 1) {
+    while (status == 1) 
+    {
         const char * tag = (const char *) xmlTextReaderConstName(reader);
 
-        if (strcmp(tag, "cluster")    == 0) {
-            clusterNode(reader);
-        }
+        if      (strcmp(tag, "cluster")    == 0) { clusterNode(reader); }
         else if (strcmp(tag, "#text")      == 0) { }
         else if (strcmp(tag, "#comment")   == 0) { }
-        else if (strcmp(tag, "clusterset") == 0) {
+        else if (strcmp(tag, "clusterset") == 0) 
+        {
             // checking source file consistency
-            if (cluster_index != header->clusters) {
+            if (cluster_index != header->clusters) 
+            {
                 printf("[XML ERROR] Wrong number of clusters\n");
                 exit(1);
             }
 
-            if (header->tty_clusterid == 0xFFFFFFFF) {
+            // At least one TTY terminal for system boot
+            if (header->tty_cluster == 0xFFFFFFFF) 
+            {
                 printf("[XML ERROR] illegal or missing tty peripheral");
                 exit(1);
@@ -1647,4 +1786,5 @@
             header->coprocs = coproc_index;
             header->cp_ports = cp_port_index;
+            header->periphs = periph_index;
             return;
         }
@@ -1669,10 +1809,9 @@
 
     int status = xmlTextReaderRead(reader);
-    while (status == 1) {
+    while (status == 1) 
+    {
         const char * tag = (const char *) xmlTextReaderConstName(reader);
 
-        if (strcmp(tag, "vseg") == 0) {
-            vsegNode(reader);
-        }
+        if      (strcmp(tag, "vseg")      == 0) { vsegNode(reader); }
         else if (strcmp(tag, "#text")     == 0) { }
         else if (strcmp(tag, "#comment")  == 0) { }
@@ -1736,12 +1875,11 @@
 
 //////////////////////////////////////////
-void headerNode(xmlTextReaderPtr reader) {
+void headerNode(xmlTextReaderPtr reader) 
+{
     char * name;
     unsigned int value;
     unsigned int ok;
 
-    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) {
-        return;
-    }
+    if (xmlTextReaderNodeType(reader) == XML_READER_TYPE_END_ELEMENT) { return; }
 
 #if XML_PARSER_DEBUG
@@ -1820,9 +1958,17 @@
     }
 
-    //////// initialise non replicated peripherals cluster_id
-    header->tty_clusterid = 0xFFFFFFFF;
-    header->nic_clusterid = 0xFFFFFFFF;
-    header->ioc_clusterid = 0xFFFFFFFF;
-    header->fbf_clusterid = 0xFFFFFFFF;
+    //////// initialise non replicated peripherals cluster index
+    header->tty_cluster = 0xFFFFFFFF;
+    header->nic_cluster = 0xFFFFFFFF;
+    header->ioc_cluster = 0xFFFFFFFF;
+    header->fbf_cluster = 0xFFFFFFFF;
+    header->cma_cluster = 0xFFFFFFFF;
+    header->iob_cluster = 0xFFFFFFFF;
+    header->tty_cluster_bis = 0xFFFFFFFF;
+    header->nic_cluster_bis = 0xFFFFFFFF;
+    header->ioc_cluster_bis = 0xFFFFFFFF;
+    header->fbf_cluster_bis = 0xFFFFFFFF;
+    header->cma_cluster_bis = 0xFFFFFFFF;
+    header->iob_cluster_bis = 0xFFFFFFFF;
 
     ///////// set signature
@@ -1940,5 +2086,6 @@
 // this function set the value the vobj_id fiels of all cp_ports
 ///////////////////////////////////////////////////////////////////////
-void prepareBuild() {
+void prepareBuild() 
+{
     unsigned int i;
     //asign for all cp_ports the correct vspaceid and vobjid
@@ -1972,9 +2119,10 @@
 }
 
-
 //////////////////////////////////////////
-void file_write(int fdout, char * towrite) {
+void file_write(int fdout, char * towrite) 
+{
     unsigned int size = strlen(towrite);
-    if (size != write(fdout, towrite, size)) {
+    if (size != write(fdout, towrite, size)) 
+    {
         printf("file_write error");
         exit(1);
@@ -1982,7 +2130,7 @@
 }
 
-
 //////////////////////////////////////////////////
-void def_int_write(int fdout, char * def, int num) {
+void def_int_write(int fdout, char * def, int num) 
+{
     char  buf[64];
     sprintf(buf, "#define\t %s  %d\n", def, num);
@@ -1990,7 +2138,7 @@
 }
 
-
-/////////////////////////////////////////////////
-void def_hex_write(int fdout, char * def, int num) {
+//////////////////////////////////////////////////
+void def_hex_write(int fdout, char * def, int num) 
+{
     char  buf[64];
     sprintf(buf, "#define\t %s  0x%x\n", def, num);
@@ -1998,29 +2146,39 @@
 }
 
-
-///////////////////////////////////////
-void  genHd(const char * file_path) {
+///////////////////////////////////
+void  genHd(const char * file_path) 
+{
     int fdout = open_file(file_path);
 
-    char * prol = " /* Generated from the mapping_info file */\n\n#ifndef _HD_CONFIG_H\n#define _HD_CONFIG_H\n\n";
+    char * prol   = "/* Generated from the mapping_info file */\n\n";
+    char * ifdef  = "#ifndef _HD_CONFIG_H\n#define _HD_CONFIG_H\n\n";
+    char * epil   = "\n#endif //_HD_CONFIG_H";
+
     file_write(fdout, prol);
-
-    def_int_write(fdout, "CLUSTER_X"    , cluster_x);
-    def_int_write(fdout, "CLUSTER_Y"    , cluster_y);
-    def_int_write(fdout, "NB_CLUSTERS"  , cluster_index);
-    def_hex_write(fdout, "CLUSTER_SIZE" , (((unsigned long long) 1) << 32) / cluster_index);
-    def_int_write(fdout, "NB_PROCS_MAX" , nb_proc_max);
-    def_int_write(fdout, "NB_TIMERS_MAX", nb_timer_channel_max);
-    def_int_write(fdout, "NB_DMAS_MAX"  , nb_dma_channel_max);
-    def_int_write(fdout, "NB_TTYS"      , nb_tty_channel);
-    def_int_write(fdout, "NB_IOCS"      , nb_ioc_channel);
-    def_int_write(fdout, "NB_NICS"      , nb_nic_channel);
-    def_int_write(fdout, "NB_TASKS"     , nb_tasks_max);
+    file_write(fdout, ifdef);
+
+    def_int_write(fdout, "CLUSTER_X         ", cluster_x);
+    def_int_write(fdout, "CLUSTER_Y         ", cluster_y);
+    def_int_write(fdout, "NB_CLUSTERS       ", cluster_index);
+    def_int_write(fdout, "NB_PROCS_MAX      ", nb_proc_max);
+    def_int_write(fdout, "NB_TASKS_MAX      ", nb_tasks_max);
 
     file_write(fdout, "\n");
-    def_int_write(fdout, "USE_XICU"     , use_xicu);
-    def_int_write(fdout, "IOMMU_ACTIVE ", io_mmu_active);
-
-    char * epil = "\n#endif //_HD_CONFIG_H";
+
+    def_int_write(fdout, "NB_TIM_CHANNELS   ", tim_channels);
+    def_int_write(fdout, "NB_DMA_CHANNELS   ", dma_channels);
+
+    file_write(fdout, "\n");
+
+    def_int_write(fdout, "NB_TTY_CHANNELS   ", tty_channels);
+    def_int_write(fdout, "NB_IOC_CHANNELS   ", ioc_channels);
+    def_int_write(fdout, "NB_NIC_CHANNELS   ", nic_channels);
+    def_int_write(fdout, "NB_CMA_CHANNELS   ", cma_channels);
+
+    file_write(fdout, "\n");
+
+    def_int_write(fdout, "USE_XICU          ", use_xicu);
+    def_int_write(fdout, "IOMMU_ACTIVE      ", io_mmu_active);
+
     file_write(fdout, epil);
 
@@ -2028,48 +2186,97 @@
 }
 
-
 ////////////////////////////////////////////////////////
-void ld_write(int fdout, char * seg, unsigned int addr) {
+void ld_write(int fdout, char * seg, unsigned int addr) 
+{
     char buf[64];
     sprintf(buf, "%s = 0x%x;\n", seg, addr);
     file_write(fdout, buf);
-
 }
 
-
-///////////////////////////////////////
-void genLd(const char * file_path) {
-    int fdout = open_file(file_path);
+//////////////////////////////////
+void genLd(const char * file_path) 
+{
+    int          fdout = open_file(file_path);
+    unsigned int count = 0;
+    unsigned int vseg_id;
 
     char * prol = "/* Generated from the mapping_info file */\n\n";
     file_write(fdout, prol);
 
-    //boot
-    ld_write(fdout, "seg_boot_code_base", boot_code_base);
-    ld_write(fdout, "seg_boot_stack_base", boot_stack_base);
-    ld_write(fdout, "seg_mapping_base", boot_mapping_base);
-
-    //kernel
-    ld_write(fdout, "\nseg_kernel_code_base",  kernel_code_base);
-    ld_write(fdout, "seg_kernel_data_base",    kernel_data_base);
-    ld_write(fdout, "seg_kernel_uncdata_base", kernel_uncdata_base);
-    ld_write(fdout, "seg_kernel_init_base",    kernel_init_base);
-
-    //peripherals
-    ld_write(fdout, "\nseg_fbf_base", fbf_base_offset);
-    ld_write(fdout, "seg_icu_base",   icu_base_offset);
-    ld_write(fdout, "seg_ioc_base",   ioc_base_offset);
-    ld_write(fdout, "seg_nic_base",   nic_base_offset);
-    ld_write(fdout, "seg_tty_base",   tty_base_offset);
-    ld_write(fdout, "seg_dma_base",   dma_base_offset);
-    ld_write(fdout, "seg_tim_base",   tim_base_offset);
-    ld_write(fdout, "seg_gcd_base",   gcd_base_offset);
-    ld_write(fdout, "seg_iob_base",   iob_base_offset);
+    // boot and kernel segments
+    for (vseg_id = 0 ; vseg_id < header->vsegs ; vseg_id++)
+    {
+        if ( strcmp(vseg[vseg_id]->name, "seg_boot_code") == 0 )
+        {
+            ld_write(fdout, "seg_boot_code_base      ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+        else if ( strcmp(vseg[vseg_id]->name, "seg_boot_stack") == 0 )
+        {
+            ld_write(fdout, "seg_boot_stack_base     ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+        else if ( strcmp(vseg[vseg_id]->name, "seg_boot_mapping") == 0 )
+        {
+            ld_write(fdout, "seg_mapping_base        ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+        else if ( strcmp(vseg[vseg_id]->name, "seg_kernel_code") == 0 )
+        {
+            ld_write(fdout, "seg_kernel_code_base    ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+        else if ( strcmp(vseg[vseg_id]->name, "seg_kernel_data") == 0 )
+        {
+            ld_write(fdout, "seg_kernel_data_base    ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+        else if ( strcmp(vseg[vseg_id]->name, "seg_kernel_uncdata") == 0 )
+        {
+            ld_write(fdout, "seg_kernel_uncdata_base ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+        else if ( strcmp(vseg[vseg_id]->name, "seg_kernel_init") == 0 )
+        {
+            ld_write(fdout, "seg_kernel_init_base    ",  vseg[vseg_id]->vbase);
+            count++;
+        }
+    }
+    if ( count != 7 )
+    { 
+        printf ("[XML ERROR] Missing Boot or Kernel vseg : only %d\n", count);
+        printf ("Mandatory segments are :\n");
+        printf (" - seg_boot_code\n");
+        printf (" - seg_boot_stack\n");
+        printf (" - seg_boot_mapping\n");
+        printf (" - seg_kernel_code\n");
+        printf (" - seg_kernel_data\n");
+        printf (" - seg_kernel_uncdata\n");
+        printf (" - seg_kernel_init\n");
+    }
+
+    file_write(fdout, "\n");
+
+    // non replicated peripherals
+    ld_write(fdout, "\nseg_fbf_base            ", periph_vbase_array[PERIPH_TYPE_FBF]);
+    ld_write(fdout, "seg_ioc_base            ",   periph_vbase_array[PERIPH_TYPE_IOC]);
+    ld_write(fdout, "seg_nic_base            ",   periph_vbase_array[PERIPH_TYPE_NIC]);
+    ld_write(fdout, "seg_tty_base            ",   periph_vbase_array[PERIPH_TYPE_TTY]);
+    ld_write(fdout, "seg_gcd_base            ",   periph_vbase_array[PERIPH_TYPE_GCD]);
+    ld_write(fdout, "seg_iob_base            ",   periph_vbase_array[PERIPH_TYPE_IOB]);
+
+    file_write(fdout, "\n");
+
+    // replicated peripherals
+    ld_write(fdout, "seg_icu_base            ",   periph_vbase_array[PERIPH_TYPE_ICU]);
+    ld_write(fdout, "seg_dma_base            ",   periph_vbase_array[PERIPH_TYPE_DMA]);
+    ld_write(fdout, "seg_tim_base            ",   periph_vbase_array[PERIPH_TYPE_TIM]);
 
     close(fdout);
 }
 
-
-char * buildPath(const char * path, const char * name) {
+//////////////////////////////////////////////////////
+char * buildPath(const char * path, const char * name) 
+{
     char * res = calloc(strlen(path) + strlen(name) + 1, 1);
     strcat(res, path);
@@ -2080,6 +2287,7 @@
 
 
-/////////////////////////////////////
-int main(int argc, char * argv[]) {
+//////////////////////////////////
+int main(int argc, char * argv[]) 
+{
     if (argc < 3) {
         printf("Usage: xml2bin <input_file_path> <output_path>\n");
