Changes to enable smarter simulation.

5 files changed, 842 insertions, 891 deletions

diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 1361893a..22b6c6e5 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -116,11 +116,8 @@ extern int           Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec
 extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
 /*=== sswRarity.c ===================================================*/
-extern int           Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
-/*=== sswRarity2.c ===================================================*/
-extern int           Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-extern int           Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
+extern int           Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
+extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
 /*=== sswSim.c ===================================================*/
 extern Ssw_Sml_t *   Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index 3026cf6b..3ebc7799 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -37,19 +37,27 @@ struct Ssw_RarMan_t_
     int            nBinSize;     // the number of flops in one group
     int            fVerbose;     // the verbosiness flag
     int            nGroups;      // the number of flop groups
+    int            nWordsReg;    // the number of words in the registers
     // internal data
     Aig_Man_t *    pAig;         // AIG with equivalence classes
     Ssw_Cla_t *    ppClasses;    // equivalence classes
-    Ssw_Sml_t *    pSml;         // simulation manager
-    Vec_Ptr_t *    vSimInfo;     // simulation info from pSml manager
     Vec_Int_t *    vInits;       // initial state
+    // simulation data
+    word *         pObjData;     // simulation info for each obj
+    word *         pPatData;     // pattern data for each reg
+    // candidates to update
+    Vec_Ptr_t *    vUpdConst;    // constant 1 candidates
+    Vec_Ptr_t *    vUpdClass;    // class representatives
     // rarity data
     int *          pRarity;      // occur counts for patterns in groups
-    int *          pGroupValues; // occur counts in each group
     double *       pPatCosts;    // pattern costs
-
+    // best patterns
+    Vec_Int_t *    vPatBests;    // best patterns
+    int            iFailPo;      // failed primary output
+    int            iFailPat;     // failed pattern
 };
 
+
 static inline int  Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) 
 {
     assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
@@ -69,13 +77,19 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
     p->pRarity[iBin * (1 << p->nBinSize) + iPat]++;
 }
 
+static inline int    Ssw_RarBitWordNum( int nBits )             { return (nBits>>6) + ((nBits&63) > 0);  }
+
+static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id )  { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id;    }
+static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id )  { assert( Id < 64 * p->nWords );            return p->pPatData + p->nWordsReg * Id; }
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Prepares random number generator.]
 
   Description []
                
@@ -84,29 +98,17 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
   SeeAlso     []
 
 ***********************************************************************/
-static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
+void Ssw_RarManPrepareRandom( int nRandSeed )
 {
-    Ssw_RarMan_t * p;
-    if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
-        return NULL;
-    p = ABC_CALLOC( Ssw_RarMan_t, 1 );
-    p->pAig = pAig;
-    p->nWords = nWords;
-    p->nFrames = nFrames;
-    p->nBinSize = nBinSize;
-    p->fVerbose = fVerbose;
-    p->nGroups  = Aig_ManRegNum(pAig) / nBinSize;
-    p->pRarity  = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
-    p->pGroupValues = ABC_CALLOC( int, p->nGroups );
-    p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 );
-    p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
-    p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
-    return p;
+    int i;
+    Aig_ManRandom( 1 );
+    for ( i = 0; i < nRandSeed; i++ )
+        Aig_ManRandom( 0 );
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Initializes random primary inputs.]
 
   Description []
                
@@ -115,22 +117,112 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
   SeeAlso     []
 
 ***********************************************************************/
-static void Ssw_RarManStop( Ssw_RarMan_t * p )
+void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
 {
-    if ( p->pSml ) Ssw_SmlStop( p->pSml );
-    if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
-    Vec_PtrFreeP( &p->vSimInfo );
-    Vec_IntFreeP( &p->vInits );
-    ABC_FREE( p->pGroupValues );
-    ABC_FREE( p->pPatCosts );
-    ABC_FREE( p->pRarity );
-    ABC_FREE( p );
+    word * pSim;
+    Aig_Obj_t * pObj;
+    int w, i;
+    Saig_ManForEachPi( p->pAig, pObj, i )
+    {
+        pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+        for ( w = 0; w < p->nWords; w++ )
+            pSim[w] = Aig_ManRandom64(0);
+        pSim[0] <<= 1;
+    }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal )
+{
+    Abc_Cex_t * pCex;
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vTrace;
+    word * pSim;
+    int i, r, f, iBit, iPatThis;
+    // compute the pattern sequence
+    iPatThis = iPatFinal;
+    vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
+    Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
+    for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
+    {
+        iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
+        Vec_IntWriteEntry( vTrace, r, iPatThis );
+    }
+    // create counter-example
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
+    pCex->iFrame = iFrame;
+    pCex->iPo = iPo;
+    // insert the bits
+    iBit = Aig_ManRegNum(p->pAig);
+    for ( f = 0; f <= iFrame; f++ )
+    {
+        Ssw_RarManAssingRandomPis( p );
+        iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
+        Saig_ManForEachPi( p->pAig, pObj, i )
+        {
+            pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+            if ( Aig_InfoHasBit( (unsigned *)pSim, iPatThis ) )
+                Aig_InfoSetBit( pCex->pData, iBit );
+            iBit++;
+        }
+    }
+    Vec_IntFree( vTrace );
+    assert( iBit == pCex->nBits );
+    // verify the counter example
+    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
+    {
+        printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
+    }
+    else
+    {
+//      printf( "Counter-example verification is successful.\n" );
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+    }
+    return pCex;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transposing 32-bit matrix.]
+
+  Description [Borrowed from "Hacker's Delight", by Henry Warren.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void transpose32( unsigned A[32] )
+{
+    int j, k; 
+    unsigned t, m = 0x0000FFFF; 
+    for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) ) 
+    {
+        for ( k = 0; k < 32; k = (k + j + 1) & ~j )
+        {
+            t = (A[k] ^ (A[k+j] >> j)) & m;
+            A[k] = A[k] ^ t;
+            A[k+j] = A[k+j] ^ (t << j);
+        }
+    }
+} 
 
 /**Function*************************************************************
 
-  Synopsis    [Updates rarity counters.]
+  Synopsis    [Transposing 64-bit matrix.]
 
   Description []
                
@@ -139,39 +231,487 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
+void transpose64( word A[64] )
+{
+    int j, k; 
+    word t, m = 0x00000000FFFFFFFF; 
+    for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) 
+    {
+        for ( k = 0; k < 64; k = (k + j + 1) & ~j )
+        {
+            t = (A[k] ^ (A[k+j] >> j)) & m;
+            A[k] = A[k] ^ t;
+            A[k+j] = A[k+j] ^ (t << j);
+        }
+    }
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Transposing 64-bit matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void transpose64Simple( word A[64], word B[64] )
+{
+    int i, k; 
+    for ( i = 0; i < 64; i++ )
+        B[i] = 0;
+    for ( i = 0; i < 64; i++ ) 
+    for ( k = 0; k < 64; k++ )
+        if ( (A[i] >> k) & 1 )
+            B[k] |= ((word)1 << (63-i));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing the transposing code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void TransposeTest()
+{
+    word M[64], N[64];
+    int i, clk;
+    Aig_ManRandom64( 1 );
+//    for ( i = 0; i < 64; i++ )
+//        M[i] = Aig_ManRandom64( 0 );
+    for ( i = 0; i < 64; i++ )
+        M[i] = i? (word)0 : ~(word)0;
+//    for ( i = 0; i < 64; i++ )
+//        Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
+
+    clk = clock();
+    for ( i = 0; i < 100001; i++ )
+        transpose64Simple( M, N );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+    clk = clock();
+    for ( i = 0; i < 100001; i++ )
+        transpose64( M );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+
+    for ( i = 0; i < 64; i++ )
+        if ( M[i] != N[i] )
+            printf( "Mismatch\n" );
+/*
+    printf( "\n" );
+    for ( i = 0; i < 64; i++ )
+        Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
+    printf( "\n" );
+    for ( i = 0; i < 64; i++ )
+        Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarTranspose( Ssw_RarMan_t * p )
 {
     Aig_Obj_t * pObj;
-    unsigned * pData;
-    int i, k;
+    word M[64];
+    int w, r, i;
+    for ( w = 0; w < p->nWords; w++ )
+    for ( r = 0; r < p->nWordsReg; r++ )
+    {
+        // save input
+        for ( i = 0; i < 64; i++ )
+        {
+            if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
+            {
+                pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
+                M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
+            }
+            else
+                M[i] = 0;
+        }
+        // transpose
+        transpose64( M );
+        // save output
+        for ( i = 0; i < 64; i++ )
+            Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
+    }
 /*
     Saig_ManForEachLi( p->pAig, pObj, i )
     {
-        pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
-        Extra_PrintBinary( stdout, pData, 32 );  printf( "\n" );
+        word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+        Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" );
     }
+    printf( "\n" );
+    for ( i = 0; i < p->nWords*64; i++ )
+    {
+        word * pBitData = Ssw_RarPatSim( p, i );
+        Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
+    }
+    printf( "\n" );
 */
-    for ( k = 0; k < p->nWords * 32; k++ )
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Sets random inputs and specialied flop outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
+{
+    Aig_Obj_t * pObj, * pObjLi;
+    word * pSim, * pSimLi;
+    int w, i;
+    // constant
+    pObj = Aig_ManConst1( p->pAig );
+    pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+    for ( w = 0; w < p->nWords; w++ )
+        pSim[w] = ~(word)0;
+    // primary inputs
+    Ssw_RarManAssingRandomPis( p );
+    // flop outputs
+    if ( vInit )
     {
-        for ( i = 0; i < p->nGroups; i++ )
-            p->pGroupValues[i] = 0;
-        Saig_ManForEachLi( p->pAig, pObj, i )
+        assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords );
+        Saig_ManForEachLo( p->pAig, pObj, i )
         {
-            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
-            if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
-                p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
+            pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+            for ( w = 0; w < p->nWords; w++ )
+                pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
         }
-        for ( i = 0; i < p->nGroups; i++ )
-            Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] );
     }
-/*
-    for ( i = 0; i < p->nGroups; i++ )
+    else
     {
-        for ( k = 0; k < (1 << p->nBinSize); k++ )
-            printf( "%d ", Ssw_RarGetBinPat(p, i, k) );
-        printf( "\n" );
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
+        {
+            pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
+            pSim   = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+            for ( w = 0; w < p->nWords; w++ )
+                pSim[w] = pSimLi[w];
+        }
     }
-*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
+{
+    word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+    word Flip = pObj->fPhase ? ~0 : 0;
+    int w;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( pSim[w] ^ Flip )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
+    word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
+    word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0;
+    int w;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( pSim0[w] ^ pSim1[w] ^ Flip )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
+{
+    static int s_SPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned * pSims;
+    unsigned uHash;
+    int i;
+    uHash = 0;
+    pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
+    for ( i = 0; i < 2 * p->nWords; i++ )
+        uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
+    return uHash;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
+{
+    word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+    word Flip = pObj->fPhase ? ~0 : 0;
+    int w, i;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( pSim[w] ^ Flip )
+        {
+            for ( i = 0; i < 64; i++ )
+                if ( ((pSim[w] ^ Flip) >> i) & 1 )
+                    break;
+            assert( i < 64 );
+            return w * 64 + i;
+        }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if any of the POs becomes non-constant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    p->iFailPo  = -1;
+    p->iFailPat = -1;
+    Saig_ManForEachPo( p->pAig, pObj, i )
+    {
+        if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
+            return 0;
+        if ( !Ssw_RarManObjIsConst(p, pObj) )
+        {
+            p->iFailPo  = i;
+            p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
+{
+    Aig_Obj_t * pObj, * pRepr;
+    word * pSim, * pSim0, * pSim1;
+    word Flip, Flip0, Flip1;
+    int w, i;
+    // initialize 
+    Ssw_RarManInitialize( p, vInit );
+    Vec_PtrClear( p->vUpdConst );
+    Vec_PtrClear( p->vUpdClass );
+    Aig_ManIncrementTravId( p->pAig );
+    // check comb inputs
+    if ( fUpdate )
+    Aig_ManForEachPi( p->pAig, pObj, i )
+    {
+        pRepr = Aig_ObjRepr(p->pAig, pObj);
+        if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
+            continue;
+        if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
+            continue;
+        // save for update
+        if ( pRepr == Aig_ManConst1(p->pAig) )
+            Vec_PtrPush( p->vUpdConst, pObj );
+        else
+        {
+            Vec_PtrPush( p->vUpdClass, pRepr );
+            Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
+        }
+    }
+    // simulate 
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        pSim  = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+        pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
+        pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
+        Flip0 = Aig_ObjFaninC0(pObj) ? ~0 : 0;
+        Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0;
+        for ( w = 0; w < p->nWords; w++ )
+            pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
+        if ( !fUpdate )
+            continue;
+        // check classes
+        pRepr = Aig_ObjRepr(p->pAig, pObj);
+        if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
+            continue;
+        if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
+            continue;
+        // save for update
+        if ( pRepr == Aig_ManConst1(p->pAig) )
+            Vec_PtrPush( p->vUpdConst, pObj );
+        else
+        {
+            Vec_PtrPush( p->vUpdClass, pRepr );
+            Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
+        }
+    }
+    // transfer to POs
+    Aig_ManForEachPo( p->pAig, pObj, i )
+    {
+        pSim  = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
+        pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
+        Flip  = Aig_ObjFaninC0(pObj) ? ~0 : 0;
+        for ( w = 0; w < p->nWords; w++ )
+            pSim[w] = Flip ^ pSim0[w];
+    }
+    // refine classes
+    if ( fUpdate )
+    {
+        if ( fFirst )
+        {
+            Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
+            Aig_ManForEachObj( p->pAig, pObj, i )
+                if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
+                    Vec_PtrPush( vCands, pObj );
+            assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
+            Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
+            Vec_PtrFree( vCands );
+        }
+        else
+        {
+            Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
+            Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
+        }
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
+{
+    Ssw_RarMan_t * p;
+    if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
+        return NULL;
+    p = ABC_CALLOC( Ssw_RarMan_t, 1 );
+    p->pAig      = pAig;
+    p->nWords    = nWords;
+    p->nFrames   = nFrames;
+    p->nBinSize  = nBinSize;
+    p->fVerbose  = fVerbose;
+    p->nGroups   = Aig_ManRegNum(pAig) / nBinSize;
+    p->pRarity   = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
+    p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 );
+    p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
+    p->pObjData  = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords );
+    p->pPatData  = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg );
+    p->vUpdConst = Vec_PtrAlloc( 100 );
+    p->vUpdClass = Vec_PtrAlloc( 100 );
+    p->vPatBests = Vec_IntAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ssw_RarManStop( Ssw_RarMan_t * p )
+{
+    if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
+    Vec_IntFreeP( &p->vInits );
+    Vec_IntFreeP( &p->vPatBests );
+    Vec_PtrFreeP( &p->vUpdConst );
+    Vec_PtrFreeP( &p->vUpdClass );
+    ABC_FREE( p->pObjData );
+    ABC_FREE( p->pPatData );
+    ABC_FREE( p->pPatCosts );
+    ABC_FREE( p->pRarity );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -187,32 +727,36 @@ static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
 ***********************************************************************/
 static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
 {
-    Aig_Obj_t * pObj;
-    unsigned * pData;
+//    Aig_Obj_t * pObj;
+    unsigned char * pData;
+    unsigned * pPattern;
     int i, k, Value;
 
-    // for each pattern
-    for ( k = 0; k < p->nWords * 32; k++ )
+    // more data from regs to pats
+    Ssw_RarTranspose( p );
+
+    // update counters
+    for ( k = 0; k < p->nWords * 64; k++ )
     {
+        pData = (unsigned char *)Ssw_RarPatSim( p, k );
         for ( i = 0; i < p->nGroups; i++ )
-            p->pGroupValues[i] = 0;
-        // compute its group values
-        Saig_ManForEachLi( p->pAig, pObj, i )
-        {
-            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
-            if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
-                p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
-        }
+            Ssw_RarAddToBinPat( p, i, pData[i] );
+    }
+
+    // for each pattern
+    for ( k = 0; k < p->nWords * 64; k++ )
+    {
+        pData = (unsigned char *)Ssw_RarPatSim( p, k );
         // find the cost of its values
         p->pPatCosts[k] = 0.0;
         for ( i = 0; i < p->nGroups; i++ )
         {
-            Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] );
+            Value = Ssw_RarGetBinPat( p, i, pData[i] );
             assert( Value > 0 );
             p->pPatCosts[k] += 1.0/(Value*Value);
         }
         // print the result
-//        printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
+//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
     }
 
     // choose as many as there are words
@@ -222,7 +766,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
         // select the best
         int iPatBest = -1;
         double iCostBest = -ABC_INFINITY;
-        for ( k = 0; k < p->nWords * 32; k++ )
+        for ( k = 0; k < p->nWords * 64; k++ )
             if ( iCostBest < p->pPatCosts[k] )
             {
                 iCostBest = p->pPatCosts[k];
@@ -232,12 +776,11 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
         assert( iPatBest >= 0 );
         p->pPatCosts[iPatBest] = -ABC_INFINITY;
         // set the flops
-        Saig_ManForEachLi( p->pAig, pObj, k )
-        {
-            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
-            Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
-        }
+        pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
+        for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
+            Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) );
 //printf( "Best pattern %5d\n", iPatBest );
+        Vec_IntPush( p->vPatBests, iPatBest );
     }
     assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
 }
@@ -304,11 +847,11 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
+int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
 {
     int fMiter = 1;
     Ssw_RarMan_t * p;
-    int r, clk, clkTotal = clock();
+    int r, f, clk, clkTotal = clock();
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -316,33 +859,43 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     if ( fVerbose )
-        printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", 
-            nWords, nFrames, nBinSize, nRounds, TimeOut );
+        printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
+            nWords, nFrames, nRounds, nRandSeed, TimeOut );
     // reset random numbers
-    Aig_ManRandom( 1 );
+    Ssw_RarManPrepareRandom( nRandSeed );
 
     // create manager
     p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
     p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
-    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
 
     // perform simulation rounds
     for ( r = 0; r < nRounds; r++ )
     {
         clk = clock();
         // simulate
-        Ssw_SmlSimulateOne( p->pSml );
-        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
+        for ( f = 0; f < nFrames; f++ )
         {
-            if ( fVerbose ) printf( "\n" );
-            printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
-            RetValue = 0;
-            break;
+            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
+            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
+            {
+                if ( fVerbose ) printf( "\n" );
+//                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+                Ssw_RarManPrepareRandom( nRandSeed );
+                ABC_FREE( pAig->pSeqModel );
+                pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
+                RetValue = 0;
+                goto finish;
+            }
+            // check timeout
+            if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            {
+                if ( fVerbose ) printf( "\n" );
+                printf( "Reached timeout (%d seconds).\n",  TimeOut );
+                goto finish;
+            }
         }
         // get initialization patterns
-        Ssw_RarUpdateCounters( p );
         Ssw_RarTransferPatterns( p, p->vInits );
-        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
         // printout
         if ( fVerbose )
         {
@@ -350,15 +903,9 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
 //            Abc_PrintTime( 1, "Time", clock() - clk );
             printf( "." );
         }
-        // check timeout
-        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
-        {
-            if ( fVerbose ) printf( "\n" );
-            printf( "Reached timeout (%d seconds).\n",  TimeOut );
-            break;
-        }
     }
-    if ( r == nRounds )
+finish:
+    if ( r == nRounds && f == nFrames )
     {
         if ( fVerbose ) printf( "\n" );
         printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
@@ -372,6 +919,30 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
 
 /**Function*************************************************************
 
+  Synopsis    [Perform sequential simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
+{
+    Aig_Man_t * pAig;
+    int RetValue;
+    pAig = Gia_ManToAigSimple( p );
+    RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );
+    // save counter-example
+    Abc_CexFree( p->pCexSeq );
+    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
+    Aig_ManStop( pAig );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Filter equivalence classes of nodes.]
 
   Description []
@@ -381,11 +952,10 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
-    int fMiter = 0;
     Ssw_RarMan_t * p;
-    int r, i, k, clkTotal = clock();
+    int r, f, i, k, clkTotal = clock();
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -393,10 +963,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     if ( fVerbose )
-        printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", 
-            nWords, nFrames, nBinSize, nRounds, TimeOut );
+        printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
+            nWords, nFrames, nRounds, nRandSeed, TimeOut );
     // reset random numbers
-    Aig_ManRandom( 1 );
+    Ssw_RarManPrepareRandom( nRandSeed );
 
     // create manager
     p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
@@ -411,15 +981,13 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
         for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
             Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
     assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords );
-    // initialize simulation manager
-    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
 
     // create trivial equivalence classes with all nodes being candidates for constant 1
     if ( pAig->pReprs == NULL )
         p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
     else
         p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
-    Ssw_ClassesSetData( p->ppClasses, p->pSml, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+    Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
     // print the stats
     if ( fVerbose )
     {
@@ -436,43 +1004,53 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
             break;
         }
         // simulate
-        Ssw_SmlSimulateOne( p->pSml );
-        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
+        for ( f = 0; f < nFrames; f++ )
         {
-            if ( fVerbose ) printf( "\n" );
-            printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
-            RetValue = 0;
-            break;
+            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
+            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
+            {
+                if ( !fVerbose ) 
+                    printf( "\r" );
+//                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+                Ssw_RarManPrepareRandom( nRandSeed );
+                Abc_CexFree( pAig->pSeqModel );
+                pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
+                RetValue = 0;
+                goto finish;
+            }
+            // check timeout
+            if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            {
+                if ( fVerbose ) printf( "\n" );
+                printf( "Reached timeout (%d seconds).\n",  TimeOut );
+                goto finish;
+            }
         }
-        // check equivalence classes
-        Ssw_ClassesRefineConst1( p->ppClasses, 1 );
-        Ssw_ClassesRefine( p->ppClasses, 1 );
+        // get initialization patterns
+        Ssw_RarTransferPatterns( p, p->vInits );
         // printout
         if ( fVerbose )
         {
             printf( "Round %3d:  ", r );
             Ssw_ClassesPrint( p->ppClasses, 0 );
         }
-        // get initialization patterns
-        Ssw_RarUpdateCounters( p );
-        Ssw_RarTransferPatterns( p, p->vInits );
-        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
-        // check timeout
-        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        else
         {
-            if ( fVerbose ) printf( "\n" );
-            printf( "Reached timeout (%d seconds).\n",  TimeOut );
-            break;
+            printf( "." );
         }
     }
-    if ( r == nRounds )
+finish:
+    // report
+    if ( r == nRounds && f == nFrames )
     {
+        if ( !fVerbose ) 
+            printf( "\r" );
         printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
         Abc_PrintTime( 1, "Time", clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
-    return -1;
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -486,7 +1064,7 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 { 
     Aig_Man_t * pAig;
     int RetValue;
@@ -497,15 +1075,16 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
         ABC_FREE( p->pReprs );
         ABC_FREE( p->pNexts );
     }
-    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
+    RetValue = Ssw_RarSignalFilter( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose );
     Gia_ManReprFromAigRepr( pAig, p );
+    // save counter-example
+    Abc_CexFree( p->pCexSeq );
+    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
     Aig_ManStop( pAig );
     return RetValue;
 }
 
 
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c
index 59f59f93..3026cf6b 100644
--- a/src/aig/ssw/sswRarity2.c
+++ b/src/aig/ssw/sswRarity2.c
@@ -37,26 +37,18 @@ struct Ssw_RarMan_t_
     int            nBinSize;     // the number of flops in one group
     int            fVerbose;     // the verbosiness flag
     int            nGroups;      // the number of flop groups
-    int            nWordsReg;    // the number of words in the registers
     // internal data
     Aig_Man_t *    pAig;         // AIG with equivalence classes
     Ssw_Cla_t *    ppClasses;    // equivalence classes
+    Ssw_Sml_t *    pSml;         // simulation manager
+    Vec_Ptr_t *    vSimInfo;     // simulation info from pSml manager
     Vec_Int_t *    vInits;       // initial state
-    // simulation data
-    word *         pObjData;     // simulation info for each obj
-    word *         pPatData;     // pattern data for each reg
-    // candidates to update
-    Vec_Ptr_t *    vUpdConst;    // constant 1 candidates
-    Vec_Ptr_t *    vUpdClass;    // class representatives
     // rarity data
     int *          pRarity;      // occur counts for patterns in groups
+    int *          pGroupValues; // occur counts in each group
     double *       pPatCosts;    // pattern costs
-    // best patterns
-    Vec_Int_t *    vPatBests;    // best patterns
-    int            iFailPo;      // failed primary output
-    int            iFailPat;     // failed pattern
-};
 
+};
 
 static inline int  Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) 
 {
@@ -77,63 +69,13 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
     p->pRarity[iBin * (1 << p->nBinSize) + iPat]++;
 }
 
-static inline int    Ssw_RarBitWordNum( int nBits )             { return (nBits>>6) + ((nBits&63) > 0);  }
-
-static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id )  { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id;    }
-static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id )  { assert( Id < 64 * p->nWords );            return p->pPatData + p->nWordsReg * Id; }
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares random number generator.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_RarManPrepareRandom( int nRandSeed )
-{
-    int i;
-    Aig_ManRandom( 1 );
-    for ( i = 0; i < nRandSeed; i++ )
-        Aig_ManRandom( 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Initializes random primary inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
-{
-    word * pSim;
-    Aig_Obj_t * pObj;
-    int w, i;
-    Saig_ManForEachPi( p->pAig, pObj, i )
-    {
-        pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-        for ( w = 0; w < p->nWords; w++ )
-            pSim[w] = Aig_ManRandom64(0);
-        pSim[0] <<= 1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the counter-example.]
+  Synopsis    []
 
   Description []
                
@@ -142,113 +84,29 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal )
+static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
 {
-    Abc_Cex_t * pCex;
-    Aig_Obj_t * pObj;
-    Vec_Int_t * vTrace;
-    word * pSim;
-    int i, r, f, iBit, iPatThis;
-    // compute the pattern sequence
-    iPatThis = iPatFinal;
-    vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
-    Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
-    for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
-    {
-        iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
-        Vec_IntWriteEntry( vTrace, r, iPatThis );
-    }
-    // create counter-example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
-    pCex->iFrame = iFrame;
-    pCex->iPo = iPo;
-    // insert the bits
-    iBit = Aig_ManRegNum(p->pAig);
-    for ( f = 0; f <= iFrame; f++ )
-    {
-        Ssw_RarManAssingRandomPis( p );
-        iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
-        Saig_ManForEachPi( p->pAig, pObj, i )
-        {
-            pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-            if ( Aig_InfoHasBit( (unsigned *)pSim, iPatThis ) )
-                Aig_InfoSetBit( pCex->pData, iBit );
-            iBit++;
-        }
-    }
-    Vec_IntFree( vTrace );
-    assert( iBit == pCex->nBits );
-    // verify the counter example
-    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
-    {
-        printf( "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
-        Abc_CexFree( pCex );
-        pCex = NULL;
-    }
-    else
-    {
-//      printf( "Counter-example verification is successful.\n" );
-        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
-    }
-    return pCex;
+    Ssw_RarMan_t * p;
+    if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
+        return NULL;
+    p = ABC_CALLOC( Ssw_RarMan_t, 1 );
+    p->pAig = pAig;
+    p->nWords = nWords;
+    p->nFrames = nFrames;
+    p->nBinSize = nBinSize;
+    p->fVerbose = fVerbose;
+    p->nGroups  = Aig_ManRegNum(pAig) / nBinSize;
+    p->pRarity  = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
+    p->pGroupValues = ABC_CALLOC( int, p->nGroups );
+    p->pPatCosts = ABC_CALLOC( double, p->nWords * 32 );
+    p->pSml = Ssw_SmlStart( pAig, 0, nFrames, nWords );
+    p->vSimInfo = Ssw_SmlSimDataPointers( p->pSml );
+    return p;
 }
 
-
-/**Function*************************************************************
-
-  Synopsis    [Transposing 32-bit matrix.]
-
-  Description [Borrowed from "Hacker's Delight", by Henry Warren.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void transpose32( unsigned A[32] )
-{
-    int j, k; 
-    unsigned t, m = 0x0000FFFF; 
-    for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) ) 
-    {
-        for ( k = 0; k < 32; k = (k + j + 1) & ~j )
-        {
-            t = (A[k] ^ (A[k+j] >> j)) & m;
-            A[k] = A[k] ^ t;
-            A[k+j] = A[k+j] ^ (t << j);
-        }
-    }
-} 
-
 /**Function*************************************************************
 
-  Synopsis    [Transposing 64-bit matrix.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void transpose64( word A[64] )
-{
-    int j, k; 
-    word t, m = 0x00000000FFFFFFFF; 
-    for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) ) 
-    {
-        for ( k = 0; k < 64; k = (k + j + 1) & ~j )
-        {
-            t = (A[k] ^ (A[k+j] >> j)) & m;
-            A[k] = A[k] ^ t;
-            A[k+j] = A[k+j] ^ (t << j);
-        }
-    }
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Transposing 64-bit matrix.]
+  Synopsis    []
 
   Description []
                
@@ -257,66 +115,22 @@ void transpose64( word A[64] )
   SeeAlso     []
 
 ***********************************************************************/
-void transpose64Simple( word A[64], word B[64] )
+static void Ssw_RarManStop( Ssw_RarMan_t * p )
 {
-    int i, k; 
-    for ( i = 0; i < 64; i++ )
-        B[i] = 0;
-    for ( i = 0; i < 64; i++ ) 
-    for ( k = 0; k < 64; k++ )
-        if ( (A[i] >> k) & 1 )
-            B[k] |= ((word)1 << (63-i));
+    if ( p->pSml ) Ssw_SmlStop( p->pSml );
+    if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
+    Vec_PtrFreeP( &p->vSimInfo );
+    Vec_IntFreeP( &p->vInits );
+    ABC_FREE( p->pGroupValues );
+    ABC_FREE( p->pPatCosts );
+    ABC_FREE( p->pRarity );
+    ABC_FREE( p );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Testing the transposing code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void TransposeTest()
-{
-    word M[64], N[64];
-    int i, clk;
-    Aig_ManRandom64( 1 );
-//    for ( i = 0; i < 64; i++ )
-//        M[i] = Aig_ManRandom64( 0 );
-    for ( i = 0; i < 64; i++ )
-        M[i] = i? (word)0 : ~(word)0;
-//    for ( i = 0; i < 64; i++ )
-//        Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
-
-    clk = clock();
-    for ( i = 0; i < 100001; i++ )
-        transpose64Simple( M, N );
-    Abc_PrintTime( 1, "Time", clock() - clk );
-
-    clk = clock();
-    for ( i = 0; i < 100001; i++ )
-        transpose64( M );
-    Abc_PrintTime( 1, "Time", clock() - clk );
-
-    for ( i = 0; i < 64; i++ )
-        if ( M[i] != N[i] )
-            printf( "Mismatch\n" );
-/*
-    printf( "\n" );
-    for ( i = 0; i < 64; i++ )
-        Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
-    printf( "\n" );
-    for ( i = 0; i < 64; i++ )
-        Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\n" );
-*/
-}
 
 /**Function*************************************************************
 
-  Synopsis    [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].]
+  Synopsis    [Updates rarity counters.]
 
   Description []
                
@@ -325,393 +139,39 @@ void TransposeTest()
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_RarTranspose( Ssw_RarMan_t * p )
+static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
 {
     Aig_Obj_t * pObj;
-    word M[64];
-    int w, r, i;
-    for ( w = 0; w < p->nWords; w++ )
-    for ( r = 0; r < p->nWordsReg; r++ )
-    {
-        // save input
-        for ( i = 0; i < 64; i++ )
-        {
-            if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
-            {
-                pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
-                M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
-            }
-            else
-                M[i] = 0;
-        }
-        // transpose
-        transpose64( M );
-        // save output
-        for ( i = 0; i < 64; i++ )
-            Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
-    }
+    unsigned * pData;
+    int i, k;
 /*
     Saig_ManForEachLi( p->pAig, pObj, i )
     {
-        word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-        Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); printf( "\n" );
+        pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
+        Extra_PrintBinary( stdout, pData, 32 );  printf( "\n" );
     }
-    printf( "\n" );
-    for ( i = 0; i < p->nWords*64; i++ )
-    {
-        word * pBitData = Ssw_RarPatSim( p, i );
-        Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
-    }
-    printf( "\n" );
 */
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Sets random inputs and specialied flop outputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
-{
-    Aig_Obj_t * pObj, * pObjLi;
-    word * pSim, * pSimLi;
-    int w, i;
-    // constant
-    pObj = Aig_ManConst1( p->pAig );
-    pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-    for ( w = 0; w < p->nWords; w++ )
-        pSim[w] = ~(word)0;
-    // primary inputs
-    Ssw_RarManAssingRandomPis( p );
-    // flop outputs
-    if ( vInit )
-    {
-        assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords );
-        Saig_ManForEachLo( p->pAig, pObj, i )
-        {
-            pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-            for ( w = 0; w < p->nWords; w++ )
-                pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
-        }
-    }
-    else
-    {
-        Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
-        {
-            pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
-            pSim   = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-            for ( w = 0; w < p->nWords; w++ )
-                pSim[w] = pSimLi[w];
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
-{
-    word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-    word Flip = pObj->fPhase ? ~0 : 0;
-    int w;
-    for ( w = 0; w < p->nWords; w++ )
-        if ( pSim[w] ^ Flip )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation infos are equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_RarManObjsAreEqual( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
-    word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
-    word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
-    word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0;
-    int w;
-    for ( w = 0; w < p->nWords; w++ )
-        if ( pSim0[w] ^ pSim1[w] ^ Flip )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes hash value of the node using its simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ssw_RarManObjHashWord( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
-{
-    static int s_SPrimes[128] = { 
-        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
-        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
-        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
-        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
-        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
-        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
-        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
-        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
-        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
-        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
-        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
-        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
-        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
-    };
-    unsigned * pSims;
-    unsigned uHash;
-    int i;
-    uHash = 0;
-    pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
-    for ( i = 0; i < 2 * p->nWords; i++ )
-        uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
-    return uHash;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
-{
-    word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-    word Flip = pObj->fPhase ? ~0 : 0;
-    int w, i;
-    for ( w = 0; w < p->nWords; w++ )
-        if ( pSim[w] ^ Flip )
-        {
-            for ( i = 0; i < 64; i++ )
-                if ( ((pSim[w] ^ Flip) >> i) & 1 )
-                    break;
-            assert( i < 64 );
-            return w * 64 + i;
-        }
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check if any of the POs becomes non-constant.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    p->iFailPo  = -1;
-    p->iFailPat = -1;
-    Saig_ManForEachPo( p->pAig, pObj, i )
+    for ( k = 0; k < p->nWords * 32; k++ )
     {
-        if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
-            return 0;
-        if ( !Ssw_RarManObjIsConst(p, pObj) )
-        {
-            p->iFailPo  = i;
-            p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
-            return 1;
-        }
-    }
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one round of simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
-{
-    Aig_Obj_t * pObj, * pRepr;
-    word * pSim, * pSim0, * pSim1;
-    word Flip, Flip0, Flip1;
-    int w, i;
-    // initialize 
-    Ssw_RarManInitialize( p, vInit );
-    Vec_PtrClear( p->vUpdConst );
-    Vec_PtrClear( p->vUpdClass );
-    Aig_ManIncrementTravId( p->pAig );
-    // check comb inputs
-    if ( fUpdate )
-    Aig_ManForEachPi( p->pAig, pObj, i )
-    {
-        pRepr = Aig_ObjRepr(p->pAig, pObj);
-        if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
-            continue;
-        if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
-            continue;
-        // save for update
-        if ( pRepr == Aig_ManConst1(p->pAig) )
-            Vec_PtrPush( p->vUpdConst, pObj );
-        else
-        {
-            Vec_PtrPush( p->vUpdClass, pRepr );
-            Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
-        }
-    }
-    // simulate 
-    Aig_ManForEachNode( p->pAig, pObj, i )
-    {
-        pSim  = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-        pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
-        pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
-        Flip0 = Aig_ObjFaninC0(pObj) ? ~0 : 0;
-        Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0;
-        for ( w = 0; w < p->nWords; w++ )
-            pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
-        if ( !fUpdate )
-            continue;
-        // check classes
-        pRepr = Aig_ObjRepr(p->pAig, pObj);
-        if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
-            continue;
-        if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
-            continue;
-        // save for update
-        if ( pRepr == Aig_ManConst1(p->pAig) )
-            Vec_PtrPush( p->vUpdConst, pObj );
-        else
+        for ( i = 0; i < p->nGroups; i++ )
+            p->pGroupValues[i] = 0;
+        Saig_ManForEachLi( p->pAig, pObj, i )
         {
-            Vec_PtrPush( p->vUpdClass, pRepr );
-            Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
+            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
+            if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
+                p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
         }
+        for ( i = 0; i < p->nGroups; i++ )
+            Ssw_RarAddToBinPat( p, i, p->pGroupValues[i] );
     }
-    // transfer to POs
-    Aig_ManForEachPo( p->pAig, pObj, i )
+/*
+    for ( i = 0; i < p->nGroups; i++ )
     {
-        pSim  = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
-        pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
-        Flip  = Aig_ObjFaninC0(pObj) ? ~0 : 0;
-        for ( w = 0; w < p->nWords; w++ )
-            pSim[w] = Flip ^ pSim0[w];
+        for ( k = 0; k < (1 << p->nBinSize); k++ )
+            printf( "%d ", Ssw_RarGetBinPat(p, i, k) );
+        printf( "\n" );
     }
-    // refine classes
-    if ( fUpdate )
-    {
-        if ( fFirst )
-        {
-            Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
-            Aig_ManForEachObj( p->pAig, pObj, i )
-                if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
-                    Vec_PtrPush( vCands, pObj );
-            assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
-            Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
-            Vec_PtrFree( vCands );
-        }
-        else
-        {
-            Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
-            Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
-{
-    Ssw_RarMan_t * p;
-    if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
-        return NULL;
-    p = ABC_CALLOC( Ssw_RarMan_t, 1 );
-    p->pAig      = pAig;
-    p->nWords    = nWords;
-    p->nFrames   = nFrames;
-    p->nBinSize  = nBinSize;
-    p->fVerbose  = fVerbose;
-    p->nGroups   = Aig_ManRegNum(pAig) / nBinSize;
-    p->pRarity   = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
-    p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 );
-    p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
-    p->pObjData  = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords );
-    p->pPatData  = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg );
-    p->vUpdConst = Vec_PtrAlloc( 100 );
-    p->vUpdClass = Vec_PtrAlloc( 100 );
-    p->vPatBests = Vec_IntAlloc( 100 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ssw_RarManStop( Ssw_RarMan_t * p )
-{
-    if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
-    Vec_IntFreeP( &p->vInits );
-    Vec_IntFreeP( &p->vPatBests );
-    Vec_PtrFreeP( &p->vUpdConst );
-    Vec_PtrFreeP( &p->vUpdClass );
-    ABC_FREE( p->pObjData );
-    ABC_FREE( p->pPatData );
-    ABC_FREE( p->pPatCosts );
-    ABC_FREE( p->pRarity );
-    ABC_FREE( p );
+*/
 }
 
 /**Function*************************************************************
@@ -727,36 +187,32 @@ static void Ssw_RarManStop( Ssw_RarMan_t * p )
 ***********************************************************************/
 static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
 {
-//    Aig_Obj_t * pObj;
-    unsigned char * pData;
-    unsigned * pPattern;
+    Aig_Obj_t * pObj;
+    unsigned * pData;
     int i, k, Value;
 
-    // more data from regs to pats
-    Ssw_RarTranspose( p );
-
-    // update counters
-    for ( k = 0; k < p->nWords * 64; k++ )
-    {
-        pData = (unsigned char *)Ssw_RarPatSim( p, k );
-        for ( i = 0; i < p->nGroups; i++ )
-            Ssw_RarAddToBinPat( p, i, pData[i] );
-    }
-
     // for each pattern
-    for ( k = 0; k < p->nWords * 64; k++ )
+    for ( k = 0; k < p->nWords * 32; k++ )
     {
-        pData = (unsigned char *)Ssw_RarPatSim( p, k );
+        for ( i = 0; i < p->nGroups; i++ )
+            p->pGroupValues[i] = 0;
+        // compute its group values
+        Saig_ManForEachLi( p->pAig, pObj, i )
+        {
+            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
+            if ( Aig_InfoHasBit(pData, k) && i / p->nBinSize < p->nGroups )
+                p->pGroupValues[i / p->nBinSize] |= (1 << (i % p->nBinSize));
+        }
         // find the cost of its values
         p->pPatCosts[k] = 0.0;
         for ( i = 0; i < p->nGroups; i++ )
         {
-            Value = Ssw_RarGetBinPat( p, i, pData[i] );
+            Value = Ssw_RarGetBinPat( p, i, p->pGroupValues[i] );
             assert( Value > 0 );
             p->pPatCosts[k] += 1.0/(Value*Value);
         }
         // print the result
-//printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
+//        printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
     }
 
     // choose as many as there are words
@@ -766,7 +222,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
         // select the best
         int iPatBest = -1;
         double iCostBest = -ABC_INFINITY;
-        for ( k = 0; k < p->nWords * 64; k++ )
+        for ( k = 0; k < p->nWords * 32; k++ )
             if ( iCostBest < p->pPatCosts[k] )
             {
                 iCostBest = p->pPatCosts[k];
@@ -776,11 +232,12 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
         assert( iPatBest >= 0 );
         p->pPatCosts[iPatBest] = -ABC_INFINITY;
         // set the flops
-        pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
-        for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
-            Vec_IntPush( vInits, Aig_InfoHasBit(pPattern, k) );
+        Saig_ManForEachLi( p->pAig, pObj, k )
+        {
+            pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
+            Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
+        }
 //printf( "Best pattern %5d\n", iPatBest );
-        Vec_IntPush( p->vPatBests, iPatBest );
     }
     assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
 }
@@ -847,11 +304,11 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
+int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
 {
     int fMiter = 1;
     Ssw_RarMan_t * p;
-    int r, f, clk, clkTotal = clock();
+    int r, clk, clkTotal = clock();
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -859,43 +316,33 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     if ( fVerbose )
-        printf( "Rarity simulation with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
-            nWords, nFrames, nRounds, nRandSeed, TimeOut );
+        printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", 
+            nWords, nFrames, nBinSize, nRounds, TimeOut );
     // reset random numbers
-    Ssw_RarManPrepareRandom( nRandSeed );
+    Aig_ManRandom( 1 );
 
     // create manager
     p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
     p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
+    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
 
     // perform simulation rounds
     for ( r = 0; r < nRounds; r++ )
     {
         clk = clock();
         // simulate
-        for ( f = 0; f < nFrames; f++ )
+        Ssw_SmlSimulateOne( p->pSml );
+        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
         {
-            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
-            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
-            {
-                if ( fVerbose ) printf( "\n" );
-//                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
-                Ssw_RarManPrepareRandom( nRandSeed );
-                ABC_FREE( pAig->pSeqModel );
-                pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
-                RetValue = 0;
-                goto finish;
-            }
-            // check timeout
-            if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
-            {
-                if ( fVerbose ) printf( "\n" );
-                printf( "Reached timeout (%d seconds).\n",  TimeOut );
-                goto finish;
-            }
+            if ( fVerbose ) printf( "\n" );
+            printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+            RetValue = 0;
+            break;
         }
         // get initialization patterns
+        Ssw_RarUpdateCounters( p );
         Ssw_RarTransferPatterns( p, p->vInits );
+        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
         // printout
         if ( fVerbose )
         {
@@ -903,9 +350,15 @@ int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, i
 //            Abc_PrintTime( 1, "Time", clock() - clk );
             printf( "." );
         }
+        // check timeout
+        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+        {
+            if ( fVerbose ) printf( "\n" );
+            printf( "Reached timeout (%d seconds).\n",  TimeOut );
+            break;
+        }
     }
-finish:
-    if ( r == nRounds && f == nFrames )
+    if ( r == nRounds )
     {
         if ( fVerbose ) printf( "\n" );
         printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
@@ -919,30 +372,6 @@ finish:
 
 /**Function*************************************************************
 
-  Synopsis    [Perform sequential simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose )
-{
-    Aig_Man_t * pAig;
-    int RetValue;
-    pAig = Gia_ManToAigSimple( p );
-    RetValue = Ssw_RarSimulate2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );
-    // save counter-example
-    Abc_CexFree( p->pCexSeq );
-    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
-    Aig_ManStop( pAig );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Filter equivalence classes of nodes.]
 
   Description []
@@ -952,10 +381,11 @@ int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, i
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 {
+    int fMiter = 0;
     Ssw_RarMan_t * p;
-    int r, f, i, k, clkTotal = clock();
+    int r, i, k, clkTotal = clock();
     int RetValue = -1;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
@@ -963,10 +393,10 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
     if ( fVerbose )
-        printf( "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n", 
-            nWords, nFrames, nRounds, nRandSeed, TimeOut );
+        printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n", 
+            nWords, nFrames, nBinSize, nRounds, TimeOut );
     // reset random numbers
-    Ssw_RarManPrepareRandom( nRandSeed );
+    Aig_ManRandom( 1 );
 
     // create manager
     p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
@@ -981,13 +411,15 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
         for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
             Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
     assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * nWords );
+    // initialize simulation manager
+    Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
 
     // create trivial equivalence classes with all nodes being candidates for constant 1
     if ( pAig->pReprs == NULL )
         p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
     else
         p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
-    Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
+    Ssw_ClassesSetData( p->ppClasses, p->pSml, NULL, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
     // print the stats
     if ( fVerbose )
     {
@@ -1004,53 +436,43 @@ int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSiz
             break;
         }
         // simulate
-        for ( f = 0; f < nFrames; f++ )
+        Ssw_SmlSimulateOne( p->pSml );
+        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
         {
-            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
-            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
-            {
-                if ( !fVerbose ) 
-                    printf( "\r" );
-//                printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
-                Ssw_RarManPrepareRandom( nRandSeed );
-                Abc_CexFree( pAig->pSeqModel );
-                pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat );
-                RetValue = 0;
-                goto finish;
-            }
-            // check timeout
-            if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
-            {
-                if ( fVerbose ) printf( "\n" );
-                printf( "Reached timeout (%d seconds).\n",  TimeOut );
-                goto finish;
-            }
+            if ( fVerbose ) printf( "\n" );
+            printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+            RetValue = 0;
+            break;
         }
-        // get initialization patterns
-        Ssw_RarTransferPatterns( p, p->vInits );
+        // check equivalence classes
+        Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+        Ssw_ClassesRefine( p->ppClasses, 1 );
         // printout
         if ( fVerbose )
         {
             printf( "Round %3d:  ", r );
             Ssw_ClassesPrint( p->ppClasses, 0 );
         }
-        else
+        // get initialization patterns
+        Ssw_RarUpdateCounters( p );
+        Ssw_RarTransferPatterns( p, p->vInits );
+        Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
+        // check timeout
+        if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
         {
-            printf( "." );
+            if ( fVerbose ) printf( "\n" );
+            printf( "Reached timeout (%d seconds).\n",  TimeOut );
+            break;
         }
     }
-finish:
-    // report
-    if ( r == nRounds && f == nFrames )
+    if ( r == nRounds )
     {
-        if ( !fVerbose ) 
-            printf( "\r" );
         printf( "Simulation did not assert POs in the first %d frames.  ", nRounds * nFrames );
         Abc_PrintTime( 1, "Time", clock() - clkTotal );
     }
     // cleanup
     Ssw_RarManStop( p );
-    return RetValue;
+    return -1;
 }
 
 /**Function*************************************************************
@@ -1064,7 +486,7 @@ finish:
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
+int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
 { 
     Aig_Man_t * pAig;
     int RetValue;
@@ -1075,16 +497,15 @@ int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSiz
         ABC_FREE( p->pReprs );
         ABC_FREE( p->pNexts );
     }
-    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, pCex, fLatchOnly, fVerbose );
+    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
     Gia_ManReprFromAigRepr( pAig, p );
-    // save counter-example
-    Abc_CexFree( p->pCexSeq );
-    p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
     Aig_ManStop( pAig );
     return RetValue;
 }
 
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e319c4f8..ee0c98ff 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24776,7 +24776,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nRandSeed;
     int TimeOut;
     int fVerbose;
-    extern int Ssw_RarSimulate2Gia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
+    extern int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fVerbose );
     // set defaults
     nFrames    =  20;
     nWords     =  50;
@@ -24871,7 +24871,7 @@ int Abc_CommandAbc9Sim3( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Sim3(): There is no AIG.\n" );
         return 1;
     }
-    pAbc->Status = Ssw_RarSimulate2Gia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );  
+    pAbc->Status = Ssw_RarSimulateGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose );  
 //    pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
@@ -25310,7 +25310,7 @@ usage:
 int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
 //    extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-    extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
+    extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
     int c;
     int nFrames    =   20;
     int nWords     =   50;
@@ -25435,7 +25435,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 //    if ( fNewAlgo )
-        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
+        pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fMiter, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
 //    else
 //        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
 //    pAbc->nFrames = pAbc->pGia->pCexSeq->iFrame;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4232ab1f..695ae4ef 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3027,53 +3027,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
         Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
     }
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( Ssw_RarSimulate2( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 )
-    { 
-        if ( pMan->pSeqModel )
-        {
-            printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
-                nFrames, nWords, pMan->pSeqModel->iPo, pMan->pSeqModel->iFrame );
-            status = Saig_ManVerifyCex( pMan, pMan->pSeqModel );
-            if ( status == 0 )
-                printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
-        }
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-        RetValue = 0;
-    }
-    else
-    {
-        printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
-            nFrames, nWords );
-    }
-    ABC_PRT( "Time", clock() - clk );
-    Aig_ManStop( pMan );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs random simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
-{
-    Aig_Man_t * pMan;
-    int status, RetValue = -1, clk = clock();
-    if ( Abc_NtkGetChoiceNum(pNtk) )
-    {
-        printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pNtk) );
-        Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
-    }
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( Ssw_RarSignalFilter( pMan, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose ) == 0 )
+    if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRandSeed, TimeOut, fVerbose ) == 0 )
     { 
         if ( pMan->pSeqModel )
         {