diff --git a/alliance/src/mocha/src/mocha_check.c b/alliance/src/mocha/src/mocha_check.c
index b2dfa226..421634e4 100644
--- a/alliance/src/mocha/src/mocha_check.c
+++ b/alliance/src/mocha/src/mocha_check.c
@@ -391,6 +391,50 @@ static void MochaCheckComputeReachableStates( MochaFigure )
   addbddcircuitout( (bddcircuit *)0, "reached", BddReachedSet );
   testbddcircuit( (bddcircuit *)0 );
 # endif
+  fprintf( stdout, "First state " );
+  MochaCheckViewBddNode( MochaFigure->BDD_FIRST_STATE );
+  fprintf( stdout, "Reachable states " );
+  MochaCheckViewBddNode( BddReachedSet );
+}
+
+/*------------------------------------------------------------\
+|                                                             |
+|                    MochaCheckCtlBddEX                       |
+|                                                             |
+\------------------------------------------------------------*/
+
+static bddnode *MochaCheckCtlBddEX( BddNode )
+
+  bddnode *BddNode;
+{
+  bddnode      *BddNew;
+  bddnode      *BddReached; 
+  bddnode      *BddAssume;
+  btrtransfunc *BtrTransFunc;
+  bddassoc     *BddAssoc;
+
+  BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
+  BddAssoc     = MochaMochaFigure->BDD_ASSOC_REG;
+  BddReached   = MochaMochaFigure->BDD_REACHED_STATE;
+  BddAssume    = MochaMochaFigure->BDD_ASSUME;
+
+  BddNew = preimagebtrtransfunc( BtrTransFunc, BddNode );
+
+  BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+                         decbddrefext( BddNew ), BddAssume );
+
+  BddNew = existbddnodemissassoc( (bddsystem *)0,
+                                   decbddrefext( BddNew ), BddAssoc );
+
+  BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
+                           decbddrefext( BddNew ), BddReached );
+
+# if 1
+  fprintf( stdout, "MochaCheckCtlBddEX  -> " );
+  MochaCheckViewBddNode( BddNew );
+# endif
+
+  return( BddNew );
 }
 
 /*------------------------------------------------------------\
@@ -405,7 +449,6 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
 {
   bddnode      *BddOld;
   bddnode      *BddNew;
-  bddnode      *BddPred;
   bddnode      *BddReached; 
   bddnode      *BddAssume;
   btrtransfunc *BtrTransFunc;
@@ -418,89 +461,39 @@ static bddnode *MochaCheckCtlBddEG( BddNode )
   BddOld       = BddLocalSystem->ONE;
   BddNew       = incbddrefext( BddNode );
 
-# ifdef DEBUG
   fprintf( stdout, "> MochaCheckCtlBddEG\n" );
   fprintf( stdout, "EG:\n" );
   MochaCheckViewBddNode( BddNode );
+# ifdef DEBUG
   fprintf( stdout, "REACHED:\n" );
   MochaCheckViewBddNode( BddReached );
 # endif
 
   while ( BddNew != BddOld )
   {
-    BddOld  = BddNew;
-    BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld );
-    BddPred = applybddnode( (bddsystem *)0, ABL_AND,
-                            decbddrefext( BddPred ), BddAssume );
+    BddOld = BddNew;
 
-    BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
-                             decbddrefext( BddPred ), BddNode );
+    BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld );
 
-    BddNew  = existbddnodemissassoc( (bddsystem *)0,
-                                     decbddrefext( BddNew ), BddAssoc );
+    BddNew = applybddnode( (bddsystem *)0, ABL_AND, 
+                           decbddrefext( BddNew ), BddAssume );
 
-    BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
+    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+                            decbddrefext( BddNew ), BddNode );
+
+    BddNew = existbddnodemissassoc( (bddsystem *)0,
+                                    decbddrefext( BddNew ), BddAssoc );
+
+    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
                             decbddrefext( BddNew ), BddReached );
 
-# if DEBUG
-    fprintf( stdout, "NEW:\n" );
+    fprintf( stdout, "MochaCheckCtlBddEG:\n" );
     MochaCheckViewBddNode( BddNew );
-# endif
 
     decbddrefext( BddOld );
   }
 
-# ifdef DEBUG
   fprintf( stdout, "< MochaCheckCtlBddEG\n" );
-# endif
-
-  return( BddNew );
-}
-
-/*------------------------------------------------------------\
-|                                                             |
-|                    MochaCheckCtlBddEX                       |
-|                                                             |
-\------------------------------------------------------------*/
-
-static bddnode *MochaCheckCtlBddEX( BddNode )
-
-  bddnode *BddNode;
-{
-  bddnode      *BddOld;
-  bddnode      *BddNew;
-  bddnode      *BddPred;
-  bddnode      *BddReached; 
-  bddnode      *BddAssume;
-  btrtransfunc *BtrTransFunc;
-  bddassoc     *BddAssoc;
-
-  BtrTransFunc = MochaMochaFigure->BTR_TRANS_FUNC;
-  BddAssoc     = MochaMochaFigure->BDD_ASSOC_REG;
-  BddReached   = MochaMochaFigure->BDD_REACHED_STATE;
-  BddAssume    = MochaMochaFigure->BDD_ASSUME;
-  BddOld       = BddLocalSystem->ONE;
-  BddNew       = incbddrefext( BddReached );
-
-  do
-  {
-    BddOld  = BddNew;
-    BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld );
-    BddPred = applybddnode( (bddsystem *)0, ABL_AND,
-                            decbddrefext( BddPred ), BddAssume );
-
-    BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
-                             decbddrefext( BddPred ), BddNode );
-
-    BddNew  = existbddnodemissassoc( (bddsystem *)0,
-                                     decbddrefext( BddNew ), BddAssoc );
-
-    BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
-                            decbddrefext( BddNew ), BddReached );
-
-    decbddrefext( BddOld );
-  }
-  while ( BddNew != BddOld );
 
   return( BddNew );
 }
@@ -518,7 +511,6 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
 {
   bddnode      *BddOld;
   bddnode      *BddNew;
-  bddnode      *BddPred;
   bddnode      *BddReached; 
   bddnode      *BddAssume;
   btrtransfunc *BtrTransFunc;
@@ -533,23 +525,28 @@ static bddnode *MochaCheckCtlBddEU( BddNodeP, BddNodeQ )
 
   while ( BddNew != BddOld )
   {
-    BddOld  = BddNew;
-    BddPred = preimagebtrtransfunc( BtrTransFunc, BddOld );
-    BddPred = applybddnode( (bddsystem *)0, ABL_AND,
-                            decbddrefext( BddPred ), BddAssume );
+    BddOld = BddNew;
 
-    BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
-                             decbddrefext( BddPred ), BddNodeP );
+    BddNew = preimagebtrtransfunc( BtrTransFunc, BddOld );
+
+    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+                            decbddrefext( BddNew ), BddAssume );
+
+    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
+                            decbddrefext( BddNew ), BddNodeP );
 
     BddNew  = applybddnode( (bddsystem *)0, ABL_OR,
                             decbddrefext( BddNew ), BddNodeQ );
 
-    BddNew  = existbddnodemissassoc( (bddsystem *)0,
+    BddNew = existbddnodemissassoc( (bddsystem *)0,
                                      decbddrefext( BddNew ), BddAssoc );
 
-    BddNew  = applybddnode( (bddsystem *)0, ABL_AND,
+    BddNew = applybddnode( (bddsystem *)0, ABL_AND,
                             decbddrefext( BddNew ), BddReached );
 
+    fprintf( stdout, "MochaCheckCtlBddEU:\n" );
+    MochaCheckViewBddNode( BddNew );
+
     decbddrefext( BddOld );
   }
 
@@ -808,8 +805,10 @@ static bddnode *MochaCheckCtlAblEG( Expr )
   bddnode *BddNode;
   bddnode *BddResult;
 
+# ifdef DEBUG
   fprintf( stdout, "MochaCheckCtlAblEG: " );
   viewablexprln( Expr, ABL_VIEW_VHDL );
+# endif
 
   Expr = ABL_CDR( Expr );
 
@@ -933,9 +932,10 @@ static bddnode *MochaCheckCtlAbl( Expr )
 |                                                             |
 \------------------------------------------------------------*/
 
-static void MochaCheckCtlFormulae( MochaFigure )
+static void MochaCheckCtlFormulae( MochaFigure, FlagVerbose )
 
   mochafig_list *MochaFigure;
+  int            FlagVerbose;
 {
   ctlfig_list  *CtlFigure;
   ctlform_list *CtlForm;
@@ -959,17 +959,22 @@ static void MochaCheckCtlFormulae( MochaFigure )
 
   MochaMochaFigure = MochaFigure;
 
+# ifdef DEBUG
   fprintf( stdout, "Reachable states:\n" );
   MochaCheckViewBddNode( BddReached );
 
   fprintf( stdout, "First state:\n" );
   MochaCheckViewBddNode( BddFirst );
+# endif
 
   for ( CtlForm  = CtlFigure->FORM;
         CtlForm != (ctlform_list *)0;
         CtlForm  = CtlForm->NEXT )
   {
-    fprintf( stdout, "Verify formula %s\n", CtlForm->NAME );
+    if ( FlagVerbose )
+    {
+      fprintf( stdout, "\t    Verifying formula %s\n", CtlForm->NAME );
+    }
 
     BiAblArray = MOCHA_CTL_BIABLA( CtlForm );
     AblArray   = BiAblArray->EXPR;
@@ -989,11 +994,19 @@ static void MochaCheckCtlFormulae( MochaFigure )
 
     decbddrefext( BddNode );
 
+# ifdef DEBUG
     MochaCheckViewBddNode( BddNode );
+# endif
 
     if ( BddNode != BddFirst  )
     {
-      fprintf( stdout, " formula not verified !\n" );
+      fprintf( stdout, "\t    Formula %s IS FALSE !\n", CtlForm->NAME );
+      MochaCheckViewBddNode( BddNode );
+    }
+    else
+    if ( FlagVerbose )
+    {
+      fprintf( stdout, "\t    OK\n" );
     }
   }
 }
@@ -1012,7 +1025,7 @@ int MochaCheckModel( MochaFigure, FlagVerbose )
   MochaCheckBuildTransFunc( MochaFigure );
   MochaCheckComputeFirstState( MochaFigure );
   MochaCheckComputeReachableStates( MochaFigure );
-  MochaCheckCtlFormulae( MochaFigure );
-  /* TO BE DONE */
+  MochaCheckCtlFormulae( MochaFigure, FlagVerbose );
+
   return( 0 );
 }
diff --git a/alliance/src/mocha/src/mocha_fsm.c b/alliance/src/mocha/src/mocha_fsm.c
index b55c1dc4..4de148e1 100644
--- a/alliance/src/mocha/src/mocha_fsm.c
+++ b/alliance/src/mocha/src/mocha_fsm.c
@@ -118,24 +118,8 @@ void MochaCompileFsm( MochaFigure, FileName, FlagVerbose )
   {
     if ( IsFsmFigMixedRtl( FsmFigure ) )
     {
-      fprintf( stdout, "\t\t--> Mixed DataFlow / Fsm\n\n" );
+      fprintf( stdout, "\t\tMixed DataFlow / Fsm\n\n" );
     }
-
-    for ( ScanChain  = FsmFigure->MULTI;
-          ScanChain != (chain_list *)0;
-          ScanChain  = ScanChain->NEXT )
-    {
-      ScanFigure = (fsmfig_list *)ScanChain->DATA;
-
-      fprintf( stdout, "\t\t--> Name    : %s\n" , ScanFigure->NAME         );
-      fprintf( stdout, "\t\t--> States  : %ld\n", ScanFigure->NUMBER_STATE );
-      fprintf( stdout, "\t\t--> Inputs  : %ld\n", ScanFigure->NUMBER_IN    );
-      fprintf( stdout, "\t\t--> Outputs : %ld\n", ScanFigure->NUMBER_OUT   );
-      fprintf( stdout, "\t\t--> Edges   : %ld\n", ScanFigure->NUMBER_TRANS );
-      fprintf( stdout, "\n" );
-    }
-
-    fprintf( stdout, "\t\t--> Encode FSM figure\n" );
   }
 
   for ( ScanChain  = FsmFigure->MULTI;
@@ -143,6 +127,12 @@ void MochaCompileFsm( MochaFigure, FileName, FlagVerbose )
         ScanChain  = ScanChain->NEXT )
   {
     ScanFigure = (fsmfig_list *)ScanChain->DATA;
+
+    if ( FlagVerbose )
+    {
+      fprintf( stdout, "\t    --> Encoding FSM figure %s\n", ScanFigure->NAME );
+    }
+
     MochaSyfFsmEncode( ScanFigure, FlagVerbose );
   }
 
diff --git a/alliance/src/mocha/src/mocha_syf.c b/alliance/src/mocha/src/mocha_syf.c
index 3a9515ce..9938e7f6 100644
--- a/alliance/src/mocha/src/mocha_syf.c
+++ b/alliance/src/mocha/src/mocha_syf.c
@@ -478,6 +478,7 @@ void MochaSyfFsmEncode( FsmFigure, FlagVerbose )
 
   NumberState = FsmFigure->NUMBER_STATE;
   NumberBit   = MochaSyfGetNumberBit( NumberState - 1 );
+
   CodeMax     = ( 1 << NumberBit );
 
   CodeArray = (mochasyfcode *)autallocblock( sizeof( mochasyfcode ) * CodeMax );
@@ -498,7 +499,10 @@ void MochaSyfFsmEncode( FsmFigure, FlagVerbose )
   {
     MOCHA_SYF_STATE( ScanState )->CODE = &CodeArray[ NumberState - Index - 1 ];
 
-    CodeArray[ Index ].USED  = 1;
+    CodeArray[ NumberState - Index - 1 ].USED  = 1;
+
+    fprintf( stdout, "ScanState %s Code %ld\n",
+            ScanState->NAME, CodeArray[ NumberState - Index - 1 ].VALUE );
 
     ScanState = ScanState->NEXT;
     Index     = Index + 1;