Version abc80228

23 files changed, 1962 insertions, 482 deletions

diff --git a/abc.dsp b/abc.dsp
index 32cfed71..a8d6a3c6 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2378,6 +2378,10 @@ SOURCE=.\src\misc\espresso\verify.c
 # PROP Default_Filter ""
 # Begin Source File
 
+SOURCE=.\src\misc\util\port_type.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\util\util_hack.h
 # End Source File
 # End Group
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index ccc34caf..744a044e 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -521,9 +521,14 @@ extern Vec_Ptr_t *     Aig_ManSupports( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManSupportsInverse( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManSupportsRegisters( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
+extern Vec_Ptr_t *     Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose );
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
 extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
+/*=== aigPartReg.c =========================================================*/
+extern Vec_Ptr_t *     Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
+extern Vec_Ptr_t *     Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
+extern Aig_Man_t *     Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
 /*=== aigRepr.c =========================================================*/
 extern void            Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
 extern void            Aig_ManReprStop( Aig_Man_t * p );
@@ -532,6 +537,7 @@ extern void            Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepr( Aig_Man_t * p, int fOrdered );
 extern Aig_Man_t *     Aig_ManRehash( Aig_Man_t * p );
 extern void            Aig_ManMarkValidChoices( Aig_Man_t * p );
+extern int             Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack );
 /*=== aigRet.c ========================================================*/
 extern Aig_Man_t *     Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose );
 /*=== aigRetF.c ========================================================*/
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 7e765f60..df5792b2 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -772,6 +772,135 @@ if ( fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Perform the smart partitioning.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit, int fVerbose )
+{
+    Vec_Ptr_t * vPartSuppsBit;
+    Vec_Ptr_t * vSupports, * vPartsAll, * vPartsAll2, * vPartSuppsAll;
+    Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
+    int i, iPart, iOut, clk;
+
+    // add output number to each
+clk = clock();
+    vSupports = Aig_ManSupportsRegisters( pAig );
+    assert( Vec_PtrSize(vSupports) == Aig_ManRegNum(pAig) );
+    Vec_PtrForEachEntry( vSupports, vOne, i )
+        Vec_IntPush( vOne, i );
+if ( fVerbose )
+{
+PRT( "Supps", clock() - clk );
+}
+
+    // start char-based support representation
+    vPartSuppsBit = Vec_PtrAlloc( 1000 );
+
+    // create partitions
+clk = clock();
+    vPartsAll = Vec_PtrAlloc( 256 );
+    vPartSuppsAll = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vSupports, vOne, i )
+    {
+        // get the output number
+        iOut = Vec_IntPop(vOne);
+        // find closely matching part
+        iPart = Aig_ManPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsBit, nSuppSizeLimit, vOne );
+        if ( iPart == -1 )
+        {
+            // create new partition
+            vPart = Vec_IntAlloc( 32 );
+            Vec_IntPush( vPart, iOut );
+            // create new partition support
+            vPartSupp = Vec_IntDup( vOne );
+            // add this partition and its support
+            Vec_PtrPush( vPartsAll, vPart );
+            Vec_PtrPush( vPartSuppsAll, vPartSupp );
+
+            Vec_PtrPush( vPartSuppsBit, Aig_ManSuppCharStart(vOne, Vec_PtrSize(vSupports)) );
+        }
+        else
+        {
+            // add output to this partition
+            vPart = Vec_PtrEntry( vPartsAll, iPart );
+            Vec_IntPush( vPart, iOut );
+            // merge supports
+            vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
+            vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
+            Vec_IntFree( vTemp );
+            // reinsert new support
+            Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
+
+            Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Vec_PtrSize(vSupports) );
+        }
+    }
+
+    // stop char-based support representation
+    Vec_PtrForEachEntry( vPartSuppsBit, vTemp, i )
+        free( vTemp );
+    Vec_PtrFree( vPartSuppsBit );
+
+//printf( "\n" );
+if ( fVerbose )
+{
+PRT( "Parts", clock() - clk );
+}
+
+clk = clock();
+    // reorder partitions in the decreasing order of support sizes
+    // remember partition number in each partition support
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_IntPush( vOne, i );
+    // sort the supports in the decreasing order
+    Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
+    // reproduce partitions
+    vPartsAll2 = Vec_PtrAlloc( 256 );
+    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+        Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
+    Vec_PtrFree( vPartsAll );
+    vPartsAll = vPartsAll2;
+
+    // compact small partitions
+//    Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
+    Aig_ManPartitionCompact( vPartsAll, vPartSuppsAll, nSuppSizeLimit );
+    if ( fVerbose )
+//    Aig_ManPartitionPrint( p, vPartsAll, vPartSuppsAll );
+    printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
+
+if ( fVerbose )
+{
+//PRT( "Comps", clock() - clk );
+}
+
+    // cleanup
+    Vec_VecFree( (Vec_Vec_t *)vSupports );
+//    if ( pvPartSupps == NULL )
+        Vec_VecFree( (Vec_Vec_t *)vPartSuppsAll );
+//    else
+//        *pvPartSupps = vPartSuppsAll;
+
+/*
+    // converts from intergers to nodes
+    Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
+    {
+        vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
+        Vec_IntForEachEntry( vPart, iOut, i )
+            Vec_PtrPush( vPartPtr, Aig_ManPo(p, iOut) );
+        Vec_IntFree( vPart );
+        Vec_PtrWriteEntry( vPartsAll, iPart, vPartPtr );
+    }
+*/
+    return vPartsAll;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Perform the naive partitioning.]
 
   Description []
@@ -968,16 +1097,21 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     Vec_Ptr_t * vParts;
     Aig_Obj_t * pObj;
     void ** ppData;
-    int i, k, m;
+    int i, k, m, nIdMax;
+    assert( Vec_PtrSize(vAigs) > 1 );
+
+    // compute the total number of IDs
+    nIdMax = 0;
+    Vec_PtrForEachEntry( vAigs, pAig, i )
+        nIdMax += Aig_ManObjNumMax(pAig);
 
     // partition the first AIG in the array
-    assert( Vec_PtrSize(vAigs) > 1 );
     pAig = Vec_PtrEntry( vAigs, 0 );
     vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL );
 
     // start the total fraiged AIG
     pAigTotal = Aig_ManStartFrom( pAig );
-    Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 );
+    Aig_ManReprStart( pAigTotal, nIdMax );
     vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
 
     // set the PI numbers
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 1f218bd8..88ae66ee 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -59,14 +60,14 @@ struct Aig_ManPre_t_
   SeeAlso     []
 
 ***********************************************************************/
-Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig )
+Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig, int nPartSize )
 {
     Aig_ManPre_t * p;
     p = ALLOC( Aig_ManPre_t, 1 );
     memset( p, 0, sizeof(Aig_ManPre_t) );
     p->pAig      = pAig;
     p->vMatrix   = Aig_ManSupportsRegisters( pAig );
-    p->nRegsMax  = 500;
+    p->nRegsMax  = nPartSize;
     p->vParts    = Vec_PtrAlloc(256);
     p->vRegs     = Vec_IntAlloc(256);
     p->vUniques  = Vec_IntAlloc(256);
@@ -105,9 +106,10 @@ void Aig_ManRegManStop( Aig_ManPre_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the max-support register that is not taken yet.]
+  Synopsis    [Determines what register to use as the seed.]
 
-  Description []
+  Description [The register is selected as the one having the largest
+  number of non-taken registers in its support.]
                
   SideEffects []
 
@@ -116,12 +118,16 @@ void Aig_ManRegManStop( Aig_ManPre_t * p )
 ***********************************************************************/
 int Aig_ManRegFindSeed( Aig_ManPre_t * p )
 {
-    int i, iMax, nRegsCur, nRegsMax = -1;
+    Vec_Int_t * vRegs;
+    int i, k, iReg, iMax, nRegsCur, nRegsMax = -1;
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
         if ( p->pfUsedRegs[i] )
             continue;
-        nRegsCur = Vec_IntSize( Vec_PtrEntry(p->vMatrix,i) );
+        nRegsCur = 0;
+        vRegs = Vec_PtrEntry( p->vMatrix, i );
+        Vec_IntForEachEntry( vRegs, iReg, k )
+            nRegsCur += !p->pfUsedRegs[iReg];
         if ( nRegsMax < nRegsCur )
         {
             nRegsMax = nRegsCur;
@@ -157,7 +163,11 @@ int Aig_ManRegFindBestVar( Aig_ManPre_t * p )
         // count the number of new vars
         nNewVars = 0;
         Vec_IntForEachEntry( vSupp, iVarSupp, k )
-            nNewVars += !p->pfPartVars[iVarSupp];
+        {
+            if ( p->pfPartVars[iVarSupp] )
+                continue;
+            nNewVars += 1 + 3 * p->pfUsedRegs[iVarSupp];
+        }
         // quit if there is no new variables
         if ( nNewVars == 0 )
             return iVarFree;
@@ -229,14 +239,15 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs )
+Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
+    Aig_Obj_t * pObj, * pObjNew;
     Vec_Ptr_t * vNodes;
     Vec_Ptr_t * vRoots;
     int nOffset, iOut, i;
     int nCountPis, nCountRegs;
+    int * pMapBack;
     // collect roots
     vRoots = Vec_PtrAlloc( Vec_IntSize(vPart) );
     nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
@@ -275,6 +286,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
             pObj->pData = Aig_ObjCreatePi(pNew);
     // add variables for the register outputs
     // create fake POs to hold the register outputs
+    nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
     Vec_IntForEachEntry( vPart, iOut, i )
     {
         pObj = Aig_ManPi(pAig, nOffset+iOut);
@@ -285,7 +297,6 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
     Vec_PtrForEachEntry( vNodes, pObj, i )
         if ( Aig_ObjIsNode(pObj) )
             pObj->pData = Aig_And(pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    Vec_PtrFree( vNodes );
     // add real POs for the registers
     nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
     Vec_IntForEachEntry( vPart, iOut, i )
@@ -294,6 +305,30 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     }
     pNew->nRegs = Vec_IntSize(vPart);
+    // create map
+    if ( ppMapBack )
+    {
+        pMapBack = ALLOC( int, Aig_ManObjNumMax(pNew) );
+        memset( pMapBack, 0xff, sizeof(int) * Aig_ManObjNumMax(pNew) );
+        // map constant nodes
+        pMapBack[0] = 0;
+        // logic cones of register outputs
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+        {
+            pObjNew = Aig_Regular(pObj->pData);
+            pMapBack[pObjNew->Id] = pObj->Id;
+        }
+        // map register outputs
+        nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
+        Vec_IntForEachEntry( vPart, iOut, i )
+        {
+            pObj = Aig_ManPi(pAig, nOffset+iOut);
+            pObjNew = pObj->pData;
+            pMapBack[pObjNew->Id] = pObj->Id;
+        }
+        *ppMapBack = pMapBack;
+    }
+    Vec_PtrFree( vNodes );
     return pNew;
 }
 
@@ -308,7 +343,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig )
+Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize )
 {
     extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
 
@@ -316,11 +351,11 @@ Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig )
     Vec_Ptr_t * vResult;
     int iSeed, iNext, i, k;
     // create the manager
-    p = Aig_ManRegManStart( pAig );
+    p = Aig_ManRegManStart( pAig, nPartSize );
     // add partitions as long as registers remain
     for ( i = 0; (iSeed = Aig_ManRegFindSeed(p)) >= 0; i++ )
     {
-printf( "Seed variable = %d.\n", iSeed );
+//printf( "Seed variable = %d.\n", iSeed );
         // clean the current partition information
         Vec_IntClear( p->vRegs );
         Vec_IntClear( p->vUniques );
@@ -339,9 +374,9 @@ printf( "Seed variable = %d.\n", iSeed );
             // add the register to the support of the partition
             Aig_ManRegPartitionAdd( p, iNext );
             // report the result
-printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, 
-                Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
-                1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
+//printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, 
+//                Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
+//                1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
             // quit if there are not free variables
             if ( Vec_IntSize(p->vFreeVars) == 0 )
                 break;
@@ -351,7 +386,7 @@ printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4
 printf( "Part %3d  SUMMARY:  Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i,
                 Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
                 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
-printf( "\n" ); 
+//printf( "\n" ); 
     }
     vResult = p->vParts; p->vParts = NULL;
     Aig_ManRegManStop( p );
@@ -369,24 +404,34 @@ printf( "\n" );
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize )
+Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize )
 {
     Vec_Ptr_t * vResult;
     Vec_Int_t * vPart;
-    int i, k, nParts;
-    nParts = (Aig_ManRegNum(pAig) / nPartSize) + (int)(Aig_ManRegNum(pAig) % nPartSize > 0);
-    vResult = Vec_PtrAlloc( nParts );
-    for ( i = 0; i < nParts; i++ )
+    int i, Counter;
+    if ( nOverSize >= nPartSize )
+    {
+        printf( "Overlap size (%d) if more or equal to the partition size (%d).\n", nOverSize, nPartSize );
+        printf( "Adjusting it to be equal to half of the partition size.\n" );
+        nOverSize = nPartSize/2;
+    }
+    assert( nOverSize < nPartSize );
+    vResult = Vec_PtrAlloc( 100 );
+    for ( Counter = 0; Counter < Aig_ManRegNum(pAig); Counter -= nOverSize )
     {
         vPart = Vec_IntAlloc( nPartSize );
-        for ( k = 0; k < nPartSize; k++ )
-            if ( i * nPartSize + k < Aig_ManRegNum(pAig) )
-                Vec_IntPush( vPart, i * nPartSize + k );
-        Vec_PtrPush( vResult, vPart );
+        for ( i = 0; i < nPartSize; i++ )
+            if ( ++Counter < Aig_ManRegNum(pAig) )
+                Vec_IntPush( vPart, Counter );
+        if ( Vec_IntSize(vPart) <= nOverSize )
+            Vec_IntFree(vPart);
+        else
+            Vec_PtrPush( vResult, vPart );
     }
     return vResult;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Computes partitioning of registers.]
@@ -398,26 +443,77 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManRegPartitionRun( Aig_Man_t * pAig )
+void Aig_ManRegPartitionTraverse_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLos )
 {
-    int nPartSize = 1000;
-    char Buffer[100];
-    Aig_Man_t * pTemp;
-    Vec_Ptr_t * vResult;
-    Vec_Int_t * vPart;
-    int i, nCountPis, nCountRegs;
-    vResult = Aig_ManRegPartitionSimple( pAig, nPartSize );
-    printf( "Simple partitioning: %d partitions are saved:\n", Vec_PtrSize(vResult) );
-    Vec_PtrForEachEntry( vResult, vPart, i )
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    if ( Aig_ObjIsPi(pObj) )
     {
-        sprintf( Buffer, "part%03d.aig", i );
-        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs );
-        Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
-        printf( "part%03d.aig : Regs = %4d. PIs = %4d. (True PIs = %4d. Other regs = %4d.)\n", 
-            i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs );
-        Aig_ManStop( pTemp );
+        if ( pObj->iData >= Aig_ManPiNum(p) - Aig_ManRegNum(p) )
+        {
+            Vec_PtrPush( vLos, pObj );
+            printf( "%d ", pObj->iData - (Aig_ManPiNum(p) - Aig_ManRegNum(p)) );
+        }
+        return;
     }
-    Vec_VecFree( (Vec_Vec_t *)vResult );
+    Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin0(pObj), vLos );
+    Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin1(pObj), vLos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegPartitionTraverse( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vLos;
+    Aig_Obj_t * pObj;
+    int i, nPrev, Counter;
+    // mark the registers
+    Aig_ManForEachPi( p, pObj, i )
+       pObj->iData = i; 
+    // collect registers
+    vLos = Vec_PtrAlloc( Aig_ManRegNum(p) );
+    nPrev = 0;
+    Counter = 0;
+    Aig_ManIncrementTravId( p );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        ++Counter;
+        printf( "Latch %d: ", Counter );
+        Aig_ManRegPartitionTraverse_rec( p, Aig_ObjFanin0(pObj), vLos );
+printf( "%d=%d \n", Counter, Vec_PtrSize(vLos)-nPrev );
+        nPrev = Vec_PtrSize(vLos);
+    }
+    printf( "Total collected = %d. Total regs = %d.\n", Vec_PtrSize(vLos), Aig_ManRegNum(p) );
+    return vLos;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize )
+{
+    Vec_Ptr_t * vLos;
+    vLos = Aig_ManRegPartitionTraverse( pAig );
+    Vec_PtrFree( vLos );
+    return NULL;
 }
 
 
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 3a7e382c..eb4325f4 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -443,6 +443,11 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
         }
 //printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
         // add choice to the choice node
+        if ( pObj->nRefs > 0 )
+        {
+            Aig_ObjClearRepr( p, pObj );
+            continue;
+        }
         assert( pObj->nRefs == 0 );
         p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
         p->pEquivs[pRepr->Id] = pObj;
@@ -450,6 +455,36 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Transfers the classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBack )
+{
+    Aig_Obj_t * pObj;
+    int nClasses, k;
+    nClasses = 0;
+    if ( pPart->pReprs )
+    Aig_ManForEachObj( pPart, pObj, k )
+    {
+        if ( pPart->pReprs[pObj->Id] == NULL )
+            continue;
+        nClasses++;
+        Aig_ObjSetRepr( pAig, 
+            Aig_ManObj(pAig, pMapBack[pObj->Id]), 
+            Aig_ManObj(pAig, pMapBack[pPart->pReprs[pObj->Id]->Id]) );
+    }
+    return nClasses;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 70586c68..d8ffda9a 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -376,10 +376,14 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose )
         printf( "RBeg = %5d. NBeg = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
         }
         vMap = Aig_ManReduceLachesOnce( p );
+//Aig_ManPrintStats( p );
         p = Aig_ManRemap( pTemp = p, vMap );
+//Aig_ManPrintStats( p );
         Aig_ManStop( pTemp );
         Vec_PtrFree( vMap );
         Aig_ManSeqCleanup( p );
+//Aig_ManPrintStats( p );
+//printf( "\n" );
         if ( fVerbose )
         {
         printf( "REnd = %5d. NEnd = %6d.   ", Aig_ManRegNum(p), Aig_ManNodeNum(p) );
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index a8a3dda8..1d974778 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #define TSI_MAX_ROUNDS    1000
+#define TSI_ONE_SERIES     300
 
 #define AIG_XVS0   1
 #define AIG_XVS1   2
@@ -282,6 +283,51 @@ void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
     printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Count constant values in the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TsiStateCount( Aig_Tsi_t * p, unsigned * pState )
+{
+    Aig_Obj_t * pObjLi, * pObjLo;
+    int i, Value, nCounter = 0;
+    Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
+    {
+        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        nCounter += (Value == 1 || Value == 2);
+    }
+    return nCounter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count constant values in the state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TsiStateOrAll( Aig_Tsi_t * pTsi, unsigned * pState )
+{
+    unsigned * pPrev;
+    int i, k;
+    Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
+    {
+        for ( k = 0; k < pTsi->nWords; k++ )
+            pState[k] |= pPrev[k];
+    }
+}
+
 
 /**Function*************************************************************
 
@@ -300,8 +346,8 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     Aig_Tsi_t * pTsi;
     Vec_Ptr_t * vMap;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    unsigned * pState, * pPrev;
-    int i, k, f, fConstants, Value, nCounter;
+    unsigned * pState;//, * pPrev;
+    int i, f, fConstants, Value, nCounter;
     // allocate the simulation manager
     pTsi = Aig_TsiStart( p );
     // initialize the values
@@ -323,10 +369,16 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
             if ( Value & 2 )
                 Aig_InfoSetBit( pState, 2 * i + 1 );
         }
+
+//        printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
 //        Aig_TsiStatePrint( pTsi, pState );
         // check if this state exists
         if ( Aig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
             break;
+//        nCounter = 0;
+//        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+//            nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
+//printf( "%d -> ", nCounter );
         // insert this state
         Aig_TsiStateInsert( pTsi, pState, pTsi->nWords );
         // simulate internal nodes
@@ -335,9 +387,23 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
         // transfer the latch values
         Aig_ManForEachLiSeq( p, pObj, i )
             Aig_ObjSetXsim( pObj, Aig_ObjGetXsimFanin0(pObj) );
+        nCounter = 0;
         Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-            Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
+        {
+            if ( f < TSI_ONE_SERIES )
+                Aig_ObjSetXsim( pObjLo, Aig_ObjGetXsim(pObjLi) );
+            else
+            {
+                if ( Aig_ObjGetXsim(pObjLi) != Aig_ObjGetXsim(pObjLo) )
+                    Aig_ObjSetXsim( pObjLo, AIG_XVSX );
+            }
+            nCounter += (Aig_ObjGetXsim(pObjLo) == AIG_XVS0);
+        }
+//        if ( f && (f % 1000 == 0) )
+//            printf( "%d \n", f );
+//printf( "%d  ", nCounter );
     }
+//printf( "\n" );
     if ( f == TSI_MAX_ROUNDS )
     {
         printf( "Aig_ManTernarySimulate(): Did not reach a fixed point after %d iterations (not a bug).\n", TSI_MAX_ROUNDS );
@@ -346,11 +412,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
     }
     // OR all the states
     pState = Vec_PtrEntry( pTsi->vStates, 0 );
-    Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
-    {
-        for ( k = 0; k < pTsi->nWords; k++ )
-            pState[k] |= pPrev[k];
-    }
+    Aig_TsiStateOrAll( pTsi, pState );
     // check if there are constants
     fConstants = 0;
     if ( 2*Aig_ManRegNum(p) == 32*pTsi->nWords )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 2ee84f39..cc64b024 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -50,6 +50,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Fra_Par_t_   Fra_Par_t;
+typedef struct Fra_Ssw_t_   Fra_Ssw_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
@@ -86,6 +87,25 @@ struct Fra_Par_t_
     int              fDontShowBar;      // does not show progressbar during fraiging
 };
 
+// seq SAT sweeping parametesr
+struct Fra_Ssw_t_
+{
+    int              nPartSize;         // size of the partition
+    int              nOverSize;         // size of the overlap between partitions
+    int              nFramesP;          // number of frames in the prefix
+    int              nFramesK;          // number of frames for induction (1=simple) 
+    int              nMaxImps;          // max implications to consider
+    int              nMaxLevs;          // max levels to consider
+    int              fUseImps;          // use implications  
+    int              fRewrite;          // enable rewriting of the specualatively reduced model
+    int              fFraiging;         // enable comb SAT sweeping as preprocessing 
+    int              fLatchCorr;        // perform register correspondence
+    int              fWriteImps;        // write implications into a file
+    int              fUse1Hot;          // use one-hotness constraints
+    int              fVerbose;          // enable verbose output 
+    int              nIters;            // the number of iterations performed
+};
+
 // FRAIG equivalence classes
 struct Fra_Cla_t_
 {
@@ -287,7 +307,7 @@ extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
 extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
 extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, Fra_Ssw_t * pPars );
 /*=== fraIndVer.c =====================================================*/
 extern int                 Fra_InvariantVerify( Aig_Man_t * p, int nFrames, Vec_Int_t * vClauses, Vec_Int_t * vLits );
 /*=== fraLcr.c ========================================================*/
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ea17706c..0715524e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -234,7 +234,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs choicing of the AIG.]
+  Synopsis    [Performs partitioned sequential SAT sweepingG.]
 
   Description []
                
@@ -243,7 +243,77 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+    int fPrintParts = 0;
+    char Buffer[100];
+    Aig_Man_t * pTemp, * pNew;
+    Vec_Ptr_t * vResult;
+    Vec_Int_t * vPart;
+    int * pMapBack;
+    int i, nCountPis, nCountRegs;
+    int nClasses, nPartSize, fVerbose;
+
+    // save parameters
+    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+    fVerbose  = pPars->fVerbose;  pPars->fVerbose = 0;
+    // generate partitions
+    vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
+//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+    if ( fPrintParts )
+    {
+        // print partitions
+        printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+        Vec_PtrForEachEntry( vResult, vPart, i )
+        {
+            sprintf( Buffer, "part%03d.aig", i );
+            pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
+            Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+            printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+            Aig_ManStop( pTemp );
+        }
+    }
+
+    // perform SSW with partitions
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Vec_PtrForEachEntry( vResult, vPart, i )
+    {
+        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        // run SSW
+        pNew = Fra_FraigInduction( pTemp, pPars );
+        nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+        if ( fVerbose )
+            printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+        Aig_ManStop( pNew );
+        Aig_ManStop( pTemp );
+        free( pMapBack );
+    }
+    // remap the AIG
+    pNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pNew );
+//    Aig_ManPrintStats( pAig );
+//    Aig_ManPrintStats( pNew );
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+    pPars->nPartSize = nPartSize;
+    pPars->fVerbose = fVerbose;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sequential SAT sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
 {
     int fUseSimpleCnf = 0;
     int fUseOldSimulation = 0;
@@ -263,13 +333,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
-        if ( pnIter ) *pnIter = 0;
+        pParams->nIters = 0;
         return Aig_ManDup(pManAig, 1);
     }
     assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
-    assert( nFramesK > 0 );
+    assert( pParams->nFramesK > 0 );
 //Aig_ManShow( pManAig, 0, NULL );
+
+    if ( pParams->fWriteImps && pParams->nPartSize > 0 )
+    {
+        pParams->nPartSize = 0;
+        printf( "Partitioning was disabled to allow implication writing.\n" );
+    }
+    // perform partitioning
+    if ( pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig) )
+        return Fra_FraigInductionPart( pManAig, pParams );
  
     nNodesBeg = Aig_ManNodeNum(pManAig);
     nRegsBeg  = Aig_ManRegNum(pManAig);
@@ -279,16 +358,16 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
-    pPars->nFramesP   = nFramesP;
-    pPars->nFramesK   = nFramesK;
-    pPars->nMaxImps   = nMaxImps;
-    pPars->nMaxLevs   = nMaxLevs;
-    pPars->fVerbose   = fVerbose;
-    pPars->fRewrite   = fRewrite;
-    pPars->fLatchCorr = fLatchCorr;
-    pPars->fUseImps   = fUseImps;
-    pPars->fWriteImps = fWriteImps;
-    pPars->fUse1Hot   = fUse1Hot;
+    pPars->nFramesP   = pParams->nFramesP;
+    pPars->nFramesK   = pParams->nFramesK;
+    pPars->nMaxImps   = pParams->nMaxImps;
+    pPars->nMaxLevs   = pParams->nMaxLevs;
+    pPars->fVerbose   = pParams->fVerbose;
+    pPars->fRewrite   = pParams->fRewrite;
+    pPars->fLatchCorr = pParams->fLatchCorr;
+    pPars->fUseImps   = pParams->fUseImps;
+    pPars->fWriteImps = pParams->fWriteImps;
+    pPars->fUse1Hot   = pParams->fUse1Hot;
 
     assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
     assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
@@ -311,10 +390,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
         // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // refine the classes with more simulation rounds
-if ( fVerbose )
+if ( pPars->fVerbose )
 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
         p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
-if ( fVerbose ) 
+if ( pPars->fVerbose ) 
 {
 PRT( "Time", clock() - clk );
 }
@@ -408,7 +487,7 @@ p->timeTrav += clock() - clk2;
             Fra_OneHotAssume( p, p->vOneHots );
 
         // report the intermediate results
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
@@ -428,7 +507,7 @@ clk2 = clock();
         if ( p->pPars->fUse1Hot )
             Fra_OneHotCheck( p, p->vOneHots );
         Fra_FraigSweep( p );
-        if ( fVerbose )
+        if ( pPars->fVerbose )
         {
 //            PRT( "t", clock() - clk2 ); 
         } 
@@ -508,7 +587,7 @@ p->timeTotal = clock() - clk;
 //    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
 //        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
 //            printf( "Proved output constant 0.\n" );
-    if ( pnIter ) *pnIter = nIter;
+    pParams->nIters = nIter;
     return pManAigNew;
 }
 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index a43d83b1..75d297cf 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,73 +40,17 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
-{
-    Aig_Man_t * pNew;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
-    int fLatchCorr = 0;
-    if ( nFramesFix )
-    {
-        nFrames = nFramesFix;
-        // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
-    }
-    else
-    {
-        // perform seq sweeping while increasing the number of frames
-        for ( nFrames = 1; ; nFrames++ )
-        {
-clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
-            RetValue = Fra_FraigMiterStatus( pNew );
-            if ( fVerbose )
-            {
-                printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
-                if ( RetValue == 1 )
-                    printf( "UNSAT     " );
-                else
-                    printf( "UNDECIDED " );
-PRT( "Time", clock() - clk );
-            }
-            if ( RetValue != -1 )
-                break;
-            Aig_ManStop( pNew );
-        }
-    }
-
-    // get the miter status
-    RetValue = Fra_FraigMiterStatus( pNew );
-    Aig_ManStop( pNew );
-
-    // report the miter
-    if ( RetValue == 1 )
-        printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-    else if ( RetValue == 0 )
-        printf( "Networks are NOT EQUIVALENT. " );
-    else
-        printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-PRT( "Time", clock() - clkTotal );
-    return RetValue;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
+    Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
+    // prepare parameters
+    memset( pPars, 0, sizeof(Fra_Ssw_t) );
+    pPars->fLatchCorr  = fLatchCorr;
+    pPars->fVerbose = fVeryVerbose;
 
     pNew = Aig_ManDup( p, 1 );
     if ( fVerbose )
@@ -185,13 +129,14 @@ PRT( "Time", clock() - clk );
     for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
 clk = clock();
-        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, 0, fLatchCorr, 0, 0, fVeryVerbose, &nIter );
+        pPars->nFramesK = nFrames;
+        pNew = Fra_FraigInduction( pTemp = pNew, pPars );
         Aig_ManStop( pTemp );
         RetValue = Fra_FraigMiterStatus( pNew );
         if ( fVerbose )
         { 
             printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
-                nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+                nFrames, pPars->nIters, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
         if ( RetValue != -1 )
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index fdff8b39..86cc7e62 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -567,6 +567,8 @@ extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag,
 extern void               Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
 extern void *             Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
 extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
+/*=== abcDelay.c ==========================================================*/
+extern float              Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
 /*=== abcDfs.c ==========================================================*/
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
@@ -733,7 +735,7 @@ extern bool               Abc_NodeIsBuf( Abc_Obj_t * pNode );
 extern bool               Abc_NodeIsInv( Abc_Obj_t * pNode );    
 extern void               Abc_NodeComplement( Abc_Obj_t * pNode );
 /*=== abcPrint.c ==========================================================*/
-extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest );
+extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
 extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 492d1910..99da9201 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -30,6 +30,7 @@
 #include "aig.h"
 #include "dar.h"
 #include "mfs.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -442,6 +443,8 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int fFactor;
     int fSaveBest;
+    int fDumpResult;
+    int fUseLutLib;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -451,8 +454,10 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set the defaults
     fFactor   = 0;
     fSaveBest = 0;
+    fDumpResult = 0;
+    fUseLutLib = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "fbh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -462,6 +467,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             fSaveBest ^= 1;
             break;
+        case 'd':
+            fDumpResult ^= 1;
+            break;
+        case 'l':
+            fUseLutLib ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -474,14 +485,16 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
         return 1;
     }
-    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest );
+    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_stats [-fbh]\n" );
+    fprintf( pErr, "usage: print_stats [-fbdlh]\n" );
     fprintf( pErr, "\t        prints the network statistics\n" );
     fprintf( pErr, "\t-f    : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-b    : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
+    fprintf( pErr, "\t-d    : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" );
+    fprintf( pErr, "\t-l    : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -567,7 +580,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
         printf( "EXDC network statistics: \n" );
-    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0 );
+    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 );
     return 0;
 
 usage:
@@ -672,7 +685,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fPrintSccs = 0;
+    fPrintSccs = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
     {
@@ -6829,7 +6842,8 @@ usage:
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    Abc_Ntk_t * pNtk;
+//    Abc_Ntk_t * pNtkRes;
     int c;
     int fBmc;
     int nFrames;
@@ -6849,14 +6863,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
-    extern void Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
+//    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
-//    printf( "This command is temporarily disabled.\n" );
-//    return 0;
+    printf( "This command is temporarily disabled.\n" );
+    return 0;
 
     // set defaults
     fVeryVerbose = 0;
@@ -7032,8 +7046,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_NtkDarTestBlif( argv[globalUtilOptind] );
 */
 
-    Abc_NtkDarPartition( pNtk );
-
+//    Abc_NtkDarPartition( pNtk );
+/*
+    pNtkRes = Abc_NtkDarPartition( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
     return 0;
 usage:
     fprintf( pErr, "usage: test [-vwh]\n" );
@@ -10825,6 +10848,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         // get LUT size from the library
         pPars->nLutSize = pPars->pLutLib->LutMax;
+        // if variable pin delay, force truth table computation
+        if ( pPars->pLutLib->fVarPinDelays )
+            pPars->fTruth = 1;
     }
 
     if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
@@ -11646,6 +11672,7 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -11665,12 +11692,14 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fForward;
     int fBackward;
     int fVerbose;
-    int fComputeInit;
+    int fComputeInit, fGuaranteeInit, fBlockConst;
+    int fFastButConservative;
     int maxDelay;
 
-    extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInit,
+    extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, 
+                                             int fComputeInit, int fGuaranteeInit, int fBlockConst,
                                              int fForward, int fBackward, int nMaxIters,
-                                             int maxDelay);
+                                             int maxDelay, int fFastButConservative);
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -11678,13 +11707,16 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fForward  =  0;
+    fFastButConservative = 0;
     fBackward =  0;
     fComputeInit =  1;
+    fGuaranteeInit =  0;
     fVerbose  =  0;
+    fBlockConst  =  0;
     nMaxIters = 999;
     maxDelay  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MDfbivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MDfcgbkivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -11709,16 +11741,25 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
             globalUtilOptind++;
             if ( maxDelay < 0 ) 
                 goto usage;
-            break;
+           break;
         case 'f':
             fForward ^= 1;
             break;
+        case 'c':
+            fFastButConservative ^= 1;
+            break;
         case 'i':
             fComputeInit ^= 1;
             break;
         case 'b':
             fBackward ^= 1;
             break;
+        case 'g':
+            fGuaranteeInit ^= 1;
+            break;
+        case 'k':
+            fBlockConst ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -11741,6 +11782,12 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( fGuaranteeInit && !fComputeInit )
+    {
+      fprintf( pErr, "Initial state guarantee (-g) requires initial state computation (-i).\n" );
+      return 1;
+    }
+
     if ( !Abc_NtkLatchNum(pNtk) )
     {
         fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
@@ -11754,7 +11801,10 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
       }
 
     // perform the retiming
-    pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit, fForward, fBackward, nMaxIters, maxDelay );
+    pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit,
+                                     fGuaranteeInit, fBlockConst, 
+                                     fForward, fBackward, 
+                                     nMaxIters, maxDelay, fFastButConservative );
 
     if (pNtkRes != pNtk)
       Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -11767,6 +11817,9 @@ usage:
     fprintf( pErr, "\t-M num : the maximum number of iterations [default = %d]\n", nMaxIters );
     fprintf( pErr, "\t-D num : the maximum delay [default = none]\n" );
     fprintf( pErr, "\t-i     : enables init state computation [default = %s]\n", fComputeInit? "yes": "no" );
+    fprintf( pErr, "\t-k     : blocks retiming over const nodes [default = %s]\n", fBlockConst? "yes": "no" );
+    fprintf( pErr, "\t-g     : guarantees init state computation [default = %s]\n", fGuaranteeInit? "yes": "no" );
+    fprintf( pErr, "\t-c     : very fast (but conserv.) delay constraints [default = %s]\n", fFastButConservative? "yes": "no" );
     fprintf( pErr, "\t-f     : enables forward-only retiming  [default = %s]\n", fForward? "yes": "no" );
     fprintf( pErr, "\t-b     : enables backward-only retiming [default = %s]\n", fBackward? "yes": "no" );
     fprintf( pErr, "\t-v     : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -12044,38 +12097,30 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
+    Fra_Ssw_t Pars, * pPars = &Pars;
     int c;
-    int nFramesP;
-    int nFramesK;
-    int nMaxImps;
-    int nMaxLevs;
-    int fUseImps;
-    int fRewrite;
-    int fFraiging;
-    int fLatchCorr;
-    int fWriteImps;
-    int fUse1Hot;
-    int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFramesP   = 0;
-    nFramesK   = 1;
-    nMaxImps   = 5000;
-    nMaxLevs   = 0;
-    fUseImps   = 0;
-    fRewrite   = 0;
-    fFraiging  = 0;
-    fLatchCorr = 0;
-    fWriteImps = 0;
-    fUse1Hot   = 0;
-    fVerbose   = 0;
+    pPars->nPartSize  = 0;
+    pPars->nOverSize  = 0;
+    pPars->nFramesP   = 0;
+    pPars->nFramesK   = 1;
+    pPars->nMaxImps   = 5000;
+    pPars->nMaxLevs   = 0;
+    pPars->fUseImps   = 0;
+    pPars->fRewrite   = 0;
+    pPars->fFraiging  = 0;
+    pPars->fLatchCorr = 0;
+    pPars->fWriteImps = 0;
+    pPars->fUse1Hot   = 0;
+    pPars->fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirfletvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -12085,9 +12130,31 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFramesP = atoi(argv[globalUtilOptind]);
+            pPars->nPartSize = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFramesP < 0 ) 
+            if ( pPars->nPartSize < 2 ) 
+                goto usage;
+            break;
+        case 'Q':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nOverSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nOverSize < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesP < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -12096,9 +12163,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFramesK = atoi(argv[globalUtilOptind]);
+            pPars->nFramesK = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFramesK <= 0 ) 
+            if ( pPars->nFramesK <= 0 ) 
                 goto usage;
             break;
         case 'I':
@@ -12107,9 +12174,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nMaxImps = atoi(argv[globalUtilOptind]);
+            pPars->nMaxImps = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nMaxImps <= 0 ) 
+            if ( pPars->nMaxImps <= 0 ) 
                 goto usage;
             break;
         case 'L':
@@ -12118,31 +12185,31 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nMaxLevs = atoi(argv[globalUtilOptind]);
+            pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nMaxLevs <= 0 ) 
+            if ( pPars->nMaxLevs <= 0 ) 
                 goto usage;
             break;
         case 'i':
-            fUseImps ^= 1;
+            pPars->fUseImps ^= 1;
             break;
         case 'r':
-            fRewrite ^= 1;
+            pPars->fRewrite ^= 1;
             break;
         case 'f':
-            fFraiging ^= 1;
+            pPars->fFraiging ^= 1;
             break;
         case 'l':
-            fLatchCorr ^= 1;
+            pPars->fLatchCorr ^= 1;
             break;
         case 'e':
-            fWriteImps ^= 1;
+            pPars->fWriteImps ^= 1;
             break;
         case 't':
-            fUse1Hot ^= 1;
+            pPars->fUse1Hot ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -12169,20 +12236,20 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
-    if ( nFramesK > 1 && fUse1Hot )
+    if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
     {
         printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
         return 0;
     }
 
-    if ( nFramesP && fUse1Hot )
+    if ( pPars->nFramesP && pPars->fUse1Hot )
     {
         printf( "Currrently can only use one-hotness without prefix.\n" );
         return 0;
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fFraiging, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose );
+    pNtkRes = Abc_NtkDarSeqSweep( pNtk, pPars );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -12193,19 +12260,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrfetvh]\n" );
+    fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
-    fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
-    fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
-    fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps );
-    fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", nMaxLevs );
-    fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
-    fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
-    fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
-    fprintf( pErr, "\t-f     : toggle fraiging (combinational SAT sweeping) [default = %s]\n", fFraiging? "yes": "no" );
-    fprintf( pErr, "\t-e     : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" );
-    fprintf( pErr, "\t-t     : toggle using one-hotness conditions [default = %s]\n", fUse1Hot? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
+    fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
+    fprintf( pErr, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
+    fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
+    fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
+//    fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
+//    fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
+    fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" );
+    fprintf( pErr, "\t-e     : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" );
+    fprintf( pErr, "\t-t     : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -12331,29 +12400,29 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    int fLatchSweep;
-    int fAutoSweep;
+    int fLatchConst;
+    int fLatchEqual;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fLatchSweep = 0;
-    fAutoSweep  = 0;
+    fLatchConst = 1;
+    fLatchEqual = 1;
     fVerbose    = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'l':
-            fLatchSweep ^= 1;
+        case 'c':
+            fLatchConst ^= 1;
             break;
-        case 'a':
-            fAutoSweep ^= 1;
+        case 'e':
+            fLatchEqual ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -12380,7 +12449,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose );
+    pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential cleanup has failed.\n" );
@@ -12391,13 +12460,11 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scleanup [-lvh]\n" );
-    fprintf( pErr, "\t         performs sequential cleanup\n" );
-    fprintf( pErr, "\t         - removes nodes/latches that do not feed into POs\n" );
-    fprintf( pErr, "\t         - removes stuck-at and identical latches (latch sweep)\n" );
-//    fprintf( pErr, "\t         - replaces autonomous logic by free PI variables\n" );
-    fprintf( pErr, "\t-l     : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
-//    fprintf( pErr, "\t-a     : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
+    fprintf( pErr, "usage: scleanup [-cevh]\n" );
+    fprintf( pErr, "\t         performs sequential cleanup of the current network\n" );
+    fprintf( pErr, "\t         by removing nodes and latches that do not feed into POs\n" );
+    fprintf( pErr, "\t-c     : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
+    fprintf( pErr, "\t-e     : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -13901,7 +13968,7 @@ usage:
     fprintf( pErr, "\t         perform bounded model checking\n" );
     fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
-    fprintf( pErr, "\t-r     : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 119a2a97..6f5138c8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -263,6 +263,25 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         Abc_NtkAddDummyBoxNames( pNtkNew );
     else
     {
+        {
+            int i, k, iFlop, Counter = 0;
+            FILE * pFile;
+            pFile = fopen( "out.txt", "w" );
+            fprintf( pFile, "The total of %d registers were removed (out of %d):\n", 
+                Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) );
+            for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ )
+            {
+                Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k )
+                {
+                    if ( i == iFlop )
+                        break;
+                }
+                if ( k == Vec_IntSize(pMan->vFlopNums) )
+                    fprintf( pFile, "%6d (%6d)  :  %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) );
+            }
+            fclose( pFile );
+            //printf( "\n" );
+        }
         assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
         nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
         Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@@ -1034,7 +1053,7 @@ PRT( "Time", clock() - clkTotal );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
@@ -1046,21 +1065,23 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in
     // so fraiging does not reduce the number of functions represented by nodes
     Fraig_ParamsSetDefault( &Params );
     Params.nBTLimit = 100000;
-    if ( fFraiging )
+    if ( pPars->fFraiging && pPars->nPartSize == 0 )
+    {
         pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
-    else
-        pNtkFraig = Abc_NtkDup( pNtk );
-if ( fVerbose ) 
+if ( pPars->fVerbose ) 
 {
 PRT( "Initial fraiging time", clock() - clk );
 }
+    }
+    else
+        pNtkFraig = Abc_NtkDup( pNtk );
 
     pMan = Abc_NtkToDar( pNtkFraig, 1 );
     Abc_NtkDelete( pNtkFraig );
     if ( pMan == NULL )
         return NULL;
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, pPars );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -1283,7 +1304,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan;
@@ -1291,13 +1312,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos
     if ( pMan == NULL )
         return NULL;
     Aig_ManSeqCleanup( pMan );
-    if ( fLatchSweep )
-    {
-        if ( pMan->nRegs )
-            pMan = Aig_ManReduceLaches( pMan, fVerbose );
-        if ( pMan->nRegs )
-            pMan = Aig_ManConstReduce( pMan, fVerbose );
-    }
+    if ( fLatchConst && pMan->nRegs )
+        pMan = Aig_ManConstReduce( pMan, fVerbose );
+    if ( fLatchEqual && pMan->nRegs )
+        pMan = Aig_ManReduceLaches( pMan, fVerbose );
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     Aig_ManStop( pMan );
     return pNtkAig;
@@ -1557,41 +1575,16 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
 ***********************************************************************/
 void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
 {
+//    extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
         return;
     Aig_ManComputeSccs( pMan );
+//    Aig_ManRegPartitionLinear( pMan, 1000 );
     Aig_ManStop( pMan );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Performs partitioning.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkDarPartition( Abc_Ntk_t * pNtk )
-{
-    extern void Aig_ManRegPartitionRun( Aig_Man_t * pAig );
-    Aig_Man_t * pMan;
-
-    // convert to the AIG manager
-    assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 1 );
-    if ( pMan == NULL )
-        return;
-
-    Aig_ManRegPartitionRun( pMan );
-    Aig_ManStop( pMan );
-}
-
-
 
 #include "ntl.h"
 
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index 7317b41b..bb654b73 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -74,7 +74,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
         pPinPerm[best_i] = temp;
     }
     // verify
-    assert( pPinPerm[0] < Abc_ObjFaninNum(pNode) );
+    assert( Abc_ObjFaninNum(pNode) == 0 || pPinPerm[0] < Abc_ObjFaninNum(pNode) );
     for ( i = 1; i < Abc_ObjFaninNum(pNode); i++ )
     {
         assert( pPinPerm[i] < Abc_ObjFaninNum(pNode) );
@@ -96,6 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
 float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
 {
     extern void * Abc_FrameReadLibLut();   
+    int fUseSorting = 0;
     int pPinPerm[32];
     float pPinDelays[32];
     If_Lib_t * pLutLib;
@@ -144,10 +145,19 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
         else
         {
             pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
-            Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-            Abc_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] )
-                    tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k];
+            if ( fUseSorting )
+            {
+                Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
+                Abc_ObjForEachFanin( pNode, pFanin, k ) 
+                    if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] )
+                        tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k];
+            }
+            else
+            {
+                Abc_ObjForEachFanin( pNode, pFanin, k )
+                    if ( tArrival < Abc_ObjArrival(pFanin) + pDelays[k] )
+                        tArrival = Abc_ObjArrival(pFanin) + pDelays[k];
+            }
         }
         if ( Abc_ObjFaninNum(pNode) == 0 )
             tArrival = 0.0;
@@ -188,12 +198,24 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
         else 
         {
             pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
-            Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-            Abc_ObjForEachFanin( pNode, pFanin, k )
+            if ( fUseSorting )
             {
-                tRequired = Abc_ObjRequired(pNode) - pDelays[k];
-                if ( Abc_ObjRequired(Abc_ObjFanin(pNode,pPinPerm[k])) > tRequired )
-                    Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired );
+                Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
+                Abc_ObjForEachFanin( pNode, pFanin, k )
+                {
+                    tRequired = Abc_ObjRequired(pNode) - pDelays[k];
+                    if ( Abc_ObjRequired(Abc_ObjFanin(pNode,pPinPerm[k])) > tRequired )
+                        Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired );
+                }
+            }
+            else
+            {
+                Abc_ObjForEachFanin( pNode, pFanin, k )
+                {
+                    tRequired = Abc_ObjRequired(pNode) - pDelays[k];
+                    if ( Abc_ObjRequired(pFanin) > tRequired )
+                        Abc_ObjSetRequired( pFanin, tRequired );
+                }
             }
         }
         // set slack for this object
@@ -265,8 +287,17 @@ unsigned Abc_NtkDelayTraceTCEdges( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, float tD
 void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
 {
     Abc_Obj_t * pNode;
+    If_Lib_t * pLutLib;
     int i, Nodes, * pCounters;
     float tArrival, tDelta, nSteps, Num;
+    // get the library
+    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
+    if ( pLutLib && pLutLib->LutMax < Abc_NtkGetFaninMax(pNtk) )
+    {
+        printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
+            pLutLib->LutMax, Abc_NtkGetFaninMax(pNtk) );
+        return;
+    }
     // decide how many steps
     nSteps = fUseLutLib ? 20 : Abc_NtkLevel(pNtk);
     pCounters = ALLOC( int, nSteps + 1 );
@@ -277,6 +308,8 @@ void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
     // count how many nodes have slack in the corresponding intervals
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
         Num = Abc_ObjSlack(pNode) / tDelta;
         assert( Num >=0 && Num <= nSteps );
         pCounters[(int)Num]++;
@@ -356,15 +389,20 @@ int Abc_AigCheckTfi( Abc_Obj_t * pNew, Abc_Obj_t * pOld )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+int Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 {
     if ( Abc_NodeIsTravIdCurrent(pNode) )
-        return;
+        return 1;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
     assert( Abc_ObjIsNode(pNode) );
     Abc_NodeSetTravIdCurrent( pNode );
-    Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes );
-    Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes );
+    if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes ) )
+        return 0;
+    if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes ) )
+        return 0;
     Vec_PtrPush( vNodes, pNode );
+    return 1;
 }
 
 /**Function*************************************************************
@@ -405,7 +443,12 @@ void Abc_NtkSpeedupNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pAig, Abc_Obj_t * pNode,
     }
     // traverse from the root node
     pAnd = pNode->pCopy;
-    Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes );
+    if ( !Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes ) )
+    {
+//        printf( "Bad node!!!\n" );
+        Vec_PtrFree( vNodes );
+        return;
+    }
 
     // derive cofactors
     nCofs = (1 << Vec_PtrSize(vTimes));
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 5d24398b..742a3a02 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -252,6 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     // create a new node 
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
+    if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
+        If_CutRotatePins( pIfMan, pCutBest );
     if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
     {
         If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 5d35f329..239b155c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -111,12 +111,20 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib )
 {
     int Num;
 
     if ( fSaveBest )
         Abc_NtkCompareAndSaveBest( pNtk );
+    if ( fDumpResult )
+    {
+        char Buffer[1000] = {0};
+        char * pNameGen = pNtk->pSpec? Extra_FileNameGeneric( pNtk->pSpec ) : "nameless_";
+        sprintf( Buffer, "%s_dump.blif", pNameGen );
+        Io_Write( pNtk, Buffer, IO_FILE_BLIF );
+        if ( pNtk->pSpec ) free( pNameGen );
+    }
 
 //    if ( Abc_NtkIsStrash(pNtk) )
 //        Abc_AigCountNext( pNtk->pManFunc );
@@ -181,7 +189,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
         fprintf( pFile, "  lev = %3d", Abc_AigLevel(pNtk) );
     else 
         fprintf( pFile, "  lev = %3d", Abc_NtkLevel(pNtk) );
-
+    if ( fUseLutLib && Abc_FrameReadLibLut() )
+        fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) );
     fprintf( pFile, "\n" );
 
 //    Abc_NtkCrossCut( pNtk );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index b3d2d745..19222f3b 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -170,10 +170,10 @@ struct If_Man_t_
 // priority cut
 struct If_Cut_t_
 {
-    float              Delay;         // delay of the cut
     float              Area;          // area (or area-flow) of the cut
     float              AveRefs;       // the average number of leaf references
     float              Edge;          // the edge flow
+    float              Delay;         // delay of the cut
     unsigned           uSign;         // cut signature
     unsigned           Cost    : 14;  // the user's cost of the cut
     unsigned           fCompl  :  1;  // the complemented attribute 
@@ -379,8 +379,10 @@ extern int             If_ManPerformMappingSeq( If_Man_t * p );
 /*=== ifTime.c ============================================================*/
 extern float           If_CutDelay( If_Man_t * p, If_Cut_t * pCut );
 extern void            If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float Required );
+extern void            If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
 /*=== ifTruth.c ===========================================================*/
 extern void            If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
+extern void            If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars );
 /*=== ifUtil.c ============================================================*/
 extern void            If_ManCleanNodeCopy( If_Man_t * p );
 extern void            If_ManCleanCutData( If_Man_t * p );
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index 3d1dab1b..33bbdf74 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -221,6 +221,30 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sorts the pins in the decreasing order of delays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    float PinDelays[32];
+//    int PinPerm[32];
+    int i;
+    assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth ); 
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
+    If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
+//    If_CutSortInputPins( p, pCut, PinPerm, PinDelays );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index f18d8308..a3a7e1ee 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -126,6 +126,42 @@ void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int i
 
 /**Function*************************************************************
 
+  Synopsis    [Implements given permutation of variables.]
+
+  Description [Permutes truth table in-place (returns it in pIn).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars )
+{
+    unsigned * pTemp;
+    float tTemp;
+    int i, Temp, Counter = 0, fChange = 1;
+    while ( fChange )
+    {
+        fChange = 0;
+        for ( i = 0; i < nVars - 1; i++ )
+        {
+            if ( pDelays[i] >= pDelays[i+1] )
+                continue;
+            tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp;
+            Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp;
+            If_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
+            pTemp = pOut; pOut = pIn; pIn = pTemp;
+            fChange = 1;
+            Counter++;
+        }
+    }
+    if ( Counter & 1 )
+        If_TruthCopy( pOut, pIn, nVars );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Expands the truth table according to the phase.]
 
   Description [The input and output truth tables are in pIn/pOut. The current number
diff --git a/src/opt/fret/fretFlow.c b/src/opt/fret/fretFlow.c
index a9cef327..4b2bd936 100644
--- a/src/opt/fret/fretFlow.c
+++ b/src/opt/fret/fretFlow.c
@@ -73,6 +73,7 @@ void dfsfast_preorder( Abc_Ntk_t *pNtk ) {
 #endif
 
   // clear histogram
+  assert(pManMR->vSinkDistHist);
   memset(Vec_IntArray(pManMR->vSinkDistHist), 0, sizeof(int)*Vec_IntSize(pManMR->vSinkDistHist));
 
   // seed queue : latches, PIOs, and blocks
diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
index 53df7386..47d338cb 100644
--- a/src/opt/fret/fretInit.c
+++ b/src/opt/fret/fretInit.c
@@ -23,6 +23,10 @@
 #include "io.h"
 #include "fretime.h"
 #include "mio.h"
+#include "hop.h"
+
+#undef DEBUG_PRINT_INIT_NTK
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION PROTOTYPES                          ///
@@ -31,20 +35,24 @@
 static void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj );
 static void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk );
 static void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj );
-static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj, 
-                                                         Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis, 
-                                                         int recurse);
+static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj );
+
 static void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj );
 static void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop );
 
-extern void * Abc_FrameReadLibGen();                    
-extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
+static void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig );
+static void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag );
+static void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit );
 
+extern void * Abc_FrameReadLibGen();
+
+extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+
 /**Function*************************************************************
 
   Synopsis    [Updates initial state information.]
@@ -69,6 +77,40 @@ Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk ) {
   }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints initial state information.]
+
+  Description [Prints distribution of 0,1,and X initial states.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+inline int
+Abc_FlowRetime_ObjFirstNonLatchBox( Abc_Obj_t * pOrigObj, Abc_Obj_t ** pResult ) {
+  int lag = 0;
+  Abc_Ntk_t *pNtk;
+  *pResult = pOrigObj;
+  pNtk = Abc_ObjNtk( pOrigObj );
+
+  Abc_NtkIncrementTravId( pNtk );
+
+  while( Abc_ObjIsBo(*pResult) || Abc_ObjIsLatch(*pResult) || Abc_ObjIsBi(*pResult) ) {
+    assert(Abc_ObjFaninNum(*pResult));
+    *pResult = Abc_ObjFanin0(*pResult);
+    
+    if (Abc_NodeIsTravIdCurrent(*pResult))
+      return -1;
+    Abc_NodeSetTravIdCurrent(*pResult);
+
+    if (Abc_ObjIsLatch(*pResult)) ++lag;
+  }
+
+  return lag;
+}
+
 
 /**Function*************************************************************
 
@@ -152,6 +194,58 @@ void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj ) {
   Abc_FlowRetime_SimulateNode( pObj );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Recursively evaluates HOP netlist.]
+
+  Description [Exponential.  There aren't enough flags on a HOP node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_FlowRetime_EvalHop_rec( Hop_Man_t *pHop, Hop_Obj_t *pObj, int *f, int *dc ) {
+  int f1, dc1, f2, dc2;
+  Hop_Obj_t *pReg = Hop_Regular(pObj);
+  
+  // const 0
+  if (Hop_ObjIsConst1(pReg)) {
+    *f  = 1;
+    *f ^= (pReg == pObj ? 1 : 0);
+    *dc = 0;
+    return;
+  }
+
+  // PI
+  if (Hop_ObjIsPi(pReg)) {
+    *f  = pReg->fMarkA;
+    *f ^= (pReg == pObj ? 1 : 0);
+    *dc = pReg->fMarkB;
+    return;
+  }
+
+  // PO
+  if (Hop_ObjIsPo(pReg)) {
+    assert( pReg == pObj );
+    Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), f, dc);
+    return;
+  }
+
+  // AND
+  if (Hop_ObjIsAnd(pReg)) {
+    Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), &f1, &dc1);
+    Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild1(pReg), &f2, &dc2);
+
+    *dc = (dc1 & f2) | (dc2 & f1) | (dc1 & dc2);
+    *f  = f1 & f2;
+    *f ^= (pReg == pObj ? 1 : 0);
+    return;
+  }
+
+  assert(0);
+}
+
 
 /**Function*************************************************************
 
@@ -196,11 +290,13 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
   int i, rAnd, rVar, dcAnd, dcVar;
   DdManager * dd = pNtk->pManFunc;
   DdNode *pBdd = pObj->pData, *pVar;
+  Hop_Man_t *pHop = pNtk->pManFunc;
   
   assert(!Abc_ObjIsLatch(pObj));
+  assert(Abc_ObjRegular(pObj));
 
   // (i) constant nodes
-  if (Abc_NtkHasAig(pNtk) && Abc_AigNodeIsConst(pObj)) {
+  if (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) {
     Abc_FlowRetime_SetInitValue(pObj, 1, 0);
     return;
   }
@@ -258,10 +354,37 @@ void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
     return;
   }
 
-  // ------ AIG network
-  else if ( Abc_NtkHasAig( pNtk )) {
 
-    assert(Abc_AigNodeIsAnd(pObj));
+  // ------ AIG logic network
+  else if ( Abc_NtkHasAig( pNtk ) && !Abc_NtkIsStrash( pNtk )) {
+    
+    assert(Abc_ObjIsNode(pObj));
+    assert(pObj->pData);
+    assert(Abc_ObjFaninNum(pObj) <= Hop_ManPiNum(pHop) );
+    
+    // set vals at inputs
+    Abc_ObjForEachFanin(pObj, pFanin, i) {
+      Hop_ManPi(pHop, i)->fMarkA = FTEST(pFanin, INIT_1)?1:0;
+      Hop_ManPi(pHop, i)->fMarkB = FTEST(pFanin, INIT_CARE)?1:0;
+    }
+
+    Abc_FlowRetime_EvalHop_rec( pHop, pObj->pData, &rVar, &dcVar );
+   
+    Abc_FlowRetime_SetInitValue(pObj, rVar, dcVar);
+
+    // clear flags
+    Abc_ObjForEachFanin(pObj, pFanin, i) {
+      Hop_ManPi(pHop, i)->fMarkA = 0;
+      Hop_ManPi(pHop, i)->fMarkB = 0;
+    }
+
+    return;
+  }
+
+  // ------ strashed network
+  else if ( Abc_NtkIsStrash( pNtk )) {
+
+    assert(Abc_ObjType(pObj) == ABC_OBJ_NODE);
     dcAnd = 0, rAnd = 1;
     
     pFanin = Abc_ObjFanin0(pObj);
@@ -361,7 +484,9 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
   Vec_Ptr_t *vObj = Vec_PtrAlloc(100);
 
   // create the network used for the initial state computation
-  if (Abc_NtkHasMapping(pNtk))
+  if (Abc_NtkIsStrash(pNtk)) {
+    pManMR->pInitNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+  } else if (Abc_NtkHasMapping(pNtk))
     pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
   else
     pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
@@ -371,14 +496,12 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
     // map latch to initial state network
     pPi = Abc_NtkCreatePi( pManMR->pInitNtk );
 
+    // DEBUG
+    // printf("setup : mapping latch %d to PI %d\n", pLatch->Id, pPi->Id);
+
     // has initial state requirement?
     if (Abc_LatchIsInit0(pLatch)) {
-      
-      if (Abc_NtkHasAig(pNtk))
-        pObj = Abc_ObjNot( pPi );
-      else
-        pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
-
+      pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
       Vec_PtrPush(vObj, pObj);
     }
     else if (Abc_LatchIsInit1(pLatch)) {
@@ -397,14 +520,9 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
     pManMR->fSolutionIsDc = 0;
 
   // mitre output
-  if (Abc_NtkHasAig(pNtk)) {
-    // create AND-by-AND
-    pObj = Vec_PtrPop( vObj );
-    while( Vec_PtrSize(vObj) )
-      pObj = Abc_AigAnd( pManMR->pInitNtk->pManFunc, pObj, Vec_PtrPop( vObj ) ); 
-  } else
-    // create n-input AND gate
-    pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
+
+  // create n-input AND gate
+  pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
 
   Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
 
@@ -418,7 +536,7 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
 
   Description []
                
-  SideEffects []
+  SideEffects [Sets object copies in init ntk.]
 
   SeeAlso     []
 
@@ -427,13 +545,13 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   int i;
   Abc_Obj_t *pObj, *pInitObj;
   Vec_Ptr_t *vDelete = Vec_PtrAlloc(0);
+  Abc_Ntk_t *pSatNtk;
   int result;
 
   assert(pManMR->pInitNtk);
 
   // is the solution entirely DC's?
   if (pManMR->fSolutionIsDc) {
-    Abc_NtkDelete(pManMR->pInitNtk);
     Vec_PtrFree(vDelete);
     Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
     vprintf("\tno init state computation: all-don't-care solution\n");
@@ -441,15 +559,10 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   }
 
   // check that network is combinational
-  // mark superfluous BI nodes for deletion
   Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) {
     assert(!Abc_ObjIsLatch(pObj));
     assert(!Abc_ObjIsBo(pObj));
-    
-    if (Abc_ObjIsBi(pObj)) {
-      Abc_ObjBetterTransferFanout( pObj, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
-      Vec_PtrPush( vDelete, pObj );
-    }
+    assert(!Abc_ObjIsBi(pObj));
   }
   
   // delete superfluous nodes
@@ -464,9 +577,13 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_NtkAddDummyPiNames(pManMR->pInitNtk);
   if (Abc_NtkIsLogic(pManMR->pInitNtk))
     Abc_NtkCleanup(pManMR->pInitNtk, 0);
-  else if (Abc_NtkIsStrash(pManMR->pInitNtk)) {  
-    Abc_NtkReassignIds(pManMR->pInitNtk);
-  }
+
+#if defined(DEBUG_PRINT_INIT_NTK)
+  Abc_NtkLevelReverse( pManMR->pInitNtk );
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) 
+    if (Abc_ObjLevel( pObj ) < 2)
+      Abc_ObjPrint(stdout, pObj);
+#endif
   
   vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk));
   fflush(stdout);
@@ -474,17 +591,19 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   // convert SOPs to BDD
   if (Abc_NtkHasSop(pManMR->pInitNtk))
     Abc_NtkSopToBdd( pManMR->pInitNtk );
+  // convert AIGs to BDD
+  if (Abc_NtkHasAig(pManMR->pInitNtk))
+    Abc_NtkAigToBdd( pManMR->pInitNtk );  
+
+  pSatNtk = pManMR->pInitNtk;
   
   // solve
-  result = Abc_NtkMiterSat( pManMR->pInitNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+  result = Abc_NtkMiterSat( pSatNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
 
   if (!result) { 
     vprintf("SUCCESS\n");
   } else  {    
     vprintf("FAILURE\n");
-    printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n");
-    Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
-    Abc_NtkDelete(pManMR->pInitNtk);
     return 0;
   }
 
@@ -495,6 +614,9 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
     assert( Abc_ObjIsPi( pInitObj ));
     Abc_ObjSetCopy( pInitObj, pObj );
     Abc_LatchSetInitNone( pObj );
+
+    // DEBUG
+    // printf("solve : getting latch %d from PI %d\n", pObj->Id, pInitObj->Id);
   }
 
   // copy solution from PIs to latches
@@ -513,9 +635,6 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_NtkForEachLatch( pNtk, pObj, i ) assert( !Abc_LatchIsInitNone( pObj ) );
 #endif
 
-  // deallocate
-  Abc_NtkDelete( pManMR->pInitNtk );
-
   return 1;
 }
 
@@ -534,7 +653,9 @@ int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
 void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pOrigObj,  *pInitObj;
   Vec_Ptr_t *vBo = Vec_PtrAlloc(100);
-  Vec_Ptr_t *vOldPis = Vec_PtrAlloc(100);
+  Vec_Ptr_t *vPi = Vec_PtrAlloc(100);
+  Abc_Ntk_t *pInitNtk = pManMR-> pInitNtk;
+  Abc_Obj_t *pBuf;
   int i;
 
   // remove PIs from network (from BOs)
@@ -542,18 +663,43 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
     if (Abc_ObjIsBo(pOrigObj)) {
       pInitObj = FDATA(pOrigObj)->pInitObj;
       assert(Abc_ObjIsPi(pInitObj));
-      Vec_PtrPush(vBo, pOrigObj);
 
-      Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), pInitObj, vOldPis, 0 );
-    }
+      // DEBUG
+      // printf("update : freeing PI %d\n", pInitObj->Id);
+      
+      // create a buffer instead
+      pBuf = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pBuf );
 
-  // add PIs to network (at latches)
-  Abc_NtkForEachLatch( pNtk, pOrigObj, i )
-    Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj, NULL, vOldPis, 0 );
+      Abc_ObjBetterTransferFanout( pInitObj, pBuf, 0 );
+      FDATA(pOrigObj)->pInitObj = pBuf;
+      pOrigObj->fMarkA = 1;
+
+      Vec_PtrPush(vBo, pOrigObj);
+      Vec_PtrPush(vPi, pInitObj);
+    }
   
-  // connect nodes in init state network
+  // check that PIs are all free
+  Abc_NtkForEachPi( pInitNtk, pInitObj, i) {
+    assert( Abc_ObjFanoutNum( pInitObj ) == 0);
+  }
+
+  // add PIs to to latches
+  Abc_NtkForEachLatch( pNtk, pOrigObj, i ) {
+    assert(Vec_PtrSize(vPi) > 0);
+    pInitObj = Vec_PtrPop(vPi);
+
+    // DEBUG
+    // printf("update : mapping latch %d to PI %d\n", pOrigObj->Id, pInitObj->Id);
+
+    pOrigObj->fMarkA = pOrigObj->fMarkB = 1;
+    FDATA(pOrigObj)->pInitObj = pInitObj;
+    Abc_ObjSetData(pOrigObj, pInitObj);
+  }  
+
+  // recursively build init network
   Vec_PtrForEachEntry( vBo, pOrigObj, i )
-    Abc_FlowRetime_UpdateBackwardInit_rec( Abc_ObjFanin0( pOrigObj ), NULL, NULL, 1 );
+    Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj );
   
   // clear flags
   Abc_NtkForEachObj( pNtk, pOrigObj, i )
@@ -561,12 +707,95 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
 
   // deallocate
   Vec_PtrFree( vBo );
-  Vec_PtrFree( vOldPis );
+  Vec_PtrFree( vPi );
 }
 
 
 /**Function*************************************************************
 
+  Synopsis    [Creates a corresponding node in the init state network]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t *Abc_FlowRetime_CopyNodeToInitNtk( Abc_Obj_t *pOrigObj ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Ntk_t *pInitNtk = pManMR->pInitNtk;
+  Abc_Obj_t *pInitObj;
+  void *pData;
+  int fCompl[2];
+
+  assert(pOrigObj);
+
+  // what we do depends on the ntk types of original / init networks...
+  
+  // (0) convert BI/BO nodes to buffers
+  if (Abc_ObjIsBi( pOrigObj ) || Abc_ObjIsBo( pOrigObj ) ) {
+    pInitObj =  Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+    Abc_FlowRetime_ClearInitToOrig( pInitObj );
+    return pInitObj;
+  }
+
+  // (i) strash node -> SOP node
+  if (Abc_NtkIsStrash( pNtk )) {
+
+    if (Abc_AigNodeIsConst( pOrigObj )) {
+      return Abc_NtkCreateNodeConst1( pInitNtk );
+    }
+    if (!Abc_ObjIsNode( pOrigObj )) {
+      assert(Abc_ObjFaninNum(pOrigObj) == 1);
+      pInitObj =  Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pInitObj );
+      return pInitObj;
+    }
+
+    assert( Abc_ObjIsNode(pOrigObj) );
+    pInitObj = Abc_NtkCreateObj( pInitNtk, ABC_OBJ_NODE );
+    
+    fCompl[0] = pOrigObj->fCompl0 ? 1 : 0;
+    fCompl[1] = pOrigObj->fCompl1 ? 1 : 0;
+    
+    pData =  Abc_SopCreateAnd( pInitNtk->pManFunc, 2, fCompl );
+    assert(pData);
+    pInitObj->pData = Abc_SopRegister( pInitNtk->pManFunc, pData );
+  } 
+
+  // (ii) mapped node -> SOP node
+  else if (Abc_NtkHasMapping( pNtk )) {
+    if (!pOrigObj->pData) {
+      // assume terminal...
+      assert(Abc_ObjFaninNum(pOrigObj) == 1);
+
+      pInitObj =  Abc_NtkCreateNodeBuf( pInitNtk, NULL );
+      Abc_FlowRetime_ClearInitToOrig( pInitObj );
+      return pInitObj;
+    }
+
+    pInitObj = Abc_NtkCreateObj( pInitNtk, Abc_ObjType(pOrigObj) );
+    pData = Mio_GateReadSop(pOrigObj->pData);
+    assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
+    
+    pInitObj->pData = Abc_SopRegister( pInitNtk->pManFunc, pData );
+  } 
+
+  // (iii) otherwise, duplicate obj
+  else {
+    pInitObj = Abc_NtkDupObj( pInitNtk, pOrigObj, 0 );
+    
+    // copy phase
+    pInitObj->fPhase = pOrigObj->fPhase;
+  }
+
+  assert(pInitObj);
+  return pInitObj;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Updates backward initial state computation problem.]
 
   Description [Creates a duplicate node in the initial state network 
@@ -587,87 +816,43 @@ void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj, 
-                                                  Abc_Obj_t *pUseThisPi, Vec_Ptr_t *vOtherPis, 
-                                                  int fRecurse) {
-  Abc_Obj_t *pInitObj, *pOrigFanin, *pInitFanin;
-  void      *pData;
+Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj) {
+  Abc_Obj_t *pOrigFanin, *pInitFanin, *pInitObj;
   int i;
-  Abc_Ntk_t *pNtk = Abc_ObjNtk( pOrigObj );
+
+  assert(pOrigObj);
 
   // should never reach primary IOs
   assert(!Abc_ObjIsPi(pOrigObj));
   assert(!Abc_ObjIsPo(pOrigObj));
 
-  // if fanin is latch, it becomes a primary input
-  if (Abc_ObjIsLatch( pOrigObj )) {
-    if (pOrigObj->fMarkA)  return FDATA(pOrigObj)->pInitObj;
-
-    assert(vOtherPis);
-    
-    if (pUseThisPi) { 
-      // reuse curent PI     
-      pInitObj = pUseThisPi; }
-    else { 
-      // reuse previous PI
-      pInitObj = (Abc_Obj_t*)Vec_PtrPop(vOtherPis); 
-    }
-    
-    // remember link from original node to init ntk
-    Abc_ObjSetData( pOrigObj, pInitObj ); 
-
-    pOrigObj->fMarkA = 1;
-    return (FDATA(pOrigObj)->pInitObj = pInitObj);
-  } 
+  // skip bias nodes
+  if (FTEST(pOrigObj, BIAS_NODE)) 
+    return NULL;
 
   // does an init node already exist?
   if(!pOrigObj->fMarkA) {
 
-    if (Abc_NtkHasMapping( pNtk )) {
-      if (!pOrigObj->pData) {
-        // assume terminal...
-        assert(Abc_ObjFaninNum(pOrigObj) == 1);
-        pInitObj = Abc_NtkCreateNodeBuf( pManMR->pInitNtk, NULL );
-      } else {
-        pInitObj = Abc_NtkCreateObj( pManMR->pInitNtk, Abc_ObjType(pOrigObj) );
-        pData = Mio_GateReadSop(pOrigObj->pData);
-        assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
-
-        pInitObj->pData = Abc_SopRegister( pManMR->pInitNtk->pManFunc, pData );
-      }
-    } else {
-      pData = Abc_ObjCopy( pOrigObj );   // save ptr to flow data    
-      if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pOrigObj ))
-        pInitObj = Abc_AigConst1( pManMR->pInitNtk );
-      else
-        pInitObj = Abc_NtkDupObj( pManMR->pInitNtk, pOrigObj, 0 );
-      Abc_ObjSetCopy( pOrigObj, pData ); // restore ptr to flow data
-
-      // copy complementation
-      pInitObj->fCompl0 = pOrigObj->fCompl0;
-      pInitObj->fCompl1 = pOrigObj->fCompl1;
-      pInitObj->fPhase = pOrigObj->fPhase;
-    }
+    pInitObj = Abc_FlowRetime_CopyNodeToInitNtk( pOrigObj );
 
-    // if we didn't use given PI, immediately transfer fanouts
-    // and add to list for later reuse
-    if (pUseThisPi) {
-      Abc_ObjBetterTransferFanout( pUseThisPi, pInitObj, 0 );
-      Vec_PtrPush( vOtherPis, pUseThisPi );
-    }
+    Abc_FlowRetime_SetInitToOrig( pInitObj, pOrigObj );
+    FDATA(pOrigObj)->pInitObj = pInitObj;
 
     pOrigObj->fMarkA = 1;
-    FDATA(pOrigObj)->pInitObj = pInitObj;
   } else {
     pInitObj = FDATA(pOrigObj)->pInitObj;
   }
+  assert(pInitObj);
     
   // have we already connected this object?
-  if (fRecurse && !pOrigObj->fMarkB) {
+  if (!pOrigObj->fMarkB) {
 
     // create and/or connect fanins
     Abc_ObjForEachFanin( pOrigObj, pOrigFanin, i ) {
-      pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin, NULL, NULL, fRecurse );
+      // should not reach BOs (i.e. the start of the next frame)
+      // the new latch bounday should lie before it
+      assert(!Abc_ObjIsBo( pOrigFanin ));
+      pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin );
       Abc_ObjAddFanin( pInitObj, pInitFanin );
     }
 
@@ -745,6 +930,72 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
   Abc_FlowRetime_SimulateNode( pObj );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Constrains backward retiming for initializability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_FlowRetime_PartialSat(Vec_Ptr_t *vNodes, int cut) {
+  Abc_Ntk_t *pPartNtk, *pInitNtk = pManMR->pInitNtk;
+  Abc_Obj_t *pObj, *pNext, *pPartObj, *pPartNext, *pPo;
+  int i, j, result;
+
+  assert( Abc_NtkPoNum( pInitNtk ) == 1 );
+
+  pPartNtk = Abc_NtkAlloc( pInitNtk->ntkType, pInitNtk->ntkFunc, 0 );
+
+  // copy network
+  Vec_PtrForEachEntry( vNodes, pObj, i ) {
+    pObj->Level = i;
+    assert(!Abc_ObjIsPo( pObj ));
+
+    if (i < cut && !pObj->fMarkA) {
+      pPartObj = Abc_NtkCreatePi( pPartNtk );
+      Abc_ObjSetCopy( pObj, pPartObj );
+    } else {
+      // copy node
+      pPartObj = Abc_NtkDupObj( pPartNtk, pObj, 0 );
+      // copy complementation
+      pPartObj->fPhase = pObj->fPhase;
+   
+      // connect fanins
+      Abc_ObjForEachFanin( pObj, pNext, j ) {   
+        pPartNext = Abc_ObjCopy( pNext );
+        assert(pPartNext);
+        Abc_ObjAddFanin( pPartObj, pPartNext );
+      }
+    }
+
+    assert(pObj->pCopy == pPartObj);
+  }
+  
+  // create PO
+  pPo = Abc_NtkCreatePo( pPartNtk );
+  pNext = Abc_ObjFanin0( Abc_NtkPo( pInitNtk, 0 ) );
+  pPartNext = Abc_ObjCopy( pNext );
+  assert( pPartNext );
+  Abc_ObjAddFanin( pPo, pPartNext );
+  
+  // check network
+#if defined(DEBUG_CHECK)
+  Abc_NtkAddDummyPoNames(pPartNtk);
+  Abc_NtkAddDummyPiNames(pPartNtk);
+  Abc_NtkCheck( pPartNtk );
+#endif
+
+  result = Abc_NtkMiterSat( pPartNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
+
+  Abc_NtkDelete( pPartNtk );
+ 
+  return !result;
+}
+
 
 /**Function*************************************************************
 
@@ -758,5 +1009,321 @@ void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
 
 ***********************************************************************/
 void Abc_FlowRetime_ConstrainInit( ) {
-  // unimplemented
+  Vec_Ptr_t *vNodes;
+  int low, high, mid;
+  int i, n, lag;
+  Abc_Obj_t *pObj = NULL, *pOrigObj;
+  InitConstraint_t *pConstraint = ALLOC( InitConstraint_t, 1 );
+
+  memset( pConstraint, 0, sizeof(InitConstraint_t) );
+
+  assert(pManMR->pInitNtk);
+
+  vprintf("\tsearch for initial state conflict...\n");
+
+  vNodes = Abc_NtkDfs(pManMR->pInitNtk, 0);
+  n = Vec_PtrSize(vNodes);
+  // also add PIs to vNodes
+  Abc_NtkForEachPi(pManMR->pInitNtk, pObj, i) 
+    Vec_PtrPush(vNodes, pObj);
+  Vec_PtrReorder(vNodes, n);
+
+#if defined(DEBUG_CHECK)
+    assert(!Abc_FlowRetime_PartialSat( vNodes, 0 ));
+#endif
+
+  // grow initialization constraint
+  do {
+    vprintf("\t\t");
+
+    // find element to add to set...
+    low = 0, high = Vec_PtrSize(vNodes);
+    while (low != high-1) {
+      mid = (low + high) >> 1;
+      
+      if (!Abc_FlowRetime_PartialSat( vNodes, mid )) {
+        low = mid;
+        vprintf("-");
+      } else {
+        high = mid;
+        vprintf("*");
+      }
+      fflush(stdout);
+    }
+      
+#if defined(DEBUG_CHECK)
+    assert(Abc_FlowRetime_PartialSat( vNodes, high ));
+    assert(!Abc_FlowRetime_PartialSat( vNodes, low ));
+#endif
+    
+    // mark its TFO
+    pObj = Vec_PtrEntry( vNodes, low );
+    Abc_NtkMarkCone_rec( pObj, 1 );
+    vprintf("   conflict term = %d ", low);
+
+#if 0
+    printf("init ------\n");
+    Abc_ObjPrint(stdout, pObj);
+    printf("\n");
+    Abc_ObjPrintNeighborhood( pObj, 1 );
+    printf("------\n");
+#endif
+
+    // add node to constraint
+    Abc_FlowRetime_GetInitToOrig( pObj, &pOrigObj, &lag );
+    assert(pOrigObj);
+    vprintf(" <=> %d/%d\n", Abc_ObjId(pOrigObj), lag);
+
+#if 0    
+    printf("orig ------\n");
+    Abc_ObjPrint(stdout, pOrigObj);
+    printf("\n");
+    Abc_ObjPrintNeighborhood( pOrigObj, 1 );
+    printf("------\n");
+#endif
+    Vec_IntPush( &pConstraint->vNodes, Abc_ObjId(pOrigObj) );
+    Vec_IntPush( &pConstraint->vLags, lag );
+
+  } while (Abc_FlowRetime_PartialSat( vNodes, Vec_PtrSize(vNodes) ));
+
+  pConstraint->pBiasNode = NULL;
+
+  // add constraint
+  Vec_PtrPush( pManMR->vInitConstraints, pConstraint );
+
+  // clear marks
+  Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i)
+    pObj->fMarkA = 0;
+
+  // free
+  Vec_PtrFree( vNodes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes nodes to bias against uninitializable cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_RemoveInitBias( ) {
+  // Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Obj_t *pBiasNode;
+  InitConstraint_t *pConstraint;
+  int i;
+
+  Vec_PtrForEachEntry( pManMR->vInitConstraints, pConstraint, i ) {
+    pBiasNode = pConstraint->pBiasNode;
+    pConstraint->pBiasNode = NULL;
+
+    if (pBiasNode)
+      Abc_NtkDeleteObj(pBiasNode);
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Connects the bias node to one of the constraint vertices.]
+
+  Description [ACK!
+               Currently this is dumb dumb hack.
+               What should we do with biases that belong on BOs?  These
+               move through the circuit.
+               Currently, the bias gets marked on the fan-in of BO
+               and the bias gets implemented on every BO fan-out of a
+               node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Abc_FlowRetime_ConnectBiasNode(Abc_Obj_t *pBiasNode, Abc_Obj_t *pObj, int biasLag) {
+  Abc_Obj_t *pCur, *pNext;
+  int i;
+  int lag;
+  Vec_Ptr_t *vNodes = Vec_PtrAlloc(1);
+  Vec_Int_t *vLags = Vec_IntAlloc(1);
+  Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj );
+  
+  Vec_PtrPush( vNodes, pObj );
+  Vec_IntPush( vLags, 0 );
+
+  Abc_NtkIncrementTravId( pNtk );
+
+  while (Vec_PtrSize( vNodes )) {
+    pCur = Vec_PtrPop( vNodes );
+    lag = Vec_IntPop( vLags );
+
+    if (Abc_NodeIsTravIdCurrent( pCur )) continue;
+    Abc_NodeSetTravIdCurrent( pCur );
+
+    if (!Abc_ObjIsLatch(pCur) &&
+        !Abc_ObjIsBo(pCur) &&
+        Abc_FlowRetime_GetLag(pObj)+lag == biasLag ) {
+
+      // printf("biasing : ");
+      // Abc_ObjPrint(stdout,  pCur );
+#if 1
+      FSET( pCur, BLOCK );
+#else
+      Abc_ObjAddFanin( pCur, pBiasNode );
+#endif
+    }
+
+    Abc_ObjForEachFanout( pCur, pNext, i ) {
+      if (Abc_ObjIsBi(pNext) ||
+          Abc_ObjIsLatch(pNext) ||
+          Abc_ObjIsBo(pNext) ||
+          Abc_ObjIsBo(pCur)) {
+        Vec_PtrPush( vNodes, pNext );
+        Vec_IntPush( vLags, lag - Abc_ObjIsLatch(pNext) ? 1 : 0 );
+      }
+    }
+  }
+
+  Vec_PtrFree( vNodes );
+  Vec_IntFree( vLags );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds nodes to bias against uninitializable cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_AddInitBias( ) {
+  Abc_Ntk_t *pNtk = pManMR->pNtk;
+  Abc_Obj_t *pBiasNode, *pObj, *pNext, *pNext2;
+  InitConstraint_t *pConstraint;
+  int i, j, k, l, id;
+  const int nConstraints = Vec_PtrSize( pManMR->vInitConstraints );
+
+  pManMR->pDataArray = REALLOC( Flow_Data_t, pManMR->pDataArray, pManMR->nNodes + (nConstraints*(pManMR->iteration+1)) );
+  memset(pManMR->pDataArray + pManMR->nNodes, 0, sizeof(Flow_Data_t)*(nConstraints*(pManMR->iteration+1)));
+
+  vprintf("\t\tcreating %d bias structures\n", nConstraints);
+
+  Vec_PtrForEachEntry( pManMR->vInitConstraints, pConstraint, i ) {
+    if (pConstraint->pBiasNode) continue;
+    
+ //   printf("\t\t\tbias %d...\n", i);
+    pBiasNode = Abc_NtkCreateBlackbox( pNtk );
+
+    Vec_IntForEachEntry( &pConstraint->vNodes, id, j ) {
+      pObj = Abc_NtkObj(pNtk, id);
+      Abc_FlowRetime_ConnectBiasNode(pBiasNode, pObj, Vec_IntEntry(&pConstraint->vLags, j));
+    }
+
+    // pConstraint->pBiasNode = pBiasNode;
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Clears mapping from init node to original node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit )
+{
+  int id = Abc_ObjId( pInit );
+  
+  // grow data structure if necessary
+  if (id >= pManMR->sizeInitToOrig) {
+    int oldSize = pManMR->sizeInitToOrig;
+    pManMR->sizeInitToOrig = 1.5*id + 10;
+    pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig);
+    memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) );
+  }
+  assert( pManMR->pInitToOrig );
+
+  pManMR->pInitToOrig[id].id = -1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets mapping from init node to original node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig)
+{
+  int lag;
+  int id = Abc_ObjId( pInit );
+  
+  // grow data structure if necessary
+  if (id >= pManMR->sizeInitToOrig) {
+    int oldSize = pManMR->sizeInitToOrig;
+    pManMR->sizeInitToOrig = 1.5*id + 10;
+    pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig);
+    memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) );
+  }
+  assert( pManMR->pInitToOrig );
+
+  // ignore BI, BO, and latch nodes
+  if (Abc_ObjIsBo(pOrig) || Abc_ObjIsBi(pOrig) || Abc_ObjIsLatch(pOrig)) {
+    Abc_FlowRetime_ClearInitToOrig(pInit);
+    return;
+  }
+
+  // move out of latch boxes
+  lag = Abc_FlowRetime_ObjFirstNonLatchBox(pOrig, &pOrig);
+
+  pManMR->pInitToOrig[id].id = Abc_ObjId(pOrig);
+  pManMR->pInitToOrig[id].lag = Abc_FlowRetime_GetLag(pOrig) + lag;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Gets mapping from init node to original node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag ) {
+
+  int id = Abc_ObjId( pInit );
+  int origId;
+
+  assert(id < pManMR->sizeInitToOrig);
+
+  origId = pManMR->pInitToOrig[id].id;
+
+  if (origId < 0) {
+    assert(Abc_ObjFaninNum(pInit));
+    Abc_FlowRetime_GetInitToOrig( Abc_ObjFanin0(pInit), pOrig, lag);
+    return;
+  }
+
+  *pOrig = Abc_NtkObj(pManMR->pNtk, origId);
+  *lag = pManMR->pInitToOrig[id].lag;
 }
diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c
index 780c1f6f..a9ba8c4b 100644
--- a/src/opt/fret/fretMain.c
+++ b/src/opt/fret/fretMain.c
@@ -28,18 +28,22 @@
 
 static void Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj );
 
-static void Abc_FlowRetime_MainLoop( );
+static Abc_Ntk_t* Abc_FlowRetime_MainLoop( );
 
 static void Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk );
 static void Abc_FlowRetime_MarkReachable_rec( Abc_Obj_t * pObj, char end );
 static int  Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk );
 static void  Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch );
 
+static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk );
+
 static void Abc_FlowRetime_VerifyPathLatencies( Abc_Ntk_t * pNtk );
 static int  Abc_FlowRetime_VerifyPathLatencies_rec( Abc_Obj_t * pObj, int markD );
 
+static void Abc_FlowRetime_UpdateLags_forw_rec( Abc_Obj_t *pObj );
+static void Abc_FlowRetime_UpdateLags_back_rec( Abc_Obj_t *pObj );
+
 extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
-extern Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
 
 void
 print_node3(Abc_Obj_t *pObj);
@@ -64,12 +68,14 @@ int          fPathError = 0;
 
 ***********************************************************************/
 Abc_Ntk_t *
-Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
+Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, 
+                       int fComputeInitState, int fGuaranteeInitState, int fBlockConst,
                        int fForwardOnly, int fBackwardOnly, int nMaxIters,
                        int maxDelay, int fFastButConservative ) {
 
   int i;
   Abc_Obj_t   *pObj, *pNext;
+  InitConstraint_t *pData;
 
   // create manager
   pManMR = ALLOC( MinRegMan_t, 1 );
@@ -77,7 +83,8 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
   pManMR->pNtk = pNtk;
   pManMR->fVerbose = fVerbose;
   pManMR->fComputeInitState = fComputeInitState;
-  pManMR->fGuaranteeInitState = 0;
+  pManMR->fGuaranteeInitState = fGuaranteeInitState;
+  pManMR->fBlockConst = fBlockConst;
   pManMR->fForwardOnly = fForwardOnly;
   pManMR->fBackwardOnly = fBackwardOnly;
   pManMR->nMaxIters = nMaxIters;
@@ -85,6 +92,10 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
   pManMR->fComputeInitState = fComputeInitState;
   pManMR->fConservTimingOnly = fFastButConservative;
   pManMR->vNodes = Vec_PtrAlloc(100);
+  pManMR->vInitConstraints = Vec_PtrAlloc(2);
+  pManMR->pInitNtk = NULL;
+  pManMR->pInitToOrig = NULL;
+  pManMR->sizeInitToOrig = 0;
 
   vprintf("Flow-based minimum-register retiming...\n");  
 
@@ -96,7 +107,7 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
   if (maxDelay) {
     vprintf("\tmax delay constraint = %d\n", maxDelay);
     if (maxDelay < (i = Abc_NtkLevel(pNtk))) {
-      printf("ERROR: max delay constraint must be > current max delay (%d)\n", i);
+      printf("ERROR: max delay constraint (%d) must be > current max delay (%d)\n", maxDelay, i);
       return pNtk;
     }
   }
@@ -151,19 +162,18 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
   if (maxDelay)
     Abc_FlowRetime_InitTiming( pNtk );
 
-  // create Flow_Data structure
+  // create lag and Flow_Data structure
+  pManMR->vLags = Vec_IntStart(pManMR->nNodes);
+  memset(pManMR->vLags->pArray, 0, sizeof(int)*pManMR->nNodes);
+
   pManMR->pDataArray = ALLOC( Flow_Data_t, pManMR->nNodes );
   Abc_FlowRetime_ClearFlows( 1 );
-  Abc_NtkForEachObj( pNtk, pObj, i )
-    Abc_ObjSetCopy( pObj, (void *)(&pManMR->pDataArray[i]) );
 
   // main loop!
-  Abc_FlowRetime_MainLoop();
+  pNtk = Abc_FlowRetime_MainLoop();
 
-  // clear pCopy field
+  // cleanup node fields
   Abc_NtkForEachObj( pNtk, pObj, i ) {
-    Abc_ObjSetCopy( pObj, NULL );
-
     // if not computing init state, set all latches to DC
     if (!fComputeInitState && Abc_ObjIsLatch(pObj))
       Abc_LatchSetInitDc(pObj);
@@ -171,14 +181,24 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
 
   // deallocate space
   FREE( pManMR->pDataArray );
+  if (pManMR->pInitToOrig) FREE( pManMR->pInitToOrig );
   if (pManMR->vNodes) Vec_PtrFree(pManMR->vNodes);
+  if (pManMR->vLags) Vec_IntFree(pManMR->vLags);
   if (pManMR->vSinkDistHist) Vec_IntFree(pManMR->vSinkDistHist);
   if (pManMR->maxDelay) Abc_FlowRetime_FreeTiming( pNtk );
+  while( Vec_PtrSize( pManMR->vInitConstraints )) {
+    pData = Vec_PtrPop( pManMR->vInitConstraints );
+    //assert( pData->pBiasNode );
+    //Abc_NtkDeleteObj( pData->pBiasNode );
+    FREE( pData->vNodes.pArray );
+    FREE( pData );
+  }
+  FREE( pManMR->vInitConstraints );
 
   // restrash if necessary
   if (Abc_NtkIsStrash(pNtk)) {
     Abc_NtkReassignIds( pNtk );
-    pNtk = Abc_NtkRestrash( pNtk, 1 );
+    pNtk = Abc_FlowRetime_NtkSilentRestrash( pNtk, 1 );
   }
   
   vprintf("\tfinal reg count = %d\n", Abc_NtkLatchNum(pNtk));
@@ -205,10 +225,10 @@ Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
   SeeAlso     []
 
 ***********************************************************************/
-void
+Abc_Ntk_t *
 Abc_FlowRetime_MainLoop( ) {
-  Abc_Ntk_t *pNtk = pManMR->pNtk;
-  // Abc_Obj_t *pObj; int i;
+  Abc_Ntk_t *pNtk = pManMR->pNtk, *pNtkCopy = pNtk;
+  Abc_Obj_t *pObj; int i;
   int last, flow = 0, cut;
 
   // (i) forward retiming loop
@@ -237,30 +257,20 @@ Abc_FlowRetime_MainLoop( ) {
 
     cut = Abc_FlowRetime_ImplementCut( pNtk );
 
+#if defined (DEBUG_PRINT_LEVELS)
     vprintf("\t\tlevels = %d\n", Abc_NtkLevel(pNtk));
-
-#if 0
-    Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
-
-    Abc_NtkLevel(pNtk);
-    Abc_NtkForEachObj( pNtk, pObj, i )
-      if (pObj->Level > pManMR->maxDelay) {
-        print_node( pObj );
-        Vec_PtrForEachEntry( FTIMEEDGES(pObj), p2,j ) {
-          printf(":%d ", p2->Id);
-        }
-      }
-    Abc_NtkLevelReverse(pNtk);
-    Abc_NtkForEachObj( pNtk, pObj, i )
-      if (pObj->Level > pManMR->maxDelay) {
-        print_node( pObj );
-      }
 #endif
 
     Abc_FlowRetime_ClearFlows( 1 );
 
     pManMR->iteration++;
   } while( cut != last );
+  
+  // intermediate cleanup (for strashed networks)
+  if (Abc_NtkIsStrash(pNtk)) {
+    Abc_NtkReassignIds( pNtk );
+    pNtk = pManMR->pNtk = Abc_FlowRetime_NtkSilentRestrash( pNtk, 1 );
+  }
 
   // print info about initial states
   if (pManMR->fComputeInitState && pManMR->fVerbose)
@@ -268,10 +278,18 @@ Abc_FlowRetime_MainLoop( ) {
 
   // (ii) backward retiming loop
   pManMR->fIsForward = 0;
-  pManMR->iteration = 0;
 
   if (!pManMR->fForwardOnly) do {
     // initializability loop
+    pManMR->iteration = 0;
+
+    // copy/restore network
+    if (pManMR->fGuaranteeInitState) {
+      if ( pNtk != pNtkCopy )
+        Abc_NtkDelete( pNtk );
+      pNtk = pManMR->pNtk = Abc_FlowRetime_NtkDup( pNtkCopy );
+      vprintf("\trestoring network. regs = %d\n", Abc_NtkLatchNum( pNtk ));
+    }
 
     if (pManMR->fComputeInitState) {
       Abc_FlowRetime_SetupBackwardInit( pNtk );
@@ -284,8 +302,9 @@ Abc_FlowRetime_MainLoop( ) {
       vprintf("\tbackward iteration %d\n", pManMR->iteration);
       last = Abc_NtkLatchNum( pNtk );
 
+      Abc_FlowRetime_AddInitBias( );
       Abc_FlowRetime_MarkBlocks( pNtk );
-      
+
       if (pManMR->maxDelay) {
         // timing-constrained loop
         Abc_FlowRetime_ConstrainConserv( pNtk );
@@ -296,25 +315,13 @@ Abc_FlowRetime_MainLoop( ) {
       } else {
         flow = Abc_FlowRetime_PushFlows( pNtk, 1 );
       }
-      
+
+      Abc_FlowRetime_RemoveInitBias( );
       cut = Abc_FlowRetime_ImplementCut( pNtk );
 
+#if defined(DEBUG_PRINT_LEVELS)
       vprintf("\t\tlevels = %d\n", Abc_NtkLevelReverse(pNtk));
-      
-#if 0
-    Abc_NtkForEachObj( pNtk, pObj, i ) pObj->Level = 0;
-
-    Abc_NtkLevel(pNtk);
-    Abc_NtkForEachObj( pNtk, pObj, i )
-      if (pObj->Level > pManMR->maxDelay) {
-        print_node( pObj );
-      }
-    Abc_NtkLevelReverse(pNtk);
-    Abc_NtkForEachObj( pNtk, pObj, i )
-      if (pObj->Level > pManMR->maxDelay) {
-        print_node( pObj );
-      }
-#endif
+#endif      
 
       Abc_FlowRetime_ClearFlows( 1 );
 
@@ -328,10 +335,23 @@ Abc_FlowRetime_MainLoop( ) {
       if (pManMR->fVerbose) Abc_FlowRetime_PrintInitStateInfo( pNtk );
       break;
     } else {
-      if (!pManMR->fGuaranteeInitState) break;
+      if (!pManMR->fGuaranteeInitState) {
+        printf("WARNING: no equivalent init state. setting all initial states to don't-cares\n");
+        Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
+        break;
+      }
       Abc_FlowRetime_ConstrainInit( );
     }
+    
+    Abc_NtkDelete(pManMR->pInitNtk);
+    pManMR->pInitNtk = NULL;
   } while(1);
+
+  assert(!pManMR->fComputeInitState || pManMR->pInitNtk);
+  if (pManMR->fComputeInitState)   Abc_NtkDelete(pManMR->pInitNtk);
+  if (pManMR->fGuaranteeInitState) ; /* Abc_NtkDelete(pNtkCopy); note: original ntk deleted later */
+
+  return pNtk;
 }
 
 
@@ -369,7 +389,7 @@ Abc_FlowRetime_RemoveLatchBubbles( Abc_Obj_t * pLatch ) {
   pBi->fCompl0 ^= bubble ^ Abc_ObjFaninC0(pLatch);
 
   // convert bubble to INV if not AIG
-  if (!Abc_NtkHasAig( pNtk ) && Abc_ObjFaninC0(pBi)) {
+  if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjFaninC0(pBi)) {
     pBi->fCompl0 = 0;
     pInv = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanin0(pBi) );
     Abc_ObjPatchFanin( pBi, Abc_ObjFanin0(pBi), pInv );
@@ -397,6 +417,8 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
   Abc_Obj_t *pObj;
 
   if (pManMR->fIsForward){
+    // --- forward retiming : block TFO of inputs    
+
     // mark the frontier
     Abc_NtkForEachPo( pNtk, pObj, i )
       pObj->fMarkA = 1;
@@ -408,6 +430,8 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
     Abc_NtkForEachPi( pNtk, pObj, i )
       Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
   } else {
+    // --- backward retiming : block TFI of outputs
+
     // mark the frontier
     Abc_NtkForEachPi( pNtk, pObj, i )
       pObj->fMarkA = 1;
@@ -418,6 +442,14 @@ Abc_FlowRetime_MarkBlocks( Abc_Ntk_t * pNtk ) {
     // mark the nodes reachable from the POs
     Abc_NtkForEachPo( pNtk, pObj, i )
       Abc_NtkMarkCone_rec( pObj, pManMR->fIsForward );
+    // block constant nodes (if enabled)
+    if (pManMR->fBlockConst) {
+      Abc_NtkForEachObj( pNtk, pObj, i )
+        if ((Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) ||
+            (!Abc_NtkIsStrash(pNtk) && Abc_NodeIsConst(pObj))) {
+          FSET(pObj, BLOCK);
+        }
+    }
   }
 
   // copy marks
@@ -518,7 +550,7 @@ Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
     pBi = (Abc_Obj_t *)Vec_PtrPop( vBoxIns );
     assert(Abc_ObjIsBi(pBi));
     assert(Abc_ObjFanoutNum(pBi) == 1);
-    assert(Abc_ObjFaninNum(pBi) == 1);
+    // APH: broken by bias nodes assert(Abc_ObjFaninNum(pBi) == 1);
     pBo = Abc_ObjFanout0(pBi);
     assert(!Abc_ObjFaninC0(pBo));
 
@@ -546,7 +578,12 @@ Abc_FlowRetime_FixLatchBoxes( Abc_Ntk_t *pNtk, Vec_Ptr_t *vBoxIns ) {
       assert(Abc_ObjFanoutNum(pBi) == 0);
       assert(Abc_ObjFaninNum(pBo) == 0);
       assert(Abc_ObjFanoutNum(pBo) == 0);
-    } else assert(Abc_ObjIsLatch(pBo));
+    } else if (Abc_ObjIsLatch(pBo)) {
+    } else {
+      Abc_ObjPrint(stdout, pBi);
+      Abc_ObjPrint(stdout, pBo);
+      assert(0);
+    }
   }
 
   // 2. add bi/bos as necessary for latches
@@ -803,6 +840,7 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
   // insert latches into netlist
   Abc_NtkForEachObj( pNtk, pObj, i ) {
     if (Abc_ObjIsLatch( pObj )) continue;
+    if (FTEST(pObj, BIAS_NODE)) continue;
     
     // a latch is required on every node that lies across the min-cit
     assert(!pManMR->fIsForward || !FTEST(pObj, VISITED_E) || FTEST(pObj, VISITED_R));
@@ -837,7 +875,7 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
         if (Abc_ObjIsBi(pNext)) assert(Abc_ObjFaninNum(pNext) == 1);
 
       }
-      if (Abc_ObjIsBi(pObj)) assert(Abc_ObjFaninNum(pObj) == 1);
+      // APH: broken by bias nodes  if (Abc_ObjIsBi(pObj)) assert(Abc_ObjFaninNum(pObj) == 1);
     }
   }
 
@@ -852,6 +890,7 @@ Abc_FlowRetime_ImplementCut( Abc_Ntk_t * pNtk ) {
   }
   
   // update initial states
+  Abc_FlowRetime_UpdateLags( );
   Abc_FlowRetime_InitState( pNtk );
 
   // restore latch boxes
@@ -881,7 +920,7 @@ void
 Abc_FlowRetime_AddDummyFanin( Abc_Obj_t * pObj ) {
   Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj );
 
-  if (Abc_NtkHasAig(pNtk)) 
+  if (Abc_NtkIsStrash(pNtk)) 
     Abc_ObjAddFanin(pObj, Abc_AigConst1( pNtk ));
   else
     Abc_ObjAddFanin(pObj, Abc_NtkCreateNodeConst0( pNtk ));
@@ -1057,3 +1096,281 @@ void Abc_FlowRetime_ClearFlows( bool fClearAll ) {
     }
   }
 }
+
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates network.]
+
+  Description [Duplicates any type of network. Preserves copy data.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk ) {
+  Abc_Ntk_t *pNtkCopy;
+  Abc_Obj_t *pObj, *pObjCopy, *pNext, *pNextCopy;
+  int i, j;
+
+  pNtkCopy = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+
+  // copy each object
+  Abc_NtkForEachObj( pNtk, pObj, i) {
+
+    if (Abc_NtkIsStrash( pNtk ) && Abc_AigNodeIsConst( pObj ))
+      pObjCopy = Abc_AigConst1( pNtkCopy );
+    else
+      pObjCopy = Abc_NtkDupObj( pNtkCopy, pObj, 0 );
+
+    FDATA( pObj )->pCopy = pObjCopy;
+    FDATA( pObj )->mark = 0;
+
+    // assert( pManMR->fIsForward || pObj->Id == pObjCopy->Id );
+
+    // copy complementation
+    pObjCopy->fCompl0 = pObj->fCompl0;
+    pObjCopy->fCompl1 = pObj->fCompl1;
+    pObjCopy->fPhase = pObj->fPhase;
+  }
+
+  // connect fanin
+  Abc_NtkForEachObj( pNtk, pObj, i) {
+    pObjCopy = FDATA(pObj)->pCopy;
+    assert(pObjCopy);
+    Abc_ObjForEachFanin( pObj, pNext, j ) {
+      pNextCopy = FDATA(pNext)->pCopy;
+      assert(pNextCopy);
+      assert(pNext->Type == pNextCopy->Type);
+
+      Abc_ObjAddFanin(pObjCopy, pNextCopy);
+    }
+  }
+
+#if defined(DEBUG_CHECK) || 1
+  Abc_NtkForEachObj( pNtk, pObj, i) { 
+    pObjCopy = FDATA(pObj)->pCopy;
+    assert( Abc_ObjFanoutNum( pObj ) ==  Abc_ObjFanoutNum( pObjCopy ) );
+    assert( Abc_ObjFaninNum( pObj ) ==  Abc_ObjFaninNum( pObjCopy ) );
+  }
+#endif
+
+  assert(Abc_NtkObjNum( pNtk )   == Abc_NtkObjNum( pNtkCopy ) );
+  assert(Abc_NtkLatchNum( pNtk ) == Abc_NtkLatchNum( pNtkCopy ) );
+  assert(Abc_NtkPoNum( pNtk )    == Abc_NtkPoNum( pNtkCopy ) );
+  assert(Abc_NtkPiNum( pNtk )    == Abc_NtkPiNum( pNtkCopy ) );
+
+  return pNtkCopy;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Silent restrash.]
+
+  Description [Same functionality as Abc_NtkRestrash but w/o warnings.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
+{
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i, nNodes;//, RetValue;
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // restrash the nodes (assuming a topological order of the old network)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkAig );
+    // perform cleanup if requested
+    if ( fCleanup )
+      nNodes = Abc_AigCleanup(pNtkAig->pManFunc);
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+      pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+      {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+      }
+    return pNtkAig;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates lag values.]
+
+  Description [Recursive.  Forward retiming.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_UpdateLags_forw_rec( Abc_Obj_t *pObj ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  assert(!Abc_ObjIsPi(pObj));
+  assert(!Abc_ObjIsLatch(pObj));
+
+  if (Abc_ObjIsBo(pObj)) return;
+  if (Abc_NodeIsTravIdCurrent(pObj)) return;
+
+  Abc_NodeSetTravIdCurrent(pObj);
+
+  if (Abc_ObjIsNode(pObj)) {
+    Abc_FlowRetime_SetLag( pObj, -1+Abc_FlowRetime_GetLag(pObj) );
+  }
+
+  Abc_ObjForEachFanin( pObj, pNext, i ) {
+    Abc_FlowRetime_UpdateLags_forw_rec( pNext );
+  }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Updates lag values.]
+
+  Description [Recursive.  Backward retiming.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_UpdateLags_back_rec( Abc_Obj_t *pObj ) {
+  Abc_Obj_t *pNext;
+  int i;
+
+  assert(!Abc_ObjIsPo(pObj));
+  assert(!Abc_ObjIsLatch(pObj));
+
+  if (Abc_ObjIsBo(pObj)) return;
+  if (Abc_NodeIsTravIdCurrent(pObj)) return;
+
+  Abc_NodeSetTravIdCurrent(pObj);
+
+  if (Abc_ObjIsNode(pObj)) {
+    Abc_FlowRetime_SetLag( pObj, 1+Abc_FlowRetime_GetLag(pObj) );
+  }
+
+  Abc_ObjForEachFanout( pObj, pNext, i ) {
+    Abc_FlowRetime_UpdateLags_back_rec( pNext );
+  }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates lag values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void
+Abc_FlowRetime_UpdateLags( ) {
+  Abc_Obj_t *pObj, *pNext;
+  int i, j;
+
+  Abc_NtkIncrementTravId( pManMR->pNtk );
+
+  Abc_NtkForEachLatch( pManMR->pNtk, pObj, i )
+    if (pManMR->fIsForward) {
+      Abc_ObjForEachFanin( pObj, pNext, j )          
+        Abc_FlowRetime_UpdateLags_forw_rec( pNext );
+    } else {
+      Abc_ObjForEachFanout( pObj, pNext, j )          
+        Abc_FlowRetime_UpdateLags_back_rec( pNext );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Gets lag value of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int 
+Abc_FlowRetime_GetLag( Abc_Obj_t *pObj ) {
+  assert( !Abc_ObjIsLatch(pObj) );
+  assert( Abc_ObjId(pObj) < Vec_IntSize(pManMR->vLags) );
+
+  return Vec_IntEntry(pManMR->vLags, Abc_ObjId(pObj));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets lag value of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void 
+Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag ) {
+  assert( Abc_ObjIsNode(pObj) );
+  assert( Abc_ObjId(pObj) < Vec_IntSize(pManMR->vLags) );
+
+  Vec_IntWriteEntry(pManMR->vLags, Abc_ObjId(pObj), lag);
+}
+
+
+static void Abc_ObjPrintNeighborhood_rec( Abc_Obj_t *pObj, Vec_Ptr_t *vNodes, int depth ) {
+  Abc_Obj_t *pObj2;
+  int i;
+  
+  if (pObj->fMarkC || depth < 0) return;
+
+  pObj->fMarkC = 1;
+  Vec_PtrPush( vNodes, pObj );
+
+  Abc_ObjPrint( stdout, pObj );
+
+  Abc_ObjForEachFanout(pObj, pObj2, i) {
+    Abc_ObjPrintNeighborhood_rec( pObj2, vNodes, depth-1 );
+  }
+  Abc_ObjForEachFanin(pObj, pObj2, i) {
+    Abc_ObjPrintNeighborhood_rec( pObj2, vNodes, depth-1 );
+  }
+}
+
+void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth ) {
+  Vec_Ptr_t *vNodes = Vec_PtrAlloc(100); 
+  Abc_Obj_t *pObj2;
+
+  Abc_ObjPrintNeighborhood_rec( pObj, vNodes, depth );
+
+  while(Vec_PtrSize(vNodes)) {
+    pObj2 = Vec_PtrPop(vNodes);
+    pObj2->fMarkC = 0;
+  }
+
+  Vec_PtrFree(vNodes);
+}
diff --git a/src/opt/fret/fretime.h b/src/opt/fret/fretime.h
index 167543ce..bbb79d26 100644
--- a/src/opt/fret/fretime.h
+++ b/src/opt/fret/fretime.h
@@ -27,7 +27,8 @@
 // #define DEBUG_PRINT_FLOWS
 // #define DEBUG_VISITED
 // #define DEBUG_PREORDER
-// #define DEBUG_CHECK
+#define DEBUG_CHECK
+// #define DEBUG_PRINT_LEVELS
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -36,17 +37,18 @@
 #define MAX_DIST 30000
 
 // flags in Flow_Data structure...
-#define VISITED_E       0x01
-#define VISITED_R       0x02
+#define VISITED_E       0x001
+#define VISITED_R       0x002
 #define VISITED  (VISITED_E | VISITED_R)
-#define FLOW            0x04
-#define CROSS_BOUNDARY  0x08
-#define BLOCK           0x10
-#define INIT_0          0x20
-#define INIT_1          0x40
+#define FLOW            0x004
+#define CROSS_BOUNDARY  0x008
+#define BLOCK           0x010
+#define INIT_0          0x020
+#define INIT_1          0x040
 #define INIT_CARE (INIT_0 | INIT_1)
-#define CONSERVATIVE    0x80
+#define CONSERVATIVE    0x080
 #define BLOCK_OR_CONS (BLOCK | CONSERVATIVE)
+#define BIAS_NODE       0x100
 
 typedef struct Flow_Data_t_ {
   unsigned int mark : 16;
@@ -55,6 +57,7 @@ typedef struct Flow_Data_t_ {
     Abc_Obj_t   *pred;
     /* unsigned int var; */
     Abc_Obj_t   *pInitObj;
+    Abc_Obj_t   *pCopy;
     Vec_Ptr_t   *vNodes;
   };
 
@@ -63,26 +66,30 @@ typedef struct Flow_Data_t_ {
 } Flow_Data_t;
 
 // useful macros for manipulating Flow_Data structure...
-#define FDATA( x )     ((Flow_Data_t *)Abc_ObjCopy(x))
-#define FSET( x, y )   ((Flow_Data_t *)Abc_ObjCopy(x))->mark |= y
-#define FUNSET( x, y ) ((Flow_Data_t *)Abc_ObjCopy(x))->mark &= ~y
-#define FTEST( x, y )  (((Flow_Data_t *)Abc_ObjCopy(x))->mark & y)
+#define FDATA( x )     (pManMR->pDataArray+Abc_ObjId(x))
+#define FSET( x, y )   FDATA(x)->mark |= y
+#define FUNSET( x, y ) FDATA(x)->mark &= ~y
+#define FTEST( x, y )  (FDATA(x)->mark & y)
 #define FTIMEEDGES( x )  &(pManMR->vTimeEdges[Abc_ObjId( x )])
 
-static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
-  assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
-  FDATA(pObj)->pred = pPred;
-}
-static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
-  return FDATA(pObj)->pred;
-}
+typedef struct NodeLag_T_ {
+  int id;
+  int lag;
+} NodeLag_t;
 
+typedef struct InitConstraint_t_ {
+  Abc_Obj_t *pBiasNode;
+
+  Vec_Int_t  vNodes;
+  Vec_Int_t  vLags;
+
+} InitConstraint_t;
 
 typedef struct MinRegMan_t_ {
  
   // problem description:
   int         maxDelay;
-  bool        fComputeInitState, fGuaranteeInitState;
+  bool        fComputeInitState, fGuaranteeInitState, fBlockConst;
   int         nNodes, nLatches;
   bool        fForwardOnly, fBackwardOnly;
   bool        fConservTimingOnly;
@@ -99,24 +106,38 @@ typedef struct MinRegMan_t_ {
   int         fSolutionIsDc;
   int         constraintMask;
   int         iteration, subIteration;
+  Vec_Int_t  *vLags;
   
   // problem data
   Vec_Int_t   *vSinkDistHist;
   Flow_Data_t *pDataArray;
   Vec_Ptr_t   *vTimeEdges;
   Vec_Ptr_t   *vExactNodes;
+  Vec_Ptr_t   *vInitConstraints;
   Abc_Ntk_t   *pInitNtk;
   Vec_Ptr_t   *vNodes; // re-useable struct
-
+  
+  NodeLag_t   *pInitToOrig;
+  int          sizeInitToOrig;
+  
 } MinRegMan_t ;
 
+extern MinRegMan_t *pManMR;
+
 #define vprintf if (pManMR->fVerbose) printf 
 
+static inline void FSETPRED(Abc_Obj_t *pObj, Abc_Obj_t *pPred) {
+  assert(!Abc_ObjIsLatch(pObj)); // must preserve field to maintain init state linkage
+  FDATA(pObj)->pred = pPred;
+}
+static inline Abc_Obj_t * FGETPRED(Abc_Obj_t *pObj) {
+  return FDATA(pObj)->pred;
+}
+
 /*=== fretMain.c ==========================================================*/
- 
-extern MinRegMan_t *pManMR;
 
-Abc_Ntk_t *    Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInitState,
+Abc_Ntk_t *    Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose,
+                                      int fComputeInitState, int fGuaranteeInitState, int fBlockConst,
                                       int fForward, int fBackward, int nMaxIters,
                                       int maxDelay, int fFastButConservative);
 
@@ -128,6 +149,15 @@ int  Abc_FlowRetime_PushFlows( Abc_Ntk_t * pNtk, bool fVerbose );
 bool Abc_FlowRetime_IsAcrossCut( Abc_Obj_t *pCur, Abc_Obj_t *pNext );
 void Abc_FlowRetime_ClearFlows( bool fClearAll );
 
+int  Abc_FlowRetime_GetLag( Abc_Obj_t *pObj );
+void Abc_FlowRetime_SetLag( Abc_Obj_t *pObj, int lag );
+
+void Abc_FlowRetime_UpdateLags( );
+
+void Abc_ObjPrintNeighborhood( Abc_Obj_t *pObj, int depth );
+
+Abc_Ntk_t * Abc_FlowRetime_NtkSilentRestrash( Abc_Ntk_t * pNtk, bool fCleanup );
+
 /*=== fretFlow.c ==========================================================*/
 
 int  dfsplain_e( Abc_Obj_t *pObj, Abc_Obj_t *pPred );
@@ -150,6 +180,8 @@ void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk );
 int  Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk );
 
 void Abc_FlowRetime_ConstrainInit(  );
+void Abc_FlowRetime_AddInitBias(  );
+void Abc_FlowRetime_RemoveInitBias(  );
 
 /*=== fretTime.c ==========================================================*/