Version abc61102

14 files changed, 993 insertions, 128 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b25ca2f7..5d6af56d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36,6 +36,7 @@ static int Abc_CommandPrintExdc      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandPrintIo        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintLatch     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintFanio     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintMffc      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintFactor    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintLevel     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSupport   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -90,6 +91,7 @@ static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** arg
 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_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -102,6 +104,7 @@ static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigTrust     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -166,6 +169,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_latch",   Abc_CommandPrintLatch,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_mffc",    Abc_CommandPrintMffc,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
@@ -220,6 +224,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     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",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
@@ -232,6 +237,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "bmc",           Abc_CommandBmc,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
@@ -250,15 +256,15 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
 
-    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
+//    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, "Verification", "cec",           Abc_CommandCec,              0 );
@@ -269,8 +275,8 @@ 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 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "howard",        Abc_CommandHoward,           0 );
+//    Cmd_CommandAdd( pAbc, "Sequential",   "skew_fwd",      Abc_CommandSkewForward,      0 );
 
 //    Rwt_Man4ExploreStart();
 //    Map_Var3Print();
@@ -629,6 +635,58 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintMffc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    extern void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk );
+
+    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;
+    }
+
+    // print the nodes
+    Abc_NtkPrintMffc( pOut, pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_mffc [-h]\n" );
+    fprintf( pErr, "\t        prints the MFFC of each node in the network\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -1581,7 +1639,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int fMulti;
-    extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesShow );
     extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -1609,7 +1667,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkHasAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Visualizing networks other than AIGs can be done using command \"show_ntk\".\n" );
         return 1;
@@ -1622,7 +1680,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     if ( !fMulti )
-        Abc_NtkShowAig( pNtk );
+        Abc_NtkShowAig( pNtk, NULL );
     else
         Abc_NtkShowMulti( pNtk );
     return 0;
@@ -1683,7 +1741,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Abc_NtkHasAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Visualizing AIG can only be done using command \"show_aig\".\n" );
         return 1;
@@ -4975,14 +5033,97 @@ usage:
   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_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
     int c;
     int nLevels;
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
-    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
+//    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5064,7 +5205,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 
 //    Ivy_TruthEstimateNodesTest();
-
+/*
     pNtkRes = Abc_NtkIvy( pNtk );
 //    pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 );
 //    pNtkRes = NULL;
@@ -5075,7 +5216,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-
+*/
+    Abc_NtkMaxFlowTest( pNtk );
     return 0;
 
 usage:
@@ -5100,7 +5242,7 @@ usage:
 int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
     int c;
     extern Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk );
 
@@ -5132,11 +5274,12 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" );
-        return 1;
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+        pNtkRes = Abc_NtkIvyStrash( pNtkTemp );
+        Abc_NtkDelete( pNtkTemp );
     }
-
-    pNtkRes = Abc_NtkIvyStrash( pNtk );
+    else
+        pNtkRes = Abc_NtkIvyStrash( pNtk );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -5741,9 +5884,9 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nIters       = 3;
-    fUseZeroCost = 1;
-    fVerbose     = 0;
+    nIters       = 2;
+    fUseZeroCost = 0;
+    fVerbose     = 1;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
     {
@@ -5869,6 +6012,94 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int fInit;
+    int fVerbose;
+
+    extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames  = 5;
+    fInit    = 0;
+    fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'i':
+            fInit ^= 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_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
+    else
+    {
+        pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+        Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
+        Abc_NtkDelete( pNtk );
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: bmc [-K num] [-ivh]\n" );
+    fprintf( pErr, "\t         perform bounded model checking\n" );
+    fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-i     : toggle initialization of the first frame [default = %s]\n", fInit? "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;
+}
 
 
 /**Function*************************************************************
@@ -7573,48 +7804,38 @@ usage:
 int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
     int c, nMaxIters;
-    int fForward;
-    int fBackward;
     int fInitial;
     int fVerbose;
+    int Mode;
+    extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fForward  = 0;
-    fBackward = 0;
+    Mode      = 3;
     fInitial  = 1;
-    fVerbose  = 0;
+    fVerbose  = 1;
     nMaxIters = 15;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Ifbivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'I':
+        case 'M':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+                fprintf( pErr, "Command line switch \"-M\" should be followed by a positive integer.\n" );
                 goto usage;
             }
-            nMaxIters = atoi(argv[globalUtilOptind]);
+            Mode = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nMaxIters < 0 ) 
+            if ( Mode < 0 ) 
                 goto usage;
             break;
-        case 'f':
-            fForward ^= 1;
-            break;
-        case 'b':
-            fBackward ^= 1;
-            break;
-        case 'i':
-            fInitial ^= 1;
-            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7631,61 +7852,56 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 )
+    if ( !Abc_NtkLatchNum(pNtk) )
     {
         fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
         return 0;
     }
 
-    if ( Abc_NtkHasAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
-        // quit if there are choice nodes
         if ( Abc_NtkGetChoiceNum(pNtk) )
         {
-            fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
+            fprintf( pErr, "Retiming with choice nodes is not implemented.\n" );
             return 0;
         }
-        if ( Abc_NtkIsStrash(pNtk) )
-            pNtkRes = Abc_NtkAigToSeq(pNtk);
-        else
-            pNtkRes = Abc_NtkDup(pNtk);
-        // retime the network
-        if ( fForward )
-            Seq_NtkSeqRetimeForward( pNtkRes, fInitial, fVerbose );
-        else if ( fBackward )
-            Seq_NtkSeqRetimeBackward( pNtkRes, fInitial, fVerbose );
-        else
-            Seq_NtkSeqRetimeDelay( pNtkRes, nMaxIters, fInitial, fVerbose );
-        // if the network is an AIG, convert the result into an AIG
-        if ( Abc_NtkIsStrash(pNtk) )
-        {
-            pNtkRes = Abc_NtkSeqToLogicSop( pNtkTemp = pNtkRes );
-            Abc_NtkDelete( pNtkTemp );
-            pNtkRes = Abc_NtkStrash( pNtkTemp = pNtkRes, 0, 0 );
-            Abc_NtkDelete( pNtkTemp );
-        }
+        pNtk = Abc_NtkAigToLogicSop( pNtkTemp = pNtk );
+        Abc_NtkDelete( pNtkTemp );
     }
-    else
-        pNtkRes = Seq_NtkRetime( pNtk, nMaxIters, fInitial, fVerbose );
-    // replace the network
-    if ( pNtkRes == NULL )
+
+    // get the network in the SOP form
+    if ( !Abc_NtkLogicToSop(pNtk, 0) )
     {
-        fprintf( pErr, "Retiming has failed.\n" );
+        printf( "Converting to SOPs has failed.\n" );
         return 0;
     }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        fprintf( pErr, "The network is not a logic network. Retiming is not performed.\n" );
+        return 0;
+    }
+
+    // perform the retiming
+    Abc_NtkRetime( pNtk, Mode, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: retime [-I num] [-fbih]\n" );
-    fprintf( pErr, "\t         retimes the current network using Pan's delay-optimal retiming\n" );
-    fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
-    fprintf( pErr, "\t-f     : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" );
-    fprintf( pErr, "\t-b     : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" );
-    fprintf( pErr, "\t-i     : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" );
+    fprintf( pErr, "usage: retime [-M num] [-vh]\n" );
+    fprintf( pErr, "\t         retimes the current network using one of the algorithms:\n" );
+    fprintf( pErr, "\t             1: most forward retiming\n" );
+    fprintf( pErr, "\t             2: most backward retiming\n" );
+    fprintf( pErr, "\t             3: min-area retiming\n" );
+    fprintf( pErr, "\t             4: min-delay retiming\n" );
+    fprintf( pErr, "\t             5: min-area under min-delay constraint retiming\n" );
+    fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
+//    fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
+//    fprintf( pErr, "\t-f     : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" );
+//    fprintf( pErr, "\t-b     : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" );
+//    fprintf( pErr, "\t-i     : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" );
 }
 
 /**Function*************************************************************
@@ -8069,17 +8285,22 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    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, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -8091,18 +8312,23 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( pErr, "Only works for sequential AIGs.\n" );
+        fprintf( pErr, "Only works for logic networks.\n" );
         return 1;
     }
     // modify the current network
-    Seq_NtkCleanup( pNtk, 1 );
+    Abc_NtkCleanupSeq( pNtk, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scleanup [-h]\n" );
+    fprintf( pErr, "usage: scleanup [-vh]\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-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
new file mode 100644
index 00000000..af6d237b
--- /dev/null
+++ b/src/base/abci/abcBmc.c
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+  FileName    [abcBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Performs bounded model check.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
+
+static void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose )
+{
+    Ivy_FraigParams_t Params, * pParams = &Params; 
+    Ivy_Man_t * pMan, * pFrames, * pFraig;
+    Vec_Ptr_t * vMapping;
+    // convert to IVY manager
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+    // generate timeframes
+    pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping );
+    // fraig the timeframes
+    Ivy_FraigParamsDefault( pParams );
+    pParams->nBTLimitNode = ABC_INFINITY;
+    pParams->fVerbose = 0;
+    pParams->fProve = 0;
+    pFraig = Ivy_FraigPerform( pFrames, pParams );
+printf( "Frames have %6d nodes.  ", Ivy_ManNodeNum(pFrames) );
+printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
+    // report the classes
+//    if ( fVerbose )
+//        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
+    // free stuff
+    Vec_PtrFree( vMapping );
+    Ivy_ManStop( pFraig );
+    Ivy_ManStop( pFrames );
+    Ivy_ManStop( pMan );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames )
+{
+    Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3;
+    int i, f, nIdMax, Prev2, Prev3;
+    nIdMax = Ivy_ManObjIdMax(pMan);
+    // check what is the number of nodes in each frame
+    Prev2 = Prev3 = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Ivy_ManForEachNode( pMan, pFirst1, i )
+        {
+            pFirst2 = Ivy_Regular( Vec_PtrEntry(vMapping, f * nIdMax + pFirst1->Id) );
+            if ( Ivy_ObjIsConst1(pFirst2) || pFirst2->Type == 0 )
+                continue;
+            pFirst3 = Ivy_Regular( pFirst2->pEquiv );
+            if ( Ivy_ObjIsConst1(pFirst3) || pFirst3->Type == 0 )
+                continue;
+            break;
+        }
+        if ( f )
+            printf( "Frame %3d :  Strash = %5d  Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 );
+        Prev2 = pFirst2->Id;
+        Prev3 = pFirst3->Id;   
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 6708217c..b38012cd 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     int i, nNodesDsd;
 
     // save the CI nodes in the DSD nodes
-    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) );
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 80238b48..3bc9fbed 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -210,7 +210,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
         Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy );
     // set the constant node
 //    if ( Fpga_NodeReadRefs(Fpga_ManReadConst1(pMan)) > 0 )
-        Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) );
+        Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NtkCreateNodeConst1(pNtkNew) );
     // process the nodes in topological order
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c
index b307273f..3ad29291 100644
--- a/src/base/abci/abcFpgaFast.c
+++ b/src/base/abci/abcFpgaFast.c
@@ -99,7 +99,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
     // start the new ABC network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
-    Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) );
+    Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
         Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc ); 
     // recursively construct the network
@@ -112,7 +112,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
         if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
         {
             if ( Abc_ObjIsCi(pObjAbc) )
-                pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc );
+                pObjAbc = Abc_NtkCreateNodeInv( pNtkNew, pObjAbc );
             else
             {
                 // clone the node
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 82e03119..446eb0cc 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -51,7 +51,7 @@ static inline Abc_Obj_t *  Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge )    {
 static inline Abc_Obj_t *  Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
 static inline Abc_Obj_t *  Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
 
-static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs );
+static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -85,7 +85,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
     {
         printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
-        return NULL;
+//        return NULL;
     }
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
@@ -102,9 +102,9 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     if ( fSeq )
     {
         int nLatches = Abc_NtkLatchNum(pNtk);
-        int * pInit = Abc_NtkCollectLatchValues( pNtk, fUseDc );
-        Ivy_ManMakeSeq( pMan, nLatches, pInit );
-        FREE( pInit );
+        Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
+        Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
+        Vec_IntFree( vInit );
 //        Ivy_ManPrintStats( pMan );
     }
     return pMan;
@@ -191,8 +191,8 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
         return NULL;
 
     Ivy_ManHaigStart( pMan, fVerbose );
-    Ivy_ManRewriteSeq( pMan, 0, 0 );
-    for ( i = 1; i < nIters; i++ )
+//    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    for ( i = 0; i < nIters; i++ )
         Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
     Ivy_ManHaigPostprocess( pMan, fVerbose );
 
@@ -486,7 +486,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     int fCleanup = 1;
 //    int nNodes;
     int nLatches = Abc_NtkLatchNum(pNtk);
-    int * pInit = Abc_NtkCollectLatchValues( pNtk, 0 );
+    Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
 
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
@@ -494,7 +494,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
         {
-            FREE( pInit );
+            Vec_IntFree( vInit );
             printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
             return NULL;
         }
@@ -513,7 +513,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     pMan = Abc_NtkToAig( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
-        FREE( pInit );
+        Vec_IntFree( vInit );
         printf( "AIG check has failed.\n" );
         Ivy_ManStop( pMan );
         return NULL;
@@ -975,22 +975,23 @@ Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, cha
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs )
+Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
 {
     Abc_Obj_t * pLatch;
-    int * pArray, i;
-    pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+    Vec_Int_t * vArray;
+    int i;
+    vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         if ( fUseDcs || Abc_LatchIsInitDc(pLatch) )
-            pArray[i] = IVY_INIT_DC;
+            Vec_IntPush( vArray, IVY_INIT_DC );
         else if ( Abc_LatchIsInit1(pLatch) )
-            pArray[i] = IVY_INIT_1;
+            Vec_IntPush( vArray, IVY_INIT_1 );
         else if ( Abc_LatchIsInit0(pLatch) )
-            pArray[i] = IVY_INIT_0;
+            Vec_IntPush( vArray, IVY_INIT_0 );
         else assert( 0 );
     }
-    return pArray;
+    return vArray;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index 165d84c5..61b1ce78 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -148,7 +148,7 @@ int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int
         // if there is no delay improvement, skip; otherwise, update level
         if ( pObjTop->Level >= pObj->Level )
         {
-            Abc_NtkDeleteObj_rec( pObjTop );
+            Abc_NtkDeleteObj_rec( pObjTop, 1 );
             continue;
         }
         pObj->Level = pObjTop->Level;
@@ -570,7 +570,7 @@ Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
         {
             Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
                 if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
-                    Abc_NtkDeleteObj_rec( pFanin );
+                    Abc_NtkDeleteObj_rec( pFanin, 1 );
             return NULL;
         }
     // create the topmost node
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 276e41d0..c4f9850a 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -259,7 +259,7 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int
 
     // check the case of constant node
     if ( Map_NodeIsConst(pNodeMap) )
-        return fPhase? Abc_NodeCreateConst1(pNtkNew) : Abc_NodeCreateConst0(pNtkNew);
+        return fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
 
     // check if the phase is already implemented
     pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase );
@@ -369,7 +369,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap
              * (since the cut only has 4 variables). An interesting question is what
              * if the first variable (and not the fifth one is the redundant one;
              * can that happen?) */
-            return Abc_NodeCreateConst0(pNtkNew);
+            return Abc_NtkCreateNodeConst0(pNtkNew);
         }
     }
 
@@ -503,14 +503,14 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     // set the pointers from the mapper to the new nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
-        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) );
         Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy );
     }
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
 //        if ( Abc_NodeIsConst(pNode) )
 //            continue;
-        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) );
         Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy );
     }
 
@@ -630,7 +630,7 @@ Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * p
              * (since the cut only has 4 variables). An interesting question is what
              * if the first variable (and not the fifth one is the redundant one;
              * can that happen?) */
-            return Abc_NodeCreateConst0(pNtkNew);
+            return Abc_NtkCreateNodeConst0(pNtkNew);
         }
     }
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 9b67ab13..a1f6b9f9 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -195,7 +195,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
     pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
     st_free_table( tBdd2Node );
     if ( Cudd_IsComplement(bFunc) )
-        pNodeNew = Abc_NodeCreateInv( pNtkNew, pNodeNew );
+        pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
     return pNodeNew;
 }
 
@@ -215,18 +215,18 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
     Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
     assert( !Cudd_IsComplement(bFunc) );
     if ( bFunc == b1 )
-        return Abc_NodeCreateConst1(pNtkNew);
+        return Abc_NtkCreateNodeConst1(pNtkNew);
     if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
         return pNodeNew;
     // solve for the children nodes
     pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
     if ( Cudd_IsComplement(cuddE(bFunc)) )
-        pNodeNew0 = Abc_NodeCreateInv( pNtkNew, pNodeNew0 );
+        pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
     pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
     if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
         assert( 0 );
     // create the MUX node
-    pNodeNew = Abc_NodeCreateMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
+    pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
     st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
     return pNodeNew;
 }
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index afc635e9..6af12afd 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -61,10 +61,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else
         fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
 
-    if ( !Abc_NtkIsSeq(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) );
+//    else
+//        fprintf( pFile, "  lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
 
     if ( Abc_NtkIsNetlist(pNtk) )
     {
@@ -228,6 +228,7 @@ 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 );
@@ -236,7 +237,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
             Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
         return;
     }
-
+*/
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         fprintf( pFile, "The network is combinational.\n" );
@@ -383,6 +384,26 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints the MFFCs of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Abc_NodeMffsConeSuppPrint( pNode );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints the factored form of one node.]
 
   Description []
@@ -833,6 +854,84 @@ void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ) {
   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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    fprintf( pFile, "Object %5d : ", pObj->Id );
+    switch ( pObj->Type )
+    {
+        case ABC_OBJ_NONE: 
+            fprintf( pFile, "NONE   " );  
+            break;
+        case ABC_OBJ_CONST1: 
+            fprintf( pFile, "Const1 " );  
+            break;
+        case ABC_OBJ_PIO:    
+            fprintf( pFile, "PIO    " );  
+            break;
+        case ABC_OBJ_PI:     
+            fprintf( pFile, "PI     " );  
+            break;
+        case ABC_OBJ_PO:     
+            fprintf( pFile, "PO     " );  
+            break;
+        case ABC_OBJ_BI:     
+            fprintf( pFile, "BI     " );  
+            break;
+        case ABC_OBJ_BO:     
+            fprintf( pFile, "BO     " );  
+            break;
+        case ABC_OBJ_ASSERT:     
+            fprintf( pFile, "Assert " );  
+            break;
+        case ABC_OBJ_NET:  
+            fprintf( pFile, "Net    " );  
+            break;
+        case ABC_OBJ_NODE: 
+            fprintf( pFile, "Node   " );  
+            break;
+        case ABC_OBJ_GATE: 
+            fprintf( pFile, "Gate   " );  
+            break;
+        case ABC_OBJ_LATCH:     
+            fprintf( pFile, "Latch  " );  
+            break;
+        case ABC_OBJ_TRI:     
+            fprintf( pFile, "Tristate" );  
+            break;
+        case ABC_OBJ_BLACKBOX:     
+            fprintf( pFile, "Blackbox" );  
+            break;
+        default:
+            assert(0); 
+            break;
+    }
+    // print the fanins
+    fprintf( pFile, " Fanins ( " );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        fprintf( pFile, "%d ", pFanin->Id );
+    fprintf( pFile, ") " );
+    // print the logic function
+    if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) )
+        fprintf( pFile, " %s", pObj->pData );
+    else
+        fprintf( pFile, "\n" );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index cac634da..076bee46 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -32,6 +32,7 @@ static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t
 static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
 static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 
+static int            Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
 static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
 static void           Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 );
 static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin );
@@ -425,7 +426,7 @@ void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv,
         return;
 
     // add the invertor
-    pNodeMinInv = Abc_NodeCreateInv( pNtk, pNodeMin );
+    pNodeMinInv = Abc_NtkCreateNodeInv( pNtk, pNodeMin );
    
     // move the fanouts of the inverted nodes
     for ( pNode = pListInv; pNode; pNode = pNode->pNext )
@@ -583,7 +584,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
         if ( Abc_ObjFanoutNum(pNode) > 0 )
             Vec_PtrPush( vNodes, pNode );
         else
-            Abc_NtkDeleteObj_rec( pNode );
+            Abc_NtkDeleteObj_rec( pNode, 1 );
     }
     Vec_PtrFree( vNodes );
     // sweep a node into its CO fanout if all of this is true:
@@ -672,6 +673,263 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
     Cudd_RecursiveDeref( dd, bCof1 );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes all objects whose trav ID is not current.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRemoveNonCurrentObjects( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int Counter, i;
+    int fVerbose = 0;
+
+    // report on the nodes to be deleted
+    if ( fVerbose )
+    {
+        printf( "These nodes will be deleted: \n" );
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            if ( !Abc_NodeIsTravIdCurrent( pObj ) )
+            {
+                printf( "    " );
+                Abc_ObjPrint( stdout, pObj );
+            }
+    }
+    
+    // delete the nodes    
+    Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent( pObj ) )
+        {
+            Abc_NtkDeleteObj( pObj );
+            Counter++;
+        }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the fanin of this latch is a constant.]
+
+  Description [Returns 0/1 if constant; -1 if not a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSetTravId_rec( Abc_Obj_t * pObj )
+{
+    Abc_NodeSetTravIdCurrent(pObj);
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+        return;
+    assert( Abc_ObjFaninNum(pObj) == 1 );
+    Abc_NtkSetTravId_rec( Abc_ObjFanin0(pObj) );    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the fanin of this latch is a constant.]
+
+  Description [Returns 0/1 if constant; -1 if not a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCheckConstant_rec( Abc_Obj_t * pObj )
+{
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+    {
+        if ( !Abc_ObjIsNode(pObj) )
+            return -1;
+        if ( Abc_NodeIsConst0(pObj) )
+            return 0;
+        if ( Abc_NodeIsConst1(pObj) )
+            return 1;
+        assert( 0 );
+        return -1;
+    }
+    if ( Abc_ObjIsLatch(pObj) || Abc_ObjFaninNum(pObj) > 1 )
+        return -1;
+    if ( !Abc_ObjIsNode(pObj) || Abc_NodeIsBuf(pObj) )
+        return Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) );
+    if ( Abc_NodeIsInv(pObj) )
+    {
+        int RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) );
+        if ( RetValue == 0 )
+            return 1;
+        if ( RetValue == 1 )
+            return 0;
+        return RetValue;
+    }
+    assert( 0 );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes redundant latches.]
+
+  Description [The redundant latches are of two types:
+  - Latches fed by a constant which matches the init value of the latch.
+  - Latches fed by a constant which does not match the init value of the latch
+  can be all replaced by one latch.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkLatchSweep( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pFanin, * pLatch, * pLatchPivot = NULL;
+    int Counter, RetValue, i;
+    Counter = 0;
+    // go through the latches
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        // check if the latch has constant input
+        RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pLatch) );
+        if ( RetValue == -1 )
+            continue;
+        // found a latch with constant fanin
+        if ( (RetValue == 1 && Abc_LatchIsInit0(pLatch)) ||
+             (RetValue == 0 && Abc_LatchIsInit1(pLatch)) )
+        {
+            // fanin constant differs from the latch init value
+            if ( pLatchPivot == NULL )
+            {
+                pLatchPivot = pLatch;
+                continue;
+            }
+            if ( Abc_LatchInit(pLatch) != Abc_LatchInit(pLatchPivot) ) // add inverter
+                pFanin = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanout0(pLatchPivot) );
+            else
+                pFanin = Abc_ObjFanout0(pLatchPivot);
+        }
+        else
+            pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
+        // replace latch
+        Abc_ObjTransferFanout( Abc_ObjFanout0(pLatch), pFanin );
+        // delete the extra nodes
+        Abc_NtkDeleteObj_rec( Abc_ObjFanout0(pLatch), 0 );
+        Counter++;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces autonumnous logic by free inputs.]
+
+  Description [Assumes that non-autonomous logic is marked with
+  the current ID.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pFanin;
+    Vec_Ptr_t * vNodes;
+    int i, k, Counter;
+    // collect the nodes that feed into the reachable logic
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        // skip non-visited fanins
+        if ( !Abc_NodeIsTravIdCurrent(pNode) )
+            continue;
+        // look for non-visited fanins
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            // skip visited fanins
+            if ( Abc_NodeIsTravIdCurrent(pFanin) )
+                continue;
+            // skip constants and latches fed by constants
+            if ( Abc_NtkCheckConstant_rec(pFanin) != -1 ||
+                 (Abc_ObjIsBi(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) )
+            {
+                Abc_NtkSetTravId_rec( pFanin );
+                continue;
+            }
+            assert( !Abc_ObjIsLatch(pFanin) );
+            Vec_PtrPush( vNodes, pFanin );
+        }
+    }
+    Vec_PtrUniqify( vNodes, Abc_ObjPointerCompare );
+    // replace these nodes by the PIs
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        pFanin = Abc_NtkCreatePi(pNtk);
+        Abc_NodeSetTravIdCurrent( pFanin );
+        Abc_ObjTransferFanout( pNode, pFanin );
+    }
+    Counter = Vec_PtrSize(vNodes);
+    Vec_PtrFree( vNodes );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sequential cleanup.]
+
+  Description [Performs three tasks:
+  - Removes logic that does not feed into POs.
+  - Removes latches driven by constant values equal to the initial state.
+  - Replaces the autonomous components by additional PI variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    int Counter;
+    assert( Abc_NtkIsLogic(pNtk) );
+    // mark the nodes reachable from the POs
+    vNodes = Abc_NtkDfsSeq( pNtk );
+    Vec_PtrFree( vNodes );
+    // remove the non-marked nodes
+    Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
+    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 );
+    // 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 );
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+        printf( "Abc_NtkCleanupSeq: The network check has failed.\n" );
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 622b4103..594cc2d6 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -333,7 +333,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
         printf( "Networks are NOT EQUIVALENT after framing.\n" );
         // report the error
         pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
-        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
+//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
         FREE( pFrames->pModel );
         Abc_NtkDelete( pFrames );
         return;
@@ -365,7 +365,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     else if ( RetValue == 0 )
     {
         printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
-        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
+//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
     }
     else assert( 0 );
     // delete the fraig manager
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
new file mode 100644
index 00000000..1d56ba36
--- /dev/null
+++ b/src/base/abci/abcXsim.c
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+  FileName    [abcXsim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Using X-valued simulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcXsim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define XVS0   1
+#define XVS1   2
+#define XVSX   3
+
+static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)Value;  }
+static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)pObj->pCopy;      }
+static inline int  Abc_XsimInv( int Value )   
+{ 
+    if ( Value == XVS0 )
+        return XVS1;
+    if ( Value == XVS1 )
+        return XVS0;
+    assert( Value == XVSX );       
+    return XVSX;
+}
+static inline int  Abc_XsimAnd( int Value0, int Value1 )   
+{ 
+    if ( Value0 == XVS0 || Value1 == XVS0 )
+        return XVS0;
+    if ( Value0 == XVSX || Value1 == XVSX )
+        return XVSX;
+    assert( Value0 == XVS1 && Value1 == XVS1 );
+    return XVS1;
+}
+static inline int  Abc_XsimRand2()   
+{
+    return (rand() & 1) ? XVS1 : XVS0;
+}
+static inline int  Abc_XsimRand3()   
+{
+    int RetValue;
+    do { 
+        RetValue = rand() & 3; 
+    } while ( RetValue == 0 );
+    return RetValue;
+}
+static inline int  Abc_ObjGetXsimFanin0( Abc_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Abc_ObjGetXsim(Abc_ObjFanin0(pObj));
+    return Abc_ObjFaninC0(pObj)? Abc_XsimInv(RetValue) : RetValue;
+}
+static inline int  Abc_ObjGetXsimFanin1( Abc_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Abc_ObjGetXsim(Abc_ObjFanin1(pObj));
+    return Abc_ObjFaninC1(pObj)? Abc_XsimInv(RetValue) : RetValue;
+}
+static inline void Abc_XsimPrint( FILE * pFile, int Value )   
+{ 
+    if ( Value == XVS0 )
+    {
+        fprintf( pFile, "0" );
+        return;
+    }
+    if ( Value == XVS1 )
+    {
+        fprintf( pFile, "1" );
+        return;
+    }
+    assert( Value == XVSX );       
+    fprintf( pFile, "x" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs X-valued simulation of the sequential network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    int i, f;
+    assert( Abc_NtkIsStrash(pNtk) );
+    srand( 0x12341234 );
+    // start simulation
+    Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
+    if ( fInputs )
+    {
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, XVSX );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
+    }
+    else
+    {
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX );
+    }
+    // simulate and print the result
+    fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) );
+        // print out
+        fprintf( stdout, "%2d : ", f );
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+        fprintf( stdout, " : " );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) );
+        fprintf( stdout, " : " );
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+        fprintf( stdout, "\n" );
+        // assign input values
+        if ( fInputs )
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                Abc_ObjSetXsim( pObj, XVSX );
+        else
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+        // transfer the latch values
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
+    }
+}
+
+///////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index bb2ae1a0..50a40393 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -2,6 +2,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcAttach.c \
     src/base/abci/abcAuto.c \
     src/base/abci/abcBalance.c \
+    src/base/abci/abcBmc.c \
     src/base/abci/abcClpBdd.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
@@ -37,4 +38,5 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcTiming.c \
     src/base/abci/abcUnate.c \
     src/base/abci/abcUnreach.c \
-    src/base/abci/abcVerify.c 
+    src/base/abci/abcVerify.c \
+    src/base/abci/abcXsim.c