Version abc50814

abc.dsp

@@ -301,6 +301,10 @@ SOURCE=.\src\base\io\ioReadBlif.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\io\ioReadEdif.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\io\ioReadPla.c
 # End Source File
 # Begin Source File

abc.plg

@@ -6,13 +6,13 @@
 --------------------Configuration: abc - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60E.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEE.tmp" with contents
 [
 /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c 
-"C:\_projects\abc\src\base\abc\abc.c"
+"C:\_projects\abc\src\map\mapper\mapperCut.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60E.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60F.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEE.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEF.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept 
 .\Debug\abc.obj
@@ -39,6 +39,8 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\abcRenode.obj
 .\Debug\abcRes.obj
 .\Debug\abcSat.obj
+.\Debug\abcSeq.obj
+.\Debug\abcSeqRetime.obj
 .\Debug\abcShow.obj
 .\Debug\abcSop.obj
 .\Debug\abcStrash.obj
@@ -57,6 +59,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\ioRead.obj
 .\Debug\ioReadBench.obj
 .\Debug\ioReadBlif.obj
+.\Debug\ioReadEdif.obj
 .\Debug\ioReadPla.obj
 .\Debug\ioReadVerilog.obj
 .\Debug\ioUtil.obj
@@ -266,15 +269,14 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\safe_mem.obj
 .\Debug\strsav.obj
 .\Debug\texpand.obj
-.\Debug\abcSeq.obj
-.\Debug\abcSeqRetime.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60F.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBEF.tmp"
 <h3>Output Window</h3>
 Compiling...
-abc.c
+mapperCut.c
+C:\_projects\abc\src\map\mapper\mapperCut.c(927) : warning C4101: 'Place' : unreferenced local variable
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBF0.tmp" with contents
 [
 /nologo /o"Debug/abc.bsc" 
 .\Debug\abc.sbr
@@ -301,6 +303,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp" with conte
 .\Debug\abcRenode.sbr
 .\Debug\abcRes.sbr
 .\Debug\abcSat.sbr
+.\Debug\abcSeq.sbr
+.\Debug\abcSeqRetime.sbr
 .\Debug\abcShow.sbr
 .\Debug\abcSop.sbr
 .\Debug\abcStrash.sbr
@@ -319,6 +323,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp" with conte
 .\Debug\ioRead.sbr
 .\Debug\ioReadBench.sbr
 .\Debug\ioReadBlif.sbr
+.\Debug\ioReadEdif.sbr
 .\Debug\ioReadPla.sbr
 .\Debug\ioReadVerilog.sbr
 .\Debug\ioUtil.sbr
@@ -527,17 +532,15 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp" with conte
 .\Debug\pathsearch.sbr
 .\Debug\safe_mem.sbr
 .\Debug\strsav.sbr
-.\Debug\texpand.sbr
-.\Debug\abcSeq.sbr
-.\Debug\abcSeqRetime.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp"
+.\Debug\texpand.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPBF0.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
 
 
 <h3>Results</h3>
-abc.exe - 0 error(s), 0 warning(s)
+abc.exe - 0 error(s), 1 warning(s)
 </pre>
 </body>
 </html>

abc.rc

@@ -3,8 +3,10 @@ alias clp collapse
 alias esd ext_seq_dcs
 alias f fraig
 alias fs fraig_sweep
+alias mu renode -m
 alias pf print_factor
 alias pfan print_fanio
+alias pl print_level
 alias pio print_io
 alias ps print_stats 
 alias psu print_supp
@@ -21,10 +23,11 @@ alias so source -x
 alias st strash
 alias u undo
 alias wb write_blif
-alias wg write_gate
 alias wl write_blif
 alias wp write_pla
 alias cnf   "st; renode -c; write_cnf"
 alias prove "st; renode -c; sat"
 alias opt   "st; b; renode; sop; ps"
 alias opts  "st; b; renode; sop; st; b; ps"
+alias share "st; b; renode -m; fx; st; b; ps"
+

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);
@@ -2984,14 +3069,18 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     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");

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,8 +318,8 @@ 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_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 );    
@@ -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                                ///

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
+    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 )
+            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 );

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
+    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;
 }
 

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
+    // copy the internal nodes
+    if ( Abc_NtkIsAig(pNtk) )
+        Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
+    else
+    {
+        // duplicate the nets and nodes (CIs/COs/latches already dupped)
         Abc_NtkForEachObj( pNtk, pObj, i )
             if ( pObj->pCopy == NULL )
                 Abc_NtkDupObj(pNtkNew, pObj);
-    // connect the objects
+        // reconnect all objects (no need to transfer attributes on edges)
         Abc_NtkForEachObj( pNtk, pObj, i )
             Abc_ObjForEachFanin( pObj, pFanin, k )
                 Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
-    // for AIGs copy the complemented attributes
-    if ( Abc_NtkIsAig(pNtk) )
-    {
-        // set the data pointers and complemented attributes
-        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 ???
     }
     // 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;

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;

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) );
 }

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);

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 );

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*************************************************************

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 );

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 );
-    }
     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);
 }
 
 

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;

src/base/abc/abcNetlist.c

@@ -84,19 +84,25 @@ 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 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) )

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 ( pLatch->pData == (void *)2 )
-                Counter1++;
-            else 
+        if ( Abc_LatchIsInitDc(pLatch) )
         {
+            Counter1++;
+            continue;
+        }
+        // count the number of cases when the constant is equal to the initial value
         if ( Abc_NtkIsAig(pNtk) )
         {
-                    if ( (pLatch->pData == (void *)1) ^ Abc_ObjFaninC0(pLatch) )
+            if ( Abc_LatchIsInit1(pLatch) == !Abc_ObjFaninC0(pLatch) )
                 Counter2++;
         }
         else
         {
-                    if ( (pLatch->pData == (void *)1) ^ Abc_NodeIsConst0(pLatch) )
+            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                                ///
 ////////////////////////////////////////////////////////////////////////

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 );

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, pObj->Id) );
-        Counter += Vec_IntEntry(vNumbers, pObj->Id);
+        assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) );
+        Counter += Vec_IntEntry(vNumbers, (int)pObj->Id);
+    }
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        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                                ///
 ////////////////////////////////////////////////////////////////////////

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 );

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

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];

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 );

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 ); 
     }

src/base/abc/abcUtil.c

@@ -640,6 +640,12 @@ int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
         else
             fclose( pFile );
 
+        if ( Abc_NtkIsSeq(pNtk) )
+        {
+            pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
+            *pfDelete1 = 1;
+        }
+        else
             pNtk1 = pNtk;
         pNtk2 = Io_Read( pNtk->pSpec, fCheck );
         if ( pNtk2 == NULL )
@@ -653,6 +659,12 @@ int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
             fprintf( pErr, "Empty current network.\n" );
             return 0;
         }
+        if ( Abc_NtkIsSeq(pNtk) )
+        {
+            pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
+            *pfDelete1 = 1;
+        }
+        else
             pNtk1 = pNtk;
         pNtk2 = Io_Read( argv[util_optind], fCheck );
         if ( pNtk2 == NULL )
@@ -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                                ///

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" );
 }
 
 

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:

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 ==========================================================*/

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 )

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 []
 

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 []
 

src/base/io/ioReadEdif.c

+/**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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+

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 []
 

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;
         }

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 );

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 );

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 []
                

src/map/mapper/mapperCut.c

@@ -926,6 +926,7 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
     Map_Cut_t * pCut;
     int Place, i;
 //    int clk;
+/*
     // check the cut
     Place = Map_CutTableLookup( p, ppNodes, nNodes );
     if ( Place == -1 )
@@ -933,6 +934,7 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
     assert( nNodes > 0 );
     // create the new cut
 //clk = clock();
+*/
     pCut = Map_CutAlloc( pMan );
 //pMan->time1 += clock() - clk;
     pCut->nLeaves = nNodes;
@@ -942,12 +944,15 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
         pCut->ppLeaves[i] = ppNodes[i];
 //        pCut->fLevel += ppNodes[i]->Level;
     }
+/*
 //    pCut->fLevel /= nNodes;
     // add the cut to the table
     assert( p->pBins[Place] == NULL );
     p->pBins[Place] = pCut;
     // add the cut to the new list
     p->pCuts[ p->nCuts++ ] = Place;
+*/
+
     return pCut;
 }
 

src/misc/vec/vecFan.h

@@ -39,8 +39,8 @@
 typedef struct Abc_Fan_t_       Abc_Fan_t;
 struct Abc_Fan_t_ // 1 word
 {
-    unsigned         iFan    : 26;  // the ID of the object
-    unsigned         nLats   :  5;  // the number of latches (up to 31)
+    unsigned         iFan    : 24;  // the ID of the object
+    unsigned         nLats   :  7;  // the number of latches (up to 31)
     unsigned         fCompl  :  1;  // the complemented attribute
 };
 
@@ -279,6 +279,7 @@ static inline int Vec_FanFindEntry( Vec_Fan_t * p, unsigned iFan )
 ***********************************************************************/
 static inline int Vec_FanDeleteEntry( Vec_Fan_t * p, unsigned iFan )
 {
+/*
     int i, k, fFound = 0;
     for ( i = k = 0; i < p->nSize; i++ )
     {
@@ -289,6 +290,17 @@ static inline int Vec_FanDeleteEntry( Vec_Fan_t * p, unsigned iFan )
     }
     p->nSize = k;
     return fFound;
+*/
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i].iFan == iFan )
+            break;
+    if ( i == p->nSize )
+        return 0;
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+    return 1;
 }
 
 /**Function*************************************************************

src/sat/sim/simMan.c

@@ -51,12 +51,12 @@ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
     // internal simulation information
     p->nSimBits   = 2048;
     p->nSimWords  = SIM_NUM_WORDS(p->nSimBits);
-    p->vSim0      = Sim_UtilInfoAlloc( pNtk->vObjs->nSize, p->nSimWords, 0 );
-    p->vSim1      = Sim_UtilInfoAlloc( pNtk->vObjs->nSize, p->nSimWords, 0 );
+    p->vSim0      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
+    p->vSim1      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
     // support information
     p->nSuppBits  = Abc_NtkCiNum(pNtk);
     p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits);
-    p->vSuppStr   = Sim_UtilInfoAlloc( pNtk->vObjs->nSize, p->nSuppWords, 1 );
+    p->vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSuppWords, 1 );
     p->vSuppFun   = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk),  p->nSuppWords, 1 );
     // other data
     p->pMmPat     = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) );