Version abc90321

13 files changed, 932 insertions, 97 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 17600b4c..4af268ff 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3651,14 +3651,6 @@ SOURCE=.\src\aig\gia\giaCof.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\gia\giaCSat0.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\gia\giaCSat2.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\gia\giaDfs.c
 # End Source File
 # Begin Source File
@@ -3711,6 +3703,10 @@ SOURCE=.\src\aig\gia\giaMap.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaRetime.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaScl.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index e9bad08e..94797210 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -44,10 +44,10 @@ static inline int  Aig_XsimInv( int Value )
 }
 static inline int  Aig_XsimAnd( int Value0, int Value1 )   
 { 
-    if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
-        return AIG_XVSX;
     if ( Value0 == AIG_XVS0 || Value1 == AIG_XVS0 )
         return AIG_XVS0;
+    if ( Value0 == AIG_XVSX || Value1 == AIG_XVSX )
+        return AIG_XVSX;
     assert( Value0 == AIG_XVS1 && Value1 == AIG_XVS1 );
     return AIG_XVS1;
 }
@@ -347,7 +347,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     Vec_Ptr_t * vMap;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     unsigned * pState;//, * pPrev;
-    int i, f, fConstants, Value, nCounter;
+    int i, f, fConstants, Value, nCounter, nRetired;
     // allocate the simulation manager
     pTsi = Aig_TsiStart( p );
     // initialize the values
@@ -383,11 +383,17 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
         Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
         // simulate internal nodes
         Aig_ManForEachNode( p, pObj, i )
+        {
             Aig_ObjSetXsim( pObj, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
+//            printf( "%d %d    Id = %2d.  Value = %d.\n", 
+//                Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj),
+//                i, Aig_XsimAnd(Aig_ObjGetXsimFanin0(pObj), Aig_ObjGetXsimFanin1(pObj)) );
+        }
         // transfer the latch values
         Aig_ManForEachLiSeq( p, pObj, i )
             Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
         nCounter = 0;
+        nRetired = 0;
         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
         {
             if ( f < TSI_ONE_SERIES )
@@ -395,10 +401,16 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
             else
             {
                 if ( Aig_ObjGetXsim(pObjLi) != Aig_ObjGetXsim(pObjLo) )
+                {
                     Aig_ObjSetXsim( pObjLo, AIG_XVSX );
+                    nRetired++;
+                }
             }
             nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
         }
+//        if ( nRetired )
+//        printf( "Retired %d registers.\n", nRetired );
+
 //        if ( f && (f % 1000 == 0) )
 //            printf( "%d \n", f );
 //printf( "%d  ", nCounter );
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e3b3f014..28d610e9 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -116,6 +116,7 @@ struct Gia_Man_t_
     int *          pMapping;      // mapping for each node
     Gia_Cex_t *    pCexComb;      // combinational counter-example
     int *          pCopies;       // intermediate copies
+    Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
 };
 
 
@@ -123,15 +124,15 @@ struct Gia_Man_t_
 typedef struct Emb_Par_t_ Emb_Par_t;
 struct Emb_Par_t_
 {
-    int            nDims;            // the number of dimension
-    int            nSols;            // the number of solutions (typically, 2)
-    int            nIters;           // the number of iterations of FORCE
-    int            fRefine;          // use refinement by FORCE
-    int            fCluster;         // use clustered representation 
-    int            fDump;            // dump Gnuplot file
-    int            fDumpLarge;       // dump Gnuplot file for large benchmarks
-    int            fShowImage;       // shows image if Gnuplot is installed
-    int            fVerbose;         // verbose flag  
+    int            nDims;         // the number of dimension
+    int            nSols;         // the number of solutions (typically, 2)
+    int            nIters;        // the number of iterations of FORCE
+    int            fRefine;       // use refinement by FORCE
+    int            fCluster;      // use clustered representation 
+    int            fDump;         // dump Gnuplot file
+    int            fDumpLarge;    // dump Gnuplot file for large benchmarks
+    int            fShowImage;    // shows image if Gnuplot is installed
+    int            fVerbose;      // verbose flag  
 };
 
 
@@ -139,9 +140,9 @@ struct Emb_Par_t_
 typedef struct Gia_ParFra_t_ Gia_ParFra_t;
 struct Gia_ParFra_t_
 {
-    int            nFrames;      // the number of frames to unroll
-    int            fInit;        // initialize the timeframes
-    int            fVerbose;     // enables verbose output
+    int            nFrames;       // the number of frames to unroll
+    int            fInit;         // initialize the timeframes
+    int            fVerbose;      // enables verbose output
 };
 
 
@@ -151,11 +152,11 @@ typedef struct Gia_ParSim_t_ Gia_ParSim_t;
 struct Gia_ParSim_t_
 {
     // user-controlled parameters
-    int            nWords;       // the number of machine words
-    int            nIters;       // the number of timeframes
-    int            TimeLimit;    // time limit in seconds
-    int            fCheckMiter;  // check if miter outputs are non-zero
-    int            fVerbose;     // enables verbose output
+    int            nWords;        // the number of machine words
+    int            nIters;        // the number of timeframes
+    int            TimeLimit;     // time limit in seconds
+    int            fCheckMiter;   // check if miter outputs are non-zero
+    int            fVerbose;      // enables verbose output
 };
 
 extern void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p );
@@ -456,6 +457,7 @@ extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNo
 /*=== giaDup.c ============================================================*/
 extern Gia_Man_t *         Gia_ManDup( Gia_Man_t * p );  
 extern Gia_Man_t *         Gia_ManDupSelf( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
@@ -472,6 +474,7 @@ extern Gia_Man_t *         Gia_ManTransformMiter( Gia_Man_t * p );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
+extern Gia_Man_t *         Gia_ManRemoveEnables( Gia_Man_t * p );
 /*=== giaEquiv.c ==========================================================*/
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
@@ -515,8 +518,11 @@ extern void                Gia_ManPrintStats( Gia_Man_t * p );
 extern void                Gia_ManPrintStatsShort( Gia_Man_t * p ); 
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
+extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
 /*=== giaMap.c ===========================================================*/
 extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
+/*=== giaRetime.c ===========================================================*/
+extern Gia_Man_t *         Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose );
 /*=== giaSat.c ============================================================*/
 extern int                 Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int nConfsMax );
 /*=== giaScl.c ============================================================*/
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 3f707e1c..1c341d6f 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -194,12 +194,19 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p )
 //        if ( Aig_ObjRefs(pObj) == 0 )
             ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
     }
+
     // add logic for the POs
     Gia_ManForEachCo( p, pObj, i )
     {
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
     }
+/*
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
+    Gia_ManForEachCo( p, pObj, i )
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+*/
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     ABC_FREE( ppNodes );
     return pNew;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 5fb801a7..0c536dab 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -101,6 +101,50 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates while adding self-loops to the registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
+{
+    Gia_Man_t * pNew; 
+    Gia_Obj_t * pObj;
+    int i, Counter1 = 0, Counter2 = 0;
+    assert( p->vFlopClasses != NULL );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( Vec_IntEntry(p->vFlopClasses, i) != iClass )
+            pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( Vec_IntEntry(p->vFlopClasses, i) == iClass )
+            pObj->Value = Gia_ManAppendCi( pNew ), Counter1++;
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachRi( p, pObj, i )
+        if ( Vec_IntEntry(p->vFlopClasses, i) != iClass )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachRi( p, pObj, i )
+        if ( Vec_IntEntry(p->vFlopClasses, i) == iClass )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ), Counter2++;
+    assert( Counter1 == Counter2 );
+    Gia_ManSetRegNum( pNew, Counter1 );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG without any changes.]
 
   Description []
@@ -132,6 +176,8 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
         }
         else if ( Gia_ObjIsCo(pObj) )
         {
+            Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
+
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
             nRis += Gia_ObjIsRi(p, pObj);
         }
@@ -552,7 +598,10 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
     else
     {
         Gia_ManForEachCo( p, pObj, i )
-            Gia_ManDupDfs_rec( pNew, p, pObj );
+        {
+            Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin0(pObj) );
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        }
     }
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index f80bc885..13d6145c 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -415,7 +415,225 @@ Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, i
     Vec_IntFree( vCofSigs );
     Gia_ManStop( pAig );
     return pNew;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transform seq circuits with enables by removing enables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pAux; 
+    Gia_Obj_t * pTemp, * pObjC, * pObj0, * pObj1, * pFlopIn, * pFlopOut;
+    Gia_Obj_t * pThis, * pNode;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pThis, i )
+        pThis->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pThis, i )
+        pThis->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pThis), Gia_ObjFanin1Copy(pThis) );
+    Gia_ManForEachPo( p, pThis, i )
+        pThis->Value = Gia_ObjFanin0Copy(pThis);
+    Gia_ManForEachRi( p, pFlopIn, i )
+    {
+        pNode = Gia_ObjFanin0(pFlopIn);
+        if ( !Gia_ObjIsMuxType(pNode) )
+        {
+            printf( "Cannot recognize enable of flop %d.\n", i );
+            continue;
+        }
+        pObjC = Gia_ObjRecognizeMux( pNode, &pObj1, &pObj0 );
+        pFlopOut = Gia_ObjRiToRo( p, pFlopIn );
+        if ( Gia_Regular(pObj0) != pFlopOut && Gia_Regular(pObj1) != pFlopOut )
+        {
+            printf( "Cannot recognize self-loop of enable flop %d.\n", i );
+            continue;
+        }
+        if ( !Gia_ObjFaninC0(pFlopIn) )
+        {
+            pObj0 = Gia_Not(pObj0);
+            pObj1 = Gia_Not(pObj1);
+        }
+        if ( Gia_IsComplement(pObjC) )
+        {
+            pObjC = Gia_Not(pObjC);
+            pTemp = pObj0;
+            pObj0 = pObj1;
+            pObj1 = pTemp;
+        }
+        if ( Gia_Regular(pObj0) == pFlopOut )
+        {
+//            printf( "FlopIn compl = %d. FlopOut is d0. Complement = %d.\n", 
+//                Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj0) );
+            pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1));
+        }
+        else if ( Gia_Regular(pObj1) == pFlopOut )
+        {
+//            printf( "FlopIn compl = %d. FlopOut is d1. Complement = %d.\n", 
+//                Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj1) );
+            pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0));
+        }
+    }
+    Gia_ManForEachCo( p, pThis, i )
+        Gia_ManAppendCo( pNew, pThis->Value );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pAux = pNew );
+    Gia_ManStop( pAux );
+    return pNew;
+}
+
+/**Function*************************************************************
 
+  Synopsis    [Transform seq circuits with enables by removing enables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
+{
+    Vec_Ptr_t * vCtrls, * vDatas;
+    Vec_Int_t * vFlopClasses;
+    Gia_Man_t * pNew, * pAux; 
+    Gia_Obj_t * pFlopIn, * pFlopOut, * pDriver, * pFan0, * pFan1, * pCtrl, * pData, * pObj;
+    int i, iClass, fCompl, Counter = 0;
+    vCtrls = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( vCtrls, NULL );
+    vDatas = Vec_PtrAlloc( Gia_ManRegNum(p) );
+    vFlopClasses = Vec_IntAlloc( Gia_ManRegNum(p) );
+    Gia_ManForEachRi( p, pFlopIn, i )
+    {
+        fCompl = Gia_ObjFaninC0(pFlopIn);
+        pDriver = Gia_ObjFanin0(pFlopIn);
+        if ( !Gia_ObjIsAnd(pDriver) )
+        {
+            printf( "The flop driver %d is not a node.\n", i );
+            Vec_PtrPush( vDatas, NULL );
+            Vec_IntPush( vFlopClasses, 0 );
+            Counter++;
+            continue;
+        }
+        if ( !Gia_ObjFaninC0(pDriver) || !Gia_ObjFaninC1(pDriver) )
+        {
+            printf( "The flop driver %d is not an OR gate.\n", i );
+            Vec_PtrPush( vDatas, NULL );
+            Vec_IntPush( vFlopClasses, 0 );
+            Counter++;
+            continue;
+        }
+        pFan0 = Gia_ObjFanin0(pDriver);
+        pFan1 = Gia_ObjFanin1(pDriver);
+        if ( !Gia_ObjIsAnd(pFan0) || !Gia_ObjIsAnd(pFan1) )
+        {
+            printf( "The flop driver fanin %d is not a node.\n", i );
+            Vec_PtrPush( vDatas, NULL );
+            Vec_IntPush( vFlopClasses, 0 );
+            Counter++;
+            continue;
+        }
+        pFlopOut = Gia_ObjRiToRo( p, pFlopIn );
+        pFlopOut = Gia_NotCond( pFlopOut, !fCompl );
+        if ( Gia_ObjChild0(pFan0) != pFlopOut && Gia_ObjChild1(pFan0) != pFlopOut && 
+             Gia_ObjChild0(pFan1) != pFlopOut && Gia_ObjChild1(pFan1) != pFlopOut )
+        {
+            printf( "The flop %d does not have a self-loop.\n", i );
+            Vec_PtrPush( vDatas, NULL );
+            Vec_IntPush( vFlopClasses, 0 );
+            Counter++;
+            continue;
+        }
+        pData = NULL;
+        if ( Gia_ObjChild0(pFan0) == pFlopOut )
+        {
+            pCtrl = Gia_Not( Gia_ObjChild1(pFan0) );
+            if ( Gia_ObjFanin0(pFan1) == Gia_Regular(pCtrl) )
+                pData = Gia_ObjChild1(pFan1);
+            else
+                pData = Gia_ObjChild0(pFan1);
+        }
+        else if ( Gia_ObjChild1(pFan0) == pFlopOut )
+        {
+            pCtrl = Gia_Not( Gia_ObjChild0(pFan0) );
+            if ( Gia_ObjFanin0(pFan1) == Gia_Regular(pCtrl) )
+                pData = Gia_ObjChild1(pFan1);
+            else
+                pData = Gia_ObjChild0(pFan1);
+        }
+        else if ( Gia_ObjChild0(pFan1) == pFlopOut )
+        {
+            pCtrl = Gia_Not( Gia_ObjChild1(pFan1) );
+            if ( Gia_ObjFanin0(pFan0) == Gia_Regular(pCtrl) )
+                pData = Gia_ObjChild1(pFan0);
+            else
+                pData = Gia_ObjChild0(pFan0);
+        }
+        else if ( Gia_ObjChild1(pFan1) == pFlopOut )
+        {
+            pCtrl = Gia_Not( Gia_ObjChild0(pFan1) );
+            if ( Gia_ObjFanin0(pFan0) == Gia_Regular(pCtrl) )
+                pData = Gia_ObjChild1(pFan0);
+            else
+                pData = Gia_ObjChild0(pFan0);
+        }
+        else assert( 0 );
+        if ( Vec_PtrFind( vCtrls, pCtrl ) == -1 )
+            Vec_PtrPush( vCtrls, pCtrl );
+        iClass = Vec_PtrFind( vCtrls, pCtrl );
+        pData = Gia_NotCond( pData, !fCompl );
+        Vec_PtrPush( vDatas, pData );
+        Vec_IntPush( vFlopClasses, iClass );
+    }
+    assert( Vec_PtrSize( vDatas ) == Gia_ManRegNum(p) );
+    assert( Vec_IntSize( vFlopClasses ) == Gia_ManRegNum(p) );
+    printf( "Detected %d classes.\n", Vec_PtrSize(vCtrls) - (Counter == 0) );
+    Vec_PtrFree( vCtrls );
+    
+
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsPo(p, pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManForEachRi( p, pObj, i )
+    {
+        pData = Vec_PtrEntry(vDatas, i);
+        if ( pData == NULL )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        else
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Vec_PtrFree( vDatas );
+
+
+    pNew = Gia_ManCleanup( pAux = pNew );
+    Gia_ManStop( pAux );
+    pNew->vFlopClasses = vFlopClasses;
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 95bffee8..4439453d 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -66,6 +66,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
 ***********************************************************************/
 void Gia_ManStop( Gia_Man_t * p )  
 {
+    if ( p->vFlopClasses )
+    Vec_IntFree( p->vFlopClasses );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
     ABC_FREE( p->pCexComb );
@@ -94,6 +96,38 @@ void Gia_ManStop( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManPrintClasses( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    if ( p->vFlopClasses == NULL )
+        return;
+    Gia_ManForEachRo( p, pObj, i )
+        printf( "%d", Vec_IntEntry(p->vFlopClasses, i) );
+    printf( "\n" );
+
+    {
+        Gia_Man_t * pTemp;
+        pTemp = Gia_ManDupFlopClass( p, 1 );
+        Gia_WriteAiger( pTemp, "dom1.aig", 0, 0 );
+        Gia_ManStop( pTemp );
+        pTemp = Gia_ManDupFlopClass( p, 2 );
+        Gia_WriteAiger( pTemp, "dom2.aig", 0, 0 );
+        Gia_ManStop( pTemp );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManPrintStats( Gia_Man_t * p )
 {
     if ( p->pName )
@@ -113,6 +147,8 @@ void Gia_ManPrintStats( Gia_Man_t * p )
         Gia_ManEquivPrintClasses( p, 0, 0.0 );
     if ( p->pMapping )
         Gia_ManPrintMappingStats( p );
+    // print register classes
+//    Gia_ManPrintClasses( p );
 }
 
 /**Function*************************************************************
@@ -205,6 +241,28 @@ void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Reports the reduction of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew )
+{
+    printf( "REG: Beg = %5d. End = %5d. (R =%5.1f %%)  ",
+        Gia_ManRegNum(p), Gia_ManRegNum(pNew), 
+        Gia_ManRegNum(p)? 100.0*(Gia_ManRegNum(p)-Gia_ManRegNum(pNew))/Gia_ManRegNum(p) : 0.0 );
+    printf( "AND: Beg = %6d. End = %6d. (R =%5.1f %%)",
+        Gia_ManAndNum(p), Gia_ManAndNum(pNew), 
+        Gia_ManAndNum(p)? 100.0*(Gia_ManAndNum(p)-Gia_ManAndNum(pNew))/Gia_ManAndNum(p) : 0.0 );
+    printf( "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
new file mode 100644
index 00000000..4f2c6e08
--- /dev/null
+++ b/src/aig/gia/giaRetime.c
@@ -0,0 +1,296 @@
+/**CFile****************************************************************
+
+  FileName    [giaRetime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Performs most-forward retiming for AIG with flop classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaRetime.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks objects reachables from Const0 and PIs/
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManMarkAutonomous_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->fMark0;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( pObj->fMark0 == 0 );
+    if ( Gia_ObjIsPi(p, pObj) || Gia_ObjIsConst0(pObj) )
+        return pObj->fMark0 = 1;
+    if ( Gia_ObjIsCo(pObj) )
+        return pObj->fMark0 = Gia_ManMarkAutonomous_rec( p, Gia_ObjFanin0(pObj) );
+    if ( Gia_ObjIsCi(pObj) )
+        return pObj->fMark0 = Gia_ManMarkAutonomous_rec( p, Gia_ObjRoToRi(p, pObj) );
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( Gia_ManMarkAutonomous_rec( p, Gia_ObjFanin0(pObj) ) )
+        return pObj->fMark0 = 1;
+    return pObj->fMark0 = Gia_ManMarkAutonomous_rec( p, Gia_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks with current trav ROs reachable from Const0 and PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManMarkAutonomous( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManCleanMark0( p );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ManMarkAutonomous_rec( p, pObj );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachRo( p, pObj, i )
+        if ( pObj->fMark0 )
+            Gia_ObjSetTravIdCurrent( p, pObj );
+    Gia_ManCleanMark0( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRetimeDup_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManRetimeDup_rec( pNew, Gia_ObjFanin0(pObj) );
+    Gia_ManRetimeDup_rec( pNew, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int i;
+    // create the new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    // create the true PIs
+    Gia_ManFillValue( p );
+    Gia_ManSetPhase( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create the registers
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        pObj->Value = Gia_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase );
+    // duplicate logic above the cut
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManRetimeDup_rec( pNew, Gia_ObjFanin0(pObj) );
+    // create the true POs
+    Gia_ManForEachPo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    // remember value in LI
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    // transfer values from the LIs to the LOs
+    Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+        pObjRo->Value = pObjRi->Value;
+    // erase the data values on the internal nodes of the cut
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = ~0;
+    // duplicate logic below the cut
+    Vec_PtrForEachEntry( vCut, pObj, i )
+    {
+        Gia_ManRetimeDup_rec( pNew, pObj );
+        Gia_ManAppendCo( pNew, Gia_LitNotCond( pObj->Value, pObj->fPhase ) );
+    }
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Vec_PtrSize(vCut) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cut for forward retiming.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManRetimeForwardOne( Gia_Man_t * p, int * pnRegFixed, int * pnRegMoves )
+{
+    Vec_Int_t * vFlopClasses = NULL;
+    Vec_Int_t * vObjClasses = NULL;
+    Gia_Man_t * pNew;
+    Vec_Ptr_t * vCut;
+    Gia_Obj_t * pObj;
+    int i;
+    if ( p->vFlopClasses )
+    {
+        printf( "Performing retiming with register classes.\n" );
+        vObjClasses = Vec_IntAlloc( Gia_ManObjNum(p) );
+        for ( i = 0; i < Gia_ManObjNum(p); i++ )
+            Vec_IntPush( vObjClasses, -1 );
+        Gia_ManForEachRo( p, pObj, i )
+            Vec_IntWriteEntry( vObjClasses, Gia_ObjId(p, pObj), Vec_IntEntry(p->vFlopClasses, i) );
+        vFlopClasses = Vec_IntAlloc( Gia_ManRegNum(p) );
+    }
+    // mark the retimable nodes
+    Gia_ManResetTravId( p );
+    Gia_ManMarkAutonomous( p );
+    // mark the retimable registers with the fresh trav ID
+    Gia_ManIncrementTravId( p );
+    *pnRegFixed = 0;
+    Gia_ManForEachRo( p, pObj, i )
+        if ( Gia_ObjIsTravIdPrevious(p, pObj) )
+            Gia_ObjSetTravIdCurrent(p, pObj);
+        else
+            (*pnRegFixed)++;
+    // mark all the nodes that can be retimed forward
+    *pnRegMoves = 0;
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsTravIdCurrent(p, Gia_ObjFanin1(pObj)) )
+        {
+            if ( vObjClasses && Vec_IntEntry(vObjClasses, Gia_ObjFaninId0(pObj, i)) != Vec_IntEntry(vObjClasses, Gia_ObjFaninId1(pObj, i)) )
+                continue;
+            if ( vObjClasses )
+                Vec_IntWriteEntry( vObjClasses, Gia_ObjId(p, pObj), Vec_IntEntry(vObjClasses, Gia_ObjFaninId0(pObj, i)) );
+            Gia_ObjSetTravIdCurrent(p, pObj);
+            (*pnRegMoves)++;
+        }
+    // mark the remaining registers
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ObjSetTravIdCurrent(p, pObj);
+    // find the cut (all such marked objects that fanout into unmarked nodes)
+    vCut = Vec_PtrAlloc( 1000 );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsTravIdPrevious(p, pObj) )
+            continue;
+        if ( (Gia_ObjIsCo(pObj) || Gia_ObjIsAnd(pObj)) && Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin0(pObj)) )
+        {
+            if ( vFlopClasses )
+                Vec_IntPush( vFlopClasses, Vec_IntEntry(vObjClasses, Gia_ObjFaninId0(pObj, i)) );
+            Vec_PtrPush( vCut, Gia_ObjFanin0(pObj) );
+            Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin0(pObj) );
+        }
+        if ( Gia_ObjIsAnd(pObj) && Gia_ObjIsTravIdPrevious(p, Gia_ObjFanin1(pObj)) )
+        {
+            if ( vFlopClasses )
+                Vec_IntPush( vFlopClasses, Vec_IntEntry(vObjClasses, Gia_ObjFaninId1(pObj, i)) );
+            Vec_PtrPush( vCut, Gia_ObjFanin1(pObj) );
+            Gia_ObjSetTravIdCurrent( p, Gia_ObjFanin1(pObj) );
+        }
+    }
+    assert( vFlopClasses == NULL || Vec_IntSize(vFlopClasses) == Vec_PtrSize(vCut) );
+    // finally derive the new manager
+    pNew = Gia_ManRetimeDupForward( p, vCut );
+    Vec_PtrFree( vCut );
+    Vec_IntFree( vObjClasses );
+    pNew->vFlopClasses = vFlopClasses;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the cut for forward retiming.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManRetimeForward( Gia_Man_t * p, int nMaxIters, int fVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    int i, clk, nRegFixed, nRegMoves = 1;
+    pNew = p;
+    for ( i = 0; i < nMaxIters && nRegMoves > 0; i++ )
+    {
+        clk = clock();
+        pNew = Gia_ManRetimeForwardOne( pTemp = pNew, &nRegFixed, &nRegMoves );
+        if ( fVerbose )
+        {
+            printf( "%2d : And = %6d. Reg = %5d. Unret = %5d. Move = %6d. ", 
+                i + 1, Gia_ManAndNum(pTemp), Gia_ManRegNum(pTemp), nRegFixed, nRegMoves );
+            ABC_PRT( "Time", clock() - clk );
+        }
+        if ( pTemp != p )
+            Gia_ManStop( pTemp );
+    }
+/*
+    clk = clock();
+    pNew = Gia_ManReduceLaches( pNew, fVerbose );
+    if ( fVerbose )
+    {
+        ABC_PRT( "Register sharing time", clock() - clk );
+    }
+*/
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index 9058af7d..cf72104f 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -136,8 +136,6 @@ int Gia_ManSeqMarkUsed( Gia_Man_t * p )
     Gia_ManConst0(p)->fMark0 = 0;
     Gia_ManForEachPi( p, pObj, i )
         pObj->fMark0 = 0;
-    Gia_ManForEachPo( p, pObj, i )
-        pObj->fMark0 = 0;
     vRoots = Gia_ManCollectPoIds( p );
     Gia_ManForEachObjVec( vRoots, p, pObj, i )
         nNodes += Gia_ManSeqMarkUsed_rec( p, pObj, vRoots );
@@ -166,7 +164,7 @@ Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p )
 
   Synopsis    [Find representatives due to identical fanins.]
 
-  Description []
+  Description [Returns the old manager if there is no changes.]
                
   SideEffects []
 
@@ -189,7 +187,7 @@ Gia_Man_t * Gia_ManReduceEquiv( Gia_Man_t * p, int fVerbose )
     Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
     {
         iLit = Gia_ObjFanin0Copy( pObjRi );
-        if ( Gia_ObjFaninId0p(p, pObjRi) == 0 )
+        if ( Gia_ObjFaninId0p(p, pObjRi) == 0 && Gia_ObjFaninC0(pObjRi) == 0 ) // const 0 
             pCi2Lit[Gia_ManPiNum(p)+i] = 0, Counter0++;
         else if ( ~pMaps[iLit] ) // in this case, ID(pObj) > ID(pRepr) 
             pCi2Lit[Gia_ManPiNum(p)+i] = pMaps[iLit], Counter++; 
@@ -209,10 +207,13 @@ Gia_Man_t * Gia_ManReduceEquiv( Gia_Man_t * p, int fVerbose )
         }
     }
 */
-    if ( fVerbose )
-        printf( "ReduceEquiv detected %d constant regs and %d equivalent regs.\n", Counter0, Counter );
+//    if ( fVerbose )
+//        printf( "ReduceEquiv detected %d constant regs and %d equivalent regs.\n", Counter0, Counter );
     ABC_FREE( pMaps );
-    pNew = Gia_ManDupDfsCiMap( p, pCi2Lit, NULL );
+    if ( Counter0 || Counter )
+        pNew = Gia_ManDupDfsCiMap( p, pCi2Lit, NULL );
+    else
+        pNew = p;
     ABC_FREE( pCi2Lit );
     return pNew;
 }
@@ -233,19 +234,34 @@ Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fV
     Gia_Man_t * pTemp;
     if ( Gia_ManRegNum(p) == 0 )
         return Gia_ManDup( p );
-    p = Gia_ManSeqCleanup( p );
+    if ( fVerbose )
+        printf( "Performing sequential cleanup.\n" );
+    p = Gia_ManSeqCleanup( pTemp = p );
+    if ( fVerbose )
+        Gia_ManReportImprovement( pTemp, p );
     if ( fConst && Gia_ManRegNum(p) )
     {
         p = Gia_ManReduceConst( pTemp = p, fVerbose );
+        if ( fVerbose )
+            Gia_ManReportImprovement( pTemp, p );
         Gia_ManStop( pTemp );
     }
-    if ( fEquiv && Gia_ManRegNum(p) )
+    if ( fVerbose && fEquiv )
+        printf( "Merging combinationally equivalent flops.\n" );
+    if ( fEquiv )
+    while ( 1 )
     {
+        p = Gia_ManSeqCleanup( pTemp = p );
+        if ( fVerbose )
+            Gia_ManReportImprovement( pTemp, p );
+        Gia_ManStop( pTemp );
+        if ( Gia_ManRegNum(p) == 0 )
+            break;
         p = Gia_ManReduceEquiv( pTemp = p, fVerbose );
+        if ( p == pTemp )
+            break;
         Gia_ManStop( pTemp );
     }
-    p = Gia_ManSeqCleanup( pTemp = p );
-    Gia_ManStop( pTemp );
     return p;
 }
 
diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c
index c7aac864..8cfe5959 100644
--- a/src/aig/gia/giaTsim.c
+++ b/src/aig/gia/giaTsim.c
@@ -47,6 +47,8 @@ struct Gia_ManTer_t_
     int            nStateWords;
     Vec_Ptr_t *    vStates;
     Vec_Ptr_t *    vFlops;
+    Vec_Int_t *    vRetired;     // retired registers
+    char *         pRetired;     // retired registers
     int *          pCount0;
     int *          pCountX;
     // hash table for states
@@ -84,11 +86,13 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
     p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
     // allocate storage for terminary states
     p->nStateWords = Aig_BitWordNum( 2*Gia_ManRegNum(pAig) );
-    p->vStates = Vec_PtrAlloc( 1000 );
-    p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
-    p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
-    p->nBins   = Aig_PrimeCudd( 500 );
-    p->pBins   = ABC_CALLOC( unsigned *, p->nBins );
+    p->vStates  = Vec_PtrAlloc( 1000 );
+    p->pCount0  = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
+    p->pCountX  = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
+    p->nBins    = Aig_PrimeCudd( 500 );
+    p->pBins    = ABC_CALLOC( unsigned *, p->nBins );
+    p->vRetired = Vec_IntAlloc( 100 );
+    p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) );
     return p;
 }
 
@@ -130,6 +134,8 @@ void Gia_ManTerDelete( Gia_ManTer_t * p )
     if ( p->vFlops ) 
         Gia_ManTerStatesFree( p->vFlops );
     Gia_ManStop( p->pAig );
+    Vec_IntFree( p->vRetired );
+    ABC_FREE( p->pRetired );
     ABC_FREE( p->pCount0 );
     ABC_FREE( p->pCountX );
     ABC_FREE( p->pBins );
@@ -169,6 +175,10 @@ static inline void Gia_ManTerSimulateCi( Gia_ManTer_t * p, Gia_Obj_t * pObj, int
 static inline void Gia_ManTerSimulateCo( Gia_ManTer_t * p, int iCo, Gia_Obj_t * pObj )
 {
     int Value = Gia_ManTerSimInfoGet( p->pDataSim, Gia_ObjDiff0(pObj) );
+    if ( iCo == Gia_ManCoNum(p->pAig) -1 )
+    {
+        int s = 0;
+    }
     Gia_ManTerSimInfoSet( p->pDataSimCos, iCo, Gia_XsimNotCond( Value, Gia_ObjFaninC0(pObj) ) );
 }
 
@@ -368,7 +378,7 @@ static inline void Gia_ManTerSimulateRound( Gia_ManTer_t * p )
     int i, iCis = 0, iCos = 0;
     assert( p->pAig->nFront > 0 );
     assert( Gia_ManConst0(p->pAig)->Value == 0 );
-    Gia_ManTerSimInfoSet( p->pDataSim, 0, GIA_ONE );
+    Gia_ManTerSimInfoSet( p->pDataSim, 0, GIA_ZER );
     Gia_ManForEachObj1( p->pAig, pObj, i )
     {
         if ( Gia_ObjIsAndOrConst0(pObj) )
@@ -403,20 +413,54 @@ static inline void Gia_ManTerSimulateRound( Gia_ManTer_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManTerRetire( Gia_ManTer_t * p, unsigned * pState )
+int Gia_ManTerRetire2( Gia_ManTer_t * p, unsigned * pState )
 {
-    int i, iMaxTerValue = 0, Counter = 0;
+    int i, Entry, iMaxTerValue = -1, Counter = 0;
+    // find non-retired register with this value
     for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
-        if ( Gia_ManTerSimInfoGet( pState, i ) != GIA_UND && iMaxTerValue < p->pCountX[i] )
+        if ( Gia_ManTerSimInfoGet( pState, i ) != GIA_UND && !p->pRetired[i] && iMaxTerValue < p->pCountX[i] )
             iMaxTerValue = p->pCountX[i];
-    // retire all registers with this value
+    assert( iMaxTerValue >= 0 );
+    // retire the first registers with this value
     for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
-        if ( Gia_ManTerSimInfoGet( pState, i ) != GIA_UND && iMaxTerValue == p->pCountX[i] )
+        if ( Gia_ManTerSimInfoGet( pState, i ) != GIA_UND && !p->pRetired[i] && iMaxTerValue == p->pCountX[i] )
         {
-            Gia_ManTerSimInfoSet( p->pDataSimCis, Gia_ManPiNum(p->pAig)+i, GIA_UND );
-            Counter++;
+            assert( p->pRetired[i] == 0 );
+            p->pRetired[i] = 1;
+            Vec_IntPush( p->vRetired, i );
+            if ( iMaxTerValue == 0 )
+                break;
         }
-    return Counter;
+    // update all the retired registers
+    Vec_IntForEachEntry( p->vRetired, Entry, i )
+        Gia_ManTerSimInfoSet( p->pDataSimCis, Gia_ManPiNum(p->pAig)+Entry, GIA_UND );
+    return Vec_IntSize(p->vRetired);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Retires a set of registers to speed up convergence.]
+
+  Description [Retire all non-ternary registers which has max number 
+  of ternary values so far.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManTerRetire( Gia_ManTer_t * p, unsigned * pThis, unsigned * pPrev )
+{
+    int i, Entry;
+    // find registers whose value has changed
+    Vec_IntClear( p->vRetired );
+    for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+        if ( Gia_ManTerSimInfoGet( pThis, i ) != Gia_ManTerSimInfoGet( pPrev, i ) )
+            Vec_IntPush( p->vRetired, i );
+    // set all of them to zero
+    Vec_IntForEachEntry( p->vRetired, Entry, i )
+        Gia_ManTerSimInfoSet( p->pDataSimCis, Gia_ManPiNum(p->pAig)+Entry, GIA_UND );
+    return Vec_IntSize(p->vRetired);
 }
 
 /**Function*************************************************************
@@ -509,8 +553,8 @@ void Gia_ManTerAnalyze( Gia_ManTer_t * p )
             nZeros++;
         else if ( p->pCountX[i] == 0 )
             nConsts++;
-    printf( "Found %d constant registers.\n", nZeros );
-    printf( "Found %d non-ternary registers.\n", nConsts );
+//    printf( "Found %d constant registers.\n", nZeros );
+//    printf( "Found %d non-ternary registers.\n", nConsts );
 }
 
 
@@ -581,7 +625,7 @@ int Gia_ManFindEqualFlop( Vec_Ptr_t * vFlops, int iFlop, int nFlopWords )
   SeeAlso     []
 
 ***********************************************************************/
-int * Gia_ManTerCreateMap( Gia_ManTer_t * p )
+int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
 {
     int * pCi2Lit;
     Gia_Obj_t * pObj;
@@ -605,7 +649,8 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p )
             CounterE++;
         }
     Vec_IntFree( vMapKtoI );
-    printf( "Transformed %d const registers and %d equiv registers.\n", Counter0, CounterE );
+    if ( fVerbose )
+        printf( "Transforming %d const and %d equiv registers.\n", Counter0, CounterE );
     return pCi2Lit;
 }
 
@@ -624,13 +669,13 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p )
 Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
 {
     Gia_ManTer_t * p;
-    unsigned * pState, * pLoop;
+    unsigned * pState, * pPrev, * pLoop;
     int i, Counter, clk, clkTotal = clock();
     assert( Gia_ManRegNum(pAig) > 0 );
     // create manager
     clk = clock();
     p = Gia_ManTerCreate( pAig );
-    if ( fVerbose )
+    if ( 0 )
     {
         printf( "Obj = %8d (%8d). F = %6d. ", 
             pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront, 
@@ -648,6 +693,7 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
     Gia_ManTerStateInsert( pState, p->nStateWords, p->pBins, p->nBins );
 //Gia_ManTerStatePrint( pState, Gia_ManRegNum(pAig), 0 );
     // perform simuluation till convergence
+    pPrev = NULL;
     for ( i = 0; ; i++ )
     {
         Gia_ManTerSimulateRound( p );
@@ -663,15 +709,17 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
         Gia_ManTerStateInsert( pState, p->nStateWords, p->pBins, p->nBins );
         if ( i >= p->nIters && i % 10 == 0 )
         {
-            Counter = Gia_ManTerRetire( p, pState );
-            if ( fVerbose )
-                printf( "Retired %d registers.\n", Counter );
+            Counter = Gia_ManTerRetire( p, pState, pPrev );
+//            Counter = Gia_ManTerRetire2( p, pState );
+//            if ( fVerbose )
+//                printf( "Retired %d registers.\n", Counter );
         }
+        pPrev = pState;
     }
     if ( fVerbose )
     {
-        printf( "Saturated after %d iterations. ", i+1 );
-        ABC_PRT( "Total time", clock() - clkTotal );
+        printf( "Ternary simulation saturated after %d iterations. ", i+1 );
+        ABC_PRT( "Time", clock() - clkTotal );
     }
     return p;
 }
@@ -694,7 +742,7 @@ Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose )
     int * pCi2Lit;
     p = Gia_ManTerSimulate( pAig, fVerbose );
     Gia_ManTerAnalyze( p );
-    pCi2Lit = Gia_ManTerCreateMap( p );
+    pCi2Lit = Gia_ManTerCreateMap( p, fVerbose );
     Gia_ManTerDelete( p );
     pNew = Gia_ManDupDfsCiMap( pAig, pCi2Lit, NULL );
     ABC_FREE( pCi2Lit );
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 4410b497..d5ff628a 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -15,6 +15,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaHash.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMap.c \
+    src/aig/gia/giaRetime.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaSim.c \
     src/aig/gia/giaSort.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 556828cb..cf574ecb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -293,6 +293,8 @@ static int Abc_CommandAbc9Equiv      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc9Semi       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Times      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Frames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Retime     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Enable     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Miter      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sat        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -604,6 +606,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&semi",         Abc_CommandAbc9Semi,         0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&times",        Abc_CommandAbc9Times,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&frames",       Abc_CommandAbc9Frames,       0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&retime",       Abc_CommandAbc9Retime,       0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&enable",       Abc_CommandAbc9Enable,       0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&miter",        Abc_CommandAbc9Miter,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&scl",          Abc_CommandAbc9Scl,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&sat",          Abc_CommandAbc9Sat,          0 );
@@ -22899,7 +22903,7 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pAig == NULL )
     {
-        printf( "Abc_CommandAbc9Times(): There is no AIG.\n" );
+        printf( "Abc_CommandAbc9Frames(): There is no AIG.\n" );
         return 1;
     } 
     if ( nCofFanLit )
@@ -22931,6 +22935,121 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Retime( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c;
+    int nMaxIters = 100;
+    int fVerbose  =   0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nMaxIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMaxIters < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Retime(): There is no AIG.\n" );
+        return 1;
+    } 
+    pAbc->pAig = Gia_ManRetimeForward( pTemp = pAbc->pAig, nMaxIters, fVerbose );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &retime [-N <num>] [-vh]\n" );
+    fprintf( stdout, "\t         performs most-forward retiming\n" );
+    fprintf( stdout, "\t-N num : the number of incremental iterations [default = %d]\n", nMaxIters );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Enable( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c;
+    int fRemove  = 0;
+    int fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'r':
+            fRemove ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Enable(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( fRemove )
+        pAbc->pAig = Gia_ManRemoveEnables( pTemp = pAbc->pAig );
+    else
+        pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &enable [-rvh]\n" );
+    fprintf( stdout, "\t         adds or removes flop enable signals\n" );
+    fprintf( stdout, "\t-r     : toggle adding vs. removing enables [default = %s]\n", fRemove? "remove": "add" );
+    fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pFile;
@@ -23047,7 +23166,10 @@ usage:
 int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
-    int c, fConst = 1, fEquiv = 1, fVerbose = 1;
+    int c;
+    int fConst = 1;
+    int fEquiv = 1;
+    int fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
     {
@@ -23071,9 +23193,6 @@ int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Scl(): There is no AIG.\n" );
         return 1;
     } 
-    printf( "Implementation of this command is not finished.\n" );
-    return 0;
-
     pAbc->pAig = Gia_ManSeqStructSweep( pTemp = pAbc->pAig, fConst, fEquiv, fVerbose );
     Gia_ManStop( pTemp );
     return 0;
@@ -23953,14 +24072,18 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
+    int fSwitch = 0;
     extern void Gia_SatSolveTest( Gia_Man_t * p );
     extern void Cbs_ManSolveTest( Gia_Man_t * pGia );
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 's':
+            fSwitch ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -23982,14 +24105,19 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Gia_SatSolveTest( pAbc->pAig );
 //    For_ManExperiment( pAbc->pAig, 20, 1, 1 );
 //    Gia_ManUnrollSpecial( pAbc->pAig, 5, 100, 1 );
-//    pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
-//    Gia_ManStop( pTemp );
+
+    if ( fSwitch )
+        pAbc->pAig = Gia_ManDupSelf( pTemp = pAbc->pAig );
+    else 
+        pAbc->pAig = Gia_ManRemoveEnables( pTemp = pAbc->pAig );
+    Gia_ManStop( pTemp );
 //    Cbs_ManSolveTest( pAbc->pAig );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &test [-vh]\n" );
+    fprintf( stdout, "usage: &test [-svh]\n" );
     fprintf( stdout, "\t        testing various procedures\n" );
+    fprintf( stdout, "\t-s    : toggle enable (yes) vs. disable (no) [default = %s]\n", fSwitch? "yes": "no" );
     fprintf( stdout, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 50b0c749..b869f067 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -174,20 +174,20 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
 
     fprintf( pFile, "%-13s:",       pNtk->pName );
     if ( Abc_NtkAssertNum(pNtk) )
-        fprintf( pFile, " i/o/a = %5d/%5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
+        fprintf( pFile, " i/o/a =%5d/%5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
     else
-        fprintf( pFile, " i/o = %5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
-    fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
+        fprintf( pFile, " i/o =%5d/%5d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+    fprintf( pFile, "  lat =%5d", Abc_NtkLatchNum(pNtk) );
     if ( Abc_NtkIsNetlist(pNtk) )
     {
-        fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
-        fprintf( pFile, "  nd = %5d",  Abc_NtkNodeNum(pNtk) );
-        fprintf( pFile, "  wbox = %3d", Abc_NtkWhiteboxNum(pNtk) );
-        fprintf( pFile, "  bbox = %3d", Abc_NtkBlackboxNum(pNtk) );
+        fprintf( pFile, "  net =%5d", Abc_NtkNetNum(pNtk) );
+        fprintf( pFile, "  nd =%5d",  Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  wbox =%3d", Abc_NtkWhiteboxNum(pNtk) );
+        fprintf( pFile, "  bbox =%3d", Abc_NtkBlackboxNum(pNtk) );
     }
     else if ( Abc_NtkIsStrash(pNtk) )
     {        
-        fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  and =%7d", Abc_NtkNodeNum(pNtk) );
         if ( (Num = Abc_NtkGetChoiceNum(pNtk)) )
             fprintf( pFile, " (choice = %d)", Num );
         if ( fPrintMuxes )
@@ -201,8 +201,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
     }
     else 
     {
-        fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
-        fprintf( pFile, "  edge = %6d", Abc_NtkGetTotalFanins(pNtk) );
+        fprintf( pFile, "  nd =%6d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  edge =%7d", Abc_NtkGetTotalFanins(pNtk) );
     }
 
     if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
@@ -211,19 +211,19 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
     else if ( Abc_NtkHasSop(pNtk) )   
     {
 
-        fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
+        fprintf( pFile, "  cube =%6d",  Abc_NtkGetCubeNum(pNtk) );
 //        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
         if ( fFactored )
-            fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
+            fprintf( pFile, "  lit(fac) =%6d",  Abc_NtkGetLitFactNum(pNtk) );
     }
     else if ( Abc_NtkHasAig(pNtk) )
-        fprintf( pFile, "  aig  = %5d",  Abc_NtkGetAigNodeNum(pNtk) );
+        fprintf( pFile, "  aig  =%6d",  Abc_NtkGetAigNodeNum(pNtk) );
     else if ( Abc_NtkHasBdd(pNtk) )
-        fprintf( pFile, "  bdd  = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
+        fprintf( pFile, "  bdd  =%6d",  Abc_NtkGetBddNodeNum(pNtk) );
     else if ( Abc_NtkHasMapping(pNtk) )
     {
-        fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
-        fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
+        fprintf( pFile, "  area =%5.2f", Abc_NtkGetMappedArea(pNtk) );
+        fprintf( pFile, "  delay =%5.2f", Abc_NtkDelayTrace(pNtk) );
     }
     else if ( !Abc_NtkHasBlackbox(pNtk) )
     {
@@ -233,28 +233,28 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
     if ( Abc_NtkIsStrash(pNtk) )
     {
         extern int Abc_NtkGetMultiRefNum( Abc_Ntk_t * pNtk );
-        fprintf( pFile, "  lev = %3d", Abc_AigLevel(pNtk) );
+        fprintf( pFile, "  lev =%3d", Abc_AigLevel(pNtk) );
 //        fprintf( pFile, "  ff = %5d", Abc_NtkNodeNum(pNtk) + 2 * (Abc_NtkCoNum(pNtk)+Abc_NtkGetMultiRefNum(pNtk)) );
 //        fprintf( pFile, "  var = %5d", Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk)+Abc_NtkGetMultiRefNum(pNtk) );
     }
     else 
-        fprintf( pFile, "  lev = %3d", Abc_NtkLevel(pNtk) );
+        fprintf( pFile, "  lev =%3d", Abc_NtkLevel(pNtk) );
     if ( fUseLutLib && Abc_FrameReadLibLut() )
-        fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) );
+        fprintf( pFile, "  delay =%5.2f", Abc_NtkDelayTraceLut(pNtk, 1) );
     if ( fPower )
-        fprintf( pFile, "  power = %7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
+        fprintf( pFile, "  power =%7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
     if ( fGlitch )
     {
         extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk );
         if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 )
-            fprintf( pFile, "  glitch = %7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
+            fprintf( pFile, "  glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
         else
             printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." ); 
     }
     fprintf( pFile, "\n" );
 
     {
-        extern int Abc_NtkPrintSubraphSizes( Abc_Ntk_t * pNtk );
+//        extern int Abc_NtkPrintSubraphSizes( Abc_Ntk_t * pNtk );
 //        Abc_NtkPrintSubraphSizes( pNtk );
     }