From 4ff5203f4c8b341eb717b742bf1af51f64f31ccd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 5 Mar 2013 13:13:15 -0800 Subject: Improvements to the hierarchy/timing manager. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaAiger.c | 23 ++++++------- src/aig/gia/giaIf.c | 11 ++++--- src/aig/gia/giaSweep.c | 2 +- src/aig/gia/giaTim.c | 82 +++++++++++++++++++++++++++++++++++------------ src/base/abc/abc.h | 1 + src/base/abci/abcIf.c | 2 +- src/base/abci/abcTiming.c | 25 ++++++++------- src/base/io/ioWriteBlif.c | 2 ++ src/map/if/if.h | 3 +- src/map/if/ifCore.c | 2 +- src/map/if/ifLibBox.c | 8 ++--- src/map/if/ifMan.c | 6 ++-- src/map/if/ifSeq.c | 1 + src/map/if/ifUtil.c | 14 +++++--- src/misc/tim/tim.h | 5 ++- src/misc/tim/timBox.c | 17 ++++++++++ src/misc/tim/timInt.h | 1 + src/misc/tim/timMan.c | 75 ++++++++++++++++++++++++++++++++----------- src/proof/llb/llb4Map.c | 2 +- 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, "# \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 @@ -211,6 +211,23 @@ float * Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox ) return pTable; } +/**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.] 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 ); -- cgit v1.2.3