Version abc80123

10 files changed, 257 insertions, 49 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index d500139d..e871373a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -254,10 +254,11 @@ static inline Aig_Obj_t *  Aig_ObjChild0( Aig_Obj_t * pObj )      { return pObj-
 static inline Aig_Obj_t *  Aig_ObjChild1( Aig_Obj_t * pObj )      { return pObj->pFanin1;                          }
 static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
 static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
-static inline void         Aig_ObjChild0Flip( Aig_Obj_t * pObj )  { pObj->pFanin0 = Aig_Not(pObj->pFanin0);        }
-static inline void         Aig_ObjChild1Flip( Aig_Obj_t * pObj )  { pObj->pFanin1 = Aig_Not(pObj->pFanin1);        }
-static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->Level;                            }
-static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
+static inline void         Aig_ObjChild0Flip( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0);        }
+static inline void         Aig_ObjChild1Flip( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1);        }
+static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { assert( !Aig_IsComplement(pObj) ); return pObj->Level;                            }
+static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
+static inline int          Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i;                    }
 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;             } 
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index d3fe1412..1388c73e 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -158,6 +158,7 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     {
         pObjNew = Aig_ObjCreatePi( pNew );
         pObjNew->pHaig = pObj->pHaig;
+        pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
     // duplicate internal nodes
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 1a3695e8..dbd8676b 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -70,6 +70,7 @@ struct Ntl_Man_t_
     Vec_Ptr_t *        vCis;           // the primary inputs of the extracted part
     Vec_Ptr_t *        vCos;           // the primary outputs of the extracted part 
     Vec_Ptr_t *        vNodes;         // the nodes of the abstracted part
+    Vec_Int_t *        vBox1Cos;       // the first COs of the boxes
     Aig_Man_t *        pAig;           // the extracted AIG
     Tim_Man_t *        pManTime;       // the timing manager
 };
@@ -143,6 +144,8 @@ static inline int         Ntl_ModelPoNum( Ntl_Mod_t * p )         { return p->nO
 static inline int         Ntl_ModelNodeNum( Ntl_Mod_t * p )       { return p->nObjs[NTL_OBJ_NODE];              } 
 static inline int         Ntl_ModelLatchNum( Ntl_Mod_t * p )      { return p->nObjs[NTL_OBJ_LATCH];             } 
 static inline int         Ntl_ModelBoxNum( Ntl_Mod_t * p )        { return p->nObjs[NTL_OBJ_BOX];               } 
+static inline int         Ntl_ModelCiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; } 
+static inline int         Ntl_ModelCoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; } 
 
 static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return Vec_PtrEntry(p->vPis, i);            } 
 static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return Vec_PtrEntry(p->vPos, i);            } 
@@ -217,6 +220,7 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 ////////////////////////////////////////////////////////////////////////
 
 /*=== ntlAig.c ==========================================================*/
+extern Aig_Obj_t *     Ntl_ManExtractAigNode( Ntl_Obj_t * pNode );
 extern int             Ntl_ManExtract( Ntl_Man_t * p );
 extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping );
 extern int             Ntl_ManInsertTest( Ntl_Man_t * p );
@@ -239,7 +243,7 @@ extern void            Ntl_ModelFree( Ntl_Mod_t * p );
 extern Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
 extern Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
 extern Vec_Ptr_t *     Ntl_MappingFpga( Aig_Man_t * p );
-extern Vec_Ptr_t *     Ntl_MappingIf( Aig_Man_t * p );
+extern Vec_Ptr_t *     Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p );
 /*=== ntlObj.c ============================================================*/
 extern Ntl_Obj_t *     Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
 extern Ntl_Obj_t *     Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
@@ -254,6 +258,8 @@ extern Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
 extern Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
 extern int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
 extern int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
+/*=== ntlTime.c ==========================================================*/
+extern Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 /*=== ntlReadBlif.c ==========================================================*/
 extern Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 /*=== ntlWriteBlif.c ==========================================================*/
diff --git a/src/aig/ntl/ntlAig.c b/src/aig/ntl/ntlAig.c
index c81280d7..c0a122d3 100644
--- a/src/aig/ntl/ntlAig.c
+++ b/src/aig/ntl/ntlAig.c
@@ -367,7 +367,7 @@ Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManExtract( Ntl_Man_t * p )
+int Ntl_ManExtract_old( Ntl_Man_t * p )
 {
     Ntl_Obj_t * pNode;
     Ntl_Net_t * pNet;
@@ -394,6 +394,30 @@ int Ntl_ManExtract( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Extracts AIG from the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManExtract( Ntl_Man_t * p )
+{
+    // start the AIG manager
+    assert( p->pAig == NULL );
+    p->pAig = Aig_ManStart( 10000 );
+    // check the DFS traversal
+    if ( !Ntl_ManDfs( p ) )
+        return 0;
+    // cleanup the AIG
+    Aig_ManCleanup( p->pAig );
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Inserts the given mapping into the netlist.]
 
   Description []
@@ -557,8 +581,8 @@ int Ntl_ManInsertTestIf( Ntl_Man_t * p )
     if ( !Ntl_ManExtract( p ) )
         return 0;
     assert( p->pAig != NULL );
-    Ntl_ManPerformSynthesis( p );
-    vMapping = Ntl_MappingIf( p->pAig );
+//    Ntl_ManPerformSynthesis( p );
+    vMapping = Ntl_MappingIf( p, p->pAig );
     RetValue = Ntl_ManInsert( p, vMapping );
     Vec_PtrFree( vMapping );
     return RetValue;
diff --git a/src/aig/ntl/ntlDfs.c b/src/aig/ntl/ntlDfs.c
index 41867b29..1e9503a4 100644
--- a/src/aig/ntl/ntlDfs.c
+++ b/src/aig/ntl/ntlDfs.c
@@ -63,13 +63,27 @@ int Ntl_ManDfs_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     // add box inputs/outputs to COs/CIs
     if ( Ntl_ObjIsBox(pObj) )
     {
+        int LevelCur, LevelMax = -AIG_INFINITY;
+        Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
         Ntl_ObjForEachFanin( pObj, pNetFanin, i )
+        {
+            LevelCur = Aig_ObjLevel( Aig_Regular(pNetFanin->pFunc) );
+            LevelMax = AIG_MAX( LevelMax, LevelCur );
             Vec_PtrPush( p->vCos, pNetFanin );
+            Aig_ObjCreatePo( p->pAig, pNetFanin->pFunc );
+        }
         Ntl_ObjForEachFanout( pObj, pNetFanin, i )
+        {
             Vec_PtrPush( p->vCis, pNetFanin );
+            pNetFanin->pFunc = Aig_ObjCreatePi( p->pAig );
+            Aig_ObjSetLevel( pNetFanin->pFunc, LevelMax + 1 );
+        }
+//printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id );
     }
     // store the node
     Vec_PtrPush( p->vNodes, pObj );
+    if ( Ntl_ObjIsNode(pObj) )
+        pNet->pFunc = Ntl_ManExtractAigNode( pObj );
     pNet->nVisits = 2;
     return 1;
 }
@@ -95,6 +109,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
     assert( Vec_PtrSize(p->vCis) == 0 );
     assert( Vec_PtrSize(p->vCos) == 0 );
     assert( Vec_PtrSize(p->vNodes) == 0 );
+    assert( Vec_IntSize(p->vBox1Cos) == 0 );
     // get the root model
     pRoot = Vec_PtrEntry( p->vModels, 0 );
     // collect primary inputs
@@ -103,6 +118,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         Vec_PtrPush( p->vCis, pNet );
+        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
         if ( pNet->nVisits )
         {
             printf( "Ntl_ManDfs(): Primary input appears twice in the list.\n" );
@@ -116,6 +132,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
         assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         Vec_PtrPush( p->vCis, pNet );
+        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
         if ( pNet->nVisits )
         {
             printf( "Ntl_ManDfs(): Latch output is duplicated or defined as a primary input.\n" );
@@ -136,6 +153,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
             return 0;
         }
         Vec_PtrPush( p->vCos, pNet );
+        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
     }
     // visit the nodes starting from latch inputs outputs
     Ntl_ModelForEachLatch( pRoot, pObj, i )
@@ -150,6 +168,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
             return 0;
         }
         Vec_PtrPush( p->vCos, pNet );
+        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
     }
     // report the number of dangling objects
     nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index ce008c9c..9b4aff5f 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -49,6 +49,7 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
     p->vCis = Vec_PtrAlloc( 1000 );
     p->vCos = Vec_PtrAlloc( 1000 );
     p->vNodes = Vec_PtrAlloc( 1000 );
+    p->vBox1Cos = Vec_IntAlloc( 1000 );
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
@@ -82,6 +83,7 @@ void Ntl_ManFree( Ntl_Man_t * p )
     if ( p->vCis )     Vec_PtrFree( p->vCis );
     if ( p->vCos )     Vec_PtrFree( p->vCos );
     if ( p->vNodes )   Vec_PtrFree( p->vNodes );
+    if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos );
     if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
     if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
     if ( p->pAig )     Aig_ManStop( p->pAig );
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index d4c7d81b..59c40453 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -412,7 +412,7 @@ void Ntk_ManSetIfParsDefault( If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
+If_Man_t * Ntk_ManToIf_old( Aig_Man_t * p, If_Par_t * pPars )
 {
     If_Man_t * pIfMan;
     Aig_Obj_t * pNode;//, * pFanin, * pPrev;
@@ -455,6 +455,58 @@ If_Man_t * Ntk_ManToIf( Aig_Man_t * p, If_Par_t * pPars )
 
 /**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;
+        }
+        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 );
+//        }
+    }
+    return pIfMan;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the mapped network.]
 
   Description []
@@ -491,10 +543,9 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
         Vec_IntWriteEntry( vIfToAig, pNode->Id, pObj->Id );
     }
     // create the mapping
-    If_ManScanMappingDirect( pMan );
+    vIfMap   = If_ManCollectMappingDirect( pMan );
     nVarsMax = pMan->pPars->nLutSize;
     nWords   = Aig_TruthWordNum( nVarsMax );
-    vIfMap   = pMan->vMapped;
     vMapping = Ntl_MappingAlloc( Vec_PtrSize(vIfMap) + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
     nLuts    = 0;
     if ( Aig_ManConst1(p)->nRefs > 0 )
@@ -521,6 +572,7 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
     }
     assert( nLuts == Vec_PtrSize(vMapping) );
     Vec_IntFree( vIfToAig );
+    Vec_PtrFree( vIfMap );
     return vMapping;
 }
 
@@ -535,7 +587,7 @@ Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Ntl_MappingIf( Aig_Man_t * p )
+Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p )
 {
     Vec_Ptr_t * vMapping;
     If_Par_t Pars, * pPars = &Pars;
@@ -549,6 +601,7 @@ Vec_Ptr_t * Ntl_MappingIf( Aig_Man_t * p )
     pIfMan = Ntk_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
         return NULL;
+    pIfMan->pManTim = Ntl_ManCreateTiming( pMan );
     if ( !If_ManPerformMapping( pIfMan ) )
     {
         If_ManStop( pIfMan );
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
index c81686fa..50f3d290 100644
--- a/src/aig/ntl/ntlTime.c
+++ b/src/aig/ntl/ntlTime.c
@@ -82,26 +82,19 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     Vec_Ptr_t * vDelayTables;
     Ntl_Mod_t * pRoot, * pModel;
     Ntl_Obj_t * pObj;
-    int i, curPi, curPo, Entry;
+    int i, curPi, iBox, Entry;
     assert( p->pAig != NULL );
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
     // start the timing manager
     pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
-    // add arrival time info for the true PIs
-    pRoot = Vec_PtrEntry( p->vModels, 0 );
-    Ntl_ModelForEachPi( pRoot, pObj, i )
-        Tim_ManInitPiArrival( pMan, i, 0.0 );
     // unpack the data in the arrival times
     if ( pRoot->vArrivals )
         Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
-            Tim_ManInitPiArrival( pMan, Entry, Vec_IntEntry(pRoot->vArrivals,++i) );
-    // add the required time into for the true POs
-    pRoot = Vec_PtrEntry( p->vModels, 0 );
-    Ntl_ModelForEachPo( pRoot, pObj, i )
-        Tim_ManInitPoRequired( pMan, i, AIG_INFINITY );
+            Tim_ManInitPiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) );
     // unpack the data in the required times
     if ( pRoot->vRequireds )
         Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
-            Tim_ManInitPoRequired( pMan, Entry, Vec_IntEntry(pRoot->vRequireds,++i) );
+            Tim_ManInitPoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) );
     // derive timing tables
     vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
     Ntl_ManForEachModel( p, pModel, i )
@@ -112,17 +105,18 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     }
     Tim_ManSetDelayTables( pMan, vDelayTables );
     // set up the boxes
-    curPi = Ntl_ModelPiNum(pRoot);
-    curPo = Ntl_ModelPoNum(pRoot);
+    iBox = 0;
+    curPi = Ntl_ModelCiNum(pRoot);
     Ntl_ManForEachBox( p, pObj, i )
     {
-        Tim_ManCreateBoxFirst( pMan, curPo, Ntl_ObjFanoutNum(pObj), curPi, Ntl_ObjFaninNum(pObj), pObj->pImplem->pDelayTable );
-        curPo += Ntl_ObjFanoutNum(pObj);
-        curPi += Ntl_ObjFaninNum(pObj);
+        Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable );
+        curPi += Ntl_ObjFanoutNum(pObj);
+        iBox++;
     }
     // forget refs to the delay tables in the network
     Ntl_ManForEachModel( p, pModel, i )
         pModel->pDelayTable = NULL;
+//    Tim_ManPrint( pMan );
     return pMan;
 }
 
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index 1bd21089..8d312dba 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -67,6 +67,7 @@ struct Tim_Box_t_
 // timing object
 struct Tim_Obj_t_
 {
+    int              Id;             // the ID of this object
     int              TravId;         // traversal ID of this object
     int              iObj2Box;       // mapping of the object into its box
     int              iObj2Num;       // mapping of the object into its number in the box
@@ -80,14 +81,23 @@ static inline Tim_Obj_t * Tim_ManPo( Tim_Man_t * p, int i )
 static inline Tim_Box_t * Tim_ManPiBox( Tim_Man_t * p, int i )                        { return Tim_ManPi(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPi(p,i)->iObj2Box ); }
 static inline Tim_Box_t * Tim_ManPoBox( Tim_Man_t * p, int i )                        { return Tim_ManPo(p,i)->iObj2Box < 0 ? NULL : Vec_PtrEntry( p->vBoxes, Tim_ManPo(p,i)->iObj2Box ); }
 
-static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i )   { return p->pPos + pBox->Inouts[i];               }
-static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i )  { return p->pPis + pBox->Inouts[pBox->nInputs+i]; }
+static inline Tim_Obj_t * Tim_ManBoxInput( Tim_Man_t * p, Tim_Box_t * pBox, int i )   { assert( i < pBox->nInputs  ); return p->pPos + pBox->Inouts[i];               }
+static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int i )  { assert( i < pBox->nOutputs ); return p->pPis + pBox->Inouts[pBox->nInputs+i]; }
 
-#define Tim_ManBoxForEachInput( p, pBox, pObj, i )                                  \
+#define Tim_ManBoxForEachInput( p, pBox, pObj, i )                               \
     for ( i = 0; (i < (pBox)->nInputs) && ((pObj) = Tim_ManBoxInput(p, pBox, i)); i++ )
-#define Tim_ManBoxForEachOutput( p, pBox, pObj, i )                                 \
+#define Tim_ManBoxForEachOutput( p, pBox, pObj, i )                              \
     for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ )
 
+#define Tim_ManForEachPi( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nPis) && ((pObj) = (p)->pPis + i); i++ )              \
+        if ( pObj->iObj2Box >= 0 ) {} else 
+#define Tim_ManForEachPo( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nPos) && ((pObj) = (p)->pPos + i); i++ )              \
+        if ( pObj->iObj2Box >= 0 ) {} else 
+#define Tim_ManForEachBox( p, pBox, i )                                          \
+    Vec_PtrForEachEntry( p->vBoxes, pBox, i )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -111,7 +121,6 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
     memset( p, 0, sizeof(Tim_Man_t) );
     p->pMemObj = Mem_FlexStart();
     p->vBoxes  = Vec_PtrAlloc( 100 );
-    Vec_PtrPush( p->vBoxes, NULL );
     p->nPis = nPis;
     p->nPos = nPos;
     p->pPis = ALLOC( Tim_Obj_t, nPis );
@@ -119,9 +128,21 @@ Tim_Man_t * Tim_ManStart( int nPis, int nPos )
     p->pPos = ALLOC( Tim_Obj_t, nPos );
     memset( p->pPos, 0, sizeof(Tim_Obj_t) * nPos );
     for ( i = 0; i < nPis; i++ )
+    {
+        p->pPis[i].Id = i;
         p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
+        p->pPis[i].timeReq = AIG_INFINITY;
+        p->pPis[i].timeArr = 0.0;
+        p->pPis[i].TravId = 0;
+    }
     for ( i = 0; i < nPos; i++ )
+    {
+        p->pPos[i].Id = i;
         p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1;
+        p->pPos[i].timeReq = AIG_INFINITY;
+        p->pPos[i].timeArr = 0.0;
+        p->pPos[i].TravId = 0;
+    }
     return p;
 }
 
@@ -155,6 +176,42 @@ void Tim_ManStop( Tim_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Stops the timing manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManPrint( Tim_Man_t * p )
+{
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    int i;
+    printf( "TIMING INFORMATION:\n" );
+    Tim_ManForEachPi( p, pObj, i )
+        printf( "pi%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+    Tim_ManForEachPo( p, pObj, i )
+        printf( "po%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+    Tim_ManForEachBox( p, pBox, i )
+    {
+        printf( "*** Box %3d :  Ins = %d. Outs = %d.\n", i, pBox->nInputs, pBox->nOutputs );
+        printf( "Delay table:" );
+        for ( i = 0; i < pBox->nInputs * pBox->nOutputs; i++ )
+            printf( " %5.3f", pBox->pDelayTable[i] );
+        printf( "\n" );
+        Tim_ManBoxForEachInput( p, pBox, pObj, i )
+            printf( "box-inp%3d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+        Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+            printf( "box-out%3d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sets the vector of timing tables associated with the manager.]
 
   Description []
@@ -295,12 +352,12 @@ void Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay )
 void Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay )
 {
     assert( iPo < p->nPos );
-    p->pPos[iPo].timeArr = Delay;
+    p->pPos[iPo].timeReq = Delay;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Updates arrival time of the PO.]
+  Synopsis    [Updates required time of the PO.]
 
   Description []
                
@@ -319,7 +376,7 @@ void Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay )
 
 /**Function*************************************************************
 
-  Synopsis    [Updates required time of the PI.]
+  Synopsis    [Updates arrival time of the PI.]
 
   Description []
                
@@ -336,6 +393,44 @@ void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
     p->pPis[iPi].TravId = p->nTravIds;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Updates required time of the PO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetPoRequired( Tim_Man_t * p, int iPo, float Delay )
+{
+    assert( iPo < p->nPos );
+    assert( p->pPos[iPo].TravId != p->nTravIds );
+    p->pPos[iPo].timeReq = Delay;
+    p->pPos[iPo].TravId = p->nTravIds;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the correct required times for all POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Tim_ManSetPoRequiredAll( Tim_Man_t * p, float Delay )
+{
+    Tim_Obj_t * pObj;
+    int i;
+    Tim_ManForEachPo( p, pObj, i )
+        Tim_ManSetPoRequired( p, i, Delay );
+}
+
 
 /**Function*************************************************************
 
@@ -351,20 +446,25 @@ void Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay )
 float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
 {
     Tim_Box_t * pBox;
-    Tim_Obj_t * pObj, * pObjRes;
+    Tim_Obj_t * pObjThis, * pObj, * pObjRes;
     float * pDelays, DelayBest;
     int i, k;
-    // consider the main PI or the already processed PI
+    // consider the already processed PI
+    pObjThis = Tim_ManPi( p, iPi );
+    if ( pObjThis->TravId == p->nTravIds )
+        return pObjThis->timeArr;
+    pObjThis->TravId = p->nTravIds;
+    // consider the main PI
     pBox = Tim_ManPiBox( p, iPi );
-    if ( pBox == NULL || pBox->TravId == p->nTravIds )
-        return Tim_ManPi(p, iPi)->timeArr;
+    if ( pBox == NULL )
+        return pObjThis->timeArr;
     // update box timing
     pBox->TravId = p->nTravIds;
     // get the arrival times of the inputs of the box (POs)
     Tim_ManBoxForEachInput( p, pBox, pObj, i )
         if ( pObj->TravId != p->nTravIds )
             printf( "Tim_ManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
-    // compute the required times for each output of the box (PIs)
+    // compute the arrival times for each output of the box (PIs)
     Tim_ManBoxForEachOutput( p, pBox, pObjRes, i )
     {
         pDelays = pBox->pDelayTable + i * pBox->nInputs;
@@ -374,7 +474,7 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
         pObjRes->timeArr = DelayBest;
         pObjRes->TravId = p->nTravIds;
     }
-    return Tim_ManPi(p, iPi)->timeArr;
+    return pObjThis->timeArr;
 }
 
 /**Function*************************************************************
@@ -391,16 +491,21 @@ float Tim_ManGetPiArrival( Tim_Man_t * p, int iPi )
 float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
 {
     Tim_Box_t * pBox;
-    Tim_Obj_t * pObj, * pObjRes;
+    Tim_Obj_t * pObjThis, * pObj, * pObjRes;
     float * pDelays, DelayBest;
     int i, k;
-    // consider the main PO or the already processed PO
+    // consider the already processed PO
+    pObjThis = Tim_ManPo( p, iPo );
+    if ( pObjThis->TravId == p->nTravIds )
+        return pObjThis->timeReq;
+    pObjThis->TravId = p->nTravIds;
+    // consider the main PO
     pBox = Tim_ManPoBox( p, iPo );
-    if ( pBox == NULL || pBox->TravId == p->nTravIds )
-        return Tim_ManPo(p, iPo)->timeReq;
+    if ( pBox == NULL )
+        return pObjThis->timeReq;
     // update box timing
     pBox->TravId = p->nTravIds;
-    // get the arrival times of the inputs of the box (POs)
+    // get the required times of the inputs of the box (POs)
     Tim_ManBoxForEachOutput( p, pBox, pObj, i )
         if ( pObj->TravId != p->nTravIds )
             printf( "Tim_ManGetPoRequired(): PI required times of the box are not up to date!\n" );
@@ -411,12 +516,12 @@ float Tim_ManGetPoRequired( Tim_Man_t * p, int iPo )
         Tim_ManBoxForEachOutput( p, pBox, pObj, k )
         {
             pDelays = pBox->pDelayTable + k * pBox->nInputs;
-            DelayBest = AIG_MIN( DelayBest, pObj->timeReq + pDelays[i] );
+            DelayBest = AIG_MIN( DelayBest, pObj->timeReq - pDelays[i] );
         }
         pObjRes->timeReq = DelayBest;
         pObjRes->TravId = p->nTravIds;
     }
-    return Tim_ManPo(p, iPo)->timeReq;
+    return pObjThis->timeReq;
 }
 
 
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index 8b11ca02..d7544169 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 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 );
 extern void            Tim_ManCreateBox( Tim_Man_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
 extern void            Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
@@ -67,6 +68,8 @@ extern void            Tim_ManInitPiArrival( Tim_Man_t * p, int iPi, float Delay
 extern void            Tim_ManInitPoRequired( Tim_Man_t * p, int iPo, float Delay );
 extern void            Tim_ManSetPoArrival( Tim_Man_t * p, int iPo, float Delay );
 extern void            Tim_ManSetPiRequired( Tim_Man_t * p, int iPi, float Delay );
+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 );