Version abc50814

author: Alan Mishchenko <alanmi@berkeley.edu> 2005-08-14 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2005-08-14 08:01:00 -0700
commit: 9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4 (patch)
tree: 52895e3901def014deaa5920d92637a8171d8acd /src/base
parent: f2b6b3be958e6d5629dc8a8b6c1b77195c16a2aa (diff)
download: abc-9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4.tar.gz
abc-9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4.tar.bz2
abc-9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4.zip
36 files changed, 1153 insertions, 375 deletions
diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 97d8b56a..f52df69f 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -33,6 +33,7 @@ static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPrintLatch   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -97,6 +98,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_latch",   Abc_CommandPrintLatch,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
@@ -480,6 +482,88 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    int c;
+    int fProfile;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fProfile = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'p':
+            fProfile ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs.\n" );
+        return 1;
+    }
+
+    if ( argc > util_optind + 1 )
+    {
+        fprintf( pErr, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+
+    if ( argc == util_optind + 1 )
+    {
+        pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+        if ( pNode == NULL )
+        {
+            fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+            return 1;
+        }
+        Abc_NodePrintLevel( pOut, pNode );
+        return 0;
+    }
+    // process all COs
+    Abc_NtkPrintLevel( pOut, pNtk, fProfile );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_level [-ph] <node>\n" );
+    fprintf( pErr, "\t        prints information about node level and cone size\n" );
+    fprintf( pErr, "\t-p    : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "\tnode  : (optional) one node to consider\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -2973,9 +3057,10 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nArgcNew;
     int c;
     int fSat;
+    int fVerbose;
 
     extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
-    extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
+    extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose );
 
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -2983,15 +3068,19 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fSat   = 0;
+    fSat     = 0;
+    fVerbose = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "svh" ) ) != EOF )
     {
         switch ( c )
         {
         case 's':
             fSat ^= 1;
             break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         default:
             goto usage;
         }
@@ -3006,16 +3095,17 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fSat )
         Abc_NtkCecSat( pNtk1, pNtk2 );
     else
-        Abc_NtkCecFraig( pNtk1, pNtk2 );
+        Abc_NtkCecFraig( pNtk1, pNtk2, fVerbose );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cec [-sh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: cec [-svh] <file1> <file2>\n" );
     fprintf( pErr, "\t        performs combinational equivalence checking\n" );
     fprintf( pErr, "\t-s    : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
+    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 438291d5..6acded6e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -43,26 +43,36 @@
 
 // network types
 typedef enum { 
-    ABC_NTK_NONE,              // unknown
-    ABC_NTK_NETLIST_SOP,       // netlist with nodes represented using SOPs
-    ABC_NTK_NETLIST_MAP,       // netlist with nodes represented using gates from the library
-    ABC_NTK_LOGIC_SOP,         // only SOP logic nodes (similar to SIS network)
-    ABC_NTK_LOGIC_BDD,         // only BDD logic nodes (similar to BDS network)
-    ABC_NTK_LOGIC_MAP,         // only mapped logic nodes (similar to mapped SIS network)
-    ABC_NTK_AIG,               // AIG or FRAIG (two input gates with c-attributes on edges)
-    ABC_NTK_SEQ,               // sequential AIG (two input gates with c- and latch-attributes on edges)
-    ABC_NTK_OTHER              // unused
+    ABC_NTK_NONE,          // 0:  unknown
+    ABC_NTK_NETLIST_SOP,   // 1:  netlist with nodes represented using SOPs
+    ABC_NTK_NETLIST_MAP,   // 2:  netlist with nodes represented using gates from the library
+    ABC_NTK_LOGIC_SOP,     // 3:  only SOP logic nodes (similar to SIS network)
+    ABC_NTK_LOGIC_BDD,     // 4:  only BDD logic nodes (similar to BDS network)
+    ABC_NTK_LOGIC_MAP,     // 5:  only mapped logic nodes (similar to mapped SIS network)
+    ABC_NTK_AIG,           // 6:  AIG or FRAIG (two input gates with c-attributes on edges)
+    ABC_NTK_SEQ,           // 7:  sequential AIG (two input gates with c- and latch-attributes on edges)
+    ABC_NTK_OTHER          // 8:  unused
 } Abc_NtkType_t;
 
+// functionality types
+typedef enum { 
+    ABC_FUNC_NONE,         // 0:  unknown
+    ABC_FUNC_SOP,          // 1:  sum-of-products
+    ABC_FUNC_BDD,          // 2:  binary decision diagrams
+    ABC_FUNC_AIG,          // 3:  and-inverter graphs
+    ABC_FUNC_MAP,          // 4:  standard cell library
+    ABC_FUNC_OTHER         // 5:  unused
+} Abc_FuncType_t;
+
 // object types
 typedef enum { 
-    ABC_OBJ_NONE,              // unknown
-    ABC_OBJ_NET,               // net
-    ABC_OBJ_NODE,              // node
-    ABC_OBJ_LATCH,             // latch
-    ABC_OBJ_PI,                // terminal
-    ABC_OBJ_PO,                // terminal
-    ABC_OBJ_OTHER              // unused
+    ABC_OBJ_NONE,          // 0:  unknown
+    ABC_OBJ_NET,           // 1:  net
+    ABC_OBJ_NODE,          // 2:  node
+    ABC_OBJ_LATCH,         // 3:  latch
+    ABC_OBJ_PI,            // 4:  primary input terminal
+    ABC_OBJ_PO,            // 5:  primary output terminal
+    ABC_OBJ_OTHER          // 6:  unused
 } Abc_ObjType_t;
 
 ////////////////////////////////////////////////////////////////////////
@@ -201,6 +211,7 @@ static inline void        Abc_NtkSetBackup( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNetBa
 static inline void        Abc_NtkSetStep  ( Abc_Ntk_t * pNtk, int iStep )              { pNtk->iStep      = iStep;      }
 
 // getting the number of objects 
+static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )    { return pNtk->vObjs->nSize;         }
 static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )       { return pNtk->nObjs;                }
 static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )       { return pNtk->nNets;                }
 static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )      { return pNtk->nNodes;               }
@@ -279,6 +290,7 @@ static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )    { return Abc_N
 static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl;                               }
 static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].fCompl;                               }
 static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].fCompl;                               }
+static inline bool        Abc_ObjFanoutC( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjFaninC0(pFanout) : Abc_ObjFaninC1(pFanout);  }
 static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats;                                }
 static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].nLats;                                }
 static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].nLats;                                }
@@ -287,6 +299,10 @@ static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )   {  assert( Abc_
 static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
 static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
+static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjFanoutFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjChild0(pFanout) : Abc_ObjChild1(pFanout);  }
 static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
 static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
 static inline void        Abc_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats )  { pObj->vFanins.pArray[i].nLats = nLats;               }
@@ -302,9 +318,9 @@ extern int                Abc_ObjFanoutLMin( Abc_Obj_t * pObj );
 extern int                Abc_ObjFanoutLMax( Abc_Obj_t * pObj );
 
 // checking the node type
-static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )   { assert(Abc_NtkIsAig(pNode->pNtk));            return Abc_ObjFaninNum(pNode) == 2;                         }
-static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode ){ assert(Abc_NtkIsAig(pNode->pNtk));            return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
-static inline bool        Abc_NodeIsConst( Abc_Obj_t * pNode )    { assert(Abc_ObjIsNode(Abc_ObjRegular(pNode))); return Abc_ObjFaninNum(Abc_ObjRegular(pNode)) == 0;         }
+static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )   { assert(Abc_NtkIsAig(pNode->pNtk) || Abc_NtkIsSeq(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2;                         }
+static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode ){ assert(Abc_NtkIsAig(pNode->pNtk) || Abc_NtkIsSeq(pNode->pNtk)); return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
+static inline bool        Abc_NodeIsConst( Abc_Obj_t * pNode )    { assert(Abc_ObjIsNode(Abc_ObjRegular(pNode)));                   return Abc_ObjFaninNum(Abc_ObjRegular(pNode)) == 0;         }
 extern        bool        Abc_NodeIsConst0( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsConst1( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsBuf( Abc_Obj_t * pNode );    
@@ -317,6 +333,14 @@ static inline void        Abc_NodeSetTravIdPrevious( Abc_Obj_t * pNode )     { p
 static inline bool        Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode )       { return (bool)(pNode->TravId == pNode->pNtk->nTravIds);     }
 static inline bool        Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { return (bool)(pNode->TravId == pNode->pNtk->nTravIds - 1); }
 
+// checking initial state of the latches
+static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)0;   }
+static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)1;   }
+static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)2;   }
+static inline bool        Abc_LatchIsInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)0;  }
+static inline bool        Abc_LatchIsInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)1;  }
+static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)2;  }
+
 // outputs the runtime in seconds
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
 
@@ -369,8 +393,8 @@ static inline bool        Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { r
 ////////////////////////////////////////////////////////////////////////
 
 /*=== abcAig.c ==========================================================*/
-extern Abc_Aig_t *        Abc_AigAlloc( Abc_Ntk_t * pNtk, bool fSeq );
-extern Abc_Aig_t *        Abc_AigDup( Abc_Aig_t * pMan, bool fSeq );
+extern Abc_Aig_t *        Abc_AigAlloc( Abc_Ntk_t * pNtk );
+extern Abc_Aig_t *        Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew );
 extern void               Abc_AigFree( Abc_Aig_t * pMan );
 extern int                Abc_AigCleanup( Abc_Aig_t * pMan );
 extern bool               Abc_AigCheck( Abc_Aig_t * pMan );
@@ -387,6 +411,7 @@ extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 /*=== abcCheck.c ==========================================================*/
 extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
+extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
@@ -424,9 +449,9 @@ extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanin
 extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
 extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 /*=== abcDfs.c ==========================================================*/
-extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
 extern int                Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
@@ -490,6 +515,8 @@ extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
 extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode );
+extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
+extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcRefs.c ==========================================================*/
 extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcRemove( Abc_Obj_t * pNode );
@@ -588,10 +615,10 @@ extern void               Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t *
 extern void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern Vec_Ptr_t *        Abc_AigCollectAll( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
 extern void               Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames );
 extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
+extern void               Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 67f19ba7..7e4cf33f 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -97,7 +97,7 @@ static void        Abc_AigDelete_int( Abc_Aig_t * pMan );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig, bool fSeq )
+Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
 {
     Abc_Aig_t * pMan;
     // start the manager
@@ -113,8 +113,11 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig, bool fSeq )
     pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
     // save the current network
     pMan->pNtkAig = pNtkAig;
+    // allocate constant nodes
     pMan->pConst1 = Abc_NtkCreateNode( pNtkAig );    
-    pMan->pReset  = fSeq? Abc_NtkCreateNode( pNtkAig ) : NULL;    
+    pMan->pReset  = Abc_NtkCreateNode( pNtkAig );
+    // subtract these nodes from the total number
+    pNtkAig->nNodes -= 2;
     return pMan;
 }
 
@@ -122,19 +125,54 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig, bool fSeq )
 
   Synopsis    [Duplicated the AIG manager.]
 
-  Description []
+  Description [Assumes that CI/CO nodes are already created.
+  Transfers the latch attributes on the edges.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, bool fSeq )
+Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
 {
-    Abc_Aig_t * pManNew;
-    pManNew = Abc_AigAlloc( pMan->pNtkAig, fSeq );
-
-
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkCiNum(pMan->pNtkAig)    == Abc_NtkCiNum(pManNew->pNtkAig) );
+    assert( Abc_NtkCoNum(pMan->pNtkAig)    == Abc_NtkCoNum(pManNew->pNtkAig) );
+    assert( Abc_NtkLatchNum(pMan->pNtkAig) == Abc_NtkLatchNum(pManNew->pNtkAig) );
+    // set mapping of the constant nodes
+    Abc_AigConst1( pMan )->pCopy = Abc_AigConst1( pManNew );
+    Abc_AigReset( pMan )->pCopy  = Abc_AigReset( pManNew );
+    // set the mapping of CIs/COs
+    Abc_NtkForEachPi( pMan->pNtkAig, pObj, i )
+        pObj->pCopy = Abc_NtkPi( pManNew->pNtkAig, i );
+    Abc_NtkForEachPo( pMan->pNtkAig, pObj, i )
+        pObj->pCopy = Abc_NtkPo( pManNew->pNtkAig, i );
+    Abc_NtkForEachLatch( pMan->pNtkAig, pObj, i )
+        pObj->pCopy = Abc_NtkLatch( pManNew->pNtkAig, i );
+    // copy internal nodes
+    vNodes = Abc_AigDfs( pMan->pNtkAig, 1 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( !Abc_NodeIsAigAnd(pObj) )
+            continue;
+        pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+        // transfer latch attributes
+        Abc_ObjSetFaninL0( pObj->pCopy, Abc_ObjFaninL0(pObj) );
+        Abc_ObjSetFaninL1( pObj->pCopy, Abc_ObjFaninL1(pObj) );
+    }
+    Vec_PtrFree( vNodes );
+    // relink the CO nodes
+    Abc_NtkForEachCo( pMan->pNtkAig, pObj, i )
+    {
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
+        Abc_ObjSetFaninL0( pObj->pCopy, Abc_ObjFaninL0(pObj) );
+    }
+    // get the number of nodes before and after
+    if ( Abc_NtkNodeNum(pMan->pNtkAig) != Abc_NtkNodeNum(pManNew->pNtkAig) )
+        printf( "Warning: Structural hashing reduced %d nodes (should not happen).\n",
+            Abc_NtkNodeNum(pMan->pNtkAig) - Abc_NtkNodeNum(pManNew->pNtkAig) );
     return pManNew;
 }
 
@@ -183,7 +221,10 @@ int Abc_AigCleanup( Abc_Aig_t * pMan )
     for ( i = 0; i < pMan->nBins; i++ )
         Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
             if ( Abc_ObjFanoutNum(pAnd) == 0 )
+            {
                 Vec_PtrPush( pMan->vStackDelete, pAnd );
+                pAnd->fMarkA = 1;
+            }
     // process the dangling nodes and their MFFCs
     for ( Counter = 0; Vec_PtrSize(pMan->vStackDelete) > 0; Counter++ )
         Abc_AigDelete_int( pMan );
@@ -239,7 +280,7 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
     for ( i = 0; i < pMan->nBins; i++ )
         Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
             Counter++;
-    if ( Counter + 1 + Abc_NtkIsSeq(pMan->pNtkAig) != Abc_NtkNodeNum(pMan->pNtkAig) )
+    if ( Counter != Abc_NtkNodeNum(pMan->pNtkAig) )
     {
         printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n", Counter );
         return 0;
@@ -329,10 +370,11 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 ***********************************************************************/
 Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd )
 {
+    Abc_Obj_t * pTemp;
     unsigned Key;
     // order the arguments
     if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
-        pAnd = p0, p0 = p1, p1 = pAnd;
+        pTemp = p0, p0 = p1, p1 = pTemp;
     // create the new node
     Abc_ObjAddFanin( pAnd, p0 );
     Abc_ObjAddFanin( pAnd, p1 );
@@ -384,10 +426,7 @@ Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     Key = Abc_HashKey2( p0, p1, pMan->nBins );
     // find the mataching node in the table
     Abc_AigBinForEachEntry( pMan->pBins[Key], pAnd )
-        if ( Abc_ObjFanin0(pAnd)  == Abc_ObjRegular(p0) && 
-             Abc_ObjFanin1(pAnd)  == Abc_ObjRegular(p1) &&  
-             Abc_ObjFaninC0(pAnd) == Abc_ObjIsComplement(p0) && 
-             Abc_ObjFaninC1(pAnd) == Abc_ObjIsComplement(p1) )
+        if ( p0 == Abc_ObjChild0(pAnd) && p1 == Abc_ObjChild1(pAnd) )
              return pAnd;
     return NULL;
 }
@@ -408,7 +447,6 @@ void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
     Abc_Obj_t * pAnd, ** ppPlace;
     unsigned Key;
     assert( !Abc_ObjIsComplement(pThis) );
-    assert( Abc_ObjFanoutNum(pThis) == 0 );
     assert( pMan->pNtkAig == pThis->pNtk );
     // get the hash key for these two nodes
     Key = Abc_HashKey2( Abc_ObjChild0(pThis), Abc_ObjChild1(pThis), pMan->nBins );
@@ -454,7 +492,7 @@ clk = clock();
     for ( i = 0; i < pMan->nBins; i++ )
         Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
         {
-            Key = Abc_HashKey2( Abc_ObjFanin(pEnt,0), Abc_ObjFanin(pEnt,1), nBinsNew );
+            Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), nBinsNew );
             pEnt->pNext   = pBinsNew[Key];
             pBinsNew[Key] = pEnt;
             Counter++;
@@ -597,7 +635,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
     pNew = Vec_PtrPop( pMan->vStackReplaceNew );
     // make sure the old node is regular and has fanouts
     // the new node can be complemented and can have fanouts
-    assert( !Abc_ObjIsComplement(pOld) == 0 );
+    assert( !Abc_ObjIsComplement(pOld) );
     assert( Abc_ObjFanoutNum(pOld) > 0 );
     // look at the fanouts of old node
     Abc_NodeCollectFanouts( pOld, pMan->vNodes );
@@ -632,7 +670,11 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
     }
     // schedule deletion of the old node
-    Vec_PtrPush( pMan->vStackDelete, pOld );
+    if ( Abc_NodeIsAigAnd(pOld) && pOld->fMarkA == 0 )
+    {
+        Vec_PtrPush( pMan->vStackDelete, pOld );
+        pOld->fMarkA = 1;
+    }
 }
 
 /**Function*************************************************************
@@ -653,18 +695,21 @@ void Abc_AigDelete_int( Abc_Aig_t * pMan )
     // get the node to delete
     assert( Vec_PtrSize(pMan->vStackDelete) > 0 );
     pNode = Vec_PtrPop( pMan->vStackDelete );
+
     // make sure the node is regular and dangling
-    assert( !Abc_ObjIsComplement(pNode) == 0 );
+    assert( !Abc_ObjIsComplement(pNode) );
     assert( Abc_ObjFanoutNum(pNode) == 0 );
-    // skip the constant node
-    if ( pNode == pMan->pConst1 )
-        return;
+    assert( pNode != pMan->pConst1 );
     // schedule fanins for deletion if they dangle
     Abc_ObjForEachFanin( pNode, pFanin, k )
     {
         assert( Abc_ObjFanoutNum(pFanin) > 0 );
         if ( Abc_ObjFanoutNum(pFanin) == 1 )
-            Vec_PtrPush( pMan->vStackDelete, pFanin );
+            if ( Abc_NodeIsAigAnd(pFanin) && pFanin->fMarkA == 0 )
+            {
+                Vec_PtrPush( pMan->vStackDelete, pFanin );
+                pFanin->fMarkA = 1;
+            }
     }
     // remove the node from the table
     Abc_AigAndDelete( pMan, pNode );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 5686baaf..f46dbb60 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -28,7 +28,7 @@
 static bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk );
 static bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk );
-static bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
+//static bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 static bool Abc_NtkCheckNet( Abc_Ntk_t * pNtk, Abc_Obj_t * pNet );
 static bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
 static bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch );
@@ -57,7 +57,7 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pNet, * pNode;
     int i;
 
-    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
         return 0;
@@ -110,9 +110,18 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     }
 
     // check the nodes
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( !Abc_NtkCheckNode( pNtk, pNode ) )
-            return 0;
+    if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    {
+        if ( Abc_NtkIsAig(pNtk) ) 
+            Abc_AigCheck( pNtk->pManFunc );
+    }
+    else
+    {
+        Abc_NtkForEachNode( pNtk, pNode, i )
+            if ( !Abc_NtkCheckNode( pNtk, pNode ) )
+                return 0;
+    }
+
     // check the latches
     Abc_NtkForEachLatch( pNtk, pNode, i )
         if ( !Abc_NtkCheckLatch( pNtk, pNode ) )
@@ -120,7 +129,7 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
 
     // finally, check for combinational loops
 //  clk = clock();
-    if ( !Abc_NtkIsAcyclic( pNtk ) )
+    if ( !Abc_NtkIsSeq( pNtk ) && !Abc_NtkIsAcyclic( pNtk ) )
     {
         fprintf( stdout, "NetworkCheck: Network contains a combinational loop.\n" );
         return 0;
@@ -352,7 +361,7 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
 bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanin, * pFanout;
-    int i, Value = 1;
+    int i, k, Value = 1;
 
     // check the network
     if ( pObj->pNtk != pNtk )
@@ -361,7 +370,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
         return 0;
     }
     // check the object ID
-    if ( pObj->Id < 0 || (int)pObj->Id > pNtk->vObjs->nSize )
+    if ( pObj->Id < 0 || (int)pObj->Id >= Abc_NtkObjNumMax(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Object \"%s\" has incorrect ID.\n", Abc_ObjName(pObj) );
         return 0;
@@ -386,6 +395,24 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             Value = 0;
         }
     }
+/*
+    // make sure fanins are not duplicated
+    for ( i = 0; i < pObj->vFanins.nSize; i++ )
+        for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
+            if ( pObj->vFanins.pArray[k].iFan == pObj->vFanins.pArray[i].iFan )
+            {
+                printf( "Warning: Node %s has", Abc_ObjName(pObj) );
+                printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) );
+            }
+    // make sure fanouts are not duplicated
+    for ( i = 0; i < pObj->vFanouts.nSize; i++ )
+        for ( k = i + 1; k < pObj->vFanouts.nSize; k++ )
+            if ( pObj->vFanouts.pArray[k].iFan == pObj->vFanouts.pArray[i].iFan )
+            {
+                printf( "Warning: Node %s has", Abc_ObjName(pObj) );
+                printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
+            }
+*/
     return Value;
 }
 
@@ -435,9 +462,9 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
         return 0;
     }
     // the node should have a function assigned unless it is an AIG
-    if ( pNode->pData == NULL && !Abc_NtkIsAig(pNtk) )
+    if ( pNode->pData == NULL )
     {
-        fprintf( stdout, "NodeCheck: An internal node \"%s\" has no logic function.\n", Abc_ObjName(pNode) );
+        fprintf( stdout, "NodeCheck: An internal node \"%s\" does not have a logic function.\n", Abc_ObjName(pNode) );
         return 0;
     }
     // the netlist and SOP logic network should have SOPs
@@ -458,7 +485,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
             return 0;
         }
     }
-    else if ( !Abc_NtkIsAig(pNtk) && !Abc_NtkIsLogicMap(pNtk) && !Abc_NtkIsNetlistMap(pNtk) )
+    else if ( !Abc_NtkIsMapped(pNtk) )
     {
         assert( 0 );
     }
@@ -562,7 +589,7 @@ bool Abc_NtkComparePos( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
         printf( "Networks have different number of primary outputs.\n" );
         return 0;
     }
-    // for each PI of pNet1 find corresponding PI of pNet2 and reorder them
+    // for each PO of pNet1 find corresponding PO of pNet2 and reorder them
     Abc_NtkForEachPo( pNtk1, pObj1, i )
     {
         if ( strcmp( Abc_ObjName(pObj1), Abc_ObjName(Abc_NtkPo(pNtk2,i)) ) != 0 )
@@ -623,12 +650,14 @@ bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 ***********************************************************************/
 bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
+    Abc_NtkAlphaOrderSignals( pNtk1, fComb );
+    Abc_NtkAlphaOrderSignals( pNtk2, fComb );
     if ( !Abc_NtkCompareLatches( pNtk1, pNtk2, fComb ) )
         return 0;
     if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) )
         return 0;
-//    if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) )
-//        return 0;
+    if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) )
+        return 0;
     return 1;
 }
 
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 9412305b..47ad5aea 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -75,10 +75,8 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
         pNtk->pManFunc = Extra_MmFlexStart();
     else if ( Abc_NtkIsLogicBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    else if ( Abc_NtkIsAig(pNtk) )
-        pNtk->pManFunc = Abc_AigAlloc( pNtk, 0 );
-    else if ( Abc_NtkIsSeq(pNtk) )
-        pNtk->pManFunc = Abc_AigAlloc( pNtk, 1 );
+    else if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+        pNtk->pManFunc = Abc_AigAlloc( pNtk );
     else if ( Abc_NtkIsMapped(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
     else
@@ -245,27 +243,21 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
     int i, k;
     if ( pNtk == NULL )
         return NULL;
-    assert( !Abc_NtkIsSeq(pNtk) );
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->Type );
-    // duplicate the nets and nodes
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( pObj->pCopy == NULL )
-            Abc_NtkDupObj(pNtkNew, pObj);
-    // connect the objects
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
-    // for AIGs copy the complemented attributes
+    // copy the internal nodes
     if ( Abc_NtkIsAig(pNtk) )
+        Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
+    else
     {
-        // set the data pointers and complemented attributes
+        // duplicate the nets and nodes (CIs/COs/latches already dupped)
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            if ( pObj->pCopy == NULL )
+                Abc_NtkDupObj(pNtkNew, pObj);
+        // reconnect all objects (no need to transfer attributes on edges)
         Abc_NtkForEachObj( pNtk, pObj, i )
             Abc_ObjForEachFanin( pObj, pFanin, k )
-                if ( Abc_ObjFaninC( pObj, k ) )
-                    Abc_ObjSetFaninC( pObj->pCopy, k );
-        // add the nodes to the structural hashing table
-        // TODO ???
+                Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     }
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
@@ -324,9 +316,7 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
         // if it is an AIG, add to the hash table
         if ( Abc_NtkIsAig(pNtk) )
         {
-            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, 
-                Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ),
-                Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) )  );
+            pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
         }
         else
         {
@@ -415,7 +405,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         Extra_MmFlexStop( pNtk->pManFunc, 0 );
     else if ( Abc_NtkIsLogicBdd(pNtk) )
         Extra_StopManager( pNtk->pManFunc );
-    else if ( Abc_NtkIsAig(pNtk) )
+    else if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
         Abc_AigFree( pNtk->pManFunc );
     else if ( !Abc_NtkIsMapped(pNtk) )
         assert( 0 );
@@ -598,7 +588,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
                 pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
             else if ( Abc_NtkIsMapped(pNtkNew) )
                 pObjNew->pData = pObj->pData;
-            else if ( !Abc_NtkIsAig(pNtkNew) )
+            else if ( !Abc_NtkIsAig(pNtkNew) && !Abc_NtkIsSeq(pNtkNew) )
                 assert( 0 );
         }
     }
@@ -626,9 +616,10 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pConst1;
-    assert( Abc_NtkIsAig(pNtkAig) );
+    assert( Abc_NtkIsAig(pNtkAig) || Abc_NtkIsSeq(pNtkAig) );
+    assert( Abc_NtkIsLogicSop(pNtkNew) );
     pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
-    if ( Abc_ObjFanoutNum( pConst1 ) > 0 )
+    if ( Abc_ObjFanoutNum(pConst1) > 0 )
         pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
     return pConst1->pCopy; 
 } 
@@ -647,16 +638,16 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
 Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pReset, * pConst1;
-    assert( Abc_NtkIsAig(pNtkAig) );
+    assert( Abc_NtkIsAig(pNtkAig) || Abc_NtkIsSeq(pNtkAig) );
     assert( Abc_NtkIsLogicSop(pNtkNew) );
     pReset = Abc_AigReset(pNtkAig->pManFunc);
-    if ( Abc_ObjFanoutNum( pReset ) > 0 )
+    if ( Abc_ObjFanoutNum(pReset) > 0 )
     {
         // create new latch with reset value 0
         pReset->pCopy = Abc_NtkCreateLatch( pNtkNew );
         // add constant node fanin to the latch
-        pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
-        Abc_ObjAddFanin( pReset->pCopy, pConst1->pCopy );
+        pConst1 = Abc_NodeCreateConst1( pNtkNew );
+        Abc_ObjAddFanin( pReset->pCopy, pConst1 );
     }
     return pReset->pCopy; 
 } 
@@ -712,7 +703,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     else if ( Abc_ObjIsLatch(pObj) )
     {
         pNtk->nLatches--;
-        assert( 0 ); // currently do not allow removing latches
     }
     else 
         assert( 0 );
@@ -772,7 +762,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
         return NULL;
     }
     Num = atoi( pName + 1 );
-    if ( Num < 0 || Num > Abc_NtkObjNum(pNtk) )
+    if ( Num < 0 || Num >= Abc_NtkObjNumMax(pNtk) )
     {
         printf( "The node \"%s\" with ID %d is not in the current network.\n", pName, Num );
         return NULL;
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index a02c3602..6313a1c5 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -46,7 +46,7 @@ static bool     Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
@@ -60,6 +60,13 @@ Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk )
         Abc_NodeSetTravIdCurrent( pNode );
         Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode)), vNodes );
     }
+    // collect dangling nodes if asked to
+    if ( fCollectAll )
+    {
+        Abc_NtkForEachNode( pNtk, pNode, i )
+            if ( !Abc_NodeIsTravIdCurrent(pNode) )
+                Abc_NtkDfs_rec( pNode, vNodes );
+    }
     return vNodes;
 }
 
@@ -141,12 +148,12 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk )
+Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
@@ -157,6 +164,13 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk )
         Abc_NodeSetTravIdCurrent( pNode );
         Abc_AigDfs_rec( Abc_ObjFanin0(pNode), vNodes );
     }
+    // collect dangling nodes if asked to
+    if ( fCollectAll )
+    {
+        Abc_NtkForEachNode( pNtk, pNode, i )
+            if ( !Abc_NodeIsTravIdCurrent(pNode) )
+                Abc_AigDfs_rec( pNode, vNodes );
+    }
     return vNodes;
 }
 
@@ -308,7 +322,7 @@ int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk )
 int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pFanin;
-    int i;
+    int i, Level;
     assert( !Abc_ObjIsNet(pNode) );
     // skip the PI
     if ( Abc_ObjIsCi(pNode) )
@@ -323,9 +337,9 @@ int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode )
     pNode->Level = 0;
     Abc_ObjForEachFanin( pNode, pFanin, i )
     {
-        Abc_NtkGetLevelNum_rec( Abc_ObjFanin0Ntk(pFanin) );
-        if ( pNode->Level < pFanin->Level )
-            pNode->Level = pFanin->Level;
+        Level = Abc_NtkGetLevelNum_rec( Abc_ObjFanin0Ntk(pFanin) );
+        if ( pNode->Level < (unsigned)Level )
+            pNode->Level = Level;
     }
     pNode->Level++;
     return pNode->Level;
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 2e242d9c..2bc87c85 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -24,6 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_LARGE_ID   ((1<<24)-1)   // should correspond to value in "vecFan.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,8 +47,8 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     assert( !Abc_ObjIsComplement(pObj) );
     assert( pObj->pNtk == pFaninR->pNtk );
     assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
-    assert( pObj->Id    < (1<<26)-1 );  // created but forgot to add it to the network?
-    assert( pFaninR->Id < (1<<26)-1 );  // created but forgot to add it to the network?
+    assert( pObj->Id    < ABC_LARGE_ID );  // created but forgot to add it to the network?
+    assert( pFaninR->Id < ABC_LARGE_ID );  // created but forgot to add it to the network?
     Vec_FanPush( pObj->pNtk->pMmStep, &pObj->vFanins,     Vec_Int2Fan(pFaninR->Id) );
     Vec_FanPush( pObj->pNtk->pMmStep, &pFaninR->vFanouts, Vec_Int2Fan(pObj->Id)    );
     if ( Abc_ObjIsComplement(pFanin) )
@@ -71,8 +73,8 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     assert( !Abc_ObjIsComplement(pFanin) );
     assert( pObj->pNtk == pFanin->pNtk );
     assert( pObj->Id >= 0 && pFanin->Id >= 0 );
-    assert( pObj->Id   < (1<<26)-1 );  // created but forgot to add it to the network?
-    assert( pFanin->Id < (1<<26)-1 );  // created but forgot to add it to the network?
+    assert( pObj->Id   < ABC_LARGE_ID );  // created but forgot to add it to the network?
+    assert( pFanin->Id < ABC_LARGE_ID );  // created but forgot to add it to the network?
     if ( !Vec_FanDeleteEntry( &pObj->vFanins, pFanin->Id ) )
     {
         printf( "The obj %d is not found among the fanins of obj %d ...\n", pFanin->Id, pObj->Id );
@@ -128,29 +130,36 @@ void Abc_ObjRemoveFanins( Abc_Obj_t * pObj )
 void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew )
 {
     Abc_Obj_t * pFaninNewR = Abc_ObjRegular(pFaninNew);
-    int iFanin, fCompl;
+    int iFanin, fCompl, nLats;
     assert( !Abc_ObjIsComplement(pObj) );
     assert( !Abc_ObjIsComplement(pFaninOld) );
     assert( pFaninOld != pFaninNewR );
+//    assert( pObj != pFaninOld );
+//    assert( pObj != pFaninNewR );
     assert( pObj->pNtk == pFaninOld->pNtk );
     assert( pObj->pNtk == pFaninNewR->pNtk );
     if ( (iFanin = Vec_FanFindEntry( &pObj->vFanins, pFaninOld->Id )) == -1 )
     {
-        printf( "Fanin node %d is not among the fanins of node %d...\n", pFaninOld->Id, pObj->Id );
+        printf( "Node %s is not among", Abc_ObjName(pFaninOld) );
+        printf( " the fanins of node %s...\n", Abc_ObjName(pObj) );
         return;
     }
-    // remember the polarity of the old fanin
+    // remember the attributes of the old fanin
     fCompl = Abc_ObjFaninC(pObj, iFanin);
-    // replace the old fanin entry by the new fanin entry (removes polarity)
+    nLats  = Abc_ObjFaninL(pObj, iFanin);
+    // replace the old fanin entry by the new fanin entry (removes attributes)
     Vec_FanWriteEntry( &pObj->vFanins, iFanin, Vec_Int2Fan(pFaninNewR->Id) );
-    // set the polarity of the new fanin
+    // set the attributes of the new fanin
     if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) )
         Abc_ObjSetFaninC( pObj, iFanin );
+    if ( nLats )
+        Abc_ObjSetFaninL( pObj, iFanin, nLats );
     // update the fanout of the fanin
     if ( !Vec_FanDeleteEntry( &pFaninOld->vFanouts, pObj->Id ) )
     {
-        printf( "The node %d is not among the fanouts of its old fanin %d...\n", pObj->Id, pFaninOld->Id );
-        return;
+        printf( "Node %s is not among", Abc_ObjName(pObj) );
+        printf( " the fanouts of its old fanin %s...\n", Abc_ObjName(pFaninOld) );
+//        return;
     }
     Vec_FanPush( pObj->pNtk->pMmStep, &pFaninNewR->vFanouts, Vec_Int2Fan(pObj->Id) );
 }
diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c
index 336a382c..1ced34d2 100644
--- a/src/base/abc/abcFpga.c
+++ b/src/base/abc/abcFpga.c
@@ -121,13 +121,12 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
         pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i];
 
     // load the AIG into the mapper
-    vNodes = Abc_AigDfs( pNtk );
+    vNodes = Abc_AigDfs( pNtk, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // consider the case of a constant
-        pNode = vNodes->pArray[i];
         if ( Abc_NodeIsConst(pNode) )
         {
             Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Fpga_ManReadConst1(pMan);
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index 2b6f0af2..3f5304a7 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -104,15 +104,11 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     pConst1 = Abc_AigConst1( pNtk->pManFunc );
 
     // perform strashing
-    if ( fAllNodes )
-        vNodes = Abc_AigCollectAll( pNtk );
-    else
-        vNodes = Abc_AigDfs( pNtk );
+    vNodes = Abc_AigDfs( pNtk, fAllNodes );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNode = vNodes->pArray[i];
         if ( pNode == pConst1 )
             pNodeFraig = Fraig_ManReadConst1(pMan);
         else
@@ -328,13 +324,12 @@ void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     int i;
 
     // perform strashing
-    vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // get the node
-        pNode = vNodes->pArray[i];
         assert( Abc_ObjIsNode(pNode) );
          // strash the node
         pNodeNew = Abc_NodeFraigTrust( pMan, pNode );
diff --git a/src/base/abc/abcFxu.c b/src/base/abc/abcFxu.c
index bbfef208..5721a50b 100644
--- a/src/base/abc/abcFxu.c
+++ b/src/base/abc/abcFxu.c
@@ -143,10 +143,10 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     p->vFanins    = Vec_PtrAlloc(0);
     p->vSopsNew   = Vec_PtrAlloc(0);
     p->vFaninsNew = Vec_PtrAlloc(0);
-    Vec_PtrFill( p->vSops,      pNtk->vObjs->nSize, NULL );
-    Vec_PtrFill( p->vFanins,    pNtk->vObjs->nSize, NULL );
-    Vec_PtrFill( p->vSopsNew,   pNtk->vObjs->nSize + p->nNodesExt, NULL );
-    Vec_PtrFill( p->vFaninsNew, pNtk->vObjs->nSize + p->nNodesExt, NULL );
+    Vec_PtrFill( p->vSops,      Abc_NtkObjNumMax(pNtk), NULL );
+    Vec_PtrFill( p->vFanins,    Abc_NtkObjNumMax(pNtk), NULL );
+    Vec_PtrFill( p->vSopsNew,   Abc_NtkObjNumMax(pNtk) + p->nNodesExt, NULL );
+    Vec_PtrFill( p->vFaninsNew, Abc_NtkObjNumMax(pNtk) + p->nNodesExt, NULL );
     // add SOPs and fanin array
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -157,7 +157,7 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
         p->vSops->pArray[i]   = pNode->pData;
         p->vFanins->pArray[i] = &pNode->vFanins;
     }
-    p->nNodesOld = pNtk->vObjs->nSize;
+    p->nNodesOld = Abc_NtkObjNumMax(pNtk);
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index 4c53ba8e..78f2faaa 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -32,7 +32,6 @@ static Abc_Ntk_t *  Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t *  Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
 static Abc_Obj_t *  Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
 static Abc_Obj_t *  Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis );
-static Abc_Obj_t *  Abc_NtkFixCiDriver( Abc_Obj_t * pNode );
 
 static Abc_Ntk_t *  Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk );
 static void         Abc_NodeSuperChoice( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
@@ -148,13 +147,12 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
         pNode->pCopy = (Abc_Obj_t *)Map_ManReadInputs(pMan)[i];
 
     // load the AIG into the mapper
-    vNodes = Abc_AigDfs( pNtk );
+    vNodes = Abc_AigDfs( pNtk, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // consider the case of a constant
-        pNode = vNodes->pArray[i];
         if ( Abc_NodeIsConst(pNode) )
         {
             Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Map_ManReadConst1(pMan);
@@ -221,8 +219,6 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
         pNodeMap = Map_ManReadOutputs(pMan)[i];
         pNodeNew = Abc_NodeFromMap_rec( pNtkNew, Map_Regular(pNodeMap), !Map_IsComplement(pNodeMap) );
         assert( !Abc_ObjIsComplement(pNodeNew) );
-        if ( !Abc_ObjIsNode(pNodeNew) )
-            pNodeNew = Abc_NtkFixCiDriver( pNodeNew );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
@@ -408,36 +404,6 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
 }
 
 
-/**Function*************************************************************
-
-  Synopsis    [Add buffer when the CO driver is a CI.]
-
-  Description [Hack: If the PO has the same name as the PI, it will still count
-  as the buffer but this node will not be written into file during writing]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkFixCiDriver( Abc_Obj_t * pNode )
-{
-    Mio_Gate_t * pGateBuffer = Mio_LibraryReadBuf(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())); 
-    Mio_Gate_t * pGateInv    = Mio_LibraryReadInv(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())); 
-    // add the buffer
-    if ( pGateBuffer )
-        return Abc_NodeCreateBuf( pNode->pNtk, pNode ); 
-    // add two inverters
-    if ( pGateInv )
-        return Abc_NodeCreateInv( pNode->pNtk, Abc_NodeCreateInv(pNode->pNtk, pNode) ); 
-    assert( 0 );
-    return NULL;
-}
-
-
-
-
-
 
 
 /**Function*************************************************************
@@ -561,7 +527,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     }
 
     // assign the mapping of the required phase to the POs
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c
index 52141ebb..7e6d4905 100644
--- a/src/base/abc/abcMiter.c
+++ b/src/base/abc/abcMiter.c
@@ -51,17 +51,14 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
     Abc_Ntk_t * pTemp = NULL;
     int fRemove1, fRemove2;
+    // check that the networks have the same PIs/POs/latches
+    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
+        return NULL;
     // make sure the circuits are strashed 
     fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
     fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
     if ( pNtk1 && pNtk2 )
-    {
-        // check that the networks have the same PIs/POs/latches
-        // reorder PIs/POs/latches of pNtk2 according to pNtk1
-        // compute the miter of two strashed sequential networks
-        if ( Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
-            pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
-    }
+        pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
     if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
     return pTemp;
@@ -196,25 +193,21 @@ void Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter )
 {
     ProgressBar * pProgress;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pNodeNew, * pConst1, * pConst1New;
+    Abc_Obj_t * pNode, * pConst1, * pConst1New;
     int i;
     // get the constant nodes
     pConst1    = Abc_AigConst1( pNtk->pManFunc );
     pConst1New = Abc_AigConst1( pNtkMiter->pManFunc );
     // perform strashing
-    vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNode = vNodes->pArray[i];
         if ( pNode == pConst1 )
-            pNodeNew = pConst1New;
+            pNode->pCopy = pConst1New;
         else
-            pNodeNew = Abc_AigAnd( pNtkMiter->pManFunc, 
-                Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
-                Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
-        pNode->pCopy = pNodeNew;
+            pNode->pCopy = Abc_AigAnd( pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
     }
     Vec_PtrFree( vNodes );
     Extra_ProgressBarStop( pProgress );
@@ -247,9 +240,7 @@ void Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t
         if ( pNode == pConst1 )
             pNodeNew = pConst1New;
         else
-            pNodeNew = Abc_AigAnd( pNtkMiter->pManFunc, 
-                Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
-                Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
+            pNodeNew = Abc_AigAnd( pNtkMiter->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
         pNode->pCopy = pNodeNew;
     }
     Vec_PtrFree( vNodes );
@@ -270,7 +261,7 @@ void Abc_NtkMiterAddOneNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t
 void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb )
 {
     Vec_Ptr_t * vPairs;
-    Abc_Obj_t * pDriverNew, * pMiter, * pNode;
+    Abc_Obj_t * pMiter, * pNode;
     int i;
     // collect the PO pairs from both networks
     vPairs = Vec_PtrAlloc( 100 );
@@ -279,11 +270,9 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
         // collect the CO nodes for the miter
         Abc_NtkForEachCo( pNtk1, pNode, i )
         {
-            pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-            Vec_PtrPush( vPairs, pDriverNew );
+            Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
             pNode = Abc_NtkCo( pNtk2, i );
-            pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-            Vec_PtrPush( vPairs, pDriverNew );
+            Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
         }
     }
     else
@@ -291,23 +280,15 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
         // collect the PO nodes for the miter
         Abc_NtkForEachPo( pNtk1, pNode, i )
         {
-            pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-            Vec_PtrPush( vPairs, pDriverNew );
+            Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
             pNode = Abc_NtkPo( pNtk2, i );
-            pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-            Vec_PtrPush( vPairs, pDriverNew );
+            Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pNode) );
         }
         // connect new latches
         Abc_NtkForEachLatch( pNtk1, pNode, i )
-        {
-            pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-            Abc_ObjAddFanin( pNode->pCopy, pDriverNew );
-        }
+            Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
         Abc_NtkForEachLatch( pNtk2, pNode, i )
-        {
-            pDriverNew = Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-            Abc_ObjAddFanin( pNode->pCopy, pDriverNew );
-        }
+            Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
     }
     // add the miter
     pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
@@ -347,7 +328,7 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
     pNtkMiter->pName = util_strsav(Buffer);
 
     // get the root output
-    pRoot = Abc_NtkCo(pNtk,Out);
+    pRoot = Abc_NtkCo( pNtk, Out );
 
     // perform strashing
     Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 );
@@ -410,7 +391,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
     Abc_NtkForEachPo( pMiter, pNodePo, i )
     {
         pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
-        if ( Abc_NodeIsConst(pChild) )
+        if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) )
         {
             assert( Abc_ObjRegular(pChild) == Abc_AigConst1(pMiter->pManFunc) );
             if ( !Abc_ObjIsComplement(pChild) )
@@ -446,7 +427,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
     if ( Abc_NtkPoNum(pMiter) == 1 )
     {
         pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,0) );
-        if ( Abc_NodeIsConst(Abc_ObjRegular(pChild)) )
+        if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) )
         {
             if ( Abc_ObjIsComplement(pChild) )
                 printf( "Unsatisfiable.\n" );
@@ -462,7 +443,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
         {
             pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
             printf( "Output #%2d : ", i );
-            if ( Abc_NodeIsConst(Abc_ObjRegular(pChild)) )
+            if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) )
             {
                 if ( Abc_ObjIsComplement(pChild) )
                     printf( "Unsatisfiable.\n" );
@@ -478,7 +459,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the time frames of the network.]
+  Synopsis    [Derives the timeframes of the network.]
 
   Description []
                
@@ -495,7 +476,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     Abc_Ntk_t * pNtkFrames;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pLatch, * pLatchNew;
-    int i;
+    int i, Counter;
     assert( nFrames > 0 );
     assert( Abc_NtkIsAig(pNtk) );
     // start the new network
@@ -510,12 +491,24 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     }
     else
     {
+        Counter = 0;
         Abc_NtkForEachLatch( pNtk, pLatch, i )
-            pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), ((int)pLatch->pData)!=1 );
+        {
+            if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
+            {
+                pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
+                Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) );
+                Counter++;
+            }
+            else
+                pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) );
+        }
+        if ( Counter )
+            printf( "Warning: %d uninitialized latches are replaced by free variables.\n", Counter );
     }
     
     // create the timeframes
-    vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 0 );
     pProgress = Extra_ProgressBarStart( stdout, nFrames );
     for ( i = 0; i < nFrames; i++ )
     {
@@ -579,27 +572,24 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
         Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
     }
     // add the internal nodes
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        pNode = vNodes->pArray[i];
         if ( pNode == pConst1 )
             pNodeNew = pConst1New;
         else
-            pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, 
-                Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
-                Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
+            pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
         pNode->pCopy = pNodeNew;
     }
     // add the new POs
     Abc_NtkForEachPo( pNtk, pNode, i )
     {
         pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
-        Abc_ObjAddFanin( pNodeNew, Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
+        Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) );
         Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
     }
     // transfer the implementation of the latch drivers to the latches
     Abc_NtkForEachLatch( pNtk, pLatch, i )
-        pLatch->pCopy = Abc_ObjNotCond( Abc_ObjFanin0(pLatch)->pCopy, Abc_ObjFaninC0(pLatch) );
+        pLatch->pCopy = Abc_ObjChild0Copy(pLatch);
 }
 
 
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 82040404..07c64712 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -108,7 +108,7 @@ char * Abc_ObjName( Abc_Obj_t * pObj )
     {
         // in a logic network, PI/PO/latch names are stored in the hash table
         // internal nodes have made up names
-        assert( Abc_ObjIsNode(pObj) );
+        assert( Abc_ObjIsNode(pObj) || Abc_ObjIsLatch(pObj) );
         sprintf( Buffer, "[%d]", pObj->Id );
     }
     return Buffer;
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 3f7fae2b..bfa41842 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -84,20 +84,26 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
-    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsAig(pNtk) );
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) );
+    if ( Abc_NtkIsAig(pNtk) )
     {
-        Abc_NtkBddToSop(pNtk);
-        pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
-        Abc_NtkSopToBdd(pNtk);
+        pNtkTemp = Abc_NtkAigToLogicSop(pNtk);
+        pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
+        Abc_NtkDelete( pNtkTemp );
     }
-    else if ( Abc_NtkIsAig(pNtk) )
+    else if ( Abc_NtkIsSeq(pNtk) )
     {
-        pNtkTemp = Abc_NtkAigToLogicSop(pNtk);
+        pNtkTemp = Abc_NtkSeqToLogicSop(pNtk);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
         Abc_NtkDelete( pNtkTemp );
     }
-    else
+    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    {
+        Abc_NtkBddToSop(pNtk);
+        pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
+        Abc_NtkSopToBdd(pNtk);
+    }
+    else 
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
     return pNtkNew;
 }
@@ -261,10 +267,12 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         // set the new node
         pObj->pCopy = pNodeNew;
     }
-    // connect the objects, including the COs
-    Abc_NtkForEachObj( pNtk, pObj, i )
+    // connect the internal nodes
+    Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+    // connect the COs
+    Abc_NtkFinalize( pNtk, pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate the EXDC Ntk
@@ -306,7 +314,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     // create the constant node
     Abc_NtkDupConst1( pNtk, pNtkNew );
     // collect the nodes to be used (marks all nodes with current TravId)
-    vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 0 );
     // create inverters for the CI and remember them
     Abc_NtkForEachCi( pNtk, pObj, i )
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index f4833a11..e85b02d7 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -43,7 +43,7 @@
 void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
     fprintf( pFile, "%-15s:",       pNtk->pName );
-    fprintf( pFile, "  i/o = %3d/%3d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+    fprintf( pFile, "  i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
 
     if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
@@ -65,7 +65,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
-    if ( Abc_NtkIsLogicSop(pNtk) )   
+    if ( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsNetlistSop(pNtk) )   
     {
         fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
 //        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
@@ -74,7 +74,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     }
     else if ( Abc_NtkIsLogicBdd(pNtk) )
         fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
-    else if ( Abc_NtkIsLogicMap(pNtk) )
+    else if ( Abc_NtkIsLogicMap(pNtk) || Abc_NtkIsNetlistMap(pNtk) )
     {
         fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
         fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
@@ -85,7 +85,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     }
 
     if ( !Abc_NtkIsSeq(pNtk) )
-        fprintf( pFile, "  lev = %2d", Abc_NtkGetLevelNum(pNtk) );
+        fprintf( pFile, "  lev = %3d", Abc_NtkGetLevelNum(pNtk) );
 
     fprintf( pFile, "\n" );
 }
@@ -135,7 +135,7 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pLatch;
+    Abc_Obj_t * pLatch, * pFanin;
     int i, Counter0, Counter1, Counter2;
     int Init0, Init1, Init2;
 
@@ -152,38 +152,46 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
 
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
-        if ( pLatch->pData == (void *)0 )
+        if ( Abc_LatchIsInit0(pLatch) )
             Init0++;
-        else if ( pLatch->pData == (void *)1 )
+        else if ( Abc_LatchIsInit1(pLatch) )
             Init1++;
-        else if ( pLatch->pData == (void *)2 )
+        else if ( Abc_LatchIsInitDc(pLatch) )
             Init2++;
         else
             assert( 0 );
 
-        if ( Abc_ObjFaninNum( Abc_ObjFanin0(pLatch) ) == 0 )
+        pFanin = Abc_ObjFanin0(pLatch);
+        if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) )
+            continue;
+
+        // the latch input is a constant node
+        Counter0++;
+        if ( Abc_LatchIsInitDc(pLatch) )
         {
-            Counter0++;
-            if ( pLatch->pData == (void *)2 )
-                Counter1++;
-            else 
-            {
-                if ( Abc_NtkIsAig(pNtk) )
-                {
-                    if ( (pLatch->pData == (void *)1) ^ Abc_ObjFaninC0(pLatch) )
-                        Counter2++;
-                }
-                else
-                {
-                    if ( (pLatch->pData == (void *)1) ^ Abc_NodeIsConst0(pLatch) )
-                        Counter2++;
-                }
-            }
+            Counter1++;
+            continue;
+        }
+        // count the number of cases when the constant is equal to the initial value
+        if ( Abc_NtkIsAig(pNtk) )
+        {
+            if ( Abc_LatchIsInit1(pLatch) == !Abc_ObjFaninC0(pLatch) )
+                Counter2++;
+        }
+        else
+        {
+            if ( Abc_LatchIsInit1(pLatch) == Abc_NodeIsConst1(pLatch) )
+                Counter2++;
         }
     }
-    fprintf( pFile, "Latches = %5d:  Init 0 = %5d. Init 1 = %5d. Init any = %5d.\n", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
-    fprintf( pFile, "Constant driver = %4d. Init any = %4d. Init match = %4d.\n", Counter0, Counter1, Counter2 );
-    fprintf( pFile, "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+//    fprintf( pFile, "%-15s: ", pNtk->pName );
+//    fprintf( pFile, "L = %5d: 0 = %4d. 1 = %3d. DC = %4d. ", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
+//    fprintf( pFile, "Con = %3d. DC = %3d. Mat = %3d. ", Counter0, Counter1, Counter2 );
+//    fprintf( pFile, "SFeed = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+    fprintf( pFile, "%-15s:  ", pNtk->pName );
+    fprintf( pFile, "Lat = %5d: 0 = %4d. 1 = %3d. DC = %4d. \n", Abc_NtkLatchNum(pNtk), Init0, Init1, Init2 );
+    fprintf( pFile, "Con = %3d. DC = %3d. Mat = %3d. ", Counter0, Counter1, Counter2 );
+    fprintf( pFile, "SFeed = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
 }
 
 /**Function*************************************************************
@@ -270,21 +278,17 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode )
     if ( Abc_ObjIsPo(pNode) )
         pNode = Abc_ObjFanin0(pNode);
 
+    fprintf( pFile, "Node %s", Abc_ObjName(pNode) );    
+    fprintf( pFile, "\n" ); 
+
     fprintf( pFile, "Fanins (%d): ", Abc_ObjFaninNum(pNode) );    
     Abc_ObjForEachFanin( pNode, pNode2, i )
-    {
-        pNode2->pCopy = NULL;
         fprintf( pFile, " %s", Abc_ObjName(pNode2) );
-    }
     fprintf( pFile, "\n" ); 
     
-    fprintf( pFile, "\n" );    
     fprintf( pFile, "Fanouts (%d): ", Abc_ObjFaninNum(pNode) );    
     Abc_ObjForEachFanout( pNode, pNode2, i )
-    {
-        pNode2->pCopy = NULL;
         fprintf( pFile, " %s", Abc_ObjName(pNode2) );
-    }
     fprintf( pFile, "\n" );   
 }
 
@@ -326,21 +330,122 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
         pNode = Abc_ObjFanin0(pNode);
     if ( Abc_ObjIsPi(pNode) )
     {
-        printf( "Skipping the PI node.\n" );
+        fprintf( pFile, "Skipping the PI node.\n" );
         return;
     }
     if ( Abc_ObjIsLatch(pNode) )
     {
-        printf( "Skipping the latch.\n" );
+        fprintf( pFile, "Skipping the latch.\n" );
         return;
     }
     assert( Abc_ObjIsNode(pNode) );
     vFactor = Ft_Factor( pNode->pData );
-    pNode->pCopy = NULL;
     Ft_FactorPrint( stdout, vFactor, NULL, Abc_ObjName(pNode) );
     Vec_IntFree( vFactor );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the level stats of the PO node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
+{
+    Abc_Obj_t * pNode;
+    int i, Length;
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // print the delay profile
+    if ( fProfile )
+    {
+        int LevelMax, * pLevelCounts;
+        int nOutsSum, nOutsTotal;
+
+        LevelMax = 0;
+        Abc_NtkForEachCo( pNtk, pNode, i )
+            if ( LevelMax < (int)Abc_ObjFanin0(pNode)->Level )
+                LevelMax = Abc_ObjFanin0(pNode)->Level;
+        pLevelCounts = ALLOC( int, LevelMax + 1 );
+        memset( pLevelCounts, 0, sizeof(int) * (LevelMax + 1) );
+        Abc_NtkForEachCo( pNtk, pNode, i )
+            pLevelCounts[Abc_ObjFanin0(pNode)->Level]++;
+
+        nOutsSum   = 0;
+        nOutsTotal = Abc_NtkCoNum(pNtk);
+        for ( i = 0; i <= LevelMax; i++ )
+            if ( pLevelCounts[i] )
+            {
+                nOutsSum += pLevelCounts[i];
+                printf( "Level = %4d.  COs = %4d.   %5.1f %%\n", i, pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal );
+            }
+        return;
+    }
+
+    // find the longest name
+    Length = 0;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        if ( Length < (int)strlen(Abc_ObjName(pNode)) )
+            Length = strlen(Abc_ObjName(pNode));
+    if ( Length < 5 )
+        Length = 5;
+    // print stats for each output
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        fprintf( pFile, "CO %4d :  %*s    ", i, Length, Abc_ObjName(pNode) ); 
+        Abc_NodePrintLevel( pFile, pNode );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pDriver;
+    Vec_Ptr_t * vNodes;
+
+    pDriver = Abc_ObjIsCo(pNode)? Abc_ObjFanin0(pNode) : pNode;
+    if ( Abc_ObjIsPi(pDriver) )
+    {
+        fprintf( pFile, "Primary input.\n" );
+        return;
+    }
+    if ( Abc_ObjIsLatch(pDriver) )
+    {
+        fprintf( pFile, "Latch.\n" );
+        return;
+    }
+    if ( Abc_NodeIsConst(pDriver) )
+    {
+        fprintf( pFile, "Constant %d.\n", !Abc_ObjFaninC0(pNode) );
+        return;
+    }
+    // print the level
+    fprintf( pFile, "Level = %3d.  ", pDriver->Level );
+    // print the size of MFFC
+    fprintf( pFile, "Mffc = %5d.  ", Abc_NodeMffcSize(pDriver) );
+    // print the size of the shole cone
+    vNodes = Abc_NtkDfsNodes( pNode->pNtk, &pDriver, 1 );
+    fprintf( pFile, "Cone = %5d.  ", Vec_PtrSize(vNodes) );
+    Vec_PtrFree( vNodes );
+    fprintf( pFile, "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c
index 12bf0912..8037f642 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abc/abcRenode.c
@@ -492,8 +492,8 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
             nMuxes++;
     }
     printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
-}
-
+} 
+ 
 /**Function*************************************************************
 
   Synopsis    [Sets the expansion boundary for conversion into multi-input AND graph.]
diff --git a/src/base/abc/abcRes.c b/src/base/abc/abcRes.c
index 658c8229..221b6f87 100644
--- a/src/base/abc/abcRes.c
+++ b/src/base/abc/abcRes.c
@@ -79,7 +79,7 @@ int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p )
     pProgress = Extra_ProgressBarStart( stdout, 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        Approx = (int)(100.0 * i / pNtk->vObjs->nSize );
+        Approx = (int)(100.0 * i / Abc_NtkObjNumMax(pNtk) );
         Extra_ProgressBarUpdate( pProgress, Approx, NULL );
         p->pNode = pNode;
         Abc_NodeResyn( p );
diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c
index 9d4658ce..e0685bf7 100644
--- a/src/base/abc/abcSeq.c
+++ b/src/base/abc/abcSeq.c
@@ -25,8 +25,8 @@
     in addition to the complemented attibutes. 
 
     The sets of PIs/POs remain the same as in logic network. 
-    Constant 1 node can only be used as a fanin of a PO node and reset node.
-    The reset node producing sequence (01111...) is used to create the
+    Constant 1 node can only be used as a fanin of a PO node and the reset node.
+    The reset node produces sequence (01111...). It is used to create the
     initialization logic of all latches.
     The latches do not have explicit initial state but they are implicitly
     reset by the reset node.
@@ -60,10 +60,124 @@ static void        Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
 {
+    int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
+    Abc_Aig_t * pManNew;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pConst, * pFanout, * pFaninNew, * pLatch;
+    int i, k, fChange, Counter;
+
     assert( Abc_NtkIsAig(pNtk) );
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_SEQ );
+    pManNew = pNtkNew->pManFunc;
+
+    // set mapping of the constant nodes
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1( pManNew );
+    Abc_AigReset(pNtk->pManFunc)->pCopy  = Abc_AigReset( pManNew );
+
+    // get rid of initial states
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        pObj->pNext = pObj->pCopy;
+        if ( Abc_LatchIsInit0(pObj) )
+            pObj->pCopy = Abc_AigAnd( pManNew, pObj->pCopy, Abc_AigReset(pManNew) );
+        else if ( Abc_LatchIsInit1(pObj) )
+            pObj->pCopy = Abc_AigOr( pManNew, pObj->pCopy, Abc_ObjNot( Abc_AigReset(pManNew) ) );
+    }
+
+    // copy internal nodes
+    vNodes = Abc_AigDfs( pNtk, 1 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Abc_ObjFaninNum(pObj) == 2 )
+            pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    Vec_PtrFree( vNodes );
+
+    // relink the CO nodes
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pNext, Abc_ObjChild0Copy(pObj) );
+
+    // propagate constant input latches in the new network
+    Counter = 0;
+    fChange = 1;
+    while ( fChange )
+    {
+        fChange = 0;
+        Abc_NtkForEachLatch( pNtkNew, pLatch, i )
+        {
+            if ( Abc_ObjFanoutNum(pLatch) == 0 )
+                continue;
+            pFaninNew = Abc_ObjFanin0(pLatch);
+            if ( Abc_ObjIsCi(pFaninNew) || !Abc_NodeIsConst(pFaninNew) )
+                continue;
+            pConst = Abc_ObjNotCond( Abc_AigConst1(pManNew), Abc_ObjFaninC0(pLatch) );
+            Abc_AigReplace( pManNew, pLatch, pConst );
+            fChange = 1;
+            Counter++;
+        }
+    }
+    if ( Counter )
+        fprintf( stdout, "Latch sweeping removed %d latches (out of %d).\n", Counter, Abc_NtkLatchNum(pNtk) );
+
+    // redirect fanouts of each latch to the latch fanins
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachLatch( pNtkNew, pLatch, i )
+    {
+//printf( "Latch %s. Fanouts = %d.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) );
+
+        Abc_NodeCollectFanouts( pLatch, vNodes );
+        Vec_PtrForEachEntry( vNodes, pFanout, k )
+        {
+            if ( Abc_ObjFaninId0(pFanout) == Abc_ObjFaninId1(pFanout))
+                printf( " ******* Identical fanins!!! ******* \n" );
+
+            if ( Abc_ObjFaninId0(pFanout) == (int)pLatch->Id )
+            {
+//                pFaninNew = Abc_ObjNotCond( Abc_ObjChild0(pLatch), Abc_ObjFaninC0(pFanout) );
+                pFaninNew = Abc_ObjChild0(pLatch);
+                Abc_ObjPatchFanin( pFanout, pLatch, pFaninNew );
+                Abc_ObjAddFaninL0( pFanout, 1 );
+            }
+            else if ( Abc_ObjFaninId1(pFanout) == (int)pLatch->Id )
+            {
+//                pFaninNew = Abc_ObjNotCond( Abc_ObjChild0(pLatch), Abc_ObjFaninC1(pFanout) );
+                pFaninNew = Abc_ObjChild0(pLatch);
+                Abc_ObjPatchFanin( pFanout, pLatch, pFaninNew );
+                Abc_ObjAddFaninL1( pFanout, 1 );
+            }
+            else
+                assert( 0 );
+        }
+        assert( Abc_ObjFanoutNum(pLatch) == 0 );
+        Abc_NtkDeleteObj( pLatch );
+    }
+    Vec_PtrFree( vNodes );
+    // get rid of latches altogether 
+//    Abc_NtkForEachLatch( pNtkNew, pObj, i )
+//        Abc_NtkDeleteObj( pObj );
+    assert( pNtkNew->nLatches == 0 );
+    Vec_PtrClear( pNtkNew->vLats );
+    Vec_PtrShrink( pNtkNew->vCis, pNtk->nPis );
+    Vec_PtrShrink( pNtkNew->vCos, pNtk->nPos );
+
+/*
+/////////////////////////////////////////////
+Abc_NtkForEachNode( pNtkNew, pObj, i )
+    if ( !Abc_NodeIsConst(pObj) )
+        if ( Abc_ObjFaninL0(pObj) + Abc_ObjFaninL1(pObj) > 20 )
+            printf( "(%d,%d) ", Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) );
+Abc_NtkForEachCo( pNtkNew, pObj, i )
+    printf( "(%d) ", Abc_ObjFaninL0(pObj) );
+/////////////////////////////////////////////
+printf( "\n" );
+*/
+
+    if ( pNtk->pExdc )
+        fprintf( stdout, "Warning: EXDC is dropped when converting to sequential AIG.\n" );
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" );
     return pNtkNew;
 }
 
@@ -83,7 +197,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pFaninNew;
-    int i, k;
+    int i, k, c;
     assert( Abc_NtkIsSeq(pNtk) );
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
@@ -106,10 +220,14 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
         {
             // find the fanin
             pFaninNew = pFanin->pCopy;
-            for ( i = 0; i < Abc_ObjFaninL(pObj, k); i++ )
+            for ( c = 0; c < Abc_ObjFaninL(pObj, k); c++ )
                 pFaninNew = pFaninNew->pCopy;
             Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
         }
+    // set the complemented attributed of CO edges (to be fixed by making simple COs)
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( Abc_ObjFaninC0(pObj) )
+            Abc_ObjSetFaninC( pObj->pCopy, 0 );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     // duplicate the EXDC network
@@ -142,7 +260,7 @@ Vec_Int_t * Abc_NtkSeqCountLatches( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsSeq( pNtk ) );
     // start the array of counters
     vNumbers = Vec_IntAlloc( 0 );
-    Vec_IntFill( vNumbers, Abc_NtkObjNum(pNtk), 0 );
+    Vec_IntFill( vNumbers, Abc_NtkObjNumMax(pNtk), 0 );
     // count for each edge
     Abc_NtkForEachObj( pNtk, pObj, i )
         Abc_NodeSeqCountLatches( pObj, vNumbers );
@@ -197,7 +315,11 @@ void Abc_NtkSeqCreateLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     // create latches for each new object according to the counters
     vNumbers = Abc_NtkSeqCountLatches( pNtk );
     Abc_NtkForEachObj( pNtk, pObj, i )
-        Abc_NodeSeqCreateLatches( pObj->pCopy, Vec_IntEntry(vNumbers, pObj->Id) );
+    {
+        if ( pObj->pCopy == NULL )
+            continue;
+        Abc_NodeSeqCreateLatches( pObj->pCopy, Vec_IntEntry(vNumbers, (int)pObj->Id) );
+    }
     Vec_IntFree( vNumbers );
     // add latch to the PI/PO lists, create latch names
     Abc_NtkFinalizeLatches( pNtkNew );
@@ -224,6 +346,7 @@ void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches )
     for ( i = 0, pFanin = pObj; i < nLatches; pFanin = pLatch, i++ )
     {
         pLatch = Abc_NtkCreateLatch( pNtk );
+        Abc_LatchSetInitDc(pLatch);
         Abc_ObjAddFanin( pLatch, pFanin );
         pFanin->pCopy = pLatch;
     }
@@ -249,12 +372,21 @@ int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk )
     // create latches for each new object according to the counters
     Counter = 0;
     vNumbers = Abc_NtkSeqCountLatches( pNtk );
-    Abc_NtkForEachObj( pNtk, pObj, i )
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) );
+        Counter += Vec_IntEntry(vNumbers, (int)pObj->Id);
+    }
+    Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, pObj->Id) );
-        Counter += Vec_IntEntry(vNumbers, pObj->Id);
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) );
+        Counter += Vec_IntEntry(vNumbers, (int)pObj->Id);
     }
     Vec_IntFree( vNumbers );
+    if ( Abc_ObjFanoutNum( Abc_AigReset(pNtk->pManFunc) ) > 0 )
+        Counter++;
     return Counter;
 }
 
@@ -284,12 +416,15 @@ void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         Vec_PtrPush( vNodes, pNode );
         pNode->fMarkA = 1;
     }
     // process the nodes
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
+//        printf( "(%d,%d) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) );
         // get the number of latches to retime
         nLatches = Abc_ObjFaninLMin(pNode);
         if ( nLatches == 0 )
@@ -316,6 +451,8 @@ void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         pNode->fMarkA = 0;
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         assert( Abc_ObjFaninLMin(pNode) == 0 );
     }
 }
@@ -341,6 +478,8 @@ void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         Vec_PtrPush( vNodes, pNode );
         pNode->fMarkA = 1;
     }
@@ -359,6 +498,8 @@ void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
         Abc_ObjForEachFanin( pNode, pFanin, k )
         {
             Abc_ObjAddFaninL( pNode, k, nLatches );
+            if ( Abc_ObjIsPi(pFanin) || Abc_NodeIsConst(pFanin) )
+                continue;
             if ( pFanin->fMarkA == 0 )
             {   // schedule the node for updating
                 Vec_PtrPush( vNodes, pFanin );
@@ -373,7 +514,9 @@ void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         pNode->fMarkA = 0;
-        assert( Abc_ObjFanoutLMin(pNode) == 0 );
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+//        assert( Abc_ObjFanoutLMin(pNode) == 0 );
     }
 }
 
@@ -394,9 +537,9 @@ void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
 int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )
 {
     assert( Abc_NtkIsSeq(pObj->pNtk) );
-    if ( Abc_ObjFanin0(pFanout) == pObj )
+    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
         return Abc_ObjFaninL0(pFanout);
-    else if ( Abc_ObjFanin1(pFanout) == pObj )
+    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
         return Abc_ObjFaninL1(pFanout);
     else 
         assert( 0 );
@@ -417,9 +560,9 @@ int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )
 void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )  
 { 
     assert( Abc_NtkIsSeq(pObj->pNtk) );
-    if ( Abc_ObjFanin0(pFanout) == pObj )
+    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
         Abc_ObjSetFaninL0(pFanout, nLats);
-    else if ( Abc_ObjFanin1(pFanout) == pObj )
+    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
         Abc_ObjSetFaninL1(pFanout, nLats);
     else 
         assert( 0 );
@@ -439,9 +582,9 @@ void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )
 void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )  
 { 
     assert( Abc_NtkIsSeq(pObj->pNtk) );
-    if ( Abc_ObjFanin0(pFanout) == pObj )
+    if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
         Abc_ObjAddFaninL0(pFanout, nLats);
-    else if ( Abc_ObjFanin1(pFanout) == pObj )
+    else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
         Abc_ObjAddFaninL1(pFanout, nLats);
     else 
         assert( 0 );
@@ -462,7 +605,7 @@ int Abc_ObjFanoutLMax( Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pFanout;
     int i, nLatch, nLatchRes;
-    nLatchRes = -1;
+    nLatchRes = 0;
     Abc_ObjForEachFanout( pObj, pFanout, i )
         if ( nLatchRes < (nLatch = Abc_ObjFanoutL(pObj, pFanout)) )
             nLatchRes = nLatch;
@@ -494,7 +637,6 @@ int Abc_ObjFanoutLMin( Abc_Obj_t * pObj )
 }
 
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcSeqRetime.c b/src/base/abc/abcSeqRetime.c
index ecd8b3d7..13b8a926 100644
--- a/src/base/abc/abcSeqRetime.c
+++ b/src/base/abc/abcSeqRetime.c
@@ -121,7 +121,7 @@ int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
     int RetValue, i, k;
 
     // set l-values of all nodes to be minus infinity
-    Vec_IntFill( pNtk->pData, Abc_NtkObjNum(pNtk), -ABC_INFINITY );
+    Vec_IntFill( pNtk->pData, Abc_NtkObjNumMax(pNtk), -ABC_INFINITY );
 
     // start the frontier by including PI fanouts
     vFrontier = Vec_PtrAlloc( 100 );
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index bf494767..ad732d2a 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -57,6 +57,8 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
+    int nNodes;
+
     assert( !Abc_NtkIsNetlist(pNtk) );
     if ( Abc_NtkIsLogicBdd(pNtk) )
     {
@@ -73,6 +75,8 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
     // print warning about self-feed latches
     if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
         printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
+    if ( nNodes = Abc_AigCleanup(pNtkAig->pManFunc) )
+        printf( "Cleanup has removed %d nodes.\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
         pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 );
@@ -106,16 +110,12 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes
     int i;
 
     // perform strashing
-    if ( fAllNodes )
-        vNodes = Abc_AigCollectAll( pNtk );
-    else
-        vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, fAllNodes );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
-    for ( i = 0; i < vNodes->nSize; i++ )
+    Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         // get the node
-        pNode = vNodes->pArray[i];
         assert( Abc_ObjIsNode(pNode) );
          // strash the node
         pNodeNew = Abc_NodeStrash( pMan, pNode );
@@ -159,9 +159,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
 //        pChild1 = Abc_ObjFanin1(pNode);
         if ( Abc_NodeIsConst(pNode) )
             return Abc_AigConst1(pMan);
-        return Abc_AigAnd( pMan, 
-            Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
-            Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) )  );
+        return Abc_AigAnd( pMan, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
     }
 
     // get the SOP of the node
@@ -471,7 +469,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, bool
 ***********************************************************************/
 int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate )
 {
-    Abc_Obj_t * p0, * p1;
     int RetValue1, RetValue2, i;
     // check if the node is visited
     if ( Abc_ObjRegular(pNode)->fMarkB )
@@ -496,12 +493,9 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst,
     }
     assert( !Abc_ObjIsComplement(pNode) );
     assert( Abc_ObjIsNode(pNode) );
-    // get the children
-    p0 = Abc_ObjNotCond( Abc_ObjFanin0(pNode), Abc_ObjFaninC0(pNode) );
-    p1 = Abc_ObjNotCond( Abc_ObjFanin1(pNode), Abc_ObjFaninC1(pNode) );
     // go through the branches
-    RetValue1 = Abc_NodeBalanceCone_rec( p0, vSuper, 0, fDuplicate );
-    RetValue2 = Abc_NodeBalanceCone_rec( p1, vSuper, 0, fDuplicate );
+    RetValue1 = Abc_NodeBalanceCone_rec( Abc_ObjChild0(pNode), vSuper, 0, fDuplicate );
+    RetValue2 = Abc_NodeBalanceCone_rec( Abc_ObjChild1(pNode), vSuper, 0, fDuplicate );
     if ( RetValue1 == -1 || RetValue2 == -1 )
         return -1;
     // return 1 if at least one branch has a duplicate
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 17f2f0c6..92d354ac 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -395,7 +395,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_Obj_t * pNode;
     int i, Counter;
     // mark the nodes reachable from the POs
-    vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 0 );
     for ( i = 0; i < vNodes->nSize; i++ )
     {
         pNode = vNodes->pArray[i];
diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c
index 861a1b14..d91a4443 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abc/abcTiming.c
@@ -235,7 +235,7 @@ void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk )
     int i;
     if ( pNtk->pManTime == NULL )
         return;
-    Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNum(pNtk), 0 );
+    Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNumMax(pNtk), 0 );
     // set the default timing
     ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray;
     Abc_NtkForEachPi( pNtk, pObj, i )
@@ -287,7 +287,7 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
         return;
     }
     // if timing manager is given, expand it if necessary
-    Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNum(pNtk), 0 );
+    Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNumMax(pNtk), 0 );
     // clean arrivals except for PIs
     ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray;
     Abc_NtkForEachNode( pNtk, pObj, i )
@@ -376,7 +376,7 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
     assert( Abc_NtkLatchNum(pNtkOld) == Abc_NtkLatchNum(pNtkNew) );
     // create the new timing manager
     pNtkNew->pManTime = Abc_ManTimeStart();
-    Abc_ManTimeExpand( pNtkNew->pManTime, Abc_NtkObjNum(pNtkNew), 0 );
+    Abc_ManTimeExpand( pNtkNew->pManTime, Abc_NtkObjNumMax(pNtkNew), 0 );
     // set the default timing
     pNtkNew->pManTime->tArrDef = pNtkOld->pManTime->tArrDef;
     pNtkNew->pManTime->tReqDef = pNtkOld->pManTime->tReqDef;
@@ -556,7 +556,7 @@ float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsLogicMap(pNtk) );
 
     Abc_NtkTimePrepare( pNtk );
-    vNodes = Abc_NtkDfs( pNtk );
+    vNodes = Abc_NtkDfs( pNtk, 1 );
     for ( i = 0; i < vNodes->nSize; i++ )
         Abc_NodeDelayTraceArrival( vNodes->pArray[i] );
     Vec_PtrFree( vNodes );
diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c
index 21196f97..b5a3a644 100644
--- a/src/base/abc/abcUnreach.c
+++ b/src/base/abc/abcUnreach.c
@@ -190,7 +190,7 @@ DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
         pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
         pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
         // get the initial value of the latch
-        bVar  = Cudd_NotCond( pbVarsX[i], (((int)pLatch->pData) != 1) );
+        bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
         bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
         Cudd_RecursiveDeref( dd, bTemp ); 
     }
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index f144bbdc..48fd2f66 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -640,7 +640,13 @@ int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
         else
             fclose( pFile );
 
-        pNtk1 = pNtk;
+        if ( Abc_NtkIsSeq(pNtk) )
+        {
+            pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
+            *pfDelete1 = 1;
+        }
+        else
+            pNtk1 = pNtk;
         pNtk2 = Io_Read( pNtk->pSpec, fCheck );
         if ( pNtk2 == NULL )
             return 0;
@@ -653,7 +659,13 @@ int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
             fprintf( pErr, "Empty current network.\n" );
             return 0;
         }
-        pNtk1 = pNtk;
+        if ( Abc_NtkIsSeq(pNtk) )
+        {
+            pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
+            *pfDelete1 = 1;
+        }
+        else
+            pNtk1 = pNtk;
         pNtk2 = Io_Read( argv[util_optind], fCheck );
         if ( pNtk2 == NULL )
             return 0;
@@ -766,10 +778,9 @@ int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
     return 0; 
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    [Collect all nodes by level.]
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
 
   Description []
                
@@ -778,23 +789,17 @@ int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk )
+int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
 {
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode;
-    int i;
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        Vec_PtrPush( vNodes, pNode );
-
-    // works only if the levels are set!!!
-    if ( !Abc_NtkIsAig(pNtk) )
-        Abc_NtkGetLevelNum(pNtk);
-
-    Vec_PtrSort( vNodes, Abc_NodeCompareLevelsIncrease );
-    return vNodes;
+    int Diff = strcmp( (char *)(*pp1)->pCopy, (char *)(*pp2)->pCopy );
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Gets fanin node names.]
@@ -867,6 +872,53 @@ char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos )
     return ppNames;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Orders PIs/POs/latches alphabetically.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // temporarily store the names in the copy field
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    // order objects alphabetically
+    qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), 
+        (int (*)(const void *, const void *)) Abc_NodeCompareNames );
+    qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), 
+        (int (*)(const void *, const void *)) Abc_NodeCompareNames );
+    // if the comparison if combinational (latches as PIs/POs), order them too
+    if ( fComb )
+    {
+        qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), 
+            (int (*)(const void *, const void *)) Abc_NodeCompareNames );
+        // add latches to make COs
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+        {
+            Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj );
+            Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj );
+        }
+    }
+    // clean the copy fields
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcVerify.c b/src/base/abc/abcVerify.c
index d0b424a9..55d6cf7d 100644
--- a/src/base/abc/abcVerify.c
+++ b/src/base/abc/abcVerify.c
@@ -57,7 +57,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         return;
     }
     if ( RetValue == 0 )
@@ -78,9 +78,9 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 
     // solve the CNF using the SAT solver
     if ( Abc_NtkMiterSat( pCnf, 0 ) )
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after SAT.\n" );
     else
-        printf( "Networks are equivalent.\n" );
+        printf( "Networks are equivalent after SAT.\n" );
     Abc_NtkDelete( pCnf );
 }
 
@@ -96,7 +96,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pMiter;
@@ -114,7 +114,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         return;
     }
     if ( RetValue == 0 )
@@ -126,6 +126,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 
     // convert the miter into a FRAIG
     Fraig_ParamsSetDefault( &Params );
+    Params.fVerbose = fVerbose;
     pFraig = Abc_NtkFraig( pMiter, &Params, 0 );
     Abc_NtkDelete( pMiter );
     if ( pFraig == NULL )
@@ -140,7 +141,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
         printf( "Networks are equivalent after fraiging.\n" );
         return;
     }
-    printf( "Networks are not equivalent.\n" );
+    printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
 }
 
 /**Function*************************************************************
@@ -172,7 +173,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         return;
     }
     if ( RetValue == 0 )
@@ -194,7 +195,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pFrames );
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after framing.\n" );
         return;
     }
     if ( RetValue == 0 )
@@ -215,9 +216,9 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
 
     // solve the CNF using the SAT solver
     if ( Abc_NtkMiterSat( pCnf, 0 ) )
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after SAT.\n" );
     else
-        printf( "Networks are equivalent.\n" );
+        printf( "Networks are equivalent after SAT.\n" );
     Abc_NtkDelete( pCnf );
 }
 
@@ -251,7 +252,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pMiter );
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         return;
     }
     if ( RetValue == 0 )
@@ -273,7 +274,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
     if ( RetValue == 1 )
     {
         Abc_NtkDelete( pFrames );
-        printf( "Networks are not equivalent.\n" );
+        printf( "Networks are NOT EQUIVALENT after framing.\n" );
         return;
     }
     if ( RetValue == 0 )
@@ -285,7 +286,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
 
     // convert the miter into a FRAIG
     Fraig_ParamsSetDefault( &Params );
-    pFraig = Abc_NtkFraig( pMiter, &Params, 0 );
+    pFraig = Abc_NtkFraig( pFrames, &Params, 0 );
     Abc_NtkDelete( pFrames );
     if ( pFraig == NULL )
     {
@@ -299,7 +300,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
         printf( "Networks are equivalent after fraiging.\n" );
         return;
     }
-    printf( "Networks are not equivalent.\n" );
+    printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
 }
 
 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index b1f44abd..1fe73690 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -28,6 +28,7 @@
 static int IoCommandRead        ( 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 );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 
@@ -56,6 +57,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read",          IoCommandRead,         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 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
 
@@ -232,6 +234,7 @@ usage:
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
     return 1;
 }
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -323,6 +326,86 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    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", ".mvpla", NULL ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pNtk = Io_ReadEdif( FileName, fCheck );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from EDIF file has failed.\n" );
+        return 1;
+    }
+
+    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    Abc_NtkDelete( pTemp );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_edif [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in EDIF (works only for ISCAS benchmarks)\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 IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pTemp;
@@ -521,12 +604,13 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[util_optind];
 
     // check the network type
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
-        fprintf( pAbc->Out, "Currently can only write logic networks and AIGs.\n" );
+        fprintf( pAbc->Out, "Currently can only write logic networks, AIGs, and seq AIGs.\n" );
         return 0;
     }
     Io_WriteBlifLogic( pNtk, FileName, fWriteLatches );
+//    Io_WriteBlif( pNtk, FileName, fWriteLatches );
     return 0;
 
 usage:
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 2465fa9f..d45b7b1b 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -51,6 +51,8 @@ extern Abc_Ntk_t *        Io_Read( char * pFileName, int fCheck );
 extern Abc_Ntk_t *        Io_ReadBlif( char * pFileName, int fCheck );
 /*=== abcReadBench.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadBench( char * pFileName, int fCheck );
+/*=== abcReadEdif.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadEdif( char * pFileName, int fCheck );
 /*=== abcReadVerilog.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcReadPla.c ==========================================================*/
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 8a0c11a5..75c87a80 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -49,6 +49,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
         pNtk = Io_ReadVerilog( pFileName, fCheck );
     else if ( Extra_FileNameCheckExtension( pFileName, "bench" ) )
         pNtk = Io_ReadBench( pFileName, fCheck );
+    else if ( Extra_FileNameCheckExtension( pFileName, "edf" ) )
+        pNtk = Io_ReadEdif( pFileName, fCheck );
     else if ( Extra_FileNameCheckExtension( pFileName, "pla" ) )
         pNtk = Io_ReadPla( pFileName, fCheck );
     else 
@@ -58,6 +60,7 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
     }
     if ( pNtk == NULL )
         return NULL;
+
     pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
     Abc_NtkDelete( pTemp );
     if ( pNtk == NULL )
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 9667fcc7..dd571f91 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -32,9 +32,9 @@ static Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p );
 
 /**Function*************************************************************
 
-  Synopsis    [Read the network from BENCH file.]
+  Synopsis    [Reads the network from a BENCH file.]
 
-  Description [Currently works only for the miter cone.]
+  Description []
                
   SideEffects []
 
@@ -68,9 +68,9 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
 }
 /**Function*************************************************************
 
-  Synopsis    [Read the network from BENCH file.]
+  Synopsis    []
 
-  Description [Currently works only for the miter cone.]
+  Description []
                
   SideEffects []
 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 693f1104..f598c4e5 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -66,9 +66,9 @@ static int Io_ReadBlifNetworkDefaultInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t *
 
 /**Function*************************************************************
 
-  Synopsis    [Read the network from BLIF file.]
+  Synopsis    [Reads the network from a BLIF file.]
 
-  Description []
+  Description [Works only for flat (non-hierarchical) BLIF.]
                
   SideEffects []
 
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
new file mode 100644
index 00000000..172849bd
--- /dev/null
+++ b/src/base/io/ioReadEdif.c
@@ -0,0 +1,228 @@
+/**CFile****************************************************************
+
+  FileName    [ioReadEdif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedure to read ISCAS benchmarks in EDIF.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioReadEdif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the network from an EDIF file.]
+
+  Description [Works only for the ISCAS benchmarks.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadEdif( char * pFileName, int fCheck )
+{
+    Extra_FileReader_t * p;
+    Abc_Ntk_t * pNtk;
+
+    // start the file
+    p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r()" );
+    if ( p == NULL )
+        return NULL;
+
+    // read the network
+    pNtk = Io_ReadEdifNetwork( p );
+    Extra_FileReaderFree( p );
+    if ( pNtk == NULL )
+        return NULL;
+
+    // make sure that everything is okay with the network structure
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Io_ReadEdif: The network check has failed.\n" );
+        Abc_NtkDelete( pNtk );
+        return NULL;
+    }
+    return pNtk;
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
+{
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vTokens;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNet, * pObj, * pFanout;
+    char * pGateName, * pNetName;
+    int fTokensReady, iLine, i;
+
+    // read the first line
+    vTokens = Extra_FileReaderGetTokens(p);
+    if ( strcmp( vTokens->pArray[0], "edif" ) != 0 )
+    {
+        printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
+        return NULL;
+    }
+    
+    // allocate the empty network
+    pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
+
+    // go through the lines of the file
+    fTokensReady = 0;
+    pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
+    for ( iLine = 1; fTokensReady || (vTokens = Extra_FileReaderGetTokens(p)); iLine++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
+
+        // get the type of the line
+        fTokensReady = 0;
+        if ( strcmp( vTokens->pArray[0], "instance" ) == 0 )
+        { 
+            pNetName = vTokens->pArray[1];
+            pNet = Abc_NtkFindOrCreateNet( pNtk, pNetName );
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            pGateName = vTokens->pArray[1];
+            if ( strncmp( pGateName, "Flip", 4 ) == 0 )
+                pObj = Abc_NtkCreateLatch( pNtk );
+            else
+            {
+                pObj = Abc_NtkCreateNode( pNtk );
+                pObj->pData = Abc_NtkRegisterName( pNtk, pGateName );
+            }
+            Abc_ObjAddFanin( pNet, pObj );
+        }
+        else if ( strcmp( vTokens->pArray[0], "net" ) == 0 )
+        {
+            pNetName = vTokens->pArray[1];
+            if ( strcmp( pNetName, "CK" ) == 0 || strcmp( pNetName, "RESET" ) == 0 )
+                continue;
+            if ( strcmp( pNetName + strlen(pNetName) - 4, "_out" ) == 0 )
+                pNetName[strlen(pNetName) - 4] = 0;
+            pNet = Abc_NtkFindNet( pNtk, pNetName );
+            assert( pNet );
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            while ( strcmp( vTokens->pArray[0], "portRef" ) == 0 )
+            {
+                if ( strcmp( pNetName, vTokens->pArray[3] ) != 0 )
+                {
+                    pFanout = Abc_NtkFindNet( pNtk, vTokens->pArray[3] );
+                    Abc_ObjAddFanin( Abc_ObjFanin0(pFanout), pNet );
+                }
+                vTokens = Extra_FileReaderGetTokens(p);
+            }
+            fTokensReady = 1;
+        }
+        else if ( strcmp( vTokens->pArray[0], "library" ) == 0 )
+        {
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            vTokens = Extra_FileReaderGetTokens(p);
+            while ( strcmp( vTokens->pArray[0], "port" ) == 0 )
+            {
+                pNetName = vTokens->pArray[1];
+                if ( strcmp( pNetName, "CK" ) == 0 || strcmp( pNetName, "RESET" ) == 0 )
+                {
+                    vTokens = Extra_FileReaderGetTokens(p);
+                    continue;
+                }
+                if ( strcmp( pNetName + strlen(pNetName) - 3, "_PO" ) == 0 )
+                    pNetName[strlen(pNetName) - 3] = 0;
+                if ( strcmp( vTokens->pArray[3], "INPUT" ) == 0 )
+                    Io_ReadCreatePi( pNtk, vTokens->pArray[1] );
+                else if ( strcmp( vTokens->pArray[3], "OUTPUT" ) == 0 )
+                    Io_ReadCreatePo( pNtk, vTokens->pArray[1] );
+                else
+                {
+                    printf( "%s (line %d): Wrong interface specification.\n", Extra_FileReaderGetFileName(p), iLine );
+                    Abc_NtkDelete( pNtk );
+                    return NULL;
+                }
+                vTokens = Extra_FileReaderGetTokens(p);
+            }
+        }
+        else if ( strcmp( vTokens->pArray[0], "design" ) == 0 )
+        {
+            free( pNtk->pName ); 
+            pNtk->pName = util_strsav( vTokens->pArray[3] );
+            break;
+        }
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // assign logic functions
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( strncmp( pObj->pData, "And", 3 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateAnd(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+        else if ( strncmp( pObj->pData, "Or", 2 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateOr(pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
+        else if ( strncmp( pObj->pData, "Nand", 4 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateNand(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+        else if ( strncmp( pObj->pData, "Nor", 3 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateNor(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+        else if ( strncmp( pObj->pData, "Exor", 4 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateXor(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+        else if ( strncmp( pObj->pData, "Exnor", 5 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateNxor(pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+        else if ( strncmp( pObj->pData, "Inv", 3 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateInv(pNtk->pManFunc) );
+        else if ( strncmp( pObj->pData, "Buf", 3 ) == 0 )
+            Abc_ObjSetData( pObj, Abc_SopCreateBuf(pNtk->pManFunc) );
+        else
+        {
+            printf( "%s: Unknown gate type \"%s\".\n", Extra_FileReaderGetFileName(p), pObj->pData );
+            Abc_NtkDelete( pNtk );
+            return NULL;
+        }
+    }
+    // check if constants have been added
+//    if ( pNet = Abc_NtkFindNet( pNtk, "VDD" ) )
+//        Io_ReadCreateConst( pNtk, "VDD", 1 );
+//    if ( pNet = Abc_NtkFindNet( pNtk, "GND" ) )
+//        Io_ReadCreateConst( pNtk, "GND", 0 );
+
+    Abc_NtkFinalizeRead( pNtk );
+    return pNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 951fb229..a334ded0 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -32,9 +32,9 @@ static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p );
 
 /**Function*************************************************************
 
-  Synopsis    [Read the network from BENCH file.]
+  Synopsis    [Reads the network from a PLA file.]
 
-  Description [Currently works only for the miter cone.]
+  Description []
                
   SideEffects []
 
@@ -68,9 +68,9 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
 }
 /**Function*************************************************************
 
-  Synopsis    [Read the network from BENCH file.]
+  Synopsis    []
 
-  Description [Currently works only for the miter cone.]
+  Description []
                
   SideEffects []
 
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 755fb1db..936a1c0c 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -124,9 +124,9 @@ static void           Io_ReadVerFree( Io_ReadVer_t * p );
 
 /**Function*************************************************************
 
-  Synopsis    [Read the network from BENCH file.]
+  Synopsis    [Reads the network from a Verilog file.]
 
-  Description [Currently works only for the miter cone.]
+  Description [Works only for IWLS 2005 benchmarks.]
                
   SideEffects []
 
@@ -633,9 +633,13 @@ bool Io_ReadVerNetworkGateComplex( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t
 bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTokens )
 {
     Abc_Obj_t * pLatch, * pNet;
+    char * pLatchName;
     char * pToken, * pToken2, * pTokenRN, * pTokenSN, * pTokenSI, * pTokenSE, * pTokenD, * pTokenQ, * pTokenQN;
     int k, fRN1, fSN1;
 
+    // get the latch name
+    pLatchName = vTokens->pArray[1];
+
     // collect the FF signals
     pTokenRN = pTokenSN = pTokenSI = pTokenSE = pTokenD = pTokenQ = pTokenQN = NULL;
     for ( k = 2; k < vTokens->nSize-1; k++ )
@@ -666,21 +670,21 @@ bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTo
     if ( pTokenD == NULL )
     {
         p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
-        sprintf( p->sError, "Cannot read pin D of the latch \"%s\".", vTokens->pArray[1] );
+        sprintf( p->sError, "Cannot read pin D of the latch \"%s\".", pLatchName );
         Io_ReadVerPrintErrorMessage( p );
         return 0;
     }
     if ( pTokenQ == NULL && pTokenQN == NULL )
     {
         p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
-        sprintf( p->sError, "Cannot read pins Q/QN of the latch \"%s\".", vTokens->pArray[1] );
+        sprintf( p->sError, "Cannot read pins Q/QN of the latch \"%s\".", pLatchName );
         Io_ReadVerPrintErrorMessage( p );
         return 0;
     }
     if ( (pTokenRN == NULL) ^ (pTokenSN == NULL) )
     {
         p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 1 );
-        sprintf( p->sError, "Cannot read pins RN/SN of the latch \"%s\".", vTokens->pArray[1] );
+        sprintf( p->sError, "Cannot read pins RN/SN of the latch \"%s\".", pLatchName );
         Io_ReadVerPrintErrorMessage( p );
         return 0;
     }
@@ -693,7 +697,7 @@ bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTo
     }
 
     // create the latch
-    pLatch = Io_ReadCreateLatch( pNtk, pTokenD, vTokens->pArray[1] );
+    pLatch = Io_ReadCreateLatch( pNtk, pTokenD, pLatchName );
 
     // create the buffer if Q signal is available
     if ( pTokenQ )
@@ -706,7 +710,7 @@ bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTo
             Io_ReadVerPrintErrorMessage( p );
             return 0;
         }
-        Io_ReadCreateBuf( pNtk, vTokens->pArray[1], pTokenQ );
+        Io_ReadCreateBuf( pNtk, pLatchName, pTokenQ );
     }
     if ( pTokenQN )
     {
@@ -718,26 +722,26 @@ bool Io_ReadVerNetworkLatch( Io_ReadVer_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vTo
             Io_ReadVerPrintErrorMessage( p );
             return 0;
         }
-        Io_ReadCreateInv( pNtk, vTokens->pArray[1], pTokenQN );
+        Io_ReadCreateInv( pNtk, pLatchName, pTokenQN );
     }
 
     // set the initial value
     if ( pTokenRN == NULL && pTokenSN == NULL )
-        Abc_ObjSetData( pLatch, (char *)2 );
+        Abc_LatchSetInitDc( pLatch );
     else 
     {
         fRN1 = (strcmp( pTokenRN, "1'b1" ) == 0);
         fSN1 = (strcmp( pTokenSN, "1'b1" ) == 0);
         if ( fRN1 && fSN1 )
-            Abc_ObjSetData( pLatch, (char *)2 );
+            Abc_LatchSetInitDc( pLatch );
         else if ( fRN1 )
-            Abc_ObjSetData( pLatch, (char *)1 );
+            Abc_LatchSetInit1( pLatch );
         else if ( fSN1 )
-            Abc_ObjSetData( pLatch, (char *)0 );
+            Abc_LatchSetInit0( pLatch );
         else
         {
             p->LineCur = Extra_FileReaderGetLineNumber( p->pReader, 0 );
-            sprintf( p->sError, "Cannot read the initial value of latch \"%s\".", vTokens->pArray[1] );
+            sprintf( p->sError, "Cannot read the initial value of latch \"%s\".", pLatchName );
             Io_ReadVerPrintErrorMessage( p );
             return 0;
         }
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 980015b2..7c4a4ab1 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -92,7 +92,7 @@ int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk )
             Abc_ObjName(pNode), Abc_ObjName(Abc_ObjFanin0(pNode)) );
 
     // write internal nodes
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 79de62b8..5c83aad2 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -86,6 +86,7 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
         return;
     }
     // write the model name
+    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
     // write the network
     Io_NtkWriteOne( pFile, pNtk, fWriteLatches );
@@ -145,7 +146,7 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     }
 
     // write each internal node
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 48e358e3..9c78b149 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -32,7 +32,7 @@ static int    Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk );
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the network in BENCH format.]
+  Synopsis    [Writes the network in PLA format.]
 
   Description []
                
@@ -69,7 +69,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the network in BENCH format.]
+  Synopsis    [Writes the network in PLA format.]
 
   Description []
author	Alan Mishchenko <alanmi@berkeley.edu>	2005-08-14 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2005-08-14 08:01:00 -0700
commit	9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4 (patch)
tree	52895e3901def014deaa5920d92637a8171d8acd /src/base
parent	f2b6b3be958e6d5629dc8a8b6c1b77195c16a2aa (diff)
download	abc-9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4.tar.gz abc-9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4.tar.bz2 abc-9b3fa55b8a6fca4fb75e0bbc9a8d52c5ab3c11e4.zip