Version abc61122

27 files changed, 757 insertions, 664 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dffe4b99..9613ab40 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22,10 +22,9 @@
 #include "mainInt.h"
 #include "fraig.h"
 #include "fxu.h"
-#include "fpga.h"
-#include "pga.h"
 #include "cut.h"
-//#include "seq.h"
+#include "fpga.h"
+#include "if.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -46,12 +45,10 @@ static int Abc_CommandPrintAuto      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandPrintKMap      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintGates     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSharing   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSkews     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandShow           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowBdd        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowCut        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowAig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowNtk        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCollapse       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandStrash         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -123,7 +120,7 @@ static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** arg
 
 static int Abc_CommandFpga           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFpgaFast       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPga            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIf             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInit           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -145,9 +142,6 @@ static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-static int Abc_CommandHoward       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSkewForward  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -182,12 +176,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_sharing", Abc_CommandPrintSharing,     0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "print_skews",   Abc_CommandPrintSkews,       0 );
 
+    Cmd_CommandAdd( pAbc, "Printing",     "show",          Abc_CommandShow,             0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "show_aig",      Abc_CommandShowAig,          0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "show_ntk",      Abc_CommandShowNtk,          0 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
@@ -259,7 +251,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "if",            Abc_CommandIf,               1 );
 
 //    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
@@ -281,9 +273,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
 
-//    Cmd_CommandAdd( pAbc, "Sequential",   "howard",        Abc_CommandHoward,           0 );
-//    Cmd_CommandAdd( pAbc, "Sequential",   "skew_fwd",      Abc_CommandSkewForward,      0 );
-
 //    Rwt_Man4ExploreStart();
 //    Map_Var3Print();
 //    Map_Var4Test();
@@ -1383,29 +1372,38 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandPrintSkews( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    int fPrintAll;
+    int fSeq;
+    int fGateNames;
+    int fUseReverse;
+    extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames, int fSeq, int fUseReverse );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fPrintAll = 0;
+    fSeq        = 0;
+    fGateNames  = 0;
+    fUseReverse = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rsgh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'a':
-            fPrintAll = 1;
+        case 'r':
+            fUseReverse ^= 1;
+            break;
+        case 's':
+            fSeq ^= 1;
+            break;
+        case 'g':
+            fGateNames ^= 1;
             break;
-        case 'h':
-            goto usage;
         default:
             goto usage;
         }
@@ -1417,25 +1415,19 @@ int Abc_CommandPrintSkews( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 )
-    {
-        fprintf( pErr, "The network has no latches.\n" );
-        return 0;
-    }
-
-    if ( pNtk->vSkews == NULL || pNtk->vSkews->nSize == 0 )
-    {
-        fprintf( pErr, "The network has no clock skew schedule.\n" );
-        return 0;
-    }
-
-    Abc_NtkPrintSkews( pOut, pNtk, fPrintAll );
+    Abc_NtkShow( pNtk, fGateNames, fSeq, fUseReverse );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_skews [-h] [-a]\n" );
-    fprintf( pErr, "\t        prints information about a clock skew schedule\n" );
-    fprintf( pErr, "\t-a    : dumps the skew of every latch [default = no]\n");
+    fprintf( pErr, "usage: show [-srgh]\n" );
+    fprintf( pErr, "       visualizes the network structure using DOT and GSVIEW\n" );
+#ifdef WIN32
+    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+    fprintf( pErr, "\t-s    : toggles visualization of sequential networks [default = %s].\n", fSeq? "yes": "no" );  
+    fprintf( pErr, "\t-r    : toggles ordering nodes in reverse order [default = %s].\n", fUseReverse? "yes": "no" );  
+    fprintf( pErr, "\t-g    : toggles printing gate names for mapped network [default = %s].\n", fGateNames? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -1628,145 +1620,6 @@ usage:
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int fMulti;
-    extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesShow );
-    extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    fMulti = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'm':
-            fMulti ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( pErr, "Visualizing networks other than AIGs can be done using command \"show_ntk\".\n" );
-        return 1;
-    }
-
-    if ( fMulti && !Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( pErr, "Visualizing multi-input ANDs cannot be done for sequential network (run \"unseq\").\n" );
-        return 1;
-    }
-
-    if ( !fMulti )
-        Abc_NtkShowAig( pNtk, NULL );
-    else
-        Abc_NtkShowMulti( pNtk );
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: show_aig [-h]\n" );
-    fprintf( pErr, "       visualizes the AIG with choices using DOT and GSVIEW\n" );
-#ifdef WIN32
-    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
-    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
-#endif
-    fprintf( pErr, "\t-m    : toggles visualization of multi-input ANDs [default = %s].\n", fMulti? "yes": "no" );  
-    fprintf( pErr, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int fGateNames;
-    extern void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    fGateNames = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'g':
-            fGateNames ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( pErr, "Visualizing AIG can only be done using command \"show_aig\".\n" );
-        return 1;
-    }
-    Abc_NtkShow( pNtk, fGateNames );
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: show_ntk [-gh]\n" );
-    fprintf( pErr, "       visualizes the network structure using DOT and GSVIEW\n" );
-#ifdef WIN32
-    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
-    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
-#endif
-    fprintf( pErr, "\t-g    : toggles printing gate names for mapped network [default = %s].\n", fGateNames? "yes": "no" );  
-    fprintf( pErr, "\t-h    : print the command usage\n");
-    return 1;
-}
-
 
 /**Function*************************************************************
 
@@ -5136,8 +4989,8 @@ int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames    = 50;
-    fVerbose   =  0;
+    nFrames    = 100;
+    fVerbose   =   0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
     {
@@ -5633,7 +5486,7 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fUpdateLevel = 1;
+    fUpdateLevel = 0;
     fUseZeroCost = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
@@ -7343,7 +7196,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     if ( DelayTarget == -1 ) 
-        sprintf( Buffer, "not used" );
+        sprintf( Buffer, "best possible" );
     else
         sprintf( Buffer, "%.2f", DelayTarget );
     if ( nLutSize == -1 ) 
@@ -7394,7 +7247,7 @@ int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
     fRecovery   = 1;
     fVerbose    = 0;
     DelayTarget =-1;
-    nLutSize    = 8;
+    nLutSize    = 5;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "avhDK" ) ) != EOF )
     {
@@ -7514,46 +7367,90 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    char Buffer[100];
+    char LutSize[100];
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    Pga_Params_t Params, * pParams = &Params;
+    If_Par_t Pars, * pPars = &Pars;
     int c;
-    extern Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams );
+    extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    memset( pParams, 0, sizeof(Pga_Params_t) );
-    pParams->pNtk       = pNtk;
-    pParams->pLutLib    = Abc_FrameReadLibLut();
-    pParams->fAreaFlow  = 1;
-    pParams->fArea      = 1;
-    pParams->fSwitching = 0;
-    pParams->fDropCuts  = 0;
-    pParams->fVerbose   = 0;
+    memset( pPars, 0, sizeof(If_Par_t) );
+    pPars->Mode        = 1;
+    pPars->nLutSize    = 4;
+//    pPars->pLutLib    = Abc_FrameReadLibLut();
+    pPars->nCutsMax    = 2;
+    pPars->fSeq        = 0;
+    pPars->fLatchPaths = 0;
+    pPars->nLatches    = 0;
+    pPars->pTimesArr   = Abc_NtkGetCiArrivalFloats(pNtk);
+    pPars->pTimesReq   = NULL;
+    pPars->DelayTarget = -1;
+    pPars->fVerbose    = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "fapdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDlsvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'f':
-            pParams->fAreaFlow ^= 1;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-M\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->Mode = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->Mode < 0 ) 
+                goto usage;
             break;
-        case 'a':
-            pParams->fArea ^= 1;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLutSize < 0 ) 
+                goto usage;
             break;
-        case 'p':
-            pParams->fSwitching ^= 1;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            pPars->nCutsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutsMax < 0 ) 
+                goto usage;
             break;
-        case 'd':
-            pParams->fDropCuts ^= 1;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            pPars->DelayTarget = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->DelayTarget <= 0.0 ) 
+                goto usage;
+            break;
+        case 'l':
+            pPars->fLatchPaths ^= 1;
+            break;
+        case 's':
+            pPars->fSeq ^= 1;
             break;
         case 'v':
-            pParams->fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'h':
         default:
@@ -7567,8 +7464,18 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    printf( "This command is not yet implemented.\n" );
-    return 0;
+    if ( pPars->Mode < 0 || pPars->Mode > 4 )
+    {
+        fprintf( pErr, "Incorrect mapping mode.\n" );
+        return 1;
+    }
+
+    // set the latch paths
+    if ( pPars->fLatchPaths )
+    {
+        for ( c = 0; c < Abc_NtkPiNum(pNtk); c++ )
+            pPars->pTimesArr[c] = -ABC_INFINITY;
+    }
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
@@ -7588,7 +7495,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
         fprintf( pOut, "The network was strashed and balanced before FPGA mapping.\n" );
         // get the new network
-        pNtkRes = Abc_NtkPga( pParams );
+        pNtkRes = Abc_NtkIf( pNtk, pPars );
         if ( pNtkRes == NULL )
         {
             Abc_NtkDelete( pNtk );
@@ -7600,7 +7507,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
     else
     {
         // get the new network
-        pNtkRes = Abc_NtkPga( pParams );
+        pNtkRes = Abc_NtkIf( pNtk, pPars );
         if ( pNtkRes == NULL )
         {
             fprintf( pErr, "FPGA mapping has failed.\n" );
@@ -7612,14 +7519,28 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: pga [-fapdvh]\n" );
-    fprintf( pErr, "\t        performs FPGA mapping of the current network\n" );
-    fprintf( pErr, "\t-f    : toggles area flow recovery [default = %s]\n", pParams->fAreaFlow? "yes": "no" );
-    fprintf( pErr, "\t-a    : toggles area recovery [default = %s]\n", pParams->fArea? "yes": "no" );
-    fprintf( pErr, "\t-p    : optimizes power by minimizing switching activity [default = %s]\n", pParams->fSwitching? "yes": "no" );
-    fprintf( pErr, "\t-d    : toggles dropping cuts to save memory [default = %s]\n", pParams->fDropCuts? "yes": "no" );
-    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h    : prints the command usage\n");
+    if ( pPars->DelayTarget == -1 ) 
+        sprintf( Buffer, "best possible" );
+    else
+        sprintf( Buffer, "%.2f", pPars->DelayTarget );
+    if ( pPars->nLutSize == -1 ) 
+        sprintf( LutSize, "library" );
+    else
+        sprintf( LutSize, "%d", pPars->nLutSize );
+    fprintf( pErr, "usage: if [-M num] [-K num] [-C num] [-D float] [-lsvh]\n" );
+    fprintf( pErr, "\t           performs FPGA mapping of the network as follows:\n" );
+    fprintf( pErr, "\t               1 - delay only\n" );
+    fprintf( pErr, "\t               2 - area only\n" );
+    fprintf( pErr, "\t               3 - area under delay constraints\n" );
+    fprintf( pErr, "\t               4 - area under delay constraints with area recovery\n" );
+    fprintf( pErr, "\t-M num   : the mapping mode [default = %d]\n", pPars->Mode );
+    fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < 32) [default = %s]\n", LutSize );
+    fprintf( pErr, "\t-C num   : the max number of cuts to use (1 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
+    fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+    fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeq? "yes": "no" );
+    fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : prints the command usage\n");
     return 1;
 }
 
@@ -7996,7 +7917,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
     Mode      =  5;
     fForward  =  0;
     fBackward =  0;
-    fVerbose  =  1;
+    fVerbose  =  0;
     nMaxIters = 15;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF )
@@ -8048,6 +7969,12 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
+    if ( Mode < 0 || Mode > 6 )
+    {
+        fprintf( pErr, "The mode (%d) is incorrect. Retiming is not performed.\n", Mode );
+        return 0;
+    }
+
     if ( Abc_NtkIsStrash(pNtk) )
     {
         if ( Abc_NtkGetChoiceNum(pNtk) )
@@ -8089,6 +8016,7 @@ usage:
     fprintf( pErr, "\t             3: forward and backward min-area retiming\n" );
     fprintf( pErr, "\t             4: forward and backward min-delay retiming\n" );
     fprintf( pErr, "\t             5: mode 3 followed by mode 4\n" );
+    fprintf( pErr, "\t             6: Pan's optimum-delay retiming using binary search\n" );
     fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode );
     fprintf( pErr, "\t-f     : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" );
     fprintf( pErr, "\t-b     : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" );
@@ -8488,6 +8416,8 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    int fLatchSweep;
+    int fAutoSweep;
     int fVerbose;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -8495,12 +8425,20 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose = 1;
+    fLatchSweep = 0;
+    fAutoSweep  = 0;
+    fVerbose    = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lavh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'l':
+            fLatchSweep ^= 1;
+            break;
+        case 'a':
+            fAutoSweep ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8521,16 +8459,18 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    Abc_NtkCleanupSeq( pNtk, fVerbose );
+    Abc_NtkCleanupSeq( pNtk, fLatchSweep, fAutoSweep, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scleanup [-vh]\n" );
+    fprintf( pErr, "usage: scleanup [-lavh]\n" );
     fprintf( pErr, "\t         performs sequential cleanup\n" );
     fprintf( pErr, "\t         - removes nodes/latches that do not feed into POs\n" );
     fprintf( pErr, "\t         - removes and shared latches driven by constants\n" );
     fprintf( pErr, "\t         - replaces autonomous logic by free PI variables\n" );
     fprintf( pErr, "\t           (the latter may change sequential behaviour)\n" );
+    fprintf( pErr, "\t-l     : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
+    fprintf( pErr, "\t-a     : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -8694,7 +8634,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fSat     =  0;
     fVerbose =  0;
-    nFrames  =  3;
+    nFrames  =  5;
     nSeconds = 20;
     nConfLimit = 10000;   
     nInsLimit  = 0;
@@ -8758,6 +8698,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        printf( "The network has no latches. Used combinational command \"cec\".\n" );
+        return 0;
+    }
+
     pArgvNew = argv + globalUtilOptind;
     nArgcNew = argc - globalUtilOptind;
     if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
@@ -9290,168 +9236,6 @@ usage:
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandHoward( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int fVerbose;
-    double result;
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    fVerbose =  0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 )
-    {
-        fprintf( pErr, "The network has no latches. Analysis is not performed.\n" );
-        return 0;
-    }
-
-    if ( Abc_NtkHasAig(pNtk) )
-    {
-        // quit if there are choice nodes
-        if ( Abc_NtkGetChoiceNum(pNtk) )
-        {
-            fprintf( pErr, "Currently cannot analyze networks with choice nodes.\n" );
-            return 0;
-        }
-
-        /*
-        if ( Abc_NtkIsStrash(pNtk) )
-            pNtkRes = Abc_NtkAigToSeq(pNtk);
-        else
-            pNtkRes = Abc_NtkDup(pNtk);
-
-        */
-
-        fprintf( pErr, "Currently cannot analyze unmapped networks.\n" );
-        return 0;
-    }
-
-//    result = Seq_NtkHoward( pNtk, fVerbose );
-    result = 0;
-
-    if (result < 0) {
-      fprintf( pErr, "Analysis failed.\n" );
-      return 0;
-    }
-
-    printf("Maximum mean cycle time = %.2f\n", result);
-
-    return 1;
-
-usage:
-    fprintf( pErr, "usage: howard [-h]\n" );
-    fprintf( pErr, "\t         computes the maximum mean cycle time using Howard's algorithm\n" );
-    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandSkewForward( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int fMinimize;
-    float target;
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    target = pNtk->maxMeanCycle;
-    fMinimize =  0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'm':
-            fMinimize ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 )
-    {
-        fprintf( pErr, "The network has no latches.\n" );
-        return 0;
-    }
-
-    if ( pNtk->vSkews == NULL || pNtk->vSkews->nSize == 0 )
-    {
-        fprintf( pErr, "The network has no clock skew schedule.\n" );
-        return 0;
-    }
-
-//    Seq_NtkSkewForward( pNtk, target, fMinimize );
-
-    return 1;
-
-usage:
-    fprintf( pErr, "usage: skew_fwd [-h] [-m] [-t float]\n" );
-    fprintf( pErr, "\t         converts a skew schedule into a set of forward skews 0<skew<T\n" );
-    fprintf( pErr, "\t-m     : minimizes sum of skews [default = %s]\n", fMinimize? "yes": "no" );
-    fprintf( pErr, "\t-t     : clock period, T [default = maxMeanCycle] (unimplemented)\n");
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index cc6e8913..3b307ac2 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -49,16 +49,24 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
     char ** pInputNames;    // pointers to the CI names
     char ** pOutputNames;   // pointers to the CO names
     int nOutputs, nInputs, i;
+    Vec_Ptr_t * vFuncsGlob;
+    Abc_Obj_t * pObj;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
+    if ( Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose) == NULL )
         return;
 
     // get information about the network
     nInputs  = Abc_NtkCiNum(pNtk);
     nOutputs = Abc_NtkCoNum(pNtk);
-    dd       = pNtk->pManGlob;
-    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
+//    dd       = pNtk->pManGlob;
+    dd = Abc_NtkGlobalBddMan( pNtk );
+
+    // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_PtrPush( vFuncsGlob, Abc_ObjGlobalBdd(pObj) );
+    pbGlobal = (DdNode **)Vec_PtrArray( vFuncsGlob );
 
     // get the network names
     pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
@@ -83,12 +91,14 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
         Abc_NtkAutoPrintOne( dd, nInputs, pbGlobal, Output, pInputNames, pOutputNames, fNaive );
 
     // deref the PO functions
-    Abc_NtkFreeGlobalBdds( pNtk );
+//    Abc_NtkFreeGlobalBdds( pNtk );
     // stop the global BDD manager
-    Extra_StopManager( pNtk->pManGlob );
-    pNtk->pManGlob = NULL;
+//    Extra_StopManager( pNtk->pManGlob );
+//    pNtk->pManGlob = NULL;
+    Abc_NtkFreeGlobalBdds( pNtk, 1 );
     free( pInputNames );
     free( pOutputNames );
+    Vec_PtrFree( vFuncsGlob );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index 650f379f..ce67aff7 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -49,25 +49,27 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
 
     assert( Abc_NtkIsStrash(pNtk) );
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL )
+    if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
         return NULL;
     if ( fVerbose )
     {
-        printf( "The shared BDD size is %d nodes.  ", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
+        DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
+        printf( "The shared BDD size is %d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
         PRT( "BDD construction time", clock() - clk );
     }
 
     // create the new network
     pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
-    Abc_NtkFreeGlobalBdds( pNtk );
+//    Abc_NtkFreeGlobalBdds( pNtk );
+    Abc_NtkFreeGlobalBdds( pNtk, 1 );
     if ( pNtkNew == NULL )
     {
-        Cudd_Quit( pNtk->pManGlob );
-        pNtk->pManGlob = NULL;
+//        Cudd_Quit( pNtk->pManGlob );
+//        pNtk->pManGlob = NULL;
         return NULL;
     }
-    Extra_StopManager( pNtk->pManGlob );
-    pNtk->pManGlob = NULL;
+//    Extra_StopManager( pNtk->pManGlob );
+//    pNtk->pManGlob = NULL;
 
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
@@ -100,8 +102,9 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
 {
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pNode, * pNodeNew;
-    DdManager * dd = pNtk->pManGlob;
+    Abc_Obj_t * pNode, * pDriver, * pNodeNew;
+//    DdManager * dd = pNtk->pManGlob;
+    DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
     int i;
     // start the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
@@ -112,7 +115,14 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
+        pDriver = Abc_ObjFanin0(pNode);
+        if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) )
+        {
+            Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
+            continue;
+        }
+//        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Abc_ObjGlobalBdd(pNode) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index c021728a..f1dd4ab5 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -202,6 +202,7 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
 ***********************************************************************/
 Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
 {
+/*
     Cut_Man_t *  p;
     Abc_Obj_t * pObj, * pNode;
     int i, nIters, fStatus;
@@ -288,6 +289,8 @@ printf( "Converged after %d iterations.\n", nIters );
 }
 //Abc_NtkPrintCuts( p, pNtk, 1 );
     return p;
+*/
+    return NULL;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index 4d37c496..7771148e 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -86,7 +86,8 @@ void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) )
             else // no bug
                 Abc_NtkDelete( pNtkMod );
         }
-        printf( "Iteration %6d : Nodes = %6d. Steps = %6d. Error step = %3d.  ", nIter, Abc_NtkObjNum(pNtk), nSteps, i );
+        printf( "Iter %6d : Latches = %6d. Nodes = %6d. Steps = %6d. Error step = %3d.  ", 
+            nIter, Abc_NtkLatchNum(pNtk), Abc_NtkNodeNum(pNtk), nSteps, i );
         PRT( "Time", clock() - clk );
         if ( i == nSteps ) // could not modify it while preserving the bug
             break;
@@ -116,7 +117,11 @@ int Abc_NtkCountFaninsTotal( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            if ( Abc_NodeIsConst(pFanin) )
+            if ( !Abc_ObjIsNode(pObj) && !Abc_ObjIsPo(pObj) )
+                continue;
+            if ( Abc_ObjIsPo(pObj) && Abc_NtkPoNum(pNtk) == 1 )
+                continue;
+            if ( Abc_ObjIsNode(pObj) && Abc_NodeIsConst(pFanin) )
                 continue;
             Counter++;
         }
@@ -141,7 +146,11 @@ int Abc_NtkFindGivenFanin( Abc_Ntk_t * pNtk, int Step, Abc_Obj_t ** ppObj, Abc_O
     Abc_NtkForEachObj( pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pFanin, k )
         {
-            if ( Abc_NodeIsConst(pFanin) )
+            if ( !Abc_ObjIsNode(pObj) && !Abc_ObjIsPo(pObj) )
+                continue;
+            if ( Abc_ObjIsPo(pObj) && Abc_NtkPoNum(pNtk) == 1 )
+                continue;
+            if ( Abc_ObjIsNode(pObj) && Abc_NodeIsConst(pFanin) )
                 continue;
             if ( Counter++ == Step )
             {
@@ -166,6 +175,7 @@ int Abc_NtkFindGivenFanin( Abc_Ntk_t * pNtk, int Step, Abc_Obj_t ** ppObj, Abc_O
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1 )
 {
+    extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pObj, * pFanin, * pConst;
     // copy the network
@@ -185,9 +195,9 @@ Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1
     Abc_NtkDeleteAll_rec( pFanin );
 
     Abc_NtkSweep( pNtk, 0 );
-    Abc_NtkCleanupSeq( pNtk, 0 );
+    Abc_NtkCleanupSeq( pNtk, 0, 0, 0 );
     Abc_NtkLogicToSop( pNtk, 0 );
-    Abc_NtkCycleInitStateSop( pNtk, 20, 0 );
+    Abc_NtkCycleInitStateSop( pNtk, 50, 0 );
     return pNtk;
 }
 
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index b38012cd..200f4eec 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -55,31 +55,22 @@ static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int n
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
 {
+    DdManager * dd;
     Abc_Ntk_t * pNtkNew;
-
     assert( Abc_NtkIsStrash(pNtk) );
-
-    // perform FPGA mapping
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
+    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
+    if ( dd == NULL )
         return NULL;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
-
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
     // transform the result of mapping into a BDD network
     pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
+    Extra_StopManager( dd );
     if ( pNtkNew == NULL )
-    {
-        Cudd_Quit( pNtk->pManGlob );
-        pNtk->pManGlob = NULL;
         return NULL;
-    }
-    Extra_StopManager( pNtk->pManGlob );
-    pNtk->pManGlob = NULL;
-
+    // copy EXDC network
     if ( pNtk->pExdc )
         pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-
-    // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
@@ -102,26 +93,25 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
 {
-    DdManager * dd = pNtk->pManGlob;
+    char ** ppNamesCi, ** ppNamesCo;
+    Vec_Ptr_t * vFuncsGlob;
     Dsd_Manager_t * pManDsd;
     Abc_Ntk_t * pNtkNew;
-    DdNode * bFunc;
-    char ** ppNamesCi, ** ppNamesCo;
+    DdManager * dd;
     Abc_Obj_t * pObj;
     int i;
 
     // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        bFunc = Vec_PtrEntry(pNtk->vFuncsGlob, i);
-        Vec_PtrWriteEntry(pNtk->vFuncsGlob, i, Cudd_NotCond(bFunc, Abc_ObjFaninC0(pObj)) );
-    }
+        Vec_PtrPush( vFuncsGlob, Cudd_NotCond(Abc_ObjGlobalBdd(pObj), Abc_ObjFaninC0(pObj)) );
 
     // perform the decomposition
-    assert( Vec_PtrSize(pNtk->vFuncsGlob) == Abc_NtkCoNum(pNtk) );
+    dd = Abc_NtkGlobalBddMan(pNtk);
     pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
-    Dsd_Decompose( pManDsd, (DdNode **)pNtk->vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
-    Abc_NtkFreeGlobalBdds( pNtk );
+    Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
+    Vec_PtrFree( vFuncsGlob );
+    Abc_NtkFreeGlobalBdds( pNtk, 0 );
     if ( pManDsd == NULL )
     {
         Cudd_Quit( dd );
@@ -138,7 +128,6 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bo
     Abc_NtkFinalize( pNtk, pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
-
     if ( fPrint )
     {
         ppNamesCi = Abc_NtkCollectCioNames( pNtk, 0 );
diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c
index 3ad29291..356b855e 100644
--- a/src/base/abci/abcFpgaFast.c
+++ b/src/base/abci/abcFpgaFast.c
@@ -118,7 +118,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
                 // clone the node
                 pObj = Abc_NtkCloneObj( pObjAbc );
                 // set complemented functions
-                pObj->pData = Aig_Not( pObjAbc->pData );
+                pObj->pData = Hop_Not( pObjAbc->pData );
                 // return the new node
                 pObjAbc = pObj;
             }
@@ -172,9 +172,9 @@ Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj
     Ivy_ManForEachNodeVec( pMan, vNodes, pNodeIvy, i )
     {
         if ( i < Vec_IntSize(vSupp) )
-            pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_IthVar( pNtkNew->pManFunc, i );
+            pNodeIvy->pEquiv = (Ivy_Obj_t *)Hop_IthVar( pNtkNew->pManFunc, i );
         else
-            pNodeIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pNtkNew->pManFunc, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pNodeIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pNodeIvy) );
+            pNodeIvy->pEquiv = (Ivy_Obj_t *)Hop_And( pNtkNew->pManFunc, (Hop_Obj_t *)Ivy_ObjChild0Equiv(pNodeIvy), (Hop_Obj_t *)Ivy_ObjChild1Equiv(pNodeIvy) );
     }
     // set the local function
     pObjAbc->pData = (Abc_Obj_t *)pObjIvy->pEquiv;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
new file mode 100644
index 00000000..6b3e0e7c
--- /dev/null
+++ b/src/base/abci/abcIf.c
@@ -0,0 +1,287 @@
+/**CFile****************************************************************
+
+  FileName    [abcIf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - November 21, 2006.]
+
+  Revision    [$Id: abcIf.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "if.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
+static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
+static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut );
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
+{
+    Abc_Ntk_t * pNtkNew;
+    If_Man_t * pIfMan;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // print a warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Performing FPGA mapping with choices.\n" );
+
+    // perform FPGA mapping
+    pIfMan = Abc_NtkToIf( pNtk, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+
+    // transform the result of mapping into a BDD network
+    pNtkNew = Abc_NtkFromIf( pIfMan, pNtk );
+    if ( pNtkNew == NULL )
+        return NULL;
+    If_ManStop( pIfMan );
+
+    // duplicate EXDC
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkIf: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
+{
+    ProgressBar * pProgress;
+    If_Man_t * pIfMan;
+    Abc_Obj_t * pNode, * pFanin, * pPrev;
+    int i;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // start the mapping manager and set its parameters
+    pIfMan = If_ManStart( pPars );
+
+    // create PIs and remember them in the old nodes
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)If_ManCreatePi( pIfMan );
+
+    // load the AIG into the mapper
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_AigForEachAnd( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // add the node to the mapper
+        pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan, 
+            (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode), 
+            (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+        // set up the choice node
+        if ( Abc_AigNodeIsChoice( pNode ) )
+            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+                If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // set the primary outputs without copying the phase
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        If_ManCreatePo( pIfMan, (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+    return pIfMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description [Assuming the copy field of the mapped nodes are NULL.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int i, nDupGates;
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
+    // prepare the mapping manager
+    If_ManCleanNodeCopy( pIfMan );
+    If_ManCleanCutData( pIfMan );
+    // make the mapper point to the new network
+    If_ObjSetCopy( If_ManConst1(pIfMan), Abc_NtkCreateNodeConst1(pNtkNew) );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        If_ObjSetCopy( If_ManPi(pIfMan, i), pNode->pCopy );
+    // process the nodes in topological order
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNodeNew = Abc_NodeFromIf_rec( pNtkNew, pIfMan, If_ObjFanin0(If_ManPo(pIfMan, i)) );
+        pNodeNew = Abc_ObjNotCond( pNodeNew, If_ObjFaninC0(If_ManPo(pIfMan, i)) );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+    }
+    Extra_ProgressBarStop( pProgress );
+    // remove the constant node if not used
+    pNodeNew = (Abc_Obj_t *)If_ObjCopy( If_ManConst1(pIfMan) );
+    if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
+        Abc_NtkDeleteObj( pNodeNew );
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+//    if ( nDupGates && If_ManReadVerbose(pIfMan) )
+//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive one node after FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+{
+    Abc_Obj_t * pNodeNew;
+    If_Cut_t * pCutBest;
+    If_Obj_t * pIfLeaf;
+    int i;
+    // return if the result if known
+    pNodeNew = (Abc_Obj_t *)If_ObjCopy( pIfObj );
+    if ( pNodeNew )
+        return pNodeNew;
+    assert( pIfObj->Type == IF_AND );
+    // get the parameters of the best cut
+    // create a new node 
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    pCutBest = If_ObjCutBest( pIfObj );
+    If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
+        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
+    // derive the function of this node
+    pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pCutBest );
+    If_ObjSetCopy( pIfObj, pNodeNew );
+    return pNodeNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Ptr_t * vVisited )
+{
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    // if the cut is visited, return the result
+    if ( If_CutData(pCut) )
+        return If_CutData(pCut);
+    // compute the functions of the children
+    gFunc0 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut->pOne, vVisited );
+    gFunc1 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut->pTwo, vVisited );
+    // get the function of the cut
+    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, pCut->fCompl0), Hop_NotCond(gFunc1, pCut->fCompl1) );  
+    gFunc  = Hop_NotCond( gFunc, pCut->Phase );
+    assert( If_CutData(pCut) == NULL );
+    If_CutSetData( pCut, gFunc );
+    // add this cut to the visited list
+    Vec_PtrPush( vVisited, pCut );
+    return gFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the truth table for one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut )
+{
+    Hop_Obj_t * gFunc;
+    If_Obj_t * pLeaf;
+    int i;
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut, pIfMan->vTemp ); 
+//    printf( "%d ", Vec_PtrSize(p->vTemp) );
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetData( If_ObjCutTriv(pLeaf), NULL );
+    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
+        If_CutSetData( pCut, NULL );
+    return gFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 30ed21cf..be8b8ec5 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -53,6 +53,8 @@ static inline Abc_Obj_t *  Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) {
 
 static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs );
 
+extern int timeRetime;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -72,6 +74,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
 {
     Ivy_Man_t * pMan;
     int fCleanup = 1;
+//timeRetime = clock();
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
@@ -107,6 +110,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
         Vec_IntFree( vInit );
 //        Ivy_ManPrintStats( pMan );
     }
+//timeRetime = clock() - timeRetime;
     return pMan;
 }
 
@@ -184,17 +188,22 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
-    int i;
+//    int i;
 
     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
     if ( pMan == NULL )
         return NULL;
+//timeRetime = clock();
 
     Ivy_ManHaigStart( pMan, fVerbose );
 //    Ivy_ManRewriteSeq( pMan, 0, 0 );
-    for ( i = 0; i < nIters; i++ )
-        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
-    Ivy_ManHaigPostprocess( pMan, fVerbose );
+//    for ( i = 0; i < nIters; i++ )
+//        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    Ivy_ManRewriteSeq( pMan, 1, 0 );
+//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
+//    Ivy_ManHaigPostprocess( pMan, fVerbose );
+//timeRetime = clock() - timeRetime;
 
     // write working AIG into the current network
 //    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 ); 
@@ -246,7 +255,9 @@ Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroC
     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
+//timeRetime = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
+//timeRetime = clock() - timeRetime;
     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
@@ -270,7 +281,9 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
     if ( pMan == NULL )
         return NULL;
+//timeRetime = clock();
     Ivy_ManRewriteSeq( pMan, fUseZeroCost, fVerbose );
+//timeRetime = clock() - timeRetime;
 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
     pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1, 0 );
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index 61b1ce78..afa76cc8 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -104,7 +104,7 @@ int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->Level = 0;
 
-//Abc_NtkGetLevelNum( pNtk );
+//Abc_NtkLevel( pNtk );
  
     // start the managers
     pManScl = Abc_ManSclStart( nLutSize, nCutSizeMax, 1000 );
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index 014eafd3..dc90bee0 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -24,8 +24,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk );
-static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
+static Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Hop_Man_t * pMan );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -45,29 +45,29 @@ static Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
 Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkAig;
-    Aig_Man_t * pMan, * pTemp;
+    Hop_Man_t * pMan, * pTemp;
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
     pMan = Abc_NtkToAig( pNtk );
     if ( pMan == NULL )
         return NULL;
-    if ( !Aig_ManCheck( pMan ) )
+    if ( !Hop_ManCheck( pMan ) )
     {
         printf( "AIG check has failed.\n" );
-        Aig_ManStop( pMan );
+        Hop_ManStop( pMan );
         return NULL;
     }
     // perform balance
-    Aig_ManPrintStats( pMan );
-//    Aig_ManDumpBlif( pMan, "aig_temp.blif" );
-    pMan = Aig_ManBalance( pTemp = pMan, 1 );
-    Aig_ManStop( pTemp );
-    Aig_ManPrintStats( pMan );
+    Hop_ManPrintStats( pMan );
+//    Hop_ManDumpBlif( pMan, "aig_temp.blif" );
+    pMan = Hop_ManBalance( pTemp = pMan, 1 );
+    Hop_ManStop( pTemp );
+    Hop_ManPrintStats( pMan );
     // convert from the AIG manager
     pNtkAig = Abc_NtkFromAig( pNtk, pMan );
     if ( pNtkAig == NULL )
         return NULL;
-    Aig_ManStop( pMan );
+    Hop_ManStop( pMan );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
@@ -89,24 +89,24 @@ Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
+Hop_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
 {
-    Aig_Man_t * pMan;
+    Hop_Man_t * pMan;
     Abc_Obj_t * pObj;
     int i;
     // create the manager
-    pMan = Aig_ManStart();
+    pMan = Hop_ManStart();
     // transfer the pointers to the basic nodes
-    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Hop_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
+        pObj->pCopy = (Abc_Obj_t *)Hop_ObjCreatePi(pMan);
     // perform the conversion of the internal nodes (assumes DFS ordering)
     Abc_NtkForEachNode( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
+        pObj->pCopy = (Abc_Obj_t *)Hop_And( pMan, (Hop_Obj_t *)Abc_ObjChild0Copy(pObj), (Hop_Obj_t *)Abc_ObjChild1Copy(pObj) );
     // create the POs
     Abc_NtkForEachCo( pNtk, pObj, i )
-        Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
-    Aig_ManCleanup( pMan );
+        Hop_ObjCreatePo( pMan, (Hop_Obj_t *)Abc_ObjChild0Copy(pObj) );
+    Hop_ManCleanup( pMan );
     return pMan;
 }
 
@@ -121,26 +121,26 @@ Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Aig_Man_t * pMan )
+Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtk, Hop_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
-    Aig_Obj_t * pObj;
+    Hop_Obj_t * pObj;
     int i;
     // perform strashing
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
-    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
-    Aig_ManForEachPi( pMan, pObj, i )
+    Hop_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+    Hop_ManForEachPi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
     // rebuild the AIG
-    vNodes = Aig_ManDfs( pMan );
+    vNodes = Hop_ManDfs( pMan );
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+        pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) );
     Vec_PtrFree( vNodes );
     // connect the PO nodes
-    Aig_ManForEachPo( pMan, pObj, i )
-        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+    Hop_ManForEachPo( pMan, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Hop_ObjChild0Copy(pObj) );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" );
     return pNtkNew;
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index f99f7bce..bd035eb0 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -27,7 +27,7 @@
 static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
-static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -243,85 +243,63 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly, int fReorder, int fVerbose )
+DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
 {
     ProgressBar * pProgress;
-    Vec_Ptr_t * vFuncsGlob;
     Abc_Obj_t * pObj, * pFanin;
-    DdNode * bFunc;
+    Vec_Att_t * pAttMan;
     DdManager * dd;
+    DdNode * bFunc;
     int i, k, Counter;
 
     // remove dangling nodes
     Abc_AigCleanup( pNtk->pManFunc );
 
     // start the manager
-    assert( pNtk->pManGlob == NULL );
+    assert( Abc_NtkGlobalBdds(pNtk) == NULL );
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, dd, Extra_StopManager, NULL, Cudd_RecursiveDeref );
+    Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
+
     // set reordering
     if ( fReorder )
         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
 
-    // clean storage for local BDDs
-    Abc_NtkCleanCopy( pNtk );
-    // set the elementary variables
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        if ( Abc_ObjFanoutNum(pObj) > 0 )
-        {
-            pObj->pCopy = (Abc_Obj_t *)dd->vars[i]; 
-            Cudd_Ref( dd->vars[i] );
-        }
     // assign the constant node BDD
     pObj = Abc_AigConst1(pNtk);
     if ( Abc_ObjFanoutNum(pObj) > 0 )
     {
-        pObj->pCopy = (Abc_Obj_t *)dd->one;   
+        Abc_ObjSetGlobalBdd( pObj, dd->one );
         Cudd_Ref( dd->one );
     }
+    // set the elementary variables
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+        {
+            Abc_ObjSetGlobalBdd( pObj, dd->vars[i] );
+            Cudd_Ref( dd->vars[i] );
+        }
 
     // collect the global functions of the COs
     Counter = 0;
-    vFuncsGlob = Vec_PtrAlloc( 100 );
-    if ( fLatchOnly )
+    // construct the BDDs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
-        Abc_NtkForEachLatchInput( pNtk, pObj, i )
+        bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
+        if ( bFunc == NULL )
         {
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, pProgress, &Counter, fVerbose );
-            if ( bFunc == NULL )
-            {
-                if ( fVerbose )
-                printf( "Constructing global BDDs is aborted.\n" );
-                Vec_PtrFree( vFuncsGlob );
-                Cudd_Quit( dd );
-                return NULL;
-            }
-            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) );   Cudd_Ref( bFunc );
-            Vec_PtrPush( vFuncsGlob, bFunc );
-        }
-        Extra_ProgressBarStop( pProgress );
-    }
-    else
-    {
-        // construct the BDDs
-        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
-        Abc_NtkForEachCo( pNtk, pObj, i )
-        {
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, pProgress, &Counter, fVerbose );
-            if ( bFunc == NULL )
-            {
-                if ( fVerbose )
-                printf( "Constructing global BDDs is aborted.\n" );
-                Vec_PtrFree( vFuncsGlob );
-                Cudd_Quit( dd );
-                return NULL;
-            }
-            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
-            Vec_PtrPush( vFuncsGlob, bFunc );
+            if ( fVerbose )
+            printf( "Constructing global BDDs is aborted.\n" );
+            Abc_NtkFreeGlobalBdds( pNtk, 0 );
+            Cudd_Quit( dd );
+            return NULL;
         }
-        Extra_ProgressBarStop( pProgress );
+        bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
+        Abc_ObjSetGlobalBdd( pObj, bFunc );
     }
+    Extra_ProgressBarStop( pProgress );
+
 /*
     // derefence the intermediate BDDs
     Abc_NtkForEachNode( pNtk, pObj, i )
@@ -336,9 +314,9 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
         if ( pObj->pCopy != NULL )
-            printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id );
+            printf( "Abc_NtkBuildGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id );
         if ( pObj->vFanouts.nSize > 0 )
-            printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pObj->Id );
+            printf( "Abc_NtkBuildGlobalBdds() error: Node %d has refs assigned\n", pObj->Id );
     }
 */
     // reset references
@@ -353,8 +331,6 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
         Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
         Cudd_AutodynDisable( dd );
     }
-    pNtk->pManGlob = dd;
-    pNtk->vFuncsGlob = vFuncsGlob;
 //    Cudd_PrintInfo( dd, stdout );
     return dd;
 }
@@ -370,9 +346,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose )
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
 {
     DdNode * bFunc, * bFunc0, * bFunc1, * bFuncC;
+    int fDetectMuxes = 1;
     assert( !Abc_ObjIsComplement(pNode) );
     if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
     {
@@ -383,14 +360,14 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
         return NULL;
     }
     // if the result is available return
-    if ( pNode->pCopy == NULL )
+    if ( Abc_ObjGlobalBdd(pNode) == NULL )
     {
         Abc_Obj_t * pNodeC, * pNode0, * pNode1;
         pNode0 = Abc_ObjFanin0(pNode);
         pNode1 = Abc_ObjFanin1(pNode);
         // check for the special case when it is MUX/EXOR
-//        if ( 0 )
-        if ( pNode0->pCopy == NULL && pNode1->pCopy == NULL &&
+        if ( fDetectMuxes && 
+             Abc_ObjGlobalBdd(pNode0) == NULL && Abc_ObjGlobalBdd(pNode1) == NULL &&
              Abc_ObjIsNode(pNode0) && Abc_ObjFanoutNum(pNode0) == 1 && 
              Abc_ObjIsNode(pNode1) && Abc_ObjFanoutNum(pNode1) == 1 && 
              Abc_NodeIsMuxType(pNode) )
@@ -405,15 +382,15 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
             pNodeC->vFanouts.nSize--;
 
             // compute the result for all branches
-            bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            bFuncC = Abc_NodeGlobalBdds_rec( dd, pNodeC, nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
             if ( bFuncC == NULL )
                 return NULL;
             Cudd_Ref( bFuncC );
-            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
             if ( bFunc0 == NULL )
                 return NULL;
             Cudd_Ref( bFunc0 );
-            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjRegular(pNode1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
             if ( bFunc1 == NULL )
                 return NULL;
             Cudd_Ref( bFunc1 );
@@ -432,11 +409,11 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
         else
         {
             // compute the result for both branches
-            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
             if ( bFunc0 == NULL )
                 return NULL;
             Cudd_Ref( bFunc0 );
-            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); 
+            bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
             if ( bFunc1 == NULL )
                 return NULL;
             Cudd_Ref( bFunc1 );
@@ -450,26 +427,26 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
             (*pCounter)++;
         }
         // set the result
-        assert( pNode->pCopy == NULL );
-        pNode->pCopy = (Abc_Obj_t *)bFunc;
+        assert( Abc_ObjGlobalBdd(pNode) == NULL );
+        Abc_ObjSetGlobalBdd( pNode, bFunc );
         // increment the progress bar
         if ( pProgress )
             Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
     }
     // prepare the return value
-    bFunc = (DdNode *)pNode->pCopy;
+    bFunc = Abc_ObjGlobalBdd(pNode);
     // dereference BDD at the node
-    if ( --pNode->vFanouts.nSize == 0 )
+    if ( --pNode->vFanouts.nSize == 0 && fDropInternal )
     {
         Cudd_Deref( bFunc );
-        pNode->pCopy = NULL;
+        Abc_ObjSetGlobalBdd( pNode, NULL );
     }
     return bFunc;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Dereferences global BDDs of the network.]
+  Synopsis    [Frees the global BDDs of the network.]
 
   Description []
                
@@ -478,16 +455,9 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
-{
-    DdNode * bFunc;
-    int i;
-    assert( pNtk->pManGlob );
-    assert( pNtk->vFuncsGlob );
-    Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i )
-        Cudd_RecursiveDeref( pNtk->pManGlob, bFunc );
-    Vec_PtrFree( pNtk->vFuncsGlob );
-    pNtk->vFuncsGlob = NULL;
+DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan ) 
+{ 
+    return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan ); 
 }
 
 /**Function*************************************************************
@@ -503,6 +473,7 @@ void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
 {
+    /*
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pNodeR;
     DdManager * dd;
@@ -521,7 +492,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
     // build the BDD of the cone
-    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, NULL, NULL, 1 );  Cudd_Ref( bFunc );
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, 1, NULL, NULL, 1 );  Cudd_Ref( bFunc );
     bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
     // count minterms
     Result = Cudd_CountMinterm( dd, bFunc, dd->size );
@@ -533,6 +504,8 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
     Cudd_Quit( dd );
     Vec_PtrFree( vNodes );
     return Result;
+    */
+    return 0.0;
 }
 
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index bdca4a8e..40bf30a6 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -113,9 +113,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     }
 
     if ( Abc_NtkIsStrash(pNtk) )
-        fprintf( pFile, "  lev = %3d", Abc_AigGetLevelNum(pNtk) );
+        fprintf( pFile, "  lev = %3d", Abc_AigLevel(pNtk) );
     else if ( !Abc_NtkIsSeq(pNtk) )
-        fprintf( pFile, "  lev = %3d", Abc_NtkGetLevelNum(pNtk) );
+        fprintf( pFile, "  lev = %3d", Abc_NtkLevel(pNtk) );
 
     fprintf( pFile, "\n" );
     // print the statistic into a file
@@ -126,7 +126,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pTable, "%s ",  pNtk->pName );
         fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
-        fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_AigLevel(pNtk) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
@@ -150,7 +150,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         FILE * pTable;
         pTable = fopen( "fpga/fpga_stats.txt", "a+" );
         fprintf( pTable, "%s ",  pNtk->pName );
-        fprintf( pTable, "%d ", Abc_NtkGetLevelNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
         fprintf( pTable, "%.2f ", (float)(s_MappingMem)/(float)(1<<20) );
         fprintf( pTable, "%.2f", (float)(s_MappingTime)/(float)(CLOCKS_PER_SEC) );
@@ -159,23 +159,41 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     }
 */
 
-/*
+
     // print the statistic into a file
     {
         static int Counter = 0;
         extern int timeRetime;
         FILE * pTable;
         Counter++;
-        pTable = fopen( "sap/stats_retime.txt", "a+" );
+        pTable = fopen( "a/ret__stats.txt", "a+" );
         fprintf( pTable, "%s ", pNtk->pName );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
         fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
-        fprintf( pTable, "%d ", Abc_NtkGetLevelNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkLevel(pNtk) );
         fprintf( pTable, "%.2f ", (float)(timeRetime)/(float)(CLOCKS_PER_SEC) );
         if ( Counter % 4 == 0 )
             fprintf( pTable, "\n" );
         fclose( pTable );
     }
+
+/*
+    // print the statistic into a file
+    {
+        static int Counter = 0;
+        extern int timeRetime;
+        FILE * pTable;
+        Counter++;
+        pTable = fopen( "d/stats.txt", "a+" );
+        fprintf( pTable, "%s ", pNtk->pName );
+//        fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
+//        fprintf( pTable, "%d ", Abc_NtkPoNum(pNtk) );
+//        fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
+        fprintf( pTable, "%.2f ", (float)(timeRetime)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+    }
 */
 
 /*
@@ -214,7 +232,8 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
 
     fprintf( pFile, "Latches (%d):  ", Abc_NtkLatchNum(pNtk) );  
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        fprintf( pFile, " %s", Abc_ObjName(pObj) );
+        fprintf( pFile, " %s(%s=%s)", Abc_ObjName(pObj), 
+            Abc_ObjName(Abc_ObjFanout0(pObj)), Abc_ObjName(Abc_ObjFanin0(pObj)) );
     fprintf( pFile, "\n" );   
 }
 
@@ -500,7 +519,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
     if ( fListNodes )
     {
         int nLevels;
-        nLevels = Abc_NtkGetLevelNum(pNtk);
+        nLevels = Abc_NtkLevel(pNtk);
         printf( "Nodes by level:\n" );
         for ( i = 0; i <= nLevels; i++ )
         {
@@ -553,7 +572,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListN
         int nOutsSum, nOutsTotal;
 
         if ( !Abc_NtkIsStrash(pNtk) )
-            Abc_NtkGetLevelNum(pNtk);
+            Abc_NtkLevel(pNtk);
 
         LevelMax = 0;
         Abc_NtkForEachCo( pNtk, pNode, i )
@@ -840,41 +859,6 @@ void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Prints information about the clock skew schedule.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ) {
-
-  Abc_Obj_t * pObj;
-  int         i;
-  int         nNonZero = 0;
-  float       skew, sum = 0.0, avg;
-
-  if (fPrintAll) fprintf( pFile, "Full Clock Skew Schedule:\n\tGlobal Skew = %.2f\n", pNtk->globalSkew );
-
-  Abc_NtkForEachLatch( pNtk, pObj, i ) {
-    skew = Abc_NtkGetLatSkew( pNtk, i );
-    if ( skew != 0.0 ) {
-      nNonZero++;
-      sum += ABS( skew );
-    }
-    if (fPrintAll) fprintf( pFile, "\tLatch %d (Id = %d) \t Endpoint Skew = %.2f\n", i, pObj->Id, skew);
-  }
-
-  avg = sum / Abc_NtkLatchNum( pNtk );
- 
-  fprintf( pFile, "Endpoint Skews : Total |Skew| = %.2f\t Avg |Skew| = %.2f\t Non-Zero Skews = %d\n", 
-           sum, avg, nNonZero );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Prints information about the object.]
 
   Description []
@@ -942,6 +926,12 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
     Abc_ObjForEachFanin( pObj, pFanin, i )
         fprintf( pFile, "%d ", pFanin->Id );
     fprintf( pFile, ") " );
+/*
+    fprintf( pFile, " Fanouts ( " );
+    Abc_ObjForEachFanout( pObj, pFanin, i )
+        fprintf( pFile, "%d(%c) ", pFanin->Id, Abc_NodeIsTravIdCurrent(pFanin)? '+' : '-' );
+    fprintf( pFile, ") " );
+*/
     // print the logic function
     if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) )
         fprintf( pFile, " %s", pObj->pData );
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index c9e5bfd7..fcd44d30 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -310,7 +310,7 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
     if ( !fVerbose )
         return;
     printf( "Nodes = %7d.  Levels = %4d.  ", Abc_NtkNodeNum(pNtk), 
-        Abc_NtkIsStrash(pNtk)? Abc_AigGetLevelNum(pNtk) : Abc_NtkGetLevelNum(pNtk) );
+        Abc_NtkIsStrash(pNtk)? Abc_AigLevel(pNtk) : Abc_NtkLevel(pNtk) );
     PRT( pString, clock() - clk );
 }
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 3d301cd6..0328d8d3 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -156,7 +156,7 @@ pManRef->timeTotal = clock() - clkStart;
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
     else
-        Abc_NtkGetLevelNum( pNtk );
+        Abc_NtkLevel( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 9dc84999..2d4f50fb 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -183,7 +183,7 @@ pManRst->timeTotal = clock() - clkStart;
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
     else
-        Abc_NtkGetLevelNum( pNtk );
+        Abc_NtkLevel( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 9fcc6979..19e6c50a 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -232,7 +232,7 @@ pManRes->timeTotal = clock() - clkStart;
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
     else
-        Abc_NtkGetLevelNum( pNtk );
+        Abc_NtkLevel( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 2af10271..151b5256 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -158,7 +158,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     if ( fUpdateLevel )
         Abc_NtkStopReverseLevels( pNtk );
     else
-        Abc_NtkGetLevelNum( pNtk );
+        Abc_NtkLevel( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 63beac6c..b9fab415 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -104,7 +104,7 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     p->nFaninLevels  = nFaninLevels;
     p->nFanoutLevels = nFanoutLevels;
     p->nNodesOld     = Abc_NtkNodeNum(pNtk);
-    p->nLevelsOld    = Abc_AigGetLevelNum(pNtk);
+    p->nLevelsOld    = Abc_AigLevel(pNtk);
     // remember latch values
 //    Abc_NtkForEachLatch( pNtk, pNode, i )
 //        pNode->pNext = pNode->pData;
@@ -220,7 +220,7 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
 //        pNode->pData = pNode->pNext, pNode->pNext = NULL;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
-    Abc_NtkGetLevelNum( pNtk );
+    Abc_NtkLevel( pNtk );
     // check
     if ( !Abc_NtkCheck( pNtk ) )
     {
@@ -298,7 +298,7 @@ void Abc_RRManPrintStats( Abc_RRMan_t * p )
     printf( "Edges tried     = %6d.\n", p->nEdgesTried );
     printf( "Edges removed   = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried );
     printf( "Node gain       = %6d. (%5.2f %%)\n", p->nNodesOld  - Abc_NtkNodeNum(p->pNtk), Ratio );
-    printf( "Level gain      = %6d.\n", p->nLevelsOld - Abc_AigGetLevelNum(p->pNtk) );
+    printf( "Level gain      = %6d.\n", p->nLevelsOld - Abc_AigLevel(p->pNtk) );
     PRT( "Windowing      ", p->timeWindow );
     PRT( "Miter          ", p->timeMiter );
     PRT( "    Construct  ", p->timeMiter - p->timeProve );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 8d5dd2a7..55498288 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -458,7 +458,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     int i, k, fUseMuxes = 1;
     int clk1 = clock(), clk;
     int fOrderCiVarsFirst = 0;
-    int nLevelsMax = Abc_AigGetLevelNum(pNtk);
+    int nLevelsMax = Abc_AigLevel(pNtk);
     int RetValue = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index e8dc9793..a3719b10 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [aigStrash.c]
+  FileName    [abcStrash.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: aigStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -46,10 +46,12 @@ static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fA
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
 {
+    extern int timeRetime;
     Abc_Ntk_t * pNtkAig;
     Abc_Obj_t * pObj;
-    int i, nNodes;
+    int i, nNodes, RetValue;
     assert( Abc_NtkIsStrash(pNtk) );
+//timeRetime = clock();
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" );
@@ -58,7 +60,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
     // restrash the nodes (assuming a topological order of the old network)
     Abc_NtkForEachNode( pNtk, pObj, i )
         pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
-    // finalize the network
+    //l finalize the network
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
 //    if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
@@ -76,6 +78,9 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
         Abc_NtkDelete( pNtkAig );
         return NULL;
     }
+//timeRetime = clock() - timeRetime;
+    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
+        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
     return pNtkAig;
 
 }
@@ -106,7 +111,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
         return NULL;
     }
     // perform strashing
-    Abc_NtkCleanCopy( pNtk );
+//    Abc_NtkCleanCopy( pNtk );
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes );
     Abc_NtkFinalize( pNtk, pNtkAig );
@@ -205,13 +210,17 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
 ***********************************************************************/
 void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, bool fAllNodes )
 {
+    extern Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
     ProgressBar * pProgress;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNodeOld;
-    int i;
+    int i, clk = clock();
     assert( Abc_NtkIsLogic(pNtkOld) );
     assert( Abc_NtkIsStrash(pNtkNew) );
-    vNodes = Abc_NtkDfs( pNtkOld, fAllNodes );
+//    vNodes = Abc_NtkDfs( pNtkOld, fAllNodes );
+    vNodes = Abc_NtkDfsIter( pNtkOld, fAllNodes );
+//printf( "Nodes = %d. ", Vec_PtrSize(vNodes) );
+//PRT( "Time", clock() - clk );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNodeOld, i )
     {
@@ -233,16 +242,16 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, bool fAllNo
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeStrash_rec( Abc_Aig_t * pMan, Aig_Obj_t * pObj )
+void Abc_NodeStrash_rec( Abc_Aig_t * pMan, Hop_Obj_t * pObj )
 {
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
         return;
-    Abc_NodeStrash_rec( pMan, Aig_ObjFanin0(pObj) ); 
-    Abc_NodeStrash_rec( pMan, Aig_ObjFanin1(pObj) );
-    pObj->pData = Abc_AigAnd( pMan, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
+    Abc_NodeStrash_rec( pMan, Hop_ObjFanin0(pObj) ); 
+    Abc_NodeStrash_rec( pMan, Hop_ObjFanin1(pObj) );
+    pObj->pData = Abc_AigAnd( pMan, (Abc_Obj_t *)Hop_ObjChild0Copy(pObj), (Abc_Obj_t *)Hop_ObjChild1Copy(pObj) );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
 }
 
 /**Function*************************************************************
@@ -258,8 +267,8 @@ void Abc_NodeStrash_rec( Abc_Aig_t * pMan, Aig_Obj_t * pObj )
 ***********************************************************************/
 Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
 {
-    Aig_Man_t * pMan;
-    Aig_Obj_t * pRoot;
+    Hop_Man_t * pMan;
+    Hop_Obj_t * pRoot;
     Abc_Obj_t * pFanin;
     int i;
     assert( Abc_ObjIsNode(pNodeOld) );
@@ -269,15 +278,15 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
     pRoot = pNodeOld->pData;
     // check the constant case
     if ( Abc_NodeIsConst(pNodeOld) )
-        return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Aig_IsComplement(pRoot) );
+        return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Hop_IsComplement(pRoot) );
     // set elementary variables
     Abc_ObjForEachFanin( pNodeOld, pFanin, i )
-        Aig_IthVar(pMan, i)->pData = pFanin->pCopy;
+        Hop_IthVar(pMan, i)->pData = pFanin->pCopy;
     // strash the AIG of this node
-    Abc_NodeStrash_rec( pNtkNew->pManFunc, Aig_Regular(pRoot) );
-    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
+    Abc_NodeStrash_rec( pNtkNew->pManFunc, Hop_Regular(pRoot) );
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
     // return the final node
-    return Abc_ObjNotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
+    return Abc_ObjNotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
 }
 
 
@@ -328,7 +337,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCoNum(pNtk) == 1 );
     // get the cutoff level
-    LevelCut = ABC_MAX( 0, Abc_AigGetLevelNum(pNtk) - nLevels );
+    LevelCut = ABC_MAX( 0, Abc_AigLevel(pNtk) - nLevels );
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index db926d17..1b63b23c 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -79,7 +79,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
     if ( fUseTrick )
     {
         extern void * Abc_FrameReadLibGen(); 
-        Aig_ManStop( pNtk->pManFunc );
+        Hop_ManStop( pNtk->pManFunc );
         pNtk->pManFunc = Abc_FrameReadLibGen();
         pNtk->ntkFunc = ABC_FUNC_MAP;
         Abc_NtkForEachNode( pNtk, pObj, i )
@@ -269,7 +269,7 @@ void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv,
     if ( stmm_count(tEquiv) == 0 )
         return;
     // assign levels to the nodes of the network
-    Abc_NtkGetLevelNum( pNtk );
+    Abc_NtkLevel( pNtk );
     // merge nodes in the classes
     if ( Abc_NtkHasMapping( pNtk ) )
     {
@@ -897,7 +897,7 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose )
+int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fVerbose )
 {
     Vec_Ptr_t * vNodes;
     int Counter;
@@ -910,20 +910,26 @@ int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose )
     if ( fVerbose )
         printf( "Cleanup removed %4d dangling objects.\n", Counter );
     // check if some of the latches can be removed
-    Counter = Abc_NtkLatchSweep( pNtk );
-    if ( fVerbose )
-        printf( "Cleanup removed %4d redundant latches.\n", Counter );
+    if ( fLatchSweep )
+    {
+        Counter = Abc_NtkLatchSweep( pNtk );
+        if ( fVerbose )
+            printf( "Cleanup removed %4d redundant latches.\n", Counter );
+    }
     // detect the autonomous components
-    vNodes = Abc_NtkDfsSeqReverse( pNtk );
-    Vec_PtrFree( vNodes );
-    // replace them by PIs
-    Counter = Abc_NtkReplaceAutonomousLogic( pNtk );
-    if ( fVerbose )
-        printf( "Cleanup added   %4d additional PIs.\n", Counter );
-    // remove the non-marked nodes
-    Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
-    if ( fVerbose )
-        printf( "Cleanup removed %4d autonomous objects.\n", Counter );
+    if ( fAutoSweep )
+    {
+        vNodes = Abc_NtkDfsSeqReverse( pNtk );
+        Vec_PtrFree( vNodes );
+        // replace them by PIs
+        Counter = Abc_NtkReplaceAutonomousLogic( pNtk );
+        if ( fVerbose )
+            printf( "Cleanup added   %4d additional PIs.\n", Counter );
+        // remove the non-marked nodes
+        Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
+        if ( fVerbose )
+            printf( "Cleanup removed %4d autonomous objects.\n", Counter );
+    }
     // check
     if ( !Abc_NtkCheck( pNtk ) )
         printf( "Abc_NtkCleanupSeq: The network check has failed.\n" );
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index fad3bd92..d3fcb7c9 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0, 1, fVerbose );
+    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
     Cudd_AutodynDisable( dd );
     Cudd_zddVarsFromBddVars( dd, 2 );
 clkBdd = clock() - clk;
@@ -97,9 +97,10 @@ clk = clock();
     Ntk_NetworkSymmsBdd( dd, pNtk, fNaive, fVerbose );
 clkSym = clock() - clk;
     // undo the global functions
-    Abc_NtkFreeGlobalBdds( pNtk );
-    Extra_StopManager( dd );
-    pNtk->pManGlob = NULL;
+//    Abc_NtkFreeGlobalBdds( pNtk );
+//    Extra_StopManager( dd );
+//    pNtk->pManGlob = NULL;
+    Abc_NtkFreeGlobalBdds( pNtk, 1 );
 
 PRT( "Constructing BDDs", clkBdd );
 PRT( "Computing symms  ", clkSym );
@@ -129,7 +130,8 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer
     // compute symmetry info for each PO
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        bFunc = pNtk->vFuncsGlob->pArray[i];
+//      bFunc = pNtk->vFuncsGlob->pArray[i];
+        bFunc = Abc_ObjGlobalBdd( pNode );
         nSupps += Cudd_SupportSize( dd, bFunc );
         if ( Cudd_IsConstant(bFunc) )
             continue;
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index af06436f..93fa3fa5 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -648,8 +648,8 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
     int i, k, nLevelsCur;
 //    assert( Abc_NtkIsStrash(pNtk) );
     // remember the maximum number of direct levels
-//    pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
-    pNtk->LevelMax = Abc_NtkGetLevelNum(pNtk);
+//    pNtk->LevelMax = Abc_AigLevel(pNtk);
+    pNtk->LevelMax = Abc_NtkLevel(pNtk);
     // start the reverse levels
     pNtk->vLevelsR = Vec_IntAlloc( 0 );
     Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 48b7eb92..8fd2a12f 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -66,20 +66,22 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
     Abc_Obj_t * pNode;
     Extra_UnateInfo_t * p;
     DdManager * dd;         // the BDD manager used to hold shared BDDs
-    DdNode ** pbGlobal;     // temporary storage for global BDDs
+//    DdNode ** pbGlobal;     // temporary storage for global BDDs
     int TotalSupps = 0;
     int TotalUnate = 0;
     int i, clk = clock();
     int clkBdd, clkUnate;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL )
+    dd = Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose);
+    if ( dd == NULL )
         return;
 clkBdd = clock() - clk;
 
     // get information about the network
-    dd       = pNtk->pManGlob;
-    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
+//    dd       = pNtk->pManGlob;
+//    dd       = Abc_NtkGlobalBddMan( pNtk );
+//    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
 
     // print the size of the BDDs
     printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
@@ -89,7 +91,8 @@ clkBdd = clock() - clk;
     {
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
-            p = Extra_UnateComputeSlow( dd, pbGlobal[i] );
+//            p = Extra_UnateComputeSlow( dd, pbGlobal[i] );
+            p = Extra_UnateComputeSlow( dd, Abc_ObjGlobalBdd(pNode) );
             if ( fVerbose )
                 Extra_UnateInfoPrint( p );
             TotalSupps += p->nVars;
@@ -104,7 +107,8 @@ clkBdd = clock() - clk;
         Cudd_zddVarsFromBddVars( dd, 2 );
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
-            p = Extra_UnateComputeFast( dd, pbGlobal[i] );
+//            p = Extra_UnateComputeFast( dd, pbGlobal[i] );
+            p = Extra_UnateComputeFast( dd, Abc_ObjGlobalBdd(pNode) );
             if ( fVerbose )
                 Extra_UnateInfoPrint( p );
             TotalSupps += p->nVars;
@@ -122,10 +126,11 @@ clkUnate = clock() - clk - clkBdd;
     PRT( "Total    ", clock() - clk );
 
     // deref the PO functions
-    Abc_NtkFreeGlobalBdds( pNtk );
+//    Abc_NtkFreeGlobalBdds( pNtk );
     // stop the global BDD manager
-    Extra_StopManager( pNtk->pManGlob );
-    pNtk->pManGlob = NULL;
+//    Extra_StopManager( pNtk->pManGlob );
+//    pNtk->pManGlob = NULL;
+    Abc_NtkFreeGlobalBdds( pNtk, 1 );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index e4873986..acd63771 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     }
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
+    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
@@ -92,7 +92,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
     Cudd_RecursiveDeref( dd, bUnreach );
     Extra_StopManager( dd );
-    pNtk->pManGlob = NULL;
+//    pNtk->pManGlob = NULL;
 
     // make sure that everything is okay
     if ( pNtk->pExdc && !Abc_NtkCheck( pNtk->pExdc ) )
@@ -137,13 +137,15 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
     Abc_NtkForEachLatch( pNtk, pNode, i )
     {
         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
-        bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] );  Cudd_Ref( bProd );
+//        bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] );  Cudd_Ref( bProd );
+        bProd = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( bProd );
         bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );                 Cudd_Ref( bRel );
         Cudd_RecursiveDeref( dd, bTemp ); 
         Cudd_RecursiveDeref( dd, bProd ); 
     }
     // free the global BDDs
-    Abc_NtkFreeGlobalBdds( pNtk );
+//    Abc_NtkFreeGlobalBdds( pNtk );
+    Abc_NtkFreeGlobalBdds( pNtk, 0 );
 
     // quantify the PI variables
     bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) );    Cudd_Ref( bInputs );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 7db26629..04ed07a7 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -15,6 +15,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
+    src/base/abci/abcIf.c \
         src/base/abci/abcIvy.c \
     src/base/abci/abcLut.c \
     src/base/abci/abcMap.c \
@@ -22,7 +23,6 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
     src/base/abci/abcOrder.c \
-    src/base/abci/abcPga.c \
     src/base/abci/abcPrint.c \
     src/base/abci/abcProve.c \
     src/base/abci/abcReconv.c \