luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Integration of timing manager.

This commit is contained in:
Alan Mishchenko 2013-02-03 18:02:22 +08:00
parent 61f8112da0
commit 930369f36f
10 changed files with 678 additions and 284 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -3567,6 +3567,10 @@ SOURCE=.\src\aig\gia\giaTest.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\gia\giaTim.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaTruth.c SOURCE=.\src\aig\gia\giaTruth.c
# End Source File # End Source File
# Begin Source File # Begin Source File

11
src/aig/gia/gia.h
View File

@ -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_Vec_t * Gia_ManLevelize( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManOrderReverse( Gia_Man_t * p );
/*=== giaDup.c ============================================================*/ /*=== 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_ManDupOrderDfs( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupOrderDfsReverse( 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_ManDupDfsSkip( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj ); 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_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_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_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, 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 ============================================================*/ /*=== giaSwitch.c ============================================================*/
extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManEvaluateSwitching( Gia_Man_t * p );
extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); 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 ===========================================================*/ /*=== giaTruth.c ===========================================================*/
extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths ); 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 ); extern int Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );

10
src/aig/gia/giaAig.c
View File

@ -284,6 +284,7 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
// create the new manager // create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) ); pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs; pNew->nConstrs = p->nConstrs;
// pNew->pSpec = Abc_UtilStrsav( p->pName ); // pNew->pSpec = Abc_UtilStrsav( p->pName );
// duplicate representation of choice nodes // duplicate representation of choice nodes
@ -331,6 +332,7 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
// create the new manager // create the new manager
pNew = Aig_ManStart( Gia_ManAndNum(p) ); pNew = Aig_ManStart( Gia_ManAndNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs; pNew->nConstrs = p->nConstrs;
// pNew->pSpec = Abc_UtilStrsav( p->pName ); // pNew->pSpec = Abc_UtilStrsav( p->pName );
// create the PIs // create the PIs
@ -372,6 +374,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
// create the new manager // create the new manager
pNew = Aig_ManStart( Gia_ManObjNum(p) ); pNew = Aig_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->nConstrs = p->nConstrs; pNew->nConstrs = p->nConstrs;
// create the PIs // create the PIs
Gia_ManForEachObj( p, pObj, i ) 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 ); // extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
Gia_Man_t * pGia; Gia_Man_t * pGia;
Aig_Man_t * pNew, * pTemp; Aig_Man_t * pNew, * pTemp;
if ( p->pManTime && p->vLevels == NULL )
Gia_ManLevelWithBoxes( p );
pNew = Gia_ManToAig( p, 0 ); pNew = Gia_ManToAig( p, 0 );
pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose ); pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
pGia = Gia_ManFromAig( pNew ); pGia = Gia_ManFromAig( pNew );
Aig_ManStop( pNew ); Aig_ManStop( pNew );
pGia->pManTime = p->pManTime; p->pManTime = NULL;
pGia->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
// Gia_ManLevelWithBoxes( pGia );
return pGia; return pGia;
} }
@ -578,6 +586,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
// pGia = Gia_ManFromAig( pNew ); // pGia = Gia_ManFromAig( pNew );
pGia = Gia_ManFromAigChoices( pNew ); pGia = Gia_ManFromAigChoices( pNew );
Aig_ManStop( pNew ); Aig_ManStop( pNew );
pGia->pManTime = p->pManTime; p->pManTime = NULL;
pGia->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
return pGia; return pGia;
} }

18
src/aig/gia/giaAiger.c
View File

@ -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 // check if there are other types of information to read
if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' ) if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' )
{ {
int fVerbose = 1; int fVerbose = 0;
Vec_Str_t * vStr; Vec_Str_t * vStr;
unsigned char * pCurTemp; unsigned char * pCurTemp;
pCur++; 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; pNew->pName = Abc_UtilStrsav( (char *)pCur ); pCur += strlen(pNew->pName) + 1;
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
} }
if ( fVerbose ) printf( "Finished reading extension \"n\".\n" );
} }
// read placement // read placement
else if ( *pCur == 'p' ) 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_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs );
// Tim_ManPrint( (Tim_Man_t *)pNew->pManTime ); // 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 ); Vec_FltFreeP( &pNew->vInArrs );
@ -767,11 +766,11 @@ Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck )
ABC_FREE( pNew->pName ); ABC_FREE( pNew->pName );
pName = Gia_FileNameGeneric( pFileName ); pName = Gia_FileNameGeneric( pFileName );
pNew->pName = Abc_UtilStrsav( pName ); pNew->pName = Abc_UtilStrsav( pName );
// pNew->pSpec = Ioa_UtilStrsav( pFileName );
ABC_FREE( pName ); ABC_FREE( pName );
assert( pNew->pSpec == NULL );
pNew->pSpec = Abc_UtilStrsav( pFileName );
} }
assert( pNew->pSpec == NULL );
pNew->pSpec = Abc_UtilStrsav( pFileName );
return pNew; 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 ) void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact )
{ {
int fVerbose = 0;
FILE * pFile; FILE * pFile;
Gia_Man_t * p; Gia_Man_t * p;
Gia_Obj_t * pObj; 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) ); Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt ); Vec_StrFree( vStrExt );
if ( fVerbose ) printf( "Finished writing extension \"a\".\n" );
} }
/* /*
// write constraints // write constraints
@ -1099,6 +1100,8 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Vec_FltFree( vArrTimes ); Vec_FltFree( vArrTimes );
Vec_FltFree( vReqTimes ); Vec_FltFree( vReqTimes );
if ( fVerbose ) printf( "Finished writing extension \"i\".\n" );
if ( fVerbose ) printf( "Finished writing extension \"o\".\n" );
} }
} }
// write equivalences // write equivalences
@ -1135,6 +1138,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt ); Vec_StrFree( vStrExt );
if ( fVerbose ) printf( "Finished writing extension \"h\".\n" );
} }
// write packing // write packing
if ( p->vPacking ) 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) ); Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt ); Vec_StrFree( vStrExt );
if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
} }
// write mapping // write mapping
if ( p->pMapping ) 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) ); Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) );
fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile );
Vec_StrFree( vStrExt ); Vec_StrFree( vStrExt );
if ( fVerbose ) printf( "Finished writing extension \"m\".\n" );
} }
// write placement // write placement
if ( p->pPlacement ) if ( p->pPlacement )

265
src/aig/gia/giaDup.c
View File

@ -1007,271 +1007,6 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
return pNew; return pNew;
} }
/**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************************************************************* /**Function*************************************************************
Synopsis [Returns the array of non-const-0 POs of the dual-output miter.] Synopsis [Returns the array of non-const-0 POs of the dual-output miter.]

20
src/aig/gia/giaIf.c
View File

@ -733,7 +733,8 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
if ( p->pManTime ) if ( p->pManTime )
{ {
pNew = Gia_ManDupWithHierarchy( p, &vNodes ); 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; p = pNew;
} }
else else
@ -769,13 +770,20 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
// if ( pIfMan->pPars->fDelayOpt ) // if ( pIfMan->pPars->fDelayOpt )
// Vec_IntFreeP( &pNew->vMapping ); // Vec_IntFreeP( &pNew->vMapping );
// return the original (unmodified by the mapper) timing manager // 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 ); Gia_ManStop( p );
// normalize and transfer mapping // normalize and transfer mapping
p = Gia_ManDupNormalize( pNew ); pNew = Gia_ManDupNormalize( p = pNew );
Gia_ManTransferMapping( pNew, p ); Gia_ManTransferMapping( p, pNew );
Gia_ManStop( pNew ); pNew->pManTime = p->pManTime; p->pManTime = NULL;
return p; pNew->pAigExtra = p->pAigExtra; p->pAigExtra = NULL;
Gia_ManStop( p );
// printf( "PERFORMING VERIFICATION:\n" );
// Gia_ManVerifyWithBoxes( pNew, NULL );
return pNew;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

550
src/aig/gia/giaTim.c Normal file
View File

@ -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

1
src/aig/gia/module.make
View File

@ -38,6 +38,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaSupMin.c \ src/aig/gia/giaSupMin.c \
src/aig/gia/giaSwitch.c \ src/aig/gia/giaSwitch.c \
src/aig/gia/giaTest.c \ src/aig/gia/giaTest.c \
src/aig/gia/giaTim.c \
src/aig/gia/giaTruth.c \ src/aig/gia/giaTruth.c \
src/aig/gia/giaTsim.c \ src/aig/gia/giaTsim.c \
src/aig/gia/giaUtil.c src/aig/gia/giaUtil.c

79
src/base/abci/abc.c
View File

@ -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_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9EquivMark ( 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_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_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Embed ( 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 ); 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", "&reduce", Abc_CommandAbc9Reduce, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 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", "&force", Abc_CommandAbc9Force, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&embed", Abc_CommandAbc9Embed, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&embed", Abc_CommandAbc9Embed, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&if", Abc_CommandAbc9If, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&if", Abc_CommandAbc9If, 0 );
@ -27210,6 +27212,71 @@ usage:
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -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" ); Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
pAbc->pLibLut = If_LibLutSetSimple( 6 ); pAbc->pLibLut = If_LibLutSetSimple( 6 );
} }
pPars->pLutLib = pAbc->pLibLut;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikcvh" ) ) != EOF ) 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 ); Abc_Print( -1, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE );
return 1; 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 // perform mapping
pNew = Gia_ManPerformMapping( pAbc->pGia, pPars ); 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 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 Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose );
// extern void Unr_ManTest( Gia_Man_t * pGia ); // 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(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) 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 ); // Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose );
// Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); // Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 );
// Unr_ManTest( pAbc->pGia ); // Unr_ManTest( pAbc->pGia );
Mig_ManTest( pAbc->pGia ); // Mig_ManTest( pAbc->pGia );
// Gia_ManVerifyWithBoxes( pAbc->pGia );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &test [-svh]\n" ); Abc_Print( -2, "usage: &test [-svh]\n" );

2
src/misc/tim/timMan.c
View File

@ -132,7 +132,7 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
// assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) ); // assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL ); assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL );
Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew ); Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew );
printf( "Finished duplicating delay table %d.\n", i ); //printf( "Finished duplicating delay table %d.\n", i );
} }
} }
// duplicate boxes // duplicate boxes