| /**CFile**************************************************************** |
| |
| FileName [giaTim.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Scalable AIG package.] |
| |
| Synopsis [Procedures with hierarchy/timing manager.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: giaTim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "gia.h" |
| #include "giaAig.h" |
| #include "misc/tim/tim.h" |
| #include "misc/extra/extra.h" |
| #include "proof/cec/cec.h" |
| #include "proof/fra/fra.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the number of boxes in the AIG with boxes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManBoxNum( Gia_Man_t * p ) |
| { |
| return p->pManTime ? Tim_ManBoxNum((Tim_Man_t *)p->pManTime) : 0; |
| } |
| int Gia_ManRegBoxNum( Gia_Man_t * p ) |
| { |
| return p->vRegClasses ? Vec_IntSize(p->vRegClasses) : 0; |
| } |
| int Gia_ManNonRegBoxNum( Gia_Man_t * p ) |
| { |
| return Gia_ManBoxNum(p) - Gia_ManRegBoxNum(p); |
| } |
| int Gia_ManBlackBoxNum( Gia_Man_t * p ) |
| { |
| return Tim_ManBlackBoxNum((Tim_Man_t *)p->pManTime); |
| } |
| int Gia_ManBoxCiNum( Gia_Man_t * p ) |
| { |
| return p->pManTime ? Gia_ManCiNum(p) - Tim_ManPiNum((Tim_Man_t *)p->pManTime) : 0; |
| } |
| int Gia_ManBoxCoNum( Gia_Man_t * p ) |
| { |
| return p->pManTime ? Gia_ManCoNum(p) - Tim_ManPoNum((Tim_Man_t *)p->pManTime) : 0; |
| } |
| int Gia_ManClockDomainNum( Gia_Man_t * p ) |
| { |
| int i, nDoms, Count = 0; |
| if ( p->vRegClasses == NULL ) |
| return 0; |
| nDoms = Vec_IntFindMax(p->vRegClasses); |
| assert( Vec_IntCountEntry(p->vRegClasses, 0) == 0 ); |
| for ( i = 1; i <= nDoms; i++ ) |
| if ( Vec_IntCountEntry(p->vRegClasses, i) > 0 ) |
| Count++; |
| return Count; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns one if this is a seq AIG with non-trivial boxes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManIsSeqWithBoxes( Gia_Man_t * p ) |
| { |
| return (Gia_ManRegNum(p) > 0 && Gia_ManBoxNum(p) > 0); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Makes sure the manager is normalized.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManIsNormalized( Gia_Man_t * p ) |
| { |
| int i, nOffset; |
| nOffset = 1; |
| for ( i = 0; i < Gia_ManCiNum(p); i++ ) |
| if ( !Gia_ObjIsCi( Gia_ManObj(p, nOffset+i) ) ) |
| return 0; |
| nOffset = 1 + Gia_ManCiNum(p) + Gia_ManAndNum(p); |
| for ( i = 0; i < Gia_ManCoNum(p); i++ ) |
| if ( !Gia_ObjIsCo( Gia_ManObj(p, nOffset+i) ) ) |
| return 0; |
| return 1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates AIG in the DFS order while putting CIs first.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p, int fHashMapping ) |
| { |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int i; |
| Gia_ManFillValue( p ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| if ( !Gia_ManIsSeqWithBoxes(p) ) |
| { |
| Gia_ManForEachCi( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCi(pNew); |
| } |
| else |
| { |
| // current CI order: PIs + FOs + NewCIs |
| // desired reorder: PIs + NewCIs + FOs |
| int nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime ); |
| int nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime ); |
| int nPis = nCIs - Gia_ManRegNum(p); |
| assert( nAll == Gia_ManCiNum(p) ); |
| assert( nPis > 0 ); |
| // copy PIs first |
| for ( i = 0; i < nPis; i++ ) |
| Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew); |
| // copy new CIs second |
| for ( i = nCIs; i < nAll; i++ ) |
| Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew); |
| // copy flops last |
| for ( i = nCIs - Gia_ManRegNum(p); i < nCIs; i++ ) |
| Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew); |
| printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" ); |
| } |
| if ( fHashMapping ) Gia_ManHashAlloc( pNew ); |
| Gia_ManForEachAnd( p, pObj, i ) |
| if ( Gia_ObjIsBuf(pObj) ) |
| pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); |
| else if ( fHashMapping ) |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| else |
| pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| if ( fHashMapping ) Gia_ManHashStop( pNew ); |
| Gia_ManForEachCo( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| pNew->nConstrs = p->nConstrs; |
| assert( Gia_ManIsNormalized(pNew) ); |
| Gia_ManDupRemapEquiv( pNew, p ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reorders flops for sequential AIGs with boxes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p ) |
| { |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int i, nCIs, nAll, nPis; |
| // sanity checks |
| assert( Gia_ManIsNormalized(p) ); |
| assert( Gia_ManIsSeqWithBoxes(p) ); |
| Gia_ManFillValue( p ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| Gia_ManConst0(p)->Value = 0; |
| // change input order |
| // desired reorder: PIs + NewCIs + FOs |
| // current CI order: PIs + FOs + NewCIs |
| nCIs = Tim_ManPiNum( (Tim_Man_t *)p->pManTime ); |
| nAll = Tim_ManCiNum( (Tim_Man_t *)p->pManTime ); |
| nPis = nCIs - Gia_ManRegNum(p); |
| assert( nAll == Gia_ManCiNum(p) ); |
| assert( nPis > 0 ); |
| // copy PIs first |
| for ( i = 0; i < nPis; i++ ) |
| Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew); |
| // copy flops second |
| for ( i = nAll - Gia_ManRegNum(p); i < nAll; i++ ) |
| Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew); |
| // copy new CIs last |
| for ( i = nPis; i < nAll - Gia_ManRegNum(p); i++ ) |
| Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew); |
| printf( "Warning: Unshuffled CI order to be correct AIG with boxes.\n" ); |
| // other things |
| Gia_ManForEachAnd( p, pObj, i ) |
| pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| Gia_ManForEachCo( p, pObj, i ) |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| pNew->nConstrs = p->nConstrs; |
| assert( Gia_ManIsNormalized(pNew) ); |
| Gia_ManDupRemapEquiv( pNew, p ); |
| return pNew; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find the ordering of AIG objects.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManOrderWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) |
| { |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) |
| return 0; |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| if ( Gia_ObjIsCi(pObj) ) |
| { |
| p->iData2 = Gia_ObjCioId(pObj); |
| return 1; |
| } |
| assert( Gia_ObjIsAnd(pObj) ); |
| if ( Gia_ObjIsBuf(pObj) ) |
| { |
| if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) ) |
| return 1; |
| Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); |
| return 0; |
| } |
| if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) ) |
| if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), vNodes ) ) |
| return 1; |
| if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) ) |
| return 1; |
| if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin1(pObj), vNodes ) ) |
| return 1; |
| Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); |
| return 0; |
| } |
| Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p ) |
| { |
| Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; |
| Vec_Int_t * vNodes; |
| Gia_Obj_t * pObj; |
| int i, k, curCi, curCo; |
| assert( pManTime != NULL ); |
| assert( Gia_ManIsNormalized( p ) ); |
| // start trav IDs |
| Gia_ManIncrementTravId( p ); |
| // start the array |
| vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); |
| // include constant |
| Vec_IntPush( vNodes, 0 ); |
| Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); |
| // include primary inputs |
| for ( i = 0; i < Tim_ManPiNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCi( p, i ); |
| Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| assert( Gia_ObjId(p, pObj) == i+1 ); |
| } |
| // for each box, include box nodes |
| curCi = Tim_ManPiNum(pManTime); |
| curCo = 0; |
| for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) |
| { |
| // add internal nodes |
| for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ ) |
| { |
| pObj = Gia_ManCo( p, curCo + k ); |
| if ( Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ) ) |
| { |
| int iCiNum = p->iData2; |
| int iBoxNum = Tim_ManBoxFindFromCiNum( pManTime, iCiNum ); |
| printf( "The command has to terminate. Boxes are not in a topological order.\n" ); |
| printf( "The following information may help debugging (numbers are 0-based):\n" ); |
| printf( "Input %d of BoxA %d (1stCI = %d; 1stCO = %d) has TFI with CI %d,\n", |
| k, i, Tim_ManBoxOutputFirst(pManTime, i), Tim_ManBoxInputFirst(pManTime, i), iCiNum ); |
| printf( "which corresponds to output %d of BoxB %d (1stCI = %d; 1stCO = %d).\n", |
| iCiNum - Tim_ManBoxOutputFirst(pManTime, iBoxNum), iBoxNum, |
| Tim_ManBoxOutputFirst(pManTime, iBoxNum), Tim_ManBoxInputFirst(pManTime, iBoxNum) ); |
| printf( "In a correct topological order, BoxB should precede BoxA.\n" ); |
| Vec_IntFree( vNodes ); |
| p->iData2 = 0; |
| return NULL; |
| } |
| } |
| // add POs corresponding to box inputs |
| for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ ) |
| { |
| pObj = Gia_ManCo( p, curCo + k ); |
| Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); |
| } |
| curCo += Tim_ManBoxInputNum(pManTime, i); |
| // add PIs corresponding to box outputs |
| for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ ) |
| { |
| pObj = Gia_ManCi( p, curCi + k ); |
| Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| } |
| curCi += Tim_ManBoxOutputNum(pManTime, i); |
| } |
| // add remaining nodes |
| for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCo( p, i ); |
| Gia_ManOrderWithBoxes_rec( p, Gia_ObjFanin0(pObj), vNodes ); |
| } |
| // add POs |
| for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCo( p, i ); |
| Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); |
| } |
| curCo += Tim_ManPoNum(pManTime); |
| // verify counts |
| assert( curCi == Gia_ManCiNum(p) ); |
| assert( curCo == Gia_ManCoNum(p) ); |
| //assert( Vec_IntSize(vNodes) == Gia_ManObjNum(p) ); |
| return vNodes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Duplicates AIG according to the timing manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p ) |
| { |
| Vec_Int_t * vNodes; |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int i; |
| assert( !Gia_ManBufNum(p) ); |
| vNodes = Gia_ManOrderWithBoxes( p ); |
| if ( vNodes == NULL ) |
| return NULL; |
| Gia_ManFillValue( p ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| if ( Gia_ManHasChoices(p) ) |
| pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) ); |
| Gia_ManForEachObjVec( vNodes, p, pObj, i ) |
| { |
| if ( Gia_ObjIsBuf(pObj) ) |
| pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); |
| else if ( Gia_ObjIsAnd(pObj) ) |
| { |
| pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) ) |
| pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))->Value); |
| } |
| else if ( Gia_ObjIsCi(pObj) ) |
| pObj->Value = Gia_ManAppendCi( pNew ); |
| else if ( Gia_ObjIsCo(pObj) ) |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| else if ( Gia_ObjIsConst0(pObj) ) |
| pObj->Value = 0; |
| else assert( 0 ); |
| } |
| Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); |
| Vec_IntFree( vNodes ); |
| return pNew; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Remaps the AIG from the old manager into the new manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManCleanupRemap( Gia_Man_t * p, Gia_Man_t * pGia ) |
| { |
| Gia_Obj_t * pObj, * pObjGia; |
| int i, iPrev; |
| Gia_ManForEachObj1( p, pObj, i ) |
| { |
| iPrev = Gia_ObjValue(pObj); |
| if ( iPrev == ~0 ) |
| continue; |
| pObjGia = Gia_ManObj( pGia, Abc_Lit2Var(iPrev) ); |
| if ( pObjGia->Value == ~0 ) |
| Gia_ObjSetValue( pObj, pObjGia->Value ); |
| else |
| Gia_ObjSetValue( pObj, Abc_LitNotCond(pObjGia->Value, Abc_LitIsCompl(iPrev)) ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes level with boxes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) |
| return 0; |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| if ( Gia_ObjIsCi(pObj) ) |
| return 1; |
| assert( Gia_ObjIsAnd(pObj) ); |
| if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) ) |
| Gia_ManLevelWithBoxes_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)) ); |
| if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) ) |
| return 1; |
| if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin1(pObj) ) ) |
| return 1; |
| Gia_ObjSetAndLevel( p, pObj ); |
| return 0; |
| } |
| int Gia_ManLevelWithBoxes( Gia_Man_t * p ) |
| { |
| int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1; |
| Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; |
| Gia_Obj_t * pObj, * pObjIn; |
| int i, k, j, curCi, curCo, LevelMax; |
| assert( Gia_ManRegNum(p) == 0 ); |
| assert( Gia_ManBufNum(p) == 0 ); |
| // copy const and real PIs |
| Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); |
| Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 ); |
| Gia_ManIncrementTravId( p ); |
| Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); |
| for ( i = 0; i < Tim_ManPiNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCi( p, i ); |
| Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay ); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| } |
| // create logic for each box |
| curCi = Tim_ManPiNum(pManTime); |
| curCo = 0; |
| for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) |
| { |
| int nBoxInputs = Tim_ManBoxInputNum( pManTime, i ); |
| int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i ); |
| float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i ); |
| // compute level for TFI of box inputs |
| for ( k = 0; k < nBoxInputs; k++ ) |
| { |
| pObj = Gia_ManCo( p, curCo + k ); |
| if ( Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) ) |
| { |
| printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" ); |
| return Gia_ManLevelNum( p ); |
| } |
| // set box input level |
| Gia_ObjSetCoLevel( p, pObj ); |
| } |
| // compute level for box outputs |
| for ( k = 0; k < nBoxOutputs; k++ ) |
| { |
| pObj = Gia_ManCi( p, curCi + k ); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| // evaluate delay of this output |
| LevelMax = 0; |
| assert( nBoxInputs == (int)pDelayTable[1] ); |
| for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ ) |
| if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY ) |
| LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) ); |
| // set box output level |
| Gia_ObjSetLevel( p, pObj, LevelMax ); |
| } |
| curCo += nBoxInputs; |
| curCi += nBoxOutputs; |
| } |
| // add remaining nodes |
| p->nLevels = 0; |
| for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCo( p, i ); |
| Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ); |
| Gia_ObjSetCoLevel( p, pObj ); |
| p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) ); |
| } |
| curCo += Tim_ManPoNum(pManTime); |
| // verify counts |
| assert( curCi == Gia_ManCiNum(p) ); |
| assert( curCo == Gia_ManCoNum(p) ); |
| // printf( "Max level is %d.\n", p->nLevels ); |
| return p->nLevels; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes level with boxes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManLutLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) |
| { |
| int iObj, k, iFan, Level = 0; |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) |
| return 0; |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| if ( Gia_ObjIsCi(pObj) ) |
| return 1; |
| assert( Gia_ObjIsAnd(pObj) ); |
| iObj = Gia_ObjId( p, pObj ); |
| Gia_LutForEachFanin( p, iObj, iFan, k ) |
| { |
| if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ManObj(p, iFan) ) ) |
| return 1; |
| Level = Abc_MaxInt( Level, Gia_ObjLevelId(p, iFan) ); |
| } |
| Gia_ObjSetLevelId( p, iObj, Level + 1 ); |
| return 0; |
| } |
| int Gia_ManLutLevelWithBoxes( Gia_Man_t * p ) |
| { |
| // int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1; |
| Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; |
| Gia_Obj_t * pObj, * pObjIn; |
| int i, k, j, curCi, curCo, LevelMax; |
| assert( Gia_ManRegNum(p) == 0 ); |
| if ( pManTime == NULL ) |
| return Gia_ManLutLevel(p, NULL); |
| // copy const and real PIs |
| Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); |
| Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 ); |
| Gia_ManIncrementTravId( p ); |
| Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); |
| for ( i = 0; i < Tim_ManPiNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCi( p, i ); |
| // Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay ); |
| Gia_ObjSetLevel( p, pObj, 0 ); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| } |
| // create logic for each box |
| curCi = Tim_ManPiNum(pManTime); |
| curCo = 0; |
| for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) |
| { |
| int nBoxInputs = Tim_ManBoxInputNum( pManTime, i ); |
| int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i ); |
| float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i ); |
| // compute level for TFI of box inputs |
| for ( k = 0; k < nBoxInputs; k++ ) |
| { |
| pObj = Gia_ManCo( p, curCo + k ); |
| if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) ) |
| { |
| printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" ); |
| return Gia_ManLevelNum( p ); |
| } |
| // set box input level |
| Gia_ObjSetCoLevel( p, pObj ); |
| } |
| // compute level for box outputs |
| for ( k = 0; k < nBoxOutputs; k++ ) |
| { |
| pObj = Gia_ManCi( p, curCi + k ); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| // evaluate delay of this output |
| LevelMax = 0; |
| assert( nBoxInputs == (int)pDelayTable[1] ); |
| for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManCo(p, curCo + j)); j++ ) |
| if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY ) |
| // LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) ); |
| LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + 1 ); |
| // set box output level |
| Gia_ObjSetLevel( p, pObj, LevelMax ); |
| } |
| curCo += nBoxInputs; |
| curCi += nBoxOutputs; |
| } |
| // add remaining nodes |
| p->nLevels = 0; |
| for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCo( p, i ); |
| Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ); |
| Gia_ObjSetCoLevel( p, pObj ); |
| p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) ); |
| } |
| curCo += Tim_ManPoNum(pManTime); |
| // verify counts |
| assert( curCi == Gia_ManCiNum(p) ); |
| assert( curCo == Gia_ManCoNum(p) ); |
| // printf( "Max level is %d.\n", p->nLevels ); |
| return p->nLevels; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Update hierarchy/timing manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres ) |
| { |
| Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; |
| assert( pManTime != NULL ); |
| assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) ); |
| return Tim_ManTrim( pManTime, vBoxPres ); |
| } |
| void * Gia_ManUpdateTimMan2( Gia_Man_t * p, Vec_Int_t * vBoxesLeft, int nTermsDiff ) |
| { |
| Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; |
| assert( pManTime != NULL ); |
| assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) ); |
| return Tim_ManReduce( pManTime, vBoxesLeft, nTermsDiff ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Update AIG of the holes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxPres ) |
| { |
| Gia_Man_t * pNew; |
| Tim_Man_t * pManTime = (Tim_Man_t *)pTime; |
| Vec_Int_t * vOutPres = Vec_IntAlloc( 100 ); |
| int i, k, curPo = 0; |
| assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(pManTime) ); |
| assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - Tim_ManPiNum(pManTime) ); |
| for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) |
| { |
| for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ ) |
| Vec_IntPush( vOutPres, Vec_IntEntry(vBoxPres, i) ); |
| curPo += Tim_ManBoxOutputNum(pManTime, i); |
| } |
| assert( curPo == Gia_ManCoNum(p) ); |
| pNew = Gia_ManDupOutputVec( p, vOutPres ); |
| Vec_IntFree( vOutPres ); |
| return pNew; |
| } |
| Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * p, Vec_Int_t * vBoxesLeft ) |
| { |
| Gia_Man_t * pNew; |
| Tim_Man_t * pManTime = (Tim_Man_t *)pTime; |
| int nRealPis = Tim_ManPiNum(pManTime); |
| Vec_Int_t * vOutsLeft = Vec_IntAlloc( 100 ); |
| int i, k, iBox, iOutFirst; |
| assert( Vec_IntSize(vBoxesLeft) <= Tim_ManBoxNum(pManTime) ); |
| assert( Gia_ManCoNum(p) == Tim_ManCiNum(pManTime) - nRealPis ); |
| Vec_IntForEachEntry( vBoxesLeft, iBox, i ) |
| { |
| iOutFirst = Tim_ManBoxOutputFirst(pManTime, iBox) - nRealPis; |
| for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, iBox); k++ ) |
| Vec_IntPush( vOutsLeft, iOutFirst + k ); |
| } |
| pNew = Gia_ManDupSelectedOutputs( p, vOutsLeft ); |
| Vec_IntFree( vOutsLeft ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Computes AIG with boxes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManDupCollapse_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew ) |
| { |
| if ( Gia_ObjIsTravIdCurrent(p, pObj) ) |
| return; |
| Gia_ObjSetTravIdCurrent(p, pObj); |
| assert( Gia_ObjIsAnd(pObj) ); |
| if ( Gia_ObjSibl(p, Gia_ObjId(p, pObj)) ) |
| Gia_ManDupCollapse_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)), pNew ); |
| Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew ); |
| Gia_ManDupCollapse_rec( p, Gia_ObjFanin1(pObj), pNew ); |
| // assert( !~pObj->Value ); |
| pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| 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, Vec_Int_t * vBoxPres, int fSeq ) |
| { |
| // this procedure assumes that sequential AIG with boxes is unshuffled to have valid boxes |
| Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; |
| Gia_Man_t * pNew, * pTemp; |
| Gia_Obj_t * pObj, * pObjBox; |
| int i, k, curCi, curCo, nBBins = 0, nBBouts = 0; |
| assert( !fSeq || p->vRegClasses ); |
| //assert( Gia_ManRegNum(p) == 0 ); |
| assert( Gia_ManCiNum(p) == Tim_ManPiNum(pManTime) + Gia_ManCoNum(pBoxes) ); |
| pNew = Gia_ManStart( Gia_ManObjNum(p) ); |
| pNew->pName = Abc_UtilStrsav( p->pName ); |
| pNew->pSpec = Abc_UtilStrsav( p->pSpec ); |
| if ( Gia_ManHasChoices(p) ) |
| pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) ); |
| Gia_ManHashAlloc( pNew ); |
| // copy const and real PIs |
| Gia_ManFillValue( p ); |
| Gia_ManConst0(p)->Value = 0; |
| Gia_ManIncrementTravId( p ); |
| Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); |
| for ( i = 0; i < Tim_ManPiNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCi( p, i ); |
| pObj->Value = Gia_ManAppendCi(pNew); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| } |
| // create logic for each box |
| curCi = Tim_ManPiNum(pManTime); |
| curCo = 0; |
| for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) |
| { |
| // clean boxes |
| Gia_ManIncrementTravId( pBoxes ); |
| Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) ); |
| Gia_ManConst0(pBoxes)->Value = 0; |
| // add internal nodes |
| //printf( "%d ", Tim_ManBoxIsBlack(pManTime, i) ); |
| if ( Tim_ManBoxIsBlack(pManTime, i) ) |
| { |
| int fSkip = (vBoxPres != NULL && !Vec_IntEntry(vBoxPres, i)); |
| for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ ) |
| { |
| pObj = Gia_ManCo( p, curCo + k ); |
| Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew ); |
| pObj->Value = fSkip ? -1 : Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| nBBouts++; |
| } |
| for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ ) |
| { |
| pObj = Gia_ManCi( p, curCi + k ); |
| pObj->Value = fSkip ? 0 : Gia_ManAppendCi(pNew); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| nBBins++; |
| } |
| } |
| else |
| { |
| for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ ) |
| { |
| // build logic |
| pObj = Gia_ManCo( p, curCo + k ); |
| Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew ); |
| // transfer to the PI |
| pObjBox = Gia_ManCi( pBoxes, k ); |
| pObjBox->Value = Gia_ObjFanin0Copy(pObj); |
| Gia_ObjSetTravIdCurrent( pBoxes, pObjBox ); |
| } |
| for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ ) |
| { |
| // build logic |
| pObjBox = Gia_ManCo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k ); |
| Gia_ManDupCollapse_rec( pBoxes, Gia_ObjFanin0(pObjBox), pNew ); |
| // transfer to the PI |
| pObj = Gia_ManCi( p, curCi + k ); |
| pObj->Value = Gia_ObjFanin0Copy(pObjBox); |
| Gia_ObjSetTravIdCurrent( p, pObj ); |
| } |
| } |
| curCo += Tim_ManBoxInputNum(pManTime, i); |
| curCi += Tim_ManBoxOutputNum(pManTime, i); |
| } |
| //printf( "\n" ); |
| // add remaining nodes |
| for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) |
| { |
| pObj = Gia_ManCo( p, i ); |
| Gia_ManDupCollapse_rec( p, Gia_ObjFanin0(pObj), pNew ); |
| pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); |
| } |
| curCo += Tim_ManPoNum(pManTime); |
| // verify counts |
| assert( curCi == Gia_ManCiNum(p) ); |
| assert( curCo == Gia_ManCoNum(p) ); |
| Gia_ManSetRegNum( pNew, (fSeq && p->vRegClasses) ? Vec_IntSize(p->vRegClasses) : Gia_ManRegNum(p) ); |
| Gia_ManHashStop( pNew ); |
| pNew = Gia_ManCleanup( pTemp = pNew ); |
| Gia_ManCleanupRemap( p, pTemp ); |
| Gia_ManStop( pTemp ); |
| assert( Tim_ManPoNum(pManTime) == Gia_ManCoNum(pNew) - nBBouts ); |
| assert( Tim_ManPiNum(pManTime) == Gia_ManCiNum(pNew) - nBBins ); |
| // implement initial state if given |
| if ( fSeq && p->vRegInits && Vec_IntSum(p->vRegInits) ) |
| { |
| char * pInit = ABC_ALLOC( char, Vec_IntSize(p->vRegInits) + 1 ); |
| Gia_Obj_t * pObj; |
| int i; |
| assert( Vec_IntSize(p->vRegInits) == Gia_ManRegNum(pNew) ); |
| Gia_ManForEachRo( pNew, pObj, i ) |
| { |
| if ( Vec_IntEntry(p->vRegInits, i) == 0 ) |
| pInit[i] = '0'; |
| else if ( Vec_IntEntry(p->vRegInits, i) == 1 ) |
| pInit[i] = '1'; |
| else |
| pInit[i] = 'X'; |
| } |
| pInit[i] = 0; |
| pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 ); |
| pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0; |
| Gia_ManStop( pTemp ); |
| ABC_FREE( pInit ); |
| } |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Verify XAIG against its spec.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec ) |
| { |
| int Status = -1; |
| Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter; |
| Vec_Int_t * vBoxPres = NULL; |
| if ( pFileSpec == NULL && pGia->pSpec == NULL ) |
| { |
| printf( "Spec file is not given. Use standard flow.\n" ); |
| return Status; |
| } |
| if ( Gia_ManBoxNum(pGia) && pGia->pAigExtra == NULL ) |
| { |
| printf( "Design has no box logic. Use standard flow.\n" ); |
| return Status; |
| } |
| // read original AIG |
| pSpec = Gia_AigerRead( pFileSpec ? pFileSpec : pGia->pSpec, 0, 0, 0 ); |
| if ( Gia_ManBoxNum(pSpec) && pSpec->pAigExtra == NULL ) |
| { |
| Gia_ManStop( pSpec ); |
| printf( "Spec has no box logic. Use standard flow.\n" ); |
| return Status; |
| } |
| // prepare miter |
| if ( pGia->pManTime == NULL && pSpec->pManTime == NULL ) |
| { |
| pGia0 = Gia_ManDup( pSpec ); |
| pGia1 = Gia_ManDup( pGia ); |
| } |
| else |
| { |
| // if timing managers have different number of black boxes, |
| // it is possible that some of the boxes are swept away |
| if ( pSpec->pManTime && Tim_ManBlackBoxNum((Tim_Man_t *)pSpec->pManTime) > 0 && Gia_ManBoxNum(pGia) > 0 ) |
| { |
| // specification cannot have fewer boxes than implementation |
| if ( Gia_ManBoxNum(pSpec) < Gia_ManBoxNum(pGia) ) |
| { |
| printf( "Spec has less boxes than the design. Cannot proceed.\n" ); |
| return Status; |
| } |
| // to align the boxes, find what boxes of pSpec are dropped in pGia |
| if ( Gia_ManBoxNum(pSpec) > Gia_ManBoxNum(pGia) ) |
| { |
| 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 |
| if ( Gia_ManBoxNum(pSpec) > 0 ) |
| pGia0 = Gia_ManDupCollapse( pSpec, pSpec->pAigExtra, vBoxPres, fSeq ); |
| else |
| pGia0 = Gia_ManDup( pSpec ); |
| if ( Gia_ManBoxNum(pGia) > 0 ) |
| pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL, fSeq ); |
| else |
| pGia1 = Gia_ManDup( pGia ); |
| Vec_IntFreeP( &vBoxPres ); |
| } |
| if ( fDumpFiles ) |
| { |
| char pFileName0[1000], pFileName1[1000]; |
| char * pNameGeneric = Extra_FileNameGeneric( pFileSpec ? pFileSpec : pGia->pSpec ); |
| sprintf( pFileName0, "%s_spec.aig", pNameGeneric ); |
| sprintf( pFileName1, "%s_impl.aig", pNameGeneric ); |
| Gia_AigerWrite( pGia0, pFileName0, 0, 0 ); |
| Gia_AigerWrite( pGia1, pFileName1, 0, 0 ); |
| ABC_FREE( pNameGeneric ); |
| printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 ); |
| } |
| // compute the miter |
| if ( fSeq ) |
| { |
| pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose ); |
| if ( pMiter ) |
| { |
| Aig_Man_t * pMan; |
| Fra_Sec_t SecPar, * pSecPar = &SecPar; |
| Fra_SecSetDefaultParams( pSecPar ); |
| pSecPar->fRetimeFirst = 0; |
| pSecPar->nBTLimit = nBTLimit; |
| pSecPar->TimeLimit = nTimeLim; |
| pSecPar->fVerbose = fVerbose; |
| pMan = Gia_ManToAig( pMiter, 0 ); |
| Gia_ManStop( pMiter ); |
| Status = Fra_FraigSec( pMan, pSecPar, NULL ); |
| Aig_ManStop( pMan ); |
| } |
| } |
| else |
| { |
| pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose ); |
| if ( pMiter ) |
| { |
| Cec_ParCec_t ParsCec, * pPars = &ParsCec; |
| Cec_ManCecSetDefaultParams( pPars ); |
| pPars->nBTLimit = nBTLimit; |
| pPars->TimeLimit = nTimeLim; |
| pPars->fVerbose = fVerbose; |
| Status = Cec_ManVerify( pMiter, pPars ); |
| if ( pPars->iOutFail >= 0 ) |
| Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail ); |
| Gia_ManStop( pMiter ); |
| } |
| } |
| Gia_ManStop( pGia0 ); |
| Gia_ManStop( pGia1 ); |
| Gia_ManStop( pSpec ); |
| return Status; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
