Skip to content

A
abc
Commit dfd871c2 by Alan Mishchenko
Options

Integration of timing manager.

parent 68636887
Showing with 64 additions and 8 deletions
src/aig/gia/gia.h
...@@ -128,6 +128,7 @@ struct Gia_Man_t_ ...@@ -128,6 +128,7 @@ struct Gia_Man_t_
Vec_Int_t * vFanoutNums; // static fanout Vec_Int_t * vFanoutNums; // static fanout
Vec_Int_t * vFanout; // static fanout Vec_Int_t * vFanout; // static fanout
int * pMapping; // mapping for each node int * pMapping; // mapping for each node
int nOffset; // mapping offset
Vec_Int_t * vMapping; Vec_Int_t * vMapping;
Vec_Int_t * vLutConfigs; // LUT configurations Vec_Int_t * vLutConfigs; // LUT configurations
Abc_Cex_t * pCexComb; // combinational counter-example Abc_Cex_t * pCexComb; // combinational counter-example
......
src/aig/gia/giaAiger.c
...@@ -495,10 +495,11 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -495,10 +495,11 @@ 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;
Vec_Str_t * vStr; Vec_Str_t * vStr;
unsigned char * pCurTemp; unsigned char * pCurTemp;
pCur++; pCur++;
while ( 1 ) while ( pCur < (unsigned char *)pContents + nFileSize )
{ {
// read extra AIG // read extra AIG
if ( *pCur == 'a' ) if ( *pCur == 'a' )
...@@ -509,6 +510,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -509,6 +510,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pCur += Vec_StrSize(vStr); pCur += Vec_StrSize(vStr);
pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 ); pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 );
Vec_StrFree( vStr ); Vec_StrFree( vStr );
if ( fVerbose ) printf( "Finished reading extension \"a\".\n" );
} }
// read number of constraints // read number of constraints
else if ( *pCur == 'c' ) else if ( *pCur == 'c' )
...@@ -516,6 +518,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -516,6 +518,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pCur++; pCur++;
assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4; assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4;
pNew->nConstrs = Gia_AigerReadInt( pCur ); pCur += 4; pNew->nConstrs = Gia_AigerReadInt( pCur ); pCur += 4;
if ( fVerbose ) printf( "Finished reading extension \"c\".\n" );
} }
// read delay information // read delay information
else if ( *pCur == 'i' ) else if ( *pCur == 'i' )
...@@ -524,6 +527,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -524,6 +527,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
nInputs = Gia_AigerReadInt(pCur)/4; pCur += 4; nInputs = Gia_AigerReadInt(pCur)/4; pCur += 4;
pNew->vInArrs = Vec_FltStart( nInputs ); pNew->vInArrs = Vec_FltStart( nInputs );
memcpy( Vec_FltArray(pNew->vInArrs), pCur, 4*nInputs ); pCur += 4*nInputs; memcpy( Vec_FltArray(pNew->vInArrs), pCur, 4*nInputs ); pCur += 4*nInputs;
if ( fVerbose ) printf( "Finished reading extension \"i\".\n" );
} }
else if ( *pCur == 'o' ) else if ( *pCur == 'o' )
{ {
...@@ -531,6 +535,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -531,6 +535,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
nOutputs = Gia_AigerReadInt(pCur)/4; pCur += 4; nOutputs = Gia_AigerReadInt(pCur)/4; pCur += 4;
pNew->vOutReqs = Vec_FltStart( nOutputs ); pNew->vOutReqs = Vec_FltStart( nOutputs );
memcpy( Vec_FltArray(pNew->vOutReqs), pCur, 4*nOutputs ); pCur += 4*nOutputs; memcpy( Vec_FltArray(pNew->vOutReqs), pCur, 4*nOutputs ); pCur += 4*nOutputs;
if ( fVerbose ) printf( "Finished reading extension \"o\".\n" );
} }
// read equivalence classes // read equivalence classes
else if ( *pCur == 'e' ) else if ( *pCur == 'e' )
...@@ -541,6 +546,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -541,6 +546,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
pNew->pNexts = Gia_ManDeriveNexts( pNew ); pNew->pNexts = Gia_ManDeriveNexts( pNew );
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"e\".\n" );
} }
// read flop classes // read flop classes
else if ( *pCur == 'f' ) else if ( *pCur == 'f' )
...@@ -549,6 +555,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -549,6 +555,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) ); pCur += 4; assert( Gia_AigerReadInt(pCur) == 4*Gia_ManRegNum(pNew) ); pCur += 4;
pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) ); pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
memcpy( Vec_IntArray(pNew->vFlopClasses), pCur, 4*Gia_ManRegNum(pNew) ); pCur += 4*Gia_ManRegNum(pNew); memcpy( Vec_IntArray(pNew->vFlopClasses), pCur, 4*Gia_ManRegNum(pNew) ); pCur += 4*Gia_ManRegNum(pNew);
if ( fVerbose ) printf( "Finished reading extension \"f\".\n" );
} }
// read gate classes // read gate classes
else if ( *pCur == 'g' ) else if ( *pCur == 'g' )
...@@ -557,6 +564,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -557,6 +564,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) ); pCur += 4; assert( Gia_AigerReadInt(pCur) == 4*Gia_ManObjNum(pNew) ); pCur += 4;
pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) ); pNew->vGateClasses = Vec_IntStart( Gia_ManObjNum(pNew) );
memcpy( Vec_IntArray(pNew->vGateClasses), pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew); memcpy( Vec_IntArray(pNew->vGateClasses), pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew);
if ( fVerbose ) printf( "Finished reading extension \"g\".\n" );
} }
// read hierarchy information // read hierarchy information
else if ( *pCur == 'h' ) else if ( *pCur == 'h' )
...@@ -568,6 +576,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -568,6 +576,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pNew->pManTime = Tim_ManLoad( vStr, 1 ); pNew->pManTime = Tim_ManLoad( vStr, 1 );
Vec_StrFree( vStr ); Vec_StrFree( vStr );
fHieOnly = 1; fHieOnly = 1;
if ( fVerbose ) printf( "Finished reading extension \"h\".\n" );
} }
// read packing // read packing
else if ( *pCur == 'k' ) else if ( *pCur == 'k' )
...@@ -577,15 +586,23 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -577,15 +586,23 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4; pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4;
pNew->vPacking = Gia_AigerReadPacking( &pCur, pCurTemp - pCur ); pNew->vPacking = Gia_AigerReadPacking( &pCur, pCurTemp - pCur );
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"k\".\n" );
} }
// read mapping // read mapping
else if ( *pCur == 'm' ) else if ( *pCur == 'm' )
{ {
extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize ); extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize );
int nSize;
pCur++; pCur++;
pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4; nSize = Gia_AigerReadInt(pCur);
pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) ); pCurTemp = pCur + nSize + 4; pCur += 4;
// pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) );
pNew->pMapping = Gia_AigerReadMappingSimple( &pCur, nSize );
pNew->nOffset = nSize / 4;
pCur += nSize;
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"m\".\n" );
} }
// read model name // read model name
else if ( *pCur == 'n' ) else if ( *pCur == 'n' )
...@@ -602,6 +619,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -602,6 +619,7 @@ 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' )
...@@ -612,6 +630,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -612,6 +630,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) ); pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) );
memcpy( pPlacement, pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew); memcpy( pPlacement, pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew);
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"p\".\n" );
} }
// read switching activity // read switching activity
else if ( *pCur == 's' ) else if ( *pCur == 's' )
...@@ -622,6 +641,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -622,6 +641,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) ); pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) );
memcpy( pSwitching, pCur, Gia_ManObjNum(pNew) ); pCur += Gia_ManObjNum(pNew); memcpy( pSwitching, pCur, Gia_ManObjNum(pNew) ); pCur += Gia_ManObjNum(pNew);
assert( pCur == pCurTemp ); assert( pCur == pCurTemp );
if ( fVerbose ) printf( "Finished reading extension \"s\".\n" );
} }
// read timing manager // read timing manager
else if ( *pCur == 't' ) else if ( *pCur == 't' )
...@@ -631,6 +651,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -631,6 +651,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); pCur += Vec_StrSize(vStr); memcpy( Vec_StrArray(vStr), pCur, Vec_StrSize(vStr) ); pCur += Vec_StrSize(vStr);
pNew->pManTime = Tim_ManLoad( vStr, 0 ); pNew->pManTime = Tim_ManLoad( vStr, 0 );
Vec_StrFree( vStr ); Vec_StrFree( vStr );
if ( fVerbose ) printf( "Finished reading extension \"t\".\n" );
} }
// read object classes // read object classes
else if ( *pCur == 'v' ) else if ( *pCur == 'v' )
...@@ -639,6 +660,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -639,6 +660,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4; pNew->vObjClasses = Vec_IntStart( Gia_AigerReadInt(pCur)/4 ); pCur += 4;
memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) ); memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) );
pCur += 4*Vec_IntSize(pNew->vObjClasses); pCur += 4*Vec_IntSize(pNew->vObjClasses);
if ( fVerbose ) printf( "Finished reading extension \"v\".\n" );
} }
else break; else break;
} }
...@@ -680,11 +702,16 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS ...@@ -680,11 +702,16 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
if ( fHieOnly ) if ( fHieOnly )
{ {
Tim_ManPrint( (Tim_Man_t *)pNew->pManTime ); Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs ); if ( Abc_FrameReadLibBox() == NULL )
Tim_ManPrint( (Tim_Man_t *)pNew->pManTime ); printf( "Cannot create TIM manager because box library is not available.\n" );
Vec_FltFreeP( &pNew->vInArrs ); else
Vec_FltFreeP( &pNew->vOutReqs ); {
Tim_ManCreate( (Tim_Man_t *)pNew->pManTime, Abc_FrameReadLibBox(), pNew->vInArrs, pNew->vOutReqs );
Tim_ManPrint( (Tim_Man_t *)pNew->pManTime );
}
} }
Vec_FltFreeP( &pNew->vInArrs );
Vec_FltFreeP( &pNew->vOutReqs );
/* /*
if ( pNew->pManTime ) if ( pNew->pManTime )
...@@ -1122,8 +1149,9 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int ...@@ -1122,8 +1149,9 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
if ( p->pMapping ) if ( p->pMapping )
{ {
extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p ); extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
extern Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p );
fprintf( pFile, "m" ); fprintf( pFile, "m" );
vStrExt = Gia_AigerWriteMapping( p ); vStrExt = Gia_AigerWriteMappingSimple( p );
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 );
......
src/aig/gia/giaAigerExt.c
...@@ -207,6 +207,32 @@ Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p ) ...@@ -207,6 +207,32 @@ Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Read/write mapping information.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize )
{
int * pMapping = ABC_ALLOC( int, nSize/4 );
memcpy( pMapping, *ppPos, nSize );
assert( nSize % 4 == 0 );
return pMapping;
}
Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p )
{
unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*p->nOffset );
memcpy( pBuffer, p->pMapping, 4*p->nOffset );
assert( p->pMapping != NULL && p->nOffset >= Gia_ManObjNum(p) );
return Vec_StrAllocArray( (char *)pBuffer, 4*p->nOffset );
}
/**Function*************************************************************
Synopsis [Read/write packing information.] Synopsis [Read/write packing information.]
Description [] Description []
......
src/aig/gia/giaIf.c
...@@ -591,6 +591,7 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan ) ...@@ -591,6 +591,7 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
*/ */
} }
} }
pNew->nOffset = iOffset;
Gia_ManCleanMark0( pNew ); Gia_ManCleanMark0( pNew );
// assert( iOffset == Gia_ManObjNum(pNew) + nItems ); // assert( iOffset == Gia_ManObjNum(pNew) + nItems );
if ( pIfMan->pManTim ) if ( pIfMan->pManTim )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment