From 4a9789e58d27ecaba541ba3fcb0565a334dcd54b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 1 Jul 2008 08:01:00 -0700 Subject: Version abc80701 --- src/base/io/ioReadAiger.c | 104 +++++++++++++++++- src/base/io/ioWriteAiger.c | 262 +++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 354 insertions(+), 12 deletions(-) (limited to 'src/base/io') diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index 3739205d..9ecc00fd 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -20,6 +20,7 @@ ***********************************************************************/ #include "ioAbc.h" +#include //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -85,6 +86,92 @@ Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries ) return vLits; } + +/**Function************************************************************* + + Synopsis [Reads the file into a character buffer.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct buflist { + char buf[1<<20]; + int nBuf; + struct buflist * next; +} buflist; + +static char * Ioa_ReadLoadFileBz2Aig( char * pFileName ) +{ + FILE * pFile; + int nFileSize = 0; + char * pContents; + BZFILE * b; + int bzError; + struct buflist * pNext; + buflist * bufHead = NULL, * buf = NULL; + + pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Ioa_ReadLoadFileBz2(): The file is unavailable (absent or open).\n" ); + return NULL; + } + b = BZ2_bzReadOpen(&bzError,pFile,0,0,NULL,0); + if (bzError != BZ_OK) { + printf( "Ioa_ReadLoadFileBz2(): BZ2_bzReadOpen() failed with error %d.\n",bzError ); + return NULL; + } + do { + if (!bufHead) + buf = bufHead = ALLOC( buflist, 1 ); + else + buf = buf->next = ALLOC( buflist, 1 ); + nFileSize += buf->nBuf = BZ2_bzRead(&bzError,b,buf->buf,1<<20); + buf->next = NULL; + } while (bzError == BZ_OK); + if (bzError == BZ_STREAM_END) { + // we're okay + char * p; + int nBytes = 0; + BZ2_bzReadClose(&bzError,b); + p = pContents = ALLOC( char, nFileSize + 10 ); + buf = bufHead; + do { + memcpy(p+nBytes,buf->buf,buf->nBuf); + nBytes += buf->nBuf; +// } while((buf = buf->next)); + pNext = buf->next; + free( buf ); + } while((buf = pNext)); + } else if (bzError == BZ_DATA_ERROR_MAGIC) { + // not a BZIP2 file + BZ2_bzReadClose(&bzError,b); + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + if ( nFileSize == 0 ) + { + printf( "Ioa_ReadLoadFileBz2(): The file is empty.\n" ); + return NULL; + } + pContents = ALLOC( char, nFileSize + 10 ); + rewind( pFile ); + fread( pContents, nFileSize, 1, pFile ); + } else { + // Some other error. + printf( "Ioa_ReadLoadFileBz2(): Unable to read the compressed BLIF.\n" ); + return NULL; + } + fclose( pFile ); + // finish off the file with the spare .end line + // some benchmarks suddenly break off without this line + strcpy( pContents + nFileSize, "\n.end\n" ); + return pContents; +} + /**Function************************************************************* Synopsis [Reads the AIG in the binary AIGER format.] @@ -109,11 +196,18 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) unsigned uLit0, uLit1, uLit; // read the file into the buffer - nFileSize = Extra_FileSize( pFileName ); - pFile = fopen( pFileName, "rb" ); - pContents = ALLOC( char, nFileSize ); - fread( pContents, nFileSize, 1, pFile ); - fclose( pFile ); + if ( !strncmp(pFileName+strlen(pFileName)-4,".bz2",4) ) + pContents = Ioa_ReadLoadFileBz2Aig( pFileName ); + else + { +// pContents = Ioa_ReadLoadFile( pFileName ); + nFileSize = Extra_FileSize( pFileName ); + pFile = fopen( pFileName, "rb" ); + pContents = ALLOC( char, nFileSize ); + fread( pContents, nFileSize, 1, pFile ); + fclose( pFile ); + } + // check if the input file format is correct if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') ) diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index fb107e77..9e5ee8b4 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -21,6 +21,13 @@ #include "ioAbc.h" +#include +#include + +#ifdef _WIN32 +#define vsnprintf _vsnprintf +#endif + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -248,7 +255,7 @@ Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits ) SeeAlso [] ***********************************************************************/ -void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ) +void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ) { ProgressBar * pProgress; FILE * pFile; @@ -258,6 +265,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f unsigned uLit0, uLit1, uLit; assert( Abc_NtkIsStrash(pNtk) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( !Abc_LatchIsInit0(pObj) ) + { + fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); + return; + } + // start the output stream pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) @@ -265,12 +279,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); return; } - Abc_NtkForEachLatch( pNtk, pObj, i ) - if ( !Abc_LatchIsInit0(pObj) ) - { - fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); - return; - } // set the node numbers to be used in the output file nNodes = 0; @@ -368,6 +376,246 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f fclose( pFile ); } + +/**Function************************************************************* + + Synopsis [Procedure to write data into BZ2 file.] + + Description [Based on the vsnprintf() man page.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct bz2file { + FILE * f; + BZFILE * b; + char * buf; + int nBytes; + int nBytesMax; +} bz2file; + +int fprintfBz2Aig( bz2file * b, char * fmt, ... ) { + if (b->b) { + char * newBuf; + int bzError; + va_list ap; + while (1) { + va_start(ap,fmt); + b->nBytes = vsnprintf(b->buf,b->nBytesMax,fmt,ap); + va_end(ap); + if (b->nBytes > -1 && b->nBytes < b->nBytesMax) + break; + if (b->nBytes > -1) + b->nBytesMax = b->nBytes + 1; + else + b->nBytesMax *= 2; + if ((newBuf = REALLOC( char,b->buf,b->nBytesMax )) == NULL) + return -1; + else + b->buf = newBuf; + } + BZ2_bzWrite( &bzError, b->b, b->buf, b->nBytes ); + if (bzError == BZ_IO_ERROR) { + fprintf( stdout, "Ioa_WriteBlif(): I/O error writing to compressed stream.\n" ); + return -1; + } + return b->nBytes; + } else { + int n; + va_list ap; + va_start(ap,fmt); + n = vfprintf( b->f, fmt, ap); + va_end(ap); + return n; + } +} + +/**Function************************************************************* + + Synopsis [Writes the AIG in the binary AIGER format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ) +{ + ProgressBar * pProgress; +// FILE * pFile; + Abc_Obj_t * pObj, * pDriver; + int i, nNodes, Pos, nBufferSize, bzError; + unsigned char * pBuffer; + unsigned uLit0, uLit1, uLit; + bz2file b; + + // check that the network is valid + assert( Abc_NtkIsStrash(pNtk) ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( !Abc_LatchIsInit0(pObj) ) + { + fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); + return; + } + + memset(&b,0,sizeof(b)); + b.nBytesMax = (1<<12); + b.buf = ALLOC( char,b.nBytesMax ); + + // start the output stream + b.f = fopen( pFileName, "wb" ); + if ( b.f == NULL ) + { + fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName ); + FREE(b.buf); + return; + } + if (!strncmp(pFileName+strlen(pFileName)-4,".bz2",4)) { + b.b = BZ2_bzWriteOpen( &bzError, b.f, 9, 0, 0 ); + if ( bzError != BZ_OK ) { + BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL ); + fprintf( stdout, "Ioa_WriteBlif(): Cannot start compressed stream.\n" ); + fclose( b.f ); + FREE(b.buf); + return; + } + } + + // set the node numbers to be used in the output file + nNodes = 0; + Io_ObjSetAigerNum( Abc_AigConst1(pNtk), nNodes++ ); + Abc_NtkForEachCi( pNtk, pObj, i ) + Io_ObjSetAigerNum( pObj, nNodes++ ); + Abc_AigForEachAnd( pNtk, pObj, i ) + Io_ObjSetAigerNum( pObj, nNodes++ ); + + // write the header "M I L O A" where M = I + L + A + fprintfBz2Aig( &b, "aig%s %u %u %u %u %u\n", + fCompact? "2" : "", + Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), + Abc_NtkPiNum(pNtk), + Abc_NtkLatchNum(pNtk), + Abc_NtkPoNum(pNtk), + Abc_NtkNodeNum(pNtk) ); + + // if the driver node is a constant, we need to complement the literal below + // because, in the AIGER format, literal 0/1 is represented as number 0/1 + // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0 + + if ( !fCompact ) + { + // write latch drivers + Abc_NtkForEachLatchInput( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + } + // write PO drivers + Abc_NtkForEachPo( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + } + } + else + { + Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk ); + Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits ); + if ( !b.b ) + fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), b.f ); + else + { + BZ2_bzWrite( &bzError, b.b, Vec_StrArray(vBinary), Vec_StrSize(vBinary) ); + if (bzError == BZ_IO_ERROR) { + fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" ); + fclose( b.f ); + FREE(b.buf); + return; + } + } + Vec_StrFree( vBinary ); + Vec_IntFree( vLits ); + } + + // write the nodes into the buffer + Pos = 0; + nBufferSize = 6 * Abc_NtkNodeNum(pNtk) + 100; // skeptically assuming 3 chars per one AIG edge + pBuffer = ALLOC( unsigned char, nBufferSize ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + uLit = Io_ObjMakeLit( Io_ObjAigerNum(pObj), 0 ); + uLit0 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin0(pObj)), Abc_ObjFaninC0(pObj) ); + uLit1 = Io_ObjMakeLit( Io_ObjAigerNum(Abc_ObjFanin1(pObj)), Abc_ObjFaninC1(pObj) ); + assert( uLit0 < uLit1 ); + Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) ); + Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) ); + if ( Pos > nBufferSize - 10 ) + { + printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); + fclose( b.f ); + FREE(b.buf); + return; + } + } + assert( Pos < nBufferSize ); + Extra_ProgressBarStop( pProgress ); + + // write the buffer + if ( !b.b ) + fwrite( pBuffer, 1, Pos, b.f ); + else + { + BZ2_bzWrite( &bzError, b.b, pBuffer, Pos ); + if (bzError == BZ_IO_ERROR) { + fprintf( stdout, "Io_WriteAiger(): I/O error writing to compressed stream.\n" ); + fclose( b.f ); + FREE(b.buf); + return; + } + } + free( pBuffer ); + + // write the symbol table + if ( fWriteSymbols ) + { + // write PIs + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintfBz2Aig( &b, "i%d %s\n", i, Abc_ObjName(pObj) ); + // write latches + Abc_NtkForEachLatch( pNtk, pObj, i ) + fprintfBz2Aig( &b, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) ); + // write POs + Abc_NtkForEachPo( pNtk, pObj, i ) + fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) ); + } + + // write the comment + fprintfBz2Aig( &b, "c\n" ); + if ( pNtk->pName && strlen(pNtk->pName) > 0 ) + fprintfBz2Aig( &b, ".model %s\n", pNtk->pName ); + fprintfBz2Aig( &b, "This file was produced by ABC on %s\n", Extra_TimeStamp() ); + fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); + + // close the file + if (b.b) { + BZ2_bzWriteClose( &bzError, b.b, 0, NULL, NULL ); + if (bzError == BZ_IO_ERROR) { + fprintf( stdout, "Io_WriteAiger(): I/O error closing compressed stream.\n" ); + fclose( b.f ); + FREE(b.buf); + return; + } + } + fclose( b.f ); + FREE(b.buf); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3