Version abc50904

11 files changed, 2618 insertions, 0 deletions

diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
new file mode 100644
index 00000000..43d0a125
--- /dev/null
+++ b/src/opt/sim/module.make
@@ -0,0 +1,9 @@
+SRC +=  src/opt/sim/simMan.c \
+    src/opt/sim/simSat.c \
+    src/opt/sim/simSupp.c \
+    src/opt/sim/simSwitch.c \
+    src/opt/sim/simSym.c \
+    src/opt/sim/simSymSat.c \
+    src/opt/sim/simSymSim.c \
+    src/opt/sim/simSymStr.c \
+    src/opt/sim/simUtils.c
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
new file mode 100644
index 00000000..9b4d9699
--- /dev/null
+++ b/src/opt/sim/sim.h
@@ -0,0 +1,190 @@
+/**CFile****************************************************************
+
+  FileName    [sim.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Simulation package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __SIM_H__
+#define __SIM_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sym_Man_t_ Sym_Man_t;
+struct Sym_Man_t_
+{
+    // info about the network
+    Abc_Ntk_t *       pNtk;          // the network 
+    Vec_Ptr_t *       vNodes;        // internal nodes in topological order
+    int               nInputs;
+    int               nOutputs;
+    // internal simulation information
+    int               nSimWords;     // the number of bits in simulation info
+    Vec_Ptr_t *       vSim;          // simulation info
+    // support information
+    Vec_Ptr_t *       vSuppFun;      // functional supports
+    // symmetry info for each output
+    Vec_Ptr_t *       vMatrSymms;    // symmetric pairs
+    Vec_Ptr_t *       vMatrNonSymms; // non-symmetric pairs
+    Vec_Int_t *       vPairsTotal;   // total pairs
+    Vec_Int_t *       vPairsSym;     // symmetric pairs
+    Vec_Int_t *       vPairsNonSym;  // non-symmetric pairs
+    // temporary simulation info
+    unsigned *        uPatRand;
+    unsigned *        uPatCol;
+    unsigned *        uPatRow;
+    // internal data structures
+    int               nSatRuns;
+    int               nSatRunsSat;
+    int               nSatRunsUnsat;
+    // pairs
+    int               nPairsSymm;
+    int               nPairsSymmStr;
+    int               nPairsNonSymm;
+    int               nPairsTotal;
+    // runtime statistics
+    int               timeSim;
+    int               timeFraig;
+    int               timeSat;
+    int               timeTotal;
+};
+
+typedef struct Sim_Man_t_ Sim_Man_t;
+struct Sim_Man_t_
+{
+    // info about the network
+    Abc_Ntk_t *       pNtk;
+    int               nInputs;
+    int               nOutputs;
+    // internal simulation information
+    int               nSimBits;      // the number of bits in simulation info
+    int               nSimWords;     // the number of words in simulation info
+    Vec_Ptr_t *       vSim0;         // simulation info 1
+    Vec_Ptr_t *       vSim1;         // simulation info 2
+    // support information
+    int               nSuppBits;     // the number of bits in support info
+    int               nSuppWords;    // the number of words in support info
+    Vec_Ptr_t *       vSuppStr;      // structural supports
+    Vec_Ptr_t *       vSuppFun;      // functional supports
+    // simulation targets
+    Vec_Vec_t *       vSuppTargs;    // support targets
+    // internal data structures
+    Extra_MmFixed_t * pMmPat;   
+    Vec_Ptr_t *       vFifo;
+    Vec_Int_t *       vDiffs;
+    int               nSatRuns;
+    int               nSatRunsSat;
+    int               nSatRunsUnsat;
+    // runtime statistics
+    int               timeSim;
+    int               timeTrav;
+    int               timeFraig;
+    int               timeSat;
+    int               timeTotal;
+};
+
+typedef struct Sim_Pat_t_ Sim_Pat_t;
+struct Sim_Pat_t_
+{
+    int              Input;         // the input which it has detected
+    int              Output;        // the output for which it was collected
+    unsigned *       pData;         // the simulation data
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+#define SIM_NUM_WORDS(n)      ((n)/32 + (((n)%32) > 0))
+#define SIM_LAST_BITS(n)      ((((n)%32) > 0)? (n)%32 : 32)
+
+#define SIM_MASK_FULL         (0xFFFFFFFF)
+#define SIM_MASK_BEG(n)       (SIM_MASK_FULL >> (32-n))
+#define SIM_MASK_END(n)       (SIM_MASK_FULL << (n))
+#define SIM_SET_0_FROM(m,n)   ((m) & ~SIM_MASK_BEG(n))
+#define SIM_SET_1_FROM(m,n)   ((m) |  SIM_MASK_END(n))
+
+// generating random unsigned (#define RAND_MAX 0x7fff)
+#define SIM_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
+
+// macros to get hold of bits in a bit string
+#define Sim_SetBit(p,i)       ((p)[(i)>>5] |= (1<<((i) & 31)))
+#define Sim_XorBit(p,i)       ((p)[(i)>>5] ^= (1<<((i) & 31)))
+#define Sim_HasBit(p,i)      (((p)[(i)>>5]  & (1<<((i) & 31))) > 0)
+
+// macros to get hold of the support info
+#define Sim_SuppStrSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
+#define Sim_SuppStrHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
+#define Sim_SuppFunSetVar(vSupps,Output,v)    Sim_SetBit((unsigned*)(vSupps)->pArray[Output],(v))
+#define Sim_SuppFunHasVar(vSupps,Output,v)    Sim_HasBit((unsigned*)(vSupps)->pArray[Output],(v))
+#define Sim_SimInfoSetVar(vSupps,pNode,v)     Sim_SetBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
+#define Sim_SimInfoHasVar(vSupps,pNode,v)     Sim_HasBit((unsigned*)(vSupps)->pArray[(pNode)->Id],(v))
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== simMan.c ==========================================================*/
+extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk );
+extern void            Sym_ManStop( Sym_Man_t * p );
+extern void            Sym_ManPrintStats( Sym_Man_t * p );
+extern Sim_Man_t *     Sim_ManStart( Abc_Ntk_t * pNtk );
+extern void            Sim_ManStop( Sim_Man_t * p );
+extern void            Sim_ManPrintStats( Sim_Man_t * p );
+extern Sim_Pat_t *     Sim_ManPatAlloc( Sim_Man_t * p );
+extern void            Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat );
+/*=== simSupp.c ==========================================================*/
+extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk );
+/*=== simSym.c ==========================================================*/
+extern int             Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk );
+/*=== simSymStr.c ==========================================================*/
+extern void            Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs );
+/*=== simSymSim.c ==========================================================*/
+extern void            Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPatRand, Vec_Ptr_t * vMatrsNonSym );
+/*=== simUtil.c ==========================================================*/
+extern Vec_Ptr_t *     Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean );
+extern void            Sim_UtilInfoFree( Vec_Ptr_t * p );
+extern void            Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords );
+extern void            Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
+extern void            Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs );
+extern void            Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode );
+extern bool            Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode );
+extern void            Sim_UtilSimulate( Sim_Man_t * p, bool fFirst );
+extern void            Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 );
+extern void            Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords );
+extern int             Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct );
+extern int             Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords );
+extern void            Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords );
+extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters );
+extern int             Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
new file mode 100644
index 00000000..02d59343
--- /dev/null
+++ b/src/opt/sim/simMan.c
@@ -0,0 +1,278 @@
+/**CFile****************************************************************
+
+  FileName    [simMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simulation manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the simulatin manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk )
+{
+    Sym_Man_t * p;
+    int i;
+    // start the manager
+    p = ALLOC( Sym_Man_t, 1 );
+    memset( p, 0, sizeof(Sym_Man_t) );
+    p->pNtk = pNtk;
+    p->vNodes     = Abc_NtkDfs( pNtk, 0 );
+    p->nInputs    = Abc_NtkCiNum(p->pNtk);
+    p->nOutputs   = Abc_NtkCoNum(p->pNtk);
+    // internal simulation information
+    p->nSimWords  = SIM_NUM_WORDS(p->nInputs);
+    p->vSim       = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
+    // symmetry info for each output
+    p->vMatrSymms    = Vec_PtrStart( p->nOutputs );
+    p->vMatrNonSymms = Vec_PtrStart( p->nOutputs );
+    p->vPairsTotal   = Vec_IntStart( p->nOutputs );
+    p->vPairsSym     = Vec_IntStart( p->nOutputs );
+    p->vPairsNonSym  = Vec_IntStart( p->nOutputs );
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        p->vMatrSymms->pArray[i]    = Extra_BitMatrixStart( p->nInputs );
+        p->vMatrNonSymms->pArray[i] = Extra_BitMatrixStart( p->nInputs );
+    }
+    // temporary patterns
+    p->uPatRand = ALLOC( unsigned, p->nSimWords );
+    p->uPatCol  = ALLOC( unsigned, p->nSimWords );
+    p->uPatRow  = ALLOC( unsigned, p->nSimWords );
+    // compute supports
+    p->vSuppFun = Sim_ComputeFunSupp( pNtk );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the simulatin manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sym_ManStop( Sym_Man_t * p )
+{
+    int i;
+    Sym_ManPrintStats( p );
+    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );   
+    if ( p->vSim )         Sim_UtilInfoFree( p->vSim );   
+    if ( p->vNodes )       Vec_PtrFree( p->vNodes );
+    for ( i = 0; i < p->nOutputs; i++ )
+    {
+        Extra_BitMatrixStop( p->vMatrSymms->pArray[i] );
+        Extra_BitMatrixStop( p->vMatrNonSymms->pArray[i] );
+    }
+    Vec_PtrFree( p->vMatrSymms );
+    Vec_PtrFree( p->vMatrNonSymms );
+    Vec_IntFree( p->vPairsTotal );
+    Vec_IntFree( p->vPairsSym );
+    Vec_IntFree( p->vPairsNonSym );
+    FREE( p->uPatRand );
+    FREE( p->uPatCol );
+    FREE( p->uPatRow );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the manager statisticis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sym_ManPrintStats( Sym_Man_t * p )
+{
+    printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", 
+        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+/*
+    printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
+    printf( "Total func supps   = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
+    printf( "Total targets      = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) );
+    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
+*/
+    printf( "Sat runs SAT       = %6d.\n", p->nSatRunsSat );
+    printf( "Sat runs UNSAT     = %6d.\n", p->nSatRunsUnsat );
+    PRT( "Simulation  ", p->timeSim );
+    PRT( "Fraiging    ", p->timeFraig );
+    PRT( "SAT         ", p->timeSat );
+    PRT( "TOTAL       ", p->timeTotal );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the simulatin manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
+{
+    Sim_Man_t * p;
+    // start the manager
+    p = ALLOC( Sim_Man_t, 1 );
+    memset( p, 0, sizeof(Sim_Man_t) );
+    p->pNtk = pNtk;
+    p->nInputs    = Abc_NtkCiNum(p->pNtk);
+    p->nOutputs   = Abc_NtkCoNum(p->pNtk);
+    // internal simulation information
+    p->nSimBits   = 2048;
+    p->nSimWords  = SIM_NUM_WORDS(p->nSimBits);
+    p->vSim0      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
+    p->vSim1      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
+    // support information
+    p->nSuppBits  = Abc_NtkCiNum(pNtk);
+    p->nSuppWords = SIM_NUM_WORDS(p->nSuppBits);
+    p->vSuppStr   = Sim_ComputeStrSupp( pNtk );
+    p->vSuppFun   = Sim_UtilInfoAlloc( Abc_NtkCoNum(p->pNtk),  p->nSuppWords, 1 );
+    // other data
+    p->pMmPat     = Extra_MmFixedStart( sizeof(Sim_Pat_t) + p->nSuppWords * sizeof(unsigned) ); 
+    p->vFifo      = Vec_PtrAlloc( 100 );
+    p->vDiffs     = Vec_IntAlloc( 100 );
+    // allocate support targets (array of unresolved outputs for each input)
+    p->vSuppTargs = Vec_VecStart( p->nInputs );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the simulatin manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_ManStop( Sim_Man_t * p )
+{
+    Sim_ManPrintStats( p );
+    if ( p->vSim0 )        Sim_UtilInfoFree( p->vSim0 );       
+    if ( p->vSim1 )        Sim_UtilInfoFree( p->vSim1 );       
+    if ( p->vSuppStr )     Sim_UtilInfoFree( p->vSuppStr );    
+//    if ( p->vSuppFun )     Sim_UtilInfoFree( p->vSuppFun );    
+    if ( p->vSuppTargs )   Vec_VecFree( p->vSuppTargs );
+    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat, 0 );
+    if ( p->vFifo )        Vec_PtrFree( p->vFifo );
+    if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the manager statisticis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_ManPrintStats( Sim_Man_t * p )
+{
+    printf( "Inputs = %d. Outputs = %d. Sim words = %d.\n", 
+        Abc_NtkCiNum(p->pNtk), Abc_NtkCoNum(p->pNtk), p->nSimWords );
+    printf( "Total struct supps = %6d.\n", Sim_UtilCountSuppSizes(p, 1) );
+    printf( "Total func supps   = %6d.\n", Sim_UtilCountSuppSizes(p, 0) );
+    printf( "Total targets      = %6d.\n", Vec_VecSizeSize(p->vSuppTargs) );
+    printf( "Total sim patterns = %6d.\n", Vec_PtrSize(p->vFifo) );
+    printf( "Sat runs SAT       = %6d.\n", p->nSatRunsSat );
+    printf( "Sat runs UNSAT     = %6d.\n", p->nSatRunsUnsat );
+    PRT( "Simulation  ", p->timeSim );
+    PRT( "Traversal   ", p->timeTrav );
+    PRT( "Fraiging    ", p->timeFraig );
+    PRT( "SAT         ", p->timeSat );
+    PRT( "TOTAL       ", p->timeTotal );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns one simulation pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sim_Pat_t * Sim_ManPatAlloc( Sim_Man_t * p )
+{
+    Sim_Pat_t * pPat;
+    pPat = (Sim_Pat_t *)Extra_MmFixedEntryFetch( p->pMmPat );
+    pPat->Output = -1;
+    pPat->pData  = (unsigned *)((char *)pPat + sizeof(Sim_Pat_t));
+    memset( pPat->pData, 0, p->nSuppWords * sizeof(unsigned) );
+    return pPat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns one simulation pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_ManPatFree( Sim_Man_t * p, Sim_Pat_t * pPat )
+{
+    Extra_MmFixedEntryRecycle( p->pMmPat, (char *)pPat );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSat.c b/src/opt/sim/simSat.c
new file mode 100644
index 00000000..b4e080fe
--- /dev/null
+++ b/src/opt/sim/simSat.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [simSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simulation to determine functional support.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
new file mode 100644
index 00000000..2f380866
--- /dev/null
+++ b/src/opt/sim/simSupp.c
@@ -0,0 +1,594 @@
+/**CFile****************************************************************
+
+  FileName    [simSupp.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simulation to determine functional support.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static int    Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets );
+static int    Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets );
+static void   Sim_ComputeSuppSetTargets( Sim_Man_t * p );
+
+static void   Sim_UtilAssignRandom( Sim_Man_t * p );
+static void   Sim_UtilAssignFromFifo( Sim_Man_t * p );
+static void   Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters );
+static int    Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output );
+
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes structural supports.]
+
+  Description [Supports are returned as an array of bit strings, one
+  for each CO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vSuppStr;
+    Abc_Obj_t * pNode;
+    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
+    int nSuppWords, i, k;
+    // allocate room for structural supports
+    nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
+    vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
+    // assign the structural support to the PIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Sim_SuppStrSetVar( vSuppStr, pNode, i );
+    // derive the structural supports of the internal nodes
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        pSimmNode  = vSuppStr->pArray[ pNode->Id ];
+        pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
+        pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
+        for ( k = 0; k < nSuppWords; k++ )
+            pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
+    }
+    // set the structural supports of the PO nodes
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pSimmNode  = vSuppStr->pArray[ pNode->Id ];
+        pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
+        for ( k = 0; k < nSuppWords; k++ )
+            pSimmNode[k] = pSimmNode1[k];
+    }
+    return vSuppStr;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute functional supports.]
+
+  Description [Supports are returned as an array of bit strings, one
+  for each CO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk )
+{
+    Sim_Man_t * p;
+    Vec_Ptr_t * vResult;
+    int nSolved, i, clk = clock();
+
+//    srand( time(NULL) );
+    srand( 0xABC );
+
+    // start the simulation manager
+    p = Sim_ManStart( pNtk );
+
+    // compute functional support using one round of random simulation
+    Sim_UtilAssignRandom( p );
+    Sim_ComputeSuppRound( p, 0 );
+
+    // set the support targets 
+    Sim_ComputeSuppSetTargets( p );
+printf( "Initial targets    = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
+    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
+        goto exit;
+
+    for ( i = 0; i < 1; i++ )
+    {
+    // compute patterns using one round of random simulation
+    Sim_UtilAssignRandom( p );
+    nSolved = Sim_ComputeSuppRound( p, 1 );
+printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
+    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
+        goto exit;
+    }
+
+
+    // simulate until saturation
+    while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
+    {
+        // solve randomly a given number of targets
+        Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
+        // compute additional functional support
+//        Sim_UtilAssignRandom( p );
+        Sim_UtilAssignFromFifo( p );
+        nSolved = Sim_ComputeSuppRound( p, 1 );
+printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
+            Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
+    }
+
+exit:
+    vResult = p->vSuppFun;  
+    //  p->vSuppFun = NULL;
+    Sim_ManStop( p );
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes functional support using one round of simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_ComputeSuppRound( Sim_Man_t * p, bool fUseTargets )
+{
+    Vec_Int_t * vTargets;
+    Abc_Obj_t * pNode;
+    int i, Counter = 0;
+    int clk;
+    // perform one round of random simulation
+clk = clock();
+    Sim_UtilSimulate( p, 0 );
+p->timeSim += clock() - clk;
+    // iterate through the CIs and detect COs that depend on them
+    Abc_NtkForEachCi( p->pNtk, pNode, i )
+    {
+        vTargets = p->vSuppTargs->pArray[i];
+        if ( fUseTargets && vTargets->nSize == 0 )
+            continue;
+        Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes functional support for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
+{
+    int fVerbose = 0;
+    Sim_Pat_t * pPat;
+    Vec_Int_t * vTargets;
+    Vec_Vec_t * vNodesByLevel;
+    Abc_Obj_t * pNodeCi, * pNode;
+    int i, k, v, Output, LuckyPat, fType0, fType1;
+    int Counter = 0;
+    int fFirst = 1;
+    int clk;
+    // collect nodes by level in the TFO of the CI 
+    // (this procedure increments TravId of the collected nodes)
+clk = clock();
+    pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
+    vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
+p->timeTrav += clock() - clk;
+    // complement the simulation info of the selected CI
+    Sim_UtilInfoFlip( p, pNodeCi );
+    // simulate the levelized structure of nodes
+    Vec_VecForEachEntry( vNodesByLevel, pNode, i, k )
+    {
+        fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
+        fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
+clk = clock();
+        Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
+p->timeSim += clock() - clk;
+    }
+    // set the simulation info of the affected COs
+    if ( fUseTargets )
+    {
+        vTargets = p->vSuppTargs->pArray[iNumCi];
+        for ( i = vTargets->nSize - 1; i >= 0; i-- )
+        {
+            // get the target output
+            Output = vTargets->pArray[i];
+            // get the target node
+            pNode  = Abc_NtkCo( p->pNtk, Output );
+            // the output should be in the cone
+            assert( Abc_NodeIsTravIdCurrent(pNode) );
+
+            // simulate the node
+            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
+
+            // skip if the simulation info is equal
+            if ( Sim_UtilInfoCompare( p, pNode ) )
+                continue;
+
+            // otherwise, we solved a new target
+            Vec_IntRemove( vTargets, Output );
+if ( fVerbose )
+    printf( "(%d,%d) ", iNumCi, Output );
+            Counter++;
+            // make sure this variable is not yet detected
+            assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) );
+            // set this variable
+            Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+            
+            // detect the differences in the simulation info
+            Sim_UtilInfoDetectDiffs( p->vSim0->pArray[pNode->Id], p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs );
+            // create new patterns
+            if ( !fFirst && p->vFifo->nSize > 1000 )
+                continue;
+
+            Vec_IntForEachEntry( p->vDiffs, LuckyPat, k )
+            {
+                // set the new pattern
+                pPat = Sim_ManPatAlloc( p );
+                pPat->Input  = iNumCi;
+                pPat->Output = Output;
+                Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
+                    if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) )
+                        Sim_SetBit( pPat->pData, v );
+                Vec_PtrPush( p->vFifo, pPat );
+
+                fFirst = 0;
+                break;
+            }
+        }
+if ( fVerbose && Counter )
+printf( "\n" );
+    }
+    else
+    {
+        Abc_NtkForEachCo( p->pNtk, pNode, Output )
+        {
+            if ( !Abc_NodeIsTravIdCurrent( pNode ) )
+                continue;
+            Sim_UtilSimulateNode( p, pNode, 1, 1, 1 );
+            if ( !Sim_UtilInfoCompare( p, pNode ) )
+            {
+                if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
+                    Counter++;
+                Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
+            }
+        }
+    }
+    Vec_VecFree( vNodesByLevel );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the simulation targets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_ComputeSuppSetTargets( Sim_Man_t * p )
+{
+    Abc_Obj_t * pNode;
+    unsigned * pSuppStr, * pSuppFun;
+    int i, k, Num;
+    Abc_NtkForEachCo( p->pNtk, pNode, i )
+    {
+        pSuppStr = p->vSuppStr->pArray[pNode->Id];
+        pSuppFun = p->vSuppFun->pArray[i];
+        // find vars in the structural support that are not in the functional support
+        Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs );
+        Vec_IntForEachEntry( p->vDiffs, Num, k )
+            Vec_VecPush( p->vSuppTargs, Num, (void *)i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns random simulation info to the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilAssignRandom( Sim_Man_t * p )
+{
+    Abc_Obj_t * pNode;
+    unsigned * pSimInfo;
+    int i, k;
+    // assign the random/systematic simulation info to the PIs
+    Abc_NtkForEachCi( p->pNtk, pNode, i )
+    {
+        pSimInfo = p->vSim0->pArray[pNode->Id];
+        for ( k = 0; k < p->nSimWords; k++ )
+            pSimInfo[k] = SIM_RANDOM_UNSIGNED;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the new patterns from fifo.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilAssignFromFifo( Sim_Man_t * p )
+{
+    int fUseOneWord = 0;
+    Abc_Obj_t * pNode;
+    Sim_Pat_t * pPat;
+    unsigned * pSimInfo;
+    int iWord, iWordLim, i, w;
+    int iBeg, iEnd;
+    int Counter = 0;
+    // go through the patterns and fill in the dist-1 minterms for each
+    for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim )
+    {
+        ++Counter;
+        // get the pattern
+        pPat = Vec_PtrPop( p->vFifo );
+        if ( fUseOneWord )
+        {
+            // get the first word of the next series
+            iWordLim = iWord + 1; 
+            // set the pattern for all PIs from iBit to iWord + p->nInputs
+            iBeg = ABC_MAX( 0, pPat->Input - 16 );
+            iEnd = ABC_MIN( iBeg + 32, p->nInputs );
+//            for ( i = iBeg; i < iEnd; i++ )
+            Abc_NtkForEachCi( p->pNtk, pNode, i )
+            {
+                pNode = Abc_NtkCi(p->pNtk,i);
+                pSimInfo = p->vSim0->pArray[pNode->Id];
+                if ( Sim_HasBit(pPat->pData, i) )
+                    pSimInfo[iWord] = SIM_MASK_FULL;
+                else
+                    pSimInfo[iWord] = 0;
+                // flip one bit
+                if ( i >= iBeg && i < iEnd )
+                    Sim_XorBit( pSimInfo + iWord, i-iBeg );
+            }
+        }
+        else
+        {
+            // get the first word of the next series
+            iWordLim = (iWord + p->nSuppWords < p->nSimWords)? iWord + p->nSuppWords : p->nSimWords; 
+            // set the pattern for all PIs from iBit to iWord + p->nInputs
+            Abc_NtkForEachCi( p->pNtk, pNode, i )
+            {
+                pSimInfo = p->vSim0->pArray[pNode->Id];
+                if ( Sim_HasBit(pPat->pData, i) )
+                {
+                    for ( w = iWord; w < iWordLim; w++ )
+                        pSimInfo[w] = SIM_MASK_FULL;
+                }
+                else
+                {
+                    for ( w = iWord; w < iWordLim; w++ )
+                        pSimInfo[w] = 0;
+                }
+                // flip one bit
+                Sim_XorBit( pSimInfo + iWord, i );
+            }
+        }
+        Sim_ManPatFree( p, pPat );
+        // stop if we ran out of room for patterns
+        if ( iWordLim == p->nSimWords )
+            break;
+//        if ( Counter == 1 )
+//            break;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Get the given number of counter-examples using SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
+{
+    Fraig_Params_t Params;
+    Fraig_Man_t * pMan;
+    Abc_Obj_t * pNodeCi;
+    Abc_Ntk_t * pMiter;
+    Sim_Pat_t * pPat;
+    void * pEntry;
+    int * pModel;
+    int RetValue, Output, Input, k, v;
+    int Counter = 0;
+    int clk;
+
+    p->nSatRuns = 0;
+    // put targets into one array
+    Vec_VecForEachEntryReverse( p->vSuppTargs, pEntry, Input, k )
+    {
+        p->nSatRuns++;
+        Output = (int)pEntry;
+        // set up the miter for the two cofactors of this output w.r.t. this input
+        pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );
+
+        // transform the target into a fraig
+        Fraig_ParamsSetDefault( &Params );
+        Params.fInternal = 1;
+clk = clock();
+        pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+p->timeFraig += clock() - clk;
+clk = clock();
+        Fraig_ManProveMiter( pMan );
+p->timeSat += clock() - clk;
+
+        // analyze the result
+        RetValue = Fraig_ManCheckMiter( pMan );
+        assert( RetValue >= 0 );
+        if ( RetValue == 1 ) // unsat
+        {
+            p->nSatRunsUnsat++;
+            pModel = NULL;
+            Vec_PtrRemove( p->vSuppTargs->pArray[Input], pEntry );
+        }
+        else // sat
+        {
+            p->nSatRunsSat++;
+            pModel = Fraig_ManReadModel( pMan );
+            assert( pModel != NULL );
+            assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) );
+
+//printf( "Solved by SAT (%d,%d).\n", Input, Output );
+            // set the new pattern
+            pPat = Sim_ManPatAlloc( p );
+            pPat->Input  = Input;
+            pPat->Output = Output;
+            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
+                if ( pModel[v] )
+                    Sim_SetBit( pPat->pData, v );
+            Vec_PtrPush( p->vFifo, pPat );
+/*
+            // set the new pattern
+            pPat = Sim_ManPatAlloc( p );
+            pPat->Input  = Input;
+            pPat->Output = Output;
+            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
+                if ( pModel[v] )
+                    Sim_SetBit( pPat->pData, v );
+            Sim_XorBit( pPat->pData, Input ); // flip the given bit
+            Vec_PtrPush( p->vFifo, pPat );
+*/
+            Counter++;
+        }
+        // delete the fraig manager
+        Fraig_ManFree( pMan );
+        // delete the target
+        Abc_NtkDelete( pMiter );
+
+        // stop when we found enough patterns
+//        if ( Counter == Limit )
+        if ( Counter == 1 )
+            return;
+        // switch to the next input if we found one model
+        if ( pModel )
+            break;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the counter example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode )
+{
+    int Value0, Value1;
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return (int)pNode->pCopy;
+    Abc_NodeSetTravIdCurrent( pNode );
+    Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
+    Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
+    if ( Abc_ObjFaninC0(pNode) )
+        Value0 = ~Value0;
+    if ( Abc_ObjFaninC1(pNode) )
+        Value1 = ~Value1;
+    pNode->pCopy = (Abc_Obj_t *)(Value0 & Value1);
+    return Value0 & Value1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies that pModel proves the presence of Input in the support of Output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output )
+{
+    Abc_Obj_t * pNode;
+    int RetValue, i;
+    // set the PI values
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        Abc_NodeSetTravIdCurrent( pNode );
+        if ( pNode == Abc_NtkCi(pNtk,Input) )
+            pNode->pCopy = (Abc_Obj_t *)1;
+        else if ( pModel[i] == 1 )
+            pNode->pCopy = (Abc_Obj_t *)3;
+        else
+            pNode->pCopy = NULL;
+    }
+    // perform the traversal
+    RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) );
+    if ( RetValue == 0 || RetValue == 3 )
+    {
+        int x = 0;
+    }
+//    assert( RetValue == 1 || RetValue == 2 ); 
+    return RetValue == 1 || RetValue == 2;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
new file mode 100644
index 00000000..06b730fc
--- /dev/null
+++ b/src/opt/sim/simSwitch.c
@@ -0,0 +1,107 @@
+/**CFile****************************************************************
+
+  FileName    [simSwitch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Computes switching activity of nodes in the ABC network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSwitch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Sim_NodeSimulate( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords );
+static float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes switching activity using simulation.]
+
+  Description [Computes switching activity, which is understood as the
+  probability of switching under random simulation. Assigns the
+  random simulation information at the CI and propagates it through
+  the internal nodes of the AIG.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
+{
+    Vec_Int_t * vSwitching;
+    float * pSwitching;
+    Vec_Ptr_t * vNodes;
+    Vec_Ptr_t * vSimInfo;
+    Abc_Obj_t * pNode;
+    unsigned * pSimInfo;
+    int nSimWords, i;
+
+    // allocate space for simulation info of all nodes
+    nSimWords = SIM_NUM_WORDS(nPatterns);
+    vSimInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSimWords, 0 );
+    // assign the random simulation to the CIs
+    vSwitching = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+    pSwitching = (float *)vSwitching->pArray;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+        Sim_UtilGetRandom( pSimInfo, nSimWords );
+        pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
+    }
+    // simulate the internal nodes
+    vNodes  = Abc_AigDfs( pNtk, 1, 0 );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
+        pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
+        pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
+    }
+    Vec_PtrFree( vNodes );
+    Sim_UtilInfoFree( vSimInfo );
+    return vSwitching;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes switching activity of one node.]
+
+  Description [Uses the formula: Switching = 2 * nOnes * nZeros / (nTotal ^ 2) ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords )
+{
+    int nOnes, nTotal;
+    nTotal = 32 * nSimWords;
+    nOnes = Sim_UtilCountOnes( pSimInfo, nSimWords );
+    return (float)2.0 * nOnes * (nTotal - nOnes) / nTotal / nTotal;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
new file mode 100644
index 00000000..706b13dc
--- /dev/null
+++ b/src/opt/sim/simSym.c
@@ -0,0 +1,93 @@
+/**CFile****************************************************************
+
+  FileName    [simSym.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simulation to determine two-variable symmetries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSym.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes two variable symmetries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_ComputeTwoVarSymms( Abc_Ntk_t * pNtk )
+{
+    Sym_Man_t * p;
+    Vec_Ptr_t * vResult;
+    int Result;
+    int i, clk = clock();
+
+//    srand( time(NULL) );
+    srand( 0xABC );
+
+    // start the simulation manager
+    p = Sym_ManStart( pNtk );
+    p->nPairsTotal = Sim_UtilCountAllPairs( p->vSuppFun, p->nSimWords, p->vPairsTotal );
+
+    // detect symmetries using circuit structure
+    Sim_SymmsStructCompute( pNtk, p->vMatrSymms );
+    p->nPairsSymm = p->nPairsSymmStr = Sim_UtilCountPairs( p->vMatrSymms, p->vPairsSym );
+
+printf( "Total = %6d.  Sym = %6d.  NonSym = %6d.  Remaining = %6d.\n", 
+       p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+
+    // detect symmetries using simulation
+    for ( i = 1; i <= 1000; i++ )
+    {
+        // generate random pattern
+        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
+        // simulate this pattern
+        Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
+        if ( i % 100 != 0 )
+            continue;
+        // count the number of pairs
+        p->nPairsSymm    = Sim_UtilCountPairs( p->vMatrSymms,    p->vPairsSym );
+        p->nPairsNonSymm = Sim_UtilCountPairs( p->vMatrNonSymms, p->vPairsNonSym );
+
+printf( "Total = %6d.  Sym = %6d.  NonSym = %6d.  Remaining = %6d.\n", 
+       p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsTotal-p->nPairsSymm-p->nPairsNonSymm );
+    }
+
+    Result = p->nPairsSymm;
+    vResult = p->vMatrSymms;  
+    //  p->vMatrSymms = NULL;
+    Sym_ManStop( p );
+    return Result;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
new file mode 100644
index 00000000..88e33161
--- /dev/null
+++ b/src/opt/sim/simSymSat.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+  FileName    [simSymSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Satisfiability to determine two variable symmetries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSymSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int   Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 );
+static int   Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the SAT based check.]
+
+  Description [Given two bit matrices, with symm info and non-symm info, 
+  checks the remaining pairs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_SymmsSatComputeOne( Fraig_Man_t * p, Extra_BitMat_t * pMatSym, Extra_BitMat_t * pMatNonSym )
+{
+    int VarsU[512], VarsV[512];
+    int nVarsU, nVarsV;
+    int v, u, i, k;
+    int Counter = 0;
+    int satCalled = 0;
+    int satProved = 0;
+    double Density;
+    int clk = clock();
+
+    extern int symsSat;
+    extern int Fraig_CountBits( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
+
+
+    // count undecided pairs
+    for ( v = 0; v < p->vInputs->nSize; v++ )
+    for ( u = v+1; u < p->vInputs->nSize; u++ )
+    {
+        if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
+            continue;
+        Counter++;
+    }
+    // compute the density of 1's in the input space of the functions
+    Density = (double)Fraig_CountBits(p, Fraig_Regular(p->vOutputs->pArray[0])) * 100.0 / FRAIG_SIM_ROUNDS / 32;
+
+    printf( "Ins = %3d. Pairs to test = %4d. Dens = %5.2f %%. ", 
+        p->vInputs->nSize, Counter, Density );
+
+
+    // go through the remaining variable pairs
+    for ( v = 0; v < p->vInputs->nSize; v++ )
+    for ( u = v+1; u < p->vInputs->nSize; u++ )
+    {
+        if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
+            continue;
+        symsSat++;
+        satCalled++;
+
+        // collect the variables that are symmetric with each
+        nVarsU = nVarsV = 0;
+        for ( i = 0; i < p->vInputs->nSize; i++ )
+        {
+            if ( Extra_BitMatrixLookup1( pMatSym, u, i ) )
+                VarsU[nVarsU++] = i;
+            if ( Extra_BitMatrixLookup1( pMatSym, v, i ) )
+                VarsV[nVarsV++] = i;
+        }
+
+        if ( Fraig_SymmsSatProveOne( p, v, u ) )
+        { // update the symmetric variable info            
+//printf( "%d sym %d\n", v, u );
+            for ( i = 0; i < nVarsU; i++ )
+            for ( k = 0; k < nVarsV; k++ )
+            {
+                Extra_BitMatrixInsert1( pMatSym, VarsU[i], VarsV[k] );   // Theorem 1
+                Extra_BitMatrixInsert2( pMatSym, VarsU[i], VarsV[k] );   // Theorem 1
+                Extra_BitMatrixOrTwo( pMatNonSym, VarsU[i], VarsV[k] );  // Theorem 2
+            }
+            satProved++;
+        }
+        else
+        { // update the assymmetric variable info
+//printf( "%d non-sym %d\n", v, u );
+            for ( i = 0; i < nVarsU; i++ )
+            for ( k = 0; k < nVarsV; k++ )
+            {
+                Extra_BitMatrixInsert1( pMatNonSym, VarsU[i], VarsV[k] );   // Theorem 3
+                Extra_BitMatrixInsert2( pMatNonSym, VarsU[i], VarsV[k] );   // Theorem 3
+            }
+        }
+//Extra_BitMatrixPrint( pMatSym );
+//Extra_BitMatrixPrint( pMatNonSym );
+    }
+printf( "SAT calls = %3d. Proved = %3d. ", satCalled, satProved );
+PRT( "Time", clock() - clk );
+
+    // make sure that the symmetry matrix contains only cliques
+    assert( Fraig_SymmsIsCliqueMatrix( p, pMatSym ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the variables are symmetric; 0 otherwise.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_SymmsSatProveOne( Fraig_Man_t * p, int Var1, int Var2 )
+{
+    Fraig_Node_t * pCof01, * pCof10, * pVar1, * pVar2;
+    int RetValue;
+    int nSatRuns = p->nSatCalls;
+    int nSatProof = p->nSatProof;
+
+    p->nBTLimit = 10;  // set the backtrack limit
+
+    pVar1 = p->vInputs->pArray[Var1];
+    pVar2 = p->vInputs->pArray[Var2];
+    pCof01 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], pVar1, Fraig_Not(pVar2) );
+    pCof10 = Fraig_CofactorTwo( p, p->vOutputs->pArray[0], Fraig_Not(pVar1), pVar2 );
+
+//printf( "(%d,%d)", p->nSatCalls - nSatRuns, p->nSatProof - nSatProof );
+
+//    RetValue = (pCof01 == pCof10);
+//    RetValue = Fraig_NodesAreaEqual( p, pCof01, pCof10 );
+    RetValue = Fraig_NodesAreEqual( p, pCof01, pCof10, -1 );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [A sanity check procedure.]
+
+  Description [Makes sure that the symmetry information in the matrix
+  is closed w.r.t. the relationship of transitivity (that is the symmetry
+  graph is composed of cliques).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fraig_SymmsIsCliqueMatrix( Fraig_Man_t * p, Extra_BitMat_t * pMat )
+{
+    int v, u, i;
+    for ( v = 0; v < p->vInputs->nSize; v++ )
+    for ( u = v+1; u < p->vInputs->nSize; u++ )
+    {
+        if ( !Extra_BitMatrixLookup1( pMat, v, u ) )
+            continue;
+        // v and u are symmetric
+        for ( i = 0; i < p->vInputs->nSize; i++ )
+        {
+            if ( i == v || i == u )
+                continue;
+            // i is neither v nor u
+            // the symmetry status of i is the same w.r.t. to v and u
+            if ( Extra_BitMatrixLookup1( pMat, i, v ) != Extra_BitMatrixLookup1( pMat, i, u ) )
+                return 0;
+        }
+    }
+    return 1;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
new file mode 100644
index 00000000..53fc4ac2
--- /dev/null
+++ b/src/opt/sim/simSymSim.c
@@ -0,0 +1,159 @@
+/**CFile****************************************************************
+
+  FileName    [simSymSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Simulation to determine two-variable symmetries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSymSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat );
+static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMatrix, int Output );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Detects non-symmetric pairs using one pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // create the simulation matrix
+    Sim_SymmsCreateSquare( p, pPat );
+    // simulate each node in the DFS order
+    Vec_PtrForEachEntry( p->vNodes, pNode, i )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords );
+    }
+    // collect info into the CO matrices
+    Abc_NtkForEachCo( p->pNtk, pNode, i )
+    {
+        pNode = Abc_ObjFanin0(pNode);
+        if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) )
+            continue;
+        if ( Vec_IntEntry(p->vPairsTotal,i) == Vec_IntEntry(p->vPairsSym,i) + Vec_IntEntry(p->vPairsNonSym,i) )
+            continue;
+        Sim_SymmsDeriveInfo( p, pPat, pNode, Vec_PtrEntry(vMatrsNonSym, i), i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the square matrix of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat )
+{
+    unsigned * pSimInfo;
+    Abc_Obj_t * pNode;
+    int i, w;
+    // for each PI var copy the pattern
+    Abc_NtkForEachCi( p->pNtk, pNode, i )
+    {
+        pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
+        if ( Sim_HasBit(pPat, i) )
+        {
+            for ( w = 0; w < p->nSimWords; w++ )
+                pSimInfo[w] = SIM_MASK_FULL;
+        }
+        else
+        {
+            for ( w = 0; w < p->nSimWords; w++ )
+                pSimInfo[w] = 0;
+        }
+        // flip one bit
+        Sim_XorBit( pSimInfo, i );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the info to the POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Extra_BitMat_t * pMat, int Output )
+{
+    unsigned * pSuppInfo;
+    unsigned * pSimInfo;
+    int i, w;
+    // get the simuation info for the node
+    pSimInfo = Vec_PtrEntry( p->vSim, pNode->Id );
+    pSuppInfo = Vec_PtrEntry( p->vSuppFun, Output );
+    // generate vectors A1 and A2
+    for ( w = 0; w < p->nSimWords; w++ )
+    {
+        p->uPatCol[w] = pSuppInfo[w] & pPat[w] &  pSimInfo[w];
+        p->uPatRow[w] = pSuppInfo[w] & pPat[w] & ~pSimInfo[w];
+    }
+    // add two dimensions
+    for ( i = 0; i < p->nInputs; i++ )
+        if ( Sim_HasBit( p->uPatCol, i ) )
+            Extra_BitMatrixOr( pMat, i, p->uPatRow );
+    // add two dimensions
+    for ( i = 0; i < p->nInputs; i++ )
+        if ( Sim_HasBit( p->uPatRow, i ) )
+            Extra_BitMatrixOr( pMat, i, p->uPatCol );
+    // generate vectors B1 and B2
+    for ( w = 0; w < p->nSimWords; w++ )
+    {
+        p->uPatCol[w] = pSuppInfo[w] & ~pPat[w] &  pSimInfo[w];
+        p->uPatRow[w] = pSuppInfo[w] & ~pPat[w] & ~pSimInfo[w];
+    }
+    // add two dimensions
+    for ( i = 0; i < p->nInputs; i++ )
+        if ( Sim_HasBit( p->uPatCol, i ) )
+            Extra_BitMatrixOr( pMat, i, p->uPatRow );
+    // add two dimensions
+    for ( i = 0; i < p->nInputs; i++ )
+        if ( Sim_HasBit( p->uPatRow, i ) )
+            Extra_BitMatrixOr( pMat, i, p->uPatCol );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
new file mode 100644
index 00000000..c3059d84
--- /dev/null
+++ b/src/opt/sim/simSymStr.c
@@ -0,0 +1,481 @@
+/**CFile****************************************************************
+
+  FileName    [simSymStr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Structural detection of symmetries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simSymStr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define SIM_READ_SYMMS(pNode)       ((Vec_Int_t *)pNode->pCopy) 
+#define SIM_SET_SYMMS(pNode,vVect)  (pNode->pCopy = (Abc_Obj_t *)(vVect)) 
+
+static void  Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap );
+static void  Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void  Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther );
+static void  Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap );
+static void  Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap );
+static int   Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap );
+static int   Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap );
+static void  Sim_SymmsPrint( Vec_Int_t * vSymms );
+static void  Sim_SymmsTrans( Vec_Int_t * vSymms );
+static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms );
+static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes symmetries for a single output function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pTemp;
+    int * pMap, i;
+
+    assert( Abc_NtkCiNum(pNtk) + 10 < (1<<16) );
+
+    // get the structural support
+    pNtk->vSupps = Sim_ComputeStrSupp( pNtk );
+    // set elementary info for the CIs
+    Abc_NtkForEachCi( pNtk, pTemp, i )
+        SIM_SET_SYMMS( pTemp, Vec_IntAlloc(0) );
+    // create the map of CI ids into their numbers
+    pMap = Sim_SymmsCreateMap( pNtk );
+    // collect the nodes in the TFI cone of this output
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+    {
+        if ( Abc_NodeIsConst(pTemp) )
+            continue;
+        Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
+    }
+    // collect the results for the COs;
+    Abc_NtkForEachCo( pNtk, pTemp, i )
+    {
+        pTemp = Abc_ObjFanin0(pTemp);
+        if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) )
+            continue;
+        Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp) );
+    }
+    // clean the intermediate results
+    Sim_UtilInfoFree( pNtk->vSupps );
+    pNtk->vSupps = NULL;
+    Abc_NtkForEachCi( pNtk, pTemp, i )
+        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+        Vec_IntFree( SIM_READ_SYMMS(pTemp) );
+    Vec_PtrFree( vNodes );
+    free( pMap );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes symmetries. ]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsStructComputeOne( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int * pMap )
+{
+    Vec_Ptr_t * vNodes, * vNodesPi0, * vNodesPi1, * vNodesOther;
+    Vec_Int_t * vSymms;
+    Abc_Obj_t * pTemp;
+    int i;
+
+    // allocate the temporary arrays
+    vNodes      = Vec_PtrAlloc( 10 );
+    vNodesPi0   = Vec_PtrAlloc( 10 );
+    vNodesPi1   = Vec_PtrAlloc( 10 );
+    vNodesOther = Vec_PtrAlloc( 10 );  
+
+    // collect the fanins of the implication supergate
+    Sim_SymmsBalanceCollect_rec( pNode, vNodes );
+
+    // sort the nodes in the implication supergate
+    Sim_SymmsPartitionNodes( vNodes, vNodesPi0, vNodesPi1, vNodesOther );
+
+    // start the resulting set
+    vSymms = Vec_IntAlloc( 10 );
+    // generate symmetries from the groups
+    Sim_SymmsAppendFromGroup( pNtk, vNodesPi0, vNodesOther, vSymms, pMap );
+    Sim_SymmsAppendFromGroup( pNtk, vNodesPi1, vNodesOther, vSymms, pMap );
+    // add symmetries from other inputs
+    for ( i = 0; i < vNodesOther->nSize; i++ )
+    {
+        pTemp = Abc_ObjRegular(vNodesOther->pArray[i]);
+        Sim_SymmsAppendFromNode( pNtk, SIM_READ_SYMMS(pTemp), vNodesOther, vNodesPi0, vNodesPi1, vSymms, pMap );
+    }
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vNodesPi0 );
+    Vec_PtrFree( vNodesPi1 );
+    Vec_PtrFree( vNodesOther );
+
+    // set the symmetry at the node
+    SIM_SET_SYMMS( pNode, vSymms );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of nodes to be combined into one multi-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsBalanceCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    // if the new node is complemented, another gate begins
+    if ( Abc_ObjIsComplement(pNode) )
+    {
+        Vec_PtrPushUnique( vNodes, pNode );
+        return;
+    }
+    // if pNew is the PI node, return
+    if ( Abc_ObjIsCi(pNode) )
+    {
+        Vec_PtrPushUnique( vNodes, pNode );
+        return;    
+    }
+    // go through the branches
+    Sim_SymmsBalanceCollect_rec( Abc_ObjChild0(pNode), vNodes );
+    Sim_SymmsBalanceCollect_rec( Abc_ObjChild1(pNode), vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Divides PI variables into groups.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsPartitionNodes( Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesPis0, 
+    Vec_Ptr_t * vNodesPis1, Vec_Ptr_t * vNodesOther )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( !Abc_ObjIsCi(Abc_ObjRegular(pNode)) )
+            Vec_PtrPush( vNodesOther, pNode );
+        else if ( Abc_ObjIsComplement(pNode) )
+            Vec_PtrPush( vNodesPis0, pNode );
+        else
+            Vec_PtrPush( vNodesPis1, pNode );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the product of two partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsAppendFromGroup( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesPi, Vec_Ptr_t * vNodesOther, Vec_Int_t * vSymms, int * pMap )
+{
+    Abc_Obj_t * pNode1, * pNode2;
+    unsigned uSymm;
+    int i, k;
+
+    if ( vNodesPi->nSize == 0 )
+        return;
+
+    // go through the pairs
+    for ( i = 0; i < vNodesPi->nSize; i++ )
+    for ( k = i+1; k < vNodesPi->nSize; k++ )
+    {
+        // get the two PI nodes
+        pNode1 = Abc_ObjRegular(vNodesPi->pArray[i]);
+        pNode2 = Abc_ObjRegular(vNodesPi->pArray[k]);
+        assert( pMap[pNode1->Id] != pMap[pNode2->Id] );
+        assert( pMap[pNode1->Id] >= 0 );
+        assert( pMap[pNode2->Id] >= 0 );
+        // generate symmetry
+        if ( pMap[pNode1->Id] < pMap[pNode2->Id] )
+            uSymm = ((pMap[pNode1->Id] << 16) | pMap[pNode2->Id]);
+        else
+            uSymm = ((pMap[pNode2->Id] << 16) | pMap[pNode1->Id]);
+        // check if symmetry belongs
+        if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) )
+            Vec_IntPushUnique( vSymms, (int)uSymm );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the filters symmetries from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsAppendFromNode( Abc_Ntk_t * pNtk, Vec_Int_t * vSymms0, Vec_Ptr_t * vNodesOther, 
+    Vec_Ptr_t * vNodesPi0, Vec_Ptr_t * vNodesPi1, Vec_Int_t * vSymms, int * pMap )
+{
+    unsigned uSymm;
+    int i;
+
+    if ( vSymms0->nSize == 0 )
+        return;
+
+    // go through the pairs
+    for ( i = 0; i < vSymms0->nSize; i++ )
+    {
+        uSymm = (unsigned)vSymms0->pArray[i];
+        // check if symmetry belongs
+        if ( Sim_SymmsIsCompatibleWithNodes( pNtk, uSymm, vNodesOther, pMap ) &&
+             Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi0, pMap ) && 
+             Sim_SymmsIsCompatibleWithGroup( uSymm, vNodesPi1, pMap ) )
+            Vec_IntPushUnique( vSymms, (int)uSymm );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if symmetry is compatible with the group of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_SymmsIsCompatibleWithNodes( Abc_Ntk_t * pNtk, unsigned uSymm, Vec_Ptr_t * vNodesOther, int * pMap )
+{
+    Vec_Int_t * vSymmsNode;
+    Abc_Obj_t * pNode;
+    int i, s, Ind1, Ind2, fIsVar1, fIsVar2;
+
+    if ( vNodesOther->nSize == 0 )
+        return 1;
+
+    // get the indices of the PI variables
+    Ind1 = (uSymm & 0xffff);
+    Ind2 = (uSymm >> 16);
+
+    // go through the nodes
+    // if they do not belong to a support, it is okay
+    // if one belongs, the other does not belong, quit
+    // if they belong, but are not part of symmetry, quit
+    for ( i = 0; i < vNodesOther->nSize; i++ )
+    {
+        pNode = Abc_ObjRegular(vNodesOther->pArray[i]);
+        fIsVar1 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind1 );
+        fIsVar2 = Sim_SuppStrHasVar( pNtk->vSupps, pNode, Ind2 );
+
+        if ( !fIsVar1 && !fIsVar2 )
+            continue;
+        if ( fIsVar1 ^ fIsVar2 )
+            return 0;
+        // both belong
+        // check if there is a symmetry
+        vSymmsNode = SIM_READ_SYMMS( pNode );
+        for ( s = 0; s < vSymmsNode->nSize; s++ )
+            if ( uSymm == (unsigned)vSymmsNode->pArray[s] )
+                break;
+        if ( s == vSymmsNode->nSize )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if symmetry is compatible with the group of PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_SymmsIsCompatibleWithGroup( unsigned uSymm, Vec_Ptr_t * vNodesPi, int * pMap )
+{
+    Abc_Obj_t * pNode;
+    int i, Ind1, Ind2, fHasVar1, fHasVar2;
+
+    if ( vNodesPi->nSize == 0 )
+        return 1;
+
+    // get the indices of the PI variables
+    Ind1 = (uSymm & 0xffff);
+    Ind2 = (uSymm >> 16);
+
+    // go through the PI nodes
+    fHasVar1 = fHasVar2 = 0;
+    for ( i = 0; i < vNodesPi->nSize; i++ )
+    {
+        pNode = Abc_ObjRegular(vNodesPi->pArray[i]);
+        if ( pMap[pNode->Id] == Ind1 )
+            fHasVar1 = 1;
+        else if ( pMap[pNode->Id] == Ind2 )
+            fHasVar2 = 1;
+    }
+    return fHasVar1 == fHasVar2;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Improvements due to transitivity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsTrans( Vec_Int_t * vSymms )
+{
+    unsigned uSymm, uSymma, uSymmr;
+    int i, Ind1, Ind2;
+    int k, Ind1a, Ind2a;
+    int j;
+    int nTrans = 0;
+
+    for ( i = 0; i < vSymms->nSize; i++ )
+    {
+        uSymm = (unsigned)vSymms->pArray[i];
+        Ind1 = (uSymm & 0xffff);
+        Ind2 = (uSymm >> 16);
+        // find other symmetries that have Ind1
+        for ( k = i+1; k < vSymms->nSize; k++ )
+        {
+            uSymma = (unsigned)vSymms->pArray[k];
+            if ( uSymma == uSymm )
+                continue;
+            Ind1a = (uSymma & 0xffff);
+            Ind2a = (uSymma >> 16);
+            if ( Ind1a == Ind1 )
+            {
+                // find the symmetry (Ind2,Ind2a)
+                if ( Ind2 < Ind2a )
+                    uSymmr = ((Ind2 << 16) | Ind2a);
+                else
+                    uSymmr = ((Ind2a << 16) | Ind2);
+                for ( j = 0; j < vSymms->nSize; j++ )
+                    if ( uSymmr == (unsigned)vSymms->pArray[j] )
+                        break;
+                if ( j == vSymms->nSize )
+                    nTrans++;
+            }
+        }
+
+    }
+    printf( "Trans = %d.\n", nTrans );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers from the vector to the matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms )
+{
+    int i, Ind1, Ind2, nInputs;
+    unsigned uSymm;
+    // add diagonal elements
+    nInputs = Extra_BitMatrixReadSize( pMatSymm );
+    for ( i = 0; i < nInputs; i++ )
+        Extra_BitMatrixInsert1( pMatSymm, i, i );
+    // add non-diagonal elements
+    for ( i = 0; i < vSymms->nSize; i++ )
+    {
+        uSymm = (unsigned)vSymms->pArray[i];
+        Ind1 = (uSymm & 0xffff);
+        Ind2 = (uSymm >> 16);
+        Extra_BitMatrixInsert1( pMatSymm, Ind1, Ind2 );
+        Extra_BitMatrixInsert2( pMatSymm, Ind1, Ind2 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mapping of indices into numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk )
+{
+    int * pMap;
+    Abc_Obj_t * pNode;
+    int i;
+    pMap = ALLOC( int, Abc_NtkObjNumMax(pNtk) );
+    for ( i = 0; i < Abc_NtkObjNumMax(pNtk); i++ )
+        pMap[i] = -1;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pMap[pNode->Id] = i;
+    return pMap;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
new file mode 100644
index 00000000..5a57ca2d
--- /dev/null
+++ b/src/opt/sim/simUtils.c
@@ -0,0 +1,457 @@
+/**CFile****************************************************************
+
+  FileName    [simUtils.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Various simulation utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: simUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "sim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static int bit_count[256] = {
+  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation information for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Sim_UtilInfoAlloc( int nSize, int nWords, bool fClean )
+{
+    Vec_Ptr_t * vInfo;
+    int i;
+    assert( nSize > 0 && nWords > 0 );
+    vInfo = Vec_PtrAlloc( nSize );
+    vInfo->pArray[0] = ALLOC( unsigned, nSize * nWords );
+    if ( fClean )
+        memset( vInfo->pArray[0], 0, sizeof(unsigned) * nSize * nWords );
+    for ( i = 1; i < nSize; i++ )
+        vInfo->pArray[i] = ((unsigned *)vInfo->pArray[i-1]) + nWords;
+    vInfo->nSize = nSize;
+    return vInfo;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates simulation information for all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilInfoFree( Vec_Ptr_t * p )
+{
+    free( p->pArray[0] );
+    Vec_PtrFree( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the second supp-info the first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilInfoAdd( unsigned * pInfo1, unsigned * pInfo2, int nWords )
+{
+    int w;
+    for ( w = 0; w < nWords; w++ )
+        pInfo1[w] |= pInfo2[w];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the positions where pInfo2 is 1 while pInfo1 is 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilInfoDetectDiffs( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs )
+{
+    int w, b;
+    unsigned uMask;
+    vDiffs->nSize = 0;
+    for ( w = 0; w < nWords; w++ )
+        if ( uMask = (pInfo2[w] ^ pInfo1[w]) )
+            for ( b = 0; b < 32; b++ )
+                if ( uMask & (1 << b) )
+                    Vec_IntPush( vDiffs, 32*w + b );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the positions where pInfo2 is 1 while pInfo1 is 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilInfoDetectNews( unsigned * pInfo1, unsigned * pInfo2, int nWords, Vec_Int_t * vDiffs )
+{
+    int w, b;
+    unsigned uMask;
+    vDiffs->nSize = 0;
+    for ( w = 0; w < nWords; w++ )
+        if ( uMask = (pInfo2[w] & ~pInfo1[w]) )
+            for ( b = 0; b < 32; b++ )
+                if ( uMask & (1 << b) )
+                    Vec_IntPush( vDiffs, 32*w + b );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Flips the simulation info of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilInfoFlip( Sim_Man_t * p, Abc_Obj_t * pNode )
+{
+    unsigned * pSimInfo1, * pSimInfo2;
+    int k;
+    pSimInfo1 = p->vSim0->pArray[pNode->Id];
+    pSimInfo2 = p->vSim1->pArray[pNode->Id];
+    for ( k = 0; k < p->nSimWords; k++ )
+        pSimInfo2[k] = ~pSimInfo1[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Sim_UtilInfoCompare( Sim_Man_t * p, Abc_Obj_t * pNode )
+{
+    unsigned * pSimInfo1, * pSimInfo2;
+    int k;
+    pSimInfo1 = p->vSim0->pArray[pNode->Id];
+    pSimInfo2 = p->vSim1->pArray[pNode->Id];
+    for ( k = 0; k < p->nSimWords; k++ )
+        if ( pSimInfo2[k] != pSimInfo1[k] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilSimulate( Sim_Man_t * p, bool fType )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // simulate the internal nodes
+    Abc_NtkForEachNode( p->pNtk, pNode, i )
+        Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
+    // assign simulation info of the CO nodes
+    Abc_NtkForEachCo( p->pNtk, pNode, i )
+        Sim_UtilSimulateNode( p, pNode, fType, fType, fType );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fType1, bool fType2 )
+{
+    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
+    int k, fComp1, fComp2;
+    // simulate the internal nodes
+    if ( Abc_ObjIsNode(pNode) )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            return;
+
+        if ( fType )
+            pSimmNode  = p->vSim1->pArray[ pNode->Id ];
+        else
+            pSimmNode  = p->vSim0->pArray[ pNode->Id ];
+
+        if ( fType1 )
+            pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
+        else
+            pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
+
+        if ( fType2 )
+            pSimmNode2 = p->vSim1->pArray[ Abc_ObjFaninId1(pNode) ];
+        else
+            pSimmNode2 = p->vSim0->pArray[ Abc_ObjFaninId1(pNode) ];
+
+        fComp1 = Abc_ObjFaninC0(pNode);
+        fComp2 = Abc_ObjFaninC1(pNode);
+        if ( fComp1 && fComp2 )
+            for ( k = 0; k < p->nSimWords; k++ )
+                pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
+        else if ( fComp1 && !fComp2 )
+            for ( k = 0; k < p->nSimWords; k++ )
+                pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
+        else if ( !fComp1 && fComp2 )
+            for ( k = 0; k < p->nSimWords; k++ )
+                pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
+        else // if ( fComp1 && fComp2 )
+            for ( k = 0; k < p->nSimWords; k++ )
+                pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
+    }
+    else 
+    {
+        assert( Abc_ObjFaninNum(pNode) == 1 );
+        if ( fType )
+            pSimmNode  = p->vSim1->pArray[ pNode->Id ];
+        else
+            pSimmNode  = p->vSim0->pArray[ pNode->Id ];
+
+        if ( fType1 )
+            pSimmNode1 = p->vSim1->pArray[ Abc_ObjFaninId0(pNode) ];
+        else
+            pSimmNode1 = p->vSim0->pArray[ Abc_ObjFaninId0(pNode) ];
+
+        fComp1 = Abc_ObjFaninC0(pNode);
+        if ( fComp1 )
+            for ( k = 0; k < p->nSimWords; k++ )
+                pSimmNode[k] = ~pSimmNode1[k];
+        else 
+            for ( k = 0; k < p->nSimWords; k++ )
+                pSimmNode[k] =  pSimmNode1[k];
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords )
+{
+    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
+    int k, fComp1, fComp2;
+    // simulate the internal nodes
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Abc_NodeIsConst(pNode) )
+        return;
+    pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
+    pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
+    pSimmNode2 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId1(pNode));
+    fComp1 = Abc_ObjFaninC0(pNode);
+    fComp2 = Abc_ObjFaninC1(pNode);
+    if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pSimmNode[k] = ~pSimmNode1[k] & ~pSimmNode2[k];
+    else if ( fComp1 && !fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pSimmNode[k] = ~pSimmNode1[k] &  pSimmNode2[k];
+    else if ( !fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pSimmNode[k] =  pSimmNode1[k] & ~pSimmNode2[k];
+    else // if ( fComp1 && fComp2 )
+        for ( k = 0; k < nSimWords; k++ )
+            pSimmNode[k] =  pSimmNode1[k] &  pSimmNode2[k];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilCountSuppSizes( Sim_Man_t * p, int fStruct )
+{
+    Abc_Obj_t * pNode, * pNodeCi;
+    int i, v, Counter;
+    Counter = 0;
+    if ( fStruct )
+    {
+        Abc_NtkForEachCo( p->pNtk, pNode, i )
+            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
+                Counter += Sim_SuppStrHasVar( p->vSuppStr, pNode, v );
+    }
+    else
+    {
+        Abc_NtkForEachCo( p->pNtk, pNode, i )
+            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
+                Counter += Sim_SuppFunHasVar( p->vSuppFun, i, v );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1's in the bitstring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
+{
+    unsigned char * pBytes;
+    int nOnes, nBytes, i;
+    pBytes = (unsigned char *)pSimInfo;
+    nBytes = 4 * nSimWords;
+    nOnes  = 0;
+    for ( i = 0; i < nBytes; i++ )
+        nOnes += bit_count[ pBytes[i] ];
+    return nOnes;    
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the random pattern.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords )
+{
+    int k;
+    for ( k = 0; k < nSimWords; k++ )
+        pPatRand[k] = SIM_RANDOM_UNSIGNED;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the total number of pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWords, Vec_Int_t * vCounters )
+{
+    unsigned * pSupp;
+    int Counter, nOnes, nPairs, i;
+    Counter = 0;
+    Vec_PtrForEachEntry( vSuppFun, pSupp, i )
+    {
+        nOnes  = Sim_UtilCountOnes( pSupp, nSimWords );
+        nPairs = nOnes * (nOnes - 1) / 2;
+        Vec_IntWriteEntry( vCounters, i, nPairs );
+        Counter += nPairs;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of entries in the array of matrices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sim_UtilCountPairs( Vec_Ptr_t * vMatrs, Vec_Int_t * vCounters )
+{
+    Extra_BitMat_t * vMat;
+    int Counter, nPairs, i;
+    Counter = 0;
+    Vec_PtrForEachEntry( vMatrs, vMat, i )
+    {
+        nPairs = Extra_BitMatrixCountOnesUpper( vMat );
+        Vec_IntWriteEntry( vCounters, i, nPairs );
+        Counter += nPairs;
+    }
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+