Index: branch/giet_vm_ioc_drivers/giet_drivers/bdv_driver.c
===================================================================
--- branch/giet_vm_ioc_drivers/giet_drivers/bdv_driver.c	(revision 283)
+++ branch/giet_vm_ioc_drivers/giet_drivers/bdv_driver.c	(revision 283)
@@ -0,0 +1,329 @@
+///////////////////////////////////////////////////////////////////////////////////
+// File     : ioc_driver.c
+// Date     : 23/05/2013
+// Author   : alain greiner
+// Copyright (c) UPMC-LIP6
+///////////////////////////////////////////////////////////////////////////////////
+// The ioc_driver.c and ioc_driver.h files are part ot the GIET-VM kernel.
+// This driver supports the SocLib vci_block_device component, that is
+// a single channel, block oriented, external storage contrÃŽler.
+//
+// It can exist only one block-device controler in the architecture.
+//
+// The _bdv_read() and _bdv_write() functions use the _bdv_access() function,
+// that is always blocking, but can be called in 4 modes:
+//
+// - In BOOT_PA mode, the _bdv_access() function use the buffer virtual address 
+//   as a physical address (as the page tables are not build) and use a polling
+//   policy on the IOC_STATUS register to detect transfer completion, as
+//   hardware interrupts are not activated. This mode is used by the
+//   boot code to load the map.bin file into memory.
+//
+// - In BOOT_VA mode, the _bdv_access() function makes a V2P translation to
+//   compute the buffer physical address, and use a polling policy on IOC_STATUS
+//   register to detect transfer completion. This mode is used by the boot code
+//   to load the various .elf files into memory.
+//
+// - In KERNEL mode, the _bdv_access() function makes a V2P translation to
+//   compute the buffer physical address, and use a descheduling strategy:
+//   The ISR executed when transfer completes should restart the calling task. 
+//   There is no checking of user access right to the memory buffer.
+//   This mode must be used to access IOC, for an "open" system call.
+//
+// - In USER mode, the _bdv_access() function makes a V2P translation to
+//   compute the buffer physical address, and use a descheduling strategy:
+//   The ISR executed when transfer completes should restart the calling task, 
+//   The user access right to the memory buffer must be checked.
+//   This mode must be used to access IOC, for a "read/write" system call.
+//
+// As the IOC component can be used by several programs running in parallel,
+// the _ioc_lock variable guaranties exclusive access to the device.  The
+// _bdv_read() and _bdv_write() functions use atomic LL/SC to get the lock.
+//
+// The IOMMU can be activated or not:
+// 
+// 1) When the IOMMU is used, a fixed size 2Mbytes vseg is allocated to 
+// the IOC peripheral, in the I/O virtual space, and the user buffer is
+// dynamically remapped in the IOMMU page table. The corresponding entry 
+// in the IOMMU PT1 is defined by the kernel _ioc_iommu_ix1 variable.
+// The number of pages to be unmapped is stored in the _ioc_npages variable.
+// The number of PT2 entries is dynamically computed and stored in the
+// kernel _ioc_iommu_npages variable. It cannot be larger than 512.
+// The user buffer is unmapped by the _ioc_completed() function when 
+// the transfer is completed.
+//
+// 2/ If the IOMMU is not used, we check that  the user buffer is mapped to a
+// contiguous physical buffer (this is generally true because the user space
+// page tables are statically constructed to use contiguous physical memory).
+//
+// Finally, the memory buffer must fulfill the following conditions:
+// - The buffer must be word aligned, 
+// - The buffer must be mapped in user space for an user access, 
+// - The buffer must be writable in case of (to_mem) access,
+// - The total number of physical pages occupied by the user buffer cannot
+//   be larger than 512 pages if the IOMMU is activated,
+// - All physical pages occupied by the user buffer must be contiguous
+//   if the IOMMU is not activated.
+// An error code is returned if these conditions are not verified.
+///////////////////////////////////////////////////////////////////////////////////
+// The seg_ioc_base virtual base addresses must be defined in giet_vsegs.ld file.
+///////////////////////////////////////////////////////////////////////////////////
+
+#include <giet_config.h>
+#include <ioc_driver.h>
+#include <bdv_driver.h>
+#include <utils.h>
+#include <tty_driver.h>
+#include <ctx_handler.h>
+
+///////////////////////////////////////////////////////////////////////////////
+//      _bdv_access()
+// This function transfer data between a memory buffer and the block device.
+// The buffer lentgth is (count*block_size) bytes.
+// Arguments are:
+// - to_mem     : from external storage to memory when non 0.
+// - kernel     : kernel buffer with identity mapping when non 0. 
+// - lba        : first block index on the external storage.
+// - buf_vaddr  : virtual base address of the memory buffer.
+// - count      : number of blocks to be transfered.
+// Returns 0 if success, > 0 if error.
+///////////////////////////////////////////////////////////////////////////////
+static unsigned int _bdv_access( unsigned int to_mem,
+                                 unsigned int mode,
+                                 unsigned int lba,
+                                 paddr_t buf_paddr,
+                                 unsigned int count) 
+{
+
+#if GIET_DEBUG_IOC_DRIVER
+_tty_get_lock( 0 );
+_puts("\n[IOC DEBUG] Enter _bdv_access() at cycle ");
+_putd( _get_proctime() );
+_puts(" for processor ");
+_putd( _get_procid() );
+_puts("\n - mode    = ");
+_putd( mode );
+_puts("\n - paddr   = ");
+_putx( buf_paddr );
+_puts("\n - sectors = ");
+_putd( count );
+_puts("\n - lba     = ");
+_putx( lba );
+_puts("\n");
+_tty_release_lock( 0 );
+#endif
+
+    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base ;
+    unsigned int error = 0;
+
+    // get the lock protecting IOC
+    _get_lock(&_ioc_lock);
+
+    // set the _ioc_status polling variable
+    _ioc_status = BLOCK_DEVICE_BUSY;
+
+    ioc_address[BLOCK_DEVICE_BUFFER]     = (unsigned int)buf_paddr;
+    ioc_address[BLOCK_DEVICE_BUFFER_EXT] = (unsigned int)(buf_paddr>>32);
+    ioc_address[BLOCK_DEVICE_COUNT]      = count;
+    ioc_address[BLOCK_DEVICE_LBA]        = lba;
+
+    // There is two policies for transfer completion 
+	// detection, depending on the mode argument:
+
+    if ( (mode == IOC_BOOT_PA_MODE) ||    // We poll directly the IOC_STATUS register
+         (mode == IOC_BOOT_VA_MODE) )     // as IRQs are masked.
+    {
+        // Launch transfert
+        if (to_mem == 0) ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_WRITE;
+        else             ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_READ;
+
+        unsigned int status;
+        if ( _bdv_get_status(0, &status) ) return 1;
+
+        while( (status != BLOCK_DEVICE_READ_SUCCESS)  &&
+               (status != BLOCK_DEVICE_READ_ERROR)    &&
+               (status != BLOCK_DEVICE_WRITE_SUCCESS) &&
+               (status != BLOCK_DEVICE_WRITE_ERROR) ) 
+        {
+            if ( _bdv_get_status(0, &status) ) return 1;
+
+#if GIET_DEBUG_IOC_DRIVER
+_tty_get_lock( 0 );
+_puts("\n[IOC DEBUG] _bdv_access() : ... waiting on IOC_STATUS register ...\n");
+_tty_release_lock( 0 );
+#endif
+
+        }
+        // analyse status
+        error = ( (status == BLOCK_DEVICE_READ_ERROR) ||
+                  (status == BLOCK_DEVICE_WRITE_ERROR) );
+
+        // release lock
+        _release_lock(&_ioc_lock);      
+    }
+    else                           // in USER or KERNEL mode, we deschedule the task.
+                                   // When the task is rescheduled by the ISR, we reset 
+                                   // the _ioc_status variable, and release the lock
+    {
+        // We need a critical section, because we must reset the RUN bit
+		// before to launch the transfer, and we want to avoid to be descheduled
+		// between these two operations. 
+
+        // Enter critical section
+        _it_disable(); 
+        
+        // set _ioc_gtid and reset runnable 
+        unsigned int ltid = _get_proc_task_id();
+        unsigned int pid = _get_procid();
+        _ioc_gtid = (pid<<16) + ltid;
+        _set_task_slot( pid, ltid, CTX_RUN_ID, 0 );  
+        
+        // Launch transfert
+        if (to_mem == 0) ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_WRITE;
+        else             ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_READ;
+
+        // deschedule task
+        _ctx_switch();                      
+
+        // analyse status
+        error = ( (_ioc_status == BLOCK_DEVICE_READ_ERROR) ||
+                  (_ioc_status == BLOCK_DEVICE_WRITE_ERROR) );
+
+        // reset _ioc_status and release lock
+        _ioc_status = BLOCK_DEVICE_IDLE; 
+        _release_lock(&_ioc_lock);      
+    }
+
+#if GIET_DEBUG_IOC_DRIVER
+_tty_get_lock( 0 );
+_puts("\n[IOC DEBUG] _bdv_access completed at cycle ");
+_putd( _get_proctime() );
+_puts(" for processor ");
+_putd( _get_procid() );
+_puts(" : error = ");
+_putd( (unsigned int)error );
+_puts("\n");
+_tty_release_lock( 0 );
+#endif
+
+    return error;
+} // end _bdv_access()
+
+///////////////////////////////////////////////////////////////////////////////
+//       _bdv_init()
+// This function cheks block size, and activates the IOC interrupts.
+// Return 0 for success, > 0 if error
+///////////////////////////////////////////////////////////////////////////////
+unsigned int _bdv_init( unsigned int channel )
+{
+    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base ;
+    
+    if ( ioc_address[BLOCK_DEVICE_BLOCK_SIZE] != 512 )
+    {
+        _tty_get_lock( 0 );
+        _puts("\n[GIET ERROR] in _bdv_init() : block size must be 512 bytes\n");
+        _tty_release_lock( 0 );
+        return 1; 
+    }
+
+    if ( channel != 0 )
+    {
+        _tty_get_lock( 0 );
+        _puts("\n[GIET ERROR] in _bdv_init() : illegal channel\n");
+        _tty_release_lock( 0 );
+
+        return 1;
+    }
+
+    ioc_address[BLOCK_DEVICE_IRQ_ENABLE] = 1;
+    return 0;
+}
+
+///////////////////////////////////////////////////////////////////////////////
+//     _bdv_read()
+// Transfer data from the block device to a memory buffer. 
+// - mode     : BOOT / KERNEL / USER
+// - lba      : first block index on the block device
+// - buffer   : base address of the memory buffer (must be word aligned)
+// - count    : number of blocks to be transfered.
+// Returns 0 if success, > 0 if error.
+///////////////////////////////////////////////////////////////////////////////
+unsigned int _bdv_read( unsigned int mode,  
+                        unsigned int lba, 
+                        paddr_t      buffer, 
+                        unsigned int count) 
+{
+    return _bdv_access( 1,        // read access
+                        mode,  
+                        lba,
+                        buffer,
+                        count );
+}
+
+///////////////////////////////////////////////////////////////////////////////
+//     _bdv_write()
+// Transfer data from a memory buffer to the block device. 
+// - mode     : BOOT / KERNEL / USER
+// - lba      : first block index on the block device
+// - buffer   : base address of the memory buffer (must be word aligned)
+// - count    : number of blocks to be transfered.
+// Returns 0 if success, > 0 if error.
+///////////////////////////////////////////////////////////////////////////////
+unsigned int _bdv_write( unsigned int mode,  
+                         unsigned int lba, 
+                         paddr_t  buffer, 
+                         unsigned int count ) 
+{
+    return _bdv_access( 0,        // write access
+                        mode,  
+                        lba,
+                        buffer,
+                        count );
+}
+
+///////////////////////////////////////////////////////////////////////////////
+//     _bdv_get_status()
+// This function returns in the status variable, the transfert status, and
+// acknowledge the IRQ if the IOC controler is not busy.
+// Returns 0 if success, > 0 if error
+///////////////////////////////////////////////////////////////////////////////
+unsigned int _bdv_get_status( unsigned int  channel,
+                              unsigned int* status )
+{
+    if ( channel != 0 )
+    {
+        _tty_get_lock( 0 );
+        _puts("\n[GIET ERROR] in _bdv_get_status() : illegal channel\n");
+        _tty_release_lock( 0 );
+
+        return 1;
+    }
+
+    // get IOC base address
+    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base;
+    *status = ioc_address[BLOCK_DEVICE_STATUS];
+
+    return 0;
+}
+
+///////////////////////////////////////////////////////////////////////////////
+//     _bdv_get_block_size()
+// This function returns the block_size with which the IOC has been configured.
+///////////////////////////////////////////////////////////////////////////////
+unsigned int _bdv_get_block_size() 
+{
+    // get IOC base address
+    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base;
+    
+    return  ioc_address[BLOCK_DEVICE_BLOCK_SIZE];
+}
+
+
+// Local Variables:
+// tab-width: 4
+// c-basic-offset: 4
+// c-file-offsets:((innamespace . 0)(inline-open . 0))
+// indent-tabs-mode: nil
+// End:
+// vim: filetype=c:expandtab:shiftwidth=4:tabstop=4:softtabstop=4
+
Index: branch/giet_vm_ioc_drivers/giet_drivers/bdv_driver.h
===================================================================
--- branch/giet_vm_ioc_drivers/giet_drivers/bdv_driver.h	(revision 283)
+++ branch/giet_vm_ioc_drivers/giet_drivers/bdv_driver.h	(revision 283)
@@ -0,0 +1,46 @@
+///////////////////////////////////////////////////////////////////////////////////
+// File      : bdv_driver.h
+// Date      : 01/11/2013
+// Author    : alain greiner
+// Maintainer: cesar fuguet
+// Copyright (c) UPMC-LIP6
+///////////////////////////////////////////////////////////////////////////////////
+
+#ifndef _GIET_BDV_DRIVERS_H_
+#define _GIET_BDV_DRIVERS_H_
+
+#include <mapping_info.h>
+
+///////////////////////////////////////////////////////////////////////////////////
+// BDV access functions and variables (vci_block_device)
+///////////////////////////////////////////////////////////////////////////////////
+
+extern unsigned int _bdv_init( unsigned int channel );
+
+extern unsigned int _bdv_write( unsigned int mode,
+                                unsigned int lba, 
+                                paddr_t      buffer, 
+                                unsigned int count );
+
+extern unsigned int _bdv_read(  unsigned int mode,
+                                unsigned int lba, 
+                                paddr_t      buffer,
+                                unsigned int count );
+
+extern unsigned int _bdv_get_status( unsigned int  channel,
+                                     unsigned int* status );
+
+extern unsigned int _bdv_get_block_size();
+
+///////////////////////////////////////////////////////////////////////////////////
+
+#endif
+
+// Local Variables:
+// tab-width: 4
+// c-basic-offset: 4
+// c-file-offsets:((innamespace . 0)(inline-open . 0))
+// indent-tabs-mode: nil
+// End:
+// vim: filetype=c:expandtab:shiftwidth=4:tabstop=4:softtabstop=4
+
Index: branch/giet_vm_ioc_drivers/giet_drivers/hba_driver.c
===================================================================
--- soft/giet_vm/giet_drivers/hba_driver.c	(revision 281)
+++ branch/giet_vm_ioc_drivers/giet_drivers/hba_driver.c	(revision 283)
@@ -124,5 +124,5 @@
 {
     volatile unsigned int* hba_address;
-    hba_address = (unsigned int*)(&seg_hba_base) + (HBA_SPAN*channel);
+    hba_address = (unsigned int*)(&seg_ioc_base) + (HBA_SPAN*channel);
 
     if( channel >= NB_HBA_CHANNELS )
@@ -146,5 +146,5 @@
 {
     volatile unsigned int* hba_address;
-    hba_address = (unsigned int*)(&seg_hba_base) + (HBA_SPAN*channel);
+    hba_address = (unsigned int*)(&seg_ioc_base) + (HBA_SPAN*channel);
 
     if( channel >= NB_HBA_CHANNELS )
@@ -214,5 +214,5 @@
 
     // get hba device address
-    hba_address = (unsigned int*)(&seg_hba_base) + (HBA_SPAN * channel_id);
+    hba_address = (unsigned int*)(&seg_ioc_base) + (HBA_SPAN * channel_id);
 
     // get command list status
@@ -434,5 +434,5 @@
 }
 //////////////////////////////////////////////////////////////////
-// This function initializes for a given channel (k)
+// This function initializes for a given channel
 // - the HBA hardware registers,
 // - the command list pointer,
@@ -440,5 +440,5 @@
 // - the command tables physical addresses array,
 //////////////////////////////////////////////////////////////////
-void _hba_init( unsigned int k )  // k == channel_index
+void _hba_init( unsigned int channel )
 {
     unsigned int ppn;
@@ -452,8 +452,8 @@
 
     // HBA registers
-    unsigned int*  hba_address = (unsigned int*)(&seg_hba_base) + (HBA_SPAN*k);
-    hba_address = (unsigned int*)&seg_hba_base + HBA_SPAN * k;
-
-    hba_address[HBA_PXCLB]  = (unsigned int)(&hba_cmd_list[k]);
+    unsigned int*  hba_address;
+    hba_address = (unsigned int*)&seg_ioc_base + HBA_SPAN * channel;
+
+    hba_address[HBA_PXCLB]  = (unsigned int)(&hba_cmd_list[channel]);
     hba_address[HBA_PXCLBU] = 0;
     hba_address[HBA_PXIE]   = 0x40000001;
@@ -463,8 +463,8 @@
 
     // command list pointer       
-    hba_cmd_slot[k] = 0;
+    hba_cmd_slot[channel] = 0;
 
     // Command list physical addresse
-    vbase = (unsigned int)(&hba_cmd_list[k]);
+    vbase = (unsigned int)(&hba_cmd_list[channel]);
     fail = _v2p_translate( (page_table_t*)pt,
                            vbase>>12,
@@ -478,10 +478,10 @@
         _exit();
     }
-    hba_cmd_list_paddr[k] = ((paddr_t)ppn) | (vbase & 0xFFF);
+    hba_cmd_list_paddr[channel] = ((paddr_t)ppn) | (vbase & 0xFFF);
 
     // Command tables physical addresses
     for( c=0 ; c<32 ; c++ )
     {
-        vbase = (unsigned int)(&hba_cmd_table[k][c]);
+        vbase = (unsigned int)(&hba_cmd_table[channel][c]);
         fail = _v2p_translate( (page_table_t*)pt,
                                vbase>>12,
@@ -495,5 +495,5 @@
             _exit();
         }
-        hba_cmd_table_paddr[k][c] = ((paddr_t)ppn) | (vbase & 0xFFF);
+        hba_cmd_table_paddr[channel][c] = ((paddr_t)ppn) | (vbase & 0xFFF);
     }
 }
Index: branch/giet_vm_ioc_drivers/giet_drivers/ioc_driver.c
===================================================================
--- soft/giet_vm/giet_drivers/ioc_driver.c	(revision 281)
+++ branch/giet_vm_ioc_drivers/giet_drivers/ioc_driver.c	(revision 283)
@@ -87,10 +87,27 @@
 #endif
 
+#if (USE_BDV + USE_SPI + USE_HBA) != 1
+# error: You must use only one IOC controller (BDV or SPI or HBA)
+#endif
+
+#if USE_BDV
+# include <bdv_driver.h>
+#endif
+
+#if USE_SPI
+# include <sdc_driver.h>
+#endif
+
+#if USE_HBA
+# include <hba_driver.h>
+#endif
+
+
 #define in_unckdata __attribute__((section (".unckdata")))
 
 ///////////////////// IOC global variables
 
-in_unckdata unsigned int          _ioc_lock = 0;
-in_unckdata volatile unsigned int _ioc_status = 0;
+in_unckdata unsigned int _ioc_lock = 0;
+in_unckdata unsigned int _ioc_status = 0;
 in_unckdata volatile unsigned int _ioc_gtid;
 in_unckdata volatile unsigned int _ioc_iommu_ix1 = 0;
@@ -154,6 +171,4 @@
         return 1; 
     }
-
-    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base ;
 
     unsigned int length = count << 9;  // count * 512 bytes
@@ -269,117 +284,15 @@
     }
 
-    // get the lock protecting IOC
-    _get_lock(&_ioc_lock);
-
-    // set the _ioc_status polling variable
-    _ioc_status = BLOCK_DEVICE_BUSY;
-
-#if GIET_DEBUG_IOC_DRIVER
-_tty_get_lock( 0 );
-_puts("\n[IOC DEBUG] _ioc_access() : configure IOC\n");
-_puts(" - buf_paddr = ");
-_putl( buf_paddr );
-_puts("\n");
-_puts(" - count     = ");
-_putd( count );
-_puts("\n");
-_puts(" - lba       = ");
-_putx( lba );
-_puts("\n");
-_tty_release_lock( 0 );
-#endif
-
-    // send command to IOC   
-    if ( GIET_USE_IOMMU ) 
-    {
-        ioc_address[BLOCK_DEVICE_BUFFER] = buf_xaddr;
-        ioc_address[BLOCK_DEVICE_COUNT]  = count;
-        ioc_address[BLOCK_DEVICE_LBA]    = lba;
-    }
-    else
-    {
-        ioc_address[BLOCK_DEVICE_BUFFER]     = (unsigned int)buf_paddr;
-        ioc_address[BLOCK_DEVICE_BUFFER_EXT] = (unsigned int)(buf_paddr>>32);
-        ioc_address[BLOCK_DEVICE_COUNT]      = count;
-        ioc_address[BLOCK_DEVICE_LBA]        = lba;
-    }
-
-    // There is two policies for transfer completion 
-	// detection, depending on the mode argument:
-
-    if ( (mode == IOC_BOOT_PA_MODE) ||    // We poll directly the IOC_STATUS register
-         (mode == IOC_BOOT_VA_MODE) )     // as IRQs are masked.
-    {
-        // Launch transfert
-        if (to_mem == 0) ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_WRITE;
-        else             ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_READ;
-
-        unsigned int status;
-        if ( _ioc_get_status(0, &status) ) return 1;
-
-        while( (status != BLOCK_DEVICE_READ_SUCCESS)  &&
-               (status != BLOCK_DEVICE_READ_ERROR)    &&
-               (status != BLOCK_DEVICE_WRITE_SUCCESS) &&
-               (status != BLOCK_DEVICE_WRITE_ERROR) ) 
-        {
-            if ( _ioc_get_status(0, &status) ) return 1;
-
-#if GIET_DEBUG_IOC_DRIVER
-_tty_get_lock( 0 );
-_puts("\n[IOC DEBUG] _ioc_access() : ... waiting on IOC_STATUS register ...\n");
-_tty_release_lock( 0 );
-#endif
-
-        }
-        // analyse status
-        error = ( (status == BLOCK_DEVICE_READ_ERROR) ||
-                  (status == BLOCK_DEVICE_WRITE_ERROR) );
-
-        // release lock
-        _release_lock(&_ioc_lock);      
-    }
-    else                           // in USER or KERNEL mode, we deschedule the task.
-                                   // When the task is rescheduled by the ISR, we reset 
-                                   // the _ioc_status variable, and release the lock
-    {
-        // We need a critical section, because we must reset the RUN bit
-		// before to launch the transfer, and we want to avoid to be descheduled
-		// between these two operations. 
-
-        // Enter critical section
-        _it_disable(); 
-        
-        // set _ioc_gtid and reset runnable 
-        unsigned int ltid = _get_proc_task_id();
-        unsigned int pid = _get_procid();
-        _ioc_gtid = (pid<<16) + ltid;
-        _set_task_slot( pid, ltid, CTX_RUN_ID, 0 );  
-        
-        // Launch transfert
-        if (to_mem == 0) ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_WRITE;
-        else             ioc_address[BLOCK_DEVICE_OP] = BLOCK_DEVICE_READ;
-
-        // deschedule task
-        _ctx_switch();                      
-
-        // analyse status
-        error = ( (_ioc_status == BLOCK_DEVICE_READ_ERROR) ||
-                  (_ioc_status == BLOCK_DEVICE_WRITE_ERROR) );
-
-        // reset _ioc_status and release lock
-        _ioc_status = BLOCK_DEVICE_IDLE; 
-        _release_lock(&_ioc_lock);      
-    }
-
-#if GIET_DEBUG_IOC_DRIVER
-_tty_get_lock( 0 );
-_puts("\n[IOC DEBUG] _ioc_access completed at cycle ");
-_putd( _get_proctime() );
-_puts(" for processor ");
-_putd( _get_procid() );
-_puts(" : error = ");
-_putd( (unsigned int)error );
-_puts("\n");
-_tty_release_lock( 0 );
+    if ( GIET_USE_IOMMU ) buf_paddr = (paddr_t) buf_xaddr;
+
+#if   USE_BDV
+    if (to_mem) error = _bdv_read (mode, lba, buf_paddr, count);
+    else        error = _bdv_write(mode, lba, buf_paddr, count);
+#elif USE_SPI
+    if (to_mem) error = _sdc_read (mode, lba, buf_paddr, count);
+    else        error = _sdc_write(mode, lba, buf_paddr, count);
+#elif USE_HBA
+    if (to_mem) error = _hba_read (mode, lba, buf_paddr, count);
+    else        error = _hba_write(mode, lba, buf_paddr, count);
 #endif
 
@@ -392,16 +305,13 @@
 // Return 0 for success.
 ///////////////////////////////////////////////////////////////////////////////
-unsigned int _ioc_init()
-{
-    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base ;
-    
-    if ( ioc_address[BLOCK_DEVICE_BLOCK_SIZE] != 512 )
-    {
-        _puts("\n[GIET ERROR] in _ioc_init() : block size must be 512 bytes\n");
-        _exit();
-    }
-
-    ioc_address[BLOCK_DEVICE_IRQ_ENABLE] = 1;
-    return 0;
+unsigned int _ioc_init( unsigned int channel )
+{
+#if   USE_BDV
+    return _bdv_init( channel );
+#elif USE_SPI
+    return _sdc_init( channel );
+#elif USE_HBA
+    return _hba_init( channel );
+#endif
 }
 
@@ -457,18 +367,11 @@
                               unsigned int* status )
 {
-    if ( channel != 0 )
-    {
-        _tty_get_lock( 0 );
-        _puts("\n[GIET ERROR] in _ioc_get_status : illegal channel\n");
-        _tty_release_lock( 0 );
-
-        return 1;
-    }
-
-    // get IOC base address
-    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base;
-    *status = ioc_address[BLOCK_DEVICE_STATUS];
-
-    return 0;
+#if   USE_BDV
+    return _bdv_get_status(channel, status);
+#elif USE_SPI
+    return _sdc_get_status(channel, status);
+#elif USE_HBA
+    return _hba_get_status(channel, status);
+#endif
 }
 
@@ -479,8 +382,11 @@
 unsigned int _ioc_get_block_size() 
 {
-    // get IOC base address
-    volatile unsigned int * ioc_address = (unsigned int *) &seg_ioc_base;
-    
-    return  ioc_address[BLOCK_DEVICE_BLOCK_SIZE];
+#if   USE_BDV
+    return _bdv_get_block_size();
+#elif USE_SPI
+    return _sdc_get_block_size();
+#elif USE_HBA
+    return _hba_get_block_size();
+#endif
 }
 
Index: branch/giet_vm_ioc_drivers/giet_drivers/ioc_driver.h
===================================================================
--- soft/giet_vm/giet_drivers/ioc_driver.h	(revision 281)
+++ branch/giet_vm_ioc_drivers/giet_drivers/ioc_driver.h	(revision 283)
@@ -53,11 +53,11 @@
 ///////////////////////////////////////////////////////////////////////////////////
 
-extern unsigned int          _ioc_lock;
-extern volatile unsigned int _ioc_status;
+extern unsigned int _ioc_lock;
+extern unsigned int _ioc_status;
 extern volatile unsigned int _ioc_gtid;
 extern volatile unsigned int _ioc_iommu_ix1;
 extern volatile unsigned int _ioc_iommu_npages; 
 
-extern unsigned int _ioc_init();
+extern unsigned int _ioc_init( unsigned int channel );
 
 extern unsigned int _ioc_write( unsigned int mode,
Index: branch/giet_vm_ioc_drivers/giet_drivers/sdc_driver.c
===================================================================
--- branch/giet_vm_ioc_drivers/giet_drivers/sdc_driver.c	(revision 283)
+++ branch/giet_vm_ioc_drivers/giet_drivers/sdc_driver.c	(revision 283)
@@ -0,0 +1,490 @@
+/**
+ * \file    : sdc_driver.c
+ * \date    : 30 August 2012
+ * \author  : Cesar Fuguet
+ *
+ * This file defines the driver of a SD Card device using an SPI controller
+ */
+
+#include <sdc_driver.h>
+#include <utils.h>
+
+#define SYSCLK_FREQ           50000000
+#define SDCARD_RESET_ITER_MAX 4
+
+static struct sdcard_dev sdcard;
+static struct spi_dev*   spi;
+
+/**
+ * \return  void
+ *
+ * \brief   Enable SD Card select signal
+ */
+static void _sdc_enable()
+{
+    spi_ss_assert(sdcard.spi, sdcard.slave_id);
+}
+
+/**
+ * \return  void
+ *
+ * \brief   Disable SD Card select signal
+ */
+static void _sdc_disable()
+{
+    spi_ss_deassert(sdcard.spi, sdcard.slave_id);
+}
+
+/**
+ * \param   tick_count: SD Card clock ticks number
+ *
+ * \return  void
+ *
+ * \brief   Enable SD Card clock
+ *          The tick count is byte measured (1 tick, 8 clock)
+ */
+static void _sdc_gen_tick(unsigned int tick_count)
+{
+    register int i = 0;
+    while(i++ < tick_count) spi_put_tx(sdcard.spi, 0xFF, 0);
+}
+
+/**
+ * \param   lba : Position where the block device access
+ *                pointer must be move
+ *
+ * \return  void
+ *
+ * \brief   Change block device access pointer position
+ *  
+ * The block device access pointer is relocated in terms of blocks
+ */
+void _sdc_lseek(unsigned int lba)
+{
+    sdcard.access_pointer = sdcard.block_length * lba;
+}
+
+/**
+ * \return  char from the SD card
+ *
+ * \brief   Get a byte from the SD Card
+ */
+static unsigned char _sdc_receive_char()
+{
+    _sdc_gen_tick(1);
+
+    return spi_get_rx(sdcard.spi, 0);
+}
+
+/**
+ * \return  sdcard response
+ *
+ * \brief   Wait for a valid response after the send of a command
+ *          This function can return if one of the next two conditions are true:
+ *           1. Bit valid received
+ *           2. Timeout (not valid bit received after SDCARD_COMMAND_TIMEOUT
+ *              wait ticks)
+ */
+static unsigned char _sdc_wait_response()
+{
+    unsigned char sdcard_rsp;
+    register int  iter;
+
+    iter       = 0;
+    sdcard_rsp = _sdc_receive_char();
+    while (
+            (iter < SDCARD_COMMAND_TIMEOUT) &&
+            !SDCARD_CHECK_R1_VALID(sdcard_rsp)
+          )
+    {
+        sdcard_rsp = _sdc_receive_char();
+        iter++;
+    }
+
+    return sdcard_rsp;
+}
+
+/**
+ * \return  void
+ *
+ * \brief   Wait data block start marker
+ */
+static void _sdc_wait_data_block()
+{
+	while (_sdc_receive_char() != 0xFE);
+}
+
+/**
+ * \param   index   : SD card CMD index
+ * \param   app     : Type of command, 0 for normal command or 1 for
+ *                    application specific
+ * \param   args    : SD card CMD arguments
+ *
+ * \return  response first byte
+ *
+ * \brief   Send command to the SD card
+ */
+static int _sdc_send_command ( int      index,
+                               int      app  ,
+                               void *   args ,
+                               unsigned crc7 )
+{
+    unsigned char sdcard_rsp;
+    unsigned char * _args;
+
+    _sdc_gen_tick(5);  
+
+    if (app == SDCARD_ACMD)
+    {
+        spi_put_tx(sdcard.spi, 0x40 | 55         , 0 );/* CMD and START bit */
+        spi_put_tx(sdcard.spi, 0x00              , 0 );/* Argument[0]       */
+        spi_put_tx(sdcard.spi, 0x00              , 0 );/* Argument[1]       */
+        spi_put_tx(sdcard.spi, 0x00              , 0 );/* Argument[2]       */
+        spi_put_tx(sdcard.spi, 0x00              , 0 );/* Argument[3]       */
+        spi_put_tx(sdcard.spi, 0x01 | (crc7 << 1), 0 );/* END bit           */
+
+        sdcard_rsp = _sdc_wait_response();
+        if (SDCARD_CHECK_R1_ERROR(sdcard_rsp))
+        {
+            return sdcard_rsp;        
+        }
+    }
+
+    _args = (unsigned char *) args;
+
+    _sdc_gen_tick(1);  
+
+    spi_put_tx(sdcard.spi, 0x40 | index      , 0 );
+    spi_put_tx(sdcard.spi, _args[0]          , 0 );
+    spi_put_tx(sdcard.spi, _args[1]          , 0 );
+    spi_put_tx(sdcard.spi, _args[2]          , 0 );
+    spi_put_tx(sdcard.spi, _args[3]          , 0 );
+    spi_put_tx(sdcard.spi, 0x01 | (crc7 << 1), 0 );
+
+    return _sdc_wait_response();
+}
+
+static int _sdc_open( unsigned int channel )
+{
+	unsigned char args[4];
+	unsigned char sdcard_rsp;
+	unsigned int  iter, ersp;
+
+	sdcard.spi      = spi;
+	sdcard.slave_id = channel;
+
+	/* 
+	* Supply SD card ramp up time (min 74 cycles)
+	*/
+	_sdc_gen_tick(10);
+
+	/* 
+	* Assert slave select signal
+	* Send CMD0 (Reset Command)
+	* Deassert slave select signal
+	*/
+	_sdc_enable();
+
+	args[0] = 0;
+	args[1] = 0;
+	args[2] = 0;
+	args[3] = 0;
+	sdcard_rsp = _sdc_send_command(0, SDCARD_CMD, args, 0x4A);
+	if ( sdcard_rsp != 0x01 )
+	{
+
+		_puts("card CMD0 failed ");
+		return sdcard_rsp;
+	}
+
+	_sdc_disable();
+	/*
+	 * send CMD8. If card is pre-v2, It will reply with illegal command.
+	 * Otherwise we announce sdhc support.
+	 */
+	_sdc_enable();
+	args[0] = 0;
+	args[1] = 0;
+	args[2] = 0x01;
+	args[3] = 0x01;
+	sdcard_rsp = _sdc_send_command(8, SDCARD_CMD, args, 0x63);
+	if (!SDCARD_CHECK_R1_VALID(sdcard_rsp)) {
+		_puts("card CMD8 failed ");
+		return sdcard_rsp;
+	}
+	if (!SDCARD_CHECK_R1_ERROR(sdcard_rsp)) {
+		/* no error, command accepted. get whole reply */
+		ersp = _sdc_receive_char();
+		ersp = (ersp << 8) | _sdc_receive_char();
+		ersp = (ersp << 8) | _sdc_receive_char();
+		ersp = (ersp << 8) | _sdc_receive_char();
+		if ((ersp & 0xffff) != 0x0101) {
+			/* voltage mismatch */
+			_puts("card CMD8 mismatch: ");
+			_putx(ersp);
+			return sdcard_rsp;
+		}
+		_puts("v2 or later ");
+		sdcard.sdhc = 1;
+	} else if ((sdcard_rsp & SDCARD_R1_ILLEGAL_CMD) == 0) {
+		/* other error */
+		_puts("card CMD8 error ");
+		return sdcard_rsp;
+	} else {
+		sdcard.sdhc = 0;
+	}
+	_sdc_disable();
+	/* send CMD41, enabling the card */
+	_sdc_enable();
+	args[0] = sdcard.sdhc ? 0x40: 0;
+	args[1] = 0;
+	args[2] = 0;
+	args[3] = 0;
+
+	iter = 0;
+	while( iter++ < SDCARD_COMMAND_TIMEOUT )
+	{
+		sdcard_rsp = _sdc_send_command(41, SDCARD_ACMD, args, 0x00);
+		if( sdcard_rsp == 0x01 )
+		{
+			continue;
+		}
+
+		break;
+	}
+
+	_sdc_disable();
+	if (sdcard_rsp) {
+		_puts("SD ACMD41 failed ");
+		return sdcard_rsp;
+	}
+	if (sdcard.sdhc != 0) {
+		/* get the card capacity to see if it's really HC */
+		_sdc_enable();
+		args[0] = sdcard.sdhc ? 0x40: 0;
+		args[1] = 0;
+		args[2] = 0;
+		args[3] = 0;
+        sdcard_rsp = _sdc_send_command(58, SDCARD_CMD, args, 0x00);
+		if (sdcard_rsp) {
+			_puts("SD CMD58 failed ");
+			return sdcard_rsp;
+		}
+		ersp = _sdc_receive_char();
+		ersp = (ersp << 8) | _sdc_receive_char();
+		ersp = (ersp << 8) | _sdc_receive_char();
+		ersp = (ersp << 8) | _sdc_receive_char();
+		if (ersp & 0x40000000) {
+			_puts("SDHC ");
+		} else {
+			sdcard.sdhc = 0;
+		}
+		_sdc_disable();
+	}
+	_puts("card detected ");
+	return 0;
+}
+
+static unsigned int _sdc_set_block_size(unsigned int len)
+{
+    unsigned char args[4];
+    unsigned char sdcard_rsp;
+    register int i;
+
+    /*
+     * For now, supported block size is 512 bytes
+     */
+    if (len != 512) return 1;
+
+    /*
+     * When using high capacity SDCARD, the block_length is not a number of bytes
+     * but a number of blocks (transfer unit)
+     */
+    if (sdcard.sdhc)
+    {
+        sdcard.block_length = len / 512;
+        return 0;
+    }
+
+    for (i = 0; i < 4; i++)
+    {
+        args[i] = (len >> (32 - (i+1)*8)) & 0xFF;
+    }
+
+    _sdc_enable();
+
+    sdcard_rsp = _sdc_send_command(16, SDCARD_CMD, args, 0x00);
+    if ( SDCARD_CHECK_R1_ERROR(sdcard_rsp) )
+    {
+        _sdc_disable();
+        return sdcard_rsp;
+    }
+
+    _sdc_disable();
+
+    sdcard.block_length = len;
+
+	return 0;
+}
+
+unsigned int _sdc_init( unsigned int channel )
+{
+    spi = (struct spi_dev*) &seg_ioc_base;
+
+    /**
+     * Initializing the SPI controller
+     */
+    _spi_init (
+        spi           ,
+        200000        , /**< SPI_clk: 200 Khz */
+        SYSCLK_FREQ   , /**< Sys_clk          */
+        8             , /**< Charlen: 8       */
+        SPI_TX_NEGEDGE,
+        SPI_RX_POSEDGE
+    );
+
+    /**
+     * Initializing the SD Card
+     */
+    unsigned int iter = 0;
+    unsigned char sdcard_rsp;
+    unsigned int i;
+
+    while(1)
+    {
+        _puts("Trying to initialize SD card... ");
+
+        sdcard_rsp = _sdc_open( channel );
+        if (sdcard_rsp == 0)
+        {
+            _puts("OK\n");
+            break;
+        }
+
+        _puts("KO\n");
+
+        for (i = 0; i < 1000; i++);
+
+        if (++iter >= SDCARD_RESET_ITER_MAX)
+        {
+            _puts("\nERROR: During SD card reset to IDLE state\n"
+                 "/ card response = ");
+            _putx(sdcard_rsp);
+            _puts("\n");
+            _exit();
+        }
+    }
+
+    /**
+     * Set the block length of the SD Card
+     */
+    sdcard_rsp = _sdc_set_block_size(512);
+    if (sdcard_rsp)
+    {
+        _puts("ERROR: During SD card blocklen initialization\n");
+        _exit();
+    }
+
+    /**
+     * Incrementing SDCARD clock frequency for normal function
+     */
+    _spi_init (
+        spi         ,
+        10000000    , /**< SPI_clk 10 Mhz */
+        SYSCLK_FREQ , /**< Sys_clk        */
+        -1          , /**< Charlen: 8     */
+        -1          ,
+        -1
+    );
+
+    _puts("Finish block device initialization\n\r");
+
+    return 0;
+}
+
+
+///////////////////////////////////////////////////////////////////////////////
+//     _sdc_read()
+// Transfer data from the block device to a memory buffer. 
+// - mode     : BOOT / KERNEL / USER
+// - lba      : first block index on the block device
+// - buffer   : base address of the memory buffer (must be word aligned)
+// - count    : number of blocks to be transfered.
+// Returns 0 if success, > 0 if error.
+///////////////////////////////////////////////////////////////////////////////
+unsigned int _sdc_read( unsigned int mode,
+                        unsigned int lba,
+                        paddr_t      buffer,
+                        unsigned int count )
+{
+    unsigned char args[4];
+    unsigned char sdcard_rsp;
+    unsigned int i;
+    unsigned int curr = lba;
+    unsigned int last = lba + count;
+
+    for ( ; curr < last ; curr++ )
+    {
+        _sdc_lseek(curr);
+
+        for (i = 0; i < 4; i++)
+        {
+            args[i] = (sdcard.access_pointer >> (32 - (i+1)*8)) & 0xFF;
+        }
+
+        _sdc_enable();
+
+        sdcard_rsp = _sdc_send_command(17, SDCARD_CMD, args, 0x00);
+        if ( SDCARD_CHECK_R1_ERROR(sdcard_rsp) )
+        {
+            _sdc_disable();
+            return sdcard_rsp;
+        }
+
+        _sdc_wait_data_block();
+
+        if (spi_get_data(sdcard.spi, buffer, 512 ))
+        {
+            _sdc_disable();
+            return 1;
+        }
+
+        /*
+         * Get the CRC16 (comes at the end of the data block)
+         */
+        _sdc_receive_char(); // first byte
+        _sdc_receive_char(); // second byte
+
+        _sdc_disable();
+
+        buffer += 512;
+    }
+
+    return 0;
+}
+
+unsigned int _sdc_write( unsigned int mode,
+                         unsigned int lba,
+                         paddr_t      buffer,
+                         unsigned int count )
+{
+	return 0;
+}
+
+unsigned int _sdc_get_status( unsigned int channel ,
+                              unsigned int* status )
+{
+    return BLOCK_DEVICE_IDLE;
+}
+
+unsigned int _sdc_get_block_size()
+{
+    if (sdcard.sdhc) return sdcard.block_length*512;
+    else             return sdcard.block_length;
+}
+
+
+
+/*
+ * vim: tabstop=4 : shiftwidth=4 : expandtab : softtabstop=4
+ */
Index: branch/giet_vm_ioc_drivers/giet_drivers/sdc_driver.h
===================================================================
--- branch/giet_vm_ioc_drivers/giet_drivers/sdc_driver.h	(revision 283)
+++ branch/giet_vm_ioc_drivers/giet_drivers/sdc_driver.h	(revision 283)
@@ -0,0 +1,126 @@
+/**
+ * \file sdc_driver.h
+ * \date 30 August 2012
+ * \author Cesar fuguet <cesar.fuguet-tortolero@lip6.fr>
+ *
+ * This file defines the driver of a SD Card device using an SPI controller
+ */
+
+#ifndef SDC_DRIVER_H
+#define SDC_DRIVER_H
+
+#include <ioc_driver.h>
+#include <spi_driver.h>
+#include <mapping_info.h>
+
+/**
+ * \brief SD Card type definition
+ */
+struct sdcard_dev
+{ 
+    /** 
+     * SPI controller pointer 
+     */
+    struct spi_dev * spi;
+
+    /**
+     * Block length of the SDCARD
+     */
+    unsigned int block_length;
+
+    /**
+     * Access pointer representing the offset in bytes used
+     * to read or write in the SDCARD.
+     *
+     * \note this driver is for cards SDSD, therefore this offset
+     *       must be multiple of the block length
+     */ 
+    unsigned int access_pointer;
+
+    /**
+     * Slave ID. This ID represents the number of the slave select signal
+     * used in the hardware platform (SPI channel)
+     */
+    int    slave_id;
+
+    /* is the card high capacity ? */
+    int sdhc;
+};
+
+unsigned int _sdc_init( unsigned int channel );
+
+
+unsigned int _sdc_read( unsigned int mode,
+                        unsigned int lba,
+                        paddr_t      buffer,
+                        unsigned int count);
+
+
+unsigned int _sdc_write( unsigned int mode,
+                         unsigned int lba,
+                         paddr_t      buffer,
+                         unsigned int count);
+
+unsigned int _sdc_get_block_size();
+
+unsigned int _sdc_get_status( unsigned int channel ,
+                              unsigned int* status );
+
+
+/**
+ * SD Card constants
+ */
+
+/** Number of retries after an unacknowledge command */
+#define SDCARD_COMMAND_TIMEOUT      100
+
+/** This command is a simple SD commmand */
+#define SDCARD_CMD                  0
+
+/** This is an application specific command */
+#define SDCARD_ACMD                 1
+
+/** The transmition is done in the negative edge of the clock */
+#define SDCARD_TX_NEGEDGE           0
+
+/** The transmition is done in the positive edge of the clock */
+#define SDCARD_TX_POSEDGE           1
+
+/** The reception is done in the negative edge of the clock */
+#define SDCARD_RX_NEGEDGE           0
+
+/** The reception is done in the positive edge of the clock */
+#define SDCARD_RX_POSEDGE           1
+
+/**
+ * SD Card macros
+ */
+
+/** Check if the response is valid */
+#define SDCARD_CHECK_R1_VALID(x)    (~x & SDCARD_R1_RSP_VALID) ? 1 : 0
+
+/**
+ * Check if there is an error in the response
+ *
+ * \note this macro must be used after verify that the response is
+ *       valid
+ */
+#define SDCARD_CHECK_R1_ERROR(x)    ( x & 0x7E)                ? 1 : 0
+
+/**
+ * SD Card Response 1 (R1) format constants
+ */
+#define SDCARD_R1_IN_IDLE_STATE     ( 1 << 0 ) /**< \brief R1 bit 0 */
+#define SDCARD_R1_ERASE_RESET       ( 1 << 1 ) /**< \brief R1 bit 1 */
+#define SDCARD_R1_ILLEGAL_CMD       ( 1 << 2 ) /**< \brief R1 bit 2 */
+#define SDCARD_R1_COM_CRC_ERR       ( 1 << 3 ) /**< \brief R1 bit 3 */
+#define SDCARD_R1_ERASE_SEQ_ERR     ( 1 << 4 ) /**< \brief R1 bit 4 */
+#define SDCARD_R1_ADDRESS_ERR       ( 1 << 5 ) /**< \brief R1 bit 5 */
+#define SDCARD_R1_PARAMETER_ERR     ( 1 << 6 ) /**< \brief R1 bit 6 */
+#define SDCARD_R1_RSP_VALID         ( 1 << 7 ) /**< \brief R1 bit 7 */
+
+#endif
+
+/*
+ * vim: tabstop=4 : shiftwidth=4 : expandtab : softtabstop=4
+ */
Index: branch/giet_vm_ioc_drivers/giet_drivers/spi_driver.c
===================================================================
--- branch/giet_vm_ioc_drivers/giet_drivers/spi_driver.c	(revision 283)
+++ branch/giet_vm_ioc_drivers/giet_drivers/spi_driver.c	(revision 283)
@@ -0,0 +1,209 @@
+/**
+ * \file    spi.c
+ * \date    31 August 2012
+ * \author  Cesar Fuguet <cesar.fuguet-tortolero@lip6.fr>
+ */
+#include <spi_driver.h>
+#include <utils.h>
+
+/**
+ * \param   x: input value
+ *
+ * \return  byte-swapped value
+ *
+ * \brief   byte-swap a 32bit word
+ */
+static unsigned int bswap32(unsigned int x)
+{
+  unsigned int y;
+  y =  (x & 0x000000ff) << 24;
+  y |= (x & 0x0000ff00) <<  8;
+  y |= (x & 0x00ff0000) >>  8;
+  y |= (x & 0xff000000) >> 24;
+  return y;
+}
+
+/**
+ * \param   spi :   Initialized pointer to the SPI controller
+ *
+ * \brief   Wait until the SPI controller has finished a transfer
+ *
+ * Wait until the GO_BUSY bit of the SPI controller be deasserted
+ */
+static void _spi_wait_if_busy(struct spi_dev * spi)
+{
+    register int delay;
+
+    while(SPI_IS_BUSY(spi))
+    {
+        for (delay = 0; delay < 100; delay++);
+    }
+}
+
+/**
+ * \param   spi : Initialized pointer to the SPI controller
+ *
+ * \return  void
+ *
+ * \brief   Init transfer of the tx registers to the selected slaves
+ */
+static void _spi_init_transfer(struct spi_dev * spi)
+{
+    unsigned int spi_ctrl = ioread32(&spi->ctrl);
+
+    iowrite32(&spi->ctrl, spi_ctrl | SPI_CTRL_GO_BSY);
+}
+
+/**
+ * \param   spi_freq    : Desired frequency for the generated clock from the SPI
+ *                        controller
+ * \param   sys_freq    : System clock frequency
+ *
+ * \brief   Calculated the value for the divider register in order to obtain the SPI
+ *          desired clock frequency 
+ */
+static unsigned int _spi_calc_divider_value( unsigned int spi_freq ,
+                                             unsigned int sys_freq )
+{
+    return ((sys_freq / (spi_freq * 2)) - 1);
+}
+
+void spi_put_tx(struct spi_dev * spi, unsigned char byte, int index)
+{
+    _spi_wait_if_busy(spi);
+    {
+        iowrite8(&spi->rx_tx[index % 4], byte);
+        _spi_init_transfer(spi);
+    }
+    _spi_wait_if_busy(spi);
+}
+
+volatile unsigned char spi_get_rx(struct spi_dev * spi, int index)
+{
+    return ioread8(&spi->rx_tx[index % 4]);
+}
+
+unsigned int spi_get_data( struct spi_dev * spi,
+                           paddr_t buffer      ,
+                           unsigned int count  )
+{
+    unsigned int spi_ctrl0; // ctrl value before calling this function
+    unsigned int spi_ctrl;
+    int i;
+
+    /*
+     * Only reading of one block (512 bytes) are supported
+     */
+    if ( count != 512 ) return 1;
+
+    _spi_wait_if_busy(spi);
+
+    spi_ctrl0 = ioread32(&spi->ctrl);
+
+#if 0
+    /*
+     * Read data using SPI DMA mechanism
+     * Two restrictions:
+     *   1. Can transfer only one block (512 bytes).
+     *   2. The destination buffer must be aligned to SPI burst size (64 bytes)
+     */
+    if ((buffer & 0x3f) == 0)
+    {
+        _puts("spi_get_data(): Starting DMA transfer / count = ");
+        _putx(count);
+        _puts("\n");
+
+        _puts("spi_get_data(): buffer = ");
+        _putx(buffer);
+        _puts("\n");
+
+        spi->dma_base  = (buffer      ) & ((1 << 32) - 1); // 32 lsb
+        spi->dma_baseh = (buffer >> 32) & ((1 << 8 ) - 1); // 8  msb
+        spi->dma_count = count | SPI_DMA_COUNT_READ;
+
+        while ( (spi->dma_count >> 1) );
+
+        goto reset_ctrl;
+    }
+#endif
+
+    /*
+     * Read data without SPI DMA mechanism
+     *
+     * Switch to 128 bits words
+     */
+
+    spi_ctrl = (spi_ctrl0 & ~SPI_CTRL_CHAR_LEN_MASK) | 128;
+    iowrite32(&spi->ctrl, spi_ctrl);
+
+    /* 
+     * Read data.
+     * Four 32 bits words at each iteration (128 bits = 16 bytes)
+     */
+    for (i = 0; i < count/16; i++)
+    {
+        iowrite32(&spi->rx_tx[0], 0xffffffff);
+        iowrite32(&spi->rx_tx[1], 0xffffffff);
+        iowrite32(&spi->rx_tx[2], 0xffffffff);
+        iowrite32(&spi->rx_tx[3], 0xffffffff);
+        iowrite32(&spi->ctrl,  spi_ctrl | SPI_CTRL_GO_BSY);
+
+        _spi_wait_if_busy(spi);
+
+        _physical_write( buffer, bswap32(ioread32(&spi->rx_tx[3])) ); 
+        buffer += 4;
+        _physical_write( buffer, bswap32(ioread32(&spi->rx_tx[2])) ); 
+        buffer += 4;
+        _physical_write( buffer, bswap32(ioread32(&spi->rx_tx[1])) ); 
+        buffer += 4;
+        _physical_write( buffer, bswap32(ioread32(&spi->rx_tx[0])) ); 
+        buffer += 4;
+    }
+
+//reset_ctrl:
+
+    /* Switch back to original word size */
+    iowrite32(&spi->ctrl, spi_ctrl0);
+
+    return 0;
+}
+
+void spi_ss_assert(struct spi_dev * spi, int index)
+{
+    unsigned int spi_ss = ioread32(&spi->ss);
+
+    iowrite32(&spi->ss, spi_ss | (1 << index));
+}
+
+void spi_ss_deassert(struct spi_dev * spi, int index)
+{
+    unsigned int spi_ss = ioread32(&spi->ss);
+
+    iowrite32(&spi->ss, spi_ss & ~(1 << index));
+}
+
+void _spi_init ( struct spi_dev * spi,
+                 int spi_freq        ,
+                 int sys_freq        ,
+                 int char_len        ,
+                 int tx_edge         ,
+                 int rx_edge         )
+{
+    unsigned int spi_ctrl = ioread32(&spi->ctrl);
+
+    if      ( tx_edge == 0 ) spi_ctrl |=  SPI_CTRL_TXN_EN;
+    else if ( tx_edge == 1 ) spi_ctrl &= ~SPI_CTRL_TXN_EN;
+    if      ( rx_edge == 0 ) spi_ctrl |=  SPI_CTRL_RXN_EN;
+    else if ( rx_edge == 1 ) spi_ctrl &= ~SPI_CTRL_RXN_EN;
+    if      ( char_len > 0 ) spi_ctrl  = (spi_ctrl & ~SPI_CTRL_CHAR_LEN_MASK) |
+                                         (char_len &  SPI_CTRL_CHAR_LEN_MASK);
+
+    iowrite32(&spi->ctrl, spi_ctrl);
+
+    if (spi_freq > 0 && sys_freq > 0)
+        iowrite32(&spi->divider, _spi_calc_divider_value(spi_freq, sys_freq));
+}
+
+/*
+ * vim: tabstop=4 : shiftwidth=4 : expandtab : softtabstop=4
+ */
Index: branch/giet_vm_ioc_drivers/giet_drivers/spi_driver.h
===================================================================
--- branch/giet_vm_ioc_drivers/giet_drivers/spi_driver.h	(revision 283)
+++ branch/giet_vm_ioc_drivers/giet_drivers/spi_driver.h	(revision 283)
@@ -0,0 +1,155 @@
+/**
+ * \file  : spi_driver.h
+ * \date  : 30 August 2012
+ * \author: Cesar Fuguet <cesar.fuguet-tortolero@lip6.fr>
+ *
+ * This file contains the definition of a driver for the SPI controller
+ */
+
+#ifndef SPI_DRIVER_H
+#define SPI_DRIVER_H
+
+#include <io.h>
+#include <mapping_info.h>
+
+/**
+ * SPI type definition
+ */
+struct spi_dev
+{
+    /**
+     * RX/TX registers of the SPI controller 
+     */
+    unsigned int rx_tx[4];
+
+    /**
+     * Control register of the SPI controller
+     */
+    unsigned int ctrl;
+
+    /**
+     * Divider register for the SPI controller generated clock signal
+     */
+    unsigned int divider;
+
+    /**
+     * Slave select register of the SPI controller
+     */
+    unsigned int ss;
+    unsigned int dma_base;
+    unsigned int dma_baseh;
+    unsigned int dma_count;
+};
+
+/**
+ * \param   spi     : initialized pointer to a SPI controller.
+ * \param   byte    : Byte to send to the SPI controller
+ * \param   index   : index of the TX register in the SPI (TX[index])
+ *
+ * \return  void
+ *
+ * \brief   Send a byte to one of the tx buffer registers of the
+ *          SPI controller
+ */
+void spi_put_tx(struct spi_dev * spi, unsigned char byte, int index);
+
+/**
+ * \param   spi     : initialized pointer to a SPI controller.
+ * \param   index   : index of the RX register in the SPI (RX[index])
+ *
+ * \return  byte from the RX[index] register
+ *
+ * \brief   Get a byte from one of the rx buffer registers of the
+ *          SPI controller
+ */
+inline volatile unsigned char spi_get_rx(struct spi_dev * spi, int index);
+
+/**
+ * \param   spi     : initialized pointer to a SPI controller.
+ * \param   buf     : buffer to store data read
+ * \param   count   : byte count to read
+ *
+ * \return  void
+ *
+ * \brief   get a data block from the SPI controller using 128bits
+ *          reads if possible
+ */
+unsigned int spi_get_data(struct spi_dev * spi, paddr_t buffer, unsigned int count);
+
+/**
+ * \param   spi     : initialized pointer to a SPI controller.
+ * \param   index   : index of the slave select signal to assert
+ *
+ * \return  void
+ *
+ * \brief   Set the index selected slave select signal (ss[index] <= '0')
+ */
+inline void spi_ss_assert(struct spi_dev * spi, int index);
+
+/**
+ * \param   spi     : initialized pointer to a SPI controller.
+ * \param   index   : index of the slave select signal to deassert
+ *
+ * \return  void
+ *
+ * \brief   Unset the index selected slave select signal (ss[index] <= '0')
+ */
+inline void spi_ss_deassert(struct spi_dev * spi, int index);
+
+/**
+ * \param   spi         : initialized pointer to a SPI controller.
+ * \param   spi_freq    : SPI Master to Slave clock frequency (in Hz)
+ * \param   sys_freq    : System clock frequency (in Hz)
+ * \param   char_len    : number to bits to transmit in one transfer
+ * \param   tx_edge     : when 0, the Master Out Slave In signal is changed
+ *                        on the falling edge of the clock
+ * \param   rx_edge     : when 0, the Master In Slave Out signal is latched
+ *                        on the falling edge of the clock
+ *
+ * \return  void
+ *
+ * \brief   Configure the SPI controller
+ * \note    Any of the arguments can be less than 0 if you want to keep the old value
+ */
+void _spi_init (
+        struct spi_dev * spi,
+        int spi_freq        ,
+        int sys_freq        ,
+        int char_len        ,
+        int tx_edge         ,
+        int rx_edge         );
+
+/**
+ * SPI macros and constants
+ */
+#define SPI_TX_POSEDGE         1           /**< MOSI is changed on neg edge   */
+#define SPI_TX_NEGEDGE         0           /**< MOSI is changed on pos edge   */
+#define SPI_RX_POSEDGE         1           /**< MISO is latched on pos edge   */
+#define SPI_RX_NEGEDGE         0           /**< MISO is latched on neg edge   */
+
+#define SPI_CTRL_ASS_EN        ( 1 << 13 ) /**< Auto Slave Sel Assertion      */
+#define SPI_CTRL_IE_EN         ( 1 << 12 ) /**< Interrupt Enable              */
+#define SPI_CTRL_LSB_EN        ( 1 << 11 ) /**< LSB are sent first            */
+#define SPI_CTRL_TXN_EN        ( 1 << 10 ) /**< MOSI is changed on neg edge   */
+#define SPI_CTRL_RXN_EN        ( 1 << 9  ) /**< MISO is latched on neg edge   */
+#define SPI_CTRL_GO_BSY        ( 1 << 8  ) /**< Start the transfer            */
+#define SPI_CTRL_DMA_BSY        (1 << 16)  /***   DMA in progress             */
+#define SPI_CTRL_CHAR_LEN_MASK (  0xFF   ) /**< Bits transmited in 1 transfer */
+#define SPI_RXTX_MASK          (  0xFF   ) /**< Mask for the an RX/TX value   */
+
+#define SPI_DMA_COUNT_READ      (1 << 0) /* operation is a read (else write) */
+
+/** 
+ * \param  x : Initialized pointer to the SPI controller
+ *
+ * \return 1 if there is an unfinished transfer in the SPI controller
+ *
+ * \brief  Check the GO_BUSY bit of the SPI Controller
+ */
+#define SPI_IS_BUSY(x)         ((ioread32(&x->ctrl) & (SPI_CTRL_GO_BSY|SPI_CTRL_DMA_BSY)) != 0) ? 1 : 0
+
+#endif
+
+/*
+ * vim: tabstop=4 : shiftwidth=4 : expandtab : softtabstop=4
+ */
