Integration of timing manager.

5 files changed, 138 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e868866e..f87a88fa 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -826,7 +826,7 @@ extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnomalize( Gia_Man_t * p );
-extern Gia_Man_t *         Gia_ManDupWithHierarchy( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes );
 extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue );
 extern Gia_Man_t *         Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 9958f155..48204e8b 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -701,13 +701,14 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
 
     if ( fHieOnly )
     {
-        Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
+//        Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
         if ( Abc_FrameReadLibBox() == NULL )
             printf( "Cannot create TIM manager because box library is not available.\n" );
         else
         {
             Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs );
-            Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
+//            Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
+            printf( "Created timing manager using Tim_ManCreate().\n" );
         }
     }
     Vec_FltFreeP( &pNew->vInArrs );
@@ -1089,12 +1090,12 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
             fprintf( pFile, "i" );
             Gia_FileWriteBufferSize( pFile, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
             assert( Vec_FltSize(vArrTimes) == Tim_ManPiNum((Tim_Man_t *)p->pManTime) );
-            fwrite( Vec_FltArray(vArrTimes), 1, 4*Gia_ManPiNum(p), pFile );
+            fwrite( Vec_FltArray(vArrTimes), 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
 
             fprintf( pFile, "o" );
             Gia_FileWriteBufferSize( pFile, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
             assert( Vec_FltSize(vReqTimes) == Tim_ManPoNum((Tim_Man_t *)p->pManTime) );
-            fwrite( Vec_FltArray(vReqTimes), 1, 4*Gia_ManPoNum(p), pFile );
+            fwrite( Vec_FltArray(vReqTimes), 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
 
             Vec_FltFree( vArrTimes );
             Vec_FltFree( vReqTimes );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 50d1088f..bc1e59f6 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1182,11 +1182,13 @@ Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p )
     curCo = 0;
     for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
     {
+//printf( "Box %d:\n", i );
         // add internal nodes
         for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
         {
             pObj = Gia_ManPo( p, curCo + k );
 //Gia_ObjPrint( p, pObj );
+//printf( "Fanin " );
 //Gia_ObjPrint( p, Gia_ObjFanin0(pObj) );
             Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes );
         }
@@ -1201,7 +1203,9 @@ Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p )
         for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
         {
             pObj = Gia_ManPi( p, curCi + k );
+//Gia_ObjPrint( p, pObj );
             Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+            Gia_ObjSetTravIdCurrent( p, pObj );
         }
         curCi += Tim_ManBoxOutputNum(pTime, i);
     }
@@ -1236,7 +1240,7 @@ Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p )
+Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes )
 {
     Vec_Int_t * vNodes;
     Gia_Man_t * pNew;
@@ -1260,7 +1264,10 @@ Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p )
         else assert( 0 );
     }
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
-    Vec_IntFree( vNodes );
+    if ( pvNodes )
+        *pvNodes = vNodes;
+    else
+        Vec_IntFree( vNodes );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 64cc7cf7..19c2fe0b 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -594,8 +594,8 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
     pNew->nOffset = iOffset;
     Gia_ManCleanMark0( pNew );
 //    assert( iOffset == Gia_ManObjNum(pNew) + nItems );
-    if ( pIfMan->pManTim )
-        pNew->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+//    if ( pIfMan->pManTim )
+//        pNew->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
     // verify that COs have mapping
     {
         Gia_Obj_t * pObj;
@@ -610,6 +610,110 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManMappingVerify_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Id, iFan, k, Result = 1;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return 1;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( !Gia_ObjIsAnd(pObj) )
+        return 1;
+    if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pObj)) )
+    {
+        Abc_Print( -1, "Gia_ManMappingVerify: Internal node %d does not have mapping.\n", Gia_ObjId(p, pObj) );
+        return 0;
+    }
+    Id = Gia_ObjId(p, pObj);
+    Gia_LutForEachFanin( p, Id, iFan, k )
+        if ( Result )
+            Result &= Gia_ManMappingVerify_rec( p, Gia_ManObj(p, iFan) );
+    return Result;
+}
+void Gia_ManMappingVerify( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj, * pFanin;
+    int i, Result = 1;
+/*
+    if ( p->pMapping )
+    {
+        assert( p->nOffset != 0 );
+        Vec_IntFreeP( p->vMapping );
+        Vec_IntAlloc( p->vMapping, p->nOffset );
+        memmove( Vec_IntArray(p->vMapping), p->pMapping, p->nOffset );
+    }
+    assert( p->vMapping );
+*/
+    assert( p->pMapping );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        pFanin = Gia_ObjFanin0(pObj);
+        if ( !Gia_ObjIsAnd(pFanin) )
+            continue;
+        if ( !Gia_ObjIsLut(p, Gia_ObjId(p, pFanin)) )
+        {
+            Abc_Print( -1, "Gia_ManMappingVerify: CO driver %d does not have mapping.\n", Gia_ObjId(p, pFanin) );
+            Result = 0;
+            continue;
+        }
+        Result &= Gia_ManMappingVerify_rec( p, pFanin );
+    }
+//    if ( Result && Gia_NtkIsRoot(p) )
+//        Abc_Print( 1, "Mapping verified correctly.\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers mapping from hie GIA to normalized GIA.]
+
+  Description [Hie GIA (pGia) points to normalized GIA (p).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, k, iFan;
+    assert( pGia->pMapping != NULL );
+    Gia_ManMappingVerify( pGia );
+    Vec_IntFreeP( &p->vMapping );
+    p->vMapping = Vec_IntAlloc( 2 * Gia_ManObjNum(p) );
+    Vec_IntFill( p->vMapping, Gia_ManObjNum(p), 0 );
+    Gia_ManForEachLut( pGia, i )
+    {
+        assert( !Abc_LitIsCompl(Gia_ObjValue(Gia_ManObj(pGia, i))) );
+        pObj = Gia_ManObj( p, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, i))) );
+        Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
+        Vec_IntPush( p->vMapping, Gia_ObjLutSize(pGia, i) );
+        Gia_LutForEachFanin( pGia, i, iFan, k )
+            Vec_IntPush( p->vMapping, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, iFan))) );
+        Vec_IntPush( p->vMapping, Gia_ObjId(p, pObj) );
+    }
+    // create standard mapping
+    assert( p->pMapping == NULL );
+    p->pMapping = Vec_IntArray( p->vMapping );
+    p->vMapping->pArray = NULL;
+    p->nOffset = Vec_IntSize(p->vMapping);
+    p->vMapping->nSize = 0;
+    Gia_ManMappingVerify( p );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Interface of LUT mapping package.]
 
   Description []
@@ -624,15 +728,20 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     Gia_Man_t * pNew;
     If_Man_t * pIfMan;
     If_Par_t * pPars = (If_Par_t *)pp;
+    Vec_Int_t * vNodes = NULL;
     // reconstruct GIA according to the hierarchy manager
     if ( p->pManTime )
-        p = Gia_ManDupWithHierarchy( p );
+    {
+        pNew = Gia_ManDupWithHierarchy( p, &vNodes );
+        pNew->pManTime = p->pManTime; p->pManTime = NULL;
+        p = pNew;
+    }
     else 
         p = Gia_ManDup( p );
+    Vec_IntFreeP( &vNodes );
     // set the arrival times
     assert( pPars->pTimesArr == NULL );
-    pPars->pTimesArr = ABC_ALLOC( float, Gia_ManCiNum(p) );
-    memset( pPars->pTimesArr, 0, sizeof(float) * Gia_ManCiNum(p) );
+    pPars->pTimesArr = ABC_CALLOC( float, Gia_ManCiNum(p) );
     // translate into the mapper
     pIfMan = Gia_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
@@ -659,7 +768,14 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     // unmap in case of SOP balancing
 //    if ( pIfMan->pPars->fDelayOpt )
 //        Vec_IntFreeP( &pNew->vMapping );
-    return pNew;
+    // return the original (unmodified by the mapper) timing manager
+    pNew->pManTime = p->pManTime; p->pManTime = NULL;
+    Gia_ManStop( p );
+    // normalize and transfer mapping
+    p = Gia_ManDupNormalize( pNew );
+    Gia_ManTransferMapping( pNew, p );
+    Gia_ManStop( pNew );
+    return p;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 60581e8e..8900fda4 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -195,6 +195,7 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t *
     int i, k;
     assert( p->vDelayTables == NULL );
     p->vDelayTables = Vec_PtrStart( Vec_PtrSize(pLibBox->vBoxes) );
+    if ( p->vBoxes )
     Tim_ManForEachBox( p, pBox, i )
     {
         if ( pBox->iDelayTable == -1 )