diff options
Diffstat (limited to 'src/base/io')
-rw-r--r-- | src/base/io/io.c | 25 | ||||
-rw-r--r-- | src/base/io/io.h | 2 | ||||
-rw-r--r-- | src/base/io/ioReadAiger.c | 146 | ||||
-rw-r--r-- | src/base/io/ioUtil.c | 2 | ||||
-rw-r--r-- | src/base/io/ioWriteAiger.c | 174 |
5 files changed, 245 insertions, 104 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index ed314fcd..fe88a285 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1174,17 +1174,22 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; int fWriteSymbols; + int fCompact; int c; - fWriteSymbols = 1; + fCompact = 1; + fWriteSymbols = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF ) { switch ( c ) { case 's': fWriteSymbols ^= 1; break; + case 'c': + fCompact ^= 1; + break; case 'h': goto usage; default: @@ -1196,23 +1201,19 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv ) // get the output file name pFileName = argv[globalUtilOptind]; // call the corresponding file writer - if ( fWriteSymbols ) - Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_AIGER ); - else + if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) { - if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) - { - fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" ); - return 1; - } - Io_WriteAiger( pAbc->pNtkCur, pFileName, 0 ); + fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" ); + return 1; } + Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact ); return 0; usage: - fprintf( pAbc->Err, "usage: write_aiger [-sh] <file>\n" ); + fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" ); fprintf( pAbc->Err, "\t write the network in the AIGER format (http://fmv.jku.at/aiger)\n" ); fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" ); + fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" ); return 1; diff --git a/src/base/io/io.h b/src/base/io/io.h index 45762b77..126de332 100644 --- a/src/base/io/io.h +++ b/src/base/io/io.h @@ -87,7 +87,7 @@ extern Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck ); /*=== abcReadVerilog.c ========================================================*/ extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck ); /*=== abcWriteAiger.c =========================================================*/ -extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ); +extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ); /*=== abcWriteBaf.c ===========================================================*/ extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName ); /*=== abcWriteBlif.c ==========================================================*/ diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index 273b2d5a..4820bced 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -25,14 +25,68 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -unsigned Io_ReadAigerDecode( char ** ppPos ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Extracts one unsigned AIG edge from the input buffer.] + + Description [This procedure is a slightly modified version of Armin Biere's + procedure "unsigned decode (FILE * file)". ] + + SideEffects [Updates the current reading position.] + + SeeAlso [] + +***********************************************************************/ +unsigned Io_ReadAigerDecode( char ** ppPos ) +{ + unsigned x = 0, i = 0; + unsigned char ch; + +// while ((ch = getnoneofch (file)) & 0x80) + while ((ch = *(*ppPos)++) & 0x80) + x |= (ch & 0x7f) << (7 * i++); + + return x | (ch << (7 * i)); +} + +/**Function************************************************************* + + Synopsis [Decodes the encoded array of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries ) +{ + Vec_Int_t * vLits; + int Lit, LitPrev, Diff, i; + vLits = Vec_IntAlloc( nEntries ); + LitPrev = Io_ReadAigerDecode( ppPos ); + Vec_IntPush( vLits, LitPrev ); + for ( i = 1; i < nEntries; i++ ) + { +// Diff = Lit - LitPrev; +// Diff = (Lit < LitPrev)? -Diff : Diff; +// Diff = ((2 * Diff) << 1) | (int)(Lit < LitPrev); + Diff = Io_ReadAigerDecode( ppPos ); + Diff = (Diff & 1)? -(Diff >> 1) : Diff >> 1; + Lit = Diff + LitPrev; + Vec_IntPush( vLits, Lit ); + LitPrev = Lit; + } + return vLits; +} + +/**Function************************************************************* + Synopsis [Reads the AIG in the binary AIGER format.] Description [] @@ -47,6 +101,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) ProgressBar * pProgress; FILE * pFile; Vec_Ptr_t * vNodes, * vTerms; + Vec_Int_t * vLits = NULL; Abc_Obj_t * pObj, * pNode0, * pNode1; Abc_Ntk_t * pNtkNew; int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i; @@ -61,7 +116,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) fclose( pFile ); // check if the input file format is correct - if ( strncmp(pContents, "aig", 3) != 0 ) + if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') ) { fprintf( stdout, "Wrong input file format.\n" ); return NULL; @@ -125,13 +180,20 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) // printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); } - // remember the beginning of latch/PO literals - pDrivers = pCur; - // scroll to the beginning of the binary data - for ( i = 0; i < nLatches + nOutputs; ) - if ( *pCur++ == '\n' ) - i++; + if ( pContents[3] == ' ' ) // standard AIGER + { + // remember the beginning of latch/PO literals + pDrivers = pCur; + // scroll to the beginning of the binary data + for ( i = 0; i < nLatches + nOutputs; ) + if ( *pCur++ == '\n' ) + i++; + } + else // modified AIGER + { + vLits = Io_WriteDecodeLiterals( &pCur, nLatches + nOutputs ); + } // create the AND gates pProgress = Extra_ProgressBarStart( stdout, nAnds ); @@ -154,21 +216,39 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) // read the latch driver literals pCur = pDrivers; - Abc_NtkForEachLatchInput( pNtkNew, pObj, i ) + if ( pContents[3] == ' ' ) // standard AIGER { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); - Abc_ObjAddFanin( pObj, pNode0 ); - -// printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id ); - + Abc_NtkForEachLatchInput( pNtkNew, pObj, i ) + { + uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); + Abc_ObjAddFanin( pObj, pNode0 ); + } + // read the PO driver literals + Abc_NtkForEachPo( pNtkNew, pObj, i ) + { + uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); + Abc_ObjAddFanin( pObj, pNode0 ); + } } - // read the PO driver literals - Abc_NtkForEachPo( pNtkNew, pObj, i ) + else { - uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); - Abc_ObjAddFanin( pObj, pNode0 ); + // read the latch driver literals + Abc_NtkForEachLatchInput( pNtkNew, pObj, i ) + { + uLit0 = Vec_IntEntry( vLits, i ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + Abc_ObjAddFanin( pObj, pNode0 ); + } + // read the PO driver literals + Abc_NtkForEachPo( pNtkNew, pObj, i ) + { + uLit0 = Vec_IntEntry( vLits, i+Abc_NtkLatchNum(pNtkNew) ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + Abc_ObjAddFanin( pObj, pNode0 ); + } + Vec_IntFree( vLits ); } // read the names if present @@ -278,30 +358,6 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) } -/**Function************************************************************* - - Synopsis [Extracts one unsigned AIG edge from the input buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "unsigned decode (FILE * file)". ] - - SideEffects [Updates the current reading position.] - - SeeAlso [] - -***********************************************************************/ -unsigned Io_ReadAigerDecode( char ** ppPos ) -{ - unsigned x = 0, i = 0; - unsigned char ch; - -// while ((ch = getnoneofch (file)) & 0x80) - while ((ch = *(*ppPos)++) & 0x80) - x |= (ch & 0x7f) << (7 * i++); - - return x | (ch << (7 * i)); -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 94ec4316..4f9f2e9f 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -257,7 +257,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) return; } if ( FileType == IO_FILE_AIGER ) - Io_WriteAiger( pNtk, pFileName, 1 ); + Io_WriteAiger( pNtk, pFileName, 1, 0 ); else // if ( FileType == IO_FILE_BAF ) Io_WriteBaf( pNtk, pFileName ); return; diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index ff34b177..758e5335 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -129,14 +129,116 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (V static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj ) { return (unsigned)pObj->pCopy; } static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (void *)Num; } -int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Adds one unsigned AIG edge to the output buffer.] + + Description [This procedure is a slightly modified version of Armin Biere's + procedure "void encode (FILE * file, unsigned x)" ] + + SideEffects [Returns the current writing position.] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ) +{ + unsigned char ch; + while (x & ~0x7f) + { + ch = (x & 0x7f) | 0x80; +// putc (ch, file); + pBuffer[Pos++] = ch; + x >>= 7; + } + ch = x; +// putc (ch, file); + pBuffer[Pos++] = ch; + return Pos; +} + +/**Function************************************************************* + + Synopsis [Create the array of literals to be written.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Io_WriteAigerLiterals( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vLits; + Abc_Obj_t * pObj, * pDriver; + int i; + vLits = Vec_IntAlloc( Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachLatchInput( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + } + Abc_NtkForEachPo( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + Vec_IntPush( vLits, Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + } + return vLits; +} + +/**Function************************************************************* + + Synopsis [Creates the binary encoded array of literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Io_WriteEncodeLiterals( Vec_Int_t * vLits ) +{ + Vec_Str_t * vBinary; + int Pos = 0, Lit, LitPrev, Diff, i; + vBinary = Vec_StrAlloc( 2 * Vec_IntSize(vLits) ); + LitPrev = Vec_IntEntry( vLits, 0 ); + Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, LitPrev ); + Vec_IntForEachEntryStart( vLits, Lit, i, 1 ) + { + Diff = Lit - LitPrev; + Diff = (Lit < LitPrev)? -Diff : Diff; + Diff = (Diff << 1) | (int)(Lit < LitPrev); + Pos = Io_WriteAigerEncode( Vec_StrArray(vBinary), Pos, Diff ); + LitPrev = Lit; + if ( Pos + 10 > vBinary->nCap ) + Vec_StrGrow( vBinary, vBinary->nCap+1 ); + } + vBinary->nSize = Pos; +/* + // verify + { + extern Vec_Int_t * Io_WriteDecodeLiterals( char ** ppPos, int nEntries ); + char * pPos = Vec_StrArray( vBinary ); + Vec_Int_t * vTemp = Io_WriteDecodeLiterals( &pPos, Vec_IntSize(vLits) ); + for ( i = 0; i < Vec_IntSize(vLits); i++ ) + { + int Entry1 = Vec_IntEntry(vLits,i); + int Entry2 = Vec_IntEntry(vTemp,i); + assert( Entry1 == Entry2 ); + } + } +*/ + return vBinary; +} + +/**Function************************************************************* + Synopsis [Writes the AIG in the binary AIGER format.] Description [] @@ -146,7 +248,7 @@ int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); SeeAlso [] ***********************************************************************/ -void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) +void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact ) { ProgressBar * pProgress; FILE * pFile; @@ -179,7 +281,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) Io_ObjSetAigerNum( pObj, nNodes++ ); // write the header "M I L O A" where M = I + L + A - fprintf( pFile, "aig %u %u %u %u %u\n", + fprintf( pFile, "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), @@ -190,24 +293,34 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) // 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 - // write latch drivers - Abc_NtkForEachLatchInput( pNtk, pObj, i ) + if ( !fCompact ) { - pDriver = Abc_ObjFanin0(pObj); - fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + // write latch drivers + Abc_NtkForEachLatchInput( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + fprintf( pFile, "%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); + fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + } } - - // write PO drivers - Abc_NtkForEachPo( pNtk, pObj, i ) + else { - pDriver = Abc_ObjFanin0(pObj); - fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + Vec_Int_t * vLits = Io_WriteAigerLiterals( pNtk ); + Vec_Str_t * vBinary = Io_WriteEncodeLiterals( vLits ); + fwrite( Vec_StrArray(vBinary), 1, Vec_StrSize(vBinary), pFile ); + 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( char, nBufferSize ); + pBuffer = ALLOC( unsigned char, nBufferSize ); pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) ); Abc_AigForEachAnd( pNtk, pObj, i ) { @@ -216,8 +329,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) 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, uLit - uLit1 ); - Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); + 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" ); @@ -255,35 +368,6 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) fclose( pFile ); } -/**Function************************************************************* - - Synopsis [Adds one unsigned AIG edge to the output buffer.] - - Description [This procedure is a slightly modified version of Armin Biere's - procedure "void encode (FILE * file, unsigned x)" ] - - SideEffects [Returns the current writing position.] - - SeeAlso [] - -***********************************************************************/ -int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ) -{ - unsigned char ch; - while (x & ~0x7f) - { - ch = (x & 0x7f) | 0x80; -// putc (ch, file); - pBuffer[Pos++] = ch; - x >>= 7; - } - ch = x; -// putc (ch, file); - pBuffer[Pos++] = ch; - return Pos; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |