Version abc90310

12 files changed, 1741 insertions, 780 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index fa7c5dbc..16748233 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -45,24 +45,42 @@ struct Cec_ParSat_t_
     int              nSatVarMax;    // the max number of SAT variables
     int              nCallsRecycle; // calls to perform before recycling SAT solver
     int              fPolarFlip;    // flops polarity of variables
+    int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
     int              fVerbose;      // verbose stats
 };
 
+// simulation parameters
+typedef struct Cec_ParSim_t_ Cec_ParSim_t;
+struct Cec_ParSim_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nRounds;       // the number of simulation rounds
+    int              TimeLimit;     // the runtime limit in seconds
+    int              fDoubleOuts;   // miter with separate outputs
+    int              fCheckMiter;   // the circuit is the miter
+    int              fFirstStop;    // stop on the first sat output
+    int              fSeqSimulate;  // performs sequential simulation
+    int              fVeryVerbose;  // verbose stats
+    int              fVerbose;      // verbose stats
+};
+
 // combinational SAT sweeping parameters
-typedef struct Cec_ParCsw_t_ Cec_ParCsw_t;
-struct Cec_ParCsw_t_
+typedef struct Cec_ParFra_t_ Cec_ParFra_t;
+struct Cec_ParFra_t_
 {
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
     int              nItersMax;     // the maximum number of iterations of SAT sweeping
     int              nBTLimit;      // conflict limit at a node
-    int              nSatVarMax;    // the max number of SAT variables
-    int              nCallsRecycle; // calls to perform before recycling SAT solver
+    int              TimeLimit;     // the runtime limit in seconds
     int              nLevelMax;     // restriction on the level nodes to be swept
     int              nDepthMax;     // the depth in terms of steps of speculative reduction
     int              fRewriting;    // enables AIG rewriting
+    int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
+    int              fDoubleOuts;   // miter with separate outputs
+    int              fColorDiff;    // miter with separate outputs
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
@@ -71,13 +89,12 @@ struct Cec_ParCsw_t_
 typedef struct Cec_ParCec_t_ Cec_ParCec_t;
 struct Cec_ParCec_t_
 {
-    int              nIters;        // iterations of SAT solving/sweeping
-    int              nBTLimitBeg;   // starting backtrack limit
-    int              nBTlimitMulti; // multiple of backtrack limit
+    int              nBTLimit;      // conflict limit at a node
+    int              TimeLimit;     // the runtime limit in seconds
+    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
     int              fRewriting;    // enables AIG rewriting
-    int              fSatSweeping;  // enables SAT sweeping
-    int              fFirstStop;    // stop on the first sat output
+    int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
 
@@ -89,12 +106,17 @@ struct Cec_ParCec_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== cecCec.c ==========================================================*/
+extern int           Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
+extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
 /*=== cecCore.c ==========================================================*/
 extern void          Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
-extern void          Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p );
+extern void          Cec_ManSimSetDefaultParams( Cec_ParSim_t * p );
+extern void          Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
 extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
-extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars );
+extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
 extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void          Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
new file mode 100644
index 00000000..ea730693
--- /dev/null
+++ b/src/aig/cec/cecCec.c
@@ -0,0 +1,241 @@
+/**CFile****************************************************************
+
+  FileName    [cecCec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Integrated combinatinal equivalence checker.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecCec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the input pattern with the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
+{
+    int i;
+    assert( p->pCexComb == NULL );
+    p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, 
+        sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p)) );
+    p->pCexComb->iPo = iOut;
+    p->pCexComb->nPis = Gia_ManCiNum(p);
+    p->pCexComb->nBits = Gia_ManCiNum(p);
+    for ( i = 0; i < Gia_ManCiNum(p); i++ )
+        if ( pValues[i] )
+            Aig_InfoSetBit( p->pCexComb->pData, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface to the old CEC engine]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose )
+{
+    extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
+    extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
+    Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
+    Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp );
+    int RetValue, iOut, nOuts, clkTotal = clock();
+    Gia_ManStop( pTemp );
+    // run CEC on this miter
+    RetValue = Fra_FraigCec( &pMiterCec, 100000, fVerbose );
+    // report the miter
+    if ( RetValue == 1 )
+    {
+        printf( "Networks are equivalent.   " );
+ABC_PRT( "Time", clock() - clkTotal );
+    }
+    else if ( RetValue == 0 )
+    {
+        printf( "Networks are NOT EQUIVALENT.   " );
+ABC_PRT( "Time", clock() - clkTotal );
+        if ( pMiterCec->pData == NULL )
+            printf( "Counter-example is not available.\n" );
+        else
+        {
+            iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts );
+            if ( iOut == -1 )
+                printf( "Counter-example verification has failed.\n" );
+            else 
+            {
+                printf( "Primary output %d has failed in frame %d.\n", iOut );
+                printf( "The counter-example detected %d incorrect outputs.\n", nOuts );
+            }
+            Cec_ManTransformPattern( pMiter, iOut, pMiterCec->pData );
+        }
+    }
+    else
+    {
+        printf( "Networks are UNDECIDED.   " );
+ABC_PRT( "Time", clock() - clkTotal );
+    }
+    fflush( stdout );
+    Aig_ManStop( pMiterCec );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [New CEC engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
+{
+    int fDumpUndecided = 1;
+    Cec_ParFra_t ParsFra, * pParsFra = &ParsFra;
+    Gia_Man_t * pNew;
+    int RetValue, clk = clock();
+    double clkTotal = clock();
+    // sweep for equivalences
+    Cec_ManFraSetDefaultParams( pParsFra );
+    pParsFra->nBTLimit     = pPars->nBTLimit;
+    pParsFra->TimeLimit    = pPars->TimeLimit;
+    pParsFra->fVerbose     = pPars->fVerbose;
+    pParsFra->fCheckMiter  = 1;
+    pParsFra->fFirstStop   = 1;
+    pParsFra->fDoubleOuts  = 1;
+    pNew = Cec_ManSatSweeping( p, pParsFra );
+    if ( pNew == NULL )
+    {
+        if ( !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
+            printf( "Counter-example simulation has failed.\n" );
+        printf( "Networks are NOT EQUIVALENT.  " );
+        ABC_PRT( "Time", clock() - clk );
+        return 0;
+    }
+    if ( Gia_ManAndNum(pNew) == 0 )
+    {
+        printf( "Networks are equivalent.  " );
+        ABC_PRT( "Time", clock() - clk );
+        Gia_ManStop( pNew );
+        return 1;
+    }
+    printf( "Networks are UNDECIDED after the new CEC engine.  " );
+    ABC_PRT( "Time", clock() - clk );
+    if ( fDumpUndecided )
+    {
+        Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
+        printf( "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
+    }
+    if ( pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+    {
+        Gia_ManStop( pNew );
+        return -1;
+    }
+    // call other solver
+    printf( "Calling the old CEC engine.\n" );
+    fflush( stdout );
+    RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose );
+    p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
+    if ( p->pCexComb && !Gia_ManVerifyCounterExample( p, p->pCexComb, 1 ) )
+        printf( "Counter-example simulation has failed.\n" );
+    Gia_ManStop( pNew );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [New CEC engine applied to two circuits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
+{
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    Gia_Man_t * pMiter;
+    int RetValue;
+    Cec_ManCecSetDefaultParams( pPars );
+    pPars->fVerbose = fVerbose;
+    pMiter = Gia_ManMiter( p0, p1, 0, 1, pPars->fVerbose );
+    if ( pMiter == NULL )
+        return -1;
+    RetValue = Cec_ManVerify( pMiter, pPars );
+    p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL;
+    Gia_ManStop( pMiter );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [New CEC engine applied to two circuits.]
+
+  Description [Returns 1 if equivalent, 0 if counter-example, -1 if undecided.
+  Counter-example is returned in the first manager as pAig0->pSeqModel.
+  The format is given in Gia_Cex_t (file "abc\src\aig\gia\gia.h").]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose )
+{
+    Gia_Man_t * p0, * p1, * pTemp;
+    int RetValue;
+
+    p0 = Gia_ManFromAig( pAig0 );
+    p0 = Gia_ManCleanup( pTemp = p0 );
+    Gia_ManStop( pTemp );
+
+    p1 = Gia_ManFromAig( pAig1 );
+    p1 = Gia_ManCleanup( pTemp = p1 );
+    Gia_ManStop( pTemp );
+
+    RetValue = Cec_ManVerifyTwo( p0, p1, fVerbose );
+    pAig0->pSeqModel = p0->pCexComb; p0->pCexComb = NULL;
+    Gia_ManStop( p0 );
+    Gia_ManStop( p1 );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 65fa2e9b..aaa85ffa 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -24,39 +24,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int        Cec_ObjRepr( Cec_ManCsw_t * p, int Id )               { return p->pObjs[Id].iRepr;               }
-static inline void       Cec_ObjSetRepr( Cec_ManCsw_t * p, int Id, int Num )   { p->pObjs[Id].iRepr = Num;                }
-
-static inline int        Cec_ObjProved( Cec_ManCsw_t * p, int Id )             { return p->pObjs[Id].iProved;             }
-static inline void       Cec_ObjSetProved( Cec_ManCsw_t * p, int Id )          { p->pObjs[Id].iProved = 1;                }
-
-static inline int        Cec_ObjFailed( Cec_ManCsw_t * p, int Id )             { return p->pObjs[Id].iFailed;             }
-static inline void       Cec_ObjSetFailed( Cec_ManCsw_t * p, int Id )          { p->pObjs[Id].iFailed = 1;                }
-
-static inline int        Cec_ObjNext( Cec_ManCsw_t * p, int Id )               { return p->pObjs[Id].iNext;               }
-static inline void       Cec_ObjSetNext( Cec_ManCsw_t * p, int Id, int Num )   { p->pObjs[Id].iNext = Num;                }
-
-static inline unsigned   Cec_ObjSim( Cec_ManCsw_t * p, int Id )                { return p->pObjs[Id].SimNum;              }
-static inline unsigned * Cec_ObjSimP1( Cec_ManCsw_t * p, int Id )              { return &p->pObjs[Id].SimNum;             }
-static inline unsigned * Cec_ObjSimP( Cec_ManCsw_t * p, int Id )               { return p->pMems + Cec_ObjSim(p, Id) + 1; }
-static inline void       Cec_ObjSetSim( Cec_ManCsw_t * p, int Id, unsigned n ) { p->pObjs[Id].SimNum = n;                 }
-
-static inline int        Cec_ObjIsConst( Cec_ManCsw_t * p, int Id )            { return Cec_ObjRepr(p, Id) == 0;                           }
-static inline int        Cec_ObjIsHead( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) > 0;  }
-static inline int        Cec_ObjIsNone( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) < 0 && Cec_ObjNext(p, Id) == 0; }
-static inline int        Cec_ObjIsTail( Cec_ManCsw_t * p, int Id )             { return Cec_ObjRepr(p, Id) > 0 && Cec_ObjNext(p, Id) == 0; }
-static inline int        Cec_ObjIsClass( Cec_ManCsw_t * p, int Id )            { return Cec_ObjRepr(p, Id) > 0 || Cec_ObjNext(p, Id) > 0;  }
-
-#define Cec_ManForEachObj( p, i )                              \
-    for ( i = 0; i < Gia_ManObjNum(p->pAig); i++ )
-#define Cec_ManForEachObj1( p, i )                             \
-    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
-#define Cec_ManForEachClass( p, i )                            \
-    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ ) if ( !Cec_ObjIsHead(p, i) ) {} else
-#define Cec_ClassForEachObj( p, i, iObj )                      \
-    for ( assert(Cec_ObjIsHead(p, i)), iObj = i; iObj; iObj = Cec_ObjNext(p, iObj) )
-#define Cec_ClassForEachObj1( p, i, iObj )                     \
-    for ( assert(Cec_ObjIsHead(p, i)), iObj = Cec_ObjNext(p, i); iObj; iObj = Cec_ObjNext(p, iObj) )
+static inline unsigned * Cec_ObjSim( Cec_ManSim_t * p, int Id )            { return p->pMems + p->pSimInfo[Id] + 1;   }
+static inline void       Cec_ObjSetSim( Cec_ManSim_t * p, int Id, int n )  { p->pSimInfo[Id] = n;                     }
+
+static inline float      Cec_MemUsage( Cec_ManSim_t * p )                  { return 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20);   }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -64,30 +35,7 @@ static inline int        Cec_ObjIsClass( Cec_ManCsw_t * p, int Id )            {
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the set of representatives.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p )
-{
-    int i, * pReprs = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
-    for ( i = 1; i < Gia_ManObjNum(p->pAig); i++ )
-        if ( Cec_ObjProved(p, i) )
-        {
-            assert( Cec_ObjRepr(p, i) >= 0 );
-            pReprs[i] = Cec_ObjRepr(p, i);
-        }
-    return pReprs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
+  Synopsis    [Compares simulation info of one node with constant 0.]
 
   Description []
                
@@ -96,250 +44,28 @@ int * Cec_ManCswDeriveReprs( Cec_ManCsw_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManCswDupWithClasses( Cec_ManCsw_t * p )
+int Cec_ManSimCompareConst( unsigned * p, int nWords )
 {
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj, * pRepr;
-    int iRes0, iRes1, iRepr, iNode;
-    int i, fCompl, * piCopies;
-    Vec_IntClear( p->vXorNodes );
-    Gia_ManLevelNum( p->pAig );
-    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
-    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
-    Gia_ManHashAlloc( pNew );
-    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
-    piCopies[0] = 0;
-    Gia_ManForEachObj1( p->pAig, pObj, i )
-    {
-        if ( Gia_ObjIsCi(pObj) ) 
-        {
-            piCopies[i] = Gia_ManAppendCi( pNew );
-            continue;
-        }
-        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
-        if ( Gia_ObjIsCo(pObj) ) 
-        {
-            Gia_ManAppendCo( pNew, iRes0 );
-            continue;
-        }
-        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
-        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
-        if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
-            continue;
-        assert( Cec_ObjRepr(p, i) < i );
-        iRepr = piCopies[Cec_ObjRepr(p, i)];
-        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
-            continue;
-        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
-        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
-        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
-    }
-    ABC_FREE( piCopies );
-    Gia_ManHashStop( pNew );
-    Gia_ManSetRegNum( pNew, 0 );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Cec_ManCswSpecReduction( Cec_ManCsw_t * p )
-{
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj, * pRepr;
-    int iRes0, iRes1, iRepr, iNode, iMiter;
-    int i, fCompl, * piCopies, * pDepths;
-    Vec_IntClear( p->vXorNodes );
-//    Gia_ManLevelNum( p->pAig );
-    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
-    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
-    Gia_ManHashAlloc( pNew );
-    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
-    pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
-    piCopies[0] = 0;
-    Gia_ManForEachObj1( p->pAig, pObj, i )
-    {
-        if ( Gia_ObjIsCi(pObj) ) 
-        {
-            piCopies[i] = Gia_ManAppendCi( pNew );
-            continue;
-        }
-        if ( Gia_ObjIsCo(pObj) ) 
-            continue;
-        if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
-             piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
-             continue;
-        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
-        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
-        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
-        pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
-        if ( Cec_ObjRepr(p, i) < 0 || Cec_ObjFailed(p, i) )
-            continue;
-        assert( Cec_ObjRepr(p, i) < i );
-        iRepr = piCopies[Cec_ObjRepr(p, i)];
-        if ( iRepr == -1 )
-            continue;
-        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
-            continue;
-        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
-        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
-        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
-        if ( Cec_ObjProved(p, i) )
-            continue;
-//        if ( p->pPars->nLevelMax && 
-//            (Gia_ObjLevel(p->pAig, pObj)  > p->pPars->nLevelMax || 
-//             Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
-//            continue;
-        // produce speculative miter
-        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
-        Gia_ManAppendCo( pNew, iMiter );
-        Vec_IntPush( p->vXorNodes, Cec_ObjRepr(p, i) );
-        Vec_IntPush( p->vXorNodes, i );
-        // add to the depth of this node
-        pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Cec_ObjRepr(p, i)] );
-        if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
-            piCopies[i] = -1;
-    }
-    ABC_FREE( piCopies );
-    ABC_FREE( pDepths );
-    Gia_ManHashStop( pNew );
-    Gia_ManSetRegNum( pNew, 0 );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Gia_Man_t * Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p )
-{
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj, * pRepr;
-    int iRes0, iRes1, iRepr, iNode, iMiter;
-    int i, fCompl, * piCopies;
-    Vec_IntClear( p->vXorNodes );
-    Gia_ManLevelNum( p->pAig );
-    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
-    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
-    Gia_ManHashAlloc( pNew );
-    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
-    piCopies[0] = 0;
-    Gia_ManForEachObj1( p->pAig, pObj, i )
+    int w;
+    if ( p[0] & 1 )
     {
-        if ( Gia_ObjIsCi(pObj) ) 
-        {
-            piCopies[i] = Gia_ManAppendCi( pNew );
-            continue;
-        }
-        if ( Gia_ObjIsCo(pObj) ) 
-            continue;
-        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
-        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
-        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
-        if ( Cec_ObjRepr(p, i) < 0 || !Cec_ObjProved(p, i) )
-            continue;
-        assert( Cec_ObjRepr(p, i) < i );
-        iRepr = piCopies[Cec_ObjRepr(p, i)];
-        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
-            continue;
-        pRepr = Gia_ManObj( p->pAig, Cec_ObjRepr(p, i) );
-        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
-        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
-        // add speculative miter
-        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
-        Gia_ManAppendCo( pNew, iMiter );
+        for ( w = 0; w < nWords; w++ )
+            if ( p[w] != ~0 )
+                return 0;
+        return 1;
     }
-    ABC_FREE( piCopies );
-    Gia_ManHashStop( pNew );
-    Gia_ManSetRegNum( pNew, 0 );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManCswCountOne( Cec_ManCsw_t * p, int i )
-{
-    int Ent, nLits = 1;
-    Cec_ClassForEachObj1( p, i, Ent )
+    else
     {
-        assert( Cec_ObjRepr(p, Ent) == i );
-        nLits++;
+        for ( w = 0; w < nWords; w++ )
+            if ( p[w] != 0 )
+                return 0;
+        return 1;
     }
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManCswCountLitsAll( Cec_ManCsw_t * p )
-{
-    int i, nLits = 0;
-    Cec_ManForEachObj( p, i )
-        nLits += (Cec_ObjRepr(p, i) >= 0);
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter )
-{
-    int Ent;
-    printf( "Class %4d :  Num = %2d  {", Counter, Cec_ManCswCountOne(p, i) );
-    Cec_ClassForEachObj( p, i, Ent )
-        printf(" %d", Ent );
-    printf( " }\n" );
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Compares simulation info of two nodes.]
 
   Description []
                
@@ -348,32 +74,28 @@ void Cec_ManCswPrintOne( Cec_ManCsw_t * p, int i, int Counter )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose )
+int Cec_ManSimCompareEqual( unsigned * p0, unsigned * p1, int nWords )
 {
-    int i, Counter = 0, Counter1 = 0, CounterX = 0, nLits;
-    Cec_ManForEachObj1( p, i )
+    int w;
+    if ( (p0[0] & 1) == (p1[0] & 1) )
     {
-        if ( Cec_ObjIsHead(p, i) )
-            Counter++;
-        else if ( Cec_ObjIsConst(p, i) )
-            Counter1++;
-        else if ( Cec_ObjIsNone(p, i) )
-            CounterX++;
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != p1[w] )
+                return 0;
+        return 1;
     }
-    nLits = Cec_ManCswCountLitsAll( p );
-    printf( "Class =%7d. Const =%7d. Unsed =%7d. Lits =%8d. All =%8d. Mem = %5.2f Mb\n", 
-        Counter, Counter1, CounterX, nLits-Counter1, nLits, 1.0*p->nMemsMax*(p->pPars->nWords+1)/(1<<20) );
-    if ( fVerbose )
+    else
     {
-        Counter = 0;
-        Cec_ManForEachClass( p, i )
-            Cec_ManCswPrintOne( p, i, ++Counter );
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != ~p1[w] )
+                return 0;
+        return 1;
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns the number of the first non-equal bit.]
 
   Description []
                
@@ -382,28 +104,28 @@ void Cec_ManCswPrintClasses( Cec_ManCsw_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords )
+int Cec_ManSimCompareConstFirstBit( unsigned * p, int nWords )
 {
     int w;
-    if ( (p0[0] & 1) == (p1[0] & 1) )
+    if ( p[0] & 1 )
     {
         for ( w = 0; w < nWords; w++ )
-            if ( p0[w] != p1[w] )
-                return 0;
-        return 1;
+            if ( p[w] != ~0 )
+                return 32*w + Aig_WordFindFirstBit( ~p[w] );
+        return -1;
     }
     else
     {
         for ( w = 0; w < nWords; w++ )
-            if ( p0[w] != ~p1[w] )
-                return 0;
-        return 1;
+            if ( p[w] != 0 )
+                return 32*w + Aig_WordFindFirstBit( p[w] );
+        return -1;
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Compares simulation info of two nodes.]
 
   Description []
                
@@ -412,28 +134,28 @@ int Cec_ManCswCompareEqual( unsigned * p0, unsigned * p1, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswCompareConst( unsigned * p, int nWords )
+int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
 {
     int w;
-    if ( p[0] & 1 )
+    if ( (p0[0] & 1) == (p1[0] & 1) )
     {
         for ( w = 0; w < nWords; w++ )
-            if ( p[w] != ~0 )
-                return 0;
-        return 1;
+            if ( p0[w] != p1[w] )
+                return 32*w + Aig_WordFindFirstBit( p0[w] ^ p1[w] );
+        return -1;
     }
     else
     {
         for ( w = 0; w < nWords; w++ )
-            if ( p[w] != 0 )
-                return 0;
-        return 1;
+            if ( p0[w] != ~p1[w] )
+                return 32*w + Aig_WordFindFirstBit( p0[w] ^ ~p1[w] );
+        return -1;
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Creates equivalence class.]
 
   Description []
                
@@ -442,31 +164,31 @@ int Cec_ManCswCompareConst( unsigned * p, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass )
+void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
 {
-    int Repr = -1, EntPrev = -1, Ent, i;
+    int Repr = GIA_VOID, EntPrev = -1, Ent, i;
     assert( Vec_IntSize(vClass) > 0 );
     Vec_IntForEachEntry( vClass, Ent, i )
     {
         if ( i == 0 )
         {
             Repr = Ent;
-            Cec_ObjSetRepr( p, Ent, -1 );
+            Gia_ObjSetRepr( p, Ent, GIA_VOID );
             EntPrev = Ent;
         }
         else
         {
-            Cec_ObjSetRepr( p, Ent, Repr );
-            Cec_ObjSetNext( p, EntPrev, Ent );
+            Gia_ObjSetRepr( p, Ent, Repr );
+            Gia_ObjSetNext( p, EntPrev, Ent );
             EntPrev = Ent;
         }
     }
-    Cec_ObjSetNext( p, EntPrev, 0 );
+    Gia_ObjSetNext( p, EntPrev, 0 );
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Refines one equivalence class.]
 
   Description []
                
@@ -475,34 +197,34 @@ void Cec_ManCswClassCreate( Cec_ManCsw_t * p, Vec_Int_t * vClass )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst )
+int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
 {
     unsigned * pSim0, * pSim1;
     int Ent;
     Vec_IntClear( p->vClassOld );
     Vec_IntClear( p->vClassNew );
     Vec_IntPush( p->vClassOld, i );
-    pSim0 = fFirst? Cec_ObjSimP1(p, i) : Cec_ObjSimP(p, i);
-    Cec_ClassForEachObj1( p, i, Ent )
+    pSim0 = Cec_ObjSim(p, i);
+    Gia_ClassForEachObj1( p->pAig, i, Ent )
     {
-        pSim1 = fFirst? Cec_ObjSimP1(p, Ent) : Cec_ObjSimP(p, Ent);
-        if ( Cec_ManCswCompareEqual( pSim0, pSim1, p->nWords ) )
+        pSim1 = Cec_ObjSim(p, Ent);
+        if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
             Vec_IntPush( p->vClassOld, Ent );
         else
             Vec_IntPush( p->vClassNew, Ent );
     }
     if ( Vec_IntSize( p->vClassNew ) == 0 )
         return 0;
-    Cec_ManCswClassCreate( p, p->vClassOld );
-    Cec_ManCswClassCreate( p, p->vClassNew );
+    Cec_ManSimClassCreate( p->pAig, p->vClassOld );
+    Cec_ManSimClassCreate( p->pAig, p->vClassNew );
     if ( Vec_IntSize(p->vClassNew) > 1 )
-        return 1 + Cec_ManCswClassRefineOne( p, Vec_IntEntry(p->vClassNew,0), fFirst );
+        return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
     return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Computes hash key of the simuation info.]
 
   Description []
                
@@ -511,7 +233,7 @@ int Cec_ManCswClassRefineOne( Cec_ManCsw_t * p, int i, int fFirst )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
+int Cec_ManSimHashKey( unsigned * pSim, int nWords, int nTableSize )
 {
     static int s_Primes[16] = { 
         1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
@@ -530,7 +252,7 @@ int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Resets pointers to the simulation memory.]
 
   Description []
                
@@ -539,90 +261,7 @@ int Cec_ManCswHashKey( unsigned * pSim, int nWords, int nTableSize )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswClassesCreate( Cec_ManCsw_t * p )
-{
-    int * pTable, nTableSize, i, Key;
-    p->nWords = 1;
-    nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p->pAig) / 10 );
-    pTable = ABC_CALLOC( int, nTableSize );
-    Cec_ObjSetRepr( p, 0, -1 );
-    Cec_ManForEachObj1( p, i )
-    {
-        if ( Gia_ObjIsCo(Gia_ManObj(p->pAig, i)) ) 
-        {
-            Cec_ObjSetRepr( p, i, -1 );
-            continue;
-        }
-        if ( Cec_ManCswCompareConst( Cec_ObjSimP1(p, i), p->nWords ) )
-        {
-            Cec_ObjSetRepr( p, i, 0 );
-            continue;
-        }
-        Key = Cec_ManCswHashKey( Cec_ObjSimP1(p, i), p->nWords, nTableSize );
-        if ( pTable[Key] == 0 )
-            Cec_ObjSetRepr( p, i, -1 );
-        else
-        {
-            Cec_ObjSetNext( p, pTable[Key], i );
-            Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
-            if ( Cec_ObjRepr(p, i) == -1 )
-                Cec_ObjSetRepr( p, i, pTable[Key] );
-        }
-        pTable[Key] = i;
-    }
-    ABC_FREE( pTable );
-    if ( p->pPars->fVeryVerbose )
-    Cec_ManCswPrintClasses( p, 0 );
-    // refine classes
-    Cec_ManForEachClass( p, i )
-        Cec_ManCswClassRefineOne( p, i, 1 );
-    // clean memory
-    Cec_ManForEachObj( p, i )
-        Cec_ObjSetSim( p, i, 0 );
-    if ( p->pPars->fVeryVerbose )
-    Cec_ManCswPrintClasses( p, 0 );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManCswSimulateSimple( Cec_ManCsw_t * p )
-{
-    Gia_Obj_t * pObj;
-    unsigned Res0, Res1;
-    int i;
-    Gia_ManForEachCi( p->pAig, pObj, i )
-        Cec_ObjSetSim( p, i, Aig_ManRandom(0) );
-    Gia_ManForEachAnd( p->pAig, pObj, i )
-    {
-        Res0 = Cec_ObjSim( p, Gia_ObjFaninId0(pObj, i) );
-        Res1 = Cec_ObjSim( p, Gia_ObjFaninId1(pObj, i) );
-        Cec_ObjSetSim( p, i, (Gia_ObjFaninC0(pObj)? ~Res0: Res0) &
-                             (Gia_ObjFaninC1(pObj)? ~Res1: Res1) );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [References simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
+void Cec_ManSimMemRelink( Cec_ManSim_t * p )
 {
     unsigned * pPlace, Ent;
     pPlace = &p->MemFree;
@@ -634,6 +273,7 @@ void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
         pPlace = p->pMems + Ent;
     }
     *pPlace = 0;
+    p->nWordsOld = p->nWords;
 }
 
 /**Function*************************************************************
@@ -647,10 +287,10 @@ void Cec_ManCswSimMemRelink( Cec_ManCsw_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
+unsigned * Cec_ManSimSimRef( Cec_ManSim_t * p, int i )
 {
     unsigned * pSim;
-    assert( p->pObjs[i].SimNum == 0 );
+    assert( p->pSimInfo[i] == 0 );
     if ( p->MemFree == 0 )
     {
         if ( p->nWordsAlloc == 0 )
@@ -661,9 +301,9 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
         }
         p->nWordsAlloc *= 2;
         p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
-        Cec_ManCswSimMemRelink( p );
+        Cec_ManSimMemRelink( p );
     }
-    p->pObjs[i].SimNum = p->MemFree;
+    p->pSimInfo[i] = p->MemFree;
     pSim = p->pMems + p->MemFree;
     p->MemFree = pSim[0];
     pSim[0] = Gia_ObjValue( Gia_ManObj(p->pAig, i) );
@@ -675,7 +315,7 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
 
 /**Function*************************************************************
 
-  Synopsis    [Dereference simulaton info.]
+  Synopsis    [Dereferences simulaton info.]
 
   Description []
                
@@ -684,16 +324,16 @@ unsigned * Cec_ManCswSimRef( Cec_ManCsw_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
+unsigned * Cec_ManSimSimDeref( Cec_ManSim_t * p, int i )
 {
     unsigned * pSim;
-    assert( p->pObjs[i].SimNum > 0 );
-    pSim = p->pMems + p->pObjs[i].SimNum;
+    assert( p->pSimInfo[i] > 0 );
+    pSim = p->pMems + p->pSimInfo[i];
     if ( --pSim[0] == 0 )
     {
         pSim[0] = p->MemFree;
-        p->MemFree = p->pObjs[i].SimNum;
-        p->pObjs[i].SimNum = 0;
+        p->MemFree = p->pSimInfo[i];
+        p->pSimInfo[i] = 0;
         p->nMems--;
     }
     return pSim;
@@ -701,7 +341,7 @@ unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Refines nodes belonging to candidate constant class.]
 
   Description []
                
@@ -710,52 +350,145 @@ unsigned * Cec_ManCswSimDeref( Cec_ManCsw_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined )
+void Cec_ManSimProcessRefined( Cec_ManSim_t * p, Vec_Int_t * vRefined )
 {
     unsigned * pSim;
     int * pTable, nTableSize, i, k, Key;
     if ( Vec_IntSize(vRefined) == 0 )
         return;
-    nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
+    nTableSize = Aig_PrimeCudd( 100 + Vec_IntSize(vRefined) / 3 );
     pTable = ABC_CALLOC( int, nTableSize );
     Vec_IntForEachEntry( vRefined, i, k )
     {
-        if ( i == 7720 )
-        {
-            int s = 0;
-        }
-        pSim = Cec_ObjSimP( p, i );
-        assert( !Cec_ManCswCompareConst( pSim, p->nWords ) );
-        Key = Cec_ManCswHashKey( pSim, p->nWords, nTableSize );
+        pSim = Cec_ObjSim( p, i );
+        assert( !Cec_ManSimCompareConst( pSim, p->nWords ) );
+        Key = Cec_ManSimHashKey( pSim, p->nWords, nTableSize );
         if ( pTable[Key] == 0 )
         {
-            assert( Cec_ObjRepr(p, i) == 0 );
-            assert( Cec_ObjNext(p, i) == 0 );
-            Cec_ObjSetRepr( p, i, -1 );
+            assert( Gia_ObjRepr(p->pAig, i) == 0 );
+            assert( Gia_ObjNext(p->pAig, i) == 0 );
+            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
         }
         else
         {
-            Cec_ObjSetNext( p, pTable[Key], i );
-            Cec_ObjSetRepr( p, i, Cec_ObjRepr(p, pTable[Key]) );
-            if ( Cec_ObjRepr(p, i) == -1 )
-                Cec_ObjSetRepr( p, i, pTable[Key] );
-            assert( Cec_ObjRepr(p, i) > 0 );
+            Gia_ObjSetNext( p->pAig, pTable[Key], i );
+            Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
+            if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
+                Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
+            assert( Gia_ObjRepr(p->pAig, i) > 0 );
         }
         pTable[Key] = i;
     }
     Vec_IntForEachEntry( vRefined, i, k )
     {
-        if ( Cec_ObjIsHead( p, i ) )
-            Cec_ManCswClassRefineOne( p, i, 0 );
+        if ( Gia_ObjIsHead( p->pAig, i ) )
+            Cec_ManSimClassRefineOne( p, i );
     }
     Vec_IntForEachEntry( vRefined, i, k )
-        Cec_ManCswSimDeref( p, i );
+        Cec_ManSimSimDeref( p, i );
     ABC_FREE( pTable );
 }
 
 
 /**Function*************************************************************
 
+  Synopsis    [Saves the input pattern with the given number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
+{
+    unsigned * pInfo;
+    int i;
+    assert( p->pCexComb == NULL );
+    assert( iPat >= 0 && iPat < 32 * p->nWords );
+    p->pCexComb = (Gia_Cex_t *)ABC_CALLOC( char, 
+        sizeof(Gia_Cex_t) + sizeof(unsigned) * Aig_BitWordNum(Gia_ManCiNum(p->pAig)) );
+    p->pCexComb->iPo = p->iOut;
+    p->pCexComb->nPis = Gia_ManCiNum(p->pAig);
+    p->pCexComb->nBits = Gia_ManCiNum(p->pAig);
+    for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+    {
+        pInfo = Vec_PtrEntry( p->vCiSimInfo, i );
+        if ( Aig_InfoHasBit( pInfo, iPat ) )
+            Aig_InfoSetBit( p->pCexComb->pData, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if computation should stop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
+{
+    unsigned * pInfo, * pInfo2;
+    int i;
+    if ( p->vCoSimInfo == NULL )
+        return 0;
+    // compare outputs with 0
+    if ( p->pPars->fDoubleOuts )
+    {
+        assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
+        for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+        {
+            pInfo  = Vec_PtrEntry( p->vCoSimInfo, i );
+            pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i );
+            if ( !Cec_ManSimCompareEqual( pInfo, pInfo2, p->nWords ) )
+            {
+                if ( p->iOut == -1 )
+                {
+                    p->iOut = i/2;
+                    Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
+                }
+                if ( p->pCexes == NULL )
+                    p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 );
+                if ( p->pCexes[i/2] == NULL )
+                {
+                    p->nOuts++;
+                    p->pCexes[i/2] = (void *)1;
+                }
+            }
+        }
+    }
+    else
+    {
+        for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+        {
+            pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
+            if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
+            {
+                if ( p->iOut == -1 )
+                {
+                    p->iOut = i;
+                    Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
+                }
+                if ( p->pCexes == NULL )
+                    p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) );
+                if ( p->pCexes[i] == NULL )
+                {
+                    p->nOuts++;
+                    p->pCexes[i] = (void *)1;
+                }
+            }
+        }
+    }
+    return p->pCexes != NULL && p->pPars->fFirstStop;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Simulates one round.]
 
   Description [Returns the number of PO entry if failed; 0 otherwise.]
@@ -765,17 +498,20 @@ void Cec_ManCswProcessRefined( Cec_ManCsw_t * p, Vec_Int_t * vRefined )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos, int iSeries, int fRandomize )
+int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
 {
-    static int nCountRand = 0;
     Gia_Obj_t * pObj;
     unsigned * pRes0, * pRes1, * pRes;
     int i, k, w, Ent, iCiId = 0, iCoId = 0;
+    // prepare internal storage
+    if ( p->nWordsOld != p->nWords )
+        Cec_ManSimMemRelink( p );
     p->nMemsMax = 0;
+    // simulate nodes
     Vec_IntClear( p->vRefinedC );
     if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
     {
-        pRes = Cec_ManCswSimRef( p, 0 );
+        pRes = Cec_ManSimSimRef( p, 0 );
         for ( w = 1; w <= p->nWords; w++ )
             pRes[w] = 0;
     }
@@ -788,16 +524,12 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
                 iCiId++;
                 continue;
             }
-            pRes = Cec_ManCswSimRef( p, i );
+            pRes = Cec_ManSimSimRef( p, i );
             if ( vInfoCis ) 
             {
                 pRes0 = Vec_PtrEntry( vInfoCis, iCiId++ );
                 for ( w = 1; w <= p->nWords; w++ )
-                {
-                    pRes[w] = pRes0[iSeries*p->nWords+w-1];
-                    if ( fRandomize )
-                        pRes[w] ^= (1 << (nCountRand++ & 0x1f));
-                }
+                    pRes[w] = pRes0[w-1];
             }
             else
             {
@@ -810,7 +542,7 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
         }
         if ( Gia_ObjIsCo(pObj) ) // co always has non-zero 1st fanin and zero 2nd fanin
         {
-            pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
+            pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
             if ( vInfoCos )
             {
                 pRes = Vec_PtrEntry( vInfoCos, iCoId++ );
@@ -824,9 +556,9 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
             continue;
         }
         assert( Gia_ObjValue(pObj) );
-        pRes  = Cec_ManCswSimRef( p, i );
-        pRes0 = Cec_ManCswSimDeref( p, Gia_ObjFaninId0(pObj,i) );
-        pRes1 = Cec_ManCswSimDeref( p, Gia_ObjFaninId1(pObj,i) );
+        pRes  = Cec_ManSimSimRef( p, i );
+        pRes0 = Cec_ManSimSimDeref( p, Gia_ObjFaninId0(pObj,i) );
+        pRes1 = Cec_ManSimSimDeref( p, Gia_ObjFaninId1(pObj,i) );
         if ( Gia_ObjFaninC0(pObj) )
         {
             if ( Gia_ObjFaninC1(pObj) )
@@ -847,47 +579,50 @@ void Cec_ManCswSimulateRound( Cec_ManCsw_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t
         }
 references:
         // if this node is candidate constant, collect it
-        if ( Cec_ObjIsConst(p, i) && !Cec_ManCswCompareConst(pRes + 1, p->nWords) )
+        if ( Gia_ObjIsConst(p->pAig, i) && !Cec_ManSimCompareConst(pRes + 1, p->nWords) )
         {
             pRes[0]++;
             Vec_IntPush( p->vRefinedC, i );
         }
         // if the node belongs to a class, save it
-        if ( Cec_ObjIsClass(p, i) )
+        if ( Gia_ObjIsClass(p->pAig, i) )
             pRes[0]++;
         // if this is the last node of the class, process it
-        if ( Cec_ObjIsTail(p, i) )
+        if ( Gia_ObjIsTail(p->pAig, i) )
         {
             Vec_IntClear( p->vClassTemp );
-            Cec_ClassForEachObj( p, Cec_ObjRepr(p, i), Ent )
+            Gia_ClassForEachObj( p->pAig, Gia_ObjRepr(p->pAig, i), Ent )
                 Vec_IntPush( p->vClassTemp, Ent );
-            Cec_ManCswClassRefineOne( p, Cec_ObjRepr(p, i), 0 );
+            Cec_ManSimClassRefineOne( p, Gia_ObjRepr(p->pAig, i) );
             Vec_IntForEachEntry( p->vClassTemp, Ent, k )
-                Cec_ManCswSimDeref( p, Ent );
+                Cec_ManSimSimDeref( p, Ent );
         }
     }
     if ( Vec_IntSize(p->vRefinedC) > 0 )
-        Cec_ManCswProcessRefined( p, p->vRefinedC );
+        Cec_ManSimProcessRefined( p, p->vRefinedC );
     assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
     assert( vInfoCos == NULL || iCoId == Gia_ManCoNum(p->pAig) );
     assert( p->nMems == 1 );
+    if ( p->nMems != 1 )
+        printf( "Cec_ManSimSimulateRound(): Memory management error!\n" );
     if ( p->pPars->fVeryVerbose )
-        Cec_ManCswPrintClasses( p, 0 );
+        Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
 /*
-    if ( p->nMems > 1 )
-    {
+    if ( p->nMems > 1 ) {
         for ( i = 1; i < p->nObjs; i++ )
-        if ( p->pSims[i] )
-        {
+        if ( p->pSims[i] ) {
             int x = 0;
         }
     }
 */
+    return Cec_ManSimAnalyzeOutputs( p );
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Creates simulation info for this round.]
 
   Description []
                
@@ -896,28 +631,41 @@ references:
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p )
+void Cec_ManSimCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos )
 {
-    int i;
-    Gia_ManSetRefs( p->pAig );
-    Cec_ManCswSimulateSimple( p );
-    Cec_ManCswClassesCreate( p );
-    for ( i = 0; i < p->pPars->nRounds; i++ )
+    unsigned * pRes0, * pRes1;
+    int i, w;
+    if ( p->pPars->fSeqSimulate && Gia_ManRegNum(p->pAig) > 0 )
     {
-        p->nWords = i + 1;
-        Cec_ManCswSimMemRelink( p );
-        Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
+        assert( vInfoCis && vInfoCos );
+        for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+        {
+            pRes0 = Vec_PtrEntry( vInfoCis, i );
+            for ( w = 0; w < p->nWords; w++ )
+                pRes0[w] = Aig_ManRandom( 0 );
+        }
+        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+        {
+            pRes0 = Vec_PtrEntry( vInfoCis, Gia_ManPiNum(p->pAig) + i );
+            pRes1 = Vec_PtrEntry( vInfoCos, Gia_ManPoNum(p->pAig) + i );
+            for ( w = 0; w < p->nWords; w++ )
+                pRes0[w] = pRes1[w];
+        }
+    }
+    else 
+    {
+        for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+        {
+            pRes0 = Vec_PtrEntry( vInfoCis, i );
+            for ( w = 0; w < p->nWords; w++ )
+                pRes0[w] = Aig_ManRandom( 0 );
+        }
     }
-    p->nWords = p->pPars->nWords;
-    Cec_ManCswSimMemRelink( p );
-    for ( i = 0; i < p->pPars->nRounds; i++ )
-        Cec_ManCswSimulateRound( p, NULL, NULL, 0, 0 );
-    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns 1 if the bug is found.]
 
   Description []
                
@@ -926,21 +674,37 @@ int Cec_ManCswClassesPrepare( Cec_ManCsw_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj )
+int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
 {
-    int Result;
-    if ( pObj->fMark0 )
-        return 1;
-    if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
-        return 0;
-    Result = (Cec_ManCswClassesUpdate_rec( Gia_ObjFanin0(pObj) ) |
-              Cec_ManCswClassesUpdate_rec( Gia_ObjFanin1(pObj) ));
-    return pObj->fMark0 = Result;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pAig->pReprs == NULL );
+    // allocate representation
+    p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
+    p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+    Gia_ManForEachObj( p->pAig, pObj, i )
+        Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj)) ? 0 : GIA_VOID );
+    // perform simulation
+    Gia_ManSetRefs( p->pAig );
+    p->nWords = 1;
+    do {
+        if ( p->pPars->fVerbose )
+            Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+        for ( i = 0; i < 4; i++ )
+        {
+            Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+            if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+                return 1;
+        }
+        p->nWords = 2 * p->nWords + 1;
+    }
+    while ( p->nWords <= p->pPars->nWords );
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns 1 if the bug is found.]
 
   Description []
                
@@ -949,100 +713,23 @@ int Cec_ManCswClassesUpdate_rec( Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew )
+int Cec_ManSimClassesRefine( Cec_ManSim_t * p )
 {
-    Vec_Ptr_t * vInfo;
-    Gia_Obj_t * pObj, * pObjOld, * pReprOld;
-    int i, k, iRepr, iNode;
-    vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), p->pPars->nWords );
-    if ( vInfo != NULL )
-    {
-        for ( i = 0; i < pPat->nSeries; i++ )
-            Cec_ManCswSimulateRound( p, vInfo, NULL, i, 0 );
-        Vec_PtrFree( vInfo );
-    }
-    assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
-    // mark the transitive fanout of failed nodes
-    if ( p->pPars->nDepthMax != 1 )
+    int i;
+    Gia_ManSetRefs( p->pAig );
+    p->nWords = p->pPars->nWords;
+    for ( i = 0; i < p->pPars->nRounds; i++ )
     {
-        Gia_ManCleanMark0( p->pAig );
-        Gia_ManCleanMark1( p->pAig );
-        Gia_ManForEachCo( pNew, pObj, k )
-        {
-            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
-            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
-            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
-                continue;
-//            Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
-            Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
-        }
-        // mark the nodes reachable through the failed nodes
-        Gia_ManForEachAnd( p->pAig, pObjOld, k )
-            pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
-        // unmark the disproved nodes
-        Gia_ManForEachCo( pNew, pObj, k )
-        {
-            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
-            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
-            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
-                continue; 
-            pObjOld = Gia_ManObj(p->pAig, iNode);
-            assert( pObjOld->fMark0 == 1 );
-            if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
-                pObjOld->fMark1 = 1;
-        }
-        // clean marks
-        Gia_ManForEachAnd( p->pAig, pObjOld, k )
-            if ( pObjOld->fMark1 )
-            {
-                pObjOld->fMark0 = 0;
-                pObjOld->fMark1 = 0;
-            }
+        if ( (i % 4) == 0 && p->pPars->fVerbose )
+            Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+        Cec_ManSimCreateInfo( p, p->vCiSimInfo, p->vCoSimInfo );
+        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+            return 1;
     }
-    // set the results
-    Gia_ManForEachCo( pNew, pObj, k )
-    {
-        iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
-        iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
-        pReprOld = Gia_ManObj(p->pAig, iRepr);
-        pObjOld = Gia_ManObj(p->pAig, iNode);
-        if ( pObj->fMark1 )
-        { // proved
-            assert( pObj->fMark0 == 0 );
-            assert( !Cec_ObjProved(p, iNode) );
-            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
-//            if ( pObjOld->fMark0 == 0 )
-            {
-                assert( iRepr == Cec_ObjRepr(p, iNode) );
-                Cec_ObjSetProved( p, iNode );
-                p->nAllProved++;
-            }
-        }
-        else if ( pObj->fMark0 )
-        { // disproved
-            assert( pObj->fMark1 == 0 );
-            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
-//            if ( pObjOld->fMark0 == 0 )
-            {
-                if ( iRepr == Cec_ObjRepr(p, iNode) )
-                    printf( "Cec_ManCswClassesUpdate(): Error! Node is not refined!\n" );
-                p->nAllDisproved++;
-            }
-        }
-        else
-        { // failed
-            assert( pObj->fMark0 == 0 );
-            assert( pObj->fMark1 == 0 );
-            assert( !Cec_ObjFailed(p, iNode) );
-            assert( !Cec_ObjProved(p, iNode) );
-            Cec_ObjSetFailed( p, iNode );
-            p->nAllFailed++;
-        }
-    } 
+    if ( p->pPars->fVerbose )
+        Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
     return 0;
 }
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index ab8fd5cf..e25ddc90 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -44,11 +44,37 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
     memset( p, 0, sizeof(Cec_ParSat_t) );
     p->nBTLimit       =      10;  // conflict limit at a node
     p->nSatVarMax     =    2000;  // the max number of SAT variables
-    p->nCallsRecycle  =     100;  // calls to perform before recycling SAT solver
+    p->nCallsRecycle  =     200;  // calls to perform before recycling SAT solver
     p->fPolarFlip     =       1;  // flops polarity of variables
+    p->fCheckMiter    =       0;  // the circuit is the miter
     p->fFirstStop     =       0;  // stop on the first sat output
-    p->fVerbose       =       1;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
 }  
+
+/**Function************  *************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParSim_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->TimeLimit      =       0;  // the runtime limit in seconds
+    p->fCheckMiter    =       0;  // the circuit is the miter
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fDoubleOuts    =       0;  // miter with separate outputs
+    p->fSeqSimulate   =       0;  // performs sequential simulation
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
+} 
   
 /**Function************  *************************************************
 
@@ -61,19 +87,21 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
+void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
 {
-    memset( p, 0, sizeof(Cec_ParCsw_t) );
-    p->nWords         =      20;  // the number of simulation words
-    p->nRounds        =      20;  // the number of simulation rounds
-    p->nItersMax      =      20;  // the maximum number of iterations of SAT sweeping
-    p->nBTLimit       =   10000;  // conflict limit at a node
-    p->nSatVarMax     =    2000;  // the max number of SAT variables
-    p->nCallsRecycle  =     100;  // calls to perform before recycling SAT solver
+    memset( p, 0, sizeof(Cec_ParFra_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->TimeLimit      =       0;  // the runtime limit in seconds
+    p->nItersMax      =    1000;  // the maximum number of iterations of SAT sweeping
+    p->nBTLimit       =    1000;  // conflict limit at a node
     p->nLevelMax      =       0;  // restriction on the level of nodes to be swept
     p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
     p->fRewriting     =       0;  // enables AIG rewriting
+    p->fCheckMiter    =       0;  // the circuit is the miter
     p->fFirstStop     =       0;  // stop on the first sat output
+    p->fDoubleOuts    =       0;  // miter with separate outputs
+    p->fColorDiff     =       0;  // miter with separate outputs
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
 } 
@@ -92,14 +120,13 @@ void Cec_ManCswSetDefaultParams( Cec_ParCsw_t * p )
 void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
 {
     memset( p, 0, sizeof(Cec_ParCec_t) );
-    p->nIters         =       1;  // iterations of SAT solving/sweeping
-    p->nBTLimitBeg    =       2;  // starting backtrack limit
-    p->nBTlimitMulti  =       8;  // multiple of backtrack limiter
+    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->TimeLimit      =       0;  // the runtime limit in seconds
+    p->fFirstStop     =       0;  // stop on the first sat output
     p->fUseSmartCnf   =       0;  // use smart CNF computation
     p->fRewriting     =       0;  // enables AIG rewriting
-    p->fSatSweeping   =       0;  // enables SAT sweeping
-    p->fFirstStop     =       0;  // stop on the first sat output
-    p->fVerbose       =       1;  // verbose stats
+    p->fVeryVerbose   =       0;  // verbose stats
+    p->fVerbose       =       0;  // verbose stats
 }  
 
 /**Function*************************************************************
@@ -124,6 +151,35 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Core procedure for simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
+{
+    Cec_ManSim_t * pSim;
+    int RetValue, clkTotal = clock();
+    if ( pPars->fSeqSimulate )
+        printf( "Performing sequential simulation of %d frames with %d words.\n", 
+            pPars->nWords, pPars->nRounds );
+    Aig_ManRandom( 1 );
+    pSim = Cec_ManSimStart( pAig, pPars );
+    if ( pAig->pReprs == NULL )
+        RetValue = Cec_ManSimClassesPrepare( pSim );
+    Cec_ManSimClassesRefine( pSim );
+    if ( pPars->fCheckMiter )
+        printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", 
+            pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds );
+    ABC_PRT( "Time", clock() - clkTotal );
+    Cec_ManSimStop( pSim );
+}
 
 /**Function*************************************************************
 
@@ -136,96 +192,185 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParCsw_t * pPars )
+Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
 {
+    int fOutputResult = 0;
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
-    Gia_Man_t * pNew;
-    Cec_ManCsw_t * p;
+    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+    Gia_Man_t * pIni, * pSrm, * pTemp;
+    Cec_ManFra_t * p;
+    Cec_ManSim_t * pSim;
     Cec_ManPat_t * pPat;
-    int i, RetValue, clk, clk2, clkTotal = clock();
+    int i, fTimeOut = 0, nMatches = 0, clk, clk2;
+    double clkTotal = clock();
+
+    // duplicate AIG and transfer equivalence classes
     Aig_ManRandom( 1 );
-    Gia_ManSetPhase( pAig );
-    Gia_ManCleanMark0( pAig );
-    Gia_ManCleanMark1( pAig );
-    p = Cec_ManCswStart( pAig, pPars );
-clk = clock();
-    RetValue = Cec_ManCswClassesPrepare( p );
-p->timeSim += clock() - clk;
+    pIni = Gia_ManDup(pAig);
+    pIni->pReprs = pAig->pReprs; pAig->pReprs = NULL;
+    pIni->pNexts = pAig->pNexts; pAig->pNexts = NULL;
+
+    // prepare the managers
+    // SAT sweeping
+    p = Cec_ManFraStart( pIni, pPars );
+    if ( pPars->fDoubleOuts )
+        pPars->fColorDiff = 1;
+    // simulation
+    Cec_ManSimSetDefaultParams( pParsSim );
+    pParsSim->nWords      = pPars->nWords;
+    pParsSim->nRounds     = pPars->nRounds;
+    pParsSim->fCheckMiter = pPars->fCheckMiter;
+    pParsSim->fFirstStop  = pPars->fFirstStop;
+    pParsSim->fDoubleOuts = pPars->fDoubleOuts;
+    pParsSim->fVerbose    = pPars->fVerbose;
+    pSim = Cec_ManSimStart( p->pAig, pParsSim );
+    pSim->nWords = p->pPars->nWords;
+    // SAT solving
     Cec_ManSatSetDefaultParams( pParsSat );
     pParsSat->nBTLimit = pPars->nBTLimit;
     pParsSat->fVerbose = pPars->fVeryVerbose;
+    // simulation patterns
     pPat = Cec_ManPatStart();
     pPat->fVerbose = pPars->fVeryVerbose;
+
+    // start equivalence classes
+clk = clock();
+    if ( p->pAig->pReprs == NULL )
+    {
+        if ( Cec_ManSimClassesPrepare(pSim) || Cec_ManSimClassesRefine(pSim) )
+        {
+            Gia_ManStop( p->pAig );
+            p->pAig = NULL;
+            goto finalize;
+        }
+    }
+p->timeSim += clock() - clk;
+    // perform solving
     for ( i = 1; i <= pPars->nItersMax; i++ )
     {
         clk2 = clock();
-        pNew = Cec_ManCswSpecReduction( p ); 
-        if ( pPars->fVeryVerbose )
+        nMatches = 0;
+        if ( pPars->fDoubleOuts )
         {
-            Gia_ManPrintStats( p->pAig );
-            Gia_ManPrintStats( pNew );
+            nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose );
+//            p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig );
+//            Gia_ManEquivTransform( p->pAig, 1 );
         }
-        if ( Gia_ManCoNum(pNew) == 0 )
+        pSrm = Cec_ManFraSpecReduction( p ); 
+        if ( pPars->fVeryVerbose )
+            Gia_ManPrintStats( pSrm );
+        if ( Gia_ManCoNum(pSrm) == 0 )
         {
-            Gia_ManStop( pNew );
+            Gia_ManStop( pSrm );
+            if ( p->pPars->fVerbose )
+                printf( "Considered all available candidate equivalences.\n" );
+            if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) > 0 )
+            {
+                if ( pPars->fColorDiff )
+                {
+                    if ( p->pPars->fVerbose )
+                        printf( "Switching into reduced mode.\n" );
+                    pPars->fColorDiff = 0;
+                }
+                else
+                {
+                    if ( p->pPars->fVerbose )
+                        printf( "Switching into normal mode.\n" );
+                    pPars->fDoubleOuts = 0;
+                }
+                continue;
+            }
             break;
         }
 clk = clock();
-        Cec_ManSatSolve( pPat, pNew, pParsSat ); 
+        Cec_ManSatSolve( pPat, pSrm, pParsSat ); 
 p->timeSat += clock() - clk;
-clk = clock();
-        Cec_ManCswClassesUpdate( p, pPat, pNew );
-p->timeSim += clock() - clk;
-        Gia_ManStop( pNew );
-        pNew = Cec_ManCswDupWithClasses( p );
-        Gia_WriteAiger( pNew, "gia_temp_new.aig", 0, 1 );
+        if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) )
+        {
+            Gia_ManStop( pSrm );
+            Gia_ManStop( p->pAig );
+            p->pAig = NULL;
+            goto finalize;
+        }
+        Gia_ManStop( pSrm );
+
+        // update the manager
+        pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDoubleOuts );
+        Gia_ManStop( pTemp );
         if ( p->pPars->fVerbose )
         {
-            printf( "%3d : P =%7d. D =%7d. F =%6d. Lit =%8d. And =%8d. ", 
-                i, p->nAllProved, p->nAllDisproved, p->nAllFailed,  
-                Cec_ManCswCountLitsAll(p), Gia_ManAndNum(pNew) );
+            printf( "%3d : P =%7d. D =%7d. F =%6d. M = %7d. And =%8d. ", 
+                i, p->nAllProved, p->nAllDisproved, p->nAllFailed, nMatches, Gia_ManAndNum(p->pAig) );
             ABC_PRT( "Time", clock() - clk2 );
         }
-        if ( p->pPars->fVeryVerbose )
+        if ( Gia_ManAndNum(p->pAig) == 0 )
         {
-            ABC_PRTP( "Sim ", p->timeSim, clock() - clkTotal );
-            ABC_PRTP( "Sat ", p->timeSat, clock() - clkTotal );
-            ABC_PRT( "Time", clock() - clkTotal );
-            printf( "****** Intermedate result %3d ******\n", i );
-            Gia_ManPrintStats( p->pAig );
-            Gia_ManPrintStats( pNew );
-            printf("The result is written into file \"%s\".\n", "gia_temp.aig" );
-            printf( "************************************\n" );
+            if ( p->pPars->fVerbose )
+                printf( "Network after reduction is empty.\n" );
+            break;
         }
-        if ( Gia_ManAndNum(pNew) == 0 )
+        // check resource limits
+        if ( p->pPars->TimeLimit && ((double)clock() - clkTotal)/CLOCKS_PER_SEC >= p->pPars->TimeLimit )
         {
-            Gia_ManStop( pNew );
+            fTimeOut = 1;
             break;
         }
-        Gia_ManStop( pNew );
+//        if ( p->nAllFailed && !p->nAllProved && !p->nAllDisproved )
+        if ( p->nAllFailed > p->nAllProved + p->nAllDisproved )
+        {
+            if ( pParsSat->nBTLimit >= 10000 )
+                break;
+            pParsSat->nBTLimit *= 10;
+            if ( p->pPars->fVerbose )
+            {
+                if ( p->pPars->fVerbose )
+                    printf( "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
+                if ( fOutputResult )
+                {
+                    Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 );
+                    printf("The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
+                }
+            }
+        }
+        if ( pPars->fDoubleOuts && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 )
+        {
+            if ( p->pPars->fVerbose )
+                printf( "Switching into reduced mode.\n" );
+            pPars->fColorDiff = 0;
+        }
+        if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) < 20000 )
+        {
+            if ( p->pPars->fVerbose )
+                printf( "Switching into normal mode.\n" );
+            pPars->fColorDiff = 0;
+            pPars->fDoubleOuts = 0;
+        }
     }
-    Gia_ManCleanMark0( pAig );
-    Gia_ManCleanMark1( pAig );
-
-    // verify the result
+finalize:
     if ( p->pPars->fVerbose )
     {
-        printf( "Verifying the result:\n" );
-        pNew = Cec_ManCswSpecReductionProved( p );
-        pParsSat->nBTLimit = 1000000;
-        pParsSat->fVerbose = 1;
-        Cec_ManSatSolve( NULL, pNew, pParsSat ); 
-        Gia_ManStop( pNew );
+        ABC_PRTP( "Sim ", p->timeSim, clock() - (int)clkTotal );
+        ABC_PRTP( "Sat ", p->timeSat-pPat->timeTotalSave, clock() - (int)clkTotal );
+        ABC_PRTP( "Pat ", p->timePat+pPat->timeTotalSave, clock() - (int)clkTotal );
+        ABC_PRT( "Time", clock() - clkTotal );
     }
 
-    // create the resulting miter
-    pAig->pReprs = Cec_ManCswDeriveReprs( p );
-    pNew = Gia_ManDupDfsClasses( pAig );
-    Cec_ManCswStop( p );
+    pTemp = p->pAig; p->pAig = NULL;
+    if ( pTemp == NULL )
+        printf( "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
+    else if ( pSim->pCexes )
+        printf( "Disproved %d outputs of the miter.\n", pSim->nOuts );
+    if ( fTimeOut )
+        printf( "Timed out after %d seconds.\n", (int)((double)clock() - clkTotal)/CLOCKS_PER_SEC );
+
+    pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;
+    Cec_ManSimStop( pSim );
     Cec_ManPatStop( pPat );
-    return pNew;
+    Cec_ManFraStop( p );
+    return pTemp;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 309f4292..1898b07c 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -65,6 +65,7 @@ struct Cec_ManPat_t_
     int              timeSort;       // sorting literals 
     int              timePack;       // packing into sim info structures 
     int              timeTotal;      // total runtime  
+    int              timeTotalSave;  // total runtime for saving  
 };
 
 // SAT solving manager
@@ -100,38 +101,43 @@ struct Cec_ManSat_t_
     int              timeTotal;      // total runtime
 };
 
-// combinational sweeping object
-typedef struct Cec_ObjCsw_t_ Cec_ObjCsw_t;
-struct Cec_ObjCsw_t_
-{
-    int              iRepr;          // representative node
-    unsigned         iNext   : 30;   // next node in the class
-    unsigned         iProved :  1;   // this node is proved
-    unsigned         iFailed :  1;   // this node is failed
-    unsigned         SimNum;         // simulation info number
-};
-
 // combinational simulation manager
-typedef struct Cec_ManCsw_t_ Cec_ManCsw_t;
-struct Cec_ManCsw_t_
+typedef struct Cec_ManSim_t_ Cec_ManSim_t;
+struct Cec_ManSim_t_
 {
     // parameters
     Gia_Man_t *      pAig;           // the AIG to be used for simulation
-    Cec_ParCsw_t *   pPars;          // SAT sweeping parameters 
+    Cec_ParSim_t *   pPars;          // simulation parameters 
     int              nWords;         // the number of simulation words
-    // equivalence classes
-    Cec_ObjCsw_t *   pObjs;          // objects used for SAT sweeping
     // recycable memory
+    int *            pSimInfo;       // simulation information offsets
     unsigned *       pMems;          // allocated simulaton memory
     int              nWordsAlloc;    // the number of allocated entries
     int              nMems;          // the number of used entries  
     int              nMemsMax;       // the max number of used entries 
     int              MemFree;        // next free entry
+    int              nWordsOld;      // the number of simulation words after previous relink
+    // bug catcher
+    Vec_Ptr_t *      vCiSimInfo;     // CI simulation info  
+    Vec_Ptr_t *      vCoSimInfo;     // CO simulation info  
+    void **          pCexes;         // counter-examples for each output
+    int              iOut;           // first failed output
+    int              nOuts;          // the number of failed outputs
+    Gia_Cex_t *      pCexComb;       // counter-example for the first failed output
     // temporaries
     Vec_Int_t *      vClassOld;      // old class numbers
     Vec_Int_t *      vClassNew;      // new class numbers
     Vec_Int_t *      vClassTemp;     // temporary storage
     Vec_Int_t *      vRefinedC;      // refined const reprs
+};
+
+// combinational simulation manager
+typedef struct Cec_ManFra_t_ Cec_ManFra_t;
+struct Cec_ManFra_t_
+{
+    // parameters
+    Gia_Man_t *      pAig;           // the AIG to be used for simulation
+    Cec_ParFra_t *   pPars;          // SAT sweeping parameters 
     // simulation patterns
     Vec_Int_t *      vXorNodes;      // nodes used in speculative reduction
     int              nAllProved;     // total number of proved nodes
@@ -139,6 +145,7 @@ struct Cec_ManCsw_t_
     int              nAllFailed;     // total number of failed nodes
     // runtime stats
     int              timeSim;        // unsat
+    int              timePat;        // unsat
     int              timeSat;        // sat
     int              timeTotal;      // total runtime
 };
@@ -153,29 +160,31 @@ struct Cec_ManCsw_t_
 
 /*=== cecCore.c ============================================================*/
 /*=== cecClass.c ============================================================*/
-extern int                  Cec_ManCswCountLitsAll( Cec_ManCsw_t * p );
-extern int *                Cec_ManCswDeriveReprs( Cec_ManCsw_t * p );
-extern Gia_Man_t *          Cec_ManCswSpecReduction( Cec_ManCsw_t * p );
-extern Gia_Man_t *          Cec_ManCswSpecReductionProved( Cec_ManCsw_t * p );
-extern Gia_Man_t *          Cec_ManCswDupWithClasses( Cec_ManCsw_t * p );
-extern int                  Cec_ManCswClassesPrepare( Cec_ManCsw_t * p );
-extern int                  Cec_ManCswClassesUpdate( Cec_ManCsw_t * p, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
+extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p );
+extern int                  Cec_ManSimClassesRefine( Cec_ManSim_t * p );
+extern int                  Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
+/*=== cecIso.c ============================================================*/
+extern int *                Cec_ManDetectIsomorphism( Gia_Man_t * p );
 /*=== cecMan.c ============================================================*/
-extern Cec_ManCsw_t *       Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t *  pPars );  
-extern void                 Cec_ManCswStop( Cec_ManCsw_t * p );
-extern Cec_ManPat_t *       Cec_ManPatStart();
-extern void                 Cec_ManPatPrintStats( Cec_ManPat_t * p );
-extern void                 Cec_ManPatStop( Cec_ManPat_t * p );
 extern Cec_ManSat_t *       Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern void                 Cec_ManSatPrintStats( Cec_ManSat_t * p );
 extern void                 Cec_ManSatStop( Cec_ManSat_t * p );
+extern Cec_ManPat_t *       Cec_ManPatStart();
+extern void                 Cec_ManPatPrintStats( Cec_ManPat_t * p );
+extern void                 Cec_ManPatStop( Cec_ManPat_t * p );
+extern Cec_ManSim_t *       Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t *  pPars ); 
+extern void                 Cec_ManSimStop( Cec_ManSim_t * p );  
+extern Cec_ManFra_t *       Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t *  pPars );  
+extern void                 Cec_ManFraStop( Cec_ManFra_t * p );
 /*=== cecPat.c ============================================================*/
 extern void                 Cec_ManPatSavePattern( Cec_ManPat_t *  pPat, Cec_ManSat_t *  p, Gia_Obj_t * pObj );
 extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int nInputs, int nWords );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
-/*=== cecUtil.c ============================================================*/
+/*=== ceFraeep.c ============================================================*/
+extern Gia_Man_t *          Cec_ManFraSpecReduction( Cec_ManFra_t * p );
+extern int                  Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/cec/cecIso.c b/src/aig/cec/cecIso.c
new file mode 100644
index 00000000..08d4b7ec
--- /dev/null
+++ b/src/aig/cec/cecIso.c
@@ -0,0 +1,370 @@
+/**CFile****************************************************************
+
+  FileName    [cecIso.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Detection of structural isomorphism.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned * Cec_ManIsoInfo( unsigned * pStore, int nWords, int Id ) { return pStore + nWords * Id; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes simulation info for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ManIsoSimulate( Gia_Obj_t * pObj, int Id, unsigned * pStore, int nWords )
+{
+    unsigned * pInfo  = Cec_ManIsoInfo( pStore, nWords, Id );
+    unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Gia_ObjFaninId0(pObj, Id) );
+    unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, Gia_ObjFaninId1(pObj, Id) );
+    int w;
+    if ( Gia_ObjFaninC0(pObj) )
+    {
+        if (  Gia_ObjFaninC1(pObj) )
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
+        else 
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = ~pInfo0[w] & pInfo1[w];
+    }
+    else 
+    {
+        if (  Gia_ObjFaninC1(pObj) )
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = pInfo0[w] & ~pInfo1[w];
+        else 
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = pInfo0[w] & pInfo1[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copies simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ManIsoCopy( int IdDest, int IdSour, unsigned * pStore, int nWords )
+{
+    unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, IdDest );
+    unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, IdSour );
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pInfo0[w] = pInfo1[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares simulation info of two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManIsoEqual( int Id0, int Id1, unsigned * pStore, int nWords )
+{
+    unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id0 );
+    unsigned * pInfo1 = Cec_ManIsoInfo( pStore, nWords, Id1 );
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        if ( pInfo0[w] != pInfo1[w] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates random simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ManIsoRandom( int Id, unsigned * pStore, int nWords )
+{
+    unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pInfo0[w] = Aig_ManRandom( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash key of the simuation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManIsoHashKey( int Id, unsigned * pStore, int nWords, int nTableSize )
+{
+    static int s_Primes[16] = { 
+        1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
+        4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
+    unsigned * pInfo0 = Cec_ManIsoInfo( pStore, nWords, Id );
+    unsigned uHash = 0;
+    int i;
+    for ( i = 0; i < nWords; i++ )
+        uHash ^= pInfo0[i] * s_Primes[i & 0xf];
+    return (int)(uHash % nTableSize);
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds node to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ManIsoTableAdd( Gia_Man_t * p, int Id, unsigned * pStore, int nWords, int * pTable, int nTableSize )
+{
+    Gia_Obj_t * pTemp;
+    int Key, Ent, Counter = 0, Color = Gia_ObjColors( p, Id );
+    assert( Color == 1 || Color == 2 );
+    Key = Gia_ManIsoHashKey( Id, pStore, nWords, nTableSize );
+    for ( Ent = pTable[Key],  pTemp = (Ent ?  Gia_ManObj(p, Ent) : NULL);  pTemp;
+          Ent = pTemp->Value, pTemp = (Ent ?  Gia_ManObj(p, Ent) : NULL) )
+    {
+        if ( Gia_ObjColors( p, Ent ) != Color )
+            continue;
+        if ( !Gia_ManIsoEqual( Id, Ent, pStore, nWords ) )
+            continue;
+        // found node with the same color and signature - mark it and do not add new node
+        pTemp->fMark0 = 1;
+        return;
+    }
+    // did not find the node with the same color and signature - add new node
+    pTemp = Gia_ManObj( p, Id );
+    assert( pTemp->Value == 0 );
+    assert( pTemp->fMark0 == 0 );
+    pTemp->Value = pTable[Key];
+    pTable[Key] = Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts equivalence class candidates from one bin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Gia_ManIsoExtractClasses( Gia_Man_t * p, int Bin, unsigned * pStore, int nWords, Vec_Int_t * vNodesA, Vec_Int_t * vNodesB )
+{
+    Gia_Obj_t * pTemp;
+    int Ent;
+    Vec_IntClear( vNodesA );
+    Vec_IntClear( vNodesB );
+    for ( Ent = Bin,          pTemp = (Ent ?  Gia_ManObj(p, Ent) : NULL);  pTemp;
+          Ent = pTemp->Value, pTemp = (Ent ?  Gia_ManObj(p, Ent) : NULL) )
+    {
+        if ( pTemp->fMark0 )
+        {
+            pTemp->fMark0 = 0;
+            continue;
+        }
+        if ( Gia_ObjColors( p, Ent ) == 1 )
+            Vec_IntPush( vNodesA, Ent );
+        else
+            Vec_IntPush( vNodesB, Ent );
+    }
+    return Vec_IntSize(vNodesA) > 0 && Vec_IntSize(vNodesB) > 0;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Matches nodes in the extacted classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Gia_ManIsoMatchNodes( int * pIso, unsigned * pStore, int nWords, Vec_Int_t * vNodesA, Vec_Int_t * vNodesB )
+{
+    int k0, k1, IdA, IdB;
+    Vec_IntForEachEntry( vNodesA, IdA, k0 )
+    Vec_IntForEachEntry( vNodesB, IdB, k1 )
+    {
+        if ( Gia_ManIsoEqual( IdA, IdB, pStore, nWords ) )
+        {
+            assert( pIso[IdA] == 0 );
+            assert( pIso[IdB] == 0 );
+            assert( IdA != IdB );
+            pIso[IdA] = IdB;
+            pIso[IdB] = IdA;
+            continue;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms iso into equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManTransformClasses( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pReprs && p->pNexts && p->pIso );
+    memset( p->pReprs, 0, sizeof(int) * Gia_ManObjNum(p) );
+    memset( p->pNexts, 0, sizeof(int) * Gia_ManObjNum(p) );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        p->pReprs[i].iRepr = GIA_VOID;
+        if ( p->pIso[i] && p->pIso[i] < i )
+        {
+            p->pReprs[i].iRepr = p->pIso[i];
+            p->pNexts[p->pIso[i]] = i;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds node correspondences in the miter.]
+
+  Description [Assumes that the colors are assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Cec_ManDetectIsomorphism( Gia_Man_t * p )
+{
+    int nWords = 2;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vNodesA, * vNodesB;
+    unsigned * pStore, Counter;
+    int i, * pIso, * pTable, nTableSize;
+    // start equivalence classes
+    pIso = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsCo(pObj) )
+        {
+            assert( Gia_ObjColors(p, i) == 0 );
+            continue;
+        }
+        assert( Gia_ObjColors(p, i) );
+        if ( Gia_ObjColors(p, i) == 3 )
+            pIso[i] = i;
+    }
+    // start simulation info
+    pStore = ABC_ALLOC( unsigned, Gia_ManObjNum(p) * nWords );
+    // simulate and create table
+    nTableSize = Aig_PrimeCudd( 100 + Gia_ManObjNum(p)/2 );
+    pTable = ABC_CALLOC( int, nTableSize );
+    Gia_ManCleanValue( p );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsCo(pObj) )
+            continue;
+        if ( pIso[i] == 0 ) // simulate
+            Gia_ManIsoSimulate( pObj, i, pStore, nWords );
+        else if ( pIso[i] < i ) // copy
+            Gia_ManIsoCopy( i, pIso[i], pStore, nWords );
+        else // generate
+            Gia_ManIsoRandom( i, pStore, nWords );
+        if ( pIso[i] == 0 )
+            Gia_ManIsoTableAdd( p, i, pStore, nWords, pTable, nTableSize );
+    }
+    // create equivalence classes
+    vNodesA = Vec_IntAlloc( 100 );
+    vNodesB = Vec_IntAlloc( 100 );
+    for ( i = 0; i < nTableSize; i++ )
+        if ( Gia_ManIsoExtractClasses( p, pTable[i], pStore, nWords, vNodesA, vNodesB ) )
+            Gia_ManIsoMatchNodes( pIso, pStore, nWords, vNodesA, vNodesB );
+    Vec_IntFree( vNodesA );
+    Vec_IntFree( vNodesB );
+    // collect info
+    Counter = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        Counter += (pIso[i] && pIso[i] < i);
+/*
+        if ( pIso[i] && pIso[i] < i )
+        {
+            if ( (Gia_ObjIsHead(p,pIso[i]) && Gia_ObjRepr(p,i)==pIso[i]) || 
+                 (Gia_ObjIsClass(p,pIso[i]) && Gia_ObjRepr(p,i)==Gia_ObjRepr(p,pIso[i])) )
+                 printf( "1" );
+            else
+                printf( "0" );
+        }
+*/
+    }
+    printf( "Computed %d pairs of structurally equivalent nodes.\n", Counter );
+//    p->pIso = pIso;
+//    Cec_ManTransformClasses( p );
+
+    ABC_FREE( pTable );
+    ABC_FREE( pStore );
+    return pIso;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index b8ee75b2..1a94409f 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -30,7 +30,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Creates AIG.]
+  Synopsis    [Creates the manager.]
 
   Description []
                
@@ -39,26 +39,25 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t *  pPars )  
-{ 
-    Cec_ManCsw_t * p;
-    p = ABC_ALLOC( Cec_ManCsw_t, 1 );
-    memset( p, 0, sizeof(Cec_ManCsw_t) );
-    p->pAig  = pAig;
-    p->pPars = pPars;
-    p->pObjs = ABC_CALLOC( Cec_ObjCsw_t, Gia_ManObjNum(pAig) );
-    // temporaries
-    p->vClassOld  = Vec_IntAlloc( 1000 );
-    p->vClassNew  = Vec_IntAlloc( 1000 );
-    p->vClassTemp = Vec_IntAlloc( 1000 );
-    p->vRefinedC  = Vec_IntAlloc( 10000 );
-    p->vXorNodes  = Vec_IntAlloc( 1000 );
+Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
+{
+    Cec_ManSat_t * p;
+    // create interpolation manager
+    p = ABC_ALLOC( Cec_ManSat_t, 1 );
+    memset( p, 0, sizeof(Cec_ManSat_t) );
+    p->pPars        = pPars;
+    p->pAig         = pAig;
+    // SAT solving
+    p->nSatVars     = 1;
+    p->pSatVars     = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
+    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
+    p->vFanins      = Vec_PtrAlloc( 100 );
     return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Deletes AIG.]
+  Synopsis    [Prints statistics of the manager.]
 
   Description []
                
@@ -67,19 +66,46 @@ Cec_ManCsw_t * Cec_ManCswStart( Gia_Man_t * pAig, Cec_ParCsw_t *  pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManCswStop( Cec_ManCsw_t * p )  
+void Cec_ManSatPrintStats( Cec_ManSat_t * p )
 {
-    Vec_IntFree( p->vXorNodes );
-    Vec_IntFree( p->vClassOld );
-    Vec_IntFree( p->vClassNew );
-    Vec_IntFree( p->vClassTemp );
-    Vec_IntFree( p->vRefinedC );
-    ABC_FREE( p->pMems );
-    ABC_FREE( p->pObjs );
+    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
+    printf( "Conf = %5d  ", p->pPars->nBTLimit );
+    printf( "MinVar = %5d  ", p->pPars->nSatVarMax );
+    printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
+    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+    ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
+    printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+    ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
+    printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
+        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+    ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatStop( Cec_ManSat_t * p )
+{
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    Vec_PtrFree( p->vUsedNodes );
+    Vec_PtrFree( p->vFanins );
+    ABC_FREE( p->pSatVars );
     ABC_FREE( p );
 }
 
 
+
 /**Function*************************************************************
 
   Synopsis    [Creates AIG.]
@@ -147,9 +173,11 @@ void Cec_ManPatStop( Cec_ManPat_t * p )
     ABC_FREE( p );
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Creates the manager.]
+  Synopsis    [Creates AIG.]
 
   Description []
                
@@ -158,25 +186,31 @@ void Cec_ManPatStop( Cec_ManPat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
-{
-    Cec_ManSat_t * p;
-    // create interpolation manager
-    p = ABC_ALLOC( Cec_ManSat_t, 1 );
-    memset( p, 0, sizeof(Cec_ManSat_t) );
-    p->pPars        = pPars;
-    p->pAig         = pAig;
-    // SAT solving
-    p->nSatVars     = 1;
-    p->pSatVars     = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
-    p->vUsedNodes   = Vec_PtrAlloc( 1000 );
-    p->vFanins      = Vec_PtrAlloc( 100 );
+Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t *  pPars )  
+{ 
+    Cec_ManSim_t * p;
+    p = ABC_ALLOC( Cec_ManSim_t, 1 );
+    memset( p, 0, sizeof(Cec_ManSim_t) );
+    p->pAig  = pAig;
+    p->pPars = pPars;
+    p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
+    p->vClassOld  = Vec_IntAlloc( 1000 );
+    p->vClassNew  = Vec_IntAlloc( 1000 );
+    p->vClassTemp = Vec_IntAlloc( 1000 );
+    p->vRefinedC  = Vec_IntAlloc( 10000 );
+    p->vCiSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(p->pAig), pPars->nWords );
+    if ( pPars->fCheckMiter || Gia_ManRegNum(p->pAig) )
+    {
+        p->vCoSimInfo = Vec_PtrAllocSimInfo( Gia_ManCoNum(p->pAig), pPars->nWords );
+        Vec_PtrCleanSimInfo( p->vCoSimInfo, 0, pPars->nWords );
+    }
+    p->iOut = -1;
     return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prints statistics of the manager.]
+  Synopsis    [Deletes AIG.]
 
   Description []
                
@@ -185,26 +219,27 @@ Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSatPrintStats( Cec_ManSat_t * p )
+void Cec_ManSimStop( Cec_ManSim_t * p )  
 {
-    printf( "CO = %6d  ", Gia_ManCoNum(p->pAig) );
-    printf( "Conf = %5d  ", p->pPars->nBTLimit );
-    printf( "MinVar = %5d  ", p->pPars->nSatVarMax );
-    printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
-    printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
-    ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
-    printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
-    ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
-    printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
-    ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
+    Vec_IntFree( p->vClassOld );
+    Vec_IntFree( p->vClassNew );
+    Vec_IntFree( p->vClassTemp );
+    Vec_IntFree( p->vRefinedC );
+    if ( p->vCiSimInfo ) 
+        Vec_PtrFree( p->vCiSimInfo );
+    if ( p->vCoSimInfo ) 
+        Vec_PtrFree( p->vCoSimInfo );
+    ABC_FREE( p->pCexComb );
+    ABC_FREE( p->pCexes );
+    ABC_FREE( p->pMems );
+    ABC_FREE( p->pSimInfo );
+    ABC_FREE( p );
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Frees the manager.]
+  Synopsis    [Creates AIG.]
 
   Description []
                
@@ -213,16 +248,35 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSatStop( Cec_ManSat_t * p )
+Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t *  pPars )  
+{ 
+    Cec_ManFra_t * p;
+    p = ABC_ALLOC( Cec_ManFra_t, 1 );
+    memset( p, 0, sizeof(Cec_ManFra_t) );
+    p->pAig  = pAig;
+    p->pPars = pPars;
+    p->vXorNodes  = Vec_IntAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManFraStop( Cec_ManFra_t * p )  
 {
-    if ( p->pSat )
-        sat_solver_delete( p->pSat );
-    Vec_PtrFree( p->vUsedNodes );
-    Vec_PtrFree( p->vFanins );
-    ABC_FREE( p->pSatVars );
+    Vec_IntFree( p->vXorNodes );
     ABC_FREE( p );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecPat.c b/src/aig/cec/cecPat.c
index 1af4f333..b80f1e44 100644
--- a/src/aig/cec/cecPat.c
+++ b/src/aig/cec/cecPat.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [cec.c]
+  FileName    [cecPat.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Combinatinoal equivalence checking.]
 
-  Synopsis    []
+  Synopsis    [Simulation pattern manager.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: cec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: cecPat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/aig/cec/cecSim.c b/src/aig/cec/cecSim.c
new file mode 100644
index 00000000..dbd3bd5e
--- /dev/null
+++ b/src/aig/cec/cecSim.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [cecSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Simulation manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index e4daf719..ba4b0477 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -390,6 +390,70 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets variable activities in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMin, int LevelMax )
+{
+    float dActConeBumpMax = 20.0;
+    int iVar;
+    // skip visited variables
+    if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p->pAig, pObj);
+    // add the PI to the list
+    if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) )
+        return;
+    // set the factor of this variable
+    // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
+    if ( (iVar = Cec_ObjSatNum(p,pObj)) )
+    {
+        p->pSat->factors[iVar] = dActConeBumpMax * (Gia_ObjLevel(p->pAig, pObj) - LevelMin)/(LevelMax - LevelMin);
+        veci_push(&p->pSat->act_vars, iVar);
+    }
+    // explore the fanins
+    Cec_SetActivityFactors_rec( p, Gia_ObjFanin0(pObj), LevelMin, LevelMax );
+    Cec_SetActivityFactors_rec( p, Gia_ObjFanin1(pObj), LevelMin, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets variable activities in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
+{
+    float dActConeRatio = 0.5;
+    int LevelMin, LevelMax;
+    // reset the active variables
+    veci_resize(&p->pSat->act_vars, 0);
+    // prepare for traversal
+    Gia_ManIncrementTravId( p->pAig );
+    // determine the min and max level to visit
+    assert( dActConeRatio > 0 && dActConeRatio < 1 );
+    LevelMax = Gia_ObjLevel(p->pAig,pObj);
+    LevelMin = (int)(LevelMax * (1.0 - dActConeRatio));
+    // traverse
+    Cec_SetActivityFactors_rec( p, pObj, LevelMin, LevelMax );
+//Cec_PrintActivity( p );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Runs equivalence test for the two nodes.]
 
   Description []
@@ -402,7 +466,7 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
 int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 {
     int nBTLimit = p->pPars->nBTLimit;
-    int Lit, RetValue, status, clk, nConflicts;
+    int Lit, RetValue, status, clk, clk2, nConflicts;
 
     p->nCallsSince++;  // experiment with this!!!
     p->nSatTotal++;
@@ -415,7 +479,14 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
         Cec_ManSatSolverRecycle( p );
 
     // if the nodes do not have SAT variables, allocate them
+clk2 = clock();
     Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) );
+//ABC_PRT( "cnf", clock() - clk2 );
+//printf( "%d \n", p->pSat->size );
+
+clk2 = clock();
+//    Cec_SetActivityFactors( p, Gia_ObjFanin0(pObj) ); 
+//ABC_PRT( "act", clock() - clk2 );
 
     // propage unit clauses
     if ( p->pSat->qtail != p->pSat->qhead )
@@ -435,8 +506,12 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
 clk = clock();
     nConflicts = p->pSat->stats.conflicts;
+
+clk2 = clock();
     RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, 
         (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+//ABC_PRT( "sat", clock() - clk2 );
+
     if ( RetValue == l_False )
     {
 p->timeSatUnsat += clock() - clk;
@@ -466,6 +541,7 @@ p->timeSatUndec += clock() - clk;
     }
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs one round of solving for the POs of the AIG.]
@@ -486,7 +562,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
     Bar_Progress_t * pProgress = NULL;
     Cec_ManSat_t * p;
     Gia_Obj_t * pObj;
-    int i, status, clk = clock();
+    int i, status, clk = clock(), clk2;
 
 //    sprintf( Buffer, "gia%03d.aig", Counter++ );
 //Gia_WriteAiger( pAig, Buffer, 0, 0 );
@@ -499,8 +575,9 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
         pPat->nPats = 0;
         pPat->nPatLits = 0;
         pPat->nPatLitsMin = 0;
-    }
+    } 
     Gia_ManSetPhase( pAig );
+    Gia_ManLevelNum( pAig );
     Gia_ManResetTravId( pAig );
     p = Cec_ManSatCreate( pAig, pPars );
     pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
@@ -512,13 +589,19 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
             pObj->fMark1 = 1;
             continue;
         }
-//printf( "Output %6d : ", i );
-
         Bar_ProgressUpdate( pProgress, i, "SAT..." );
+clk2 = clock();
         status = Cec_ManSatCheckNode( p, pObj );
         pObj->fMark0 = (status == 0);
         pObj->fMark1 = (status == 1);
 /*
+printf( "Output %6d : ", i );
+printf( "conf = %6d ", p->pSat->stats.conflicts );
+printf( "prop = %6d ", p->pSat->stats.propagations );
+ABC_PRT( "time", clock() - clk2 );
+*/
+
+/*
         if ( status == -1 )
         {
             Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
@@ -531,7 +614,11 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
             continue;
         // save the pattern
         if ( pPat )
+        {
+            int clk3 = clock();
             Cec_ManPatSavePattern( pPat, p, pObj );
+            pPat->timeTotalSave += clock() - clk3;
+        }
         // quit if one of them is solved
         if ( pPars->fFirstStop )
             break;
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
new file mode 100644
index 00000000..20a668bd
--- /dev/null
+++ b/src/aig/cec/cecSweep.c
@@ -0,0 +1,294 @@
+/**CFile****************************************************************
+
+  FileName    [ceFraeep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [SAT sweeping manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ceFraeep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs limited speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int iRes0, iRes1, iRepr, iNode, iMiter;
+    int i, fCompl, * piCopies, * pDepths;
+    Gia_ManSetPhase( p->pAig );
+    Vec_IntClear( p->vXorNodes );
+    if ( p->pPars->nLevelMax )
+        Gia_ManLevelNum( p->pAig );
+    pNew = Gia_ManStart( Gia_ManObjNum(p->pAig) );
+    pNew->pName = Aig_UtilStrsav( p->pAig->pName );
+    Gia_ManHashAlloc( pNew );
+    piCopies = ABC_FALLOC( int, Gia_ManObjNum(p->pAig) );
+    pDepths  = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+    piCopies[0] = 0;
+    Gia_ManForEachObj1( p->pAig, pObj, i )
+    {
+        if ( Gia_ObjIsCi(pObj) ) 
+        {
+            piCopies[i] = Gia_ManAppendCi( pNew );
+            continue;
+        }
+        if ( Gia_ObjIsCo(pObj) ) 
+            continue;
+        if ( piCopies[Gia_ObjFaninId0(pObj,i)] == -1 ||
+             piCopies[Gia_ObjFaninId1(pObj,i)] == -1 )
+             continue;
+        iRes0 = Gia_LitNotCond( piCopies[Gia_ObjFaninId0(pObj,i)], Gia_ObjFaninC0(pObj) );
+        iRes1 = Gia_LitNotCond( piCopies[Gia_ObjFaninId1(pObj,i)], Gia_ObjFaninC1(pObj) );
+        iNode = piCopies[i] = Gia_ManHashAnd( pNew, iRes0, iRes1 );
+        pDepths[i] = AIG_MAX( pDepths[Gia_ObjFaninId0(pObj,i)], pDepths[Gia_ObjFaninId1(pObj,i)] );
+        if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID || Gia_ObjFailed(p->pAig, i) )
+            continue;
+        assert( Gia_ObjRepr(p->pAig, i) < i );
+        iRepr = piCopies[Gia_ObjRepr(p->pAig, i)];
+        if ( iRepr == -1 )
+            continue;
+        if ( Gia_LitRegular(iNode) == Gia_LitRegular(iRepr) )
+            continue;
+        if ( p->pPars->nLevelMax && 
+            (Gia_ObjLevel(p->pAig, pObj)  > p->pPars->nLevelMax || 
+             Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
+            continue;
+        if ( p->pPars->fDoubleOuts )
+        {
+//            if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) )
+//                Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 );
+            if ( p->pPars->fColorDiff )
+            {
+                if ( !Gia_ObjDiffColors( p->pAig, Gia_ObjRepr(p->pAig, i), i ) )
+                    continue;
+            }
+            else
+            {
+                if ( !Gia_ObjDiffColors2( p->pAig, Gia_ObjRepr(p->pAig, i), i ) )
+                    continue;
+            }
+        }
+        pRepr = Gia_ManObj( p->pAig, Gia_ObjRepr(p->pAig, i) );
+        fCompl = Gia_ObjPhaseReal(pObj) ^ Gia_ObjPhaseReal(pRepr);
+        piCopies[i] = Gia_LitNotCond( iRepr, fCompl );
+        if ( Gia_ObjProved(p->pAig, i) )
+            continue;
+        // produce speculative miter
+        iMiter = Gia_ManHashXor( pNew, iNode, piCopies[i] );
+        Gia_ManAppendCo( pNew, iMiter );
+        Vec_IntPush( p->vXorNodes, Gia_ObjRepr(p->pAig, i) );
+        Vec_IntPush( p->vXorNodes, i );
+        // add to the depth of this node
+        pDepths[i] = 1 + AIG_MAX( pDepths[i], pDepths[Gia_ObjRepr(p->pAig, i)] );
+        if ( p->pPars->nDepthMax && pDepths[i] >= p->pPars->nDepthMax )
+            piCopies[i] = -1;
+    }
+    ABC_FREE( piCopies );
+    ABC_FREE( pDepths );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManFraClassesUpdate_rec( Gia_Obj_t * pObj )
+{
+    int Result;
+    if ( pObj->fMark0 )
+        return 1;
+    if ( Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj) )
+        return 0;
+    Result = (Cec_ManFraClassesUpdate_rec( Gia_ObjFanin0(pObj) ) |
+              Cec_ManFraClassesUpdate_rec( Gia_ObjFanin1(pObj) ));
+    return pObj->fMark0 = Result;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates simulation info for this round.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManFraCreateInfo( Cec_ManSim_t * p, Vec_Ptr_t * vCiInfo, Vec_Ptr_t * vInfo, int nSeries )
+{
+    unsigned * pRes0, * pRes1;
+    int i, w;
+    for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ )
+    {
+        pRes0 = Vec_PtrEntry( vCiInfo, i );
+        pRes1 = Vec_PtrEntry( vInfo, i );
+        pRes1 += p->nWords * nSeries;
+        for ( w = 0; w < p->nWords; w++ )
+            pRes0[w] = pRes1[w];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates equivalence classes using the patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew )
+{
+    Vec_Ptr_t * vInfo;
+    Gia_Obj_t * pObj, * pObjOld, * pReprOld;
+    int i, k, iRepr, iNode, clk;
+clk = clock();
+    vInfo = Cec_ManPatCollectPatterns( pPat, Gia_ManCiNum(p->pAig), pSim->nWords );
+p->timePat += clock() - clk;
+clk = clock();
+    if ( vInfo != NULL )
+    {
+        Gia_ManSetRefs( p->pAig );
+        for ( i = 0; i < pPat->nSeries; i++ )
+        {
+            Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i );
+            if ( Cec_ManSimSimulateRound( pSim, pSim->vCiSimInfo, pSim->vCoSimInfo ) )
+            {
+                Vec_PtrFree( vInfo );
+                return 1;
+            }
+        }
+        Vec_PtrFree( vInfo );
+    }
+p->timeSim += clock() - clk;
+    assert( Vec_IntSize(p->vXorNodes) == 2*Gia_ManCoNum(pNew) );
+    // mark the transitive fanout of failed nodes
+    if ( p->pPars->nDepthMax != 1 )
+    {
+        Gia_ManCleanMark0( p->pAig );
+        Gia_ManCleanMark1( p->pAig );
+        Gia_ManForEachCo( pNew, pObj, k )
+        {
+            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
+            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
+            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
+                continue;
+//            Gia_ManObj(p->pAig, iRepr)->fMark0 = 1;
+            Gia_ManObj(p->pAig, iNode)->fMark0 = 1;
+        }
+        // mark the nodes reachable through the failed nodes
+        Gia_ManForEachAnd( p->pAig, pObjOld, k )
+            pObjOld->fMark0 |= (Gia_ObjFanin0(pObjOld)->fMark0 | Gia_ObjFanin1(pObjOld)->fMark0);
+        // unmark the disproved nodes
+        Gia_ManForEachCo( pNew, pObj, k )
+        {
+            iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
+            iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
+            if ( pObj->fMark0 == 0 && pObj->fMark1 == 1 ) // proved
+                continue; 
+            pObjOld = Gia_ManObj(p->pAig, iNode);
+            assert( pObjOld->fMark0 == 1 );
+            if ( Gia_ObjFanin0(pObjOld)->fMark0 == 0 && Gia_ObjFanin1(pObjOld)->fMark0 == 0 )
+                pObjOld->fMark1 = 1;
+        }
+        // clean marks
+        Gia_ManForEachAnd( p->pAig, pObjOld, k )
+            if ( pObjOld->fMark1 )
+            {
+                pObjOld->fMark0 = 0;
+                pObjOld->fMark1 = 0;
+            }
+    }
+    // set the results
+    p->nAllProved = p->nAllDisproved = p->nAllFailed = 0;
+    Gia_ManForEachCo( pNew, pObj, k )
+    {
+        iRepr = Vec_IntEntry( p->vXorNodes, 2*k );
+        iNode = Vec_IntEntry( p->vXorNodes, 2*k+1 );
+        pReprOld = Gia_ManObj(p->pAig, iRepr);
+        pObjOld = Gia_ManObj(p->pAig, iNode);
+        if ( pObj->fMark1 )
+        { // proved
+            assert( pObj->fMark0 == 0 );
+            assert( !Gia_ObjProved(p->pAig, iNode) );
+            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
+//            if ( pObjOld->fMark0 == 0 )
+            {
+                assert( iRepr == Gia_ObjRepr(p->pAig, iNode) );
+                Gia_ObjSetProved( p->pAig, iNode );
+                p->nAllProved++;
+            }
+        }
+        else if ( pObj->fMark0 )
+        { // disproved
+            assert( pObj->fMark1 == 0 );
+            if ( pReprOld->fMark0 == 0 && pObjOld->fMark0 == 0 )
+//            if ( pObjOld->fMark0 == 0 )
+            {
+                if ( iRepr == Gia_ObjRepr(p->pAig, iNode) )
+                    printf( "Cec_ManFraClassesUpdate(): Error! Node is not refined!\n" );
+                p->nAllDisproved++;
+            }
+        }
+        else
+        { // failed
+            assert( pObj->fMark0 == 0 );
+            assert( pObj->fMark1 == 0 );
+            assert( !Gia_ObjFailed(p->pAig, iNode) );
+            assert( !Gia_ObjProved(p->pAig, iNode) );
+            Gia_ObjSetFailed( p->pAig, iNode );
+            p->nAllFailed++;
+        }
+    } 
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make
index f8e2602a..4618c424 100644
--- a/src/aig/cec/module.make
+++ b/src/aig/cec/module.make
@@ -1,5 +1,9 @@
-SRC +=    src/aig/cec/cecClass.c \
+SRC +=    src/aig/cec/cecCec.c \
+    src/aig/cec/cecClass.c \
     src/aig/cec/cecCore.c \
+    src/aig/cec/cecIso.c \
     src/aig/cec/cecMan.c \
     src/aig/cec/cecPat.c \
-    src/aig/cec/cecSolve.c
+    src/aig/cec/cecSim.c \
+    src/aig/cec/cecSolve.c \
+    src/aig/cec/cecSweep.c