Improvements to the hierarchy/timing manager.

20 files changed, 197 insertions, 87 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 )
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index eeda95a3..e5b57ec8 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -907,6 +907,7 @@ extern ABC_DLL void               Abc_ManTimeStop( Abc_ManTime_t * p );
 extern ABC_DLL void               Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
 extern ABC_DLL void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
 extern ABC_DLL float *            Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
+extern ABC_DLL float *            Abc_NtkGetCoRequiredFloats( Abc_Ntk_t * pNtk );
 extern ABC_DLL Abc_Time_t *       Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
 extern ABC_DLL Abc_Time_t *       Abc_NtkGetCoRequiredTimes( Abc_Ntk_t * pNtk );
 extern ABC_DLL float              Abc_NtkDelayTrace( Abc_Ntk_t * pNtk, Abc_Obj_t * pOut, Abc_Obj_t * pIn, int fPrint );
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 315507c2..926f3e74 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -123,7 +123,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 
     // get timing information
     pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
-    pPars->pTimesReq = NULL;
+    pPars->pTimesReq = Abc_NtkGetCoRequiredFloats(pNtk);
 
     // set the latch paths
     if ( pPars->fLatchPaths && pPars->pTimesArr )
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 87c0e2b3..ce05e83e 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -557,18 +557,6 @@ Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk )
         p[i] = *Abc_NodeArrival(pNode);
     return p;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the CI node levels according to the arrival info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 Abc_Time_t * Abc_NtkGetCoRequiredTimes( Abc_Ntk_t * pNtk )
 {
     Abc_Time_t * p;
@@ -608,6 +596,19 @@ float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk )
         p[i] = Abc_NodeArrival(pNode)->Worst;
     return p;
 }
+float * Abc_NtkGetCoRequiredFloats( Abc_Ntk_t * pNtk )
+{
+    float * p;
+    Abc_Obj_t * pNode;
+    int i;
+    if ( pNtk->pManTime == NULL )
+        return NULL;
+    // set the PO required times
+    p = ABC_CALLOC( float, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        p[i] = Abc_NodeRequired(pNode)->Worst;
+    return p;
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 7cc0d696..692ec3bb 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -712,6 +712,8 @@ void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk )
             continue;
         fprintf( pFile, ".output_required %s %g %g\n", Abc_ObjName(Abc_ObjFanin0(pNode)), pTime->Rise, pTime->Fall );
     }
+
+    fprintf( pFile, "\n" );
 }
 
 
diff --git a/src/map/if/if.h b/src/map/if/if.h
index bdc505be..e8a4c604 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -193,6 +193,7 @@ struct If_Man_t_
     int                pPerm[3][IF_MAX_LUTSIZE]; // permutations
     unsigned           uSharedMask;   // mask of shared variables
     int                nShared;       // the number of shared variables
+    int                fReqTimeWarn;  // warning about exceeding required times was printed
     // SOP balancing
     Vec_Int_t *        vCover;        // used to compute ISOP
     Vec_Wrd_t *        vAnds;         // intermediate storage
@@ -318,7 +319,7 @@ struct If_Box_t_
 {
     char *             pName;
     int                Id;
-    int                fWhite;
+    int                fBlack;
     int                nPis;
     int                nPos;
     int *              pDelays;
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index afaccfe9..95dc03bf 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -86,7 +86,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
     // set arrival times and fanout estimates
     If_ManForEachCi( p, pObj, i )
     {
-        If_ObjSetArrTime( pObj, p->pPars->pTimesArr[i] );
+        If_ObjSetArrTime( pObj, p->pPars->pTimesArr ? p->pPars->pTimesArr[i] : (float)0.0 );
         pObj->EstRefs = (float)1.0;
     }
 
diff --git a/src/map/if/ifLibBox.c b/src/map/if/ifLibBox.c
index 8d7cb33b..042cb7f1 100644
--- a/src/map/if/ifLibBox.c
+++ b/src/map/if/ifLibBox.c
@@ -45,13 +45,13 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-If_Box_t * If_BoxStart( char * pName, int Id, int fWhite, int nPis, int nPos )
+If_Box_t * If_BoxStart( char * pName, int Id, int fBlack, int nPis, int nPos )
 {
     If_Box_t * p;
     p = ABC_CALLOC( If_Box_t, 1 );
     p->pName   = pName; // consumes memory
     p->Id      = Id;
-    p->fWhite  = fWhite;
+    p->fBlack  = fBlack;
     p->nPis    = nPis;
     p->nPos    = nPos;
     p->pDelays = ABC_CALLOC( int, nPis * nPos );
@@ -202,7 +202,7 @@ If_LibBox_t * If_LibBoxRead( char * pFileName )
         pToken = If_LibBoxGetToken( pFile );
         nPos   = atoi( pToken );
         // create box
-        pBox   = If_BoxStart( pName, Id, fWhite, nPis, nPos );
+        pBox   = If_BoxStart( pName, Id, !fWhite, nPis, nPos );
         If_LibBoxAdd( p, pBox );
         // read the table
         for ( i = 0; i < nPis * nPos; i++ )
@@ -224,7 +224,7 @@ void If_LibBoxPrint( FILE * pFile, If_LibBox_t * p )
     fprintf( pFile, "# <Name> <ID> <Type> <I> <O>\n" );
     If_LibBoxForEachBox( p, pBox, i )
     {
-        fprintf( pFile, "%s %d %d %d %d\n", pBox->pName, pBox->Id, pBox->fWhite, pBox->nPis, pBox->nPos );
+        fprintf( pFile, "%s %d %d %d %d\n", pBox->pName, pBox->Id, !pBox->fBlack, pBox->nPis, pBox->nPos );
         for ( j = 0; j < pBox->nPos; j++, printf("\n") )
             for ( k = 0; k < pBox->nPis; k++ )
                 if ( pBox->pDelays[j * pBox->nPis + k] == -1 )
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 9f9e360e..b0a70a32 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -189,10 +189,8 @@ void If_ManStop( If_Man_t * p )
     ABC_FREE( p->puTemp[0] );
     ABC_FREE( p->pCutTemp );
     // free pars memory
-    if ( p->pPars->pTimesArr )
-        ABC_FREE( p->pPars->pTimesArr );
-    if ( p->pPars->pTimesReq )
-        ABC_FREE( p->pPars->pTimesReq );
+    ABC_FREE( p->pPars->pTimesArr );
+    ABC_FREE( p->pPars->pTimesReq );
     if ( p->pManTim )
         Tim_ManStop( p->pManTim );
     if ( p->vSwitching )
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index 37c98f0d..d6037ce8 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -294,6 +294,7 @@ void If_ManPerformMappingSeqPost( If_Man_t * p )
 {
     If_Obj_t * pObjLi, * pObjLo, * pObj;
     int i;
+    assert( 0 );
 
     // set arrival times
     assert( p->pPars->pTimesArr != NULL );
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index b8b03d70..efc6fba3 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -156,23 +156,27 @@ void If_ManComputeRequired( If_Man_t * p )
     if ( p->pManTim == NULL )
     {
         // consider the case when the required times are given
-        if ( p->pPars->pTimesReq )
+        if ( p->pPars->pTimesReq && !p->pPars->fAreaOnly )
         {
-            assert( !p->pPars->fAreaOnly );
             // make sure that the required time hold
             Counter = 0;
             If_ManForEachCo( p, pObj, i )
             {
                 if ( If_ObjArrTime(If_ObjFanin0(pObj)) > p->pPars->pTimesReq[i] + p->fEpsilon )
                 {
+                    If_ObjFanin0(pObj)->Required = If_ObjArrTime(If_ObjFanin0(pObj));
                     Counter++;
     //                Abc_Print( 0, "Required times are violated for output %d (arr = %d; req = %d).\n", 
     //                    i, (int)If_ObjArrTime(If_ObjFanin0(pObj)), (int)p->pPars->pTimesReq[i] );
                 }
-                If_ObjFanin0(pObj)->Required = p->pPars->pTimesReq[i];
+                else
+                    If_ObjFanin0(pObj)->Required = p->pPars->pTimesReq[i];
+            }
+            if ( Counter && !p->fReqTimeWarn )
+            {
+                Abc_Print( 0, "Required times are exceeded at %d output%s. The earliest arrival times are used.\n", Counter, Counter > 1 ? "s":"" );
+                p->fReqTimeWarn = 1;
             }
-            if ( Counter )
-                Abc_Print( 0, "Required times are violated for %d outputs.\n", Counter );
         }
         else
         {
diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h
index b2303c21..df787748 100644
--- a/src/misc/tim/tim.h
+++ b/src/misc/tim/tim.h
@@ -119,6 +119,7 @@ extern int             Tim_ManBoxInputNum( Tim_Man_t * p, int iBox );
 extern int             Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox );
 extern int             Tim_ManBoxDelayTableId( Tim_Man_t * p, int iBox );
 extern float *         Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox );
+extern int             Tim_ManBoxIsBlack( Tim_Man_t * p, int iBox );
 extern int             Tim_ManBoxCopy( Tim_Man_t * p, int iBox );
 extern void            Tim_ManBoxSetCopy( Tim_Man_t * p, int iBox, int iCopy );
 extern int             Tim_ManBoxFindFromCiNum( Tim_Man_t * p, int iCiNum );
@@ -129,8 +130,10 @@ extern Tim_Man_t *     Tim_ManLoad( Vec_Str_t * p, int fHieOnly );
 extern Tim_Man_t *     Tim_ManStart( int nCis, int nCos );
 extern Tim_Man_t *     Tim_ManDup( Tim_Man_t * p, int fUnitDelay );
 extern Tim_Man_t *     Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres );
+extern Vec_Int_t *     Tim_ManAlignTwo( Tim_Man_t * pSpec, Tim_Man_t * pImpl );
 extern void            Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * vOutReqs );
-extern int             Tim_ManGetArrsReqs( Tim_Man_t * p, Vec_Flt_t ** pvInArrs, Vec_Flt_t ** pvOutReqs );
+extern float *         Tim_ManGetArrTimes( Tim_Man_t * p );
+extern float *         Tim_ManGetReqTimes( Tim_Man_t * p );
 extern void            Tim_ManStop( Tim_Man_t * p );
 extern void            Tim_ManStopP( Tim_Man_t ** p );
 extern void            Tim_ManPrint( Tim_Man_t * p );
diff --git a/src/misc/tim/timBox.c b/src/misc/tim/timBox.c
index 5d29970e..bff7b39c 100644
--- a/src/misc/tim/timBox.c
+++ b/src/misc/tim/timBox.c
@@ -213,6 +213,23 @@ float * Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox )
 
 /**Function*************************************************************
 
+  Synopsis    [Return 1 if the box is black.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Tim_ManBoxIsBlack( Tim_Man_t * p, int iBox )
+{
+    return Tim_ManBox(p, iBox)->fBlack;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Returns the copy of the box.]
 
   Description []
diff --git a/src/misc/tim/timInt.h b/src/misc/tim/timInt.h
index 67312064..27881498 100644
--- a/src/misc/tim/timInt.h
+++ b/src/misc/tim/timInt.h
@@ -71,6 +71,7 @@ struct Tim_Box_t_
     int              nOutputs;       // the number of box outputs (PIs)
     int              iDelayTable;    // index of the delay table
     int              iCopy;          // copy of this box
+    int              fBlack;         // this is black box
     int              Inouts[0];      // the int numbers of PIs and POs
 };
 
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 4825ed71..51a0c381 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -234,6 +234,36 @@ Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Aligns two sets of boxes using the copy field.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Tim_ManAlignTwo( Tim_Man_t * pSpec, Tim_Man_t * pImpl )
+{
+    Vec_Int_t * vBoxPres;
+    Tim_Box_t * pBox;
+    int i;
+    assert( Tim_ManBoxNum(pSpec) > Tim_ManBoxNum(pImpl) );
+    // check if boxes of pImpl can be aligned
+    Tim_ManForEachBox( pImpl, pBox, i )
+        if ( pBox->iCopy < 0 || pBox->iCopy >= Tim_ManBoxNum(pSpec) ) 
+            return NULL;
+    // map dropped boxes into 1, others into 0
+    vBoxPres = Vec_IntStart( Tim_ManBoxNum(pSpec) );
+    Tim_ManForEachBox( pImpl, pBox, i )
+    {
+        assert( !Vec_IntEntry(vBoxPres, pBox->iCopy) );
+        Vec_IntWriteEntry( vBoxPres, pBox->iCopy, 1 );
+    }
+    return vBoxPres;
+}
 
 /**Function*************************************************************
 
@@ -306,6 +336,7 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t *
         assert( pIfBox != NULL );
         assert( pIfBox->nPis == pBox->nInputs );
         assert( pIfBox->nPos == pBox->nOutputs );
+        pBox->fBlack = pIfBox->fBlack;
         if ( Vec_PtrEntry( p->vDelayTables, pBox->iDelayTable ) != NULL )
             continue;
         // create table of boxes
@@ -349,33 +380,36 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t *
   SeeAlso     []
 
 ***********************************************************************/
-int Tim_ManGetArrsReqs( Tim_Man_t * p, Vec_Flt_t ** pvInArrs, Vec_Flt_t ** pvOutReqs )
+float * Tim_ManGetArrTimes( Tim_Man_t * p )
 {
+    float * pTimes;
     Tim_Obj_t * pObj;
-    int i, fTrivial = 1;
-    *pvInArrs = NULL;
-    *pvOutReqs = NULL;
+    int i;
     Tim_ManForEachPi( p, pObj, i )
         if ( pObj->timeArr != 0.0 )
-        {
-            fTrivial = 0;
             break;
-        }
+    if ( i == Tim_ManPiNum(p) )
+        return NULL;
+    pTimes  = ABC_ALLOC( float, Tim_ManPiNum(p) );
+    Tim_ManForEachPi( p, pObj, i )
+        pTimes[i] = pObj->timeArr;
+    return pTimes;
+}
+float * Tim_ManGetReqTimes( Tim_Man_t * p )
+{
+    float * pTimes;
+    Tim_Obj_t * pObj;
+    int i, k = 0;
     Tim_ManForEachPo( p, pObj, i )
         if ( pObj->timeReq != TIM_ETERNITY )
-        {
-            fTrivial = 0;
             break;
-        }
-    if ( fTrivial )
-        return 0;
-    *pvInArrs  = Vec_FltAlloc( Tim_ManPiNum(p) );
-    Tim_ManForEachPi( p, pObj, i )
-        Vec_FltPush( *pvInArrs, pObj->timeArr );
-    *pvOutReqs = Vec_FltAlloc( Tim_ManPoNum(p) );
+    if ( i == Tim_ManPoNum(p) )
+        return NULL;
+    pTimes  = ABC_ALLOC( float, Tim_ManPoNum(p) );
     Tim_ManForEachPo( p, pObj, i )
-        Vec_FltPush( *pvOutReqs, pObj->timeReq );
-    return 1;
+        pTimes[k++] = pObj->timeArr;
+    assert( k == Tim_ManPoNum(p) );
+    return pTimes;
 }
 
 
@@ -421,8 +455,11 @@ void Tim_ManPrint( Tim_Man_t * p )
     if ( i == Tim_ManCoNum(p) )
         printf( "All POs :  arr = %5.3f  req = %5.3f\n", pPrev->timeArr, pPrev->timeReq );
     else
+    {
+        int k = 0;
         Tim_ManForEachPo( p, pObj, i )
-            printf( "PO%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+            printf( "PO%5d :  arr = %5.3f  req = %5.3f\n", k++, pObj->timeArr, pObj->timeReq );
+    }
 
     // print box info
     if ( Tim_ManBoxNum(p) > 0 )
diff --git a/src/proof/llb/llb4Map.c b/src/proof/llb/llb4Map.c
index 4b46f308..4487ce25 100644
--- a/src/proof/llb/llb4Map.c
+++ b/src/proof/llb/llb4Map.c
@@ -68,7 +68,7 @@ Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin )
 
     // get timing information
     pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
-    pPars->pTimesReq = NULL;
+    pPars->pTimesReq = Abc_NtkGetCoRequiredFloats(pNtk);
 
     // perform LUT mapping
     pIfMan = Abc_NtkToIf( pNtk, pPars );