Version abc80222

28 files changed, 1502 insertions, 43 deletions

diff --git a/abc.dsp b/abc.dsp
index 5830eeb8..32cfed71 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -222,6 +222,10 @@ SOURCE=.\src\base\abci\abcDebug.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcDelay.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcDress.c
 # End Source File
 # Begin Source File
@@ -2962,6 +2966,10 @@ SOURCE=.\src\aig\aig\aigPart.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigPartReg.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigRepr.c
 # End Source File
 # Begin Source File
diff --git a/abc.rc b/abc.rc
index 22c0a0b7..5f7d5904 100644
--- a/abc.rc
+++ b/abc.rc
@@ -44,6 +44,7 @@ alias plat print_latch
 alias pio print_io
 alias pk print_kmap
 alias ps print_stats 
+alias psb print_stats -b
 alias psu print_supp
 alias psy print_symm
 alias pun print_unate
@@ -65,6 +66,7 @@ alias rvl read_verlib
 alias rsup read_super mcnc5_old.super
 alias rlib read_library
 alias rlibc read_library cadence.genlib
+alias rlut read_lut
 alias rw rewrite
 alias rwz rewrite -z
 alias rf refactor
@@ -104,7 +106,6 @@ alias choice      "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_r
 alias choice2     "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore"
 alias rwsat       "st; rw -l; b -l; rw -l; rf -l"
 alias rwsat2      "st; rw -l; b -l; rw -l; rf -l; fraig; rw -l; b -l; rw -l; rf -l"
-alias shake       "st; ps; sat -C 5000; rw -l; ps; sat -C 5000; b -l; rf -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000; rwz -l; ps; sat -C 5000; rfz -l; ps; sat -C 5000"
 alias share       "st; multi -m; fx; resyn2"
 
 # resubstitution scripts for the IWLS paper
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 9d9bf22a..ccc34caf 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -519,6 +519,7 @@ extern void            Aig_ObjOrderAdvance( Aig_Man_t * p );
 /*=== aigPart.c =========================================================*/
 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_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index c7488487..5681f689 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -46,11 +46,14 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
+//    if ( Aig_ObjIsPi(pObj) )
+//        return;
 //    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+    Aig_ObjSetTravIdCurrent(p, pObj);
     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-    Aig_ObjSetTravIdCurrent(p, pObj);
+//    assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
+//    Aig_ObjSetTravIdCurrent(p, pObj);
     Vec_PtrPush( vNodes, pObj );
 }
 
@@ -113,7 +116,7 @@ Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects internal nodes in the DFS order.]
+  Synopsis    [Collects internal nodes and PIs in the DFS order.]
 
   Description []
                
@@ -125,14 +128,14 @@ Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
 Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
 {
     Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
+//    Aig_Obj_t * pObj;
     int i;
     assert( Aig_ManLatchNum(p) == 0 );
     Aig_ManIncrementTravId( p );
     // mark constant and PIs
     Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjSetTravIdCurrent( p, pObj );
+//    Aig_ManForEachPi( p, pObj, i )
+//        Aig_ObjSetTravIdCurrent( p, pObj );
     // go through the nodes
     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
     for ( i = 0; i < nNodes; i++ )
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 9afc5f91..7e765f60 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -380,6 +380,58 @@ Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the register dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vSupports, * vMatrix;
+    Vec_Int_t * vSupp;
+    int iOut, iIn, k, m, i;
+    // get structural supports for each output
+    vSupports = Aig_ManSupports( p );
+    // transforms the supports into the latch dependency matrix
+    vMatrix = Vec_PtrStart( Aig_ManRegNum(p) );
+    Vec_PtrForEachEntry( vSupports, vSupp, i )
+    {
+        // skip true POs
+        iOut = Vec_IntPop( vSupp );
+        iOut -= Aig_ManPoNum(p) - Aig_ManRegNum(p);
+        if ( iOut < 0 )
+        {
+            Vec_IntFree( vSupp );
+            continue;
+        }
+        // remove PIs
+        m = 0;
+        Vec_IntForEachEntry( vSupp, iIn, k )
+        {
+            iIn -= Aig_ManPiNum(p) - Aig_ManRegNum(p);
+            if ( iIn < 0 )
+                continue;
+            assert( iIn < Aig_ManRegNum(p) );
+            Vec_IntWriteEntry( vSupp, m++, iIn );
+        }
+        Vec_IntShrink( vSupp, m );
+        // store support in the matrix
+        assert( iOut < Aig_ManRegNum(p) );
+        Vec_PtrWriteEntry( vMatrix, iOut, vSupp );
+    }
+    Vec_PtrFree( vSupports );
+    // check that all supports are used
+    Vec_PtrForEachEntry( vMatrix, vSupp, i )
+        assert( vSupp != NULL );
+    return vMatrix;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Start char-bases support representation.]
 
   Description []
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
new file mode 100644
index 00000000..1f218bd8
--- /dev/null
+++ b/src/aig/aig/aigPartReg.c
@@ -0,0 +1,428 @@
+/**CFile****************************************************************
+
+  FileName    [aigPartReg.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Register partitioning algorithm.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigPartReg.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Aig_ManPre_t_         Aig_ManPre_t;
+
+struct Aig_ManPre_t_
+{
+    // input data    
+    Aig_Man_t *     pAig;            // seq AIG manager 
+    Vec_Ptr_t *     vMatrix;         // register dependency
+    int             nRegsMax;        // the max number of registers in the cluster
+    // information about partitions
+    Vec_Ptr_t *     vParts;          // the partitions
+    char *          pfUsedRegs;      // the registers already included in the partitions
+    // info about the current partition
+    Vec_Int_t *     vRegs;           // registers of this partition
+    Vec_Int_t *     vUniques;        // unique registers of this partition
+    Vec_Int_t *     vFreeVars;       // free variables of this partition
+    Vec_Flt_t *     vPartCost;       // costs of adding each variable
+    char *          pfPartVars;      // input/output registers of the partition
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_ManPre_t * Aig_ManRegManStart( Aig_Man_t * pAig )
+{
+    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->vParts    = Vec_PtrAlloc(256);
+    p->vRegs     = Vec_IntAlloc(256);
+    p->vUniques  = Vec_IntAlloc(256);
+    p->vFreeVars = Vec_IntAlloc(256);
+    p->vPartCost = Vec_FltAlloc(256);
+    p->pfUsedRegs = ALLOC( char, Aig_ManRegNum(p->pAig) );
+    memset( p->pfUsedRegs, 0, sizeof(char) * Aig_ManRegNum(p->pAig) );
+    p->pfPartVars  = ALLOC( char, Aig_ManRegNum(p->pAig) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManRegManStop( Aig_ManPre_t * p )
+{
+    Vec_VecFree( (Vec_Vec_t *)p->vMatrix );
+    if ( p->vParts )
+        Vec_VecFree( (Vec_Vec_t *)p->vParts );
+    Vec_IntFree( p->vRegs );
+    Vec_IntFree( p->vUniques );
+    Vec_IntFree( p->vFreeVars );
+    Vec_FltFree( p->vPartCost );
+    free( p->pfUsedRegs );
+    free( p->pfPartVars );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the max-support register that is not taken yet.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManRegFindSeed( Aig_ManPre_t * p )
+{
+    int i, 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) );
+        if ( nRegsMax < nRegsCur )
+        {
+            nRegsMax = nRegsCur;
+            iMax = i;
+        }
+    }
+    return iMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the next register to be added to the set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManRegFindBestVar( Aig_ManPre_t * p )
+{
+    Vec_Int_t * vSupp;
+    int nNewVars, nNewVarsBest = AIG_INFINITY;
+    int iVarFree, iVarSupp, iVarBest = -1, i, k;
+    // go through the free variables
+    Vec_IntForEachEntry( p->vFreeVars, iVarFree, i )
+    {
+//        if ( p->pfUsedRegs[iVarFree] )
+//            continue;
+        // get support of this variable
+        vSupp = Vec_PtrEntry( p->vMatrix, iVarFree );
+        // count the number of new vars
+        nNewVars = 0;
+        Vec_IntForEachEntry( vSupp, iVarSupp, k )
+            nNewVars += !p->pfPartVars[iVarSupp];
+        // quit if there is no new variables
+        if ( nNewVars == 0 )
+            return iVarFree;
+        // compare the cost of this
+        if ( nNewVarsBest > nNewVars )
+        {
+            nNewVarsBest = nNewVars;
+            iVarBest = iVarFree;
+        }
+    }
+    return iVarBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
+{
+    Vec_Int_t * vSupp;
+    int RetValue, iVar, i;
+    // make sure this is a new variable
+//    assert( !p->pfUsedRegs[iReg] );
+    if ( !p->pfUsedRegs[iReg] )
+    {
+        p->pfUsedRegs[iReg] = 1;
+        Vec_IntPush( p->vUniques, iReg );
+    }
+    // remove it from the free variables
+    if ( Vec_IntSize(p->vFreeVars) > 0 )
+    {
+        assert( p->pfPartVars[iReg] );
+        RetValue = Vec_IntRemove( p->vFreeVars, iReg );
+        assert( RetValue );
+    }
+    else
+        assert( !p->pfPartVars[iReg] );
+    // add it to the partition
+    p->pfPartVars[iReg] = 1;
+    Vec_IntPush( p->vRegs, iReg );
+    // add new variables
+    vSupp = Vec_PtrEntry( p->vMatrix, iReg );
+    Vec_IntForEachEntry( vSupp, iVar, i )
+    {
+        if ( p->pfPartVars[iVar] )
+            continue;
+        p->pfPartVars[iVar] = 1;
+        Vec_IntPush( p->vFreeVars, iVar );
+    }
+    // add it to the cost
+    Vec_FltPush( p->vPartCost, 1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    Vec_Ptr_t * vNodes;
+    Vec_Ptr_t * vRoots;
+    int nOffset, iOut, i;
+    int nCountPis, nCountRegs;
+    // collect roots
+    vRoots = Vec_PtrAlloc( Vec_IntSize(vPart) );
+    nOffset = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
+    Vec_IntForEachEntry( vPart, iOut, i )
+    {
+        pObj = Aig_ManPo(pAig, nOffset+iOut);
+        Vec_PtrPush( vRoots, Aig_ObjFanin0(pObj) );
+    }
+    // collect/mark nodes/PIs in the DFS order
+    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(vRoots), Vec_PtrSize(vRoots) );
+    Vec_PtrFree( vRoots );
+    // unmark register outputs
+    nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
+    Vec_IntForEachEntry( vPart, iOut, i )
+    {
+        pObj = Aig_ManPi(pAig, nOffset+iOut);
+        Aig_ObjSetTravIdPrevious( pAig, pObj );
+    }
+    // count pure PIs
+    nCountPis = nCountRegs = 0;
+    Aig_ManForEachPiSeq( pAig, pObj, i )
+        nCountPis += Aig_ObjIsTravIdCurrent(pAig, pObj);
+    // count outputs of other registers
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        nCountRegs += Aig_ObjIsTravIdCurrent(pAig, pObj);
+    if ( pnCountPis )
+        *pnCountPis = nCountPis;
+    if ( pnCountRegs )
+        *pnCountRegs = nCountRegs;
+    // create the new manager
+    pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pNew);
+    // create the PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+            pObj->pData = Aig_ObjCreatePi(pNew);
+    // add variables for the register outputs
+    // create fake POs to hold the register outputs
+    Vec_IntForEachEntry( vPart, iOut, i )
+    {
+        pObj = Aig_ManPi(pAig, nOffset+iOut);
+        pObj->pData = Aig_ObjCreatePi(pNew);
+        Aig_ObjCreatePo( pNew, pObj->pData );
+    }
+    // create the nodes
+    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 )
+    {
+        pObj = Aig_ManPo( pAig, nOffset+iOut );
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    pNew->nRegs = Vec_IntSize(vPart);
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig )
+{
+    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+
+    Aig_ManPre_t * p;
+    Vec_Ptr_t * vResult;
+    int iSeed, iNext, i, k;
+    // create the manager
+    p = Aig_ManRegManStart( pAig );
+    // add partitions as long as registers remain
+    for ( i = 0; (iSeed = Aig_ManRegFindSeed(p)) >= 0; i++ )
+    {
+printf( "Seed variable = %d.\n", iSeed );
+        // clean the current partition information
+        Vec_IntClear( p->vRegs );
+        Vec_IntClear( p->vUniques );
+        Vec_IntClear( p->vFreeVars );
+        Vec_FltClear( p->vPartCost );
+        memset( p->pfPartVars, 0, sizeof(char) * Aig_ManRegNum(p->pAig) );
+        // add the register and its partition support
+        Aig_ManRegPartitionAdd( p, iSeed );
+        // select the best var to add
+        for ( k = 0; Vec_IntSize(p->vRegs) < p->nRegsMax; k++ )
+        {
+            // get the next best variable
+            iNext = Aig_ManRegFindBestVar( p );
+            if ( iNext == -1 )
+                break;
+            // 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) );
+            // quit if there are not free variables
+            if ( Vec_IntSize(p->vFreeVars) == 0 )
+                break;
+        }
+        // add this partition to the set
+        Vec_PtrPush( p->vParts, Vec_IntDup(p->vRegs) );        
+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" ); 
+    }
+    vResult = p->vParts; p->vParts = NULL;
+    Aig_ManRegManStop( p );
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize )
+{
+    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++ )
+    {
+        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 );
+    }
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes partitioning of registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManRegPartitionRun( Aig_Man_t * pAig )
+{
+    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 )
+    {
+        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 );
+    }
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 67040e2c..b02d3bb5 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -12,6 +12,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigOper.c \
     src/aig/aig/aigOrder.c \
     src/aig/aig/aigPart.c \
+    src/aig/aig/aigPartReg.c \
     src/aig/aig/aigRepr.c \
     src/aig/aig/aigRet.c \
     src/aig/aig/aigRetF.c \
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index fab9093d..2ee66916 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -223,7 +223,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
         return;
     }
     fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
-    fprintf( pFile, "p %d %d\n", p->nVars, p->nClauses );
+    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
     for ( i = 0; i < p->nClauses; i++ )
     {
         for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c
index d966df15..8453e3cc 100644
--- a/src/aig/cnf/cnfMap.c
+++ b/src/aig/cnf/cnfMap.c
@@ -44,7 +44,8 @@ void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut, int * pAreaFlows )
     Aig_Obj_t * pLeaf;
     int i;
     pCut->Value = 0;
-    pCut->uSign = 100 * Cnf_CutSopCost( p, pCut );
+//    pCut->uSign = 100 * Cnf_CutSopCost( p, pCut );
+    pCut->uSign = 10 * Cnf_CutSopCost( p, pCut );
     Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
     {
         pCut->Value += pLeaf->nRefs;
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 8796f827..4a3f9b03 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -130,7 +130,7 @@ int Fra_OneHotNodesAreClause( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * p
 ***********************************************************************/
 Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
 {
-    int fSkipConstEqu = 0;
+    int fSkipConstEqu = 1;
     Vec_Int_t * vOneHots;
     Aig_Obj_t * pObj1, * pObj2;
     int i, k;
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f09d7626..fdff8b39 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -203,6 +203,7 @@ struct Abc_Ntk_t_
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;
     Hop_Man_t *       pHaig;         // history AIG
+    float *           pLutTimes;     // arrivals/requireds/slacks using LUT-delay model
     // node attributes
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
 };
@@ -521,6 +522,7 @@ extern Abc_Obj_t *        Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Ab
 extern Abc_Obj_t *        Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType );
 extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern Abc_Obj_t *        Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
 extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
 extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
 extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
@@ -731,7 +733,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 );
+extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest );
 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/abc/abcAig.c b/src/base/abc/abcAig.c
index 16f66dc6..89026863 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -737,6 +737,22 @@ Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     return Abc_AigOr( pMan, Abc_AigAnd(pMan, p0, Abc_ObjNot(p1)), 
                             Abc_AigAnd(pMan, p1, Abc_ObjNot(p0)) );
 }
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 )
+{
+    return Abc_AigOr( pMan, Abc_AigAnd(pMan, pC, p1), Abc_AigAnd(pMan, Abc_ObjNot(pC), p0) );
+}
  
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index fd3b9253..778581c2 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -1031,7 +1031,7 @@ int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk )
   Synopsis    [Recursively detects combinational loops.]
 
   Description []
-               
+                
   SideEffects []
 
   SeeAlso     []
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index b1f75ab6..5c565ce6 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1031,6 +1031,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_PtrFree( pNtk->vAttrs );
     FREE( pNtk->pName );
     FREE( pNtk->pSpec );
+    FREE( pNtk->pLutTimes );
     free( pNtk );
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 31c09fd2..492d1910 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -70,6 +70,8 @@ static int Abc_CommandDisjoint       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandLutpack        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandImfs           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMfs            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTrace          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSpeedup        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRewrite        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -250,6 +252,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "lutpack",       Abc_CommandLutpack,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "imfs",          Abc_CommandImfs,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs",           Abc_CommandMfs,              1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -402,6 +406,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
 void Abc_End()
 {
 //    Dar_LibDumpPriorities();
+    {
+        extern int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk );
+        Abc_NtkCompareAndSaveBest( NULL );
+    }
 
     {
         extern void Cnf_ClearMemory();
@@ -432,28 +440,28 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    bool fShort;
-    int c;
     int fFactor;
+    int fSaveBest;
+    int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set the defaults
-    fShort  = 1;
-    fFactor = 0;
+    fFactor   = 0;
+    fSaveBest = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "sfh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fbh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 's':
-            fShort ^= 1;
-            break;
         case 'f':
             fFactor ^= 1;
             break;
+        case 'b':
+            fSaveBest ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -466,13 +474,14 @@ 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 );
+    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_stats [-fh]\n" );
+    fprintf( pErr, "usage: print_stats [-fbh]\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-h    : print the command usage\n");
     return 1;
 }
@@ -558,7 +567,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
         printf( "EXDC network statistics: \n" );
-    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0 );
+    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0 );
     return 0;
 
 usage:
@@ -3130,7 +3139,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nWindow      = 62;
     pPars->nCands       =  5;
     pPars->nSimWords    =  4;
-    pPars->nGrowthLevel =  1;
+    pPars->nGrowthLevel =  0;
     pPars->fArea        =  0;
     pPars->fVerbose     =  0;
     pPars->fVeryVerbose =  0;
@@ -3262,9 +3271,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nWinTfoLevs  =   2;
     pPars->nFanoutsMax  =  10;
     pPars->nDepthMax    =  20;
-    pPars->nDivMax      = 200;
+    pPars->nDivMax      = 250;
     pPars->nWinSizeMax  = 300;
-    pPars->nGrowthLevel =   1;
+    pPars->nGrowthLevel =   0;
     pPars->fResub       =   1;
     pPars->fArea        =   0;
     pPars->fMoreEffort  =   0;
@@ -3381,7 +3390,7 @@ usage:
     fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
     fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
     fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
-    fprintf( pErr, "\t-M <num> : the max size of  window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+    fprintf( pErr, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
     fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
     fprintf( pErr, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
     fprintf( pErr, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
@@ -3393,6 +3402,190 @@ usage:
     return 1;
 } 
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandTrace( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Mfs_Par_t Pars, * pPars = &Pars;
+    int c;
+    int fUseLutLib;
+    int fVerbose;
+    extern void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseLutLib = 0;
+    fVerbose   = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUseLutLib ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to a logic network.\n" );
+        return 1;
+    }
+
+    // modify the current network
+    Abc_NtkDelayTracePrint( pNtk, fUseLutLib, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: trace [-lvh]\n" );
+    fprintf( pErr, "\t           performs delay trace of LUT-mapped network\n" );
+    fprintf( pErr, "\t-l       : toggle using unit- or LUT-library-delay model [default = %s]\n", fUseLutLib? "lib": "unit" );
+    fprintf( pErr, "\t-v       : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : print the command usage\n");
+    return 1;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Mfs_Par_t Pars, * pPars = &Pars;
+    int c;
+    int fUseLutLib;
+    int Percentage;
+    int Degree;
+    int fVerbose;
+    int fVeryVerbose;
+    extern Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseLutLib = 0;
+    Percentage = 3;
+    Degree     = 2;
+    fVerbose   = 0;
+    fVeryVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PNlvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Percentage = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Percentage < 1 || Percentage > 100 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Degree = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Degree < 1 || Degree > 5 ) 
+                goto usage;
+            break;
+        case 'l':
+            fUseLutLib ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to a logic network.\n" );
+        return 1;
+    }
+
+    // modify the current network
+    pNtkRes = Abc_NtkSpeedup( pNtk, fUseLutLib, Percentage, Degree, fVerbose, fVeryVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "The command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: speedup [-P num] [-N num] [-lvwh]\n" );
+    fprintf( pErr, "\t           transforms LUT-mapped network into an AIG with choices;\n" );
+    fprintf( pErr, "\t           the choices are added to speedup the next round of mapping\n" );
+    fprintf( pErr, "\t-P <num> : delay delta defining critical path for library model [default = %d%%]\n", Percentage );
+    fprintf( pErr, "\t-N <num> : the max critical path degree for resynthesis (0 < num < 6) [default = %d]\n", Degree );
+    fprintf( pErr, "\t-l       : toggle using unit- or LUT-library-delay model [default = %s]\n", fUseLutLib? "lib" : "unit" );
+    fprintf( pErr, "\t-v       : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : print the command usage\n");
+    return 1;
+} 
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -6656,13 +6849,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 );
 
     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;
@@ -6837,6 +7031,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     Abc_NtkDarTestBlif( argv[globalUtilOptind] );
 */
+
+    Abc_NtkDarPartition( pNtk );
+
     return 0;
 usage:
     fprintf( pErr, "usage: test [-vwh]\n" );
@@ -10642,10 +10839,16 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( pPars->fSeqMap )
+    {
+        fprintf( pErr, "Sequential mapping is currently disabled.\n" );
+        return 1;
+    }
+
     // enable truth table computation if choices are selected
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
+    if ( (c = Abc_NtkGetChoiceNum( pNtk )) )
     {
-        printf( "Performing FPGA mapping with choices.\n" );
+        printf( "Performing LUT mapping with %d choices.\n", c );
         pPars->fTruth = 1;
     }
     // enable truth table computation if cut minimization is selected
@@ -11034,7 +11237,7 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "The current network is combinational.\n" );
-        return 1;
+        return 0;
     }
 
     // update the network
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 6c5cabce..119a2a97 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -326,7 +326,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
-        if ( pTemp = pMan->pEquivs[pObj->Id] )
+        if ( (pTemp = pMan->pEquivs[pObj->Id]) )
         {
             Abc_Obj_t * pAbcRepr, * pAbcObj;
             assert( pTemp->pData != NULL );
@@ -1565,6 +1565,32 @@ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
     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
new file mode 100644
index 00000000..7317b41b
--- /dev/null
+++ b/src/base/abci/abcDelay.c
@@ -0,0 +1,587 @@
+/**CFile****************************************************************
+
+  FileName    [abcDelay.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Delay trace and speedup.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDelay.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline float Abc_ObjArrival( Abc_Obj_t * pNode )                 { return pNode->pNtk->pLutTimes[3*pNode->Id+0]; }
+static inline float Abc_ObjRequired( Abc_Obj_t * pNode )                { return pNode->pNtk->pLutTimes[3*pNode->Id+1]; }
+static inline float Abc_ObjSlack( Abc_Obj_t * pNode )                   { return pNode->pNtk->pLutTimes[3*pNode->Id+2]; }
+
+static inline void  Abc_ObjSetArrival( Abc_Obj_t * pNode, float Time )  { pNode->pNtk->pLutTimes[3*pNode->Id+0] = Time; }
+static inline void  Abc_ObjSetRequired( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+1] = Time; }
+static inline void  Abc_ObjSetSlack( Abc_Obj_t * pNode, float Time )    { pNode->pNtk->pLutTimes[3*pNode->Id+2] = Time; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the pins in the decreasing order of delays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinDelays )
+{
+    Abc_Obj_t * pFanin;
+    int i, j, best_i, temp;
+    // start the trivial permutation and collect pin delays
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        pPinPerm[i] = i;
+        pPinDelays[i] = Abc_ObjArrival(pFanin);
+    }
+    // selection sort the pins in the decreasible order of delays
+    // this order will match the increasing order of LUT input pins
+    for ( i = 0; i < Abc_ObjFaninNum(pNode)-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < Abc_ObjFaninNum(pNode); j++ )
+            if ( pPinDelays[pPinPerm[j]] > pPinDelays[pPinPerm[best_i]] )
+                best_i = j;
+        if ( best_i == i )
+            continue;
+        temp = pPinPerm[i]; 
+        pPinPerm[i] = pPinPerm[best_i]; 
+        pPinPerm[best_i] = temp;
+    }
+    // verify
+    assert( pPinPerm[0] < Abc_ObjFaninNum(pNode) );
+    for ( i = 1; i < Abc_ObjFaninNum(pNode); i++ )
+    {
+        assert( pPinPerm[i] < Abc_ObjFaninNum(pNode) );
+        assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
+{
+    extern void * Abc_FrameReadLibLut();   
+    int pPinPerm[32];
+    float pPinDelays[32];
+    If_Lib_t * pLutLib;
+    Abc_Obj_t * pNode, * pFanin;
+    Vec_Ptr_t * vNodes;
+    float tArrival, tRequired, tSlack, * pDelays;
+    int i, k;
+
+    assert( Abc_NtkIsLogic(pNtk) );
+    // 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 -ABC_INFINITY;
+    }
+
+    // initialize the arrival times
+    FREE( pNtk->pLutTimes );
+    pNtk->pLutTimes = ALLOC( float, 3 * Abc_NtkObjNumMax(pNtk) );
+    for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
+    {
+        pNtk->pLutTimes[3*i+0] = pNtk->pLutTimes[3*i+2] = 0;
+        pNtk->pLutTimes[3*i+1] = ABC_INFINITY;
+    }
+
+    // propagate arrival times
+    vNodes = Abc_NtkDfs( pNtk, 1 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        tArrival = -ABC_INFINITY;
+        if ( pLutLib == NULL )
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+                if ( tArrival < Abc_ObjArrival(pFanin) + 1.0 )
+                    tArrival = Abc_ObjArrival(pFanin) + 1.0;
+        }
+        else if ( !pLutLib->fVarPinDelays )
+        {
+            pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+                if ( tArrival < Abc_ObjArrival(pFanin) + pDelays[0] )
+                    tArrival = Abc_ObjArrival(pFanin) + pDelays[0];
+        }
+        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 ( Abc_ObjFaninNum(pNode) == 0 )
+            tArrival = 0.0;
+        Abc_ObjSetArrival( pNode, tArrival );
+    }
+    Vec_PtrFree( vNodes );
+
+    // get the latest arrival times
+    tArrival = -ABC_INFINITY;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        if ( tArrival < Abc_ObjArrival(Abc_ObjFanin0(pNode)) )
+            tArrival = Abc_ObjArrival(Abc_ObjFanin0(pNode));
+
+    // initialize the required times
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        if ( Abc_ObjRequired(Abc_ObjFanin0(pNode)) > tArrival )
+            Abc_ObjSetRequired( Abc_ObjFanin0(pNode), tArrival );
+
+    // propagate the required times
+    vNodes = Abc_NtkDfsReverse( pNtk );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( pLutLib == NULL )
+        {
+            tRequired = Abc_ObjRequired(pNode) - (float)1.0;
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+                if ( Abc_ObjRequired(pFanin) > tRequired )
+                    Abc_ObjSetRequired( pFanin, tRequired );
+        }
+        else if ( !pLutLib->fVarPinDelays )
+        {
+            pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
+            tRequired = Abc_ObjRequired(pNode) - pDelays[0];
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+                if ( Abc_ObjRequired(pFanin) > tRequired )
+                    Abc_ObjSetRequired( pFanin, tRequired );
+        }
+        else 
+        {
+            pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
+            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 );
+            }
+        }
+        // set slack for this object
+        tSlack = Abc_ObjRequired(pNode) - Abc_ObjArrival(pNode);
+        assert( tSlack + 0.001 > 0.0 );
+        Abc_ObjSetSlack( pNode, tSlack < 0.0 ? 0.0 : tSlack );
+    }
+    Vec_PtrFree( vNodes );
+    return tArrival;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determines timing-critical edges of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Abc_NtkDelayTraceTCEdges( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, float tDelta, int fUseLutLib )
+{
+    int pPinPerm[32];
+    float pPinDelays[32];
+    If_Lib_t * pLutLib;
+    Abc_Obj_t * pFanin;
+    unsigned uResult = 0;
+    float tRequired, * pDelays;
+    int k;
+    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
+    tRequired = Abc_ObjRequired(pNode);
+    if ( pLutLib == NULL )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            if ( tRequired < Abc_ObjArrival(pFanin) + 1.0 + tDelta )
+                uResult |= (1 << k);
+    }
+    else if ( !pLutLib->fVarPinDelays )
+    {
+        pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            if ( tRequired < Abc_ObjArrival(pFanin) + pDelays[0] + tDelta )
+                uResult |= (1 << k);
+    }
+    else
+    {
+        pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)];
+        Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            if ( tRequired < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] + tDelta )
+                uResult |= (1 << pPinPerm[k]);
+    }
+    return uResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delay tracing of the LUT mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose )
+{
+    Abc_Obj_t * pNode;
+    int i, Nodes, * pCounters;
+    float tArrival, tDelta, nSteps, Num;
+    // decide how many steps
+    nSteps = fUseLutLib ? 20 : Abc_NtkLevel(pNtk);
+    pCounters = ALLOC( int, nSteps + 1 );
+    memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
+    // perform delay trace
+    tArrival = Abc_NtkDelayTraceLut( pNtk, fUseLutLib );
+    tDelta = tArrival / nSteps;
+    // count how many nodes have slack in the corresponding intervals
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Num = Abc_ObjSlack(pNode) / tDelta;
+        assert( Num >=0 && Num <= nSteps );
+        pCounters[(int)Num]++;
+    }
+    // print the results
+    printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, fUseLutLib? "LUT library" : "unit-delay" );
+    Nodes = 0;
+    for ( i = 0; i < nSteps; i++ )
+    {
+        Nodes += pCounters[i];
+        printf( "%3d %s : %5d  (%6.2f %%)\n", fUseLutLib? 5*(i+1) : i+1, 
+            fUseLutLib? "%":"lev", Nodes, 100.0*Nodes/Abc_NtkNodeNum(pNtk) );
+    }
+    free( pCounters );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_AigCheckTfi_rec( Abc_Obj_t * pNode, Abc_Obj_t * pOld )
+{
+    // check the trivial cases
+    if ( pNode == NULL )
+        return 0;
+    if ( Abc_ObjIsCi(pNode) )
+        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // skip the visited node
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return 0;
+    Abc_NodeSetTravIdCurrent( pNode );
+    // check the children
+    if ( Abc_AigCheckTfi_rec( Abc_ObjFanin0(pNode), pOld ) )
+        return 1;
+    if ( Abc_AigCheckTfi_rec( Abc_ObjFanin1(pNode), pOld ) )
+        return 1;
+    // check equivalent nodes
+    return Abc_AigCheckTfi_rec( pNode->pData, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_AigCheckTfi( Abc_Obj_t * pNew, Abc_Obj_t * pOld )
+{
+    assert( !Abc_ObjIsComplement(pNew) );
+    assert( !Abc_ObjIsComplement(pOld) );
+    Abc_NtkIncrementTravId( pNew->pNtk );
+    return Abc_AigCheckTfi_rec( pNew, pOld );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds strashed nodes for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return;
+    assert( Abc_ObjIsNode(pNode) );
+    Abc_NodeSetTravIdCurrent( pNode );
+    Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes );
+    Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes );
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds strashed nodes for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSpeedupNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pAig, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vTimes )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pObj2, * pAnd;
+    Abc_Obj_t * ppCofs[32];
+    int nCofs, i, k, nSkip;
+
+    // quit of regulars are the same
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( vLeaves, pObj2, k )
+        if ( i != k && Abc_ObjRegular(pObj->pCopy) == Abc_ObjRegular(pObj2->pCopy) )
+        {
+//            printf( "Identical after structural hashing!!!\n" );
+            return;
+        }
+
+    // collect the AIG nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pAig );
+    Abc_NodeSetTravIdCurrent( Abc_AigConst1(pAig) );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        pAnd = pObj->pCopy;
+        Abc_NodeSetTravIdCurrent( Abc_ObjRegular(pAnd) );
+    }
+    // traverse from the root node
+    pAnd = pNode->pCopy;
+    Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes );
+
+    // derive cofactors
+    nCofs = (1 << Vec_PtrSize(vTimes));
+    for ( i = 0; i < nCofs; i++ )
+    {
+        Vec_PtrForEachEntry( vLeaves, pObj, k )
+        {
+            pAnd = pObj->pCopy;
+            Abc_ObjRegular(pAnd)->pCopy = Abc_ObjRegular(pAnd);
+        }
+        Vec_PtrForEachEntry( vTimes, pObj, k )
+        {
+            pAnd = pObj->pCopy;
+            Abc_ObjRegular(pAnd)->pCopy = Abc_ObjNotCond( Abc_AigConst1(pAig), ((i & (1<<k)) == 0) );
+        }
+        Vec_PtrForEachEntry( vNodes, pObj, k )
+            pObj->pCopy = Abc_AigAnd( pAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+        // save the result
+        pAnd = pNode->pCopy;
+        ppCofs[i] = Abc_ObjNotCond( Abc_ObjRegular(pAnd)->pCopy, Abc_ObjIsComplement(pAnd) );
+    }
+    Vec_PtrFree( vNodes );
+
+//Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), ppCofs[0] );
+//Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), ppCofs[1] );
+
+    // collect the resulting tree
+    Vec_PtrForEachEntry( vTimes, pObj, k )
+        for ( nSkip = (1<<k), i = 0; i < nCofs; i += 2*nSkip )
+        {
+            pAnd = pObj->pCopy;
+            ppCofs[i] = Abc_AigMux( pAig->pManFunc, Abc_ObjRegular(pAnd), ppCofs[i+nSkip], ppCofs[i] );
+        }
+//Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), ppCofs[0] );
+
+    // create choice node
+    pAnd = Abc_ObjRegular(pNode->pCopy); // repr
+    pObj = Abc_ObjRegular(ppCofs[0]);    // new
+    if ( pAnd->pData == NULL && pObj->pData == NULL && !Abc_AigCheckTfi(pObj, pAnd) )
+    {
+        pObj->pData = pAnd->pData;
+        pAnd->pData = pObj;
+    }
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds choices to speed up the network by the given percentage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose )
+{
+    Abc_Ntk_t * pNtkNew;
+    Vec_Ptr_t * vTimeCries, * vTimeFanins;
+    Abc_Obj_t * pNode, * pFanin, * pFanin2;
+    float tDelta, tArrival;
+    int i, k, k2, Counter, CounterRes, nTimeCris;
+    unsigned * puTCEdges;
+    // perform delay trace
+    tArrival = Abc_NtkDelayTraceLut( pNtk, fUseLutLib );
+    tDelta = fUseLutLib ? tArrival*Percentage/100.0 : 1.0;
+    if ( fVerbose )
+    {
+        printf( "Max delay = %.2f. Delta = %.2f. ", tArrival, tDelta );
+        printf( "Using %s model. ", fUseLutLib? "LUT library" : "unit-delay" );
+        if ( fUseLutLib )
+            printf( "Percentage = %d. ", Percentage );
+        printf( "\n" );
+    }
+    // mark the timing critical nodes and edges
+    puTCEdges = ALLOC( int, Abc_NtkObjNumMax(pNtk) );
+    memset( puTCEdges, 0, sizeof(int) * Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjSlack(pNode) >= tDelta )
+            continue;
+        puTCEdges[pNode->Id] = Abc_NtkDelayTraceTCEdges( pNtk, pNode, tDelta, fUseLutLib );
+    }
+    if ( fVerbose )
+    {
+        Counter = CounterRes = 0;
+        Abc_NtkForEachNode( pNtk, pNode, i )
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+                if ( !Abc_ObjIsCi(pFanin) && Abc_ObjSlack(pFanin) < tDelta )
+                    Counter++;
+            CounterRes += Extra_WordCountOnes( puTCEdges[pNode->Id] );
+        }
+        printf( "Edges: Total = %7d. 0-slack = %7d. Critical = %7d. Ratio = %4.2f\n", 
+            Abc_NtkGetTotalFanins(pNtk), Counter, CounterRes, 1.0*CounterRes/Counter );
+    }
+    // start the resulting network
+    pNtkNew = Abc_NtkStrash( pNtk, 0, 1, 0 );
+
+    // collect nodes to be used for resynthesis
+    Counter = CounterRes = 0;
+    vTimeCries = Vec_PtrAlloc( 16 );
+    vTimeFanins = Vec_PtrAlloc( 16 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjSlack(pNode) >= tDelta )
+            continue;
+        // count the number of non-PI timing-critical nodes
+        nTimeCris = 0;
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            if ( !Abc_ObjIsCi(pFanin) && (puTCEdges[pNode->Id] & (1<<k)) )
+                nTimeCris++;
+        if ( !fVeryVerbose && nTimeCris == 0 )
+            continue;
+        Counter++;
+        // count the total number of timingn critical second-generation nodes
+        Vec_PtrClear( vTimeCries );
+        if ( nTimeCris )
+        {
+            Abc_ObjForEachFanin( pNode, pFanin, k )
+                if ( !Abc_ObjIsCi(pFanin) && (puTCEdges[pNode->Id] & (1<<k)) )
+                    Abc_ObjForEachFanin( pFanin, pFanin2, k2 )
+                        if ( puTCEdges[pFanin->Id] & (1<<k2) )
+                            Vec_PtrPushUnique( vTimeCries, pFanin2 );
+        }
+//        if ( !fVeryVerbose && (Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree) )
+        if ( (Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree) )
+            continue;
+        CounterRes++;
+        // collect second generation nodes
+        Vec_PtrClear( vTimeFanins );
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            if ( Abc_ObjIsCi(pFanin) )
+                Vec_PtrPushUnique( vTimeFanins, pFanin );
+            else
+                Abc_ObjForEachFanin( pFanin, pFanin2, k2 )
+                    Vec_PtrPushUnique( vTimeFanins, pFanin2 );                    
+        }
+        // print the results
+        if ( fVeryVerbose )
+        {
+        printf( "%5d Node %5d : %d %2d %2d  ", Counter, pNode->Id, 
+            nTimeCris, Vec_PtrSize(vTimeCries), Vec_PtrSize(vTimeFanins) );
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+            printf( "%d(%.2f)%s ", pFanin->Id, Abc_ObjSlack(pFanin), (puTCEdges[pNode->Id] & (1<<k))? "*":"" );
+        printf( "\n" );
+        }
+        // add the node to choices
+        if ( Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree )
+            continue;
+        Abc_NtkSpeedupNode( pNtk, pNtkNew, pNode, vTimeFanins, vTimeCries );
+    }
+    Vec_PtrFree( vTimeCries );
+    Vec_PtrFree( vTimeFanins );
+    free( puTCEdges );
+    if ( fVerbose )
+        printf( "Nodes: Total = %7d. 0-slack = %7d. Workable = %7d. Ratio = %4.2f\n", 
+            Abc_NtkNodeNum(pNtk), Counter, CounterRes, 1.0*CounterRes/Counter ); 
+
+    // remove invalid choice nodes
+    Abc_AigForEachAnd( pNtkNew, pNode, i )
+        if ( pNode->pData )
+        {
+            if ( Abc_ObjFanoutNum(pNode->pData) > 0 )
+                pNode->pData = NULL;
+        }
+
+    // return the result
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 3bc9fbed..9cc4e2c6 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -51,12 +51,13 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int
     Fpga_Man_t * pMan;
     Vec_Int_t * vSwitching;
     float * pSwitching = NULL;
+    int Num;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // print a warning about choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Performing FPGA mapping with choices.\n" );
+    if ( (Num = Abc_NtkGetChoiceNum( pNtk )) )
+        printf( "Performing LUT mapping with %d choices.\n", Num );
 
     // compute switching activity
     fShowSwitching |= fSwitching;
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 6135d009..5d35f329 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -42,6 +42,66 @@ int s_ResynTime = 0;
 
 /**Function*************************************************************
 
+  Synopsis    [If the network is best, saves it in "best.blif" and returns 1.]
+
+  Description [If the networks are incomparable, saves the new network, 
+  returns its parameters in the internal parameter structure, and returns 1.
+  If the new network is not a logic network, quits without saving and returns 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
+{
+    extern void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType );
+    static struct ParStruct {
+        char * pName;  // name of the best saved network
+        int    Depth;  // depth of the best saved network
+        int    Flops;  // flops in the best saved network 
+        int    Nodes;  // nodes in the best saved network
+        int    nPis;   // the number of primary inputs
+        int    nPos;   // the number of primary outputs
+    } ParsNew, ParsBest = { 0 };
+    // free storage for the name
+    if ( pNtk == NULL )
+    {
+        FREE( ParsBest.pName );
+        return 0;
+    }
+    // quit if not a logic network
+    if ( !Abc_NtkIsLogic(pNtk) )
+        return 0;
+    // get the parameters
+    ParsNew.Depth = Abc_NtkLevel( pNtk );
+    ParsNew.Flops = Abc_NtkLatchNum( pNtk );
+    ParsNew.Nodes = Abc_NtkNodeNum( pNtk );
+    ParsNew.nPis  = Abc_NtkPiNum( pNtk );
+    ParsNew.nPos  = Abc_NtkPoNum( pNtk );
+    // reset the parameters if the network has the same name
+    if ( ParsBest.pName == NULL || 
+         strcmp(ParsBest.pName, pNtk->pName) ||
+         ParsBest.Depth >  ParsNew.Depth || 
+         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops || 
+         ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes )
+    {
+        FREE( ParsBest.pName );
+        ParsBest.pName = Extra_UtilStrsav( pNtk->pName );
+        ParsBest.Depth = ParsNew.Depth; 
+        ParsBest.Flops = ParsNew.Flops; 
+        ParsBest.Nodes = ParsNew.Nodes; 
+        ParsBest.nPis  = ParsNew.nPis; 
+        ParsBest.nPos  = ParsNew.nPos;
+        // writ the network
+        Io_Write( pNtk, "best.blif", IO_FILE_BLIF );
+        return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Print the vital stats of the network.]
 
   Description []
@@ -51,10 +111,13 @@ int s_ResynTime = 0;
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest )
 {
     int Num;
 
+    if ( fSaveBest )
+        Abc_NtkCompareAndSaveBest( pNtk );
+
 //    if ( Abc_NtkIsStrash(pNtk) )
 //        Abc_AigCountNext( pNtk->pManFunc );
 
@@ -220,6 +283,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 
 //    if ( Abc_NtkHasSop(pNtk) )
 //        printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
+   
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 4558119e..55b724b8 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -9,6 +9,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcCut.c \
     src/base/abci/abcDar.c \
     src/base/abci/abcDebug.c \
+    src/base/abci/abcDelay.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcEspresso.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 8640b7a8..4cac6190 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -169,7 +169,7 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
 
     pAbc->TimeTotal += pAbc->TimeCommand;
     fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
-        (float)pAbc->TimeCommand / CLOCKS_PER_SEC, (float)pAbc->TimeTotal / CLOCKS_PER_SEC );
+        (float)(1.0 * pAbc->TimeCommand / CLOCKS_PER_SEC), (float)(1.0 * pAbc->TimeTotal / CLOCKS_PER_SEC) );
 /*
     {
         FILE * pTable;
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 09ad96f3..1d8cd70f 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "main.h"
+#include "port_type.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -60,8 +61,8 @@ struct Abc_Frame_t_
     FILE *          Err;
     FILE *          Hst;
     // used for runtime measurement
-    int             TimeCommand; // the runtime of the last command
-    int             TimeTotal;   // the total runtime of all commands
+    PORT_INT64_T    TimeCommand; // the runtime of the last command
+    PORT_INT64_T    TimeTotal;   // the total runtime of all commands
     // temporary storage for structural choices
     Vec_Ptr_t *     vStore;      // networks to be used by choice
     // decomposition package
diff --git a/src/misc/util/port_type.h b/src/misc/util/port_type.h
new file mode 100644
index 00000000..316905f3
--- /dev/null
+++ b/src/misc/util/port_type.h
@@ -0,0 +1,60 @@
+// Portable Data Types
+
+#ifndef __PORT_TYPE__
+#define __PORT_TYPE__
+
+/**
+ * Pointer difference type; replacement for ptrdiff_t.
+ *
+ * This is a signed integral type that is the same size as a pointer.
+ *
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type PORT_PTRDIFF_T;
+#elif     defined(LIN64)
+typedef long PORT_PTRDIFF_T;
+#elif     defined(NT64)
+typedef long long PORT_PTRDIFF_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef int PORT_PTRDIFF_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+/**
+ * Unsigned integral type that can contain a pointer.
+ *
+ * This is an unsigned integral type that is the same size as a pointer.
+ *
+ * NOTE: This type may be different sizes on different platforms.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type PORT_PTRUINT_T;
+#elif     defined(LIN64)
+typedef unsigned long PORT_PTRUINT_T;
+#elif     defined(NT64)
+typedef unsigned long long PORT_PTRUINT_T;
+#elif     defined(NT) || defined(LIN) || defined(WIN32)
+typedef unsigned int PORT_PTRUINT_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+
+/**
+ * 64-bit signed integral type.
+ */
+#if       defined(__ccdoc__)
+typedef platform_dependent_type PORT_INT64_T;
+#elif     defined(LIN64)
+typedef long PORT_INT64_T;
+#elif     defined(NT64) || defined(LIN)
+typedef long long PORT_INT64_T;
+#elif     defined(WIN32) || defined(NT)
+typedef signed __int64 PORT_INT64_T;
+#else
+   #error unknown platform
+#endif /* defined(PLATFORM) */
+
+#endif
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 082b35d4..7e6cd454 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -56,6 +56,7 @@ p->timeWin += clock() - clk;
     // compute the divisors of the window
 clk = clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+    p->nTotalDivs += Vec_PtrSize(p->vDivs);
 p->timeDiv += clock() - clk;
     // construct AIG for the window
 clk = clock();
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
index 7b156b97..da6979d1 100644
--- a/src/opt/mfs/mfsDiv.c
+++ b/src/opt/mfs/mfsDiv.c
@@ -253,7 +253,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
             if ( !Abc_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level >= nLevDivMax )
+            if ( (int)pFanout->Level > nLevDivMax )
                 continue;
             // skip nodes whose fanins are not divisors
             Abc_ObjForEachFanin( pFanout, pFanin, m )
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index e51e0bba..3c0349bb 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -83,6 +83,7 @@ struct Mfs_Man_t_
     int                 nMintsCare;
     int                 nMintsTotal;
     int                 nNodesBad;
+    int                 nTotalDivs;
     // node/edge stats
     int                 nTotalNodesBeg;
     int                 nTotalNodesEnd;
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 768e5295..421f62af 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -115,8 +115,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
             p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
             100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
         printf( "\n" );
-        printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+        printf( "Nodes = %d. Tried = %d. Resub = %d. Divs = %d. SAT calls = %d.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls );
         if ( p->pPars->fSwapEdge )
             printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
                 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index cc75b90f..f6c8a801 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -109,7 +109,7 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
             if ( !Abc_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level >= p->nLevDivMax )
+            if ( (int)pFanout->Level > p->nLevDivMax )
                 continue;
             // skip nodes whose fanins are not divisors
             Abc_ObjForEachFanin( pFanout, pFanin, m )