From 34ab59574ee4feedfd1ffb618e2e71a6a1964a6a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 3 Dec 2013 00:26:43 -0800 Subject: Suggested patch of AIG writers. --- src/aig/ioa/ioaWriteAig.c | 14 +++-- src/base/io/ioWriteAiger.c | 136 +++++++++++++++++++++++++++++++++++---------- 2 files changed, 116 insertions(+), 34 deletions(-) diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c index e6207879..bb0653b9 100644 --- a/src/aig/ioa/ioaWriteAig.c +++ b/src/aig/ioa/ioaWriteAig.c @@ -564,14 +564,20 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int if ( fWriteSymbols ) { // write PIs - Aig_ManForEachCi( pMan, pObj, i ) + Aig_ManForEachPiSeq( pMan, pObj, i ) fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) ); // write latches - Aig_ManForEachLatch( pMan, pObj, i ) + Aig_ManForEachLoSeq( pMan, pObj, i ) fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) ); // write POs - Aig_ManForEachCo( pMan, pObj, i ) - fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) ); + int bads = Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan); + Aig_ManForEachPoSeq( pMan, pObj, i ) + if ( !Aig_ManConstrNum(pMan) ) + fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) ); + else ( i < bads ) + fprintf( pFile, "b%d %s\n", i, Aig_ObjName(pObj) ); + else + fprintf( pFile, "c%d %s\n", i - bads, Aig_ObjName(pObj) ); } */ // write the comment diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 1f22b138..20689405 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -270,15 +270,22 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i { ProgressBar * pProgress; FILE * pFile; - Abc_Obj_t * pObj, * pDriver; - int i, nNodes, nBufferSize, Pos; + Abc_Obj_t * pObj, * pDriver, * pLatch; + int i, nNodes, nBufferSize, Pos, fExtended; unsigned char * pBuffer; unsigned uLit0, uLit1, uLit; + fExtended = Abc_NtkConstrNum(pNtk); + assert( Abc_NtkIsStrash(pNtk) ); Abc_NtkForEachLatch( pNtk, pObj, i ) if ( !Abc_LatchIsInit0(pObj) ) { + if ( !fCompact ) + { + fExtended = 1; + break; + } fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); return; } @@ -305,10 +312,10 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), Abc_NtkPiNum(pNtk), Abc_NtkLatchNum(pNtk), - Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk), + fExtended ? 0 : Abc_NtkPoNum(pNtk), Abc_NtkNodeNum(pNtk) ); // write the extended header "B C J F" - if ( Abc_NtkConstrNum(pNtk) ) + if ( fExtended ) fprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) ); fprintf( pFile, "\n" ); @@ -320,10 +327,21 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i if ( !fCompact ) { // write latch drivers - Abc_NtkForEachLatchInput( pNtk, pObj, i ) + Abc_NtkForEachLatch( pNtk, pLatch, i ) { + pObj = Abc_ObjFanin0(pLatch); pDriver = Abc_ObjFanin0(pObj); - fprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ); + if ( Abc_LatchIsInit0(pLatch) ) + fprintf( pFile, "%u\n", uLit ); + else if ( Abc_LatchIsInit1(pLatch) ) + fprintf( pFile, "%u 1\n", uLit ); + else + { + // Both None and DC are written as 'uninitialized' e.g. a free boolean value + assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ); + fprintf( pFile, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(pLatch), 0 ) ); + } } // write PO drivers Abc_NtkForEachPo( pNtk, pObj, i ) @@ -353,7 +371,13 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i 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 ); + if ( uLit0 > uLit1 ) + { + unsigned Temp = uLit0; + uLit0 = uLit1; + uLit1 = Temp; + } + assert( uLit1 < uLit ); Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) ); Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) ); if ( Pos > nBufferSize - 10 ) @@ -381,7 +405,12 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i fprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) ); // write POs Abc_NtkForEachPo( pNtk, pObj, i ) - fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) ); + if ( !fExtended ) + fprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) ); + else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) ) + fprintf( pFile, "b%d %s\n", i, Abc_ObjName(pObj) ); + else + fprintf( pFile, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) ); } // write the comment @@ -408,8 +437,8 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) { ProgressBar * pProgress; gzFile pFile; - Abc_Obj_t * pObj, * pDriver; - int i, nNodes, Pos, nBufferSize; + Abc_Obj_t * pObj, * pDriver, * pLatch; + int i, nNodes, Pos, nBufferSize, fExtended; unsigned char * pBuffer; unsigned uLit0, uLit1, uLit; @@ -421,12 +450,8 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) fprintf( stdout, "Io_WriteAigerGz(): Cannot open the output file \"%s\".\n", pFileName ); return; } - Abc_NtkForEachLatch( pNtk, pObj, i ) - if ( !Abc_LatchIsInit0(pObj) ) - { - fprintf( stdout, "Io_WriteAigerGz(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); - return; - } + + fExtended = Abc_NtkConstrNum(pNtk); // set the node numbers to be used in the output file nNodes = 0; @@ -441,10 +466,10 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), Abc_NtkPiNum(pNtk), Abc_NtkLatchNum(pNtk), - Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk), + fExtended ? 0 : Abc_NtkPoNum(pNtk), Abc_NtkNodeNum(pNtk) ); // write the extended header "B C J F" - if ( Abc_NtkConstrNum(pNtk) ) + if ( fExtended ) gzprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) ); gzprintf( pFile, "\n" ); @@ -454,10 +479,21 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) // write latch drivers Abc_NtkInvertConstraints( pNtk ); - Abc_NtkForEachLatchInput( pNtk, pObj, i ) + Abc_NtkForEachLatch( pNtk, pLatch, i ) { + pObj = Abc_ObjFanin0(pLatch); pDriver = Abc_ObjFanin0(pObj); - gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ); + if ( Abc_LatchIsInit0(pLatch) ) + gzprintf( pFile, "%u\n", uLit ); + else if ( Abc_LatchIsInit1(pLatch) ) + gzprintf( pFile, "%u 1\n", uLit ); + else + { + // Both None and DC are written as 'uninitialized' e.g. a free boolean value + assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ); + gzprintf( pFile, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(pLatch), 0 ) ); + } } // write PO drivers Abc_NtkForEachPo( pNtk, pObj, i ) @@ -478,7 +514,13 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) 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 ); + if ( uLit0 > uLit1 ) + { + unsigned Temp = uLit0; + uLit0 = uLit1; + uLit1 = Temp; + } + assert( uLit1 < uLit ); Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); if ( Pos > nBufferSize - 10 ) @@ -506,7 +548,12 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) gzprintf( pFile, "l%d %s\n", i, Abc_ObjName(Abc_ObjFanout0(pObj)) ); // write POs Abc_NtkForEachPo( pNtk, pObj, i ) - gzprintf( pFile, "o%d %s\n", i, Abc_ObjName(pObj) ); + if ( !fExtended ) + gzprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) ); + else ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) ) + gzprintf( pFile, "b%d %s\n", i, Aig_ObjName(pObj) ); + else + gzprintf( pFile, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Aig_ObjName(pObj) ); } // write the comment @@ -589,8 +636,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f { ProgressBar * pProgress; // FILE * pFile; - Abc_Obj_t * pObj, * pDriver; - int i, nNodes, nBufferSize, bzError, Pos; + Abc_Obj_t * pObj, * pDriver, * pLatch; + int i, nNodes, nBufferSize, bzError, Pos, fExtended; unsigned char * pBuffer; unsigned uLit0, uLit1, uLit; bz2file b; @@ -602,11 +649,18 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f fCompact = 0; } + fExtended = Abc_NtkConstrNum(pNtk); + // check that the network is valid assert( Abc_NtkIsStrash(pNtk) ); Abc_NtkForEachLatch( pNtk, pObj, i ) if ( !Abc_LatchIsInit0(pObj) ) { + if ( !fCompact ) + { + fExtended = 1; + break; + } fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); return; } @@ -655,10 +709,10 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), Abc_NtkPiNum(pNtk), Abc_NtkLatchNum(pNtk), - Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk), + fExtended ? 0 : Abc_NtkPoNum(pNtk), Abc_NtkNodeNum(pNtk) ); // write the extended header "B C J F" - if ( Abc_NtkConstrNum(pNtk) ) + if ( fExtended ) fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) ); fprintfBz2Aig( &b, "\n" ); @@ -670,10 +724,21 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f if ( !fCompact ) { // write latch drivers - Abc_NtkForEachLatchInput( pNtk, pObj, i ) + Abc_NtkForEachLatch( pNtk, pLatch, i ) { + pObj = Abc_ObjFanin0(pLatch); pDriver = Abc_ObjFanin0(pObj); - fprintfBz2Aig( &b, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) ); + uLit = Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ); + if ( Abc_LatchIsInit0(pLatch) ) + fprintfBz2Aig( &b, "%u\n", uLit ); + else if ( Abc_LatchIsInit1(pLatch) ) + fprintfBz2Aig( &b, "%u 1\n", uLit ); + else + { + // Both None and DC are written as 'uninitialized' e.g. a free boolean value + assert( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ); + fprintfBz2Aig( &b, "%u %u\n", uLit, Io_ObjMakeLit( Io_ObjAigerNum(pLatch), 0 ) ); + } } // write PO drivers Abc_NtkForEachPo( pNtk, pObj, i ) @@ -715,7 +780,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f 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 ); + if ( uLit0 > uLit1 ) + { + unsigned Temp = uLit0; + uLit0 = uLit1; + uLit1 = Temp; + } + assert( uLit1 < uLit ); Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit - uLit1) ); Pos = Io_WriteAigerEncode( pBuffer, Pos, (unsigned)(uLit1 - uLit0) ); if ( Pos > nBufferSize - 10 ) @@ -756,7 +827,12 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f 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) ); + if ( !fExtended ) + fprintfBz2Aig( &b, "o%d %s\n", i, Abc_ObjName(pObj) ); + else if ( i < Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) ) + fprintfBz2Aig( &b, "b%d %s\n", i, Abc_ObjName(pObj) ); + else + fprintfBz2Aig( &b, "c%d %s\n", i - (Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk)), Abc_ObjName(pObj) ); } // write the comment -- cgit v1.2.3