Version abc80327

35 files changed, 1721 insertions, 354 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 8901e8bb..8a61a530 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -103,6 +103,7 @@ struct Aig_Box_t_
 struct Aig_Man_t_
 {
     char *           pName;          // the design name
+    char *           pSpec;          // the input file name
     // AIG nodes
     Vec_Ptr_t *      vPis;           // the array of PIs
     Vec_Ptr_t *      vPos;           // the array of POs
@@ -328,7 +329,6 @@ static inline int          Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert(
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
 static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;             } 
-static inline Aig_Obj_t *  Aig_ObjHaig( Aig_Obj_t * pObj )        { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } 
 static inline int          Aig_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)pObj->pNext;                                                    }
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
@@ -540,6 +540,7 @@ 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 );
 extern Aig_Man_t *     Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
+extern Aig_Man_t *     Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, 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 );
@@ -612,6 +613,7 @@ extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManSetPioNumbers( Aig_Man_t * p );
 extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
+extern int             Aig_ManCountChoices( Aig_Man_t * p );
 
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 062173e6..665401c3 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -96,6 +96,7 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     {
         pObjNew = Aig_ObjCreatePi( pNew );
         pObjNew->Level = pObj->Level;
+        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     return pNew;
@@ -114,20 +115,16 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
 ***********************************************************************/
 Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
+    Aig_Obj_t * pObjNew;
     if ( pObj->pData )
         return pObj->pData;
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
         return pObj->pData = Aig_ObjChild0Copy(pObj);
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    if ( pNew->pManHaig == NULL )
-        return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    else
-    {
-        Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
-        return pObj->pData = pObjNew;
-    }
+    pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+    return pObj->pData = pObjNew;
 }
 
 /**Function*************************************************************
@@ -156,8 +153,6 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
     Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     // duplicate internal nodes
     if ( fOrdered )
     {
@@ -165,61 +160,42 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
         {
             if ( Aig_ObjIsBuf(pObj) )
             {
-                if ( pNew->pManHaig == NULL )
-                    pObj->pData = Aig_ObjChild0Copy(pObj);
-                else
-                {
-                    Aig_Obj_t * pObjNew = Aig_ObjChild0Copy(pObj);
-                    Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
-                    pObj->pData = pObjNew;
-                }
+                pObjNew = Aig_ObjChild0Copy(pObj);
             }
             else if ( Aig_ObjIsNode(pObj) )
             {
-                if ( pNew->pManHaig == NULL )
-                    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-                else
-                {
-                    Aig_Obj_t * pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-                    Aig_Regular(pObjNew->pHaig)->pHaig = Aig_Regular(pObj->pHaig);
-                    pObj->pData = pObjNew;
-                }
+                pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
             }
             else if ( Aig_ObjIsPi(pObj) )
             {
                 pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->pHaig = pObj->pHaig;
                 pObjNew->Level = pObj->Level;
-                pObj->pData = pObjNew;
             }
             else if ( Aig_ObjIsPo(pObj) )
             {
                 pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-                pObjNew->pHaig = pObj->pHaig;
-                pObj->pData = pObjNew;
+            }
+            else if ( Aig_ObjIsConst1(pObj) )
+            {
+                pObjNew = Aig_ManConst1(pNew);
             }
             else
                 assert( 0 );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
         }
     }
     else
     {
-/*
-        Aig_ManForEachPi( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePi( pNew );
-            pObjNew->pHaig = pObj->pHaig;
-            pObjNew->Level = pObj->Level;
-            pObj->pData = pObjNew;
-        }
-*/
+        Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
         Aig_ManForEachObj( p, pObj, i )
         {
             if ( Aig_ObjIsPi(pObj) )
             {
                 pObjNew = Aig_ObjCreatePi( pNew );
-                pObjNew->pHaig = pObj->pHaig;
                 pObjNew->Level = pObj->Level;
+                Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
                 pObj->pData = pObjNew;
             }
             else if ( Aig_ObjIsPo(pObj) )
@@ -227,18 +203,10 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
                 Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //                assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
                 pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-                pObjNew->pHaig = pObj->pHaig;
+                Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
                 pObj->pData = pObjNew;
             }
         }
-/*
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            pObjNew->pHaig = pObj->pHaig;
-            pObj->pData = pObjNew;
-        }
-*/
     }
     // add the POs
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
@@ -372,6 +340,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vOnehots ) Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
     FREE( p->pSeqModel );
     FREE( p->pName );
+    FREE( p->pSpec );
     FREE( p->pObjCopies );
     FREE( p->pReprs );
     FREE( p->pEquivs );
@@ -410,6 +379,27 @@ int Aig_ManCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs one iteration of AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigCounter( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int Counter, i;
+    Counter = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Counter += (pObj->pHaig != NULL);
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -421,8 +411,12 @@ int Aig_ManCleanup( Aig_Man_t * p )
 ***********************************************************************/
 void Aig_ManPrintStats( Aig_Man_t * p )
 {
+    int nChoices = Aig_ManCountChoices(p);
     printf( "PI/PO/Lat = %5d/%5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
-    printf( "A = %7d. ",    Aig_ManAndNum(p) );
+    printf( "A = %7d. ",   Aig_ManAndNum(p) );
+    printf( "Eq = %7d. ",  Aig_ManHaigCounter(p) );
+    if ( nChoices )
+        printf( "Ch = %5d. ",  nChoices );
     if ( Aig_ManExorNum(p) )
         printf( "X = %5d. ",    Aig_ManExorNum(p) );
     if ( Aig_ManBufNum(p) )
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 80838e19..734f1277 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -97,12 +97,14 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Aig_ObjType(pObj)]++;
     assert( pObj->pData == NULL );
+/*
     if ( p->pManHaig )
     {
         pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
         pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
         pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
     }
+*/
     return pObj;
 }
 
@@ -360,6 +362,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
 void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel )
 {
     Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
+    Aig_Obj_t * pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
     // the object to be replaced cannot be complemented
     assert( !Aig_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
@@ -422,6 +425,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
         Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
     }
+    pObjOld->pHaig = pHaig;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 1fb93eb7..2a9800cf 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "tim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -1346,6 +1347,235 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
 }
 
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Set the representative.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
+{
+    assert( p->pReprs != NULL );
+    assert( !Aig_IsComplement(pNode1) );
+    assert( !Aig_IsComplement(pNode2) );
+    assert( pNode1->Id < p->nReprsAlloc );
+    assert( pNode2->Id < p->nReprsAlloc );
+    if ( pNode1 == pNode2 )
+        return;
+    if ( pNode1->Id < pNode2->Id )
+        p->pReprs[pNode2->Id] = pNode1;
+    else
+        p->pReprs[pNode1->Id] = pNode2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructively accumulates choices.]
+
+  Description [pNew is a new AIG with choices under construction.
+  pPrev is the AIG preceding pThis in the order of deriving choices.
+  pThis is the current AIG to be added to pNew while creating choices.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_t * pThis )
+{
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pPrev) );
+    assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pThis) );
+    assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pPrev) );
+    assert( Aig_ManPoNum(pNew) == Aig_ManPoNum(pThis) );
+    // make sure the nodes of pPrev point to pNew
+    Aig_ManForEachObj( pNew, pObj, i )
+        pObj->fMarkB = 1;
+    Aig_ManForEachObj( pPrev, pObj, i )
+        assert( Aig_Regular(pObj->pData)->fMarkB );
+    Aig_ManForEachObj( pNew, pObj, i )
+        pObj->fMarkB = 0;
+    // make sure the nodes of pThis point to pPrev
+    Aig_ManForEachObj( pPrev, pObj, i )
+        pObj->fMarkB = 1;
+    Aig_ManForEachObj( pThis, pObj, i )
+        assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) );
+    Aig_ManForEachObj( pPrev, pObj, i )
+        pObj->fMarkB = 0;
+    // remap nodes of pThis on top of pNew using pPrev
+    pObj = Aig_ManConst1(pThis);
+    pObj->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( pThis, pObj, i )
+        pObj->pData = Aig_ManPi(pNew, i);
+    Aig_ManForEachPo( pThis, pObj, i )
+        pObj->pData = Aig_ManPo(pNew, i);
+    // go through the nodes in the topological order
+    Aig_ManForEachNode( pThis, pObj, i )
+    {
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        if ( pObj->pHaig == NULL )
+            continue;
+        // pObj->pData and pObj->pHaig->pData are equivalent
+        Aig_ObjSetRepr( pNew, Aig_Regular(pObj->pData), Aig_Regular(pObj->pHaig->pData) );
+    }
+    // set the inputs of POs as equivalent
+    Aig_ManForEachPo( pThis, pObj, i )
+    {
+        pObjNew = Aig_ObjFanin0( Aig_ManPo(pNew,i) );
+        // pObjNew and Aig_ObjFanin0(pObj)->pData are equivalent
+        Aig_ObjSetRepr( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Aig_ObjIsTravIdCurrent( pNew, pObj ) )
+        return;
+    Aig_ObjSetTravIdCurrent( pNew, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        if ( pNew->pManTime )
+        {
+            iBox = Tim_ManBoxForCi( pNew->pManTime, Aig_ObjPioNum(pObj) );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pNew->pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pNew->pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Aig_ManPo(pNew, iTerm1 + i);
+                    Aig_ManChoiceLevel_rec( pNew, pNext );
+                    if ( LevelMax < Aig_ObjLevel(pNext) )
+                        LevelMax = Aig_ObjLevel(pNext);
+                }
+                LevelMax++;
+            }
+        }
+    }
+    else if ( Aig_ObjIsPo(pObj) )
+    {
+        pNext = Aig_ObjFanin0(pObj);
+        Aig_ManChoiceLevel_rec( pNew, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+    }
+    else if ( Aig_ObjIsNode(pObj) )
+    { 
+        // get the maximum level of the two fanins
+        pNext = Aig_ObjFanin0(pObj);
+        Aig_ManChoiceLevel_rec( pNew, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+        pNext = Aig_ObjFanin1(pObj);
+        Aig_ManChoiceLevel_rec( pNew, pNext );
+        if ( LevelMax < Aig_ObjLevel(pNext) )
+            LevelMax = Aig_ObjLevel(pNext);
+        LevelMax++;
+
+        // get the level of the nodes in the choice node
+        if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->iData]) )
+        {
+            Aig_ManChoiceLevel_rec( pNew, pNext );
+            if ( LevelMax < Aig_ObjLevel(pNext) )
+                LevelMax = Aig_ObjLevel(pNext);
+        }
+    }
+    else
+        assert( 0 );
+    Aig_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManChoiceLevel( Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Aig_ManForEachObj( pNew, pObj, i )
+        Aig_ObjSetLevel( pObj, 0 );
+    Aig_ManSetPioNumbers( pNew );
+    Aig_ManIncrementTravId( pNew );
+    Aig_ManForEachPo( pNew, pObj, i )
+    {
+        Aig_ManChoiceLevel_rec( pNew, pObj );
+        if ( LevelMax < Aig_ObjLevel(pObj) )
+            LevelMax = Aig_ObjLevel(pObj);
+    }
+    Aig_ManCleanPioNumbers( pNew );
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructively accumulates choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
+{
+    Aig_Man_t * pNew, * pThis, * pPrev;
+    int i;
+    // start AIG with choices
+    pPrev = Vec_PtrEntry( vAigs, 0 );
+    pNew = Aig_ManDup( pPrev, 1 );
+    // create room for equivalent nodes and representatives
+    assert( pNew->pReprs == NULL );
+    pNew->nReprsAlloc = Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pNew);
+    pNew->pReprs = ALLOC( Aig_Obj_t *, pNew->nReprsAlloc );
+    memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * pNew->nReprsAlloc );
+    // add other AIGs one by one
+    Vec_PtrForEachEntryStart( vAigs, pThis, i, 1 )
+    {
+        Aig_ManChoiceConstructiveOne( pNew, pPrev, pThis );
+        pPrev = pThis;
+    }
+    // derive the result of choicing
+//Aig_ManPrintStats( pNew );
+    pNew = Aig_ManRehash( pNew );
+//Aig_ManPrintStats( pNew );
+    // create the equivalent nodes lists
+    Aig_ManMarkValidChoices( pNew );
+//Aig_ManPrintStats( pNew );
+    // reset levels
+    Aig_ManChoiceLevel( pNew );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index 8ca4fba1..4318be9d 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -178,6 +178,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
             p->nObjs[AIG_OBJ_BUF]++;
             Aig_ObjConnect( p, pObj, Aig_NotCond(pObjLo, fCompl), NULL );
             // create HAIG if defined
+/*
             if ( p->pManHaig )
             {
                 // create HAIG latch
@@ -188,6 +189,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
                 assert( pObjLo->pHaig->pHaig == NULL );
                 pObjLo->pHaig->pHaig = Aig_Regular(pObj->pHaig);
             }
+*/
             // mark the change
             fChange = 1;
             // check the limit
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 7900da51..dcc0a118 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -890,6 +890,28 @@ void Aig_ManCleanPioNumbers( Aig_Man_t * p )
         pObj->pNext = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the PI/PO numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCountChoices( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    Aig_ManForEachNode( p, pObj, i )
+        Counter += Aig_ObjIsChoice( p, pObj );
+    return Counter;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index b02d3bb5..00a85c26 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -3,7 +3,6 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigDfs.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
-    src/aig/aig/aigHaig.c \
     src/aig/aig/aigInter.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
diff --git a/src/aig/bdc/bdc.h b/src/aig/bdc/bdc.h
index e0c35773..fc476ec6 100644
--- a/src/aig/bdc/bdc.h
+++ b/src/aig/bdc/bdc.h
@@ -37,6 +37,7 @@ extern "C" {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Bdc_Fun_t_ Bdc_Fun_t;
 typedef struct Bdc_Man_t_ Bdc_Man_t;
 typedef struct Bdc_Par_t_ Bdc_Par_t;
 struct Bdc_Par_t_
@@ -47,6 +48,12 @@ struct Bdc_Par_t_
     int           fVeryVerbose;  // enable detailed stats
 };
 
+// working with complemented attributes of objects
+static inline int         Bdc_IsComplement( Bdc_Fun_t * p )      { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01);              }
+static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )           { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01);     }
+static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )               { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)01);     }
+static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )    { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)(c!=0)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -59,6 +66,13 @@ struct Bdc_Par_t_
 extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
 extern void        Bdc_ManFree( Bdc_Man_t * p );
 extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
+extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i );
+extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p );
+extern int         Bdc_ManNodeNum( Bdc_Man_t * p );
+extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p );
+extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p );
+extern void *      Bdc_FuncCopy( Bdc_Fun_t * p );
+extern void        Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index d7811f82..e7675420 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -24,12 +24,32 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Accessing contents of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t *  Bdc_ManFunc( Bdc_Man_t * p, int i )               { return Bdc_FunWithId(p, i); }
+Bdc_Fun_t *  Bdc_ManRoot( Bdc_Man_t * p )                      { return p->pRoot;            }
+int          Bdc_ManNodeNum( Bdc_Man_t * p )                   { return p->nNodes;           }
+Bdc_Fun_t *  Bdc_FuncFanin0( Bdc_Fun_t * p )                   { return p->pFan0;            }
+Bdc_Fun_t *  Bdc_FuncFanin1( Bdc_Fun_t * p )                   { return p->pFan1;            }
+void *       Bdc_FuncCopy( Bdc_Fun_t * p )                     { return p->pCopy;            }
+void         Bdc_FuncSetCopy( Bdc_Fun_t * p, void * pCopy )    { p->pCopy = pCopy;           }
+
+/**Function*************************************************************
+
   Synopsis    [Allocate resynthesis manager.]
 
   Description []
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index afba0e67..ab800269 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -54,7 +54,6 @@ typedef enum {
     BDC_TYPE_OTHER      // 7:  unused
 } Bdc_Type_t;
 
-typedef struct Bdc_Fun_t_ Bdc_Fun_t;
 struct Bdc_Fun_t_
 {
     int              Type;         // Const1, PI, AND, XOR, MUX
@@ -122,12 +121,6 @@ struct Bdc_Man_t_
     int              timeTotal;
 };
 
-// working with complemented attributes of objects
-static inline int         Bdc_IsComplement( Bdc_Fun_t * p )             { return (int)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01);              }
-static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )                  { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01);     }
-static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )                      { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)01);     }
-static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )           { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)(c!=0)); }
-
 static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p )                   { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; }
 static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id )        { assert( Id < p->nNodes ); return p->pNodes + Id; }
 static inline int         Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun )  { return pFun - p->pNodes; }
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index a428f435..d93af02e 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -92,7 +92,7 @@ extern Aig_Man_t *     Dar_ManRewriteDefault( Aig_Man_t * pAig );
 extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
-extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
+extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 01f75e32..03707481 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -164,6 +164,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     // make sure the balanced node is not assigned
 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
     assert( pObjOld->pData == NULL );
+    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
     return pObjOld->pData = pObjNew;
 }
 
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index fad4148c..a4ac9082 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -112,6 +112,26 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     return pAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs one iteration of AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManHaigPrintStats( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int Counter, i;
+    Counter = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Counter += (pObj->pHaig != NULL);
+    printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter );
+}
 
 /**Function*************************************************************
 
@@ -314,42 +334,28 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
 //alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 {
     Vec_Ptr_t * vAigs;
+    Aig_Obj_t * pObj;
+    int i;
+
     vAigs = Vec_PtrAlloc( 3 );
     pAig = Aig_ManDup(pAig, 0);
     Vec_PtrPush( vAigs, pAig );
-    pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
-    Vec_PtrPush( vAigs, pAig );
-    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
-    Vec_PtrPush( vAigs, pAig );
-    return vAigs;
-}
 
-/**Function*************************************************************
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pHaig = pObj;
 
-  Synopsis    [Gives the current ABC network to AIG manager for processing.]
-
-  Description []
-               
-  SideEffects []
+    pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose);
+    Vec_PtrPush( vAigs, pAig );
+//Aig_ManPrintStats( pAig );
 
-  SeeAlso     []
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->pHaig = pObj;
 
-***********************************************************************/
-/*
-Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
-{
-    Vec_Ptr_t * vAigs;
-    Aig_Man_t * pMan;
-    vAigs = Vec_PtrAlloc( 3 );
-    pMan = Ioa_ReadAiger( "i10_1.aig", 1 );
-    Vec_PtrPush( vAigs, pMan );
-    pMan = Ioa_ReadAiger( "i10_2.aig", 1 );
-    Vec_PtrPush( vAigs, pMan );
-    pMan = Ioa_ReadAiger( "i10_3.aig", 1 );
-    Vec_PtrPush( vAigs, pMan );
+    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fVerbose);
+    Vec_PtrPush( vAigs, pAig );
+//Aig_ManPrintStats( pAig );
     return vAigs;
 }
-*/
 
 /**Function*************************************************************
 
@@ -362,7 +368,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
+Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
@@ -374,16 +380,22 @@ clk = clock();
 
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
-    pMan = Vec_PtrPop( vAigs );
-    Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
-    Vec_PtrWriteEntry( vAigs, 0, pMan );
+    if ( !fConstruct )
+    {
+        pMan = Vec_PtrPop( vAigs );
+        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+        Vec_PtrWriteEntry( vAigs, 0, pMan );
+    }
 
 if ( fVerbose )
 {
 PRT( "Synthesis time", clock() - clk );
 }
 clk = clock();
-    pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
+    if ( fConstruct )
+        pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
+    else
+        pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
     Vec_PtrForEachEntry( vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 6390ff70..d7f525a2 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -321,6 +321,8 @@ extern void            Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj );
 extern void            Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj );
 extern int             Hop_TableCountEntries( Hop_Man_t * p );
 extern void            Hop_TableProfile( Hop_Man_t * p );
+/*=== hopTruth.c ========================================================*/
+unsigned *             Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
 /*=== hopUtil.c =========================================================*/
 extern void            Hop_ManIncrementTravId( Hop_Man_t * p );
 extern void            Hop_ManCleanData( Hop_Man_t * p );
diff --git a/src/aig/hop/hopTruth.c b/src/aig/hop/hopTruth.c
new file mode 100644
index 00000000..9a2161b6
--- /dev/null
+++ b/src/aig/hop/hopTruth.c
@@ -0,0 +1,210 @@
+/**CFile****************************************************************
+
+  FileName    [hopTruth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: hopTruth.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "hop.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Hop_ManTruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+
+static inline void Hop_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
+{
+    int w;
+    for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = pIn[w];
+}
+static inline void Hop_ManTruthClear( unsigned * pOut, int nVars )
+{
+    int w;
+    for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = 0;
+}
+static inline void Hop_ManTruthFill( unsigned * pOut, int nVars )
+{
+    int w;
+    for ( w = Hop_ManTruthWordNum(nVars)-1; w >= 0; w-- )
+        pOut[w] = ~(unsigned)0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Construct BDDs and mark AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Hop_ManConvertAigToTruth_rec1( Hop_Obj_t * pObj )
+{
+    int Counter = 0;
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return 0;
+    Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); 
+    Counter += Hop_ManConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Hop_ManConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    int i;
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
+        return pObj->pData;
+    // compute the truth tables of the fanins
+    pTruth0 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
+    pTruth1 = Hop_ManConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
+    // creat the truth table of the node
+    pTruth  = Vec_IntFetch( vTruth, nWords );
+    if ( Hop_ObjIsExor(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] ^ pTruth1[i];
+    else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & pTruth1[i];
+    else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & ~pTruth1[i];
+    else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & pTruth1[i];
+    else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjClearMarkA( pObj );
+    pObj->pData = pTruth;
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the node.]
+
+  Description [Assumes that the structural support is no more than 8 inputs.
+  Uses array vTruth to store temporary truth tables. The returned pointer should 
+  be used immediately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Hop_ManConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
+{
+    static unsigned uTruths[8][8] = { // elementary truth tables
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
+    };
+    Hop_Obj_t * pObj;
+    unsigned * pTruth, * pTruth2;
+    int i, nWords, nNodes;
+    Vec_Ptr_t * vTtElems;
+
+    // if the number of variables is more than 8, allocate truth tables
+    if ( nVars > 8 )
+        vTtElems = Vec_PtrAllocTruthTables( nVars );
+    else
+        vTtElems = NULL;
+
+    // clear the data fields and set marks
+    nNodes = Hop_ManConvertAigToTruth_rec1( pRoot );
+    // prepare memory
+    nWords = Hop_TruthWordNum( nVars );
+    Vec_IntClear( vTruth );
+    Vec_IntGrow( vTruth, nWords * (nNodes+1) );
+    pTruth = Vec_IntFetch( vTruth, nWords );
+    // check the case of a constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+    {
+        assert( nNodes == 0 );
+        if ( Hop_IsComplement(pRoot) )
+            Hop_ManTruthClear( pTruth, nVars );
+        else
+            Hop_ManTruthFill( pTruth, nVars );
+        return pTruth;
+    }
+    // set elementary truth tables at the leaves
+    assert( nVars <= Hop_ManPiNum(p) );
+//    assert( Hop_ManPiNum(p) <= 8 ); 
+    if ( fMsbFirst )
+    {
+        Hop_ManForEachPi( p, pObj, i )
+        {
+            if ( vTtElems )
+                pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
+            else               
+                pObj->pData = (void *)uTruths[nVars-1-i];
+        }
+    }
+    else
+    {
+        Hop_ManForEachPi( p, pObj, i )
+        {
+            if ( vTtElems )
+                pObj->pData = Vec_PtrEntry(vTtElems, i);
+            else               
+                pObj->pData = (void *)uTruths[i];
+        }
+    }
+    // clear the marks and compute the truth table
+    pTruth2 = Hop_ManConvertAigToTruth_rec2( pRoot, vTruth, nWords );
+    // copy the result
+    Hop_ManTruthCopy( pTruth, pTruth2, nVars );
+    if ( vTtElems )
+        Vec_PtrFree( vTtElems );
+    return pTruth;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/hop/hop_.c b/src/aig/hop/hop_.c
index 468413fa..658b8c4e 100644
--- a/src/aig/hop/hop_.c
+++ b/src/aig/hop/hop_.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [ivy_.c]
+  FileName    [hop_.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,11 +14,11 @@
 
   Date        [Ver. 1.0. Started - May 11, 2006.]
 
-  Revision    [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+  Revision    [$Id: hop_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "ivy.h"
+#include "hop.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/aig/hop/module.make b/src/aig/hop/module.make
index b06d91fd..e60ec4e8 100644
--- a/src/aig/hop/module.make
+++ b/src/aig/hop/module.make
@@ -6,4 +6,5 @@ SRC +=    src/aig/hop/hopBalance.c \
     src/aig/hop/hopObj.c \
     src/aig/hop/hopOper.c \
     src/aig/hop/hopTable.c \
+    src/aig/hop/hopTruth.c \
     src/aig/hop/hopUtil.c 
diff --git a/src/aig/ntk/module.make b/src/aig/ntk/module.make
new file mode 100644
index 00000000..b668de2f
--- /dev/null
+++ b/src/aig/ntk/module.make
@@ -0,0 +1,9 @@
+SRC +=    src/aig/ntk/ntkCheck.c \
+    src/aig/ntk/ntkBidec.c \
+    src/aig/ntk/ntkDfs.c \
+    src/aig/ntk/ntkFanio.c \
+    src/aig/ntk/ntkMan.c \
+    src/aig/ntk/ntkMap.c \
+    src/aig/ntk/ntkObj.c \
+    src/aig/ntk/ntkTiming.c \
+    src/aig/ntk/ntkUtil.c
diff --git a/src/aig/ntk/ntk.h b/src/aig/ntk/ntk.h
index 6ddfac81..2fcb6ddc 100644
--- a/src/aig/ntk/ntk.h
+++ b/src/aig/ntk/ntk.h
@@ -30,7 +30,9 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig.h"
+#include "hop.h"
 #include "tim.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -66,7 +68,7 @@ struct Ntk_Man_t_
     int                nObjs[NTK_OBJ_VOID]; // counter of objects of each type
     int                nFanioPlus;     // the number of extra fanins/fanouts alloc by default
     // functionality, timing, memory, etc
-    Aig_Man_t *        pAig;           // the functionality representation
+    Hop_Man_t *        pManHop;        // the functionality representation
     Tim_Man_t *        pManTime;       // the timing manager
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Vec_Ptr_t *        vTemp;          // array used for incremental updates
@@ -77,9 +79,10 @@ struct Ntk_Obj_t_
 {
     Ntk_Man_t *        pMan;           // the manager  
     void *             pCopy;          // temporary pointer
-    void *             pFunc;          // functionality
+    Hop_Obj_t *        pFunc;          // functionality
     // node information
     int                Id;             // unique ID
+    int                PioId;          // number of this node in the PI/PO list
     unsigned           Type     :  3;  // object type
     unsigned           fCompl   :  1;  // complemented attribute
     unsigned           MarkA    :  1;  // temporary mark  
@@ -113,6 +116,10 @@ static inline int         Ntk_ManLatchNum( Ntk_Man_t * p )        { return p->nO
 static inline int         Ntk_ManBoxNum( Ntk_Man_t * p )          { return p->nObjs[NTK_OBJ_BOX];               } 
 static inline int         Ntk_ManObjNumMax( Ntk_Man_t * p )       { return Vec_PtrSize(p->vObjs);               }
 
+static inline Ntk_Obj_t * Ntk_ManCi( Ntk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCis, i );          } 
+static inline Ntk_Obj_t * Ntk_ManCo( Ntk_Man_t * p, int i )       { return Vec_PtrEntry( p->vCos, i );          } 
+static inline Ntk_Obj_t * Ntk_ManObj( Ntk_Man_t * p, int i )      { return Vec_PtrEntry( p->vObjs, i );         } 
+
 static inline int         Ntk_ObjFaninNum( Ntk_Obj_t * p )        { return p->nFanins;                          } 
 static inline int         Ntk_ObjFanoutNum( Ntk_Obj_t * p )       { return p->nFanouts;                         } 
 
@@ -126,8 +133,8 @@ static inline int         Ntk_ObjIsCo( Ntk_Obj_t * p )            { return p->Ty
 static inline int         Ntk_ObjIsNode( Ntk_Obj_t * p )          { return p->Type == NTK_OBJ_NODE;             } 
 static inline int         Ntk_ObjIsLatch( Ntk_Obj_t * p )         { return p->Type == NTK_OBJ_LATCH;            } 
 static inline int         Ntk_ObjIsBox( Ntk_Obj_t * p )           { return p->Type == NTK_OBJ_BOX;              } 
-static inline int         Ntk_ObjIsPi( Ntk_Obj_t * p )            { return Ntk_ObjFaninNum(p) == 0 || (Ntk_ObjFaninNum(p) == 1 && Ntk_ObjIsLatch(Ntk_ObjFanin0(p)));   } 
-static inline int         Ntk_ObjIsPo( Ntk_Obj_t * p )            { return Ntk_ObjFanoutNum(p)== 0 || (Ntk_ObjFanoutNum(p)== 1 && Ntk_ObjIsLatch(Ntk_ObjFanout0(p)));  } 
+static inline int         Ntk_ObjIsPi( Ntk_Obj_t * p )            { return Ntk_ObjIsCi(p) && Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1; } 
+static inline int         Ntk_ObjIsPo( Ntk_Obj_t * p )            { return Ntk_ObjIsCo(p) && Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1;  }
 
 static inline float       Ntk_ObjArrival( Ntk_Obj_t * pObj )                 { return pObj->tArrival;           }
 static inline float       Ntk_ObjRequired( Ntk_Obj_t * pObj )                { return pObj->tRequired;          }
@@ -181,42 +188,41 @@ static inline int         Ntk_ObjIsTravIdPrevious( Ntk_Obj_t * pObj )        { r
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== ntlDfs.c ==========================================================*/
+/*=== ntkDfs.c ==========================================================*/
+extern int             Ntk_ManLevel( Ntk_Man_t * pNtk );
+extern int             Ntk_ManLevel2( Ntk_Man_t * pNtk );
 extern Vec_Ptr_t *     Ntk_ManDfs( Ntk_Man_t * pNtk );
 extern Vec_Ptr_t *     Ntk_ManDfsReverse( Ntk_Man_t * pNtk );
-/*=== ntlFanio.c ==========================================================*/
+/*=== ntkFanio.c ==========================================================*/
 extern void            Ntk_ObjCollectFanins( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Ntk_ObjCollectFanouts( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void            Ntk_ObjAddFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
 extern void            Ntk_ObjDeleteFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFanin );
 extern void            Ntk_ObjPatchFanin( Ntk_Obj_t * pObj, Ntk_Obj_t * pFaninOld, Ntk_Obj_t * pFaninNew );
 extern void            Ntk_ObjReplace( Ntk_Obj_t * pNodeOld, Ntk_Obj_t * pNodeNew );
-/*=== ntlMan.c ============================================================*/
+/*=== ntkMan.c ============================================================*/
 extern Ntk_Man_t *     Ntk_ManAlloc();
 extern void            Ntk_ManFree( Ntk_Man_t * p );
-extern void            Ntk_ManPrintStats( Ntk_Man_t * p );
-/*=== ntlMap.c ============================================================*/
-extern Ntk_Man_t *     Ntk_MappingIf( Aig_Man_t * p, void * pPars );
-/*=== ntlObj.c ============================================================*/
-extern Ntk_Obj_t *     Ntk_ManCreatePi( Ntk_Man_t * pMan );
-extern Ntk_Obj_t *     Ntk_ManCreatePo( Ntk_Man_t * pMan );
+extern void            Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib );
+/*=== ntkMap.c ============================================================*/
+/*=== ntkObj.c ============================================================*/
+extern Ntk_Obj_t *     Ntk_ManCreateCi( Ntk_Man_t * pMan, int nFanouts );
+extern Ntk_Obj_t *     Ntk_ManCreateCo( Ntk_Man_t * pMan );
 extern Ntk_Obj_t *     Ntk_ManCreateNode( Ntk_Man_t * pMan, int nFanins, int nFanouts );
 extern Ntk_Obj_t *     Ntk_ManCreateBox( Ntk_Man_t * pMan, int nFanins, int nFanouts );
 extern Ntk_Obj_t *     Ntk_ManCreateLatch( Ntk_Man_t * pMan );
 extern void            Ntk_ManDeleteNode( Ntk_Obj_t * pObj );
 extern void            Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj );
-/*=== ntlUtil.c ============================================================*/
+/*=== ntkTiming.c ============================================================*/
+extern float           Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
+extern void            Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib );
+/*=== ntkUtil.c ============================================================*/
 extern void            Ntk_ManIncrementTravId( Ntk_Man_t * pNtk );
 extern int             Ntk_ManGetFaninMax( Ntk_Man_t * pNtk );
 extern int             Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk );
-extern int             Ntk_ManLevel( Ntk_Man_t * pNtk );
 extern int             Ntk_ManPiNum( Ntk_Man_t * pNtk );
 extern int             Ntk_ManPoNum( Ntk_Man_t * pNtk );
-
-/*=== ntlReadBlif.c ==========================================================*/
-extern Ntk_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
-/*=== ntlWriteBlif.c ==========================================================*/
-extern void            Ioa_WriteBlif( Ntk_Man_t * p, char * pFileName );
+extern int             Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntk/ntkBidec.c b/src/aig/ntk/ntkBidec.c
new file mode 100644
index 00000000..43426d13
--- /dev/null
+++ b/src/aig/ntk/ntkBidec.c
@@ -0,0 +1,123 @@
+/**CFile****************************************************************
+
+  FileName    [ntkBidec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Bi-decomposition of local functions.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntkBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+#include "bdc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    int nNodes, i;
+    assert( nVars <= 16 );
+    // derive truth table
+    pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    if ( Hop_IsComplement(pRoot) )
+        for ( i = Aig_TruthWordNum(nVars)-1; i >= 0; i-- )
+            pTruth[i] = ~pTruth[i];
+    // decompose truth table
+    Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+    // convert back into HOP
+    Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
+    for ( i = 0; i < nVars; i++ )
+        Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
+    nNodes = Bdc_ManNodeNum(p);
+    for ( i = nVars + 1; i < nNodes; i++ )
+    {
+        pFunc = Bdc_ManFunc( p, i );
+        Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
+    }
+    return Bdc_FunCopyHop( Bdc_ManRoot(p) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManBidecResyn( Ntk_Man_t * pNtk, int fVerbose )
+{
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    Ntk_Obj_t * pObj;
+    Vec_Int_t * vTruth;
+    int i, nGainTotal = 0, nNodes1, nNodes2;
+    int clk = clock();
+    pPars->nVarsMax = Ntk_ManGetFaninMax( pNtk );
+    pPars->fVerbose = fVerbose;
+    if ( pPars->nVarsMax > 15 )
+    {
+        if ( fVerbose )
+        printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
+        pPars->nVarsMax = 15;
+    }
+    vTruth = Vec_IntAlloc( 0 );
+    p = Bdc_ManAlloc( pPars );
+    Ntk_ManForEachNode( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjFaninNum(pObj) > 15 )
+            continue;
+        nNodes1 = Hop_DagSize(pObj->pFunc);
+        pObj->pFunc = Ntk_NodeIfNodeResyn( p, pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, NULL );
+        nNodes2 = Hop_DagSize(pObj->pFunc);
+        nGainTotal += nNodes1 - nNodes2;
+    }
+    Bdc_ManFree( p );
+    Vec_IntFree( vTruth );
+    if ( fVerbose )
+    {
+    printf( "Total gain in AIG nodes = %d.  ", nGainTotal );
+    PRT( "Total runtime", clock() - clk );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkCheck.c b/src/aig/ntk/ntkCheck.c
new file mode 100644
index 00000000..6bbb67a6
--- /dev/null
+++ b/src/aig/ntk/ntkCheck.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [ntk_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntk/ntkDfs.c b/src/aig/ntk/ntkDfs.c
index ce176898..263a2740 100644
--- a/src/aig/ntk/ntkDfs.c
+++ b/src/aig/ntk/ntkDfs.c
@@ -30,6 +30,62 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Assumes that white boxes have unit level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel( Ntk_Man_t * pNtk )
+{
+    Tim_Man_t * pManTimeUnit;
+    Ntk_Obj_t * pObj, * pFanin;
+    int i, k, LevelMax, Level;
+    // clean the levels
+    Ntk_ManForEachObj( pNtk, pObj, i )
+        Ntk_ObjSetLevel( pObj, 0 );
+    // perform level computation
+    LevelMax = 0;
+    pManTimeUnit = Tim_ManDupUnit( pNtk->pManTime );
+    Tim_ManIncrementTravId( pManTimeUnit );
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjIsCi(pObj) )
+        {
+            Level = (int)Tim_ManGetPiArrival( pManTimeUnit, pObj->PioId );
+            Ntk_ObjSetLevel( pObj, Level );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            Level = Ntk_ObjLevel( Ntk_ObjFanin0(pObj) );
+            Tim_ManSetPoArrival( pManTimeUnit, pObj->PioId, (float)Level );
+            Ntk_ObjSetLevel( pObj, Level );
+            if ( LevelMax < Ntk_ObjLevel(pObj) )
+                LevelMax = Ntk_ObjLevel(pObj);
+        }
+        else if ( Ntk_ObjIsNode(pObj) )
+        {
+            Level = 0;
+            Ntk_ObjForEachFanin( pObj, pFanin, k )
+                if ( Level < Ntk_ObjLevel(pFanin) )
+                    Level = Ntk_ObjLevel(pFanin);
+            Ntk_ObjSetLevel( pObj, Level + 1 );
+        }
+        else
+            assert( 0 );
+    }
+    // set the old timing manager
+    Tim_ManStop( pManTimeUnit );
+    return LevelMax;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Performs DFS for one node.]
 
   Description []
@@ -39,16 +95,96 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDfs_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Ntk_ManLevel2_rec( Ntk_Obj_t * pObj )
+{
+    Ntk_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Ntk_ObjSetTravIdCurrent( pObj );
+    if ( Ntk_ObjIsCi(pObj) )
+    {
+        iBox = Tim_ManBoxForCi( pObj->pMan->pManTime, pObj->PioId );
+        if ( iBox >= 0 ) // this is not a true PI
+        {
+            iTerm1 = Tim_ManBoxInputFirst( pObj->pMan->pManTime, iBox );
+            nTerms = Tim_ManBoxInputNum( pObj->pMan->pManTime, iBox );
+            for ( i = 0; i < nTerms; i++ )
+            {
+                pNext = Ntk_ManCo(pObj->pMan, iTerm1 + i);
+                Ntk_ManLevel2_rec( pNext );
+                if ( LevelMax < Ntk_ObjLevel(pNext) )
+                    LevelMax = Ntk_ObjLevel(pNext);
+            }
+            LevelMax++;
+        }
+    }
+    else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCo(pObj) )
+    {
+        Ntk_ObjForEachFanin( pObj, pNext, i )
+        {
+            Ntk_ManLevel2_rec( pNext );
+            if ( LevelMax < Ntk_ObjLevel(pNext) )
+                LevelMax = Ntk_ObjLevel(pNext);
+        }
+        if ( Ntk_ObjIsNode(pObj) )
+            LevelMax++;
+    }
+    else
+        assert( 0 );
+    Ntk_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_ManLevel2( Ntk_Man_t * pNtk )
+{
+    Ntk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Ntk_ManForEachObj( pNtk, pObj, i )
+        Ntk_ObjSetLevel( pObj, 0 );
+    Ntk_ManIncrementTravId( pNtk );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+    {
+        Ntk_ManLevel2_rec( pObj );
+        if ( LevelMax < Ntk_ObjLevel(pObj) )
+            LevelMax = Ntk_ObjLevel(pObj);
+    }
+    return LevelMax;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManDfs_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     Ntk_Obj_t * pNext;
     int i;
-    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
         return;
-    Ntk_ObjSetTravIdCurrent( pNode );
-    Ntk_ObjForEachFanin( pNode, pNext, i )
+    Ntk_ObjSetTravIdCurrent( pObj );
+    Ntk_ObjForEachFanin( pObj, pNext, i )
         Ntk_ManDfs_rec( pNext, vNodes );
-    Vec_PtrPush( vNodes, pNode );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
@@ -69,8 +205,16 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
     int i;
     Ntk_ManIncrementTravId( pNtk );
     vNodes = Vec_PtrAlloc( 100 );
-    Ntk_ManForEachPo( pNtk, pObj, i )
-        Ntk_ManDfs_rec( pObj, vNodes );
+    Ntk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Ntk_ObjIsCi(pObj) )
+        {
+            Ntk_ObjSetTravIdCurrent( pObj );
+            Vec_PtrPush( vNodes, pObj );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+            Ntk_ManDfs_rec( pObj, vNodes );
+    }
     return vNodes;
 }
 
@@ -85,16 +229,35 @@ Vec_Ptr_t * Ntk_ManDfs( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+void Ntk_ManDfsReverse_rec( Ntk_Obj_t * pObj, Vec_Ptr_t * vNodes )
 {
     Ntk_Obj_t * pNext;
-    int i;
-    if ( Ntk_ObjIsTravIdCurrent( pNode ) )
+    int i, iBox, iTerm1, nTerms;
+    if ( Ntk_ObjIsTravIdCurrent( pObj ) )
         return;
-    Ntk_ObjSetTravIdCurrent( pNode );
-    Ntk_ObjForEachFanout( pNode, pNext, i )
-        Ntk_ManDfsReverse_rec( pNext, vNodes );
-    Vec_PtrPush( vNodes, pNode );
+    Ntk_ObjSetTravIdCurrent( pObj );
+    if ( Ntk_ObjIsCo(pObj) )
+    {
+        iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId );
+        if ( iBox >= 0 ) // this is not a true PO
+        {
+            iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox );
+            nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox );
+            for ( i = 0; i < nTerms; i++ )
+            {
+                pNext = Ntk_ManCi(pObj->pMan, iTerm1 + i);
+                Ntk_ManDfsReverse_rec( pNext, vNodes );
+            }
+        }
+    }
+    else if ( Ntk_ObjIsNode(pObj) || Ntk_ObjIsCi(pObj) )
+    {
+        Ntk_ObjForEachFanout( pObj, pNext, i )
+            Ntk_ManDfsReverse_rec( pNext, vNodes );
+    }
+    else
+        assert( 0 );
+    Vec_PtrPush( vNodes, pObj );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntk/ntkFanio.c b/src/aig/ntk/ntkFanio.c
index 73019231..135929af 100644
--- a/src/aig/ntk/ntkFanio.c
+++ b/src/aig/ntk/ntkFanio.c
@@ -279,7 +279,7 @@ void Ntk_ObjTransferFanout( Ntk_Obj_t * pNodeFrom, Ntk_Obj_t * pNodeTo )
     Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp;
     Ntk_Obj_t * pTemp;
     int nFanoutsOld, i;
-    assert( !Ntk_ObjIsPo(pNodeFrom) && !Ntk_ObjIsPo(pNodeTo) );
+    assert( !Ntk_ObjIsCo(pNodeFrom) && !Ntk_ObjIsCo(pNodeTo) );
     assert( pNodeFrom->pMan == pNodeTo->pMan );
     assert( pNodeFrom != pNodeTo );
     assert( Ntk_ObjFanoutNum(pNodeFrom) > 0 );
diff --git a/src/aig/ntk/ntkMan.c b/src/aig/ntk/ntkMan.c
index e302a98c..1a077495 100644
--- a/src/aig/ntk/ntkMan.c
+++ b/src/aig/ntk/ntkMan.c
@@ -50,6 +50,7 @@ Ntk_Man_t * Ntk_ManAlloc()
     p->vTemp = Vec_PtrAlloc( 1000 );
     p->nFanioPlus = 4;
     p->pMemObjs = Aig_MmFlexStart();
+    p->pManHop = Hop_ManStart();
     return p;
 }
 
@@ -72,9 +73,9 @@ void Ntk_ManFree( Ntk_Man_t * p )
     if ( p->vCos )     Vec_PtrFree( p->vCos );
     if ( p->vObjs )    Vec_PtrFree( p->vObjs );
     if ( p->vTemp )    Vec_PtrFree( p->vTemp );
-    if ( p->pAig )     Aig_ManStop( p->pAig );
     if ( p->pManTime ) Tim_ManStop( p->pManTime );
     if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pManHop )  Hop_ManStop( p->pManHop );
     free( p );
 }
 
@@ -89,7 +90,7 @@ void Ntk_ManFree( Ntk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManPrintStats( Ntk_Man_t * p )
+void Ntk_ManPrintStats( Ntk_Man_t * p, If_Lib_t * pLutLib )
 {
     printf( "%-15s : ",      p->pName );
     printf( "pi = %5d  ",    Ntk_ManPiNum(p) );
@@ -97,10 +98,15 @@ void Ntk_ManPrintStats( Ntk_Man_t * p )
     printf( "ci = %5d  ",    Ntk_ManCiNum(p) );
     printf( "co = %5d  ",    Ntk_ManCoNum(p) );
     printf( "lat = %5d  ",   Ntk_ManLatchNum(p) );
-    printf( "box = %5d  ",   Ntk_ManBoxNum(p) );
+//    printf( "box = %5d  ",   Ntk_ManBoxNum(p) );
     printf( "node = %5d  ",  Ntk_ManNodeNum(p) );
-    printf( "aig = %6d  ",   Aig_ManNodeNum(p->pAig) );
+    printf( "aig = %6d  ",   Ntk_ManGetAigNodeNum(p) );
+    printf( "lev = %3d  ",   Ntk_ManLevel(p) );
+    printf( "lev2 = %3d  ",  Ntk_ManLevel2(p) );
+    printf( "delay = %5.2f", Ntk_ManDelayTraceLut(p, pLutLib) );
     printf( "\n" );
+
+    Ntk_ManDelayTracePrint( p, pLutLib );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntk/ntkMap.c b/src/aig/ntk/ntkMap.c
index 7700fc63..9c780498 100644
--- a/src/aig/ntk/ntkMap.c
+++ b/src/aig/ntk/ntkMap.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntk.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,6 +31,209 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+{
+//    extern void * Abc_FrameReadLibLut();
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+//    pPars->nLutSize    = -1;
+    pPars->nLutSize    =  6;
+    pPars->nCutsMax    =  8;
+    pPars->nFlowIters  =  1;
+    pPars->nAreaIters  =  2;
+    pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.01;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0;
+    pPars->fLatchPaths =  0;
+    pPars->fEdge       =  1;
+    pPars->fCutMin     =  1;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  1;
+    // internal parameters
+    pPars->fTruth      =  0;
+    pPars->nLatches    =  0;
+    pPars->fLiftLeaves =  0;
+//    pPars->pLutLib     =  Abc_FrameReadLibLut();
+    pPars->pLutLib     =  NULL;
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  NULL;   
+/*
+    if ( pPars->nLutSize == -1 )
+    {
+        if ( pPars->pLutLib == NULL )
+        {
+            printf( "The LUT library is not given.\n" );
+            return;
+        }
+        // get LUT size from the library
+        pPars->nLutSize = pPars->pLutLib->LutMax;
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+{
+    If_Man_t * pIfMan;
+    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    int i;
+    // start the mapping manager and set its parameters
+    pIfMan = If_ManStart( pPars );
+    // print warning about excessive memory usage
+//    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
+//        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
+//            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
+    // load the AIG into the mapper
+    Aig_ManForEachObj( p, pNode, i )
+    {
+        if ( Aig_ObjIsAnd(pNode) )
+            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
+                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+        else if ( Aig_ObjIsPi(pNode) )
+        {
+            pNode->pData = If_ManCreateCi( pIfMan );
+            ((If_Obj_t *)pNode->pData)->Level = pNode->Level;
+            if ( pIfMan->nLevelMax < (int)pNode->Level )
+                pIfMan->nLevelMax = (int)pNode->Level;
+        }
+        else if ( Aig_ObjIsPo(pNode) )
+            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+        else if ( Aig_ObjIsConst1(pNode) )
+            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+        else // add the node to the mapper
+            assert( 0 );
+        // set up the choice node
+//        if ( Aig_AigNodeIsChoice( pNode ) )
+//        {
+//            pIfMan->nChoices++;
+//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
+//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
+//        }
+        {
+            If_Obj_t * pIfObj = pNode->pData;
+            assert( !If_IsComplement(pIfObj) );
+            assert( pIfObj->Id == pNode->Id );
+        }
+    }
+    return pIfMan;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pTemp;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutData(pCut) )
+        return If_CutData(pCut);
+    // mark the node as visited
+    Vec_PtrPush( vVisited, pCut );
+    // insert the worst case
+    If_CutSetData( pCut, (void *)1 );
+    // skip in case of primary input
+    if ( If_ObjIsCi(pIfObj) )
+        return If_CutData(pCut);
+    // compute the functions of the children
+    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        gFunc0 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited );
+        if ( gFunc0 == (void *)1 )
+            continue;
+        gFunc1 = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited );
+        if ( gFunc1 == (void *)1 )
+            continue;
+        // both branches are solved
+        gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) ); 
+        if ( pTemp->fPhase != pIfObj->fPhase )
+            gFunc = Hop_Not(gFunc);
+        If_CutSetData( pCut, gFunc );
+        break;
+    }
+    return If_CutData(pCut);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Ntk_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+{
+    If_Cut_t * pCut;
+    Hop_Obj_t * gFunc;
+    If_Obj_t * pLeaf;
+    int i;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    gFunc = Ntk_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    if ( gFunc == (void *)1 )
+    {
+        printf( "Ntk_NodeIfToHop(): Computing local AIG has failed.\n" );
+        return NULL;
+    }
+//    printf( "%d ", Vec_PtrSize(p->vTemp) );
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutBest(pLeaf), NULL );
+    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
+        If_CutSetData( pCut, NULL );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,6 +243,95 @@
   SeeAlso     []
 
 ***********************************************************************/
+Ntk_Man_t * Ntk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p )
+{
+    Ntk_Man_t * pNtk;
+    Ntk_Obj_t * pObjNew;
+    Aig_Obj_t * pObj;
+    If_Obj_t * pIfObj;
+    If_Cut_t * pCutBest;
+    int i, k, nLeaves, * ppLeaves;
+    assert( Aig_ManPiNum(p) == If_ManCiNum(pIfMan) );
+    assert( Aig_ManPoNum(p) == If_ManCoNum(pIfMan) );
+    assert( Aig_ManNodeNum(p) == If_ManAndNum(pIfMan) );
+    If_ManCleanCutData( pIfMan );
+    // construct the network
+    pNtk = Ntk_ManAlloc();
+    pNtk->pName = Aig_UtilStrsav( p->pName );
+    pNtk->pSpec = Aig_UtilStrsav( p->pSpec );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pIfObj = If_ManObj( pIfMan, i );
+        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
+            continue;
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            pCutBest = If_ObjCutBest( pIfObj );
+            nLeaves  = If_CutLeaveNum( pCutBest ); 
+            ppLeaves = If_CutLeaves( pCutBest );
+            // create node
+            pObjNew = Ntk_ManCreateNode( pNtk, nLeaves, pIfObj->nRefs );
+            for ( k = 0; k < nLeaves; k++ )
+                Ntk_ObjAddFanin( pObjNew, Aig_ManObj(p, ppLeaves[k])->pData );
+            // get the functionality
+            pObjNew->pFunc = Ntk_NodeIfToHop( pNtk->pManHop, pIfMan, pIfObj );
+        }
+        else if ( Aig_ObjIsPi(pObj) )
+            pObjNew = Ntk_ManCreateCi( pNtk, pIfObj->nRefs );
+        else if ( Aig_ObjIsPo(pObj) )
+        {
+            pObjNew = Ntk_ManCreateCo( pNtk );
+            pObjNew->fCompl = Aig_ObjFaninC0(pObj);
+            Ntk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+        {
+            pObjNew = Ntk_ManCreateNode( pNtk, 0, pIfObj->nRefs );
+            pObjNew->pFunc = Hop_ManConst1( pNtk->pManHop );
+        }
+        else
+            assert( 0 );
+        pObj->pData = pObjNew;
+    }
+    pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntk_Man_t * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars )
+{
+    Ntk_Man_t * pNtk;
+    If_Man_t * pIfMan;
+    // perform FPGA mapping
+    // set the arrival times
+    pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
+    memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
+    // translate into the mapper
+    pIfMan = Ntk_ManToIf( p, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+    // transform the result of mapping into the new network
+    pNtk = Ntk_ManFromIf( pIfMan, p );
+    If_ManStop( pIfMan );
+    return pNtk;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntk/ntkObj.c b/src/aig/ntk/ntkObj.c
index 259ed79d..7bd2f552 100644
--- a/src/aig/ntk/ntkObj.c
+++ b/src/aig/ntk/ntkObj.c
@@ -63,10 +63,11 @@ Ntk_Obj_t * Ntk_ManCreateObj( Ntk_Man_t * p, int nFanins, int nFanouts )
   SeeAlso     []
 
 ***********************************************************************/
-Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
+Ntk_Obj_t * Ntk_ManCreateCi( Ntk_Man_t * p, int nFanouts )
 {
     Ntk_Obj_t * pObj;
-    pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj = Ntk_ManCreateObj( p, 1, nFanouts );
+    pObj->PioId = Vec_PtrSize( p->vCis );
     Vec_PtrPush( p->vCis, pObj );
     pObj->Type = NTK_OBJ_CI;
     p->nObjs[NTK_OBJ_CI]++;
@@ -84,10 +85,11 @@ Ntk_Obj_t * Ntk_ManCreatePi( Ntk_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ntk_Obj_t * Ntk_ManCreatePo( Ntk_Man_t * p )
+Ntk_Obj_t * Ntk_ManCreateCo( Ntk_Man_t * p )
 {
     Ntk_Obj_t * pObj;
     pObj = Ntk_ManCreateObj( p, 1, 1 );
+    pObj->PioId = Vec_PtrSize( p->vCos );
     Vec_PtrPush( p->vCos, pObj );
     pObj->Type = NTK_OBJ_CO;
     p->nObjs[NTK_OBJ_CO]++;
@@ -200,7 +202,7 @@ void Ntk_ManDeleteNode_rec( Ntk_Obj_t * pObj )
 {
     Vec_Ptr_t * vNodes;
     int i;
-    assert( !Ntk_ObjIsPi(pObj) );
+    assert( !Ntk_ObjIsCi(pObj) );
     assert( Ntk_ObjFanoutNum(pObj) == 0 );
     vNodes = Vec_PtrAlloc( 100 );
     Ntk_ObjCollectFanins( pObj, vNodes );
diff --git a/src/aig/ntk/ntkTiming.c b/src/aig/ntk/ntkTiming.c
index f57c7987..ff867e02 100644
--- a/src/aig/ntk/ntkTiming.c
+++ b/src/aig/ntk/ntkTiming.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "ntk.h"
-#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -108,19 +107,17 @@ void Ntk_ManDelayTraceSortPins( Ntk_Obj_t * pNode, int * pPinPerm, float * pPinD
   SeeAlso     []
 
 ***********************************************************************/
-float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
+float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, If_Lib_t * pLutLib )
 {
     int fUseSorting = 1;
     int pPinPerm[32];
     float pPinDelays[32];
-    If_Lib_t * pLutLib;
-    Ntk_Obj_t * pNode, * pFanin;
+    Ntk_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vNodes;
     float tArrival, tRequired, tSlack, * pDelays;
     int i, k;
 
     // get the library
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
     if ( pLutLib && pLutLib->LutMax < Ntk_ManGetFaninMax(pNtk) )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
@@ -128,107 +125,138 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
         return -AIG_INFINITY;
     }
 
+    // compute the reverse order of all objects
+    vNodes = Ntk_ManDfsReverse( pNtk );
+
     // initialize the arrival times
     Abc_NtkPrepareTiming( pNtk );
 
     // propagate arrival times
-    vNodes = Ntk_ManDfs( pNtk );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Tim_ManIncrementTravId( pNtk->pManTime );
+    Ntk_ManForEachObj( pNtk, pObj, i )
     {
-        tArrival = -AIG_INFINITY;
-        if ( pLutLib == NULL )
-        {
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 )
-                    tArrival = Ntk_ObjArrival(pFanin) + 1.0;
-        }
-        else if ( !pLutLib->fVarPinDelays )
+        if ( Ntk_ObjIsNode(pObj) )
         {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] )
-                    tArrival = Ntk_ObjArrival(pFanin) + pDelays[0];
-        }
-        else
-        {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            if ( fUseSorting )
+            tArrival = -AIG_INFINITY;
+            if ( pLutLib == NULL )
             {
-                Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-                Ntk_ObjForEachFanin( pNode, pFanin, k ) 
-                    if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] )
-                        tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + 1.0 )
+                        tArrival = Ntk_ObjArrival(pFanin) + 1.0;
+            }
+            else if ( !pLutLib->fVarPinDelays )
+            {
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[0] )
+                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[0];
             }
             else
             {
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                    if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
-                        tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                if ( fUseSorting )
+                {
+                    Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays );
+                    Ntk_ObjForEachFanin( pObj, pFanin, k ) 
+                        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k] )
+                            tArrival = Ntk_ObjArrival(Ntk_ObjFanin(pObj,pPinPerm[k])) + pDelays[k];
+                }
+                else
+                {
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                        if ( tArrival < Ntk_ObjArrival(pFanin) + pDelays[k] )
+                            tArrival = Ntk_ObjArrival(pFanin) + pDelays[k];
+                }
             }
+            if ( Ntk_ObjFaninNum(pObj) == 0 )
+                tArrival = 0.0;
         }
-        if ( Ntk_ObjFaninNum(pNode) == 0 )
-            tArrival = 0.0;
-        Ntk_ObjSetArrival( pNode, tArrival );
+        else if ( Ntk_ObjIsCi(pObj) )
+        {
+            tArrival = Tim_ManGetPiArrival( pNtk->pManTime, pObj->PioId );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            tArrival = Ntk_ObjArrival( Ntk_ObjFanin0(pObj) );
+            Tim_ManSetPoArrival( pNtk->pManTime, pObj->PioId, tArrival );
+        }
+        else
+            assert( 0 );
+        Ntk_ObjSetArrival( pObj, tArrival );
     }
-    Vec_PtrFree( vNodes );
 
     // get the latest arrival times
     tArrival = -AIG_INFINITY;
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pNode)) )
-            tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pNode));
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        if ( tArrival < Ntk_ObjArrival(Ntk_ObjFanin0(pObj)) )
+            tArrival = Ntk_ObjArrival(Ntk_ObjFanin0(pObj));
 
     // initialize the required times
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pNode)) > tArrival )
-            Ntk_ObjSetRequired( Ntk_ObjFanin0(pNode), tArrival );
+    Ntk_ManForEachPo( pNtk, pObj, i )
+        if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tArrival )
+            Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tArrival );
 
     // propagate the required times
-    vNodes = Ntk_ManDfsReverse( pNtk );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
+    Tim_ManIncrementTravId( pNtk->pManTime );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
     {
-        if ( pLutLib == NULL )
-        {
-            tRequired = Ntk_ObjRequired(pNode) - (float)1.0;
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( Ntk_ObjRequired(pFanin) > tRequired )
-                    Ntk_ObjSetRequired( pFanin, tRequired );
-        }
-        else if ( !pLutLib->fVarPinDelays )
-        {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            tRequired = Ntk_ObjRequired(pNode) - pDelays[0];
-            Ntk_ObjForEachFanin( pNode, pFanin, k )
-                if ( Ntk_ObjRequired(pFanin) > tRequired )
-                    Ntk_ObjSetRequired( pFanin, tRequired );
-        }
-        else 
+        if ( Ntk_ObjIsNode(pObj) )
         {
-            pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-            if ( fUseSorting )
+            if ( pLutLib == NULL )
             {
-                Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                {
-                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
-                    if ( Ntk_ObjRequired(Ntk_ObjFanin(pNode,pPinPerm[k])) > tRequired )
-                        Ntk_ObjSetRequired( Ntk_ObjFanin(pNode,pPinPerm[k]), tRequired );
-                }
+                tRequired = Ntk_ObjRequired(pObj) - (float)1.0;
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    if ( Ntk_ObjRequired(pFanin) > tRequired )
+                        Ntk_ObjSetRequired( pFanin, tRequired );
             }
-            else
+            else if ( !pLutLib->fVarPinDelays )
             {
-                Ntk_ObjForEachFanin( pNode, pFanin, k )
-                {
-                    tRequired = Ntk_ObjRequired(pNode) - pDelays[k];
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                tRequired = Ntk_ObjRequired(pObj) - pDelays[0];
+                Ntk_ObjForEachFanin( pObj, pFanin, k )
                     if ( Ntk_ObjRequired(pFanin) > tRequired )
                         Ntk_ObjSetRequired( pFanin, tRequired );
+            }
+            else 
+            {
+                pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pObj)];
+                if ( fUseSorting )
+                {
+                    Ntk_ManDelayTraceSortPins( pObj, pPinPerm, pPinDelays );
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    {
+                        tRequired = Ntk_ObjRequired(pObj) - pDelays[k];
+                        if ( Ntk_ObjRequired(Ntk_ObjFanin(pObj,pPinPerm[k])) > tRequired )
+                            Ntk_ObjSetRequired( Ntk_ObjFanin(pObj,pPinPerm[k]), tRequired );
+                    }
+                }
+                else
+                {
+                    Ntk_ObjForEachFanin( pObj, pFanin, k )
+                    {
+                        tRequired = Ntk_ObjRequired(pObj) - pDelays[k];
+                        if ( Ntk_ObjRequired(pFanin) > tRequired )
+                            Ntk_ObjSetRequired( pFanin, tRequired );
+                    }
                 }
             }
         }
+        else if ( Ntk_ObjIsCi(pObj) )
+        {
+            tRequired = Ntk_ObjRequired(pObj);
+            Tim_ManSetPiRequired( pNtk->pManTime, pObj->PioId, tRequired );
+        }
+        else if ( Ntk_ObjIsCo(pObj) )
+        {
+            tRequired = Tim_ManGetPoRequired( pNtk->pManTime, pObj->PioId );
+            if ( Ntk_ObjRequired(Ntk_ObjFanin0(pObj)) > tRequired )
+                Ntk_ObjSetRequired( Ntk_ObjFanin0(pObj), tRequired );
+        }
+
         // set slack for this object
-        tSlack = Ntk_ObjRequired(pNode) - Ntk_ObjArrival(pNode);
+        tSlack = Ntk_ObjRequired(pObj) - Ntk_ObjArrival(pObj);
         assert( tSlack + 0.001 > 0.0 );
-        Ntk_ObjSetSlack( pNode, tSlack < 0.0 ? 0.0 : tSlack );
+        Ntk_ObjSetSlack( pObj, tSlack < 0.0 ? 0.0 : tSlack );
     }
     Vec_PtrFree( vNodes );
     return tArrival;
@@ -236,52 +264,6 @@ float Ntk_ManDelayTraceLut( Ntk_Man_t * pNtk, int fUseLutLib )
 
 /**Function*************************************************************
 
-  Synopsis    [Determines timing-critical edges of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tDelta, int fUseLutLib )
-{
-    int pPinPerm[32];
-    float pPinDelays[32];
-    If_Lib_t * pLutLib;
-    Ntk_Obj_t * pFanin;
-    unsigned uResult = 0;
-    float tRequired, * pDelays;
-    int k;
-    pLutLib = fUseLutLib?  Abc_FrameReadLibLut() : NULL;
-    tRequired = Ntk_ObjRequired(pNode);
-    if ( pLutLib == NULL )
-    {
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(pFanin) + 1.0 + tDelta )
-                uResult |= (1 << k);
-    }
-    else if ( !pLutLib->fVarPinDelays )
-    {
-        pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(pFanin) + pDelays[0] + tDelta )
-                uResult |= (1 << k);
-    }
-    else
-    {
-        pDelays = pLutLib->pLutDelays[Ntk_ObjFaninNum(pNode)];
-        Ntk_ManDelayTraceSortPins( pNode, pPinPerm, pPinDelays );
-        Ntk_ObjForEachFanin( pNode, pFanin, k )
-            if ( tRequired < Ntk_ObjArrival(Ntk_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] + tDelta )
-                uResult |= (1 << pPinPerm[k]);
-    }
-    return uResult;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Delay tracing of the LUT mapped network.]
 
   Description []
@@ -291,14 +273,12 @@ unsigned Ntk_ManDelayTraceTCEdges( Ntk_Man_t * pNtk, Ntk_Obj_t * pNode, float tD
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
+void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, If_Lib_t * pLutLib )
 {
     Ntk_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 < Ntk_ManGetFaninMax(pNtk) )
     {
         printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", 
@@ -306,11 +286,11 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
         return;
     }
     // decide how many steps
-    nSteps = fUseLutLib ? 20 : Ntk_ManLevel(pNtk);
+    nSteps = pLutLib ? 20 : Ntk_ManLevel(pNtk);
     pCounters = ALLOC( int, nSteps + 1 );
     memset( pCounters, 0, sizeof(int)*(nSteps + 1) );
     // perform delay trace
-    tArrival = Ntk_ManDelayTraceLut( pNtk, fUseLutLib );
+    tArrival = Ntk_ManDelayTraceLut( pNtk, pLutLib );
     tDelta = tArrival / nSteps;
     // count how many nodes have slack in the corresponding intervals
     Ntk_ManForEachNode( pNtk, pNode, i )
@@ -318,17 +298,19 @@ void Ntk_ManDelayTracePrint( Ntk_Man_t * pNtk, int fUseLutLib, int fVerbose )
         if ( Ntk_ObjFaninNum(pNode) == 0 )
             continue;
         Num = Ntk_ObjSlack(pNode) / tDelta;
+        if ( Num > nSteps )
+            continue;
         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" );
+    printf( "Max delay = %6.2f. Delay trace using %s model:\n", tArrival, pLutLib? "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/Ntk_ManNodeNum(pNtk) );
+        printf( "%3d %s : %5d  (%6.2f %%)\n", pLutLib? 5*(i+1) : i+1, 
+            pLutLib? "%":"lev", Nodes, 100.0*Nodes/Ntk_ManNodeNum(pNtk) );
     }
     free( pCounters );
 }
diff --git a/src/aig/ntk/ntkUtil.c b/src/aig/ntk/ntkUtil.c
index 543d1a60..931a26ee 100644
--- a/src/aig/ntk/ntkUtil.c
+++ b/src/aig/ntk/ntkUtil.c
@@ -95,36 +95,25 @@ int Ntk_ManGetTotalFanins( Ntk_Man_t * pNtk )
     return nFanins;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+  Synopsis    []
 
-  Description [Assumes topological ordering of the nodes.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManLevel( Ntk_Man_t * pNtk )
+int Ntk_ManPiNum( Ntk_Man_t * pNtk )
 {
-    Ntk_Obj_t * pObj, * pFanin;
-    int i, k, LevelMax;
-    Ntk_ManForEachPi( pNtk, pObj, i )
-        Ntk_ObjSetLevel( pObj, 0 );
-    Ntk_ManForEachNode( pNtk, pObj, i )
-    {
-        LevelMax = 0;
-        Ntk_ObjForEachFanin( pObj, pFanin, k )
-            if ( LevelMax < Ntk_ObjLevel(pFanin) )
-                LevelMax = Ntk_ObjLevel(pFanin);
-        Ntk_ObjSetLevel( pFanin, LevelMax+1 );
-    }
-    LevelMax = 0;
-    Ntk_ManForEachPo( pNtk, pObj, i )
-        if ( LevelMax < Ntk_ObjLevel(pObj) )
-            LevelMax = Ntk_ObjLevel(pObj);
-    return LevelMax;
+    Ntk_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntk_ManForEachCi( pNtk, pNode, i )
+        Counter += Ntk_ObjIsPi( pNode );
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -138,18 +127,18 @@ int Ntk_ManLevel( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManPiNum( Ntk_Man_t * pNtk )
+int Ntk_ManPoNum( Ntk_Man_t * pNtk )
 {
     Ntk_Obj_t * pNode;
     int i, Counter = 0;
-    Ntk_ManForEachPi( pNtk, pNode, i )
-        Counter++;
+    Ntk_ManForEachCo( pNtk, pNode, i )
+        Counter += Ntk_ObjIsPo( pNode );
     return Counter;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Reads the number of BDD nodes.]
 
   Description []
                
@@ -158,13 +147,22 @@ int Ntk_ManPiNum( Ntk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_ManPoNum( Ntk_Man_t * pNtk )
+int Ntk_ManGetAigNodeNum( Ntk_Man_t * pNtk )
 {
     Ntk_Obj_t * pNode;
-    int i, Counter = 0;
-    Ntk_ManForEachPo( pNtk, pNode, i )
-        Counter++;
-    return Counter;
+    int i, nNodes = 0;
+    Ntk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( pNode->pFunc == NULL )
+        {
+            printf( "Ntk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
+            continue;
+        }
+        if ( Ntk_ObjFaninNum(pNode) < 2 )
+            continue;
+        nNodes += Hop_DagSize( pNode->pFunc );
+    }
+    return nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index caaa86f8..72a5674b 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -31,6 +31,7 @@ extern "C" {
 
 #include "aig.h"
 #include "tim.h"
+#include "ntk.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -227,6 +228,7 @@ extern Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
 extern char *          Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
 /*=== ntlInsert.c ==========================================================*/
 extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern int             Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
 extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
@@ -236,6 +238,7 @@ extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
 extern void            Ntl_ManFree( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern void            Ntl_ManPrintStats( Ntl_Man_t * p );
+extern Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
 extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 72a8bc40..a54618e5 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -438,6 +438,8 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     // start the AIG manager
     assert( p->pAig == NULL );
     p->pAig = Aig_ManStart( 10000 );
+    p->pAig->pName = Aig_UtilStrsav( p->pName );
+    p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
     // get the root model
     pRoot = Vec_PtrEntry( p->vModels, 0 );
     // collect primary inputs
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 971d1278..84a7af84 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -123,6 +123,105 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertNtk( Ntl_Man_t * p, Ntk_Man_t * pNtk )
+{
+    char Buffer[100];
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Ntk_Obj_t * pObj, * pFanin;
+    int i, k, nDigits;
+    unsigned * pTruth;
+    assert( Vec_PtrSize(p->vCis) == Ntk_ManCiNum(pNtk) );
+    assert( Vec_PtrSize(p->vCos) == Ntk_ManCoNum(pNtk) );
+    // set the correspondence between the PI/PO nodes
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Ntk_ManCi( pNtk, i )->pCopy = pNet;
+//    Ntl_ManForEachCoNet( p, pNet, i )
+//        Ntk_ManCo( pNtk, i )->pCopy = pNet;
+    // remove old nodes
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Ntl_ModelForEachNode( pRoot, pNode, i )
+        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    // create a new node for each LUT
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    nDigits = Aig_Base10Log( Ntk_ManNodeNum(pNtk) );
+    Ntk_ManForEachNode( pNtk, pObj, i )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, Ntk_ObjFaninNum(pObj) );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, pObj->pFunc, Ntk_ObjFaninNum(pObj), vTruth, 0 );
+        pNode->pSop = Ntl_SopFromTruth( p, pTruth, Ntk_ObjFaninNum(pObj), vCover );
+        if ( !Kit_TruthIsConst0(pTruth, Ntk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Ntk_ObjFaninNum(pObj)) )
+        {
+            Ntk_ObjForEachFanin( pObj, pFanin, k )
+            {
+                pNet = pFanin->pCopy;
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+                    return 0;
+                }
+                Ntl_ObjSetFanin( pNode, pNet, k );
+            }
+        }
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        pObj->pCopy = pNet;
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->nVisits = 101;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->nVisits == 101 )
+            continue;
+        pNetCo->nVisits = 101;
+        // get the corresponding PO and its driver
+        pObj = Ntk_ManCo( pNtk, i );
+        pFanin = Ntk_ObjFanin0( pObj );
+        // get the net driving the driver
+        pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pFunc)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // update the CO driver net
+        pNetCo->pDriver = NULL;
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            return 0;
+        }
+    }
+    return 1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index b5331ae2..9614a423 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -139,6 +139,22 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
+{
+    return p->pManTime;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 3de74200..20bc79cf 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -117,7 +117,7 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
+void Ntl_ManSetIfParsDefault( If_Par_t * pPars )
 {
 //    extern void * Abc_FrameReadLibLut();
     // set defaults
@@ -162,57 +162,6 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
 */
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Load the network into FPGA manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
-{
-    If_Man_t * pIfMan;
-    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
-    Vec_Ptr_t * vNodes;
-    int i;
-    // start the mapping manager and set its parameters
-    pIfMan = If_ManStart( pPars );
-    // print warning about excessive memory usage
-    if ( 1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
-        printf( "Warning: The mapper will allocate %.1f Gb for to represent the subject graph with %d AIG nodes.\n", 
-            1.0 * Aig_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Aig_ManObjNum(p) );
-    // load the AIG into the mapper
-    vNodes = Aig_ManDfsPio( p );
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-    {
-        if ( Aig_ObjIsAnd(pNode) )
-            pNode->pData = (Aig_Obj_t *)If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
-        else if ( Aig_ObjIsPi(pNode) )
-            pNode->pData = If_ManCreateCi( pIfMan );
-        else if ( Aig_ObjIsPo(pNode) )
-            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
-        else if ( Aig_ObjIsConst1(pNode) )
-            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
-        else // add the node to the mapper
-            assert( 0 );
-        // set up the choice node
-//        if ( Aig_AigNodeIsChoice( pNode ) )
-//        {
-//            pIfMan->nChoices++;
-//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
-//                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
-//            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
-//        }
-    }
-    Vec_PtrFree( vNodes );
-    return pIfMan;
-}
 
 /**Function*************************************************************
 
@@ -225,7 +174,7 @@ If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Ntl_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 {
     If_Man_t * pIfMan;
     Aig_Obj_t * pNode;//, * pFanin, * pPrev;
@@ -251,7 +200,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
                 pIfMan->nLevelMax = (int)pNode->Level;
         }
         else if ( Aig_ObjIsPo(pNode) )
-            If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+            pNode->pData = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
         else if ( Aig_ObjIsConst1(pNode) )
             Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
         else // add the node to the mapper
@@ -264,6 +213,11 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 //                If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
 //            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
 //        }
+        {
+            If_Obj_t * pIfObj = pNode->pData;
+            assert( !If_IsComplement(pIfObj) );
+            assert( pIfObj->Id == pNode->Id );
+        }
     }
     return pIfMan;
 }
@@ -279,7 +233,7 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
+Vec_Ptr_t * Ntl_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
 {
     Vec_Ptr_t * vIfMap;
     If_Obj_t * pNode, * pLeaf; 
@@ -356,12 +310,12 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     // perform FPGA mapping
-    Ntk_ManSetIfParsDefault( pPars );
+    Ntl_ManSetIfParsDefault( pPars );
     // set the arrival times
     pPars->pTimesArr = ALLOC( float, Aig_ManPiNum(p) );
     memset( pPars->pTimesArr, 0, sizeof(float) * Aig_ManPiNum(p) );
     // translate into the mapper
-    pIfMan = Ntk_ManToIf( p, pPars );    
+    pIfMan = Ntl_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
         return NULL;
     pIfMan->pManTim = Tim_ManDup( pMan->pManTime, 0 );
@@ -371,7 +325,7 @@ Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
         return NULL;
     }
     // transform the result of mapping into the new network
-    vMapping = Ntk_ManFromIf( p, pIfMan );
+    vMapping = Ntl_ManFromIf( p, pIfMan );
     If_ManStop( pIfMan );
     if ( vMapping == NULL )
         return NULL;
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index a71e1497..77967ef6 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -150,7 +150,8 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
 
   Synopsis    [Duplicates the timing manager.]
 
-  Description []
+  Description [Derives discrete-delay-model timing manager. 
+  Useful for AIG optimization with approximate timing information.]
                
   SideEffects []
 
@@ -171,16 +172,21 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
     for ( k = 0; k < p->nPos; k++ )
         pNew->pPos[k].TravId = 0;
     if ( fDiscrete )
+    {
         for ( k = 0; k < p->nPis; k++ )
             pNew->pPis[k].timeArr = 0.0; // modify here
+        // modify the required times
+    }
     pNew->vDelayTables = Vec_PtrAlloc( 100 );
     Tim_ManForEachBox( p, pBox, i )
     {
         pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
         Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
         if ( fDiscrete )
+        {
             for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
                 pDelayTableNew[k] = 1.0; // modify here
+        }
         else
             memcpy( pDelayTableNew, pBox->pDelayTable, sizeof(float) * pBox->nInputs * pBox->nOutputs );
         Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
@@ -191,6 +197,47 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fDiscrete )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the timing manager.]
+
+  Description [Derives unit-delay-model timing manager. 
+  Useful for levelizing the network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDupUnit( Tim_Man_t * p )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    float * pDelayTableNew;
+    int i, k;
+    pNew = Tim_ManStart( p->nPis, p->nPos );
+    memcpy( pNew->pPis, p->pPis, sizeof(Tim_Obj_t) * p->nPis );
+    memcpy( pNew->pPos, p->pPos, sizeof(Tim_Obj_t) * p->nPos );
+    for ( k = 0; k < p->nPis; k++ )
+    {
+        pNew->pPis[k].TravId = 0;
+        pNew->pPis[k].timeArr = 0.0; 
+    }
+    for ( k = 0; k < p->nPos; k++ )
+        pNew->pPos[k].TravId = 0;
+    pNew->vDelayTables = Vec_PtrAlloc( 100 );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+        pDelayTableNew = ALLOC( float, pBox->nInputs * pBox->nOutputs );
+        Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
+        for ( k = 0; k < pBox->nInputs * pBox->nOutputs; k++ )
+            pDelayTableNew[k] = 1.0;
+        Tim_ManCreateBoxFirst( pNew, pBox->Inouts[0], pBox->nInputs, 
+            pBox->Inouts[pBox->nInputs], pBox->nOutputs, pDelayTableNew );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the timing manager.]
 
   Description []
@@ -567,6 +614,110 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
     return pObjThis->timeReq;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the box number for the given input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxForCi( Tim_Man_t * p, int iCi )
+{
+    if ( iCi >= p->nPis )
+        return -1;
+    return p->pPis[iCi].iObj2Box;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the box number for the given output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxForCo( Tim_Man_t * p, int iCo )
+{
+    if ( iCo >= p->nPos )
+        return -1;
+    return p->pPos[iCo].iObj2Box;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->Inouts[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->Inouts[pBox->nInputs];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxInputNum( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->nInputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first input of the box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox )
+{
+    Tim_Box_t * pBox = Vec_PtrEntry( p->vBoxes, iBox );
+    return pBox->nOutputs;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index f1fb992c..f56b0881 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -59,6 +59,7 @@ typedef struct Tim_Man_t_           Tim_Man_t;
 /*=== time.c ===========================================================*/
 extern Tim_Man_t *     Tim_ManStart( int nPis, int nPos );
 extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fDiscrete );
+extern Tim_Man_t *     Tim_ManDupUnit( Tim_Man_t * p );
 extern void            Tim_ManStop( Tim_Man_t * p );
 extern void            Tim_ManPrint( Tim_Man_t * p );
 extern void            Tim_ManSetDelayTables( Tim_Man_t * p, Vec_Ptr_t * vDelayTables );
@@ -73,6 +74,12 @@ extern void            Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay
 extern void            Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay );
 extern float           Tim_ManGetPiArrival( Tim_Man_t * p, int iPi );
 extern float           Tim_ManGetPoRequired( Tim_Man_t * p, int iPo );
+extern int             Tim_ManBoxForCi( Tim_Man_t * p, int iCo );
+extern int             Tim_ManBoxForCo( Tim_Man_t * p, int iCi );
+extern int             Tim_ManBoxInputFirst( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxOutputFirst( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxInputNum( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox );
 
 #ifdef __cplusplus
 }