summaryrefslogtreecommitdiffstats
path: root/src/base/io
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-01-21 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2008-01-21 08:01:00 -0800
commitd4fecf91efcd090caa9a5cbfb05059361e84c4ec (patch)
tree87dfc18934e7460a3be8c7cea0a587756e66aeb2 /src/base/io
parent61850d5942fcff634b16696bf3ca7ee0fc465d1c (diff)
downloadabc-d4fecf91efcd090caa9a5cbfb05059361e84c4ec.tar.gz
abc-d4fecf91efcd090caa9a5cbfb05059361e84c4ec.tar.bz2
abc-d4fecf91efcd090caa9a5cbfb05059361e84c4ec.zip
Version abc80121
Diffstat (limited to 'src/base/io')
-rw-r--r--src/base/io/io.c25
-rw-r--r--src/base/io/io.h2
-rw-r--r--src/base/io/ioReadAiger.c146
-rw-r--r--src/base/io/ioUtil.c2
-rw-r--r--src/base/io/ioWriteAiger.c174
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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-29 07:39:21 +0000