Version abc61216

7 files changed, 716 insertions, 18 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index b1ea03c1..f6d71d52 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static int IoCommandRead        ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadAiger   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBaf     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -37,6 +38,7 @@ static int IoCommandReadVerLib  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 
+static int IoCommandWriteAiger  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBaf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBench  ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -71,6 +73,7 @@ extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fC
 void Io_Init( Abc_Frame_t * pAbc )
 {
     Cmd_CommandAdd( pAbc, "I/O", "read",          IoCommandRead,         1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_aiger",    IoCommandReadAiger,    1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_baf",      IoCommandReadBaf,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_bench",    IoCommandReadBench,    1 );
@@ -82,6 +85,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
 
+    Cmd_CommandAdd( pAbc, "I/O", "write_aiger",   IoCommandWriteAiger,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_baf",     IoCommandWriteBaf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
@@ -157,7 +161,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -177,7 +181,80 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pAbc->Err, "usage: read [-ch] <file>\n" );
-    fprintf( pAbc->Err, "\t         read the network from file in Verilog/BLIF/BENCH format\n" );
+    fprintf( pAbc->Err, "\t         read the network from file in BLIF/BENCH/PLA/BAF/AIGER format\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadAiger( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+
+    fCheck = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+ 
+    // set the new network
+    pNtk = Io_ReadAiger( FileName, fCheck );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from the AIGER file has failed.\n" );
+        return 1;
+    }
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_aiger [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
@@ -229,7 +306,7 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -240,7 +317,7 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pNtk = Io_ReadBaf( FileName, fCheck );
     if ( pNtk == NULL )
     {
-        fprintf( pAbc->Err, "Reading network from BAF file has failed.\n" );
+        fprintf( pAbc->Err, "Reading network from the BAF file has failed.\n" );
         return 1;
     }
 
@@ -302,7 +379,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -383,7 +460,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -463,7 +540,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -543,7 +620,7 @@ int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -626,7 +703,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -709,7 +786,7 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -799,7 +876,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -875,7 +952,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".blif", ".bench", ".pla", ".baf", ".aig" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -992,6 +1069,65 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    int c;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+    FileName = argv[globalUtilOptind];
+
+    // check the network type
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pAbc->Out, "Writing AIGER is only possible for structurally hashed AIGs.\n" );
+        return 0;
+    }
+    Io_WriteAiger( pNtk, FileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_aiger [-lh] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
@@ -1026,7 +1162,7 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
     // check the network type
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pAbc->Out, "Currently can only write strashed combinational AIGs.\n" );
+        fprintf( pAbc->Out, "Writing BAF is only possible for structurally hashed AIGs.\n" );
         return 0;
     }
     Io_WriteBaf( pNtk, FileName );
@@ -1036,7 +1172,7 @@ usage:
     fprintf( pAbc->Err, "usage: write_baf [-lh] <file>\n" );
     fprintf( pAbc->Err, "\t         write the network into a BLIF file\n" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .baf)\n" );
     return 1;
 }
 
@@ -1102,7 +1238,7 @@ usage:
     fprintf( pAbc->Err, "\t         write the network into a BLIF file\n" );
     fprintf( pAbc->Err, "\t-l     : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .blif)\n" );
     return 1;
 }
 
@@ -1176,7 +1312,7 @@ usage:
     fprintf( pAbc->Err, "\t         write the network in BENCH format\n" );
 //    fprintf( pAbc->Err, "\t-l     : toggle writing latches [default = %s]\n", fWriteLatches? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .bench)\n" );
     return 1;
 }
 
diff --git a/src/base/io/io.h b/src/base/io/io.h
index e7971b8d..776a1b2d 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -51,6 +51,8 @@ extern "C" {
 
 /*=== abcRead.c ==========================================================*/
 extern Abc_Ntk_t *        Io_Read( char * pFileName, int fCheck );
+/*=== abcReadAiger.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadAiger( char * pFileName, int fCheck );
 /*=== abcReadBaf.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadBaf( char * pFileName, int fCheck );
 /*=== abcReadBlif.c ==========================================================*/
@@ -75,6 +77,8 @@ extern Abc_Obj_t *        Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bo
 extern Abc_Obj_t *        Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
 extern Abc_Obj_t *        Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut );
 extern FILE *             Io_FileOpen( const char * FileName, const char * PathVar, const char * Mode, int fVerbose );
+/*=== abcWriteAiger.c ==========================================================*/
+extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBaf.c ==========================================================*/
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBlif.c ==========================================================*/
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 33f23796..36619a19 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -60,6 +60,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
         pNtk = Io_ReadEqn( pFileName, fCheck );
     else if ( Extra_FileNameCheckExtension( pFileName, "baf" ) )
         return Io_ReadBaf( pFileName, fCheck );
+    else if ( Extra_FileNameCheckExtension( pFileName, "aig" ) )
+        return Io_ReadAiger( pFileName, fCheck );
     else 
     {
         fprintf( stderr, "Unknown file format\n" );
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
new file mode 100644
index 00000000..b581aa0f
--- /dev/null
+++ b/src/base/io/ioReadAiger.c
@@ -0,0 +1,273 @@
+/**CFile****************************************************************
+
+  FileName    [ioReadAiger.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to read binary AIGER format developed by
+  Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - December 16, 2006.]
+
+  Revision    [$Id: ioReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned Io_ReadAigerDecode( char ** ppPos );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
+{
+    ProgressBar * pProgress;
+    FILE * pFile;
+    Vec_Ptr_t * vNodes, * vTerms;
+    Abc_Obj_t * pObj, * pNode0, * pNode1;
+    Abc_Ntk_t * pNtkNew;
+    int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, iTerm, nDigits, i;
+    char * pContents, * pDrivers, * pSymbols, * pCur, * pName, * pType;
+    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 );
+
+    // check if the input file format is correct
+    if ( strncmp(pContents, "aig", 3) != 0 )
+    {
+        fprintf( stdout, "Wrong input file format." );
+        return NULL;
+    }
+
+    // allocate the empty AIG
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pName = Extra_FileNameGeneric( pFileName );
+    pNtkNew->pName = Extra_UtilStrsav( pName );
+    pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
+    free( pName );
+
+
+    // read the file type
+    pCur = pContents;         while ( *pCur++ != ' ' );
+    // read the number of objects
+    nTotal = atoi( pCur );    while ( *pCur++ != ' ' );
+    // read the number of inputs
+    nInputs = atoi( pCur );   while ( *pCur++ != ' ' );
+    // read the number of latches
+    nLatches = atoi( pCur );  while ( *pCur++ != ' ' );
+    // read the number of outputs
+    nOutputs = atoi( pCur );  while ( *pCur++ != ' ' );
+    // read the number of nodes
+    nAnds = atoi( pCur );     while ( *pCur++ != '\n' );  
+    // check the parameters
+    if ( nTotal != nInputs + nLatches + nAnds )
+    {
+        fprintf( stdout, "The paramters are wrong." );
+        return NULL;
+    }
+
+    // prepare the array of nodes
+    vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
+    Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) );
+
+    // create the PIs
+    for ( i = 0; i < nInputs; i++ )
+    {
+        pObj = Abc_NtkCreatePi(pNtkNew);    
+        Vec_PtrPush( vNodes, pObj );
+    }
+    // create the POs
+    for ( i = 0; i < nOutputs; i++ )
+    {
+        pObj = Abc_NtkCreatePo(pNtkNew);   
+    }
+    // create the latches
+    nDigits = Extra_Base10Log( nLatches );
+    for ( i = 0; i < nLatches; i++ )
+    {
+        pObj = Abc_NtkCreateLatch(pNtkNew);
+        Abc_LatchSetInit0( pObj );
+        pNode0 = Abc_NtkCreateBi(pNtkNew);
+        pNode1 = Abc_NtkCreateBo(pNtkNew);
+        Abc_ObjAddFanin( pObj, pNode0 );
+        Abc_ObjAddFanin( pNode1, pObj );
+        Vec_PtrPush( vNodes, pNode1 );
+        // assign names to latch and its input
+        Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
+    } 
+    
+    // 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++;
+
+    // create the AND gates
+    pProgress = Extra_ProgressBarStart( stdout, nAnds );
+    for ( i = 0; i < nAnds; i++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        uLit = ((i + 1 + nInputs + nLatches) << 1);
+        uLit1 = uLit  - Io_ReadAigerDecode( &pCur );
+        uLit0 = uLit1 - Io_ReadAigerDecode( &pCur );
+        assert( uLit1 > uLit0 );
+        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
+        pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
+        assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches );
+        Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // remember the place where symbols begin
+    pSymbols = pCur;
+
+    // read the latch driver literals
+    pCur = pDrivers;
+    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 names if present
+    pCur = pSymbols;
+    while ( pCur < pContents + nFileSize && *pCur != 'c' )
+    {
+        // get the terminal type
+        pType = pCur;
+        if ( *pCur == 'i' )
+            vTerms = pNtkNew->vPis;
+        else if ( *pCur == 'l' )
+            vTerms = pNtkNew->vBoxes;
+        else if ( *pCur == 'o' )
+            vTerms = pNtkNew->vPos;
+        else
+        {
+            fprintf( stdout, "Wrong terminal type." );
+            return NULL;
+        }
+        // get the terminal number
+        iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
+        // get the node
+        if ( iTerm >= Vec_PtrSize(vTerms) )
+        {
+            fprintf( stdout, "The number of terminal is out of bound." );
+            return NULL;
+        }
+        pObj = Vec_PtrEntry( vTerms, iTerm );
+        if ( *pType == 'l' )
+            pObj = Abc_ObjFanout0(pObj);
+        // assign the name
+        pName = pCur;          while ( *pCur++ != '\n' );
+        // assign this name
+        *(pCur-1) = 0;
+        Abc_ObjAssignName( pObj, pName, NULL );
+        if ( *pType == 'l' )
+            Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" );
+        // mark the node as named
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    }
+    // skipping the comments
+    free( pContents );
+    Vec_PtrFree( vNodes );
+
+    // assign the remaining names
+    Abc_NtkForEachPi( pNtkNew, pObj, i )
+    {
+        if ( pObj->pCopy ) continue;
+        Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+    }
+    Abc_NtkForEachLatchOutput( pNtkNew, pObj, i )
+    {
+        if ( pObj->pCopy ) continue;
+        Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+        Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL );
+    }
+    Abc_NtkForEachPo( pNtkNew, pObj, i )
+    {
+        if ( pObj->pCopy ) continue;
+        Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL );
+    }
+
+    // remove the extra nodes
+//    Abc_AigCleanup( pNtkNew->pManFunc );
+
+    // check the result
+    if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
+    {
+        printf( "Io_ReadAiger: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+/**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/ioReadBaf.c b/src/base/io/ioReadBaf.c
index a6e0c2e2..8dce54af 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the AIG in the binary format.]
+  Synopsis    [Reads the AIG in the binary format.]
 
   Description []
   
@@ -150,7 +150,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
     Vec_PtrFree( vNodes );
 
     // remove the extra nodes
-    Abc_AigCleanup( pNtkNew->pManFunc );
+//    Abc_AigCleanup( pNtkNew->pManFunc );
 
     // check the result
     if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
new file mode 100644
index 00000000..2bc2ded3
--- /dev/null
+++ b/src/base/io/ioWriteAiger.c
@@ -0,0 +1,281 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteAiger.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write binary AIGER format developed by
+  Armin Biere, Johannes Kepler University (http://fmv.jku.at/)]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - December 16, 2006.]
+
+  Revision    [$Id: ioWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+    The following is taken from the AIGER format description, 
+    which can be found at http://fmv.jku.at/aiger
+*/
+
+
+/*
+         The AIGER And-Inverter Graph (AIG) Format Version 20061129
+         ----------------------------------------------------------
+              Armin Biere, Johannes Kepler University, 2006
+
+  This report describes the AIG file format as used by the AIGER library.
+  The purpose of this report is not only to motivate and document the
+  format, but also to allow independent implementations of writers and
+  readers by giving precise and unambiguous definitions.
+
+  ...
+
+Introduction
+
+  The name AIGER contains as one part the acronym AIG of And-Inverter
+  Graphs and also if pronounced in German sounds like the name of the
+  'Eiger', a mountain in the Swiss alps.  This choice should emphasize the
+  origin of this format. It was first openly discussed at the Alpine
+  Verification Meeting 2006 in Ascona as a way to provide a simple, compact
+  file format for a model checking competition affiliated to CAV 2007.
+
+  ...
+
+Binary Format Definition
+
+  The binary format is semantically a subset of the ASCII format with a
+  slightly different syntax.  The binary format may need to reencode
+  literals, but translating a file in binary format into ASCII format and
+  then back in to binary format will result in the same file.
+
+  The main differences of the binary format to the ASCII format are as
+  follows.  After the header the list of input literals and all the
+  current state literals of a latch can be omitted.  Furthermore the
+  definitions of the AND gates are binary encoded.  However, the symbol
+  table and the comment section are as in the ASCII format.
+
+  The header of an AIGER file in binary format has 'aig' as format
+  identifier, but otherwise is identical to the ASCII header.  The standard
+  file extension for the binary format is therefore '.aig'. 
+  
+  A header for the binary format is still in ASCII encoding:
+
+    aig M I L O A
+
+  Constants, variables and literals are handled in the same way as in the
+  ASCII format.  The first simplifying restriction is on the variable
+  indices of inputs and latches.  The variable indices of inputs come first,
+  followed by the pseudo-primary inputs of the latches and then the variable
+  indices of all LHS of AND gates:
+
+    input variable indices        1,          2,  ... ,  I
+    latch variable indices      I+1,        I+2,  ... ,  (I+L)
+    AND variable indices      I+L+1,      I+L+2,  ... ,  (I+L+A) == M
+
+  The corresponding unsigned literals are
+
+    input literals                2,          4,  ... ,  2*I
+    latch literals            2*I+2,      2*I+4,  ... ,  2*(I+L)
+    AND literals          2*(I+L)+2,  2*(I+L)+4,  ... ,  2*(I+L+A) == 2*M
+                    
+  All literals have to be defined, and therefore 'M = I + L + A'.  With this
+  restriction it becomes possible that the inputs and the current state
+  literals of the latches do not have to be listed explicitly.  Therefore,
+  after the header only the list of 'L' next state literals follows, one per
+  latch on a single line, and then the 'O' outputs, again one per line.
+
+  In the binary format we assume that the AND gates are ordered and respect
+  the child parent relation.  AND gates with smaller literals on the LHS
+  come first.  Therefore we can assume that the literals on the right-hand
+  side of a definition of an AND gate are smaller than the LHS literal.
+  Furthermore we can sort the literals on the RHS, such that the larger
+  literal comes first.  A definition thus consists of three literals
+    
+      lhs rhs0 rhs1
+
+  with 'lhs' even and 'lhs > rhs0 >= rhs1'.  Also the variable indices are
+  pairwise different to avoid combinational self loops.  Since the LHS
+  indices of the definitions are all consecutive (as even integers),
+  the binary format does not have to keep 'lhs'.  In addition, we can use
+  the order restriction and only write the differences 'delta0' and 'delta1'
+  instead of 'rhs0' and 'rhs1', with
+
+      delta0 = lhs - rhs0,  delta1 = rhs0 - rhs1
+  
+  The differences will all be strictly positive, and in practice often very
+  small.  We can take advantage of this fact by the simple little-endian
+  encoding of unsigned integers of the next section.  After the binary delta
+  encoding of the RHSs of all AND gates, the optional symbol table and
+  optional comment section start in the same format as in the ASCII case.
+
+  ...
+
+*/
+
+static unsigned Io_ObjMakeLit( int Var, int fCompl )                 { return (Var << 1) | fCompl;    }
+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;     }
+
+static int      Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    ProgressBar * pProgress;
+    FILE * pFile;
+    Abc_Obj_t * pObj, * pDriver;
+    int i, nNodes, Pos, nBufferSize;
+    unsigned char * pBuffer;
+    unsigned uLit0, uLit1, uLit;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the output stream
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteBaf(): Cannot open the output file \"%s\".\n", pFileName );
+        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
+    fprintf( pFile, "aig %u %u %u %u %u\n", 
+        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
+
+    // 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 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 );
+    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, uLit  - uLit1 );
+        Pos = Io_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 );
+        if ( Pos > nBufferSize - 10 )
+        {
+            printf( "Io_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" );
+            fclose( pFile );
+            return;
+        }
+    }
+    assert( Pos < nBufferSize );
+    Extra_ProgressBarStop( pProgress );
+
+    // write the buffer
+    fwrite( pBuffer, 1, Pos, pFile );
+    free( pBuffer );
+
+    // write the symbol table
+    // write PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        fprintf( pFile, "i%d %s\n", i, Abc_ObjName(pObj) );
+    // write latches
+    Abc_NtkForEachLatch( pNtk, pObj, 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) );
+
+    // write the comment
+    fprintf( pFile, "c\n" );
+    fprintf( pFile, "%s\n", pNtk->pName );
+    fprintf( pFile, "This file in the AIGER format was written by ABC on %s\n", Extra_TimeStamp() );
+    fprintf( pFile, "For information about the format, refer to %s\n", "http://fmv.jku.at/aiger" );
+    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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 2d5e4b9e..1feffa0b 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -1,5 +1,6 @@
 SRC +=  src/base/io/io.c \
     src/base/io/ioRead.c \
+    src/base/io/ioReadAiger.c \
     src/base/io/ioReadBaf.c \
     src/base/io/ioReadBench.c \
     src/base/io/ioReadBlif.c \
@@ -8,6 +9,7 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioReadPla.c \
     src/base/io/ioReadVerilog.c \
     src/base/io/ioUtil.c \
+    src/base/io/ioWriteAiger.c \
     src/base/io/ioWriteBaf.c \
     src/base/io/ioWriteBench.c \
     src/base/io/ioWriteBlif.c \