Changes to enable smarter simulation.

5 files changed, 980 insertions, 83 deletions

diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 3870d4ff..7632d923 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -118,6 +118,9 @@ 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 TimeOut, 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 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/sswClass.c b/src/aig/ssw/sswClass.c
index a0e64cc0..51514f47 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -1041,6 +1041,26 @@ int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive )
 
 /**Function*************************************************************
 
+  Synopsis    [Refines the classes after simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )
+{
+    Aig_Obj_t * pObj;
+    int i, nRefis = 0;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
+        nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
+    return nRefis;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Refine the group of constant 1 nodes.]
 
   Description []
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 32959e85..93e828a1 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -226,6 +226,7 @@ extern Ssw_Cla_t *   Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
 extern Ssw_Cla_t *   Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
 extern Ssw_Cla_t *   Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
 extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
+extern int           Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
 extern int           Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
 extern int           Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
diff --git a/src/aig/ssw/sswRarity.c b/src/aig/ssw/sswRarity.c
index 5b262d91..5657908e 100644
--- a/src/aig/ssw/sswRarity.c
+++ b/src/aig/ssw/sswRarity.c
@@ -84,7 +84,7 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
+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 )
@@ -115,7 +115,7 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_RarManStop( Ssw_RarMan_t * p )
+static void Ssw_RarManStop( Ssw_RarMan_t * p )
 {
     if ( p->pSml ) Ssw_SmlStop( p->pSml );
     if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
@@ -139,7 +139,7 @@ void Ssw_RarManStop( Ssw_RarMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
+static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
 {
     Aig_Obj_t * pObj;
     unsigned * pData;
@@ -185,7 +185,7 @@ void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
+static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
 {
     Aig_Obj_t * pObj;
     unsigned * pData;
@@ -214,7 +214,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
         }
 //        printf( "\n" );
         // 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
@@ -239,8 +239,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
             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 );
-
+printf( "Best pattern %5d\n", iPatBest );
     }
     assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
 }
@@ -257,7 +256,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
 { 
     Vec_Int_t * vInit;
     Aig_Obj_t * pObj, * pObjLi;
@@ -295,6 +294,84 @@ Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
     return vInit;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Perform sequential simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_RarSimulate( 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, clk, clkTotal = clock();
+    int RetValue = -1;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManConstrNum(pAig) == 0 );
+    // consider the case of empty AIG
+    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 );
+    // reset random numbers
+    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
+        Ssw_SmlSimulateOne( p->pSml );
+        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
+        {
+            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 )
+        {
+//            printf( "Round %3d:  ", r );
+//            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 )
+    {
+        if ( fVerbose ) printf( "\n" );
+        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;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Filter equivalence classes of nodes.]
@@ -430,81 +507,6 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Perform sequential simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ssw_RarSimulate( 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, clk, clkTotal = clock();
-    int RetValue = -1;
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManConstrNum(pAig) == 0 );
-    // consider the case of empty AIG
-    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 );
-    // reset random numbers
-    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
-        Ssw_SmlSimulateOne( p->pSml );
-        if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
-        {
-            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 )
-        {
-//            printf( "Round %3d:  ", r );
-//            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 )
-    {
-        if ( fVerbose ) printf( "\n" );
-        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;
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ssw/sswRarity2.c b/src/aig/ssw/sswRarity2.c
new file mode 100644
index 00000000..b8fefe65
--- /dev/null
+++ b/src/aig/ssw/sswRarity2.c
@@ -0,0 +1,871 @@
+/**CFile****************************************************************
+
+  FileName    [sswRarity.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Rarity-driven refinement of equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
+struct Ssw_RarMan_t_
+{
+    // parameters
+    int            nWords;       // the number of words to simulate
+    int            nFrames;      // the number of frames to simulate
+    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
+    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
+    double *       pPatCosts;    // pattern costs
+    // best patterns
+    Vec_Int_t *    vPatBests;    // best patterns
+};
+
+
+static inline int  Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) 
+{
+    assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
+    assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
+    return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
+}
+static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value ) 
+{
+    assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
+    assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
+    p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
+}
+static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat ) 
+{
+    assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
+    assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
+    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    [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.]
+
+  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;
+    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 )
+    {
+        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" );
+*/
+}
+
+
+
+
+/**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
+    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);
+    }
+    // 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 );
+        }
+    }
+    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    [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;
+    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) )
+            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 )
+{
+    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 )
+    {
+        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*************************************************************
+
+  Synopsis    [Select best patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
+{
+//    Aig_Obj_t * pObj;
+    unsigned char * pData;
+    unsigned * pPattern;
+    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++ )
+    {
+        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, pData[i] );
+            assert( Value > 0 );
+            p->pPatCosts[k] += 1.0/(Value*Value);
+//            printf( "%d ", Value );
+        }
+//        printf( "\n" );
+        // print the result
+        printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
+    }
+
+    // choose as many as there are words
+    Vec_IntClear( vInits );
+    for ( i = 0; i < p->nWords; i++ )
+    {
+        // select the best
+        int iPatBest = -1;
+        double iCostBest = -ABC_INFINITY;
+        for ( k = 0; k < p->nWords * 64; k++ )
+            if ( iCostBest < p->pPatCosts[k] )
+            {
+                iCostBest = p->pPatCosts[k];
+                iPatBest  = k;
+            }
+        // remove from costs
+        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) );
+printf( "Best pattern %5d\n", iPatBest );
+        Vec_IntPush( p->vPatBests, iPatBest );
+    }
+    assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+{ 
+    Vec_Int_t * vInit;
+    Aig_Obj_t * pObj, * pObjLi;
+    int f, i, iBit;
+    // assign register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        pObj->fMarkB = 0;
+    // simulate the timeframes
+    iBit = pCex->nRegs;
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        // set the PI simulation information
+        Aig_ManConst1(pAig)->fMarkB = 1;
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->fMarkB = Aig_InfoHasBit( pCex->pData, iBit++ );
+        Saig_ManForEachLiLo( pAig, pObjLi, pObj, i )
+            pObj->fMarkB = pObjLi->fMarkB;
+        // simulate internal nodes
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                         & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+        // assign the COs
+        Aig_ManForEachPo( pAig, pObj, i )
+            pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
+    }
+    assert( iBit == pCex->nBits );
+    // check that the output failed as expected -- cannot check because it is not an SRM!
+//    pObj = Aig_ManPo( pAig, pCex->iPo );
+//    if ( pObj->fMarkB != 1 )
+//        printf( "The counter-example does not refine the output.\n" );
+    // record the new pattern
+    vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
+    Saig_ManForEachLo( pAig, pObj, i )
+        Vec_IntPush( vInit, pObj->fMarkB );
+    return vInit;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Perform sequential simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 RetValue = -1;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManConstrNum(pAig) == 0 );
+    // consider the case of empty AIG
+    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 );
+    // reset random numbers
+    Aig_ManRandom( 1 );
+
+    // create manager
+    p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
+    p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
+
+    // perform simulation rounds
+    for ( r = 0; r < nRounds; r++ )
+    {
+        clk = clock();
+        // simulate
+        for ( f = 0; f < nFrames; f++ )
+        {
+            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 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 );
+                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_RarTransferPatterns( p, p->vInits );
+        // printout
+        if ( fVerbose )
+        {
+//            printf( "Round %3d:  ", r );
+//            Abc_PrintTime( 1, "Time", clock() - clk );
+            printf( "." );
+        }
+    }
+finish:
+    if ( r == nRounds )
+    {
+        if ( fVerbose ) printf( "\n" );
+        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;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Filter equivalence classes of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  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 fMiter = 0;
+    Ssw_RarMan_t * p;
+    int r, f, i, k, clkTotal = clock();
+    int RetValue = -1;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManConstrNum(pAig) == 0 );
+    // consider the case of empty AIG
+    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 );
+    // reset random numbers
+    Aig_ManRandom( 1 );
+
+    // create manager
+    p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
+    // compute starting state if needed
+    assert( p->vInits == NULL );
+    if ( pCex )
+        p->vInits = Ssw_RarFindStartingState( pAig, pCex );
+    else
+        p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
+    // duplicate the array
+    for ( i = 1; i < nWords; i++ )
+        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 );
+
+    // 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, NULL, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
+    // print the stats
+    if ( fVerbose )
+    {
+        printf( "Initial  :  " );
+        Ssw_ClassesPrint( p->ppClasses, 0 );
+    }
+    // refine classes using BMC
+    for ( r = 0; r < nRounds; r++ )
+    {
+        // start filtering equivalence classes
+        if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
+        {
+            printf( "All equivalences are refined away.\n" );
+            break;
+        }
+        // simulate
+        for ( f = 0; f < nFrames; f++ )
+        {
+            Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1 );
+            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 );
+                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;
+            }
+        }
+        // printout
+        if ( fVerbose )
+        {
+            printf( "Round %3d:  ", r );
+            Ssw_ClassesPrint( p->ppClasses, 0 );
+        }
+        // get initialization patterns
+        Ssw_RarTransferPatterns( p, p->vInits );
+    }
+finish:
+    // report
+    if ( r == nRounds )
+    {
+        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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Filter equivalence classes of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  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 )
+{ 
+    Aig_Man_t * pAig;
+    int RetValue;
+    pAig = Gia_ManToAigSimple( p );
+    if ( p->pReprs != NULL )
+    {
+        Gia_ManReprToAigRepr2( pAig, p );
+        ABC_FREE( p->pReprs );
+        ABC_FREE( p->pNexts );
+    }
+    RetValue = Ssw_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
+    Gia_ManReprFromAigRepr( pAig, p );
+    Aig_ManStop( pAig );
+    return RetValue;
+}
+
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+