diff options
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaAiger.c | 44 | ||||
-rw-r--r-- | src/aig/gia/giaAigerExt.c | 26 | ||||
-rw-r--r-- | src/aig/gia/giaIf.c | 1 |
4 files changed, 64 insertions, 8 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b0e2426b..3fdbf4b5 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -128,6 +128,7 @@ struct Gia_Man_t_ Vec_Int_t * vFanoutNums; // static fanout Vec_Int_t * vFanout; // static fanout int * pMapping; // mapping for each node + int nOffset; // mapping offset Vec_Int_t * vMapping; Vec_Int_t * vLutConfigs; // LUT configurations Abc_Cex_t * pCexComb; // combinational counter-example diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index fb63e48d..63411013 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -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 if ( pCur + 1 < (unsigned char *)pContents + nFileSize && *pCur == 'c' ) { + int fVerbose = 1; Vec_Str_t * vStr; unsigned char * pCurTemp; pCur++; - while ( 1 ) + while ( pCur < (unsigned char *)pContents + nFileSize ) { // read extra AIG if ( *pCur == 'a' ) @@ -509,6 +510,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pCur += Vec_StrSize(vStr); pNew->pAigExtra = Gia_AigerReadFromMemory( Vec_StrArray(vStr), Vec_StrSize(vStr), 0, 0 ); Vec_StrFree( vStr ); + if ( fVerbose ) printf( "Finished reading extension \"a\".\n" ); } // read number of constraints else if ( *pCur == 'c' ) @@ -516,6 +518,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pCur++; assert( Gia_AigerReadInt(pCur) == 4 ); pCur += 4; pNew->nConstrs = Gia_AigerReadInt( pCur ); pCur += 4; + if ( fVerbose ) printf( "Finished reading extension \"c\".\n" ); } // read delay information else if ( *pCur == 'i' ) @@ -524,6 +527,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS nInputs = Gia_AigerReadInt(pCur)/4; pCur += 4; pNew->vInArrs = Vec_FltStart( nInputs ); memcpy( Vec_FltArray(pNew->vInArrs), pCur, 4*nInputs ); pCur += 4*nInputs; + if ( fVerbose ) printf( "Finished reading extension \"i\".\n" ); } else if ( *pCur == 'o' ) { @@ -531,6 +535,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS nOutputs = Gia_AigerReadInt(pCur)/4; pCur += 4; pNew->vOutReqs = Vec_FltStart( nOutputs ); memcpy( Vec_FltArray(pNew->vOutReqs), pCur, 4*nOutputs ); pCur += 4*nOutputs; + if ( fVerbose ) printf( "Finished reading extension \"o\".\n" ); } // read equivalence classes else if ( *pCur == 'e' ) @@ -541,6 +546,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pNew->pReprs = Gia_AigerReadEquivClasses( &pCur, Gia_ManObjNum(pNew) ); pNew->pNexts = Gia_ManDeriveNexts( pNew ); assert( pCur == pCurTemp ); + if ( fVerbose ) printf( "Finished reading extension \"e\".\n" ); } // read flop classes else if ( *pCur == 'f' ) @@ -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; pNew->vFlopClasses = Vec_IntStart( 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 else if ( *pCur == 'g' ) @@ -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; pNew->vGateClasses = Vec_IntStart( 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 else if ( *pCur == 'h' ) @@ -568,6 +576,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pNew->pManTime = Tim_ManLoad( vStr, 1 ); Vec_StrFree( vStr ); fHieOnly = 1; + if ( fVerbose ) printf( "Finished reading extension \"h\".\n" ); } // read packing else if ( *pCur == 'k' ) @@ -577,15 +586,23 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4; pNew->vPacking = Gia_AigerReadPacking( &pCur, pCurTemp - pCur ); assert( pCur == pCurTemp ); + if ( fVerbose ) printf( "Finished reading extension \"k\".\n" ); } // read mapping else if ( *pCur == 'm' ) { extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize ); + extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize ); + int nSize; pCur++; - pCurTemp = pCur + Gia_AigerReadInt(pCur) + 4; pCur += 4; - pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) ); + nSize = Gia_AigerReadInt(pCur); + 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 ); + if ( fVerbose ) printf( "Finished reading extension \"m\".\n" ); } // read model name else if ( *pCur == 'n' ) @@ -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; assert( pCur == pCurTemp ); } + if ( fVerbose ) printf( "Finished reading extension \"n\".\n" ); } // read placement else if ( *pCur == 'p' ) @@ -612,6 +630,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pPlacement = ABC_ALLOC( Gia_Plc_t, Gia_ManObjNum(pNew) ); memcpy( pPlacement, pCur, 4*Gia_ManObjNum(pNew) ); pCur += 4*Gia_ManObjNum(pNew); assert( pCur == pCurTemp ); + if ( fVerbose ) printf( "Finished reading extension \"p\".\n" ); } // read switching activity else if ( *pCur == 's' ) @@ -622,6 +641,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS pSwitching = ABC_ALLOC( unsigned char, Gia_ManObjNum(pNew) ); memcpy( pSwitching, pCur, Gia_ManObjNum(pNew) ); pCur += Gia_ManObjNum(pNew); assert( pCur == pCurTemp ); + if ( fVerbose ) printf( "Finished reading extension \"s\".\n" ); } // read timing manager else if ( *pCur == 't' ) @@ -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); pNew->pManTime = Tim_ManLoad( vStr, 0 ); Vec_StrFree( vStr ); + if ( fVerbose ) printf( "Finished reading extension \"t\".\n" ); } // read object classes else if ( *pCur == 'v' ) @@ -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; memcpy( Vec_IntArray(pNew->vObjClasses), pCur, 4*Vec_IntSize(pNew->vObjClasses) ); pCur += 4*Vec_IntSize(pNew->vObjClasses); + if ( fVerbose ) printf( "Finished reading extension \"v\".\n" ); } else break; } @@ -680,11 +702,16 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS if ( fHieOnly ) { Tim_ManPrint( (Tim_Man_t *)pNew->pManTime ); - 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 ( Abc_FrameReadLibBox() == NULL ) + printf( "Cannot create TIM manager because box library is not available.\n" ); + else + { + 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 ) @@ -1122,8 +1149,9 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int if ( p->pMapping ) { extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p ); + extern Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p ); fprintf( pFile, "m" ); - vStrExt = Gia_AigerWriteMapping( p ); + vStrExt = Gia_AigerWriteMappingSimple( p ); Gia_FileWriteBufferSize( pFile, Vec_StrSize(vStrExt) ); fwrite( Vec_StrArray(vStrExt), 1, Vec_StrSize(vStrExt), pFile ); Vec_StrFree( vStrExt ); diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c index 041c17a1..7a3e4c91 100644 --- a/src/aig/gia/giaAigerExt.c +++ b/src/aig/gia/giaAigerExt.c @@ -207,6 +207,32 @@ Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p ) /**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.] Description [] diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 0bcdc10a..1c2a56b3 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -591,6 +591,7 @@ Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan ) */ } } + pNew->nOffset = iOffset; Gia_ManCleanMark0( pNew ); // assert( iOffset == Gia_ManObjNum(pNew) + nItems ); if ( pIfMan->pManTim ) |