diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 11 | ||||
| -rw-r--r-- | src/aig/gia/giaAig.c | 10 | ||||
| -rw-r--r-- | src/aig/gia/giaAiger.c | 18 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 265 | ||||
| -rw-r--r-- | src/aig/gia/giaIf.c | 22 | ||||
| -rw-r--r-- | src/aig/gia/giaTim.c | 550 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 79 | ||||
| -rw-r--r-- | src/misc/tim/timMan.c | 2 |
10 files changed, 678 insertions, 284 deletions
@@ -3567,6 +3567,10 @@ SOURCE=.\src\aig\gia\giaTest.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaTim.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaTruth.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index f87a88fa..7ea38cda 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -806,6 +806,7 @@ extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNo extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p ); /*=== giaDup.c ============================================================*/ +extern void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); @@ -824,9 +825,6 @@ extern Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj ); extern Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ); -extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ); -extern Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p ); -extern Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes ); extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue ); extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 ); extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ); @@ -970,6 +968,13 @@ extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int De /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); +/*=== giaTim.c ===========================================================*/ +extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes ); +extern Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, Gia_Man_t * pBoxes ); +extern int Gia_ManLevelWithBoxes( Gia_Man_t * p ); +extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit ); /*=== giaTruth.c ===========================================================*/ extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths ); extern int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 5dcc6038..d523c46e 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -284,6 +284,7 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->nConstrs = p->nConstrs; // pNew->pSpec = Abc_UtilStrsav( p->pName ); // duplicate representation of choice nodes @@ -331,6 +332,7 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ) // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->nConstrs = p->nConstrs; // pNew->pSpec = Abc_UtilStrsav( p->pName ); // create the PIs @@ -372,6 +374,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ) // create the new manager pNew = Aig_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->nConstrs = p->nConstrs; // create the PIs Gia_ManForEachObj( p, pObj, i ) @@ -550,11 +553,16 @@ Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ) // extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose ); Gia_Man_t * pGia; Aig_Man_t * pNew, * pTemp; + if ( p->pManTime && p->vLevels == NULL ) + Gia_ManLevelWithBoxes( p ); pNew = Gia_ManToAig( p, 0 ); pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose ); Aig_ManStop( pTemp ); pGia = Gia_ManFromAig( pNew ); Aig_ManStop( pNew ); + pGia->pManTime = p->pManTime; p->pManTime = NULL; + pGia->pAigExtra = p->pAigExtra; p->pAigExtra = NULL; +// Gia_ManLevelWithBoxes( pGia ); return pGia; } @@ -578,6 +586,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars ) // pGia = Gia_ManFromAig( pNew ); pGia = Gia_ManFromAigChoices( pNew ); Aig_ManStop( pNew ); + pGia->pManTime = p->pManTime; p->pManTime = NULL; + pGia->pAigExtra = p->pAigExtra; p->pAigExtra = NULL; return pGia; } diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 48204e8b..476a9d36 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -495,7 +495,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS // check if there are other types of information to read if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' ) { - int fVerbose = 1; + int fVerbose = 0; Vec_Str_t * vStr; unsigned char * pCurTemp; pCur++; @@ -619,7 +619,6 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1; assert( pCur == pCurTemp ); } - if ( fVerbose ) printf( "Finished reading extension \"n\".\n" ); } // read placement else if ( *pCur == 'p' ) @@ -708,7 +707,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS { Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs ); // Tim_ManPrint( (Tim_Man_t *)pNew->pManTime ); - printf( "Created timing manager using Tim_ManCreate().\n" ); +// printf( "Created timing manager using Tim_ManCreate().\n" ); } } Vec_FltFreeP( &pNew->vInArrs ); @@ -767,11 +766,11 @@ Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck ) ABC_FREE( pNew->pName ); pName = Gia_FileNameGeneric( pFileName ); pNew->pName = Abc_UtilStrsav( pName ); -// pNew->pSpec = Ioa_UtilStrsav( pFileName ); ABC_FREE( pName ); + + assert( pNew->pSpec == NULL ); + pNew->pSpec = Abc_UtilStrsav( pFileName ); } - assert( pNew->pSpec == NULL ); - pNew->pSpec = Abc_UtilStrsav( pFileName ); return pNew; } @@ -949,6 +948,7 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve ***********************************************************************/ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact ) { + int fVerbose = 0; FILE * pFile; Gia_Man_t * p; Gia_Obj_t * pObj; @@ -1071,6 +1071,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); Vec_StrFree( vStrExt ); + if ( fVerbose ) printf( "Finished writing extension \"a\".\n" ); } /* // write constraints @@ -1099,6 +1100,8 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Vec_FltFree( vArrTimes ); Vec_FltFree( vReqTimes ); + if ( fVerbose ) printf( "Finished writing extension \"i\".\n" ); + if ( fVerbose ) printf( "Finished writing extension \"o\".\n" ); } } // write equivalences @@ -1135,6 +1138,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); Vec_StrFree( vStrExt ); + if ( fVerbose ) printf( "Finished writing extension \"h\".\n" ); } // write packing if ( p->vPacking ) @@ -1145,6 +1149,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); Vec_StrFree( vStrExt ); + if ( fVerbose ) printf( "Finished writing extension \"k\".\n" ); } // write mapping if ( p->pMapping ) @@ -1156,6 +1161,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); Vec_StrFree( vStrExt ); + if ( fVerbose ) printf( "Finished writing extension \"m\".\n" ); } // write placement if ( p->pPlacement ) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index bc1e59f6..14db2492 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1009,271 +1009,6 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ) /**Function************************************************************* - Synopsis [Duplicates AIG in the DFS order while putting CIs first.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ) -{ - 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; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - 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) ); - assert( Gia_ManIsNormalized(pNew) ); - Gia_ManDupRemapEquiv( pNew, p ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Duplicates AIG according to the timing manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p ) -{ - Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime; - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i, k, curCi, curCo, curNo, nodeLim; -//Gia_ManPrint( p ); - assert( pTime != NULL ); - assert( Gia_ManIsNormalized(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; - // copy primary inputs - for ( k = 0; k < Tim_ManPiNum(pTime); k++ ) - Gia_ManPi(p, k)->Value = Gia_ManAppendCi(pNew); - curCi = Tim_ManPiNum(pTime); - curCo = 0; - curNo = Gia_ManPiNum(p)+1; - for ( i = 0; i < Tim_ManBoxNum(pTime); i++ ) - { - // find the latest node feeding into inputs of this box - nodeLim = -1; - for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) - { - pObj = Gia_ManPo( p, curCo + k ); - nodeLim = Abc_MaxInt( nodeLim, Gia_ObjFaninId0p(p, pObj)+1 ); - } - // copy nodes up to the given node - for ( k = curNo; k < nodeLim; k++ ) - { - pObj = Gia_ManObj( p, k ); - assert( Gia_ObjIsAnd(pObj) ); - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - } - curNo = Abc_MaxInt( curNo, nodeLim ); - // copy COs - for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) - { - pObj = Gia_ManPo( p, curCo + k ); - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - } - curCo += Tim_ManBoxInputNum(pTime, i); - // copy CIs - for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ ) - { - pObj = Gia_ManPi( p, curCi + k ); - pObj->Value = Gia_ManAppendCi(pNew); - } - curCi += Tim_ManBoxOutputNum(pTime, i); - } - // copy remaining nodes - nodeLim = Gia_ManObjNum(p) - Gia_ManPoNum(p); - for ( k = curNo; k < nodeLim; k++ ) - { - pObj = Gia_ManObj( p, k ); - assert( Gia_ObjIsAnd(pObj) ); - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - } - curNo = Abc_MaxInt( curNo, nodeLim ); - curNo += Gia_ManPoNum(p); - // copy primary outputs - for ( k = 0; k < Tim_ManPoNum(pTime); k++ ) - { - pObj = Gia_ManPo( p, curCo + k ); - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - } - curCo += Tim_ManPoNum(pTime); - assert( curCi == Gia_ManPiNum(p) ); - assert( curCo == Gia_ManPoNum(p) ); - assert( curNo == Gia_ManObjNum(p) ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - Gia_ManDupRemapEquiv( pNew, p ); -//Gia_ManPrint( pNew ); - // pass the timing manager - pNew->pManTime = pTime; p->pManTime = NULL; - return pNew; -} - - -/**Function************************************************************* - - Synopsis [Find the ordering of AIG objects.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManDupFindOrderWithHie_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) -{ - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - assert( Gia_ObjIsAnd(pObj) ); - Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes ); - Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin1(pObj), vNodes ); - Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); -} -Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p ) -{ - Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime; - Vec_Int_t * vNodes; - Gia_Obj_t * pObj; - int i, k, curCi, curCo; - assert( p->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(pTime); i++ ) - { - pObj = Gia_ManPi( p, i ); - Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); - Gia_ObjSetTravIdCurrent( p, pObj ); - assert( Gia_ObjId(p, pObj) == i+1 ); -//printf( "%d ", Gia_ObjId(p, pObj) ); - } - // for each box, include box nodes - curCi = Tim_ManPiNum(pTime); - curCo = 0; - for ( i = 0; i < Tim_ManBoxNum(pTime); i++ ) - { -//printf( "Box %d:\n", i ); - // add internal nodes - for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) - { - pObj = Gia_ManPo( p, curCo + k ); -//Gia_ObjPrint( p, pObj ); -//printf( "Fanin " ); -//Gia_ObjPrint( p, Gia_ObjFanin0(pObj) ); - Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes ); - } - // add POs corresponding to box inputs - for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) - { - pObj = Gia_ManPo( p, curCo + k ); - Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); - } - curCo += Tim_ManBoxInputNum(pTime, i); - // add PIs corresponding to box outputs - for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ ) - { - pObj = Gia_ManPi( p, curCi + k ); -//Gia_ObjPrint( p, pObj ); - Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); - Gia_ObjSetTravIdCurrent( p, pObj ); - } - curCi += Tim_ManBoxOutputNum(pTime, i); - } - // add remaining nodes - for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ ) - { - pObj = Gia_ManPo( p, i ); - Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes ); - } - // add POs - for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ ) - { - pObj = Gia_ManPo( p, i ); - Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); - } - curCo += Tim_ManPoNum(pTime); - // verify counts - assert( curCi == Gia_ManPiNum(p) ); - assert( curCo == Gia_ManPoNum(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_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes ) -{ - Vec_Int_t * vNodes; - 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 ); - vNodes = Gia_ManDupFindOrderWithHie( p ); - Gia_ManForEachObjVec( vNodes, p, pObj, i ) - { - if ( Gia_ObjIsAnd(pObj) ) - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - 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) ); - if ( pvNodes ) - *pvNodes = vNodes; - else - Vec_IntFree( vNodes ); - return pNew; -} - - -/**Function************************************************************* - Synopsis [Returns the array of non-const-0 POs of the dual-output miter.] Description [] diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 19c2fe0b..b05e9106 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -720,7 +720,7 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p ) SideEffects [] - SeeAlso [] + SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp ) @@ -733,7 +733,8 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp ) if ( p->pManTime ) { pNew = Gia_ManDupWithHierarchy( p, &vNodes ); - pNew->pManTime = p->pManTime; p->pManTime = NULL; + pNew->pManTime = p->pManTime; p->pManTime = NULL; + pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL; p = pNew; } else @@ -769,13 +770,20 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp ) // if ( pIfMan->pPars->fDelayOpt ) // Vec_IntFreeP( &pNew->vMapping ); // return the original (unmodified by the mapper) timing manager - pNew->pManTime = p->pManTime; p->pManTime = NULL; + pNew->pManTime = p->pManTime; p->pManTime = NULL; + pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL; Gia_ManStop( p ); // normalize and transfer mapping - p = Gia_ManDupNormalize( pNew ); - Gia_ManTransferMapping( pNew, p ); - Gia_ManStop( pNew ); - return p; + pNew = Gia_ManDupNormalize( p = pNew ); + Gia_ManTransferMapping( p, pNew ); + pNew->pManTime = p->pManTime; p->pManTime = NULL; + pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL; + Gia_ManStop( p ); + +// printf( "PERFORMING VERIFICATION:\n" ); +// Gia_ManVerifyWithBoxes( pNew, NULL ); + + return pNew; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c new file mode 100644 index 00000000..10841216 --- /dev/null +++ b/src/aig/gia/giaTim.c @@ -0,0 +1,550 @@ +/**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 "misc/tim/tim.h" +#include "proof/cec/cec.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order while putting CIs first.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ) +{ + 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; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + 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) ); + assert( Gia_ManIsNormalized(pNew) ); + Gia_ManDupRemapEquiv( pNew, p ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG according to the timing manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p ) +{ + Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, k, curCi, curCo, curNo, nodeLim; +//Gia_ManPrint( p ); + assert( pTime != NULL ); + assert( Gia_ManIsNormalized(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; + // copy primary inputs + for ( k = 0; k < Tim_ManPiNum(pTime); k++ ) + Gia_ManPi(p, k)->Value = Gia_ManAppendCi(pNew); + curCi = Tim_ManPiNum(pTime); + curCo = 0; + curNo = Gia_ManPiNum(p)+1; + for ( i = 0; i < Tim_ManBoxNum(pTime); i++ ) + { + // find the latest node feeding into inputs of this box + nodeLim = -1; + for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); + nodeLim = Abc_MaxInt( nodeLim, Gia_ObjFaninId0p(p, pObj)+1 ); + } + // copy nodes up to the given node + for ( k = curNo; k < nodeLim; k++ ) + { + pObj = Gia_ManObj( p, k ); + assert( Gia_ObjIsAnd(pObj) ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + curNo = Abc_MaxInt( curNo, nodeLim ); + // copy COs + for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + curCo += Tim_ManBoxInputNum(pTime, i); + // copy CIs + for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ ) + { + pObj = Gia_ManPi( p, curCi + k ); + pObj->Value = Gia_ManAppendCi(pNew); + } + curCi += Tim_ManBoxOutputNum(pTime, i); + } + // copy remaining nodes + nodeLim = Gia_ManObjNum(p) - Gia_ManPoNum(p); + for ( k = curNo; k < nodeLim; k++ ) + { + pObj = Gia_ManObj( p, k ); + assert( Gia_ObjIsAnd(pObj) ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + curNo = Abc_MaxInt( curNo, nodeLim ); + curNo += Gia_ManPoNum(p); + // copy primary outputs + for ( k = 0; k < Tim_ManPoNum(pTime); k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + curCo += Tim_ManPoNum(pTime); + assert( curCi == Gia_ManPiNum(p) ); + assert( curCo == Gia_ManPoNum(p) ); + assert( curNo == Gia_ManObjNum(p) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Gia_ManDupRemapEquiv( pNew, p ); +//Gia_ManPrint( pNew ); + // pass the timing manager + pNew->pManTime = pTime; p->pManTime = NULL; + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Find the ordering of AIG objects.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupFindOrderWithHie_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes ); + Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin1(pObj), vNodes ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} +Vec_Int_t * Gia_ManDupFindOrderWithHie( Gia_Man_t * p ) +{ + Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime; + Vec_Int_t * vNodes; + Gia_Obj_t * pObj; + int i, k, curCi, curCo; + assert( p->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(pTime); i++ ) + { + pObj = Gia_ManPi( p, i ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + Gia_ObjSetTravIdCurrent( p, pObj ); + assert( Gia_ObjId(p, pObj) == i+1 ); +//printf( "%d ", Gia_ObjId(p, pObj) ); + } + // for each box, include box nodes + curCi = Tim_ManPiNum(pTime); + curCo = 0; + for ( i = 0; i < Tim_ManBoxNum(pTime); i++ ) + { +//printf( "Box %d:\n", i ); + // add internal nodes + for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); +//Gia_ObjPrint( p, pObj ); +//printf( "Fanin " ); +//Gia_ObjPrint( p, Gia_ObjFanin0(pObj) ); + Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes ); + } + // add POs corresponding to box inputs + for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + } + curCo += Tim_ManBoxInputNum(pTime, i); + // add PIs corresponding to box outputs + for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ ) + { + pObj = Gia_ManPi( p, curCi + k ); +//Gia_ObjPrint( p, pObj ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + Gia_ObjSetTravIdCurrent( p, pObj ); + } + curCi += Tim_ManBoxOutputNum(pTime, i); + } + // add remaining nodes + for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ ) + { + pObj = Gia_ManPo( p, i ); + Gia_ManDupFindOrderWithHie_rec( p, Gia_ObjFanin0(pObj), vNodes ); + } + // add POs + for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ ) + { + pObj = Gia_ManPo( p, i ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + } + curCo += Tim_ManPoNum(pTime); + // verify counts + assert( curCi == Gia_ManPiNum(p) ); + assert( curCo == Gia_ManPoNum(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_ManDupWithHierarchy( Gia_Man_t * p, Vec_Int_t ** pvNodes ) +{ + Vec_Int_t * vNodes; + 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 ); + vNodes = Gia_ManDupFindOrderWithHie( p ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + 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) ); + if ( pvNodes ) + *pvNodes = vNodes; + else + Vec_IntFree( vNodes ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupWithBoxes_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) ); + Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin0(pObj), pNew ); + Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin1(pObj), pNew ); +// assert( !~pObj->Value ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, Gia_Man_t * pBoxes ) +{ + Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjBox; + int i, k, curCi, curCo; + assert( Gia_ManRegNum(p) == 0 ); + assert( Gia_ManPiNum(p) == Tim_ManPiNum(pTime) + Gia_ManPoNum(pBoxes) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + 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(pTime); i++ ) + { + pObj = Gia_ManPi( p, i ); + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ObjSetTravIdCurrent( p, pObj ); + } + // create logic for each box + curCi = Tim_ManPiNum(pTime); + curCo = 0; + for ( i = 0; i < Tim_ManBoxNum(pTime); i++ ) + { + // clean boxes + Gia_ManIncrementTravId( pBoxes ); + Gia_ObjSetTravIdCurrent( pBoxes, Gia_ManConst0(pBoxes) ); + Gia_ManConst0(pBoxes)->Value = 0; + // add internal nodes + for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) + { + // build logic + pObj = Gia_ManPo( p, curCo + k ); + Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin0(pObj), pNew ); + // transfer to the PI + pObjBox = Gia_ManPi( pBoxes, k ); + pObjBox->Value = Gia_ObjFanin0Copy(pObj); + Gia_ObjSetTravIdCurrent( pBoxes, pObjBox ); + } + curCo += Tim_ManBoxInputNum(pTime, i); + // add internal nodes + for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ ) + { + // build logic + pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pTime) + k ); + Gia_ManDupWithBoxes_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 ); + } + curCi += Tim_ManBoxOutputNum(pTime, i); + } + // add remaining nodes + for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ ) + { + pObj = Gia_ManPo( p, i ); + Gia_ManDupWithBoxes_rec( p, Gia_ObjFanin0(pObj), pNew ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + curCo += Tim_ManPoNum(pTime); + // verify counts + assert( curCi == Gia_ManPiNum(p) ); + assert( curCo == Gia_ManPoNum(p) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + assert( Tim_ManPoNum(pTime) == Gia_ManPoNum(pNew) ); + assert( Tim_ManPiNum(pTime) == Gia_ManPiNum(pNew) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin1(pObj) ); + Gia_ObjSetAndLevel( p, pObj ); +} +int Gia_ManLevelWithBoxes( Gia_Man_t * p ) +{ + Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime; + Gia_Obj_t * pObj; + int i, k, curCi, curCo, LevelMax; + assert( Gia_ManRegNum(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(pTime); i++ ) + { + pObj = Gia_ManPi( p, i ); +// Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pTime, i) ); + Gia_ObjSetLevel( p, pObj, 0 ); + Gia_ObjSetTravIdCurrent( p, pObj ); + } + // create logic for each box + curCi = Tim_ManPiNum(pTime); + curCo = 0; + for ( i = 0; i < Tim_ManBoxNum(pTime); i++ ) + { + LevelMax = 0; + for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); + Gia_ManLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ObjSetCoLevel( p, pObj ); + LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObj) ); + } + curCo += Tim_ManBoxInputNum(pTime, i); + LevelMax++; + for ( k = 0; k < Tim_ManBoxOutputNum(pTime, i); k++ ) + { + pObj = Gia_ManPi( p, curCi + k ); + Gia_ObjSetLevel( p, pObj, LevelMax ); + Gia_ObjSetTravIdCurrent( p, pObj ); + } + curCi += Tim_ManBoxOutputNum(pTime, i); + } + // add remaining nodes + p->nLevels = 0; + for ( i = Tim_ManCoNum(pTime) - Tim_ManPoNum(pTime); i < Tim_ManCoNum(pTime); i++ ) + { + pObj = Gia_ManPo( 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(pTime); + // verify counts + assert( curCi == Gia_ManPiNum(p) ); + assert( curCo == Gia_ManPoNum(p) ); +// printf( "Max level is %d.\n", p->nLevels ); + return p->nLevels; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit ) +{ + int fVerbose = 1; + int Status = -1; + Gia_Man_t * pSpec, * pGia0, * pGia1, * pMiter; + if ( pGia->pSpec == NULL ) + { + printf( "Spec file is not given. Use standard flow.\n" ); + return Status; + } + if ( pGia->pManTime == NULL ) + { + printf( "Design has no tim manager. Use standard flow.\n" ); + return Status; + } + if ( pGia->pAigExtra == NULL ) + { + printf( "Design has no box logic. Use standard flow.\n" ); + return Status; + } + // read original AIG + pSpec = Gia_AigerRead( pGia->pSpec, 0, 0 ); + if ( pSpec->pManTime == NULL ) + { + printf( "Spec has no tim manager. Use standard flow.\n" ); + return Status; + } + if ( pSpec->pAigExtra == NULL ) + { + printf( "Spec has no box logic. Use standard flow.\n" ); + return Status; + } + pGia0 = Gia_ManDupWithBoxes( pSpec, pSpec->pAigExtra ); + pGia1 = Gia_ManDupWithBoxes( pGia, pGia->pAigExtra ); + // compute the miter + pMiter = Gia_ManMiter( pGia0, pGia1, 1, 0, fVerbose ); + if ( pMiter ) + { + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Cec_ManCecSetDefaultParams( pPars ); + pPars->fVerbose = fVerbose; + if ( pParsInit ) + memcpy( pPars, pParsInit, sizeof(Cec_ParCec_t) ); + Status = Cec_ManVerify( pMiter, pPars ); + Gia_ManStop( pMiter ); + if ( pPars->iOutFail >= 0 ) + Abc_Print( 1, "Verification failed for at least one output (%d).\n", pPars->iOutFail ); + } + Gia_ManStop( pGia0 ); + Gia_ManStop( pGia1 ); + Gia_ManStop( pSpec ); + return Status; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 947cdc08..169b71e7 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -38,6 +38,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaSupMin.c \ src/aig/gia/giaSwitch.c \ src/aig/gia/giaTest.c \ + src/aig/gia/giaTim.c \ src/aig/gia/giaTruth.c \ src/aig/gia/giaTsim.c \ src/aig/gia/giaUtil.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index aca047c4..b35eab98 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -351,6 +351,7 @@ static int Abc_CommandAbc9Filter ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Verify ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -811,6 +812,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&verify", Abc_CommandAbc9Verify, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&force", Abc_CommandAbc9Force, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&embed", Abc_CommandAbc9Embed, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&if", Abc_CommandAbc9If, 0 ); @@ -27221,6 +27223,71 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + int c; + Cec_ManCecSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CTvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimeLimit < 0 ) + goto usage; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + Gia_ManVerifyWithBoxes( pAbc->pGia, pPars ); + return 0; + +usage: + Abc_Print( -2, "usage: &verify [-CT num] [-vh]\n" ); + Abc_Print( -2, "\t performs verification of combinational design\n" ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no"); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Force( Abc_Frame_t * pAbc, int argc, char ** argv ) { int nIters = 20; @@ -27399,6 +27466,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" ); pAbc->pLibLut = If_LibLutSetSimple( 6 ); } + pPars->pLutLib = pAbc->pLibLut; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikcvh" ) ) != EOF ) { @@ -27716,6 +27784,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE ); return 1; } + if ( pAbc->pGia->pManTime && pAbc->pLibBox == NULL ) + { + Abc_Print( -1, "Design has boxes but box library is not entered.\n" ); + return 1; + } // perform mapping pNew = Gia_ManPerformMapping( pAbc->pGia, pPars ); @@ -30418,7 +30491,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); // extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); // extern void Unr_ManTest( Gia_Man_t * pGia ); - extern void Mig_ManTest( Gia_Man_t * pGia ); +// extern void Mig_ManTest( Gia_Man_t * pGia ); +// extern int Gia_ManVerify( Gia_Man_t * pGia ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30468,7 +30542,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose ); // Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); // Unr_ManTest( pAbc->pGia ); - Mig_ManTest( pAbc->pGia ); +// Mig_ManTest( pAbc->pGia ); +// Gia_ManVerifyWithBoxes( pAbc->pGia ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 8900fda4..f2245a6a 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -132,7 +132,7 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay ) // assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) ); assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL ); Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew ); -printf( "Finished duplicating delay table %d.\n", i ); +//printf( "Finished duplicating delay table %d.\n", i ); } } // duplicate boxes |