Version abc71225

10 files changed, 904 insertions, 85 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 6b34e853..28bae70f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -388,6 +388,7 @@ extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
 extern void            Aig_ManCheckPhase( Aig_Man_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
+extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *     Aig_ManDfsChoices( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsReverse( Aig_Man_t * p );
@@ -555,16 +556,17 @@ extern int             Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
 /*=== aigTime.c ===========================================================*/
 extern Aig_TMan_t *    Aig_TManStart( int nPis, int nPos );
 extern void            Aig_TManStop( Aig_TMan_t * p );
-extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes );
-extern void            Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay );
-extern void            Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay );
-extern void            Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay );
-extern void            Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables );
+extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable );
+extern void            Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable );
 extern void            Aig_TManIncrementTravId( Aig_TMan_t * p );
+extern void            Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay );
+extern void            Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay );
 extern float           Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
 extern float           Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
 
-
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index dedfeb4a..c7488487 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -46,7 +46,7 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
-    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+//    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
     Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
     Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
     assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
@@ -99,6 +99,29 @@ Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ManDfs_rec( p, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
 {
     Vec_Ptr_t * vNodes;
diff --git a/src/aig/aig/aigTime.c b/src/aig/aig/aigTime.c
index 42f5f575..1544a15b 100644
--- a/src/aig/aig/aigTime.c
+++ b/src/aig/aig/aigTime.c
@@ -31,6 +31,7 @@ typedef struct Aig_TObj_t_           Aig_TObj_t;
 struct Aig_TMan_t_
 {
     Vec_Ptr_t *      vBoxes;         // the timing boxes
+    Vec_Ptr_t *      vDelayTables;   // pointers to the delay tables
     Aig_MmFlex_t *   pMemObj;        // memory manager for boxes
     int              nTravIds;       // traversal ID of the manager
     int              nPis;           // the number of PIs
@@ -44,17 +45,20 @@ struct Aig_TBox_t_
 {
     int              iBox;           // the unique ID of this box
     int              TravId;         // traversal ID of this box
-    int              nInputs;        // the number of box inputs 
-    int              nOutputs;       // the number of box outputs
+    int              nInputs;        // the number of box inputs (POs)
+    int              nOutputs;       // the number of box outputs (PIs)
+    float *          pDelayTable;    // delay for each input->output path
     int              Inouts[0];      // the int numbers of PIs and POs
 };
 
 // timing object
 struct Aig_TObj_t_
 {
+    int              TravId;         // traversal ID of this object
     int              iObj2Box;       // mapping of the object into its box
-    float            timeOffset;     // the static timing of the node
-    float            timeActual;     // the actual timing of the node
+    int              iObj2Num;       // mapping of the object into its number in the box
+    float            timeArr;        // arrival time of the object
+    float            timeReq;        // required time of the object
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -88,9 +92,9 @@ Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
     p->pPos = ALLOC( Aig_TObj_t, nPos );
     memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos );
     for ( i = 0; i < nPis; i++ )
-        p->pPis[i].iObj2Box = -1;
+        p->pPis[i].iObj2Box = p->pPis[i].iObj2Num = -1;
     for ( i = 0; i < nPos; i++ )
-        p->pPos[i].iObj2Box = -1;
+        p->pPos[i].iObj2Box = p->pPos[i].iObj2Num = -1;
     return p;
 }
 
@@ -107,6 +111,14 @@ Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
 ***********************************************************************/
 void Aig_TManStop( Aig_TMan_t * p )
 {
+    float * pTable;
+    int i;
+    if ( p->vDelayTables )
+    {
+        Vec_PtrForEachEntry( p->vDelayTables, pTable, i )
+            FREE( pTable );
+        Vec_PtrFree( p->vDelayTables );
+    }
     Vec_PtrFree( p->vBoxes );
     Aig_MmFlexStop( p->pMemObj, 0 );
     free( p->pPis );
@@ -116,6 +128,23 @@ void Aig_TManStop( Aig_TMan_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Increments the trav ID of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetDelayTables( Aig_TMan_t * p, Vec_Ptr_t * vDelayTables )
+{
+    assert( p->vDelayTables == NULL );
+    p->vDelayTables = vDelayTables;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the new timing box.]
 
   Description []
@@ -125,29 +154,30 @@ void Aig_TManStop( Aig_TMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes )
+void Aig_TManCreateBox( Aig_TMan_t * p, int * pIns, int nIns, int * pOuts, int nOuts, float * pDelayTable )
 {
     Aig_TBox_t * pBox;
     int i;
-    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nPis+nPos) );
+    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nIns+nOuts) );
     memset( pBox, 0, sizeof(Aig_TBox_t) );
     pBox->iBox = Vec_PtrSize( p->vBoxes );
     Vec_PtrPush( p->vBoxes, pBox );
-    pBox->nInputs = nPis;
-    pBox->nOutputs = nPos;
-    for ( i = 0; i < nPis; i++ )
+    pBox->pDelayTable = pDelayTable;
+    pBox->nInputs  = nIns;
+    pBox->nOutputs = nOuts;
+    for ( i = 0; i < nIns; i++ )
     {
-        assert( pPis[i] < p->nPis );
-        pBox->Inouts[i] = pPis[i];
-        Aig_TManSetPiArrival( p, pPis[i], pPiTimes[i] );
-        p->pPis[pPis[i]].iObj2Box = pBox->iBox;
+        assert( pIns[i] < p->nPos );
+        pBox->Inouts[i] = pIns[i];
+        p->pPos[pIns[i]].iObj2Box = pBox->iBox;
+        p->pPos[pIns[i]].iObj2Num = i;
     }
-    for ( i = 0; i < nPos; i++ )
+    for ( i = 0; i < nOuts; i++ )
     {
-        assert( pPos[i] < p->nPos );
-        pBox->Inouts[nPis+i] = pPos[i];
-        Aig_TManSetPoRequired( p, pPos[i], pPoTimes[i] );
-        p->pPos[pPos[i]].iObj2Box = pBox->iBox;
+        assert( pOuts[i] < p->nPis );
+        pBox->Inouts[nIns+i] = pOuts[i];
+        p->pPis[pOuts[i]].iObj2Box = pBox->iBox;
+        p->pPis[pOuts[i]].iObj2Num = i;
     }
 }
 
@@ -162,15 +192,38 @@ void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nP
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
+void Aig_TManCreateBoxFirst( Aig_TMan_t * p, int firstIn, int nIns, int firstOut, int nOuts, float * pDelayTable )
 {
-    assert( iPi < p->nPis );
-    p->pPis[iPi].timeActual = Delay;
+    Aig_TBox_t * pBox;
+    int i;
+    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nIns+nOuts) );
+    memset( pBox, 0, sizeof(Aig_TBox_t) );
+    pBox->iBox = Vec_PtrSize( p->vBoxes );
+    Vec_PtrPush( p->vBoxes, pBox );
+    pBox->pDelayTable = pDelayTable;
+    pBox->nInputs  = nIns;
+    pBox->nOutputs = nOuts;
+    for ( i = 0; i < nIns; i++ )
+    {
+        assert( firstIn+i < p->nPos );
+        pBox->Inouts[i] = firstIn+i;
+        p->pPos[firstIn+i].iObj2Box = pBox->iBox;
+        p->pPos[firstIn+i].iObj2Num = i;
+    }
+    for ( i = 0; i < nOuts; i++ )
+    {
+        assert( firstOut+i < p->nPis );
+        pBox->Inouts[nIns+i] = firstOut+i;
+        p->pPis[firstOut+i].iObj2Box = pBox->iBox;
+        p->pPis[firstOut+i].iObj2Num = i;
+    }
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Creates the new timing box.]
+  Synopsis    [Increments the trav ID of the manager.]
 
   Description []
                
@@ -179,10 +232,9 @@ void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
+void Aig_TManIncrementTravId( Aig_TMan_t * p )
 {
-    assert( iPo < p->nPos );
-    p->pPos[iPo].timeActual = Delay;
+    p->nTravIds++;
 }
 
 /**Function*************************************************************
@@ -196,10 +248,10 @@ void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
+void Aig_TManInitPiArrival( Aig_TMan_t * p, int iPi, float Delay )
 {
     assert( iPi < p->nPis );
-    p->pPis[iPi].timeOffset = Delay;
+    p->pPis[iPi].timeArr = Delay;
 }
 
 /**Function*************************************************************
@@ -213,15 +265,15 @@ void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
+void Aig_TManInitPoRequired( Aig_TMan_t * p, int iPo, float Delay )
 {
     assert( iPo < p->nPos );
-    p->pPos[iPo].timeOffset = Delay;
+    p->pPos[iPo].timeArr = Delay;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Increments the trav ID of the manager.]
+  Synopsis    [Creates the new timing box.]
 
   Description []
                
@@ -230,9 +282,12 @@ void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_TManIncrementTravId( Aig_TMan_t * p )
+void Aig_TManSetPoArrival( Aig_TMan_t * p, int iPo, float Delay )
 {
-    p->nTravIds++;
+    assert( iPo < p->nPos );
+    assert( p->pPos[iPo].TravId != p->nTravIds );
+    p->pPos[iPo].timeArr = Delay;
+    p->pPos[iPo].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
@@ -250,29 +305,62 @@ float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
 {
     Aig_TBox_t * pBox;
     Aig_TObj_t * pObj;
+    float * pDelays;
     float DelayMax;
-    int i;
+    int i, k;
     assert( iPi < p->nPis );
     if ( p->pPis[iPi].iObj2Box < 0 )
-        return p->pPis[iPi].timeOffset;
+        return p->pPis[iPi].timeArr;
     pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
     // check if box timing is updated
     if ( pBox->TravId == p->nTravIds )
-        return p->pPis[iPi].timeOffset;
+    {
+        assert( pBox->TravId == p->nTravIds );
+        return p->pPis[iPi].timeArr;
+    }
     pBox->TravId = p->nTravIds;
     // update box timing
-    DelayMax = -1.0e+20F;
-    for ( i = 0; i < pBox->nOutputs; i++ )
+    // get the arrival times of the inputs of the box (POs)
+    for ( i = 0; i < pBox->nInputs; i++ )
     {
-        pObj = p->pPos + pBox->Inouts[pBox->nInputs+i];
-        DelayMax = AIG_MAX( DelayMax, pObj->timeActual + pObj->timeOffset );
+        pObj = p->pPos + pBox->Inouts[i];
+        if ( pObj->TravId != p->nTravIds )
+            printf( "Aig_TManGetPiArrival(): PO arrival times of the box are not up to date!\n" );
     }
-    for ( i = 0; i < pBox->nInputs; i++ )
+    // compute the required times for each output of the box (PIs)
+    for ( i = 0; i < pBox->nOutputs; i++ )
     {
-        pObj = p->pPis + pBox->Inouts[i];
-        pObj->timeActual = DelayMax + pObj->timeOffset;
+        pDelays = pBox->pDelayTable + i * pBox->nInputs;
+        DelayMax = -AIG_INFINITY;
+        for ( k = 0; k < pBox->nInputs; k++ )
+        {
+            pObj = p->pPos + pBox->Inouts[k];
+            DelayMax = AIG_MAX( DelayMax, pObj->timeArr + pDelays[k] );
+        }
+        pObj = p->pPis + pBox->Inouts[pBox->nInputs+i];
+        pObj->timeArr = DelayMax;
+        pObj->TravId = p->nTravIds;
     }
-    return p->pPis[iPi].timeActual;
+    return p->pPis[iPi].timeArr;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns PO required time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetPiRequired( Aig_TMan_t * p, int iPi, float Delay )
+{
+    assert( iPi < p->nPis );
+    assert( p->pPis[iPi].TravId != p->nTravIds );
+    p->pPis[iPi].timeReq = Delay;
+    p->pPis[iPi].TravId = p->nTravIds;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index ea6070a4..f47108a4 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -1,10 +1,11 @@
-SRC +=    src/aig/mem/ntlAig.c \
-    src/aig/mem/ntlCheck.c \
-    src/aig/mem/ntlDfs.c \
-    src/aig/mem/ntlMan.c \
-    src/aig/mem/ntlMap.c \
-    src/aig/mem/ntlObj.c \
-    src/aig/mem/ntlReadBlif.c \
-    src/aig/mem/ntlTable.c \
-    src/aig/mem/ntlWriteBlif.c
+SRC +=    src/aig/ntl/ntlAig.c \
+    src/aig/ntl/ntlCheck.c \
+    src/aig/ntl/ntlDfs.c \
+    src/aig/ntl/ntlMan.c \
+    src/aig/ntl/ntlMap.c \
+    src/aig/ntl/ntlObj.c \
+    src/aig/ntl/ntlReadBlif.c \
+    src/aig/ntl/ntlTable.c \
+    src/aig/ntl/ntlTime.c \
+    src/aig/ntl/ntlWriteBlif.c
 
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index af1e114d..ab93895d 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -47,13 +47,13 @@ typedef struct Ntl_Lut_t_    Ntl_Lut_t;
 
 // object types
 typedef enum { 
-    NTL_OBJ_NONE,                     // 0: non-existent object
-    NTL_OBJ_PI,                       // 1: primary input
-    NTL_OBJ_PO,                       // 2: primary output
-    NTL_OBJ_LATCH,                    // 3: latch node
-    NTL_OBJ_NODE,                     // 4: logic node
-    NTL_OBJ_BOX,                      // 5: white box or black box
-    NTL_OBJ_VOID                      // 6: unused object
+    NTL_OBJ_NONE,                      // 0: non-existent object
+    NTL_OBJ_PI,                        // 1: primary input
+    NTL_OBJ_PO,                        // 2: primary output
+    NTL_OBJ_LATCH,                     // 3: latch node
+    NTL_OBJ_NODE,                      // 4: logic node
+    NTL_OBJ_BOX,                       // 5: white box or black box
+    NTL_OBJ_VOID                       // 6: unused object
 } Ntl_Type_t;
 
 struct Ntl_Man_t_
@@ -88,6 +88,9 @@ struct Ntl_Mod_t_
     int                nEntries;       // the number of entries in the hash table
     // delay information
     Vec_Int_t *        vDelays;
+    Vec_Int_t *        vArrivals;
+    Vec_Int_t *        vRequireds;
+    float *            pDelayTable;   
 }; 
 
 struct Ntl_Obj_t_
@@ -148,8 +151,8 @@ static inline char *      Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_M
 
 static inline int         Ntl_ModelIsBlackBox( Ntl_Mod_t * p )    { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } 
 
-static inline int         Ntl_ObjNumFanins( Ntl_Obj_t * p )       { return p->nFanins;                          } 
-static inline int         Ntl_ObjNumFanouts( Ntl_Obj_t * p )      { return p->nFanouts;                         } 
+static inline int         Ntl_ObjFaninNum( Ntl_Obj_t * p )        { return p->nFanins;                          } 
+static inline int         Ntl_ObjFanoutNum( Ntl_Obj_t * p )       { return p->nFanouts;                         } 
 
 static inline int         Ntl_ObjIsPi( Ntl_Obj_t * p )            { return p->Type == NTL_OBJ_PI;               } 
 static inline int         Ntl_ObjIsPo( Ntl_Obj_t * p )            { return p->Type == NTL_OBJ_PO;               } 
@@ -224,8 +227,9 @@ extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
 extern int             Ntl_ManDfs( Ntl_Man_t * p );
 /*=== ntlMan.c ============================================================*/
 extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
-extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 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 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/ntlDfs.c b/src/aig/ntl/ntlDfs.c
index 6b5dc407..41867b29 100644
--- a/src/aig/ntl/ntlDfs.c
+++ b/src/aig/ntl/ntlDfs.c
@@ -100,7 +100,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
     // collect primary inputs
     Ntl_ModelForEachPi( pRoot, pObj, i )
     {
-        assert( Ntl_ObjNumFanouts(pObj) == 1 );
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         Vec_PtrPush( p->vCis, pNet );
         if ( pNet->nVisits )
@@ -113,7 +113,7 @@ int Ntl_ManDfs( Ntl_Man_t * p )
     // collect latch outputs
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        assert( Ntl_ObjNumFanouts(pObj) == 1 );
+        assert( Ntl_ObjFanoutNum(pObj) == 1 );
         pNet = Ntl_ObjFanout0(pObj);
         Vec_PtrPush( p->vCis, pNet );
         if ( pNet->nVisits )
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 6d71adb2..ce008c9c 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -111,6 +111,31 @@ Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintStats( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    printf( "%-15s : ",       p->pName );
+    printf( "pi = %5d  ",    Ntl_ModelPiNum(pRoot) );
+    printf( "po = %5d  ",    Ntl_ModelPoNum(pRoot) );
+    printf( "latch = %5d  ", Ntl_ModelLatchNum(pRoot) );
+    printf( "node = %5d  ",  Ntl_ModelNodeNum(pRoot) );
+    printf( "box = %4d  ",   Ntl_ModelBoxNum(pRoot) );
+    printf( "model = %3d",   Vec_PtrSize(p->vModels) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
@@ -152,7 +177,9 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
 ***********************************************************************/
 void Ntl_ModelFree( Ntl_Mod_t * p )
 {
-    if ( p->vDelays ) Vec_IntFree( p->vDelays );
+    if ( p->vRequireds )  Vec_IntFree( p->vRequireds );
+    if ( p->vArrivals )   Vec_IntFree( p->vArrivals );
+    if ( p->vDelays )     Vec_IntFree( p->vDelays );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index 1d8443b4..7ee0fba0 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "ntl.h"
+#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -103,6 +104,443 @@ Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
     return vMapping;
 }
 
+
+#include "fpgaInt.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ntl_FpgaComputeTruth_rec( Fpga_Cut_t * pCut, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore, Vec_Ptr_t * vVisited, int nVars, int * pnCounter )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    assert( !Fpga_IsComplement(pCut) );
+    // if the cut is visited, return the result
+    if ( pCut->pRoot )
+        return (unsigned *)pCut->pRoot;
+    // compute the functions of the children
+    pTruth0 = Ntl_FpgaComputeTruth_rec( Fpga_CutRegular(pCut->pOne), vTruthElem, vTruthStore, vVisited, nVars, pnCounter );  
+    if ( Fpga_CutIsComplement(pCut->pOne) )
+        Kit_TruthNot( pTruth0, pTruth0, nVars );
+    pTruth1 = Ntl_FpgaComputeTruth_rec( Fpga_CutRegular(pCut->pTwo), vTruthElem, vTruthStore, vVisited, nVars, pnCounter );   
+    if ( Fpga_CutIsComplement(pCut->pTwo) )
+        Kit_TruthNot( pTruth1, pTruth1, nVars );
+    // get the function of the cut
+    pTruth = Vec_PtrEntry( vTruthStore, (*pnCounter)++ );
+    Kit_TruthAnd( pTruth, pTruth0, pTruth1, nVars );
+    if ( pCut->Phase )
+        Kit_TruthNot( pTruth, pTruth, nVars );
+    assert( pCut->pRoot == NULL );
+    pCut->pRoot = (Fpga_Node_t *)pTruth;
+    // add this cut to the visited list
+    Vec_PtrPush( vVisited, pCut );
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ntl_FpgaComputeTruth( Fpga_Cut_t * pCut, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore, Vec_Ptr_t * vVisited, int nVars )
+{
+    unsigned * pTruth;
+    int i, nCounter = 0;
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pCuts->pRoot = (Fpga_Node_t *)Vec_PtrEntry( vTruthElem, i );
+    // recursively compute the function
+    Vec_PtrClear( vVisited );
+    pTruth = Ntl_FpgaComputeTruth_rec( pCut, vTruthElem, vTruthStore, vVisited, nVars, &nCounter ); 
+    // clean the intermediate BDDs
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        pCut->ppLeaves[i]->pCuts->pRoot = NULL;
+    Vec_PtrForEachEntry( vVisited, pCut, i )
+        pCut->pRoot = NULL;
+    return pTruth;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fpga_Man_t * Ntl_ManToFpga( Aig_Man_t * p )
+{
+    Fpga_Man_t * pMan;
+    Aig_Obj_t * pNode;//, * pFanin, * pPrev;
+    float * pfArrivals;
+    int i;
+    // start the mapping manager and set its parameters
+    pMan = Fpga_ManCreate( Aig_ManPiNum(p), Aig_ManPoNum(p), 0 );
+    if ( pMan == NULL )
+        return NULL;
+    // set the arrival times
+    pfArrivals = ALLOC( float, Aig_ManPiNum(p) );
+    memset( pfArrivals, 0, sizeof(float) * Aig_ManPiNum(p) );
+    Fpga_ManSetInputArrivals( pMan, pfArrivals );
+    // create PIs and remember them in the old nodes
+    Aig_ManConst1(p)->pData = Fpga_ManReadConst1(pMan);
+    Aig_ManForEachPi( p, pNode, i )
+        pNode->pData = Fpga_ManReadInputs(pMan)[i];
+    // load the AIG into the mapper
+    Aig_ManForEachNode( p, pNode, i )
+    {
+        pNode->pData = Fpga_NodeAnd( pMan, 
+            Fpga_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ),
+            Fpga_NotCond( Aig_ObjFanin1(pNode)->pData, Aig_ObjFaninC1(pNode) ) );
+        // set up the choice node
+//        if ( Aig_AigNodeIsChoice( pNode ) )
+//            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+//            {
+//                Fpga_NodeSetNextE( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
+//                Fpga_NodeSetRepr( (If_Obj_t *)pFanin->pData, (If_Obj_t *)pNode->pData );
+//            }
+    }
+    // set the primary outputs while copying the phase
+    Aig_ManForEachPo( p, pNode, i )
+        Fpga_ManReadOutputs(pMan)[i] = Fpga_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) );
+    assert( Fpga_NodeVecReadSize(pMan->vAnds) == Aig_ManNodeNum(p) );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_ManFromFpga( Aig_Man_t * p, Fpga_Man_t * pMan )
+{
+    Fpga_NodeVec_t * vFpgaMap;
+    Fpga_Node_t ** ppLeaves, * pNode; 
+    Fpga_Cut_t * pCutBest;
+    Vec_Ptr_t * vTruthElem, * vTruthStore, * vVisited, * vMapping;
+    Vec_Int_t * vFpgaToAig;
+    Aig_Obj_t * pObj;
+    Ntl_Lut_t * pLut;
+    unsigned * pTruth;
+    int i, k = 0, nLeaves, nWords, nVarsMax;
+    // create mapping of FPGA nodes into AIG nodes
+    vFpgaToAig = Vec_IntStart( Aig_ManObjNumMax(p) );
+    Vec_IntFill( vFpgaToAig, Aig_ManObjNumMax(p), -1 );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+        pNode = pObj->pData;
+        assert( pNode != NULL );
+        Vec_IntWriteEntry( vFpgaToAig, Fpga_NodeReadNum(pNode), pObj->Id );
+    }
+    // create the mapping
+    nVarsMax = Fpga_ManReadVarMax( pMan );
+    nWords   = Aig_TruthWordNum( nVarsMax );
+    vFpgaMap = Fpga_ManReadMapping( pMan );
+    vMapping = Ntl_MappingAlloc( vFpgaMap->nSize + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
+    if ( Aig_ManConst1(p)->nRefs > 0 )
+    {
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = 0;
+        pLut->nFanins = 0;
+        memset( pLut->pTruth, 0xFF, 4 * nWords );
+    }
+    vVisited    = Vec_PtrAlloc( 1000 );
+    vTruthElem  = Vec_PtrAllocTruthTables( nVarsMax );
+    vTruthStore = Vec_PtrAllocSimInfo( 256, nWords );
+    for ( i = 0; i < vFpgaMap->nSize; i++ )
+    {
+        // get the best cut
+        pNode    = vFpgaMap->pArray[i];
+        pCutBest = Fpga_NodeReadCutBest( pNode );
+        nLeaves  = Fpga_CutReadLeavesNum( pCutBest ); 
+        ppLeaves = Fpga_CutReadLeaves( pCutBest );
+        // fill the LUT
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(pNode) );
+        pLut->nFanins = nLeaves;
+        for ( k = 0; k < nLeaves; k++ )
+            pLut->pFanins[k] = Vec_IntEntry( vFpgaToAig, Fpga_NodeReadNum(ppLeaves[k]) );
+        // compute the truth table
+        pTruth = Ntl_FpgaComputeTruth( pCutBest, vTruthElem, vTruthStore, vVisited, nVarsMax );
+        memcpy( pLut->pTruth, pTruth, 4 * nWords );
+    }
+    assert( k == Vec_PtrSize(vMapping) );
+    Vec_IntFree( vFpgaToAig );
+    Vec_PtrFree( vVisited );
+    Vec_PtrFree( vTruthElem );
+    Vec_PtrFree( vTruthStore );
+    return vMapping;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_ManFpga( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMapping;
+    Fpga_Man_t * pMan;
+    // print a warning about choice nodes
+    if ( p->pEquivs )
+        printf( "Ntl_ManFpga(): Performing FPGA mapping with choices.\n" );
+    // perform FPGA mapping
+    pMan = Ntl_ManToFpga( p );    
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Fpga_Mapping( pMan ) )
+    {
+        Fpga_ManFree( pMan );
+        return NULL;
+    }
+    // transform the result of mapping into a BDD network
+    vMapping = Ntl_ManFromFpga( p, pMan );
+    Fpga_ManFree( pMan );
+    if ( vMapping == NULL )
+        return NULL;
+    return vMapping;
+}
+
+
+
+
+#include "if.h"
+
+/**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->nCutsMax    =  8;
+    pPars->nFlowIters  =  1;
+    pPars->nAreaIters  =  2;
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  1;
+    pPars->fLatchPaths =  0;
+    pPars->fEdge       =  1;
+    pPars->fCutMin     =  1;
+    pPars->fSeqMap     =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->nLatches    =  0;
+    pPars->fLiftLeaves =  0;
+    pPars->pLutLib     =  Abc_FrameReadLibLut();
+    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;
+    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_ObjIsConst1(pNode) )
+            Aig_ManConst1(p)->pData = If_ManConst1( pIfMan );
+        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 // add the node to the mapper
+            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) ) );
+        // 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*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntk_ManFromIf( Aig_Man_t * p, If_Man_t * pMan )
+{
+    Vec_Ptr_t * vIfMap;
+    If_Obj_t * pNode, * pLeaf; 
+    If_Cut_t * pCutBest;
+    Vec_Ptr_t * vMapping;
+    Vec_Int_t * vIfToAig;
+    Aig_Obj_t * pObj;
+    Ntl_Lut_t * pLut;
+    int * ppLeaves;
+    int i, k = 0, nLeaves, nWords, nVarsMax;
+    // create mapping of If nodes into AIG nodes
+    vIfToAig = Vec_IntStart( Aig_ManObjNumMax(p) );
+    Vec_IntFill( vIfToAig, Aig_ManObjNumMax(p), -1 );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+        pNode = pObj->pData;
+        assert( pNode != NULL );
+        Vec_IntWriteEntry( vIfToAig, pNode->Id, pObj->Id );
+    }
+    // create the mapping
+    nVarsMax = pMan->pPars->nLutSize;
+    nWords   = Aig_TruthWordNum( nVarsMax );
+    vIfMap   = pMan->vMapped;
+    vMapping = Ntl_MappingAlloc( Vec_PtrSize(vIfMap) + (int)(Aig_ManConst1(p)->nRefs > 0), nVarsMax );
+    if ( Aig_ManConst1(p)->nRefs > 0 )
+    {
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = 0;
+        pLut->nFanins = 0;
+        memset( pLut->pTruth, 0xFF, 4 * nWords );
+    }
+    Vec_PtrForEachEntry( vIfMap, pNode, i )
+    {
+        // get the best cut
+        pCutBest = If_ObjCutBest(pNode);
+        nLeaves  = If_CutLeaveNum( pCutBest ); 
+        ppLeaves = If_CutLeaves( pCutBest );
+        // fill the LUT
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = Vec_IntEntry( vIfToAig, pNode->Id );
+        pLut->nFanins = nLeaves;
+        If_CutForEachLeaf( pMan, pCutBest, pLeaf, k )
+            pLut->pFanins[k] = Vec_IntEntry( vIfToAig, pLeaf->Id );
+        // compute the truth table
+        memcpy( pLut->pTruth, If_CutTruth(pCutBest), 4 * nWords );
+    }
+    assert( k == Vec_PtrSize(vMapping) );
+    Vec_IntFree( vIfToAig );
+    return vMapping;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntk_ManIf( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMapping;
+    If_Par_t Pars, * pPars = &Pars;
+    If_Man_t * pIfMan;
+    // perform FPGA mapping
+    Ntk_ManSetIfParsDefault( pPars );
+    pIfMan = Ntk_ManToIf( p, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+    // transform the result of mapping into the new network
+    vMapping = Ntk_ManFromIf( p, pIfMan );
+    If_ManStop( pIfMan );
+    if ( vMapping == NULL )
+        return NULL;
+    return vMapping;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 7c6ed069..d085b5e6 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -37,6 +37,8 @@ struct Ioa_ReadMod_t_
     Vec_Ptr_t *          vNames;       // .names lines
     Vec_Ptr_t *          vSubckts;     // .subckt lines
     Vec_Ptr_t *          vDelays;      // .delay lines
+    Vec_Ptr_t *          vArrivals;    // .input_arrival lines
+    Vec_Ptr_t *          vRequireds;   // .output_required lines
     int                  fBlackBox;    // indicates blackbox model
     // the resulting network
     Ntl_Mod_t *          pNtk;   
@@ -73,7 +75,7 @@ static Ioa_ReadMod_t *   Ioa_ReadModAlloc();
 static void              Ioa_ReadModFree( Ioa_ReadMod_t * p );
 static char *            Ioa_ReadLoadFile( char * pFileName );
 static void              Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
-static void              Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
+static int               Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
 static Ntl_Man_t *       Ioa_ReadParse( Ioa_ReadMan_t * p );
 static int               Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
@@ -81,6 +83,7 @@ static int               Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLi
 static int               Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
 static int               Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput );
 static int               Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
 
 static int               Ioa_ReadCharIsSpace( char s )   { return s == ' ' || s == '\t' || s == '\r' || s == '\n';             }
@@ -132,13 +135,22 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
     // prepare the file for parsing
     Ioa_ReadReadPreparse( p );
     // parse interfaces of each network
-    Ioa_ReadReadInterfaces( p );
+    if ( !Ioa_ReadReadInterfaces( p ) )
+    {
+        if ( p->sError[0] )
+            fprintf( stdout, "%s\n", p->sError );
+        Ioa_ReadFree( p );
+        return NULL;
+    }
     // construct the network
     pDesign = Ioa_ReadParse( p );
     if ( p->sError[0] )
         fprintf( stdout, "%s\n", p->sError );
     if ( pDesign == NULL )
+    {
+        Ioa_ReadFree( p );
         return NULL;
+    }
     p->pDesign = NULL;
     Ioa_ReadFree( p );
 // pDesign should be linked to all models of the design
@@ -248,6 +260,8 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
     p->vNames   = Vec_PtrAlloc( 512 );
     p->vSubckts = Vec_PtrAlloc( 512 );
     p->vDelays  = Vec_PtrAlloc( 512 );
+    p->vArrivals  = Vec_PtrAlloc( 512 );
+    p->vRequireds = Vec_PtrAlloc( 512 );
     return p;
 }
 
@@ -270,6 +284,8 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
     Vec_PtrFree( p->vNames );
     Vec_PtrFree( p->vSubckts );
     Vec_PtrFree( p->vDelays );
+    Vec_PtrFree( p->vArrivals );
+    Vec_PtrFree( p->vRequireds );
     free( p );
 }
 
@@ -498,6 +514,10 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             Vec_PtrPush( p->pLatest->vSubckts, pCur );
         else if ( !strncmp(pCur, "delay", 5) )
             Vec_PtrPush( p->pLatest->vDelays, pCur );
+        else if ( !strncmp(pCur, "input_arrival", 13) )
+            Vec_PtrPush( p->pLatest->vArrivals, pCur );
+        else if ( !strncmp(pCur, "output_required", 15) )
+            Vec_PtrPush( p->pLatest->vRequireds, pCur );
         else if ( !strncmp(pCur, "blackbox", 8) )
             p->pLatest->fBlackBox = 1;
         else if ( !strncmp(pCur, "model", 5) ) 
@@ -538,7 +558,7 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
+static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
 {
     Ioa_ReadMod_t * pMod;
     char * pLine;
@@ -548,20 +568,27 @@ static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
     {
         // parse the model
         if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
-            return;
+            return 0;
         // parse the inputs
         Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
             if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
-                return;
+                return 0;
         // parse the outputs
         Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
             if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
-                return;
+                return 0;
         // parse the delay info
         Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
             if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
-                return;
+                return 0;
+        Vec_PtrForEachEntry( pMod->vArrivals, pLine, k )
+            if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) )
+                return 0;
+        Vec_PtrForEachEntry( pMod->vRequireds, pLine, k )
+            if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) )
+                return 0;
     }
+    return 1;
 }
 
 
@@ -626,7 +653,7 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
     assert( !strcmp(pToken, "model") );
     if ( Vec_PtrSize(vTokens) != 2 )
     {
-        sprintf( p->pMan->sError, "Line %d: Model line has %d entries while it should have 2.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+        sprintf( p->pMan->sError, "Line %d: The number of entries in .model line (%d) is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
         return 0;
     }
     p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
@@ -866,7 +893,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     int RetValue1, RetValue2, Number1, Number2, Temp;
-    char * pToken;
+    char * pToken, * pTokenNum;
     float Delay;
     assert( sizeof(float) == sizeof(int) );
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
@@ -878,8 +905,9 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
         return 0;
     }
     // find the delay number
-    Delay = atof( Vec_PtrEntryLast(vTokens) );
-    if ( Delay < 0.0 )
+    pTokenNum = Vec_PtrEntryLast(vTokens);
+    Delay = atof( pTokenNum );
+    if ( Delay == 0.0 && pTokenNum[0] != '0' )
     {
         sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
         return 0;
@@ -927,6 +955,80 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Parses the subckt line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    int RetValue, Number;
+    char * pToken, * pTokenNum;
+    float Delay;
+    assert( sizeof(float) == sizeof(int) );
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry(vTokens,0);
+    if ( fOutput )
+        assert( !strcmp(pToken, "output_required") );
+    else
+        assert( !strcmp(pToken, "input_arrival") );
+    if ( Vec_PtrSize(vTokens) != 3 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (3).", Ioa_ReadGetLine(p->pMan, pToken) );
+        return 0;
+    }
+    // find the delay number
+    pTokenNum = Vec_PtrEntryLast(vTokens);
+    if ( !strcmp( pTokenNum, "-inf" ) )
+        Delay = -AIG_INFINITY;
+    else if ( !strcmp( pTokenNum, "inf" ) ) 
+        Delay = AIG_INFINITY;
+    else
+        Delay = atof( pTokenNum );
+    if ( Delay == 0.0 && pTokenNum[0] != '0' )
+    {
+        sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
+        return 0;
+    }
+    // find the PI/PO numbers
+    if ( fOutput )
+    {
+        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
+        if ( RetValue == 0 )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+            return 0;
+        }
+        // store the values
+        if ( p->pNtk->vRequireds == NULL )
+            p->pNtk->vRequireds = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vRequireds, Number );
+        Vec_IntPush( p->pNtk->vRequireds, Aig_Float2Int(Delay) );        
+    }
+    else
+    {
+        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
+        if ( RetValue == 0 )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+            return 0;
+        }
+        // store the values
+        if ( p->pNtk->vArrivals == NULL )
+            p->pNtk->vArrivals = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vArrivals, Number );
+        Vec_IntPush( p->pNtk->vArrivals, Aig_Float2Int(Delay) );        
+    }
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
new file mode 100644
index 00000000..d4bd1375
--- /dev/null
+++ b/src/aig/ntl/ntlTime.c
@@ -0,0 +1,134 @@
+/**CFile****************************************************************
+
+  FileName    [ntlTime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Creates timing manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlTime.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float * Ntl_ManCreateDelayTable( Vec_Int_t * vDelays, int nIns, int nOuts )
+{
+    float * pDelayTable, Delay;
+    int iIn, iOut, i, k;
+    assert( Vec_IntSize(vDelays) % 3 == 0 );
+    pDelayTable = ALLOC( float, nIns * nOuts );
+    memset( pDelayTable, 0, sizeof(float) * nIns * nOuts );
+    Vec_IntForEachEntry( vDelays, iIn, i )
+    {
+        iOut = Vec_IntEntry(vDelays, ++i);
+        Delay = Aig_Int2Float( Vec_IntEntry(vDelays, ++i) );
+        if ( iIn == -1 && iOut == -1 )
+            for ( k = 0; k < nIns * nOuts; k++ )
+                pDelayTable[k] = Delay;
+        else if ( iIn == -1 )
+            for ( k = 0; k < nIns; k++ )
+                pDelayTable[iOut * nIns + k] = Delay;
+        else if ( iOut == -1 )
+            for ( k = 0; k < nOuts; k++ )
+                pDelayTable[k * nIns + iIn] = Delay;
+        else 
+            pDelayTable[iOut * nIns + iIn] = Delay;
+    }
+    return pDelayTable;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_TMan_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
+{
+    Aig_TMan_t * pMan;
+    Vec_Ptr_t * vDelayTables;
+    Ntl_Mod_t * pRoot, * pModel;
+    Ntl_Obj_t * pObj;
+    int i, curPi, curPo, Entry;
+    assert( p->pAig != NULL );
+    // start the timing manager
+    pMan = Aig_TManStart( 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 )
+        Aig_TManInitPiArrival( pMan, i, 0.0 );
+    // unpack the data in the arrival times
+    if ( pRoot->vArrivals )
+        Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
+            Aig_TManInitPiArrival( 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 )
+        Aig_TManInitPoRequired( pMan, i, AIG_INFINITY );
+    // unpack the data in the required times
+    if ( pRoot->vRequireds )
+        Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
+            Aig_TManInitPoRequired( pMan, Entry, Vec_IntEntry(pRoot->vRequireds,++i) );
+    // derive timing tables
+    vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
+    Ntl_ManForEachModel( p, pModel, i )
+    {
+        if ( pModel->vDelays )
+            pModel->pDelayTable = Ntl_ManCreateDelayTable( pModel->vDelays, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) );
+        Vec_PtrPush( vDelayTables, pModel->pDelayTable );
+    }
+    Aig_TManSetDelayTables( pMan, vDelayTables );
+    // set up the boxes
+    curPi = Ntl_ModelPiNum(pRoot);
+    curPo = Ntl_ModelPoNum(pRoot);
+    Ntl_ManForEachBox( p, pObj, i )
+    {
+        Aig_TManCreateBoxFirst( pMan, curPo, Ntl_ObjFanoutNum(pObj), curPi, Ntl_ObjFaninNum(pObj), pObj->pImplem->pDelayTable );
+        curPo += Ntl_ObjFanoutNum(pObj);
+        curPi += Ntl_ObjFaninNum(pObj);
+    }
+    // forget refs to the delay tables in the network
+    Ntl_ManForEachModel( p, pModel, i )
+        pModel->pDelayTable = NULL;
+    return pMan;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+