Index: soft/giet_vm/giet_common/utils.h
===================================================================
--- soft/giet_vm/giet_common/utils.h	(revision 399)
+++ soft/giet_vm/giet_common/utils.h	(revision 408)
@@ -45,33 +45,111 @@
 
 ///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////////////
 //     CP0 registers access functions
 ///////////////////////////////////////////////////////////////////////////////////
-
+///////////////////////////////////////////////////////////////////////////////////
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_SCHED register content
+// (virtual base address of the processor scheduler)
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_sched(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_EPC register content.
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_epc(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_BVAR register content.
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_bvar(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_CR register content.
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_cr(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_SR register content.
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_sr(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_PROCID register content.
+// Processor identifier (12 bits)
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_procid(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP0_TIME register content.
+// Processor local time (32 bits)
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_proctime(void);
 
+///////////////////////////////////////////////////////////////////////////////////
+// Save CP0_SR value to variable pointed by save_sr_ptr and disable IRQs.
+///////////////////////////////////////////////////////////////////////////////////
 extern void         _it_disable( unsigned int* save_sr_ptr );
+
+///////////////////////////////////////////////////////////////////////////////////
+// Restore CP0_SR register from variable pointed by save_sr_ptr.
+///////////////////////////////////////////////////////////////////////////////////
 extern void         _it_restore( unsigned int* save_sr_ptr );
 
+///////////////////////////////////////////////////////////////////////////////////
+// Set a new value in CP0_SCHED register.
+// (virtual base address of the processor scheduler)
+///////////////////////////////////////////////////////////////////////////////////
 extern void         _set_sched(unsigned int value);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Set a new value in CP0_SR register.
+///////////////////////////////////////////////////////////////////////////////////
 extern void         _set_sr(unsigned int value);
 
+
+///////////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////////////////////////////////////////////////////////
 //     CP2 registers access functions
 ///////////////////////////////////////////////////////////////////////////////////
-
+///////////////////////////////////////////////////////////////////////////////////
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP2_PTPR register value.
+// Page table physical base address for the running context.
+// Contains only the 27 MSB bits, right justified.
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_mmu_ptpr(void);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Returns CP2_MODE register value.
+// MMU current mode, defined by 4 bits, right justified: ITLB/DTLB/ICACHE/DCACHE
+///////////////////////////////////////////////////////////////////////////////////
 extern unsigned int _get_mmu_mode(void);
 
+///////////////////////////////////////////////////////////////////////////////////
+// Set a new value in CP2_PTPR register.
+///////////////////////////////////////////////////////////////////////////////////
 extern void         _set_mmu_ptpr(unsigned int value);
+
+///////////////////////////////////////////////////////////////////////////////////
+// Set a new value in CP2_MODE register.
+///////////////////////////////////////////////////////////////////////////////////
 extern void         _set_mmu_mode(unsigned int value);
 
 ///////////////////////////////////////////////////////////////////////////////////
+// Set a value in  CP2_DCACHE_INVAL register.
+// It invalidates the data cache line, if the virtual address defined by the 
+// value argument hit in DCACHE.
+///////////////////////////////////////////////////////////////////////////////////
+extern void         _set_mmu_dcache_inval(unsigned int value);
+
+
+
+///////////////////////////////////////////////////////////////////////////////////
+///////////////////////////////////////////////////////////////////////////////////
 //     Physical addressing related functions
+///////////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////////////////////////////////////////////////////////
 
@@ -163,6 +241,6 @@
                              char*        source );
 
-extern void         _dcache_buf_invalidate( void * buffer, 
-                                            unsigned int size );
+extern void         _dcache_buf_invalidate( unsigned int buf_vbase, 
+                                            unsigned int buf_size );
 
 extern unsigned int _heap_info( unsigned int* vaddr,
