Major restructuring of the code.

9 files changed, 1936 insertions, 0 deletions

diff --git a/src/opt/fsim/fsim.h b/src/opt/fsim/fsim.h
new file mode 100644
index 00000000..5a17550b
--- /dev/null
+++ b/src/opt/fsim/fsim.h
@@ -0,0 +1,101 @@
+/**CFile****************************************************************
+
+  FileName    [fsim.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__fsim__fsim_h
+#define ABC__aig__fsim__fsim_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Fsim_Man_t_ Fsim_Man_t;
+
+// simulation parameters
+typedef struct Fsim_ParSim_t_ Fsim_ParSim_t;
+struct Fsim_ParSim_t_
+{
+    // user-controlled parameters
+    int             nWords;       // the number of machine words
+    int             nIters;       // the number of timeframes
+    int             TimeLimit;    // time limit in seconds
+    int             fCheckMiter;  // check if miter outputs are non-zero
+    int             fVerbose;     // enables verbose output
+    // internal parameters
+    int             fCompressAig; // compresses internal data
+};
+
+// switching estimation parameters
+typedef struct Fsim_ParSwitch_t_ Fsim_ParSwitch_t;
+struct Fsim_ParSwitch_t_
+{
+    // user-controlled parameters
+    int             nWords;       // the number of machine words
+    int             nIters;       // the number of timeframes
+    int             nPref;        // the number of first timeframes to skip
+    int             nRandPiNum;   // PI trans prob (0=1/2; 1=1/4; 2=1/8, etc)
+    int             fProbOne;     // collect probability of one
+    int             fProbTrans;   // collect probatility of switching
+    int             fVerbose;     // enables verbose output
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== fsimCore.c ==========================================================*/
+extern void           Fsim_ManSetDefaultParamsSim( Fsim_ParSim_t * p );
+extern void           Fsim_ManSetDefaultParamsSwitch( Fsim_ParSwitch_t * p );
+/*=== fsimSim.c ==========================================================*/
+extern int            Fsim_ManSimulate( Aig_Man_t * pAig, Fsim_ParSim_t * pPars );
+/*=== fsimSwitch.c ==========================================================*/
+extern Vec_Int_t *    Fsim_ManSwitchSimulate( Aig_Man_t * pAig, Fsim_ParSwitch_t * pPars );
+/*=== fsimTsim.c ==========================================================*/
+extern Vec_Ptr_t *    Fsim_ManTerSimulate( Aig_Man_t * pAig, int fVerbose );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/fsim/fsimCore.c b/src/opt/fsim/fsimCore.c
new file mode 100644
index 00000000..9516f09e
--- /dev/null
+++ b/src/opt/fsim/fsimCore.c
@@ -0,0 +1,88 @@
+/**CFile****************************************************************
+
+  FileName    [fsimCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fsimInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManSetDefaultParamsSim( Fsim_ParSim_t * p )
+{
+    memset( p, 0, sizeof(Fsim_ParSim_t) );
+    // user-controlled parameters
+    p->nWords       =   8;    // the number of machine words
+    p->nIters       =  32;    // the number of timeframes
+    p->TimeLimit    =  60;    // time limit in seconds
+    p->fCheckMiter  =   0;    // check if miter outputs are non-zero 
+    p->fVerbose     =   1;    // enables verbose output
+    // internal parameters
+    p->fCompressAig =   0;    // compresses internal data
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManSetDefaultParamsSwitch( Fsim_ParSwitch_t * p )
+{
+    memset( p, 0, sizeof(Fsim_ParSwitch_t) );
+    // user-controlled parameters
+    p->nWords       =   1;    // the number of machine words
+    p->nIters       =  48;    // the number of timeframes
+    p->nPref        =  16;    // the number of first timeframes to skip
+    p->nRandPiNum   =   0;    // PI trans prob (0=1/2; 1=1/4; 2=1/8, etc)
+    p->fProbOne     =   1;    // collect probability of one
+    p->fProbTrans   =   1;    // collect probatility of switching
+    p->fVerbose     =   1;    // enables verbose output
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fsim/fsimFront.c b/src/opt/fsim/fsimFront.c
new file mode 100644
index 00000000..6169543c
--- /dev/null
+++ b/src/opt/fsim/fsimFront.c
@@ -0,0 +1,369 @@
+/**CFile****************************************************************
+
+  FileName    [fsimFront.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Simulation frontier.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimFront.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fsimInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManStoreNum( Fsim_Man_t * p, int Num )
+{
+    unsigned x = (unsigned)Num;
+    assert( Num >= 0 );
+    while ( x & ~0x7f )
+    {
+        *p->pDataCur++ = (x & 0x7f) | 0x80;
+        x >>= 7;
+    }
+    *p->pDataCur++ = x;
+    assert( p->pDataCur - p->pDataAig < p->nDataAig );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManRestoreNum( Fsim_Man_t * p )
+{
+    int ch, i, x = 0;
+    for ( i = 0; (ch = *p->pDataCur++) & 0x80; i++ )
+        x |= (ch & 0x7f) << (7 * i);
+    assert( p->pDataCur - p->pDataAig < p->nDataAig );
+    return x | (ch << (7 * i));
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManStoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj )
+{
+    if ( p->pDataAig2 )
+    {
+        *p->pDataCur2++ = pObj->iNode;
+        *p->pDataCur2++ = pObj->iFan0;
+        *p->pDataCur2++ = pObj->iFan1;
+        return;
+    }
+    if ( pObj->iFan0 && pObj->iFan1 ) // and
+    {
+        assert( pObj->iNode );
+        assert( pObj->iNode >= p->iNodePrev );
+        assert( (pObj->iNode << 1) > pObj->iFan0 );
+        assert( pObj->iFan0 > pObj->iFan1 );
+        Fsim_ManStoreNum( p, ((pObj->iNode - p->iNodePrev) << 2) | 3 );
+        Fsim_ManStoreNum( p, (pObj->iNode << 1) - pObj->iFan0 );
+        Fsim_ManStoreNum( p, pObj->iFan0 - pObj->iFan1 );
+        p->iNodePrev = pObj->iNode;
+    }
+    else if ( !pObj->iFan0 && !pObj->iFan1 ) // ci
+    {
+        assert( pObj->iNode );
+        assert( pObj->iNode >= p->iNodePrev );
+        Fsim_ManStoreNum( p, ((pObj->iNode - p->iNodePrev) << 2) | 1 );
+        p->iNodePrev = pObj->iNode;
+    }
+    else // if ( !pObj->iFan0 && pObj->iFan1 ) // co
+    {
+        assert( pObj->iNode == 0 );
+        assert( pObj->iFan0 != 0 );
+        assert( pObj->iFan1 == 0 );
+        assert( ((p->iNodePrev << 1) | 1) >= pObj->iFan0 );
+        Fsim_ManStoreNum( p, (((p->iNodePrev << 1) | 1) - pObj->iFan0) << 1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManRestoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj )
+{
+    int iValue = Fsim_ManRestoreNum( p );
+    if ( (iValue & 3) == 3 ) // and
+    {
+        pObj->iNode = (iValue >> 2) + p->iNodePrev;
+        pObj->iFan0 = (pObj->iNode << 1) - Fsim_ManRestoreNum( p );
+        pObj->iFan1 = pObj->iFan0 - Fsim_ManRestoreNum( p );
+        p->iNodePrev = pObj->iNode;
+    }
+    else if ( (iValue & 3) == 1 ) // ci
+    {
+        pObj->iNode = (iValue >> 2) + p->iNodePrev;
+        pObj->iFan0 = 0;
+        pObj->iFan1 = 0;
+        p->iNodePrev = pObj->iNode;
+    }
+    else // if ( (iValue & 1) == 0 ) // co
+    {
+        pObj->iNode = 0;
+        pObj->iFan0 = ((p->iNodePrev << 1) | 1) - (iValue >> 1);
+        pObj->iFan1 = 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManFrontFindNext( Fsim_Man_t * p, char * pFront )
+{
+    assert( p->iNumber < (1 << 30) - p->nFront );
+    while ( 1 )
+    {
+        if ( p->iNumber % p->nFront == 0 )
+            p->iNumber++;
+        if ( pFront[p->iNumber % p->nFront] == 0 )
+        {
+            pFront[p->iNumber % p->nFront] = 1;
+            return p->iNumber;
+        }
+        p->iNumber++;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManVerifyFront( Fsim_Man_t * p )
+{
+    Fsim_Obj_t * pObj;
+    int * pFans0, * pFans1;  // representation of fanins
+    int * pFrontToId;        // mapping of nodes into frontier variables
+    int i, iVar0, iVar1;
+    pFans0 = ABC_ALLOC( int, p->nObjs );
+    pFans1 = ABC_ALLOC( int, p->nObjs );
+    pFans0[0] = pFans1[0] = 0;
+    pFans0[1] = pFans1[1] = 0;
+    pFrontToId = ABC_CALLOC( int, p->nFront );
+    if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
+        pFrontToId[1] = 1;
+    Fsim_ManForEachObj( p, pObj, i )
+    {
+        if ( pObj->iNode )
+            pFrontToId[pObj->iNode % p->nFront] = i;
+        iVar0 = Fsim_Lit2Var(pObj->iFan0);
+        iVar1 = Fsim_Lit2Var(pObj->iFan1);
+        pFans0[i] = Fsim_Var2Lit(pFrontToId[iVar0 % p->nFront], Fsim_LitIsCompl(pObj->iFan0));
+        pFans1[i] = Fsim_Var2Lit(pFrontToId[iVar1 % p->nFront], Fsim_LitIsCompl(pObj->iFan1));
+    }
+    for ( i = 0; i < p->nObjs; i++ )
+    {
+        assert( pFans0[i] == p->pFans0[i] );
+        assert( pFans1[i] == p->pFans1[i] );
+    }
+    ABC_FREE( pFrontToId );
+    ABC_FREE( pFans0 );
+    ABC_FREE( pFans1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManFront( Fsim_Man_t * p, int fCompressAig )
+{
+    Fsim_Obj_t Obj, * pObj = &Obj;
+    char * pFront;    // places used for the frontier
+    int * pIdToFront; // mapping of nodes into frontier places
+    int i, iVar0, iVar1, nCrossCut = 0, nCrossCutMax = 0;
+    // start the frontier
+    pFront = ABC_CALLOC( char, p->nFront );
+    pIdToFront = ABC_ALLOC( int, p->nObjs );
+    pIdToFront[0] = -1;
+    pIdToFront[1] = -1;
+    // add constant node
+    p->iNumber = 1;
+    if ( p->pRefs[1] )
+    {
+        pIdToFront[1] = Fsim_ManFrontFindNext( p, pFront );
+        nCrossCut = 1;
+    }
+    // allocate room for data
+    if ( fCompressAig )
+    {
+        p->nDataAig = p->nObjs * 6;
+        p->pDataAig = ABC_ALLOC( unsigned char, p->nDataAig );
+        p->pDataCur = p->pDataAig;
+        p->iNodePrev = 0;
+    }
+    else
+    {
+        p->pDataAig2 = ABC_ALLOC( int, 3 * p->nObjs );
+        p->pDataCur2 = p->pDataAig2 + 6;
+    }
+    // iterate through the objects
+    for ( i = 2; i < p->nObjs; i++ )
+    {
+        if ( p->pFans0[i] == 0 ) // ci
+        {
+            // store node
+            pIdToFront[i] = Fsim_ManFrontFindNext( p, pFront );
+            pObj->iNode = pIdToFront[i];
+            pObj->iFan0 = 0;
+            pObj->iFan1 = 0;
+            Fsim_ManStoreObj( p, pObj );
+            // handle CIs without fanout
+            if ( p->pRefs[i] == 0 )
+            {
+                pFront[pIdToFront[i] % p->nFront] = 0;
+                pIdToFront[i] = -1;
+            }
+        }
+        else if ( p->pFans1[i] == 0 ) // co
+        {
+            assert( p->pRefs[i] == 0 );
+            // get the fanin
+            iVar0 = Fsim_Lit2Var(p->pFans0[i]);
+            assert( pIdToFront[iVar0] > 0 );
+            // store node
+            pObj->iNode = 0;
+            pObj->iFan0 = Fsim_Var2Lit(pIdToFront[iVar0], Fsim_LitIsCompl(p->pFans0[i]));
+            pObj->iFan1 = 0;
+            Fsim_ManStoreObj( p, pObj );
+            // deref the fanin
+            if ( --p->pRefs[iVar0] == 0 )
+            {
+                pFront[pIdToFront[iVar0] % p->nFront] = 0;
+                pIdToFront[iVar0] = -1;
+                nCrossCut--;
+            }
+        }
+        else
+        {
+            // get the fanins
+            iVar0 = Fsim_Lit2Var(p->pFans0[i]);
+            assert( pIdToFront[iVar0] > 0 );
+            iVar1 = Fsim_Lit2Var(p->pFans1[i]);
+            assert( pIdToFront[iVar1] > 0 );
+            // store node
+            pIdToFront[i] = Fsim_ManFrontFindNext( p, pFront );
+            pObj->iNode = pIdToFront[i];
+            pObj->iFan0 = Fsim_Var2Lit(pIdToFront[iVar0], Fsim_LitIsCompl(p->pFans0[i]));
+            pObj->iFan1 = Fsim_Var2Lit(pIdToFront[iVar1], Fsim_LitIsCompl(p->pFans1[i]));
+            Fsim_ManStoreObj( p, pObj );
+            // deref the fanins
+            if ( --p->pRefs[iVar0] == 0 )
+            {
+                pFront[pIdToFront[iVar0] % p->nFront] = 0;
+                pIdToFront[iVar0] = -1;
+                nCrossCut--;
+            }
+            if ( --p->pRefs[iVar1] == 0 )
+            {
+                pFront[pIdToFront[iVar1] % p->nFront] = 0;
+                pIdToFront[iVar1] = -1;
+                nCrossCut--;
+            }
+            // handle nodes without fanout (choice nodes)
+            if ( p->pRefs[i] == 0 )
+            {
+                pFront[pIdToFront[i] % p->nFront] = 0;
+                pIdToFront[i] = -1;
+            }
+        }
+        if ( p->pRefs[i] )
+            if ( nCrossCutMax < ++nCrossCut )
+                nCrossCutMax = nCrossCut;
+    }
+    assert( p->pDataAig2 == NULL || p->pDataCur2 - p->pDataAig2 == (3 * p->nObjs) );
+    assert( nCrossCut == 0 );
+    assert( nCrossCutMax == p->nCrossCutMax );
+    for ( i = 0; i < p->nFront; i++ )
+        assert( pFront[i] == 0 );
+    ABC_FREE( pFront );
+    ABC_FREE( pIdToFront );
+//    Fsim_ManVerifyFront( p );
+    ABC_FREE( p->pFans0 );
+    ABC_FREE( p->pFans1 );
+    ABC_FREE( p->pRefs );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fsim/fsimInt.h b/src/opt/fsim/fsimInt.h
new file mode 100644
index 00000000..0a7493a0
--- /dev/null
+++ b/src/opt/fsim/fsimInt.h
@@ -0,0 +1,138 @@
+/**CFile****************************************************************
+
+  FileName    [fsimInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__fsim__fsimInt_h
+#define ABC__aig__fsim__fsimInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/saig/saig.h"
+#include "fsim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation object
+typedef struct Fsim_Obj_t_ Fsim_Obj_t;
+struct Fsim_Obj_t_
+{
+    int             iNode;        // the node ID
+    int             iFan0;        // the first fanin
+    int             iFan1;        // the second fanin
+};
+
+// fast sequential simulation manager
+struct Fsim_Man_t_
+{
+    // parameters
+    Aig_Man_t *     pAig;         // the AIG to be used for simulation
+    int             nWords;       // the number of simulation words
+    // AIG representation
+    int             nPis;         // the number of primary inputs
+    int             nPos;         // the number of primary outputs
+    int             nCis;         // the number of combinational inputs
+    int             nCos;         // the number of combinational outputs
+    int             nNodes;       // the number of internal nodes
+    int             nObjs;        // nCis + nNodes + nCos + 2
+    int *           pFans0;       // fanin0 for all objects
+    int *           pFans1;       // fanin1 for all objects
+    int *           pRefs;        // reference counter for each node
+    int *           pRefsCopy;    // reference counter for each node
+    Vec_Int_t *     vCis2Ids;     // mapping of CIs into their PI ids
+    Vec_Int_t *     vLos;         // register outputs
+    Vec_Int_t *     vLis;         // register inputs
+    // cross-cut representation
+    int             nCrossCut;    // temporary cross-cut variable 
+    int             nCrossCutMax; // maximum cross-cut variable
+    int             nFront;       // the size of frontier
+    // derived AIG representation
+    int             nDataAig;     // the length of allocated data
+    unsigned char * pDataAig;     // AIG representation
+    unsigned char * pDataCur;     // AIG representation (current position)
+    int             iNodePrev;    // previous extracted value
+    int             iNumber;      // the number of the last object
+    Fsim_Obj_t      Obj;          // current object
+    // temporary AIG representation
+    int *           pDataAig2;    // temporary representation
+    int *           pDataCur2;    // AIG representation (current position)
+    // simulation information
+    unsigned *      pDataSim;     // simulation data
+    unsigned *      pDataSimCis;  // simulation data for CIs
+    unsigned *      pDataSimCos;  // simulation data for COs
+    // other information
+    int *           pData1;
+    int *           pData2;
+};
+
+static inline unsigned * Fsim_SimData( Fsim_Man_t * p, int i )    { return p->pDataSim + i * p->nWords;    }
+static inline unsigned * Fsim_SimDataCi( Fsim_Man_t * p, int i )  { return p->pDataSimCis + i * p->nWords; }
+static inline unsigned * Fsim_SimDataCo( Fsim_Man_t * p, int i )  { return p->pDataSimCos + i * p->nWords; }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Fsim_Var2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
+static inline int  Fsim_Lit2Var( int Lit )              { return Lit >> 1;           }
+static inline int  Fsim_LitIsCompl( int Lit )           { return Lit & 1;            }
+static inline int  Fsim_LitNot( int Lit )               { return Lit ^ 1;            }
+static inline int  Fsim_LitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
+static inline int  Fsim_LitRegular( int Lit )           { return Lit & ~01;          }
+
+#define Fsim_ManForEachObj( p, pObj, i )\
+    for ( i = 2, p->pDataCur = p->pDataAig, p->iNodePrev = 0, pObj = &p->Obj;\
+        i < p->nObjs && Fsim_ManRestoreObj( p, pObj ); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== fsimFront.c ========================================================*/
+extern void                Fsim_ManFront( Fsim_Man_t * p, int fCompressAig );
+/*=== fsimMan.c ==========================================================*/
+extern Fsim_Man_t *        Fsim_ManCreate( Aig_Man_t * pAig );
+extern void                Fsim_ManDelete( Fsim_Man_t * p );
+extern void                Fsim_ManTest( Aig_Man_t * pAig );
+ 
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/fsim/fsimMan.c b/src/opt/fsim/fsimMan.c
new file mode 100644
index 00000000..ea0cab43
--- /dev/null
+++ b/src/opt/fsim/fsimMan.c
@@ -0,0 +1,212 @@
+/**CFile****************************************************************
+
+  FileName    [fsimMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Simulation manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fsimInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fast simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fsim_ManCreate_rec( Fsim_Man_t * p, Aig_Obj_t * pObj )
+{
+    int iFan0, iFan1, iTemp;
+    assert( !Aig_IsComplement(pObj) );
+    if ( pObj->iData )
+        return pObj->iData;
+    assert( !Aig_ObjIsConst1(pObj) );
+    if ( Aig_ObjIsNode(pObj) )
+    {
+        iFan0 = Fsim_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
+        iFan1 = Fsim_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
+        assert( iFan0 != iFan1 );
+        if ( --p->pRefs[iFan0] == 0 )
+            p->nCrossCut--;
+        iFan0 = Fsim_Var2Lit( iFan0, Aig_ObjFaninC0(pObj) );
+        if ( --p->pRefs[iFan1] == 0 )
+            p->nCrossCut--;
+        iFan1 = Fsim_Var2Lit( iFan1, Aig_ObjFaninC1(pObj) );
+        if ( p->pAig->pEquivs )
+            Fsim_ManCreate_rec( p, Aig_ObjEquiv(p->pAig, pObj) );
+    }
+    else if ( Aig_ObjIsPo(pObj) )
+    {
+        assert( Aig_ObjRefs(pObj) == 0 );
+        iFan0 = Fsim_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
+        if ( --p->pRefs[iFan0] == 0 )
+            p->nCrossCut--;
+        iFan0 = Fsim_Var2Lit( iFan0, Aig_ObjFaninC0(pObj) );
+        iFan1 = 0;
+    }
+    else
+    {
+        iFan0 = iFan1 = 0;
+        Vec_IntPush( p->vCis2Ids, Aig_ObjPioNum(pObj) );
+    }
+    if ( iFan0 < iFan1 )
+        iTemp = iFan0, iFan0 = iFan1, iFan1 = iTemp;
+    p->pFans0[p->nObjs] = iFan0;
+    p->pFans1[p->nObjs] = iFan1;
+    p->pRefs[p->nObjs]  = Aig_ObjRefs(pObj);
+    if ( p->pRefs[p->nObjs] )
+        if ( p->nCrossCutMax < ++p->nCrossCut ) 
+            p->nCrossCutMax = p->nCrossCut;
+    return pObj->iData = p->nObjs++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fast simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fsim_Man_t * Fsim_ManCreate( Aig_Man_t * pAig )
+{
+    Fsim_Man_t * p;
+    Aig_Obj_t * pObj;
+    int i, nObjs;
+    Aig_ManCleanData( pAig );
+    p = (Fsim_Man_t *)ABC_ALLOC( Fsim_Man_t, 1 );
+    memset( p, 0, sizeof(Fsim_Man_t) );
+    p->pAig = pAig;
+    p->nPis = Saig_ManPiNum(pAig);
+    p->nPos = Saig_ManPoNum(pAig);
+    p->nCis = Aig_ManPiNum(pAig);
+    p->nCos = Aig_ManPoNum(pAig);
+    p->nNodes = Aig_ManNodeNum(pAig);
+    nObjs = p->nCis + p->nCos + p->nNodes + 2;
+    p->pFans0 = ABC_ALLOC( int, nObjs );
+    p->pFans1 = ABC_ALLOC( int, nObjs );
+    p->pRefs  = ABC_ALLOC( int, nObjs );
+    p->vCis2Ids = Vec_IntAlloc( Aig_ManPiNum(pAig) );
+    // add objects (0=unused; 1=const1)
+    p->pFans0[0] = p->pFans1[0] = 0;
+    p->pFans0[1] = p->pFans1[1] = 0;
+    p->pRefs[0] = 0;
+    p->nObjs = 2;
+    pObj = Aig_ManConst1( pAig );
+    pObj->iData = 1;
+    p->pRefs[1] = Aig_ObjRefs(pObj);
+    if ( p->pRefs[1] )
+        p->nCrossCut = 1;
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( Aig_ObjRefs(pObj) == 0 )
+            Fsim_ManCreate_rec( p, pObj );
+    Aig_ManForEachPo( pAig, pObj, i )
+        Fsim_ManCreate_rec( p, pObj );
+    assert( Vec_IntSize(p->vCis2Ids) == Aig_ManPiNum(pAig) );
+    assert( p->nObjs == nObjs );
+    // check references
+    assert( p->nCrossCut == 0 );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        assert( p->pRefs[pObj->iData] == 0 );
+        p->pRefs[pObj->iData] = Aig_ObjRefs(pObj);
+    }
+    // collect flop outputs
+    p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+    Saig_ManForEachLo( pAig, pObj, i )
+        Vec_IntPush( p->vLos, pObj->iData );
+    // collect flop inputs
+    p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+    Saig_ManForEachLi( pAig, pObj, i )
+        Vec_IntPush( p->vLis, pObj->iData );
+    // determine the frontier size
+    p->nFront = 1 + (int)(1.1 * p->nCrossCutMax); 
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes fast simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManDelete( Fsim_Man_t * p )
+{
+    Vec_IntFree( p->vCis2Ids );
+    Vec_IntFree( p->vLos );
+    Vec_IntFree( p->vLis );
+    ABC_FREE( p->pDataAig2 );
+    ABC_FREE( p->pDataAig );
+    ABC_FREE( p->pFans0 );
+    ABC_FREE( p->pFans1 );
+    ABC_FREE( p->pRefs );
+    ABC_FREE( p->pDataSim );
+    ABC_FREE( p->pDataSimCis );
+    ABC_FREE( p->pDataSimCos );
+    ABC_FREE( p->pData1 );
+    ABC_FREE( p->pData2 );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManTest( Aig_Man_t * pAig )
+{
+    Fsim_Man_t * p;
+    p = Fsim_ManCreate( pAig );
+    Fsim_ManFront( p, 0 );
+    Fsim_ManDelete( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fsim/fsimSim.c b/src/opt/fsim/fsimSim.c
new file mode 100644
index 00000000..84844407
--- /dev/null
+++ b/src/opt/fsim/fsimSim.c
@@ -0,0 +1,567 @@
+/**CFile****************************************************************
+
+  FileName    [fsimSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Simulation procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fsimInt.h"
+#include "aig/ssw/ssw.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimInfoRandom( Fsim_Man_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = Aig_ManRandom( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimInfoZero( Fsim_Man_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns index of the first pattern that failed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManSimInfoIsZero( Fsim_Man_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        if ( pInfo[w] )
+            return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimInfoOne( Fsim_Man_t * p, unsigned * pInfo )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = ~0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimInfoCopy( Fsim_Man_t * p, unsigned * pInfo, unsigned * pInfo0 )
+{
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimulateCi( Fsim_Man_t * p, int iNode, int iCi )
+{
+    unsigned * pInfo  = Fsim_SimData( p, iNode % p->nFront );
+    unsigned * pInfo0 = Fsim_SimDataCi( p, iCi );
+    int w;
+    for ( w = p->nWords-1; w >= 0; w-- )
+        pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimulateCo( Fsim_Man_t * p, int iCo, int iFan0 )
+{
+    unsigned * pInfo  = Fsim_SimDataCo( p, iCo );
+    unsigned * pInfo0 = Fsim_SimData( p, Fsim_Lit2Var(iFan0) % p->nFront );
+    int w;
+    if ( Fsim_LitIsCompl(iFan0) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = ~pInfo0[w];
+    else //if ( !Fsim_LitIsCompl(iFan0) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = pInfo0[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimulateNode( Fsim_Man_t * p, int iNode, int iFan0, int iFan1 )
+{
+    unsigned * pInfo  = Fsim_SimData( p, iNode % p->nFront );
+    unsigned * pInfo0 = Fsim_SimData( p, Fsim_Lit2Var(iFan0) % p->nFront );
+    unsigned * pInfo1 = Fsim_SimData( p, Fsim_Lit2Var(iFan1) % p->nFront );
+    int w;
+    if ( Fsim_LitIsCompl(iFan0) && Fsim_LitIsCompl(iFan1) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
+    else if ( Fsim_LitIsCompl(iFan0) && !Fsim_LitIsCompl(iFan1) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = ~pInfo0[w] & pInfo1[w];
+    else if ( !Fsim_LitIsCompl(iFan0) && Fsim_LitIsCompl(iFan1) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = pInfo0[w] & ~pInfo1[w];
+    else //if ( !Fsim_LitIsCompl(iFan0) && !Fsim_LitIsCompl(iFan1) )
+        for ( w = p->nWords-1; w >= 0; w-- )
+            pInfo[w] = pInfo0[w] & pInfo1[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimInfoInit( Fsim_Man_t * p )
+{
+    int iPioNum, i;
+    Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
+    {
+        if ( iPioNum < p->nPis )
+            Fsim_ManSimInfoRandom( p, Fsim_SimDataCi(p, i) );
+        else
+            Fsim_ManSimInfoZero( p, Fsim_SimDataCi(p, i) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimInfoTransfer( Fsim_Man_t * p )
+{
+    int iPioNum, i;
+    Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
+    {
+        if ( iPioNum < p->nPis )
+            Fsim_ManSimInfoRandom( p, Fsim_SimDataCi(p, i) );
+        else
+            Fsim_ManSimInfoCopy( p, Fsim_SimDataCi(p, i), Fsim_SimDataCo(p, p->nPos+iPioNum-p->nPis) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManRestoreNum( Fsim_Man_t * p )
+{
+    int ch, i, x = 0;
+    for ( i = 0; (ch = *p->pDataCur++) & 0x80; i++ )
+        x |= (ch & 0x7f) << (7 * i);
+    assert( p->pDataCur - p->pDataAig < p->nDataAig );
+    return x | (ch << (7 * i));
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManRestoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj )
+{
+    int iValue = Fsim_ManRestoreNum( p );
+    if ( (iValue & 3) == 3 ) // and
+    {
+        pObj->iNode = (iValue >> 2) + p->iNodePrev;
+        pObj->iFan0 = (pObj->iNode << 1) - Fsim_ManRestoreNum( p );
+        pObj->iFan1 = pObj->iFan0 - Fsim_ManRestoreNum( p );
+        p->iNodePrev = pObj->iNode;
+    }
+    else if ( (iValue & 3) == 1 ) // ci
+    {
+        pObj->iNode = (iValue >> 2) + p->iNodePrev;
+        pObj->iFan0 = 0;
+        pObj->iFan1 = 0;
+        p->iNodePrev = pObj->iNode;
+    }
+    else // if ( (iValue & 1) == 0 ) // co
+    {
+        pObj->iNode = 0;
+        pObj->iFan0 = ((p->iNodePrev << 1) | 1) - (iValue >> 1);
+        pObj->iFan1 = 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimulateRound2( Fsim_Man_t * p )
+{
+    Fsim_Obj_t * pObj;
+    int i, iCis = 0, iCos = 0;
+    if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
+        Fsim_ManSimInfoOne( p, Fsim_SimData(p, 1) );
+    Fsim_ManForEachObj( p, pObj, i )
+    {
+        if ( pObj->iFan0 == 0 )
+            Fsim_ManSimulateCi( p, pObj->iNode, iCis++ );
+        else if ( pObj->iFan1 == 0 )
+            Fsim_ManSimulateCo( p, iCos++, pObj->iFan0 );
+        else
+            Fsim_ManSimulateNode( p, pObj->iNode, pObj->iFan0, pObj->iFan1 );
+    }
+    assert( iCis == p->nCis );
+    assert( iCos == p->nCos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManSimulateRound( Fsim_Man_t * p )
+{
+    int * pCur, * pEnd;
+    int iCis = 0, iCos = 0;
+    if ( p->pDataAig2 == NULL )
+    {
+        Fsim_ManSimulateRound2( p );
+        return;
+    }
+    if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
+        Fsim_ManSimInfoOne( p, Fsim_SimData(p, 1) );
+    pCur = p->pDataAig2 + 6;
+    pEnd = p->pDataAig2 + 3 * p->nObjs;
+    while ( pCur < pEnd )
+    {
+        if ( pCur[1] == 0 )
+            Fsim_ManSimulateCi( p, pCur[0], iCis++ );
+        else if ( pCur[2] == 0 )
+            Fsim_ManSimulateCo( p, iCos++, pCur[1] );
+        else
+            Fsim_ManSimulateNode( p, pCur[0], pCur[1], pCur[2] );
+        pCur += 3;
+    }
+    assert( iCis == p->nCis );
+    assert( iCos == p->nCos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManSimulateRoundTest( Fsim_Man_t * p )
+{
+    Fsim_Obj_t * pObj;
+    int i, clk = clock();
+    Fsim_ManForEachObj( p, pObj, i )
+    {
+    }
+//    ABC_PRT( "Unpacking time", p->pPars->nIters * (clock() - clk) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns index of the PO and pattern that failed it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fsim_ManCheckPos( Fsim_Man_t * p, int * piPo, int * piPat )
+{
+    int i, iPat;
+    for ( i = 0; i < p->nPos; i++ )
+    {
+        iPat = Fsim_ManSimInfoIsZero( p, Fsim_SimDataCo(p, i) );
+        if ( iPat >= 0 )
+        {
+            *piPo = i;
+            *piPat = iPat;
+            return 1;
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Fsim_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
+{
+    Abc_Cex_t * p;
+    unsigned * pData;
+    int f, i, w, iPioId, Counter;
+    p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
+    p->iFrame = iFrame;
+    p->iPo = iOut;
+    // fill in the binary data
+    Aig_ManRandom( 1 );
+    Counter = p->nRegs;
+    pData = ABC_ALLOC( unsigned, nWords );
+    for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
+    for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
+    {
+        iPioId = Vec_IntEntry( vCis2Ids, i );
+        if ( iPioId >= p->nPis )
+            continue;
+        for ( w = nWords-1; w >= 0; w-- )
+            pData[w] = Aig_ManRandom( 0 );
+        if ( Aig_InfoHasBit( pData, iPat ) )
+            Aig_InfoSetBit( p->pData, Counter + iPioId );
+    }
+    ABC_FREE( pData );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fsim_ManSimulate( Aig_Man_t * pAig, Fsim_ParSim_t * pPars )
+{
+    Fsim_Man_t * p;
+    Sec_MtrStatus_t Status;
+    int i, iOut, iPat, clk, clkTotal = clock(), clk2, clk2Total = 0;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    if ( pPars->fCheckMiter )
+    {
+        Status = Sec_MiterStatus( pAig );
+        if ( Status.nSat > 0 )
+        {
+            printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
+            return 1;
+        }
+        if ( Status.nUndec == 0 )
+        {
+            printf( "Miter is trivially unsatisfiable.\n" );
+            return 0;
+        }
+    }
+    // create manager
+    clk = clock();
+    p = Fsim_ManCreate( pAig );
+    p->nWords = pPars->nWords;
+    if ( pPars->fVerbose )
+    {
+        printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d.  FrtMem = %7.2f Mb. ", 
+            p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront, 
+            4.0*p->nWords*(p->nFront)/(1<<20) );
+        ABC_PRT( "Time", clock() - clk );
+    }
+    // create simulation frontier
+    clk = clock();
+    Fsim_ManFront( p, pPars->fCompressAig );
+    if ( pPars->fVerbose )
+    {
+        printf( "Max ID = %8d. Log max ID = %2d.  AigMem = %7.2f Mb (%5.2f byte/obj).  ", 
+            p->iNumber, Aig_Base2Log(p->iNumber), 
+            1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
+            1.0*(p->pDataCur-p->pDataAig)/p->nObjs ); 
+        ABC_PRT( "Time", clock() - clk );
+    }
+    // perform simulation
+    Aig_ManRandom( 1 );
+    assert( p->pDataSim == NULL );
+    p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->nFront );
+    p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * p->nCis );
+    p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * p->nCos );
+    Fsim_ManSimInfoInit( p );
+    for ( i = 0; i < pPars->nIters; i++ )
+    { 
+        Fsim_ManSimulateRound( p );
+        if ( pPars->fVerbose )
+        {
+            printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
+            printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
+        }
+        if ( pPars->fCheckMiter && Fsim_ManCheckPos( p, &iOut, &iPat ) )
+        {
+            assert( pAig->pSeqModel == NULL );
+            pAig->pSeqModel = Fsim_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
+            if ( pPars->fVerbose )
+            printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
+            break;
+        }
+        if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
+            break;
+        clk2 = clock();
+        if ( i < pPars->nIters - 1 )
+            Fsim_ManSimInfoTransfer( p );
+        clk2Total += clock() - clk2;
+    }
+    if ( pAig->pSeqModel == NULL )
+        printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
+    if ( pPars->fVerbose )
+    {
+        printf( "Maxcut = %8d.  AigMem = %7.2f Mb.  SimMem = %7.2f Mb.  ", 
+            p->nCrossCutMax, 
+            p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
+            4.0*p->nWords*(p->nFront+p->nCis+p->nCos)/(1<<20) );
+        ABC_PRT( "Sim time", clock() - clkTotal );
+
+//        ABC_PRT( "Additional time", clk2Total );
+//        Fsim_ManSimulateRoundTest( p );
+//        Fsim_ManSimulateRoundTest2( p );
+    }
+    Fsim_ManDelete( p );
+    return pAig->pSeqModel != NULL;
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fsim/fsimSwitch.c b/src/opt/fsim/fsimSwitch.c
new file mode 100644
index 00000000..3eef2d4c
--- /dev/null
+++ b/src/opt/fsim/fsimSwitch.c
@@ -0,0 +1,40 @@
+/**CFile****************************************************************
+
+  FileName    [fsimSwitch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Computing switching activity.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimSwitch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fsimInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fsim/fsimTsim.c b/src/opt/fsim/fsimTsim.c
new file mode 100644
index 00000000..5ad78b33
--- /dev/null
+++ b/src/opt/fsim/fsimTsim.c
@@ -0,0 +1,415 @@
+/**CFile****************************************************************
+
+  FileName    [fsimTsim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Fast sequential AIG simulator.]
+
+  Synopsis    [Varius utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: fsimTsim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fsimInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define FSIM_ZER 1
+#define FSIM_ONE 2
+#define FSIM_UND 3
+
+static inline int Aig_XsimNotCond( int Value, int fCompl )   
+{ 
+    if ( Value == FSIM_UND )
+        return FSIM_UND;
+    if ( Value == FSIM_ZER + fCompl )
+        return FSIM_ZER;
+    return FSIM_ONE;
+}
+static inline int Aig_XsimAndCond( int Value0, int fCompl0, int Value1, int fCompl1 )   
+{ 
+    if ( Value0 == FSIM_UND || Value1 == FSIM_UND )
+        return FSIM_UND;
+    if ( Value0 == FSIM_ZER + fCompl0 || Value1 == FSIM_ZER + fCompl1 )
+        return FSIM_ZER;
+    return FSIM_ONE;
+}
+
+static inline int Fsim_ManTerSimInfoGet( unsigned * pInfo, int i )
+{
+    return 3 & (pInfo[i >> 4] >> ((i & 15) << 1));
+}
+static inline void Fsim_ManTerSimInfoSet( unsigned * pInfo, int i, int Value )
+{
+    assert( Value >= FSIM_ZER && Value <= FSIM_UND );
+    Value ^= Fsim_ManTerSimInfoGet( pInfo, i );
+    pInfo[i >> 4] ^= (Value << ((i & 15) << 1));
+}
+
+static inline unsigned * Fsim_ManTerStateNext( unsigned * pState, int nWords )                      { return *((unsigned **)(pState + nWords));  }
+static inline void       Fsim_ManTerStateSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManTerSimulateCi( Fsim_Man_t * p, int iNode, int iCi )
+{
+    Fsim_ManTerSimInfoSet( p->pDataSim, iNode, Fsim_ManTerSimInfoGet(p->pDataSimCis, iCi) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManTerSimulateCo( Fsim_Man_t * p, int iCo, int iFan0 )
+{
+    int Value = Fsim_ManTerSimInfoGet( p->pDataSim, Fsim_Lit2Var(iFan0) );
+    Fsim_ManTerSimInfoSet( p->pDataSimCos, iCo, Aig_XsimNotCond( Value, Fsim_LitIsCompl(iFan0) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManTerSimulateNode( Fsim_Man_t * p, int iNode, int iFan0, int iFan1 )
+{
+    int Value0 = Fsim_ManTerSimInfoGet( p->pDataSim, Fsim_Lit2Var(iFan0) );
+    int Value1 = Fsim_ManTerSimInfoGet( p->pDataSim, Fsim_Lit2Var(iFan1) );
+    Fsim_ManTerSimInfoSet( p->pDataSim, iNode, Aig_XsimAndCond( Value0, Fsim_LitIsCompl(iFan0), Value1, Fsim_LitIsCompl(iFan1) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManTerSimInfoInit( Fsim_Man_t * p )
+{
+    int iPioNum, i;
+    Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
+    {
+        if ( iPioNum < p->nPis )
+            Fsim_ManTerSimInfoSet( p->pDataSimCis, i, FSIM_UND );
+        else
+            Fsim_ManTerSimInfoSet( p->pDataSimCis, i, FSIM_ZER );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManTerSimInfoTransfer( Fsim_Man_t * p )
+{
+    int iPioNum, i;
+    Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
+    {
+        if ( iPioNum < p->nPis )
+            Fsim_ManTerSimInfoSet( p->pDataSimCis, i, FSIM_UND );
+        else
+            Fsim_ManTerSimInfoSet( p->pDataSimCis, i, Fsim_ManTerSimInfoGet( p->pDataSimCos, p->nPos+iPioNum-p->nPis ) );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fsim_ManTerStateHash( unsigned * pState, int nWords, int nTableSize )
+{
+    static int s_FPrimes[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 uHash;
+    int i;
+    uHash = 0;
+    for ( i = 0; i < nWords; i++ )
+        uHash ^= pState[i] * s_FPrimes[i & 0x7F];
+    return uHash % nTableSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fsim_ManTerStateLookup( unsigned * pState, int nWords, unsigned ** pBins, int nBins )
+{
+    unsigned * pEntry;
+    int Hash;
+    Hash = Fsim_ManTerStateHash( pState, nWords, nBins );
+    for ( pEntry = pBins[Hash]; pEntry; pEntry = Fsim_ManTerStateNext(pEntry, nWords) )
+        if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManTerStateInsert( unsigned * pState, int nWords, unsigned ** pBins, int nBins )
+{
+    int Hash = Fsim_ManTerStateHash( pState, nWords, nBins );
+    assert( !Fsim_ManTerStateLookup( pState, nWords, pBins, nBins ) );
+    Fsim_ManTerStateSetNext( pState, nWords, pBins[Hash] );
+    pBins[Hash] = pState;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Fsim_ManTerStateCreate( unsigned * pInfo, int nPis, int nCis, int nWords )
+{
+    unsigned * pRes;
+    int i;
+    pRes = (unsigned *)ABC_CALLOC( char, sizeof(unsigned) * nWords + sizeof(unsigned *) );
+    for ( i = nPis; i < nCis; i++ )
+        Fsim_ManTerSimInfoSet( pRes, i-nPis, Fsim_ManTerSimInfoGet(pInfo, i) );
+    return pRes;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts value into the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fsim_ManTerStatePrint( unsigned * pState, int nRegs )
+{
+    int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
+    for ( i = 0; i < nRegs; i++ )
+    {
+        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        if ( Value == 1 )
+            printf( "0" ), nZeros++;
+        else if ( Value == 2 )
+            printf( "1" ), nOnes++;
+        else if ( Value == 3 )
+            printf( "x" ), nDcs++;
+        else
+            assert( 0 );
+    }
+    printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Fsim_ManTerSimulateRound( Fsim_Man_t * p )
+{
+    int * pCur, * pEnd;
+    int iCis = 0, iCos = 0;
+    if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
+        Fsim_ManTerSimInfoSet( p->pDataSimCis, 1, FSIM_ONE );
+    pCur = p->pDataAig2 + 6;
+    pEnd = p->pDataAig2 + 3 * p->nObjs;
+    while ( pCur < pEnd )
+    {
+        if ( pCur[1] == 0 )
+            Fsim_ManTerSimulateCi( p, pCur[0], iCis++ );
+        else if ( pCur[2] == 0 )
+            Fsim_ManTerSimulateCo( p, iCos++, pCur[1] );
+        else
+            Fsim_ManTerSimulateNode( p, pCur[0], pCur[1], pCur[2] );
+        pCur += 3;
+    }
+    assert( iCis == p->nCis );
+    assert( iCos == p->nCos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Fsim_ManTerSimulate( Aig_Man_t * pAig, int fVerbose )
+{
+    Fsim_Man_t * p;
+    Vec_Ptr_t * vStates;
+    unsigned ** pBins, * pState;
+    int i, nWords, nBins, clk, clkTotal = clock();
+    assert( Aig_ManRegNum(pAig) > 0 );
+    // create manager
+    clk = clock();
+    p = Fsim_ManCreate( pAig );
+    if ( fVerbose )
+    {
+        printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d.  FrtMem = %7.2f Mb. ", 
+            p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront, 
+            4.0*Aig_BitWordNum(2 * p->nFront)/(1<<20) );
+        ABC_PRT( "Time", clock() - clk );
+    }
+    // create simulation frontier
+    clk = clock();
+    Fsim_ManFront( p, 0 );
+    if ( fVerbose )
+    {
+        printf( "Max ID = %8d. Log max ID = %2d.  AigMem = %7.2f Mb (%5.2f byte/obj).  ", 
+            p->iNumber, Aig_Base2Log(p->iNumber), 
+            1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
+            1.0*(p->pDataCur-p->pDataAig)/p->nObjs ); 
+        ABC_PRT( "Time", clock() - clk );
+    }
+    // allocate storage for terminary states
+    nWords  = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
+    vStates = Vec_PtrAlloc( 1000 );
+    nBins   = Abc_PrimeCudd( 500 );
+    pBins   = ABC_ALLOC( unsigned *, nBins );
+    memset( pBins, 0, sizeof(unsigned *) * nBins );
+    // perform simulation
+    assert( p->pDataSim == NULL );
+    p->pDataSim = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nFront) * sizeof(unsigned) );
+    p->pDataSimCis = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nCis) * sizeof(unsigned) );
+    p->pDataSimCos = ABC_ALLOC( unsigned, Aig_BitWordNum(2 * p->nCos) * sizeof(unsigned) );
+    Fsim_ManTerSimInfoInit( p );
+    // hash the first state
+    pState = Fsim_ManTerStateCreate( p->pDataSimCis, p->nPis, p->nCis, nWords );
+    Vec_PtrPush( vStates, pState );
+    Fsim_ManTerStateInsert( pState, nWords, pBins, nBins );
+    // perform simuluation till convergence
+    for ( i = 0; ; i++ )
+    {
+        Fsim_ManTerSimulateRound( p );
+        Fsim_ManTerSimInfoTransfer( p );
+        // hash the first state
+        pState = Fsim_ManTerStateCreate( p->pDataSimCis, p->nPis, p->nCis, nWords );
+        Vec_PtrPush( vStates, pState );
+        if ( Fsim_ManTerStateLookup(pState, nWords, pBins, nBins) )
+            break;
+        Fsim_ManTerStateInsert( pState, nWords, pBins, nBins );
+    }
+    if ( fVerbose )
+    {
+        printf( "Maxcut = %8d.  AigMem = %7.2f Mb.  SimMem = %7.2f Mb.  ", 
+            p->nCrossCutMax, 
+            p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20), 
+            4.0*(Aig_BitWordNum(2 * p->nFront)+Aig_BitWordNum(2 * p->nCis)+Aig_BitWordNum(2 * p->nCos))/(1<<20) );
+        ABC_PRT( "Sim time", clock() - clkTotal );
+    }
+    ABC_FREE( pBins );
+    Fsim_ManDelete( p );
+    return vStates;
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/fsim/module.make b/src/opt/fsim/module.make
new file mode 100644
index 00000000..c728e128
--- /dev/null
+++ b/src/opt/fsim/module.make
@@ -0,0 +1,6 @@
+SRC +=    src/opt/fsim/fsimCore.c \
+    src/opt/fsim/fsimFront.c \
+    src/opt/fsim/fsimMan.c \
+    src/opt/fsim/fsimSim.c \
+    src/opt/fsim/fsimSwitch.c \
+    src/opt/fsim/fsimTsim.c