Improvements to the hierarchy/timing manager.

5 files changed, 82 insertions, 38 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6ba68a55..2083f8ea 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1019,7 +1019,7 @@ extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames,
 /*=== giaTim.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnormalize( Gia_Man_t * p );
-extern Gia_Man_t *         Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes );
+extern Gia_Man_t *         Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres );
 extern int                 Gia_ManLevelWithBoxes( Gia_Man_t * p );
 extern int                 Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit );
 extern void *              Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 29bcddfa..ee90784e 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1113,22 +1113,23 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     }
     if ( p->pManTime )
     {
-        Vec_Flt_t * vArrTimes, * vReqTimes;
-        if ( Tim_ManGetArrsReqs( (Tim_Man_t *)p->pManTime, &vArrTimes, &vReqTimes ) )
+        float * pTimes;
+        pTimes = Tim_ManGetArrTimes( p->pManTime );
+        if ( pTimes )
         {
             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*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
-
+            fwrite( pTimes, 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile );
+            ABC_FREE( pTimes );
+            if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
+        }
+        pTimes = Tim_ManGetReqTimes( p->pManTime );
+        if ( pTimes )
+        {
             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*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
-
-            Vec_FltFree( vArrTimes );
-            Vec_FltFree( vReqTimes );
-            if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
+            fwrite( pTimes, 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile );
+            ABC_FREE( pTimes );
             if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
         }
     }
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 1d4373a3..dc16b886 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -82,7 +82,7 @@ void Gia_ManSetIfParsDefault( void * pp )
     p->fUseCoAttrs =  1;   // use CO attributes
     p->pLutLib     =  NULL;
     p->pTimesArr   =  NULL; 
-    p->pTimesArr   =  NULL;   
+    p->pTimesReq   =  NULL;   
     p->pFuncCost   =  NULL;   
 }
 
@@ -1143,8 +1143,11 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     If_Man_t * pIfMan;
     If_Par_t * pPars = (If_Par_t *)pp;
     // reconstruct GIA according to the hierarchy manager
+    assert( pPars->pTimesArr == NULL );
+    assert( pPars->pTimesReq == NULL );
     if ( p->pManTime )
     {
+        Vec_Flt_t * vArrTimes = NULL, * vReqTimes = NULL;
         pNew = Gia_ManDupUnnormalize( p );
         if ( pNew == NULL )
             return NULL;
@@ -1152,12 +1155,12 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
         pNew->pAigExtra  = p->pAigExtra;  p->pAigExtra = NULL;
         pNew->nAnd2Delay = p->nAnd2Delay; p->nAnd2Delay = 0;
         p = pNew;
+        // set arrival and required times
+        pPars->pTimesArr = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime );
+        pPars->pTimesReq = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime );
     }
     else 
         p = Gia_ManDup( p );
-    // set the arrival times
-    assert( pPars->pTimesArr == NULL );
-    pPars->pTimesArr = ABC_CALLOC( float, Gia_ManCiNum(p) );
     // translate into the mapper
     pIfMan = Gia_ManToIf( p, pPars );    
     if ( pIfMan == NULL )
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 4ef8725e..994aedc1 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -304,7 +304,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
         return NULL;
     // find global equivalences
     pNew->pManTime = p->pManTime;
-    pGia = Gia_ManDupCollapse( pNew, p->pAigExtra );
+    pGia = Gia_ManDupCollapse( pNew, p->pAigExtra, NULL );
     pNew->pManTime = NULL;
     Gia_ManFraigSweepPerform( pGia, pPars );
     // transfer equivalences
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index e3841856..01601625 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -285,7 +285,7 @@ void Gia_ManDupCollapse_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew )
     if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) )
         pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value);        
 }
-Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes )
+Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres )
 {
     Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
     Gia_Man_t * pNew, * pTemp;
@@ -320,28 +320,46 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes )
         Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) );
         Gia_ManConst0(pBoxes)->Value = 0;
         // add internal nodes
-        for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+        if ( Tim_ManBoxIsBlack(pTime, i) )
         {
-            // build logic
-            pObj = Gia_ManPo( p, curCo + k );
-            Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
-            // transfer to the PI
-            pObjBox = Gia_ManPi( pBoxes, k );
-            pObjBox->Value = Gia_ObjFanin0Copy(pObj);
-            Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+            int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i));
+            for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+            {
+                pObj = Gia_ManPo( p, curCo + k );
+                Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
+                pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+            }
+            for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+            {
+                pObj = Gia_ManPi( p, curCi + k );
+                pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew);
+                Gia_ObjSetTravIdCurrent( p, pObj );
+            }
         }
-        curCo += Tim_ManBoxInputNum(pTime, i);
-        // add internal nodes
-        for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+        else
         {
-            // build logic
-            pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pTime) + k );
-            Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
-            // transfer to the PI
-            pObj = Gia_ManPi( p, curCi + k );
-            pObj->Value = Gia_ObjFanin0Copy(pObjBox);
-            Gia_ObjSetTravIdCurrent( p, pObj );
+            for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
+            {
+                // build logic
+                pObj = Gia_ManPo( p, curCo + k );
+                Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew );
+                // transfer to the PI
+                pObjBox = Gia_ManPi( pBoxes, k );
+                pObjBox->Value = Gia_ObjFanin0Copy(pObj);
+                Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+            }
+            for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ )
+            {
+                // build logic
+                pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pTime) + k );
+                Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew );
+                // transfer to the PI
+                pObj = Gia_ManPi( p, curCi + k );
+                pObj->Value = Gia_ObjFanin0Copy(pObjBox);
+                Gia_ObjSetTravIdCurrent( p, pObj );
+            }
         }
+        curCo += Tim_ManBoxInputNum(pTime, i);
         curCi += Tim_ManBoxOutputNum(pTime, i);
     }
     // add remaining nodes
@@ -481,6 +499,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
     int fVerbose =  1;
     int Status   = -1;
     Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter;
+    Vec_Int_t * vBoxPres = NULL;
     if ( pGia->pSpec == NULL )
     {
         printf( "Spec file is not given. Use standard flow.\n" );
@@ -508,8 +527,29 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
         printf( "Spec has no box logic. Use standard flow.\n" );
         return Status;
     }
-    pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra );
-    pGia1 = Gia_ManDupCollapse( pGia,  pGia->pAigExtra  );
+    // if timing managers have different number of black boxes,
+    // it is possible that some of the boxes are swept away
+    // but specification cannot have fewer boxes than implementation
+    if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) < Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+    {
+        printf( "Spec has more boxes than the design. Cannot proceed.\n" );
+        return Status;
+    }
+    // in this case, it is expected that the boxes can be aligned
+    // find what boxes of pSpec are dropped in pGia
+    if ( Tim_ManBoxNum( (Tim_Man_t *)pSpec->pManTime ) != Tim_ManBoxNum( (Tim_Man_t *)pGia->pManTime ) )
+    {
+        vBoxPres = Tim_ManAlignTwo( (Tim_Man_t *)pSpec->pManTime, (Tim_Man_t *)pGia->pManTime );
+        if ( vBoxPres == NULL )
+        {
+            printf( "Boxes of spec and design cannot be aligned. Cannot proceed.\n" );
+            return Status;
+        }
+    }
+    // collapse two designs
+    pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres );
+    pGia1 = Gia_ManDupCollapse( pGia,  pGia->pAigExtra,  NULL  );
+    Vec_IntFreeP( &vBoxPres );
     // compute the miter
     pMiter = Gia_ManMiter( pGia0, pGia1, 1, 0, fVerbose );
     if ( pMiter )