Version abc70110

15 files changed, 648 insertions, 527 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 278812ef..65f1a75f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -67,6 +67,7 @@ static int Abc_CommandResubstitute   ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandRr             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandComb           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMiter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDemiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOrPos          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -88,9 +89,7 @@ static int Abc_CommandExdcSet        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDouble         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -112,6 +111,7 @@ static int Abc_CommandFraigStore     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandFraigRestore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigClean     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigDress     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnmap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -133,6 +133,8 @@ static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -194,11 +196,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "restructure",   Abc_CommandRestructure,      1 );
+//    Cmd_CommandAdd( pAbc, "Synthesis",    "restructure",   Abc_CommandRestructure,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "resub",         Abc_CommandResubstitute,     1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "rr",            Abc_CommandRr,               1 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "comb",          Abc_CommandComb,             1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
@@ -220,9 +223,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
-    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
-    Cmd_CommandAdd( pAbc, "Various",      "xsim",          Abc_CommandXsim,             0 );
-    Cmd_CommandAdd( pAbc, "Various",      "cycle",         Abc_CommandCycle,            1 );
+//    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
@@ -244,6 +245,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_restore", Abc_CommandFraigRestore,     1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Abc_CommandFraigClean,       0 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "dress",         Abc_CommandFraigDress,       1 );
 
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
@@ -265,6 +267,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
@@ -860,6 +864,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    int fStruct;
     int fVerbose;
     extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
     extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
@@ -869,12 +874,16 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fStruct = 1;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 's':
+            fStruct ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -892,12 +901,15 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // print support information
-    Abc_NtkPrintStrSupports( pNtk );
-    return 0;
+    if ( fStruct )
+    {
+        Abc_NtkPrintStrSupports( pNtk );
+        return 0;
+    }
 
     if ( !Abc_NtkIsComb(pNtk) )
     {
-        fprintf( pErr, "This command works only for combinational networks.\n" );
+        fprintf( pErr, "This command works only for combinational networks (run \"comb\").\n" );
         return 1;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
@@ -911,8 +923,9 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_supp [-vh]\n" );
+    fprintf( pErr, "usage: print_supp [-svh]\n" );
     fprintf( pErr, "\t        prints the supports of the CO nodes\n" );
+    fprintf( pErr, "\t-s    : toggle printing structural support only [default = %s].\n", fStruct? "yes": "no" );  
     fprintf( pErr, "\t-v    : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -979,7 +992,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsComb(pNtk) )
     {
-        fprintf( pErr, "This command works only for combinational networks.\n" );
+        fprintf( pErr, "This command works only for combinational networks (run \"comb\").\n" );
         return 1;
     }
     if ( Abc_NtkIsStrash(pNtk) )
@@ -1354,18 +1367,12 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Printing logic sharing does not work for sequential AIGs.\n" );
-        return 1;
-    }
-
     Abc_NtkPrintSharing( pNtk );
     return 0;
 
 usage:
     fprintf( pErr, "usage: print_sharing [-h]\n" );
-    fprintf( pErr, "\t        prints the number of shared nodes in the TFO cones of the COs\n" );
+    fprintf( pErr, "\t        prints the number of shared nodes in the TFI cones of the COs\n" );
 //    fprintf( pErr, "\t-l    : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -1859,12 +1866,6 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Balancing cannot be applied to a sequential AIG.\n" );
-        return 1;
-    }
-
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
     {
@@ -1932,7 +1933,7 @@ int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv )
     nThresh   =  1;
     nFaninMax = 20;
     fCnf      =  0;
-    fMulti    =  0;
+    fMulti    =  1;
     fSimple   =  0;
     fFactor   =  0;
     Extra_UtilGetoptReset();
@@ -2532,9 +2533,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     bool fPrecompute;
     bool fUseZeros;
     bool fVerbose;
+    bool fVeryVerbose;
     // external functions
     extern void Rwr_Precompute();
-    extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -2545,8 +2546,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     fPrecompute  = 0;
     fUseZeros    = 0;
     fVerbose     = 0;
+    fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2562,6 +2564,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2592,7 +2597,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose ) )
+    if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose ) )
     {
         fprintf( pErr, "Rewriting has failed.\n" );
         return 1;
@@ -2600,11 +2605,12 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: rewrite [-lzvh]\n" );
+    fprintf( pErr, "usage: rewrite [-lzvwh]\n" );
     fprintf( pErr, "\t         performs technology-independent rewriting of the AIG\n" );
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 } 
@@ -3127,6 +3133,65 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The network is already combinational.\n" );
+        return 0;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkDup( pNtk );
+    Abc_NtkMakeComb( pNtkRes );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: comb [-h]\n" );
+    fprintf( pErr, "\t        makes the current network combinational by replacing latches by PI/PO pairs\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -3349,7 +3414,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    FILE * pOut, * pErr, * pFile;
+    FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk2;
     char * FileName;
     int fComb;
@@ -3386,25 +3451,11 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    // get the input file name
-    FileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( FileName, "r" )) == NULL )
-    {
-        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
-            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
-        fprintf( pAbc->Err, "\n" );
-        return 1;
-    }
-    fclose( pFile );
- 
     // read the second network
-    pNtk2 = Io_Read( FileName, 1 );
+    FileName = argv[globalUtilOptind];
+    pNtk2 = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
     if ( pNtk2 == NULL )
-    {
-        fprintf( pAbc->Err, "Reading network from file has failed.\n" );
         return 1;
-    }
 
     // check if the second network is combinational
     if ( Abc_NtkLatchNum(pNtk2) )
@@ -4430,7 +4481,7 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
     fclose( pFile );
 
     // set the new network
-    pNtkNew = Io_Read( FileName, 1 );
+    pNtkNew = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
     if ( pNtkNew == NULL )
     {
         fprintf( pAbc->Err, "Reading network from file has failed.\n" );
@@ -4697,11 +4748,13 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
+/*
     if ( !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Sequential cuts can be computed for sequential AIGs (run \"seq\").\n" );
         return 1;
     }
+*/
     if ( pParams->nVarsMax < CUT_SIZE_MIN || pParams->nVarsMax > CUT_SIZE_MAX )
     {
         fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", CUT_SIZE_MIN, CUT_SIZE_MAX );
@@ -5025,168 +5078,6 @@ usage:
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int nFrames;
-    int fInputs;
-    int fVerbose;
-    extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    nFrames    = 10;
-    fInputs    =  0;
-    fVerbose   =  0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFrames = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFrames < 0 ) 
-                goto usage;
-            break;
-        case 'i':
-            fInputs ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( pErr, "Only works for strashed networks.\n" );
-        return 1;
-    }
-
-    Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
-    fprintf( pErr, "\t         performs X-valued simulation of the AIG\n" );
-    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-i     : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
-    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int nFrames;
-    int fVerbose;
-    extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
-    extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    nFrames    = 100;
-    fVerbose   =   0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFrames = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFrames < 0 ) 
-                goto usage;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSopLogic(pNtk) )
-    {
-        fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
-        return 1;
-    }
-
-    if ( Abc_NtkIsStrash(pNtk) )
-        Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
-    else
-        Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
-    fprintf( pErr, "\t         cycles sequiential circuit for the given number of timeframes\n" );
-    fprintf( pErr, "\t         to derive a new initial state (which may be on the envelope)\n" );
-    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
 
 /**Function*************************************************************
 
@@ -5433,11 +5324,6 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
@@ -5513,11 +5399,6 @@ int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
     Abc_NtkIvyCuts( pNtk, nInputs );
     return 0;
@@ -5581,11 +5462,6 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
     pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
@@ -5658,11 +5534,6 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
     pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
@@ -5731,11 +5602,6 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
     pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose );
     if ( pNtkRes == NULL )
@@ -5817,11 +5683,6 @@ int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
     pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose );
     if ( pNtkRes == NULL )
@@ -5861,7 +5722,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, fProve, fVerbose, fDoSparse;
     int nConfLimit;
 
-    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5908,13 +5769,8 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
-    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, fVerbose );
+    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5985,12 +5841,6 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
-
 
     clk = clock();
 
@@ -6091,11 +5941,6 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
 
     pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
     if ( pNtkRes == NULL )
@@ -6156,11 +6001,6 @@ int Abc_CommandMini( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" );
@@ -6247,11 +6087,6 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Only works for non-sequential networks.\n" );
-        return 1;
-    }
     if ( Abc_NtkIsStrash(pNtk) )
         Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
     else
@@ -6754,6 +6589,78 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandFraigDress( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    char * pFileName;
+    int c;
+    int fVerbose;
+    extern void Abc_NtkDress( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for logic networks.\n" );
+        return 1;
+    }
+    if ( argc != globalUtilOptind && argc != globalUtilOptind + 1 )
+        goto usage;
+    if ( argc == globalUtilOptind && Abc_NtkSpec(pNtk) == NULL )
+    {
+        fprintf( pErr, "The current network has no spec.\n" );
+        return 1;
+    }
+    // get the input file name
+    pFileName = (argc == globalUtilOptind + 1) ? argv[globalUtilOptind] : Abc_NtkSpec(pNtk);
+    // modify the current network
+    Abc_NtkDress( pNtk, pFileName, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dress [-vh] <file>\n" );
+    fprintf( pErr, "\t         transfers internal node names from file to the current network\n" );
+    fprintf( pErr, "\t<file> : network with names (if not given, the current network spec is used)\n" );  
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -6831,12 +6738,6 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Cannot map a sequential AIG.\n" );
-        return 1;
-    }
-
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0 );
@@ -7281,12 +7182,6 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
-        return 1;
-    }
-
     // create the new LUT library
     if ( nLutSize >= 3 && nLutSize <= 10 )
         Fpga_SetSimpleLutLib( nLutSize );
@@ -7438,12 +7333,6 @@ int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
-        return 1;
-    }
-
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
@@ -7791,12 +7680,6 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
-        return 1;
-    }
-
     if ( Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "The current network is combinational.\n" );
@@ -7895,12 +7778,6 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
-        return 1;
-    }
-
     if ( Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "The current network is combinational.\n" );
@@ -7959,12 +7836,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "The current network is already a sequential AIG.\n" );
-        return 1;
-    }
-
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         fprintf( pErr, "The network has no latches.\n" );
@@ -8040,13 +7911,13 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-
+/*
     if ( !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Conversion to combinational AIG works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
-
+*/
     // share the latches on the fanout edges
 //    if ( fShare )
 //        Seq_NtkShareFanouts(pNtk);
@@ -8540,12 +8411,6 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( pErr, "Sequential sweep works only for combinational networks (run \"unseq\").\n" );
-        return 1;
-    }
-
     if ( Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
@@ -8660,6 +8525,169 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int fVerbose;
+    extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+    extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames    = 100;
+    fVerbose   =   0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSopLogic(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
+    else
+        Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
+    fprintf( pErr, "\t         cycles sequiential circuit for the given number of timeframes\n" );
+    fprintf( pErr, "\t         to derive a new initial state (which may be on the envelope)\n" );
+    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int fInputs;
+    int fVerbose;
+    extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames    = 10;
+    fInputs    =  0;
+    fVerbose   =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            fInputs ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+
+    Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
+    fprintf( pErr, "\t         performs X-valued simulation of the AIG\n" );
+    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-i     : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
@@ -9002,11 +9030,6 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     } 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
-        return 0;
-    }
 
     clk = clock();
     if ( Abc_NtkIsStrash(pNtk) )
@@ -9183,12 +9206,6 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter with one output.\n" );
         return 0;
     } 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
-        return 0;
-    }
-
     clk = clock();
 
     if ( Abc_NtkIsStrash(pNtk) )
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index bf40e45b..d5d2aa16 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -142,7 +142,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
         pNode->pData = pNode->pCopy, pNode->pCopy = NULL;
     pNtk->ntkFunc = ABC_FUNC_MAP;
-    Extra_MmFlexStop( pNtk->pManFunc, 0 );
+    Extra_MmFlexStop( pNtk->pManFunc );
     pNtk->pManFunc = pGenlib;
 
     printf( "Library gates are successfully attached to the nodes.\n" );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index f1dd4ab5..d399ce5f 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -20,7 +20,6 @@
 
 #include "abc.h"
 #include "cut.h"
-//#include "seqInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
new file mode 100644
index 00000000..d7bb70fe
--- /dev/null
+++ b/src/base/abci/abcDress.c
@@ -0,0 +1,209 @@
+/**CFile****************************************************************
+
+  FileName    [abcDress.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Transfers names from one netlist to the other.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDress.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static stmm_table * Abc_NtkDressDeriveMapping( Abc_Ntk_t * pNtk );
+static void         Abc_NtkDressTransferNames( Abc_Ntk_t * pNtk, stmm_table * tMapping, int fVerbose );
+
+extern Abc_Ntk_t *  Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers names from one netlist to the other.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDress( Abc_Ntk_t * pNtkLogic, char * pFileName, int fVerbose )
+{
+    Abc_Ntk_t * pNtkOrig, * pNtkLogicOrig;
+    Abc_Ntk_t * pMiter, * pMiterFraig;
+    stmm_table * tMapping;
+
+    assert( Abc_NtkIsLogic(pNtkLogic) );
+
+    // get the original netlist
+    pNtkOrig = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), 1 );
+    if ( pNtkOrig == NULL )
+        return;
+    assert( Abc_NtkIsNetlist(pNtkOrig) );
+
+    Abc_NtkCleanCopy(pNtkLogic);
+    Abc_NtkCleanCopy(pNtkOrig);
+
+    // convert it into the logic network
+    pNtkLogicOrig = Abc_NtkNetlistToLogic( pNtkOrig );
+    // check that the networks have the same PIs/POs/latches
+    if ( !Abc_NtkCompareSignals( pNtkLogic, pNtkLogicOrig, 1, 1 ) )
+    {
+        Abc_NtkDelete( pNtkOrig );
+        Abc_NtkDelete( pNtkLogicOrig );
+        return;
+    }
+
+    // convert the current logic network into an AIG
+    pMiter = Abc_NtkStrash( pNtkLogic, 1, 0 );
+
+    // convert it into the AIG and make the netlist point to the AIG
+    Abc_NtkAppend( pMiter, pNtkLogicOrig, 1 );
+    Abc_NtkTransferCopy( pNtkOrig );
+    Abc_NtkDelete( pNtkLogicOrig );
+
+if ( fVerbose ) 
+{
+printf( "After mitering:\n" );
+printf( "Logic:  Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkLogic), Abc_NtkCountCopy(pNtkLogic) );
+printf( "Orig:   Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkOrig),  Abc_NtkCountCopy(pNtkOrig) );
+}
+
+    // fraig the miter (miter nodes point to the fraiged miter)
+    pMiterFraig = Abc_NtkIvyFraig( pMiter, 100, 1, 0, 1, 0 );
+    // make netlists point to the fraiged miter
+    Abc_NtkTransferCopy( pNtkLogic );
+    Abc_NtkTransferCopy( pNtkOrig );
+    Abc_NtkDelete( pMiter );
+
+if ( fVerbose ) 
+{
+printf( "After fraiging:\n" );
+printf( "Logic:  Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkLogic), Abc_NtkCountCopy(pNtkLogic) );
+printf( "Orig:   Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkOrig),  Abc_NtkCountCopy(pNtkOrig) );
+}
+
+    // derive mapping from the fraiged nodes into their prototype nodes in the original netlist
+    tMapping = Abc_NtkDressDeriveMapping( pNtkOrig );
+
+    // transfer the names to the new netlist
+    Abc_NtkDressTransferNames( pNtkLogic, tMapping, fVerbose );
+
+    // clean up
+    stmm_free_table( tMapping );
+    Abc_NtkDelete( pMiterFraig );
+    Abc_NtkDelete( pNtkOrig );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the mapping from the fraig nodes point into the nodes of the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+stmm_table * Abc_NtkDressDeriveMapping( Abc_Ntk_t * pNtk )
+{
+    stmm_table * tResult;
+    Abc_Obj_t * pNode, * pNodeMap, * pNodeFraig;
+    int i;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    tResult = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // get the fraiged node
+        pNodeFraig = Abc_ObjRegular(pNode->pCopy);
+        // if this node is already mapped, skip
+        if ( stmm_is_member( tResult, (char *)pNodeFraig ) )
+            continue;
+        // get the mapping of this node
+        pNodeMap = Abc_ObjNotCond( pNode, Abc_ObjIsComplement(pNode->pCopy) );
+        // add the mapping
+        stmm_insert( tResult, (char *)pNodeFraig, (char *)pNodeMap );
+    }
+    return tResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Attaches the names of to the new netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDressTransferNames( Abc_Ntk_t * pNtk, stmm_table * tMapping, int fVerbose )
+{
+    Abc_Obj_t * pNet, * pNode, * pNodeMap, * pNodeFraig;
+    char * pName;
+    int i, Counter = 0, CounterInv = 0, CounterInit = stmm_count(tMapping);
+    assert( Abc_NtkIsLogic(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // if the node already has a name, quit
+        pName = Nm_ManFindNameById( pNtk->pManName, pNode->Id );
+        if ( pName != NULL )
+            continue;
+        // get the fraiged node
+        pNodeFraig = Abc_ObjRegular(pNode->pCopy);
+        // find the matching node of the original netlist
+        if ( !stmm_lookup( tMapping, (char *)pNodeFraig, (char **)&pNodeMap ) )
+            continue;
+        // find the true match
+        pNodeMap = Abc_ObjNotCond( pNodeMap, Abc_ObjIsComplement(pNode->pCopy) );
+        // get the name
+        pNet = Abc_ObjFanout0(Abc_ObjRegular(pNodeMap));
+        pName = Nm_ManFindNameById( pNet->pNtk->pManName, pNet->Id );
+        assert( pName != NULL );
+        // set the name
+        if ( Abc_ObjIsComplement(pNodeMap) )
+        {
+            Abc_ObjAssignName( pNode, pName, "_inv" );
+            CounterInv++;
+        }
+        else
+        {
+            Abc_ObjAssignName( pNode, pName, NULL );
+            Counter++;
+        }
+        // remove the name
+        stmm_delete( tMapping, (char **)&pNodeFraig, (char **)&pNodeMap );
+    }
+    if ( fVerbose )
+    {
+        printf( "Total number of names collected = %5d.\n", CounterInit );
+        printf( "Total number of names assigned  = %5d. (Dir = %5d. Compl = %5d.)\n", 
+            Counter + CounterInv, Counter, CounterInv );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index be8b8ec5..9ce1ad26 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -76,7 +76,6 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     int fCleanup = 1;
 //timeRetime = clock();
     assert( !Abc_NtkIsNetlist(pNtk) );
-    assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
@@ -373,6 +372,43 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets the final nodes to point to the original nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkTransferPointers( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig )
+{
+    Abc_Obj_t * pObj;
+    Ivy_Obj_t * pObjIvy, * pObjFraig;
+    int i;
+    pObj = Abc_AigConst1(pNtk);
+    pObj->pCopy = Abc_AigConst1(pNtkAig);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkCi(pNtkAig, i);
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkCo(pNtkAig, i);
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkBox(pNtkAig, i);
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        pObjIvy = (Ivy_Obj_t *)pObj->pCopy;
+        if ( pObjIvy == NULL )
+            continue;
+        pObjFraig = Ivy_ObjEquiv( pObjIvy );
+        if ( pObjFraig == NULL )
+            continue;
+        pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId );
+        pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -382,7 +418,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
 {
     Ivy_FraigParams_t Params, * pParams = &Params; 
     Abc_Ntk_t * pNtkAig;
@@ -396,8 +432,19 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     pParams->fProve       = fProve;
     pParams->fDoSparse    = fDoSparse;
     pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
+    // transfer the pointers
+    if ( fTransfer == 1 )
+    {
+        Vec_Ptr_t * vCopies;
+        vCopies = Abc_NtkSaveCopy( pNtk );
+        pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+        Abc_NtkLoadCopy( pNtk, vCopies );
+        Vec_PtrFree( vCopies );
+        Abc_NtkTransferPointers( pNtk, pNtkAig );
+    }
+    else
+        pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pTemp );
-    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
     Ivy_ManStop( pMan );
     return pNtkAig;
 }
@@ -417,6 +464,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
     Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
+    Abc_Obj_t * pObj, * pFanin;
     Ivy_Man_t * pMan;
     int RetValue;
     assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
@@ -432,6 +480,16 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
         Abc_NtkDelete( pNtkTemp );
     }
 
+    // check the case when the 0000 simulation pattern detect the bug
+    pObj = Abc_NtkPo(pNtk,0);
+    pFanin = Abc_ObjFanin0(pObj);
+    if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
+    {
+        pNtk->pModel = ALLOC( int, Abc_NtkPiNum(pNtk) );
+        memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) );
+        return 0;
+    }
+
     // if SAT only, solve without iteration
     RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL );
     if ( RetValue >= 0 )
@@ -441,15 +499,16 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
     {
         pParams->fUseRewriting = 0;
-        Abc_NtkRewrite( pNtk, 0, 0, 0 );
+        Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
         pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );          
         Abc_NtkDelete( pNtkTemp );
-        Abc_NtkRewrite( pNtk, 0, 0, 0 );
+        Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
         Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
     }
 
     // convert ABC network into IVY network
     pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+
     // solve the CEC problem
     RetValue = Ivy_FraigProve( &pMan, pParams );
     // convert IVY network into ABC network    
@@ -503,7 +562,6 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
 
     assert( !Abc_NtkIsNetlist(pNtk) );
-    assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
@@ -624,14 +682,14 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     vNodes = Ivy_ManDfs( pMan );
     Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
     {
-        // add the first fanins
+        // add the first fanin
         pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
         if ( Ivy_ObjIsBuf(pNode) )
         {
             pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
             continue;
         }
-        // add the first second
+        // add the second fanin
         pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
         // create the new node
         if ( Ivy_ObjIsExor(pNode) )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 0ee1e804..ddbbf671 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1028,6 +1028,12 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
     printf( "First cone = %6d.  Second cone = %6d.  Common = %6d.\n", vNodes1->nSize, vNodes2->nSize, nCommon );
     Vec_PtrFree( vNodes1 );
     Vec_PtrFree( vNodes2 );
+
+    // reorder the latches
+    Abc_NtkOrderCisCos( pNtk );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtk ) )
+        printf( "Abc_NtkDemiter: The network check has failed.\n" );
     return 1;
 }
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 8793ce53..f127811e 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -256,7 +256,7 @@ DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDrop
     Abc_AigCleanup( pNtk->pManFunc );
 
     // start the manager
-    assert( Abc_NtkGlobalBdds(pNtk) == NULL );
+    assert( Abc_NtkGlobalBdd(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 );
diff --git a/src/base/abci/abcPga.c b/src/base/abci/abcPga.c
deleted file mode 100644
index 1227d7b8..00000000
--- a/src/base/abci/abcPga.c
+++ /dev/null
@@ -1,154 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcPga.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 - June 20, 2005.]
-
-  Revision    [$Id: abcPga.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "fraig.h"
-#include "fpga.h"
-#include "pga.h"
-#include "cut.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts );
- 
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Interface with the FPGA mapping package.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams )
-{
-    Abc_Ntk_t * pNtkNew, * pNtk = pParams->pNtk;
-    Pga_Man_t * pMan;
-    Vec_Ptr_t * vNodeCuts;
-
-    assert( Abc_NtkIsStrash(pNtk) );
-
-    // print a warning about choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Performing FPGA mapping with choices.\n" );
-
-    // start the mapping manager
-    pMan = Pga_ManStart( pParams );    
-    if ( pMan == NULL )
-        return NULL;
-
-    // perform mapping
-    vNodeCuts = Pga_DoMapping( pMan );
-
-    // transform the result of mapping into a BDD logic network
-    pNtkNew = Abc_NtkFromPga( pNtk, vNodeCuts );
-    if ( pNtkNew == NULL )
-        return NULL;
-    Pga_ManStop( pMan );
-    Vec_PtrFree( vNodeCuts );
-
-    // make the network minimum base
-    Abc_NtkMinimumBase( pNtkNew );
-
-    if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-
-    // make sure that everything is okay
-    if ( !Abc_NtkCheck( pNtkNew ) )
-    {
-        printf( "Abc_NtkPga: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
-    }
-    return pNtkNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the mapped network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts )
-{
-    ProgressBar * pProgress;
-    DdManager * dd;
-    Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pNode, * pFanin, * pNodeNew;
-    Cut_Cut_t * pCut;
-    Vec_Ptr_t * vLeaves, * vVisited;
-    int i, k, nDupGates;
-    // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
-    dd = pNtkNew->pManFunc;
-    // add new nodes in topologic order
-    vLeaves  = Vec_PtrAlloc( 6 );
-    vVisited = Vec_PtrAlloc( 100 );
-    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodeCuts) );
-    Vec_PtrForEachEntry( vNodeCuts, pCut, i )
-    {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        // create the new node
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );
-        Vec_PtrClear( vLeaves );
-        for ( k = 0; k < (int)pCut->nLeaves; k++ )
-        {
-            // add the node representing the old fanin in the new network
-            pFanin = Abc_NtkObj( pNtk, pCut->pLeaves[k] );
-            Vec_PtrPush( vLeaves, pFanin );
-            Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
-        }
-        // set the new node at the old node
-        pNode = Abc_NtkObj( pNtk, pCut->uSign );  // pCut->uSign contains the ID of the root node
-        pNode->pCopy = pNodeNew;
-        // create the function of the new node
-        pNodeNew->pData = Abc_NodeConeBdd( dd, dd->vars, pNode, vLeaves, vVisited );   Cudd_Ref( pNodeNew->pData );
-    }
-    Extra_ProgressBarStop( pProgress );
-    Vec_PtrFree( vVisited );
-    Vec_PtrFree( vLeaves );
-    // finalize the new network
-    Abc_NtkFinalize( pNtk, pNtkNew );
-    // decouple the PO driver nodes to reduce the number of levels
-    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-//    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
-//        printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
-    return pNtkNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 6698e738..e162ada4 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -51,28 +51,20 @@ int s_MappingMem = 0;
 ***********************************************************************/
 void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
-    int Num;//, Num2;
-
-//    Abc_NtkDetectMatching( pNtk );
-//    return;
+    int Num;
     fprintf( pFile, "%-13s:",       pNtk->pName );
     if ( Abc_NtkAssertNum(pNtk) )
         fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
     else
         fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
-
-//    if ( !Abc_NtkIsSeq(pNtk) )
-        fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
-//    else
-//        fprintf( pFile, "  lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
-
+    fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
     if ( Abc_NtkIsNetlist(pNtk) )
     {
         fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
         fprintf( pFile, "  nd = %5d",  Abc_NtkNodeNum(pNtk) );
         fprintf( pFile, "  box = %5d", Abc_NtkBoxNum(pNtk) );
     }
-    else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
+    else if ( Abc_NtkIsStrash(pNtk) )
     {        
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
         if ( Num = Abc_NtkGetChoiceNum(pNtk) )
@@ -87,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
-    if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) || Abc_NtkIsNetlist(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
     {
     }
     else if ( Abc_NtkHasSop(pNtk) )   
@@ -114,7 +106,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 
     if ( Abc_NtkIsStrash(pNtk) )
         fprintf( pFile, "  lev = %3d", Abc_AigLevel(pNtk) );
-    else if ( !Abc_NtkIsSeq(pNtk) )
+    else 
         fprintf( pFile, "  lev = %3d", Abc_NtkLevel(pNtk) );
 
     fprintf( pFile, "\n" );
@@ -260,16 +252,6 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
     int InitNums[4], Init;
 
     assert( !Abc_NtkIsNetlist(pNtk) );
-/*
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        Seq_NtkLatchGetInitNums( pNtk, InitNums );
-        fprintf( pFile, "%-15s:  ", pNtk->pName );
-        fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", 
-            Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
-        return;
-    }
-*/
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         fprintf( pFile, "The network is combinational.\n" );
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index fcd44d30..d206ae6e 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -26,7 +26,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
@@ -134,13 +133,13 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
                     break;
 */
 /*
-                Abc_NtkRewrite( pNtk, 0, 0, 0 );
+                Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                     break;
                 if ( --Counter == 0 )
                     break;
 */
-                Abc_NtkRewrite( pNtk, 0, 0, 0 );
+                Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                     break;
                 if ( --Counter == 0 )
@@ -329,9 +328,9 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
 Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkTemp;
-    Abc_NtkRewrite( pNtk, 0, 0, 0 );
+    Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
     pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );  Abc_NtkDelete( pNtkTemp );
-    Abc_NtkRewrite( pNtk, 0, 0, 0 );
+    Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
     Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
     return pNtk;
 }
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 151b5256..e7dbf3a1 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -51,7 +51,7 @@ static void        Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose )
+int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose )
 {
     ProgressBar * pProgress;
     Cut_Man_t * pManCut;
@@ -76,6 +76,9 @@ clk = clock();
 Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
     pNtk->pManCut = pManCut;
 
+    if ( fVeryVerbose )
+        Rwr_ScoresClean( pManRwr );
+
     // resynthesize each node once
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
@@ -147,6 +150,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     if ( fVerbose )
         Rwr_ManPrintStats( pManRwr );
 //        Rwr_ManPrintStatsFile( pManRwr );
+    if ( fVeryVerbose )
+        Rwr_ScoresReport( pManRwr );
     // delete the managers
     Rwr_ManStop( pManRwr );
     Cut_ManStop( pManCut );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 2e1b3eb1..9af6dc00 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -285,7 +285,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
     pMan = pNodeOld->pNtk->pManFunc;
     pRoot = pNodeOld->pData;
     // check the constant case
-    if ( Abc_NodeIsConst(pNodeOld) )
+    if ( Abc_NodeIsConst(pNodeOld) || Hop_Regular(pRoot) == Hop_ManConst1(pMan) )
         return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Hop_IsComplement(pRoot) );
     // set elementary variables
     Abc_ObjForEachFanin( pNodeOld, pFanin, i )
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index acd63771..7697fde1 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -280,7 +280,6 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach )
 {
-/*
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
     int * pPermute;
@@ -292,14 +291,14 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     pNtkNew->pSpec = NULL;
 
     // create PIs corresponding to LOs
-    Abc_NtkForEachLatch( pNtk, pNode, i )
+    Abc_NtkForEachLatchOutput( pNtk, pNode, i )
         Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL );
     // cannot ADD POs here because pLatch->pCopy point to the PIs
 
     // create a new node
     pNodeNew = Abc_NtkCreateNode(pNtkNew);
     // add the fanins corresponding to latch outputs
-    Abc_NtkForEachLatch( pNtk, pNode, i )
+    Abc_NtkForEachLatchOutput( pNtk, pNode, i )
         Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
 
     // create the logic function
@@ -317,14 +316,14 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkForEachPo( pNtk, pNode, i )
         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
             Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in"), NULL );
+    Abc_NtkForEachLatchInput( pNtk, pNode, i )
+        Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
 
     // link to the POs of the network 
     Abc_NtkForEachPo( pNtk, pNode, i )
         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
             Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
-    Abc_NtkForEachLatch( pNtk, pNode, i )
+    Abc_NtkForEachLatchInput( pNtk, pNode, i )
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
 
     // remove the extra nodes
@@ -340,8 +339,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
         return NULL;
     }
     return pNtkNew;
-*/
-    return NULL;
+//    return NULL;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index f4717eda..ec0ba8ca 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -176,6 +176,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Prove_ParamsSetDefault( pParams );
     pParams->nItersMax = 5;
 //    RetValue = Abc_NtkMiterProve( &pMiter, pParams );
+//    pParams->fVerbose = 1;
     RetValue = Abc_NtkIvyProve( &pMiter, pParams );
     if ( RetValue == -1 )
         printf( "Networks are undecided (resource limits is reached).\n" );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 7e674fbe..169ab577 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -7,6 +7,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
     src/base/abci/abcDebug.c \
+    src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcEspresso.c \
     src/base/abci/abcExtract.c \