Version abc80130

12 files changed, 71 insertions, 454 deletions

diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
index 54058402..43d0a125 100644
--- a/src/opt/sim/module.make
+++ b/src/opt/sim/module.make
@@ -1,6 +1,5 @@
 SRC +=  src/opt/sim/simMan.c \
     src/opt/sim/simSat.c \
-    src/opt/sim/simSeq.c \
     src/opt/sim/simSupp.c \
     src/opt/sim/simSwitch.c \
     src/opt/sim/simSym.c \
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 7fcf5ae6..afed7190 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -17,14 +17,10 @@
   Revision    [$Id: sim.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
-
+ 
 #ifndef __SIM_H__
 #define __SIM_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 /*
     The ideas realized in this package are described in the paper:
     "Detecting Symmetries in Boolean Functions using Circuit Representation, 
@@ -102,7 +98,6 @@ struct Sim_Man_t_
     Abc_Ntk_t *       pNtk;
     int               nInputs;
     int               nOutputs;
-    int               fLightweight;
     // internal simulation information
     int               nSimBits;      // the number of bits in simulation info
     int               nSimWords;     // the number of words in simulation info
@@ -140,11 +135,11 @@ struct Sim_Pat_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
+///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
-#define SIM_NUM_WORDS(n)      (((n)>>5) + (((n)&31) > 0))
-#define SIM_LAST_BITS(n)      ((((n)&31) > 0)? (n)&31 : 32)
+#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))
@@ -167,7 +162,6 @@ struct Sim_Pat_t_
 #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))
-#define Sim_SimInfoGet(vInfo,pNode)           ((unsigned *)((vInfo)->pArray[(pNode)->Id]))
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -177,14 +171,11 @@ struct Sim_Pat_t_
 extern Sym_Man_t *     Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose );
 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, int fLightweight );
+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 );
-/*=== simSeq.c ==========================================================*/
-extern Vec_Ptr_t *     Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords );
-extern Vec_Ptr_t *     Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel );
 /*=== simSupp.c ==========================================================*/
 extern Vec_Ptr_t *     Sim_ComputeStrSupp( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *     Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
@@ -206,28 +197,17 @@ 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, int nOffset );
-extern void            Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift );
+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 Vec_Int_t *     Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords );
-extern void            Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords );
-extern void            Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords );
-extern void            Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 );
-extern int             Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords );
-extern int             Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords );
-extern int             Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, 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 void            Sim_UtilCountPairsAll( Sym_Man_t * p );
 extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
+
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
index 3b50ad84..780ecfd8 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -26,12 +26,12 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the simulation manager.]
+  Synopsis    [Starts the simulatin manager.]
 
   Description []
                
@@ -83,7 +83,7 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
 
 /**Function*************************************************************
 
-  Synopsis    [Stops the simulation manager.]
+  Synopsis    [Stops the simulatin manager.]
 
   Description []
                
@@ -149,9 +149,11 @@ void Sym_ManPrintStats( Sym_Man_t * p )
 }
 
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Starts the simulation manager.]
+  Synopsis    [Starts the simulatin manager.]
 
   Description []
                
@@ -160,7 +162,7 @@ void Sym_ManPrintStats( Sym_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
+Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
 {
     Sim_Man_t * p;
     // start the manager
@@ -173,27 +175,24 @@ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
     p->nSimBits   = 2048;
     p->nSimWords  = SIM_NUM_WORDS(p->nSimBits);
     p->vSim0      = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), p->nSimWords, 0 );
-    p->fLightweight = fLightweight;
-    if (!p->fLightweight) {
-        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 );
-    }
+    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 simulation manager.]
+  Synopsis    [Stops the simulatin manager.]
 
   Description []
                
@@ -210,7 +209,7 @@ void Sim_ManStop( Sim_Man_t * p )
     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 );
+    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat, 0 );
     if ( p->vFifo )        Vec_PtrFree( p->vFifo );
     if ( p->vDiffs )       Vec_IntFree( p->vDiffs );
     free( p );
diff --git a/src/opt/sim/simSat.c b/src/opt/sim/simSat.c
index d514f7f2..b4e080fe 100644
--- a/src/opt/sim/simSat.c
+++ b/src/opt/sim/simSat.c
@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
  
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c
deleted file mode 100644
index 49fb939f..00000000
--- a/src/opt/sim/simSeq.c
+++ /dev/null
@@ -1,171 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [simSeq.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    [Simulation for sequential circuits.]
-
-  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 void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates sequential circuit.]
-
-  Description [Takes sequential circuit (pNtk). Simulates the given number
-  (nFrames) of the circuit with the given number of machine words (nWords)
-  of random simulation data, starting from the initial state. If the initial
-  state of some latches is a don't-care, uses random input for that latch.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_SimulateSeqRandom( Abc_Ntk_t * pNtk, int nFrames, int nWords )
-{
-    Vec_Ptr_t * vInfo;
-    Abc_Obj_t * pNode;
-    int i;
-    assert( Abc_NtkIsStrash(pNtk) );
-    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nWords * nFrames, 0 );
-    // set the constant data
-    pNode = Abc_AigConst1(pNtk);
-    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames, 1 );
-    // set the random PI data
-    Abc_NtkForEachPi( pNtk, pNode, i )
-        Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords * nFrames );
-    // set the initial state data
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-        if ( Abc_LatchIsInit0(pNode) )
-            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 0 );
-        else if ( Abc_LatchIsInit1(pNode) )
-            Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nWords, 1 );
-        else 
-            Sim_UtilSetRandom( Sim_SimInfoGet(vInfo,pNode), nWords );
-    // simulate the nodes for the given number of timeframes
-    for ( i = 0; i < nFrames; i++ )
-        Sim_SimulateSeqFrame( vInfo, pNtk, i, nWords, (int)(i < nFrames-1) );
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates sequential circuit.]
-
-  Description [Takes sequential circuit (pNtk). Simulates the given number
-  (nFrames) of the circuit with the given model. The model is assumed to 
-  contain values of PIs for each frame. The latches are initialized to
-  the initial state. One word of data is simulated.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Sim_SimulateSeqModel( Abc_Ntk_t * pNtk, int nFrames, int * pModel )
-{
-    Vec_Ptr_t * vInfo;
-    Abc_Obj_t * pNode;
-    unsigned * pUnsigned;
-    int i, k;
-    vInfo = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nFrames, 0 );
-    // set the constant data
-    pNode = Abc_AigConst1(pNtk);
-    Sim_UtilSetConst( Sim_SimInfoGet(vInfo,pNode), nFrames, 1 );
-    // set the random PI data
-    Abc_NtkForEachPi( pNtk, pNode, i )
-    {
-        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
-        for ( k = 0; k < nFrames; k++ )
-            pUnsigned[k] = pModel[k * Abc_NtkPiNum(pNtk) + i] ? ~((unsigned)0) : 0;
-    }
-    // set the initial state data
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-    {
-        pUnsigned = Sim_SimInfoGet(vInfo,pNode);
-        if ( Abc_LatchIsInit0(pNode) )
-            pUnsigned[0] = 0;
-        else if ( Abc_LatchIsInit1(pNode) )
-            pUnsigned[0] = ~((unsigned)0);
-        else 
-            pUnsigned[0] = SIM_RANDOM_UNSIGNED;
-    }
-    // simulate the nodes for the given number of timeframes
-    for ( i = 0; i < nFrames; i++ )
-        Sim_SimulateSeqFrame( vInfo, pNtk, i, 1, (int)(i < nFrames-1) );
-/*
-    // print the simulated values
-    for ( i = 0; i < nFrames; i++ )
-    {
-        printf( "Frame %d : ", i+1 );
-        Abc_NtkForEachPi( pNtk, pNode, k )
-            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
-        printf( " " );
-        Abc_NtkForEachLatch( pNtk, pNode, k )
-            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
-        printf( " " );
-        Abc_NtkForEachPo( pNtk, pNode, k )
-            printf( "%d", Sim_SimInfoGet(vInfo,pNode)[i] > 0 );
-        printf( "\n" );
-    }
-    printf( "\n" );
-*/
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one frame of sequential circuit.]
-
-  Description [Assumes that the latches and POs are already initialized.
-  In the end transfers the data to the latches of the next frame.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_SimulateSeqFrame( Vec_Ptr_t * vInfo, Abc_Ntk_t * pNtk, int iFrames, int nWords, int fTransfer )
-{
-    Abc_Obj_t * pNode;
-    int i;
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        Sim_UtilSimulateNodeOne( pNode, vInfo, nWords, iFrames * nWords );
-    Abc_NtkForEachPo( pNtk, pNode, i )
-        Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 0 );
-    if ( !fTransfer )
-        return;
-    Abc_NtkForEachLatch( pNtk, pNode, i )
-        Sim_UtilTransferNodeOne( pNode, vInfo, nWords, iFrames * nWords, 1 );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index f7048f4a..576e19cc 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -35,8 +35,10 @@ 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 DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -66,8 +68,8 @@ Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
     // derive the structural supports of the internal nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
         pSimmNode  = vSuppStr->pArray[ pNode->Id ];
         pSimmNode1 = vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
         pSimmNode2 = vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
@@ -106,7 +108,7 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
     srand( 0xABC );
 
     // start the simulation manager
-    p = Sim_ManStart( pNtk, 0 );
+    p = Sim_ManStart( pNtk );
 
     // compute functional support using one round of random simulation
     Sim_UtilAssignRandom( p );
@@ -467,10 +469,9 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
 
         // transform the miter into a fraig
         Fraig_ParamsSetDefault( &Params );
-        Params.nSeconds = ABC_INFINITY;
         Params.fInternal = 1;
 clk = clock();
-        pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
+        pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
 p->timeFraig += clock() - clk;
 clk = clock();
         Fraig_ManProveMiter( pMan );
@@ -586,6 +587,10 @@ int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Out
     }
     // 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;
 }
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
index 218d4d59..b43597f3 100644
--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@@ -29,7 +29,7 @@ static void Sim_NodeSimulate( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW
 static float Sim_ComputeSwitching( unsigned * pSimInfo, int nSimWords );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -65,7 +65,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
-        Sim_UtilSetRandom( pSimInfo, nSimWords );
+        Sim_UtilGetRandom( pSimInfo, nSimWords );
         pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
     }
     // simulate the internal nodes
@@ -73,7 +73,7 @@ Vec_Int_t * Sim_NtkComputeSwitching( Abc_Ntk_t * pNtk, int nPatterns )
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
         pSimInfo = Vec_PtrEntry(vSimInfo, pNode->Id);
-        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 );
+        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords );
         pSwitching[pNode->Id] = Sim_ComputeSwitching( pSimInfo, nSimWords );
     }
     Vec_PtrFree( vNodes );
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index 71de5b05..c452bb1b 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
  
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -71,7 +71,7 @@ p->timeStruct = clock() - clk;
     for ( i = 1; i <= 1000; i++ )
     {
         // simulate this pattern
-        Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
+        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
         if ( i % 50 != 0 )
             continue;
@@ -125,7 +125,6 @@ p->timeStruct = clock() - clk;
     if ( fVerbose )
         printf( "Total = %8d.  Sym = %8d.  NonSym = %8d.  Remaining = %8d.\n", 
             p->nPairsTotal, p->nPairsSymm, p->nPairsNonSymm, p->nPairsRem );
-//    Sim_UtilCountPairsAllPrint( p );
 
     Result = p->nPairsSymm;
     vResult = p->vMatrSymms;  
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index 7690a891..db9917b3 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -26,10 +26,11 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
+extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
+extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -144,10 +145,9 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
     Params.fInternal = 1;
     Params.nPatsRand = 512;
     Params.nPatsDyna = 512;
-    Params.nSeconds = ABC_INFINITY;
 
 clk = clock();
-    pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
 p->timeFraig += clock() - clk;
 clk = clock();
     Fraig_ManProveMiter( pMan );
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index 2282825b..94028c47 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -29,7 +29,7 @@ static void Sim_SymmsCreateSquare( Sym_Man_t * p, unsigned * pPat );
 static void Sim_SymmsDeriveInfo( Sym_Man_t * p, unsigned * pPat, Abc_Obj_t * pNode, Vec_Ptr_t * vMatrsNonSym, int Output );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -55,9 +55,9 @@ void Sim_SymmsSimulate( Sym_Man_t * p, unsigned * pPat, Vec_Ptr_t * vMatrsNonSym
 clk = clock();
     Vec_PtrForEachEntry( p->vNodes, pNode, i )
     {
-//        if ( Abc_NodeIsConst(pNode) )
-//            continue;
-        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords );
     }
 p->timeSim += clock() - clk;
     // collect info into the CO matrices
@@ -65,8 +65,8 @@ clk = clock();
     Abc_NtkForEachCo( p->pNtk, pNode, i )
     {
         pNode = Abc_ObjFanin0(pNode);
-//        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(pNode) )
-//            continue;
+        if ( Abc_ObjIsCi(pNode) || Abc_NodeIsConst(pNode) )
+            continue;
         nPairsTotal  = Vec_IntEntry(p->vPairsTotal, i);
         nPairsSym    = Vec_IntEntry(p->vPairsSym,   i);
         nPairsNonSym = Vec_IntEntry(p->vPairsNonSym,i);
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
index d52c4328..ed7e93bf 100644
--- a/src/opt/sim/simSymStr.c
+++ b/src/opt/sim/simSymStr.c
@@ -41,7 +41,7 @@ static void  Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * v
 static int * Sim_SymmsCreateMap( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -74,16 +74,15 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v
     vNodes = Abc_NtkDfs( pNtk, 0 );
     Vec_PtrForEachEntry( vNodes, pTemp, i )
     {
-//        if ( Abc_NodeIsConst(pTemp) )
-//            continue;
+        if ( Abc_NodeIsConst(pTemp) )
+            continue;
         Sim_SymmsStructComputeOne( pNtk, pTemp, pMap );
     }
     // collect the results for the COs;
     Abc_NtkForEachCo( pNtk, pTemp, i )
     {
-//printf( "Output %d:\n", i );
         pTemp = Abc_ObjFanin0(pTemp);
-        if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
+        if ( Abc_ObjIsCi(pTemp) || Abc_NodeIsConst(pTemp) )
             continue;
         Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
     }
@@ -93,7 +92,7 @@ void Sim_SymmsStructCompute( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMatrs, Vec_Ptr_t * v
     Abc_NtkForEachCi( pNtk, pTemp, i )
         Vec_IntFree( SIM_READ_SYMMS(pTemp) );
     Vec_PtrForEachEntry( vNodes, pTemp, i )
-//        if ( !Abc_NodeIsConst(pTemp) )
+        if ( !Abc_NodeIsConst(pTemp) )
             Vec_IntFree( SIM_READ_SYMMS(pTemp) );
     Vec_PtrFree( vNodes );
     free( pMap );
@@ -445,7 +444,6 @@ void Sim_SymmsTransferToMatrix( Extra_BitMat_t * pMatSymm, Vec_Int_t * vSymms, u
         uSymm = (unsigned)vSymms->pArray[i];
         Ind1 = (uSymm & 0xffff);
         Ind2 = (uSymm >> 16);
-//printf( "%d,%d ", Ind1, Ind2 );
         // skip variables that are not in the true support
         assert( Sim_HasBit(pSupport, Ind1) == Sim_HasBit(pSupport, Ind2) );
         if ( !Sim_HasBit(pSupport, Ind1) || !Sim_HasBit(pSupport, Ind2) )
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index b0660001..4b89c650 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -37,7 +37,7 @@ static int bit_count[256] = {
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -232,6 +232,9 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT
     // simulate the internal nodes
     if ( Abc_ObjIsNode(pNode) )
     {
+        if ( Abc_NodeIsConst(pNode) )
+            return;
+
         if ( fType )
             pSimmNode  = p->vSim1->pArray[ pNode->Id ];
         else
@@ -296,18 +299,17 @@ void Sim_UtilSimulateNode( Sim_Man_t * p, Abc_Obj_t * pNode, bool fType, bool fT
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset )
+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));
-    pSimmNode  += nOffset;
-    pSimmNode1 += nOffset;
-    pSimmNode2 += nOffset;
     fComp1 = Abc_ObjFaninC0(pNode);
     fComp2 = Abc_ObjFaninC1(pNode);
     if ( fComp1 && fComp2 )
@@ -326,36 +328,6 @@ void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimW
 
 /**Function*************************************************************
 
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilTransferNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset, int fShift )
-{
-    unsigned * pSimmNode, * pSimmNode1;
-    int k, fComp1;
-    // simulate the internal nodes
-    assert( Abc_ObjIsCo(pNode) );
-    pSimmNode  = Vec_PtrEntry(vSimInfo, pNode->Id);
-    pSimmNode1 = Vec_PtrEntry(vSimInfo, Abc_ObjFaninId0(pNode));
-    pSimmNode  += nOffset + (fShift > 0)*nSimWords;
-    pSimmNode1 += nOffset;
-    fComp1 = Abc_ObjFaninC0(pNode);
-    if ( fComp1 )
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] = ~pSimmNode1[k];
-    else 
-        for ( k = 0; k < nSimWords; k++ )
-            pSimmNode[k] =  pSimmNode1[k];
-}
-
-/**Function*************************************************************
-
   Synopsis    [Returns 1 if the simulation infos are equal.]
 
   Description []
@@ -408,31 +380,10 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
     return nOnes;    
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1's in the bitstring.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords )
-{
-    Vec_Int_t * vCounters;
-    unsigned * pSimInfo;
-    int i;
-    vCounters = Vec_IntStart( Vec_PtrSize(vInfo) );
-    Vec_PtrForEachEntry( vInfo, pSimInfo, i )
-        Vec_IntWriteEntry( vCounters, i, Sim_UtilCountOnes(pSimInfo, nSimWords) );
-    return vCounters;
-}
 
 /**Function*************************************************************
 
-  Synopsis    [Returns random patterns.]
+  Synopsis    [Returns the random pattern.]
 
   Description []
                
@@ -441,7 +392,7 @@ Vec_Int_t * Sim_UtilCountOnesArray( Vec_Ptr_t * vInfo, int nSimWords )
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
+void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords )
 {
     int k;
     for ( k = 0; k < nSimWords; k++ )
@@ -450,104 +401,6 @@ void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns complemented patterns.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSetCompl( unsigned * pPatRand, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        pPatRand[k] = ~pPatRand[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns constant patterns.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilSetConst( unsigned * pPatRand, int nSimWords, int fConst1 )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        pPatRand[k] = 0;
-    if ( fConst1 )
-        Sim_UtilSetCompl( pPatRand, nSimWords );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilInfoIsEqual( unsigned * pPats1, unsigned * pPats2, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        if ( pPats1[k] != pPats2[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if Node1 implies Node2.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilInfoIsImp( unsigned * pPats1, unsigned * pPats2, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        if ( pPats1[k] & ~pPats2[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if Node1 v Node2 is always true.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sim_UtilInfoIsClause( unsigned * pPats1, unsigned * pPats2, int nSimWords )
-{
-    int k;
-    for ( k = 0; k < nSimWords; k++ )
-        if ( ~pPats1[k] & ~pPats2[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Counts the total number of pairs.]
 
   Description []
@@ -607,51 +460,6 @@ int Sim_UtilCountPairsOne( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
   SeeAlso     []
 
 ***********************************************************************/
-int Sim_UtilCountPairsOnePrint( Extra_BitMat_t * pMat, Vec_Int_t * vSupport )
-{
-    int i, k, Index1, Index2;
-    Vec_IntForEachEntry( vSupport, i, Index1 )
-    Vec_IntForEachEntryStart( vSupport, k, Index2, Index1+1 )
-        if ( Extra_BitMatrixLookup1( pMat, i, k ) )
-            printf( "(%d,%d) ", i, k );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of entries in the array of matrices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sim_UtilCountPairsAllPrint( Sym_Man_t * p )
-{
-    int i, clk;
-clk = clock();
-    for ( i = 0; i < p->nOutputs; i++ )
-    {
-        printf( "Output %2d :", i );
-        Sim_UtilCountPairsOnePrint( Vec_PtrEntry(p->vMatrSymms, i), Vec_VecEntry(p->vSupports, i) );
-        printf( "\n" );
-    }
-p->timeCount += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of entries in the array of matrices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Sim_UtilCountPairsAll( Sym_Man_t * p )
 {
     int nPairsTotal, nPairsSym, nPairsNonSym, i, clk;