Version abc80422

10 files changed, 1313 insertions, 165 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 74e3de31..47696a41 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -273,6 +273,7 @@ static inline Aig_Obj_t *  Aig_ManLi( Aig_Man_t * p, int i )      { return (Aig_
 static inline Aig_Obj_t *  Aig_ManObj( Aig_Man_t * p, int i )     { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL;  }
 
 static inline Aig_Type_t   Aig_ObjType( Aig_Obj_t * pObj )        { return (Aig_Type_t)pObj->Type;       }
+static inline int          Aig_ObjId( Aig_Obj_t * pObj )          { return pObj->Id;                     }
 static inline int          Aig_ObjIsNone( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_NONE;   }
 static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; }
 static inline int          Aig_ObjIsPi( Aig_Obj_t * pObj )        { return pObj->Type == AIG_OBJ_PI;     }
@@ -493,6 +494,7 @@ extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
 extern int             Aig_ManPiCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
+extern void            Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
@@ -513,6 +515,7 @@ extern void            Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
 extern void            Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
 extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
+extern void            Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
 /*=== aigOper.c =========================================================*/
 extern Aig_Obj_t *     Aig_IthVar( Aig_Man_t * p, int i );
 extern Aig_Obj_t *     Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index ee782423..41a62484 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -337,6 +337,28 @@ void Aig_ManPrintStats( Aig_Man_t * p )
     fflush( stdout );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reports the reduction of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
+{
+    printf( "REGs: Beg = %d. End = %d. (R = %6.2f %%).  ",
+        Aig_ManRegNum(p), Aig_ManRegNum(pNew), 
+        Aig_ManRegNum(p)? 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pNew))/Aig_ManRegNum(p) : 0.0 );
+    printf( "ANDs: Beg = %d. End = %d. (R = %6.2f %%).",
+        Aig_ManNodeNum(p), Aig_ManNodeNum(pNew), 
+        Aig_ManNodeNum(p)? 100.0*(Aig_ManNodeNum(p)-Aig_ManNodeNum(pNew))/Aig_ManNodeNum(p) : 0.0 );
+    printf( "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index a66eb2b8..9c7cf2c4 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -416,6 +416,81 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     pObjOld->pHaig = pHaig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Verbose printing of the AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int fHaig = 0;
+    int fShowFanouts = 0;
+    Aig_Obj_t * pTemp;
+    assert( !Aig_IsComplement(pObj) );
+    printf( "Node %4d : ", Aig_ObjId(pObj) );
+    if ( Aig_ObjIsConst1(pObj) )
+        printf( "constant 1" );
+    else if ( Aig_ObjIsPi(pObj) )
+        printf( "PI" );
+    else if ( Aig_ObjIsPo(pObj) )
+        printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+    else if ( Aig_ObjIsBuf(pObj) )
+        printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+    else
+        printf( "AND( %4d%s, %4d%s )", 
+            Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), 
+            Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") );
+    printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
+    if ( fShowFanouts && p->pFanData )
+    {
+        Aig_Obj_t * pFanout;
+        int i, iFan;
+        printf( "\nFanouts:\n" );
+        Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i )
+        {
+            printf( "    " );
+            printf( "Node %4d : ", Aig_ObjId(pFanout) );
+            if ( Aig_ObjIsPo(pFanout) )
+                printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
+            else if ( Aig_ObjIsBuf(pFanout) )
+                printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
+            else
+                printf( "AND( %4d%s, %4d%s )", 
+                    Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "), 
+                    Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") );
+            printf( "\n" );
+        }
+        return;
+    }
+    if ( fHaig )
+    {
+        if ( pObj->pHaig == NULL )
+            printf( " HAIG node not given" );
+        else
+            printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
+        return;
+    }
+    // there are choices
+    if ( p->pEquivs && p->pEquivs[pObj->Id] )
+    {
+        // print equivalence class
+        printf( "  { %4d ", pObj->Id );
+        for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+            printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " );
+        printf( " }" );
+        return;
+    }
+    // this is a secondary node
+    if ( p->pReprs && p->pReprs[pObj->Id] )
+        printf( "  class of %d", pObj->Id );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 7dc0c6e3..00e0311d 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -947,6 +947,48 @@ int Aig_ManCountChoices( Aig_Man_t * p )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints the fanouts of the control register.]
+
+  Description [Useful only for Intel MC benchmarks.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPrintControlFanouts( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;
+    int i, Counter = 0;
+
+    pCtrl = Aig_ManPi( p, Aig_ManPiNum(p) - 1 );
+
+    printf( "Control signal:\n" );
+    Aig_ObjPrint( p, pCtrl ); printf( "\n\n" );
+
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) )
+            continue;
+        assert( pObj != pCtrl );
+        pFanin0 = Aig_ObjFanin0(pObj);
+        pFanin1 = Aig_ObjFanin1(pObj);
+        if ( pFanin0 == pCtrl && Aig_ObjIsPi(pFanin1) )
+        {
+            Aig_ObjPrint( p, pObj ); printf( "\n" );
+            Aig_ObjPrint( p, pFanin1 ); printf( "\n" );
+            printf( "\n" );
+        }
+        if ( pFanin1 == pCtrl && Aig_ObjIsPi(pFanin0) )
+        {
+            Aig_ObjPrint( p, pObj ); printf( "\n" );
+            Aig_ObjPrint( p, pFanin0 ); printf( "\n" );
+            printf( "\n" );
+        }
+    }
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index ddb2dafe..cf763e67 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -152,6 +152,7 @@ extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
 extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
 extern Cnf_Dat_t *     Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
 extern Cnf_Dat_t *     Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
+extern Cnf_Dat_t *     Cnf_DeriveSimpleForRetiming( Aig_Man_t * p );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 5a96f23f..23b3e8f0 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -440,6 +440,108 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
     return pCnf;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives a simple CNF for backward retiming computation.]
+
+  Description [The last argument shows the number of last outputs
+  of the manager, which will not be converted into clauses. 
+  New variables will be introduced for these outputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
+    int i, nLiterals, nClauses, Number;
+
+    // count the number of literals and clauses
+    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManPoNum(p);
+    nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManPoNum(p);
+
+    // allocate CNF
+    pCnf = ALLOC( Cnf_Dat_t, 1 );
+    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+    pCnf->pMan = p;
+    pCnf->nLiterals = nLiterals;
+    pCnf->nClauses = nClauses;
+    pCnf->pClauses = ALLOC( int *, nClauses + 1 );
+    pCnf->pClauses[0] = ALLOC( int, nLiterals );
+    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
+
+    // create room for variable numbers
+    pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );
+    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
+    // assign variables to the last (nOutputs) POs
+    Number = 1;
+    Aig_ManForEachPo( p, pObj, i )
+        pCnf->pVarNums[pObj->Id] = Number++;
+    // assign variables to the internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pCnf->pVarNums[pObj->Id] = Number++;
+    // assign variables to the PIs and constant node
+    Aig_ManForEachPi( p, pObj, i )
+        pCnf->pVarNums[pObj->Id] = Number++;
+    pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
+    pCnf->nVars = Number;
+    // assign the clauses
+    pLits = pCnf->pClauses[0];
+    pClas = pCnf->pClauses;
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        OutVar   = pCnf->pVarNums[ pObj->Id ];
+        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
+
+        // positive phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar; 
+        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
+        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
+        // negative phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
+    }
+ 
+    // write the constant literal
+    OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
+    assert( OutVar <= Aig_ManObjNumMax(p) );
+    *pClas++ = pLits;
+    *pLits++ = 2 * OutVar; 
+
+    // write the output literals
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+        PoVar  = pCnf->pVarNums[ pObj->Id ];
+        // first clause
+        *pClas++ = pLits;
+        *pLits++ = 2 * PoVar; 
+        *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
+        // second clause
+        *pClas++ = pLits;
+        *pLits++ = 2 * PoVar + 1; 
+        *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
+        // final clause (init-state is always 0 -> set the output to 0)
+        *pClas++ = pLits;
+        *pLits++ = 2 * PoVar + 1; 
+    }
+
+    // verify that the correct number of literals and clauses was written
+    assert( pLits - pCnf->pClauses[0] == nLiterals );
+    assert( pClas - pCnf->pClauses == nClauses );
+    return pCnf;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/nwk/nwkFlow.c b/src/aig/nwk/nwkFlow.c
index 3a7e6df6..48496158 100644
--- a/src/aig/nwk/nwkFlow.c
+++ b/src/aig/nwk/nwkFlow.c
@@ -20,6 +20,14 @@
 
 #include "nwk.h"
 
+/*
+    This code is based on the papers:
+    A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming 
+    via binary maximum-flow", Proc. FMCAD '07, pp. 181-187. 
+    A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming 
+    under simultaneous delay and initial state constraints". Proc. DAC'08. 
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -368,7 +376,7 @@ int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
             return 0;
     return 1;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Verifies the forward cut.]
@@ -453,7 +461,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
         Counter++;
     }
     if ( fVerbose )
-    printf( "Forward: Max-flow1 = %5d.  ", Counter );
+    printf( "Forward:  Max-flow = %4d -> ", Counter );
     // continue flow computation from each LO
     Nwk_ManIncrementTravIdFlow( pMan );
     Nwk_ManForEachLoSeq( pMan, pObj, i )
@@ -464,7 +472,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
         Counter2++;
     }
     if ( fVerbose )
-    printf( "Max-flow2 = %5d.  ", Counter+Counter2 );
+    printf( "%4d.  ", Counter+Counter2 );
     // repeat flow computation from each LO
     if ( Counter2 > 0 )
     {
@@ -489,10 +497,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
         }
     }
     Nwk_ManCleanMarks( pMan );
-    assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
+//    assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
     if ( fVerbose )
     {
-    printf( "Min-cut = %5d.  Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+    printf( "Min-cut = %4d.  Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
     PRT( "Time", clock() - clk );
     }
     return vNodes;
@@ -536,8 +544,8 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
         Nwk_ManIncrementTravIdFlow( pMan );
         Counter++; 
     }
-    if ( fVerbose )
-    printf( "Backward: Max-flow1 = %5d.  ", Counter );
+    if ( fVerbose ) 
+    printf( "Backward: Max-flow = %4d -> ", Counter );
     // continue flow computation from each LI driver
     Nwk_ManIncrementTravIdFlow( pMan );
     Nwk_ManForEachLiSeq( pMan, pObj, i )
@@ -548,7 +556,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
         Counter2++;
     }
     if ( fVerbose )
-    printf( "Max-flow2 = %5d.  ", Counter+Counter2 );
+    printf( "%4d.  ", Counter+Counter2 );
     // repeat flow computation from each LI driver
     if ( Counter2 > 0 )
     {
@@ -576,10 +584,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
         if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
             Counter++;
     Nwk_ManCleanMarks( pMan );
-    assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
+//    assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
     if ( fVerbose )
     {
-    printf( "Min-cut = %5d.  Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter );
+    printf( "Min-cut = %4d.  Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
     PRT( "Time", clock() - clk );
     }
     return vNodes;
diff --git a/src/aig/nwk/nwkFlow_depth.c b/src/aig/nwk/nwkFlow_depth.c
new file mode 100644
index 00000000..a457631c
--- /dev/null
+++ b/src/aig/nwk/nwkFlow_depth.c
@@ -0,0 +1,626 @@
+/**CFile****************************************************************
+
+  FileName    [nwkFlow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Max-flow/min-cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+/*
+    This code is based on the papers:
+    A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming 
+    via binary maximum-flow", Proc. FMCAD '07, pp. 181-187. 
+    A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming 
+    under simultaneous delay and initial state constraints". Proc. DAC'08. 
+*/
+
+int DepthFwd, DepthBwd, DepthFwdMax, DepthBwdMax;
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// predecessors
+static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj )                   { return pObj->pCopy;        }
+static inline int         Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; }
+// sink
+static inline int         Nwk_ObjIsSink( Nwk_Obj_t * pObj )                 { return pObj->MarkA;        }
+static inline void        Nwk_ObjSetSink( Nwk_Obj_t * pObj )                { pObj->MarkA = 1;           }
+// flow
+static inline int         Nwk_ObjHasFlow( Nwk_Obj_t * pObj )                { return pObj->MarkB;        }
+static inline void        Nwk_ObjSetFlow( Nwk_Obj_t * pObj )                { pObj->MarkB = 1;           }
+static inline void        Nwk_ObjClearFlow( Nwk_Obj_t * pObj )              { pObj->MarkB = 0;           }
+ 
+// representation of visited nodes
+// pObj->TravId  < pNtk->nTravIds-2   --- not visited
+// pObj->TravId == pNtk->nTravIds-2   --- visited bot only
+// pObj->TravId == pNtk->nTravIds-1   --- visited top only
+// pObj->TravId == pNtk->nTravIds     --- visited bot and top
+static inline int  Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj )   
+{
+    return pObj->TravId == pObj->pMan->nTravIds - 2;
+}
+static inline int  Nwk_ObjVisitedBot( Nwk_Obj_t * pObj )     
+{ 
+    return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds; 
+}
+static inline int  Nwk_ObjVisitedTop( Nwk_Obj_t * pObj )     
+{ 
+    return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds; 
+}
+static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj )  
+{
+    if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+        pObj->TravId = pObj->pMan->nTravIds - 2;
+    else if ( pObj->TravId == pObj->pMan->nTravIds - 1 )
+        pObj->TravId = pObj->pMan->nTravIds;
+    else
+        assert( 0 );
+}
+static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj )  
+{
+    if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
+        pObj->TravId = pObj->pMan->nTravIds - 1;
+    else if ( pObj->TravId == pObj->pMan->nTravIds - 2 )
+        pObj->TravId = pObj->pMan->nTravIds;
+    else
+        assert( 0 );
+}
+static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan )
+{
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManIncrementTravId( pMan );
+}
+
+static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks TFI of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkTfiCone_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return;
+    pObj->MarkA = 1;
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        Nwk_ManMarkTfiCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks TFO of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkTfoCone_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return;
+    pObj->MarkA = 1;
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        Nwk_ManMarkTfoCone_rec( pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast forward flow pushing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushForwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 0;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjHasFlow(pObj) )
+        return 0;
+    if ( Nwk_ObjIsSink(pObj) )
+    {
+        Nwk_ObjSetFlow(pObj);
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) )
+        {
+            Nwk_ObjSetFlow(pObj);
+            return Nwk_ObjSetPred( pObj, pPred );
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fast backward flow pushing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushBackwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 0;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjHasFlow(pObj) )
+        return 0;
+    if ( Nwk_ObjIsSink(pObj) )
+    {
+        Nwk_ObjSetFlow(pObj);
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) )
+        {
+            Nwk_ObjSetFlow(pObj);
+            return Nwk_ObjSetPred( pObj, pPred );
+        }
+    return 0;
+}
+  
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the bottom part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjVisitedBot(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedBot(pObj);
+    DepthFwd++;
+    if ( DepthFwdMax < DepthFwd )
+        DepthFwdMax = DepthFwd;
+    // propagate through the internal edge
+    if ( Nwk_ObjHasFlow(pObj) )
+    {
+        if ( Nwk_ObjPred(pObj) )
+            if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+            {
+                DepthFwd--;
+                return Nwk_ObjSetPred( pObj, pPred ); 
+            }
+    }
+    else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) )
+    {
+        DepthFwd--;
+        Nwk_ObjSetFlow( pObj );
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    // try to push through the fanins
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+        {
+            DepthFwd--;
+            return 1;
+        }
+    DepthFwd--;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the top part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjVisitedTop(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedTop(pObj);
+    // check if this is the sink
+    if ( Nwk_ObjIsSink(pObj) )
+        return 1;
+    DepthFwd++;
+    if ( DepthFwdMax < DepthFwd )
+        DepthFwdMax = DepthFwd;
+    // try to push through the fanouts
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
+        {
+            DepthFwd--;
+            return 1;
+        }
+    // redirect the flow
+    if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) )
+        if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+        {
+            DepthFwd--;
+            Nwk_ObjClearFlow( pObj );
+            return Nwk_ObjSetPred( pObj, NULL );
+        }
+    DepthFwd--;
+    return 0;
+}
+  
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the bottom part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    if ( Nwk_ObjVisitedBot(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedBot(pObj);
+    // propagate through the internal edge
+    if ( Nwk_ObjHasFlow(pObj) )
+    {
+        if ( Nwk_ObjPred(pObj) )
+            if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
+                return Nwk_ObjSetPred( pObj, pPred ); 
+    }
+    else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) )
+    {
+        Nwk_ObjSetFlow( pObj );
+        return Nwk_ObjSetPred( pObj, pPred );
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Pushing the flow through the top part of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjVisitedTop(pObj) )
+        return 0;
+    Nwk_ObjSetVisitedTop(pObj);
+    // check if this is the sink
+    if ( Nwk_ObjIsSink(pObj) )
+        return 1;
+    // try to push through the fanins
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) )
+            return 1;
+    // try to push through the fanouts
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) )
+            return 1;
+    // redirect the flow
+    if ( Nwk_ObjHasFlow(pObj) )
+        if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
+        {
+            Nwk_ObjClearFlow( pObj );
+            return Nwk_ObjSetPred( pObj, NULL );
+        }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 0 if there is an unmarked path to a CI.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( pObj->MarkA )
+        return 1;
+    if ( Nwk_ObjIsLo(pObj) )
+        return 0;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return 1;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        if ( !Nwk_ManVerifyCut_rec( pNext ) )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the forward cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutForward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    // mark the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        assert( pObj->MarkA == 0 );
+        pObj->MarkA = 1;
+    }
+    // traverse from the COs
+    Nwk_ManIncrementTravId( pMan );
+    Nwk_ManForEachCo( pMan, pObj, i )
+        if ( !Nwk_ManVerifyCut_rec( pObj ) )
+            printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" );
+    // unmark the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->MarkA = 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the forward cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManRetimeVerifyCutBackward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
+{
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes minimum cut for forward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj;
+    int i, RetValue, Counter = 0, Counter2 = 0;
+    int clk = clock();
+    // set the sequential parameters
+    pMan->nLatches = nLatches;
+    pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+    pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+    // mark the COs and the TFO of PIs
+    Nwk_ManForEachCo( pMan, pObj, i )
+        pObj->MarkA = 1;
+    Nwk_ManForEachPiSeq( pMan, pObj, i )
+        Nwk_ManMarkTfoCone_rec( pObj );
+    // start flow computation from each LO
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLoSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter++;
+    }
+    if ( fVerbose )
+    printf( "Forward:  Max-flow = %4d -> ", Counter );
+    // continue flow computation from each LO
+    DepthFwdMax = DepthFwd = 0;
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLoSeq( pMan, pObj, i )
+    {
+    printf( "%d ", DepthFwdMax );
+        if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) )
+            continue;
+        assert( DepthFwd == 0 );
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter2++;
+    }
+    printf( "DepthMax = %d.\n", DepthFwdMax );
+    if ( fVerbose )
+    printf( "%4d.  ", Counter+Counter2 );
+    // repeat flow computation from each LO
+    if ( Counter2 > 0 )
+    {
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Nwk_ManForEachLoSeq( pMan, pObj, i )
+        {
+            RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL );
+            assert( !RetValue );
+        }
+    }
+    // cut is a set of nodes whose bottom is visited but top is not visited
+    vNodes = Vec_PtrAlloc( Counter+Counter2 );
+    Counter = 0;
+    Nwk_ManForEachObj( pMan, pObj, i )
+    {
+        if ( Nwk_ObjVisitedBotOnly(pObj) )
+        {
+            assert( Nwk_ObjHasFlow(pObj) );
+            assert( !Nwk_ObjIsCo(pObj) );
+            Vec_PtrPush( vNodes, pObj );
+            Counter += Nwk_ObjIsCi(pObj);
+        }
+    }
+    Nwk_ManCleanMarks( pMan );
+    assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
+    if ( fVerbose )
+    {
+    printf( "Min-cut = %4d.  Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
+    PRT( "Time", clock() - clk );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes minimum cut for backward retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj;
+    int i, RetValue, Counter = 0, Counter2 = 0;
+    int clk = clock();
+    // set the sequential parameters
+    pMan->nLatches = nLatches;
+    pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
+    pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
+    // mark the CIs, the TFI of POs, and the constant nodes
+    Nwk_ManForEachCi( pMan, pObj, i )
+        pObj->MarkA = 1;
+    Nwk_ManForEachPoSeq( pMan, pObj, i )
+        Nwk_ManMarkTfiCone_rec( pObj );
+    Nwk_ManForEachNode( pMan, pObj, i )
+        if ( Nwk_ObjFaninNum(pObj) == 0 )
+            pObj->MarkA = 1;
+    // start flow computation from each LI driver
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter++; 
+    }
+    if ( fVerbose ) 
+    printf( "Backward: Max-flow = %4d -> ", Counter );
+    // continue flow computation from each LI driver
+    Nwk_ManIncrementTravIdFlow( pMan );
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+    {
+        if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) )
+            continue;
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Counter2++;
+    }
+    if ( fVerbose )
+    printf( "%4d.  ", Counter+Counter2 );
+    // repeat flow computation from each LI driver
+    if ( Counter2 > 0 )
+    {
+        Nwk_ManIncrementTravIdFlow( pMan );
+        Nwk_ManForEachLiSeq( pMan, pObj, i )
+        {
+            RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL );
+            assert( !RetValue );
+        }
+    }
+    // cut is a set of nodes whose bottom is visited but top is not visited
+    vNodes = Vec_PtrAlloc( Counter+Counter2 );
+    Nwk_ManForEachObj( pMan, pObj, i )
+    {
+        if ( Nwk_ObjVisitedBotOnly(pObj) )
+        {
+            assert( Nwk_ObjHasFlow(pObj) );
+            assert( !Nwk_ObjIsCo(pObj) );
+            Vec_PtrPush( vNodes, pObj );
+        }
+    }
+    // count CO drivers
+    Counter = 0;
+    Nwk_ManForEachLiSeq( pMan, pObj, i )
+        if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
+            Counter++;
+    Nwk_ManCleanMarks( pMan );
+    assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
+    if ( fVerbose )
+    {
+    printf( "Min-cut = %4d.  Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
+    PRT( "Time", clock() - clk );
+    }
+    return vNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index f83666c4..fc00ce3c 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -272,7 +272,7 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
         else
             continue;
         // print trace
-        printf( "%5d : %5d  ", Counter, i );
+        printf( "%5d : %5d %5d  ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
         Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
         {
             Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
@@ -536,6 +536,60 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits )
 
 /**Function*************************************************************
 
+  Synopsis    [Analize initial value of the selected register.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
+{
+    Aig_Obj_t * pObj, * pReg, * pCtrl, * pAnd;
+    int i;
+    pReg = Saig_ManLo( p, Reg );
+    pCtrl = Saig_ManLo( p, Saig_ManRegNum(p)-1 );
+    assert( pReg->Id < pCtrl->Id );
+    // find a node pointing to both
+    pAnd = NULL;
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( Aig_ObjFanin0(pObj) == pReg && Aig_ObjFanin1(pObj) == pCtrl )
+        {
+            pAnd = pObj;
+            break;
+        }
+    }
+    if ( pAnd == NULL )
+    {
+        printf( "Register is not found.\n" );
+        return;
+    }
+    printf( "Clock-like register: \n" );
+    Aig_ObjPrint( p, pReg );
+    printf( "\n" );
+    printf( "Control register: \n" );
+    Aig_ObjPrint( p, pCtrl );
+    printf( "\n" );
+    printf( "Their fanout: \n" );
+    Aig_ObjPrint( p, pAnd );
+    printf( "\n" );
+ 
+    // find the fanouts of pAnd
+    printf( "Fanouts of the fanout: \n" );
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjFanin0(pObj) == pAnd || Aig_ObjFanin1(pObj) == pAnd )
+        {
+            Aig_ObjPrint( p, pObj );
+            printf( "\n" );
+        }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finds the registers to phase-abstract.]
 
   Description []
@@ -587,6 +641,9 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe
             for ( k = 0; k < nFrames; k++ )
                 Saig_XsimPrint( stdout, Values[k] );
             printf( "]\n" );
+
+            if ( fVerbose )
+            Saig_ManAnalizeControl( pTsi->pAig, Reg );
         }
     }
     Vec_IntShrink( pTsi->vNonXRegs, r );
@@ -595,6 +652,7 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe
     return Vec_IntSize(pTsi->vNonXRegs);
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Mapping of AIG nodes into frames nodes.]
@@ -662,7 +720,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe
             pState = Vec_PtrEntry( pTsi->vStates, f );
             Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
             assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
-            pObjNew = Value? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
+            pObjNew = (Value == SAIG_XVS1)? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
             Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
         }
         // add internal nodes of this frame
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 3adb76c6..c53d6d6b 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -19,8 +19,10 @@
 ***********************************************************************/
 
 #include "saig.h"
-#include "satSolver.h"
+
 #include "cnf.h"
+#include "satSolver.h"
+#include "satStore.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -34,7 +36,7 @@ extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fV
 
 /**Function*************************************************************
 
-  Synopsis    [Marks the TFI cone with the current traversal ID.]
+  Synopsis    [Derives the initial state after backward retiming.]
 
   Description []
                
@@ -43,66 +45,161 @@ extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fV
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p )
 {
-    if ( pObj == NULL )
-        return;
-    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
-        return;
-    Aig_ObjSetTravIdCurrent( p, pObj );
-    Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) );
-    Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) );
+    int nConfLimit = 1000000;
+    Vec_Int_t * vCiIds, * vInit = NULL;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int i, RetValue, * pModel;
+    // solve the SAT problem
+    pCnf = Cnf_DeriveSimpleForRetiming( p );
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat == NULL )
+    {
+        Cnf_DataFree( pCnf );
+        return NULL;
+    }
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue != l_Undef );
+    // create counter-example
+    if ( RetValue == l_True )
+    {
+        // accumulate SAT variables of the CIs
+        vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+        Aig_ManForEachPi( p, pObj, i )
+            Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
+        // create the model
+        pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+        vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) );
+        Vec_IntFree( vCiIds );
+    }
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    return vInit;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of nodes to get registers after retiming.]
+  Synopsis    [Uses UNSAT core to find the part of AIG to be excluded.]
 
-  Description []
+  Description [Returns the number of the PO that appears in the UNSAT core.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
+int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
 {
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj, * pFanin;
-    int i, RetValue;
-    // mark the cones
-    Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vCut, pObj, i )
-        Saig_ManMarkCone_rec( p, pObj );
-    // collect the new cut
-    vNodes = Vec_PtrAlloc( 1000 );
-    Aig_ManForEachObj( p, pObj, i )
+    int fVeryVerbose = 0;
+    int nConfLimit = 1000000;
+    void * pSatCnf = NULL; 
+    Intp_Man_t * pManProof;
+    Vec_Int_t * vCore = NULL;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int * pClause1, * pClause2, * pLit, * pVars;
+    int i, RetValue, iBadPo, iClause, nVars, nPos;
+    // create the SAT solver
+    pCnf = Cnf_DeriveSimpleForRetiming( p );
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat ); 
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
     {
-        if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-            continue;
-        pFanin = Aig_ObjFanin0( pObj );
-        if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
         {
-            Vec_PtrPush( vNodes, pFanin );
-            pFanin->fMarkA = 1;
+            Cnf_DataFree( pCnf );
+            sat_solver_delete( pSat );
+            return -1;
         }
-        pFanin = Aig_ObjFanin1( pObj );
-        if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
+    }
+    sat_solver_store_mark_roots( pSat ); 
+    // solve the problem
+    RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    assert( RetValue != l_Undef );
+    assert( RetValue == l_False );
+    pSatCnf = sat_solver_store_release( pSat ); 
+    sat_solver_delete( pSat );
+    // derive the UNSAT core
+    pManProof = Intp_ManAlloc();
+    vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVeryVerbose );
+    Intp_ManFree( pManProof );
+    Sto_ManFree( pSatCnf );
+    // derive the set of variables on which the core depends
+    // collect the variable numbers
+    nVars = 0;
+    pVars = ALLOC( int, pCnf->nVars );
+    memset( pVars, 0, sizeof(int) * pCnf->nVars );
+    Vec_IntForEachEntry( vCore, iClause, i )
+    {
+        pClause1 = pCnf->pClauses[iClause];
+        pClause2 = pCnf->pClauses[iClause+1];
+        for ( pLit = pClause1; pLit < pClause2; pLit++ )
         {
-            Vec_PtrPush( vNodes, pFanin );
-            pFanin->fMarkA = 1;
+            if ( pVars[ (*pLit) >> 1 ] == 0 )
+                nVars++;
+            pVars[ (*pLit) >> 1 ] = 1;
+            if ( fVeryVerbose )
+            printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
         }
+        if ( fVeryVerbose )
+        printf( "\n" );
     }
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->fMarkA = 0;
-    RetValue = Vec_PtrSize( vNodes );
-    Vec_PtrFree( vNodes );
-    return RetValue;
+    // collect the nodes
+    if ( fVeryVerbose )
+    Aig_ManForEachObj( p, pObj, i )
+        if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
+        {
+            Aig_ObjPrint( p, pObj );
+            printf( "\n" );
+        }
+    // pick the first PO in the list
+    nPos = 0;
+    iBadPo = -1;
+    Aig_ManForEachPo( p, pObj, i )
+        if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
+        {
+            if ( iBadPo == -1 )
+                iBadPo = i;
+            nPos++;
+        }
+    if ( fVerbose )
+        printf( "UNSAT core: %d clauses, %d variables, %d POs.  ", Vec_IntSize(vCore), nVars, nPos );
+    free( pVars );
+    Vec_IntFree( vCore );
+    Cnf_DataFree( pCnf );
+    return iBadPo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone with the current traversal ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManMarkCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj == NULL )
+        return;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) );
+    Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the new cut after excluding the nodes in the set.]
+  Synopsis    [Counts the number of nodes to get registers after retiming.]
 
   Description []
                
@@ -111,17 +208,15 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t * vToExclude )
+int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
 {
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj, * pFanin;
-    int i;
+    int i, RetValue;
     // mark the cones
     Aig_ManIncrementTravId( p );
     Vec_PtrForEachEntry( vCut, pObj, i )
         Saig_ManMarkCone_rec( p, pObj );
-    Vec_PtrForEachEntry( vToExclude, pObj, i )
-        Saig_ManMarkCone_rec( p, pObj );
     // collect the new cut
     vNodes = Vec_PtrAlloc( 1000 );
     Aig_ManForEachObj( p, pObj, i )
@@ -143,7 +238,9 @@ Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t
     }
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->fMarkA = 0;
-    return vNodes;
+    RetValue = Vec_PtrSize( vNodes );
+    Vec_PtrFree( vNodes );
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -222,12 +319,13 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
         Saig_ManRetimeDup_rec( pNew, pObj );
         Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) );
     }
+    Aig_ManCleanup( pNew );
     return pNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives AIG for the initial state computation.]
+  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
 
   Description []
                
@@ -236,33 +334,64 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )
+Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Int_t * vInit )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i;
     // mark the cones under the cut
 //    assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = Vec_PtrSize(vCut);
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = p->nTruePos;
     // create the true PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Saig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
     // create the registers
     Vec_PtrForEachEntry( vCut, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pNew);
-    // duplicate logic above the cut and create POs
+        pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 );
+    // duplicate logic above the cut and remember values
     Saig_ManForEachLi( p, pObj, i )
     {
         Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
+        pObj->pData = Aig_ObjChild0Copy(pObj);
+    }
+    // transfer values from the LIs to the LOs
+    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+        pObjLo->pData = pObjLi->pData;
+    // erase the data values on the internal nodes of the cut
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = NULL;
+    // replicate the data on the constant node and the PIs
+    pObj = Aig_ManConst1(p);
+    pObj->pData = Aig_ManConst1(pNew);
+    Saig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ManPi( pNew, i );
+    // duplicate logic below the cut
+    Saig_ManForEachPo( p, pObj, i )
+    {
+        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     }
+    Vec_PtrForEachEntry( vCut, pObj, i )
+    {
+        Saig_ManRetimeDup_rec( pNew, pObj );
+        Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );
+    }
+    Aig_ManCleanup( pNew );
     return pNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the initial state after backward retiming.]
+  Synopsis    [Derives AIG for the initial state computation.]
 
   Description []
                
@@ -271,36 +400,28 @@ Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p )
+Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )
 {
-    int nConfLimit = 1000000;
-    Vec_Int_t * vCiIds, * vInit = NULL;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
+    Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
-    int i, RetValue, * pAssumps, * pModel;
-    // solve the SAT problem
-    pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    pAssumps = ALLOC( int, Aig_ManPoNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-        pAssumps[i] = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
-    RetValue = sat_solver_solve( pSat, pAssumps, pAssumps+Aig_ManPoNum(p), (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
-    free( pAssumps );
-    if ( RetValue == l_True )
+    int i;
+    // mark the cones under the cut
+//    assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    // create the true PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    // create the registers
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // duplicate logic above the cut and create POs
+    Saig_ManForEachLi( p, pObj, i )
     {
-        // accumulate SAT variables of the CIs
-        vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
-        Aig_ManForEachPi( p, pObj, i )
-            Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
-        // create the model
-        pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-        vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) );
-        Vec_IntFree( vCiIds );
+        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     }
-    sat_solver_delete( pSat );
-    Cnf_DataFree( pCnf );
-    return vInit;
+    return pNew;
 }
 
 /**Function*************************************************************
@@ -316,7 +437,7 @@ Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p )
 ***********************************************************************/
 Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
 {
-    Vec_Ptr_t * vNodes = NULL;
+    Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj, * pFanin;
     int i, Diffs;
     assert( Saig_ManRegNum(p) > 0 );
@@ -334,13 +455,20 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
         pFanin = Aig_ObjFanin0(pObj);
         Diffs += pFanin->fMarkA && pFanin->fMarkB;
     }
+    vNodes = Vec_PtrAlloc( 100 );
     if ( Diffs > 0 )
-        vNodes = Vec_PtrAlloc( Diffs );
+    {
+        Saig_ManForEachLi( p, pObj, i )
+        {
+            pFanin = Aig_ObjFanin0(pObj);
+            if ( pFanin->fMarkA && pFanin->fMarkB )
+                Vec_PtrPush( vNodes, pObj );
+        }
+        assert( Vec_PtrSize(vNodes) == Diffs );
+    }
     Saig_ManForEachLi( p, pObj, i )
     {
         pFanin = Aig_ObjFanin0(pObj);
-        if ( vNodes && pFanin->fMarkA && pFanin->fMarkB )
-            Vec_PtrPush( vNodes, pFanin );
         pFanin->fMarkA = pFanin->fMarkB = 0;
     }
     return vNodes;
@@ -348,7 +476,7 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG while retiming the registers to the cut.]
+  Synopsis    [Hides the registers that cannot be backward retimed.]
 
   Description []
                
@@ -357,79 +485,125 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit )
+int Saig_ManHideBadRegs( Aig_Man_t * p, Vec_Ptr_t * vBadRegs )
 {
-    Vec_Ptr_t * vToExclude, * vCut;
-    Vec_Int_t * vInit = NULL;
-    Aig_Man_t * pNew, * pInit;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i;
-    // check if there are bad registers
-    vToExclude = Saig_ManGetRegistersToExclude( p );
-    if ( vToExclude )
-    {
-        vCut = Saig_ManRetimeExtendCut( p, vCutInit, vToExclude );
-        printf( "Bad registers = %d. Extended cut from %d to %d nodes.\n", 
-            Vec_PtrSize(vToExclude), Vec_PtrSize(vCutInit), Vec_PtrSize(vCut) );
-        Vec_PtrFree( vToExclude );
-    }
-    else
-        vCut = Vec_PtrDup( vCutInit );
-    // mark the cones under the cut
-//    assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
-    // count if there are registers to disable
-    // derive the initial state
-    pInit = Saig_ManRetimeDupInitState( p, vCut );
-    vInit = Saig_ManRetimeFindInitState( pInit );
-    if ( vInit == NULL )
-        printf( "Initial state computation has failed.\n" );
-    Aig_ManStop( pInit );
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    pNew->nRegs = Vec_PtrSize(vCut);
-    pNew->nTruePis = p->nTruePis;
-    pNew->nTruePos = p->nTruePos;
-    // create the true PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Saig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pNew );
-    // create the registers
-    Vec_PtrForEachEntry( vCut, pObj, i )
-        pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 );
-    // duplicate logic above the cut and remember values
-    Saig_ManForEachLi( p, pObj, i )
+    Vec_Ptr_t * vPisNew, * vPosNew;
+    Aig_Obj_t * pObjLi, * pObjLo;
+    int nTruePi, nTruePo, nBadRegs, i;
+    if ( Vec_PtrSize(vBadRegs) == 0 )
+        return 0;
+    // attached LOs to LIs
+    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+        pObjLi->pData = pObjLo;
+    // reorder them by putting bad registers first
+    vPisNew = Vec_PtrDup( p->vPis );
+    vPosNew = Vec_PtrDup( p->vPos );
+    nTruePi = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+    nTruePo = Aig_ManPoNum(p) - Aig_ManRegNum(p);
+    assert( nTruePi == p->nTruePis );
+    assert( nTruePo == p->nTruePos );
+    Vec_PtrForEachEntry( vBadRegs, pObjLi, i )
     {
-        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
-        pObj->pData = Aig_ObjChild0Copy(pObj);
+        Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLi->pData );
+        Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
+        pObjLi->fMarkA = 1;
     }
-    // transfer values from the LIs to the LOs
     Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
-        pObjLo->pData = pObjLi->pData;
-    // erase the data values on the internal nodes of the cut
-    Vec_PtrForEachEntry( vCut, pObj, i )
-        if ( Aig_ObjIsNode(pObj) )
-            pObj->pData = NULL;
-    // replicate the data on the primary inputs
-    Saig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ManPi( pNew, i );
-    // duplicate logic below the cut
-    Saig_ManForEachPo( p, pObj, i )
     {
-        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        if ( pObjLi->fMarkA )
+        {
+            pObjLi->fMarkA = 0;
+            continue;
+        }
+        Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLo );
+        Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
     }
-    Vec_PtrForEachEntry( vCut, pObj, i )
+    // check the sizes
+    assert( nTruePi == Aig_ManPiNum(p) );
+    assert( nTruePo == Aig_ManPoNum(p) );
+    // transfer the arrays
+    Vec_PtrFree( p->vPis ); p->vPis = vPisNew;
+    Vec_PtrFree( p->vPos ); p->vPos = vPosNew;
+    // update the PIs
+    nBadRegs = Vec_PtrSize(vBadRegs);
+    p->nRegs -= nBadRegs;
+    p->nTruePis += nBadRegs;
+    p->nTruePos += nBadRegs;
+    return nBadRegs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Exposes bad registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManExposeBadRegs( Aig_Man_t * p, int nBadRegs )
+{
+    p->nRegs += nBadRegs;
+    p->nTruePis -= nBadRegs;
+    p->nTruePos -= nBadRegs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs min-area retiming backward with initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose )
+{
+    Aig_Man_t * pInit, * pFinal;
+    Vec_Ptr_t * vBadRegs, * vCut;
+    Vec_Int_t * vInit;
+    int iBadReg;
+    // transform the AIG to have no bad registers
+    vBadRegs = Saig_ManGetRegistersToExclude( pNew );
+    if ( fVerbose && Vec_PtrSize(vBadRegs) )
+        printf( "Excluding %d registers that cannot be backward retimed.\n", Vec_PtrSize(vBadRegs) ); 
+    while ( 1 )
     {
-        Saig_ManRetimeDup_rec( pNew, pObj );
-        Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );
+        Saig_ManHideBadRegs( pNew, vBadRegs );
+        Vec_PtrFree( vBadRegs );
+        // compute cut
+        vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
+        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
+        {
+            Vec_PtrFree( vCut );
+            return NULL;
+        }
+        // derive the initial state
+        pInit = Saig_ManRetimeDupInitState( pNew, vCut );
+        vInit = Saig_ManRetimeInitState( pInit );
+        if ( vInit != NULL )
+        {
+            pFinal = Saig_ManRetimeDupBackward( pNew, vCut, vInit );
+            Vec_IntFree( vInit );
+            Vec_PtrFree( vCut );
+            Aig_ManStop( pInit );
+            return pFinal;
+        }
+        Vec_PtrFree( vCut );
+        // there is no initial state - find the offending output
+        iBadReg = Saig_ManRetimeUnsatCore( pInit, fVerbose );
+        Aig_ManStop( pInit );
+        if ( fVerbose )
+            printf( "Excluding register %d.\n", iBadReg ); 
+        // prepare to remove this output
+        vBadRegs = Vec_PtrAlloc( 1 );
+        Vec_PtrPush( vBadRegs, Aig_ManPo( pNew, Saig_ManPoNum(pNew) + iBadReg ) );
     }
-    if ( vInit )
-        Vec_IntFree( vInit );
-    Vec_PtrFree( vCut );
-    return pNew;
+    return NULL;
 }
 
 /**Function*************************************************************
@@ -443,36 +617,73 @@ Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fVerbose )
+Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
 {
     Vec_Ptr_t * vCut;
-    Aig_Man_t * pNew, * pTemp;
+    Aig_Man_t * pNew, * pTemp, * pCopy;
+    int fChanges;
     pNew = Aig_ManDup( p );
     // perform several iterations of forward retiming
+    fChanges = 0;
     if ( !fBackwardOnly )
     while ( 1 )
     {
         vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
         if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
         {
+            if ( fVerbose && !fChanges )
+                printf( "Forward retiming cannot reduce registers.\n" );
             Vec_PtrFree( vCut );
             break;
         }
         pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
         Aig_ManStop( pTemp );
         Vec_PtrFree( vCut );
+        if ( fVerbose )
+            Aig_ManReportImprovement( p, pNew );
+        fChanges = 1;
     }
-    // perform one iteration of backward retiming
-    if ( !fForwardOnly )
+    // perform several iterations of backward retiming
+    fChanges = 0;
+    if ( !fForwardOnly && !fInitial )
+    while ( 1 )
     {
         vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
-        if ( Vec_PtrSize(vCut) < Aig_ManRegNum(pNew) )
+        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
         {
-            pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut );
-            Aig_ManStop( pTemp );
+            if ( fVerbose && !fChanges )
+                printf( "Backward retiming cannot reduce registers.\n" );
+            Vec_PtrFree( vCut );
+            break;
         }
+        pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL );
+        Aig_ManStop( pTemp );
         Vec_PtrFree( vCut );
+        if ( fVerbose )
+            Aig_ManReportImprovement( p, pNew );
+        fChanges = 1;
+    }
+    else if ( !fForwardOnly && fInitial )
+    while ( 1 )
+    {
+        pCopy = Aig_ManDup( pNew );
+        pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
+        Aig_ManStop( pCopy );
+        if ( pTemp == NULL )
+        {
+            if ( fVerbose && !fChanges )
+                printf( "Backward retiming cannot reduce registers.\n" );
+            break;
+        }
+        Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) );
+        Aig_ManStop( pNew );
+        pNew = pTemp;
+        if ( fVerbose )
+            Aig_ManReportImprovement( p, pNew );
+        fChanges = 1;
     }
+    if ( !fForwardOnly && !fInitial && fChanges )
+        printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" );
     return pNew;
 }