Version abc51010

8 files changed, 690 insertions, 0 deletions

diff --git a/src/base/abcs/abcSeqMan.c b/src/base/abcs/abcSeqMan.c
new file mode 100644
index 00000000..b5db4bef
--- /dev/null
+++ b/src/base/abcs/abcSeqMan.c
@@ -0,0 +1,218 @@
+/**CFile****************************************************************
+
+  FileName    [abcSeqMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Manager of sequential AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcSeqMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_SeqLat_t_  Abc_SeqLat_t;
+struct Abc_SeqLat_t_
+{
+    Abc_SeqLat_t *      pNext;    // the next Lat in the ring
+    Abc_SeqLat_t *      pPrev;    // the prev Lat in the ring 
+};
+
+typedef struct Abc_SeqMan_t_  Abc_SeqMan_t;
+struct Abc_SeqMan_t_
+{
+    int                 nSize;           // the number of entries in all internal arrays
+    Vec_Ptr_t *         vInits;          // the initial states for each edge in the AIG
+    Extra_MmFixed_t *   pMmInits;        // memory manager for initial states of the Lates
+
+};
+
+// reading the contents of the lat
+static inline Abc_InitType_t Abc_SeqLatInit( Abc_SeqLat_t * pLat )  {  return ((unsigned)pLat->pPrev) & 3;                                 }
+static inline Abc_SeqLat_t * Abc_SeqLatNext( Abc_SeqLat_t * pLat )  {  return pLat->pNext;                                                 }
+static inline Abc_SeqLat_t * Abc_SeqLatPrev( Abc_SeqLat_t * pLat )  {  return (void *)(((unsigned)pLat->pPrev) & (ABC_FULL_MASK << 2));    }
+
+// setting the contents of the lat
+static inline void           Abc_SeqLatSetInit( Abc_SeqLat_t * pLat, Abc_InitType_t Init )  { pLat->pPrev = (void *)( (3 & Init) | (((unsigned)pLat->pPrev) & (ABC_FULL_MASK << 2)) );          }
+static inline void           Abc_SeqLatSetNext( Abc_SeqLat_t * pLat, Abc_SeqLat_t * pNext ) { pLat->pNext = pNext;                                                                              }
+static inline void           Abc_SeqLatSetPrev( Abc_SeqLat_t * pLat, Abc_SeqLat_t * pPrev ) { Abc_InitType_t Init = Abc_SeqLatInit(pLat);  pLat->pPrev = pPrev;  Abc_SeqLatSetInit(pLat, Init); }
+
+// accessing initial state datastructure
+static inline Vec_Ptr_t *    Abc_SeqNodeInits( Abc_Obj_t * pObj )                                    { return ((Abc_SeqMan_t*)pObj->pNtk->pManFunc)->vInits;                           }
+static inline Abc_SeqLat_t * Abc_SeqNodeReadInit( Abc_Obj_t * pObj, int Edge )                       { return Vec_PtrEntry( Abc_SeqNodeInits(pObj), (pObj->Id<<1)+Edge );              }
+static inline void           Abc_SeqNodeSetInit ( Abc_Obj_t * pObj, int Edge, Abc_SeqLat_t * pInit ) { Vec_PtrWriteEntry( Abc_SeqNodeInits(pObj), (pObj->Id<<1)+Edge, pInit );         }
+static inline Abc_SeqLat_t * Abc_SeqNodeCreateLat( Abc_Obj_t * pObj )                                { return (Abc_SeqLat_t *)Extra_MmFixedEntryFetch( ((Abc_SeqMan_t*)pObj->pNtk->pManFunc)->pMmInits );  }
+static inline void           Abc_SeqNodeRecycleLat( Abc_Obj_t * pObj, Abc_SeqLat_t * pLat )          { Extra_MmFixedEntryRecycle( ((Abc_SeqMan_t*)pObj->pNtk->pManFunc)->pMmInits, (char *)pLat );         }
+
+// getting the Lat with the given number
+static inline Abc_SeqLat_t * Abc_SeqNodeGetLat( Abc_Obj_t * pObj, int Edge, int iLat )  
+{
+    int Counter;
+    Abc_SeqLat_t * pLat = Abc_SeqNodeReadInit(pObj, Edge);  
+    for ( Counter = 0; Counter != iLat; Counter++ )
+        pLat = pLat->pNext;
+    return pLat;
+}
+// getting the first Lat
+static inline Abc_SeqLat_t * Abc_SeqNodeGetLatFirst( Abc_Obj_t * pObj, int Edge )  
+{
+    return Abc_SeqNodeReadInit(pObj, Edge);
+}
+// getting the last Lat
+static inline Abc_SeqLat_t * Abc_SeqNodeGetLatLast( Abc_Obj_t * pObj, int Edge )  
+{
+    return Abc_SeqLatPrev( Abc_SeqNodeReadInit(pObj, Edge) );
+}
+
+// getting the init value of the given Lat on the edge
+static inline Abc_InitType_t Abc_SeqNodeGetInitOne( Abc_Obj_t * pObj, int Edge, int iLat )             
+{  
+    return Abc_SeqLatInit( Abc_SeqNodeGetLat(pObj, Edge, iLat) );  
+}
+// geting the init value of the first Lat on the edge
+static inline Abc_InitType_t Abc_SeqNodeGetInitFirst( Abc_Obj_t * pObj, int Edge )  
+{
+    return Abc_SeqLatInit( Abc_SeqNodeGetLatFirst(pObj, Edge) );  
+}
+// geting the init value of the last Lat on the edge
+static inline Abc_InitType_t Abc_SeqNodeGetInitLast( Abc_Obj_t * pObj, int Edge )  
+{
+    return Abc_SeqLatInit( Abc_SeqNodeGetLatLast(pObj, Edge) );  
+}
+
+
+// setting the init value of the given Lat on the edge
+static inline void Abc_SeqNodeSetInitOne( Abc_Obj_t * pObj, int Edge, int iLat, Abc_InitType_t Init )  
+{
+    Abc_SeqLatSetInit( Abc_SeqNodeGetLat(pObj, Edge, iLat), Init );  
+}
+
+
+// insert the first Lat on the edge
+static inline void Abc_SeqNodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )  
+{ 
+    Abc_SeqLat_t * pLat, * pRing, * pPrev;
+    pLat  = Abc_SeqNodeCreateLat( pObj );
+    pRing = Abc_SeqNodeReadInit( pObj, Edge );
+    if ( pRing == NULL )
+    {
+        pLat->pNext = pLat->pPrev = pLat;
+        Abc_SeqNodeSetInit( pObj, Edge, pLat );
+    }
+    else
+    {
+        Abc_SeqLatSetPrev( pRing, pLat );
+        Abc_SeqLatSetNext( pLat, pRing );
+        pPrev = Abc_SeqLatPrev( pRing );
+        Abc_SeqLatSetPrev( pLat, pPrev );
+        Abc_SeqLatSetNext( pPrev, pLat );
+        Abc_SeqNodeSetInit( pObj, Edge, pLat );  // rotate the ring to make pLat the first
+    }
+    Abc_SeqLatSetInit( pLat, Init );
+}
+
+// insert the last Lat on the edge
+static inline void Abc_SeqNodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )  
+{ 
+    Abc_SeqLat_t * pLat, * pRing, * pPrev;
+    pLat  = Abc_SeqNodeCreateLat( pObj );
+    pRing = Abc_SeqNodeReadInit( pObj, Edge );
+    if ( pRing == NULL )
+    {
+        pLat->pNext = pLat->pPrev = pLat;
+        Abc_SeqNodeSetInit( pObj, Edge, pLat );
+    }
+    else
+    {
+        Abc_SeqLatSetPrev( pRing, pLat );
+        Abc_SeqLatSetNext( pLat, pRing );
+        pPrev = Abc_SeqLatPrev( pRing );
+        Abc_SeqLatSetPrev( pLat, pPrev );
+        Abc_SeqLatSetNext( pPrev, pLat );
+    }
+    Abc_SeqLatSetInit( pLat, Init );
+}
+
+// delete the first Lat on the edge
+static inline Abc_InitType_t Abc_SeqNodeDeleteFirst( Abc_Obj_t * pObj, int Edge )  
+{ 
+    Abc_SeqLat_t * pLat, * pRing, * pPrev, * pNext;
+    pRing = Abc_SeqNodeReadInit( pObj, Edge );
+    pLat  = pRing; // consider the first latch
+    if ( pLat->pNext == pLat )
+        Abc_SeqNodeSetInit( pObj, Edge, NULL );
+    else
+    {
+        pPrev = Abc_SeqLatPrev( pLat );
+        pNext = Abc_SeqLatNext( pLat );
+        Abc_SeqLatSetPrev( pNext, pPrev );
+        Abc_SeqLatSetNext( pPrev, pNext );
+        Abc_SeqNodeSetInit( pObj, Edge, pNext ); // rotate the ring
+    }
+    Abc_SeqNodeRecycleLat( pObj, pLat );
+}
+
+// delete the last Lat on the edge
+static inline Abc_InitType_t Abc_SeqNodeDeleteLast( Abc_Obj_t * pObj, int Edge )  
+{
+    Abc_SeqLat_t * pLat, * pRing, * pPrev, * pNext;
+    pRing = Abc_SeqNodeReadInit( pObj, Edge );
+    pLat  = Abc_SeqLatPrev( pRing ); // consider the last latch
+    if ( pLat->pNext == pLat )
+        Abc_SeqNodeSetInit( pObj, Edge, NULL );
+    else
+    {
+        pPrev = Abc_SeqLatPrev( pLat );
+        pNext = Abc_SeqLatNext( pLat );
+        Abc_SeqLatSetPrev( pNext, pPrev );
+        Abc_SeqLatSetNext( pPrev, pNext );
+    }
+    Abc_SeqNodeRecycleLat( pObj, pLat ); 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_SeqMan_t * Abc_SeqCreate( int nMaxId )
+{
+    Abc_SeqMan_t * p;
+    // start the manager
+    p = ALLOC( Abc_SeqMan_t, 1 );
+    memset( p, 0, sizeof(Abc_SeqMan_t) );
+    p->nSize = nMaxId + 1;
+    // create internal data structures
+    p->vInits = Vec_PtrStart( 2 * p->nSize ); 
+    p->pMmInits = Extra_MmFixedStart( sizeof(Abc_SeqLat_t) );
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
index e250d929..fd0bc4c9 100644
--- a/src/base/abcs/abcs.h
+++ b/src/base/abcs/abcs.h
@@ -34,6 +34,7 @@
 
 // the maximum number of latches on the edge
 #define ABC_MAX_EDGE_LATCH   16   
+#define ABC_FULL_MASK        0xFFFFFFFF   
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
diff --git a/src/base/io/io.c b/src/base/io/io.c
index bffdfc10..bf71e72d 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 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 );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -34,6 +35,7 @@ static int IoCommandReadVerilog ( 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 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 );
 static int IoCommandWriteCnf    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -60,6 +62,7 @@ static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 void Io_Init( Abc_Frame_t * pAbc )
 {
     Cmd_CommandAdd( pAbc, "I/O", "read",          IoCommandRead,         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 );
     Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
@@ -68,6 +71,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_baf",     IoCommandWriteBaf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cnf",     IoCommandWriteCnf,     0 );
@@ -175,6 +179,79 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+
+    fCheck = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[util_optind];
+    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" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+ 
+    // set the new network
+    pNtk = Io_ReadBaf( FileName, fCheck );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from BAF file has failed.\n" );
+        return 1;
+    }
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_baf [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in Binary Aig Format (BAF)\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 IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pTemp;
@@ -727,6 +804,65 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    int c;
+
+    util_getopt_reset();
+    while ( ( c = util_getopt( 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 != util_optind + 1 )
+    {
+        goto usage;
+    }
+    FileName = argv[util_optind];
+
+    // check the network type
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pAbc->Out, "Currently can only write strashed combinational AIGs.\n" );
+        return 0;
+    }
+    Io_WriteBaf( pNtk, FileName );
+    return 0;
+
+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" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index a5aae529..8551a714 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -47,6 +47,8 @@
 
 /*=== abcRead.c ==========================================================*/
 extern Abc_Ntk_t *        Io_Read( char * pFileName, int fCheck );
+/*=== abcReadBaf.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadBaf( char * pFileName, int fCheck );
 /*=== abcReadBlif.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadBlif( char * pFileName, int fCheck );
 /*=== abcReadBench.c ==========================================================*/
@@ -67,6 +69,8 @@ extern Abc_Obj_t *        Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut,
 extern Abc_Obj_t *        Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
 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 );
+/*=== abcWriteBaf.c ==========================================================*/
+extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBlif.c ==========================================================*/
 extern void               Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
 extern void               Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index acf4deda..28500a3d 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -55,6 +55,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
         pNtk = Io_ReadPla( pFileName, fCheck );
     else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) )
         pNtk = Io_ReadEqn( pFileName, fCheck );
+    else if ( Extra_FileNameCheckExtension( pFileName, "baf" ) )
+        return Io_ReadBaf( pFileName, fCheck );
     else 
     {
         fprintf( stderr, "Unknown file format\n" );
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
new file mode 100644
index 00000000..7783373f
--- /dev/null
+++ b/src/base/io/ioReadBaf.c
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+  FileName    [ioReadBaf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to read AIG in the binary format.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioReadBaf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
+{
+    ProgressBar * pProgress;
+    FILE * pFile;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pNode0, * pNode1;
+    Abc_Ntk_t * pNtkNew;
+    int nInputs, nOutputs, nLatches, nAnds, nFileSize, Num, i;
+    char * pContents, * pName, * pCur;
+    unsigned * pBufferNode;
+
+    // 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 );
+
+    // skip the comments (comment lines begin with '#' and end with '\n')
+    for ( pCur = pContents; *pCur == '#'; )
+        while ( *pCur++ != '\n' );
+
+    // read the name
+    pName = pCur;             while ( *pCur++ );
+    // read the number of inputs
+    nInputs = atoi( pCur );   while ( *pCur++ );
+    // read the number of outputs
+    nOutputs = atoi( pCur );  while ( *pCur++ );
+    // read the number of latches
+    nLatches = atoi( pCur );  while ( *pCur++ );
+    // read the number of nodes
+    nAnds = atoi( pCur );     while ( *pCur++ );
+
+    // allocate the empty AIG
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    pNtkNew->pName = util_strsav( pName );
+    pNtkNew->pSpec = util_strsav( pFileName );
+
+    // prepare the array of nodes
+    vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
+    Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew->pManFunc) );
+
+    // create the PIs
+    for ( i = 0; i < nInputs; i++ )
+    {
+        pObj = Abc_NtkCreatePi(pNtkNew);    
+        Abc_NtkLogicStoreName( pObj, pCur );  while ( *pCur++ );
+        Vec_PtrPush( vNodes, pObj );
+    }
+    // create the POs
+    for ( i = 0; i < nOutputs; i++ )
+    {
+        pObj = Abc_NtkCreatePo(pNtkNew);   
+        Abc_NtkLogicStoreName( pObj, pCur );  while ( *pCur++ ); 
+    }
+    // create the latches
+    for ( i = 0; i < nLatches; i++ )
+    {
+        pObj = Abc_NtkCreateLatch(pNtkNew);
+        Abc_NtkLogicStoreName( pObj, pCur );  while ( *pCur++ ); 
+        Vec_PtrPush( vNodes, pObj );
+        Vec_PtrPush( pNtkNew->vCis, pObj );
+        Vec_PtrPush( pNtkNew->vCos, pObj );
+    }
+
+    // get the pointer to the beginning of the node array
+    pBufferNode = (int *)(pContents + (nFileSize - (2 * nAnds + nOutputs + nLatches) * sizeof(int)) );
+    // make sure we are at the place where the nodes begin
+    if ( pBufferNode != (int *)pCur )
+    {
+        free( pContents );
+        Vec_PtrFree( vNodes );
+        Abc_NtkDelete( pNtkNew );
+        printf( "Warning: Internal reader error.\n" );
+        return NULL;
+    }
+
+    // create the AND gates
+    pProgress = Extra_ProgressBarStart( stdout, nAnds );
+    for ( i = 0; i < nAnds; i++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, pBufferNode[2*i+0] >> 1), pBufferNode[2*i+0] & 1 );
+        pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, pBufferNode[2*i+1] >> 1), pBufferNode[2*i+1] & 1 );
+        Vec_PtrPush( vNodes, Abc_AigAnd(pNtkNew->pManFunc, pNode0, pNode1) );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // read the POs
+    Abc_NtkForEachCo( pNtkNew, pObj, i )
+    {
+        Num = pBufferNode[2*nAnds+i];
+        if ( Abc_ObjIsLatch(pObj) )
+        {
+            Abc_ObjSetData( pObj, (void *)(Num & 3) );
+            Num >>= 2;
+        }
+        pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, Num >> 1), Num & 1 );
+        Abc_ObjAddFanin( pObj, pNode0 );
+    }
+    free( pContents );
+    Vec_PtrFree( vNodes );
+
+    // remove the extra nodes
+    Abc_AigCleanup( pNtkNew->pManFunc );
+
+    // check the result
+    if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
+    {
+        printf( "Io_ReadBaf: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c
new file mode 100644
index 00000000..3ecd8e73
--- /dev/null
+++ b/src/base/io/ioWriteBaf.c
@@ -0,0 +1,163 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteBaf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write AIG in the binary format.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteBaf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+    Binary Aig Format
+
+    The motivation for this format is to have
+    - compact binary representation of large AIGs (~10x more compact than BLIF)
+    - consequently, fast reading/writing of large AIGs (~10x faster than BLIF)
+    - representation for all tech-ind info related to an AIG
+    - human-readable file header
+
+    The header:
+    (1) May contain several lines of human-readable comments.
+        Each comment line begins with symbol '#' and ends with symbol '\n'.
+    (2) Always contains the following data. 
+        - benchmark name
+        - number of primary inputs
+        - number of primary outputs
+        - number of latches
+        - number of AIG nodes (excluding the constant 1 node)
+        Each entry is followed by 0-byte (character '\0'):
+    (3) Next follow the names of the PIs, POs, and latches in this order. 
+        Each name is followed by 0-byte (character '\0').
+        Inside each set of names (PIs, POs, latches) there should be no
+        identical names but the PO names may coincide with PI/latch names.
+
+    The body:
+    (1) First part of the body contains binary information about the internal AIG nodes.
+        Each internal AIG node is represented using two 4-byte integers. 
+        Each integer is the fanin ID followed by 1-bit representation of the complemented attribute.
+        (For example, complemented edge to node 10 will be represented as 2*10 + 1 = 21.)
+        The IDs of the nodes are created as follows: Constant 1 node has ID=0. 
+        CIs (PIs and latch outputs) have 1-based IDs assigned in that order.
+        Each node in the array of the internal AIG nodes has the ID assigned in that order.
+        The constant 1 node is not written into the file.
+    (2) Second part of the body contains binary information about the edges connecting 
+        the COs (POs and latch inputs) with the internal AIG nodes.
+        Each edge is represented by one 4-byte integer the same way as a node fanin.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    ProgressBar * pProgress;
+    FILE * pFile;
+    Abc_Obj_t * pObj;
+    int i, nNodes, nAnds, nBufferSize;
+    unsigned * pBufferNode;
+    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;
+    }
+
+    // write the comment
+    fprintf( pFile, "# BAF (Binary Aig Format) for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+
+    // write the network name
+    fprintf( pFile, "%s%c", pNtk->pName, 0 );
+    // write the number of PIs
+    fprintf( pFile, "%d%c", Abc_NtkPiNum(pNtk), 0 );
+    // write the number of POs
+    fprintf( pFile, "%d%c", Abc_NtkPoNum(pNtk), 0 );
+    // write the number of latches
+    fprintf( pFile, "%d%c", Abc_NtkLatchNum(pNtk), 0 );
+    // write the number of internal nodes
+    fprintf( pFile, "%d%c", Abc_NtkNodeNum(pNtk), 0 );
+
+    // write PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
+    // write POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
+    // write latches
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        fprintf( pFile, "%s%c", Abc_ObjName(pObj), 0 );
+
+    // set the node numbers to be used in the output file
+    Abc_NtkCleanCopy( pNtk );
+    nNodes = 1;
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+
+    // write the nodes into the buffer
+    nAnds = 0;
+    nBufferSize = Abc_NtkNodeNum(pNtk) * 2 + Abc_NtkCoNum(pNtk);
+    pBufferNode = ALLOC( int, nBufferSize );
+    pProgress = Extra_ProgressBarStart( stdout, nBufferSize );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
+        pBufferNode[nAnds++] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
+        pBufferNode[nAnds++] = (((int)Abc_ObjFanin1(pObj)->pCopy) << 1) | Abc_ObjFaninC1(pObj);
+    }
+
+    // write the COs into the buffer
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, nAnds, NULL );
+        pBufferNode[nAnds] = (((int)Abc_ObjFanin0(pObj)->pCopy) << 1) | Abc_ObjFaninC0(pObj);
+        if ( Abc_ObjIsLatch(pObj) )
+            pBufferNode[nAnds] = (pBufferNode[nAnds] << 2) | ((unsigned)Abc_ObjData(pObj) & 3);
+        nAnds++;
+    }
+    Extra_ProgressBarStop( pProgress );
+    assert( nBufferSize == nAnds );
+
+    // write the buffer
+    fwrite( pBufferNode, 1, sizeof(int) * nBufferSize, pFile );
+    fclose( pFile );
+    free( pBufferNode );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 34582473..9938af12 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/ioReadBaf.c \
     src/base/io/ioReadBench.c \
     src/base/io/ioReadBlif.c \
     src/base/io/ioReadEdif.c \
@@ -7,6 +8,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/ioWriteBaf.c \
     src/base/io/ioWriteBench.c \
     src/base/io/ioWriteBlif.c \
     src/base/io/ioWriteCnf.c \