Version abc80130_2

12 files changed, 454 insertions, 71 deletions

diff --git a/src/opt/sim/module.make b/src/opt/sim/module.make
index 43d0a125..54058402 100644
--- a/src/opt/sim/module.make
+++ b/src/opt/sim/module.make
@@ -1,5 +1,6 @@
 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 afed7190..7fcf5ae6 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -17,10 +17,14 @@
   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, 
@@ -98,6 +102,7 @@ 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
@@ -135,11 +140,11 @@ struct Sim_Pat_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFITIONS                             ///
+///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#define SIM_NUM_WORDS(n)      ((n)/32 + (((n)%32) > 0))
-#define SIM_LAST_BITS(n)      ((((n)%32) > 0)? (n)%32 : 32)
+#define SIM_NUM_WORDS(n)      (((n)>>5) + (((n)&31) > 0))
+#define SIM_LAST_BITS(n)      ((((n)&31) > 0)? (n)&31 : 32)
 
 #define SIM_MASK_FULL         (0xFFFFFFFF)
 #define SIM_MASK_BEG(n)       (SIM_MASK_FULL >> (32-n))
@@ -162,6 +167,7 @@ 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                         ///
@@ -171,11 +177,14 @@ 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 );
+extern Sim_Man_t *     Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight );
 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 );
@@ -197,17 +206,28 @@ 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 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 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 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 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 780ecfd8..3b50ad84 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -26,12 +26,12 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the simulatin manager.]
+  Synopsis    [Starts the simulation manager.]
 
   Description []
                
@@ -83,7 +83,7 @@ Sym_Man_t * Sym_ManStart( Abc_Ntk_t * pNtk, int fVerbose )
 
 /**Function*************************************************************
 
-  Synopsis    [Stops the simulatin manager.]
+  Synopsis    [Stops the simulation manager.]
 
   Description []
                
@@ -149,11 +149,9 @@ void Sym_ManPrintStats( Sym_Man_t * p )
 }
 
 
-
-
 /**Function*************************************************************
 
-  Synopsis    [Starts the simulatin manager.]
+  Synopsis    [Starts the simulation manager.]
 
   Description []
                
@@ -162,7 +160,7 @@ void Sym_ManPrintStats( Sym_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
+Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk, int fLightweight )
 {
     Sim_Man_t * p;
     // start the manager
@@ -175,24 +173,27 @@ Sim_Man_t * Sim_ManStart( Abc_Ntk_t * pNtk )
     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 );
+    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 );
+    }
     return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Stops the simulatin manager.]
+  Synopsis    [Stops the simulation manager.]
 
   Description []
                
@@ -209,7 +210,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, 0 );
+    if ( p->pMmPat )       Extra_MmFixedStop( p->pMmPat );
     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 b4e080fe..d514f7f2 100644
--- a/src/opt/sim/simSat.c
+++ b/src/opt/sim/simSat.c
@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
  
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c
new file mode 100644
index 00000000..49fb939f
--- /dev/null
+++ b/src/opt/sim/simSeq.c
@@ -0,0 +1,171 @@
+/**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 576e19cc..f7048f4a 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -35,10 +35,8 @@ 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 DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -68,8 +66,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) ];
@@ -108,7 +106,7 @@ Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
     srand( 0xABC );
 
     // start the simulation manager
-    p = Sim_ManStart( pNtk );
+    p = Sim_ManStart( pNtk, 0 );
 
     // compute functional support using one round of random simulation
     Sim_UtilAssignRandom( p );
@@ -469,9 +467,10 @@ 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 ); 
+        pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
 p->timeFraig += clock() - clk;
 clk = clock();
         Fraig_ManProveMiter( pMan );
@@ -587,10 +586,6 @@ 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 b43597f3..218d4d59 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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_UtilGetRandom( pSimInfo, nSimWords );
+        Sim_UtilSetRandom( 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 );
+        Sim_UtilSimulateNodeOne( pNode, vSimInfo, nSimWords, 0 );
         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 c452bb1b..71de5b05 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -26,7 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
  
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -71,7 +71,7 @@ p->timeStruct = clock() - clk;
     for ( i = 1; i <= 1000; i++ )
     {
         // simulate this pattern
-        Sim_UtilGetRandom( p->uPatRand, p->nSimWords );
+        Sim_UtilSetRandom( p->uPatRand, p->nSimWords );
         Sim_SymmsSimulate( p, p->uPatRand, p->vMatrNonSymms );
         if ( i % 50 != 0 )
             continue;
@@ -125,6 +125,7 @@ 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 db9917b3..7690a891 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -26,11 +26,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-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 );
+static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -145,9 +144,10 @@ 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 ); 
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0, 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 94028c47..2282825b 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**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 );
+//        if ( Abc_NodeIsConst(pNode) )
+//            continue;
+        Sim_UtilSimulateNodeOne( pNode, p->vSim, p->nSimWords, 0 );
     }
 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_NodeIsConst(pNode) )
-            continue;
+//        if ( Abc_ObjIsCi(pNode) || Abc_AigNodeIsConst(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 ed7e93bf..d52c4328 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 DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -74,15 +74,16 @@ 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_NodeIsConst(pTemp) )
+        if ( Abc_ObjIsCi(pTemp) || Abc_AigNodeIsConst(pTemp) )
             continue;
         Sim_SymmsTransferToMatrix( Vec_PtrEntry(vMatrs, i), SIM_READ_SYMMS(pTemp), Vec_PtrEntry(vSuppFun, i) );
     }
@@ -92,7 +93,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 );
@@ -444,6 +445,7 @@ 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 4b89c650..b0660001 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -37,7 +37,7 @@ static int bit_count[256] = {
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -232,9 +232,6 @@ 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
@@ -299,17 +296,18 @@ 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 )
+void Sim_UtilSimulateNodeOne( Abc_Obj_t * pNode, Vec_Ptr_t * vSimInfo, int nSimWords, int nOffset )
 {
     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 )
@@ -328,6 +326,36 @@ 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 []
@@ -380,10 +408,31 @@ 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 the random pattern.]
+  Synopsis    [Returns random patterns.]
 
   Description []
                
@@ -392,7 +441,7 @@ int Sim_UtilCountOnes( unsigned * pSimInfo, int nSimWords )
   SeeAlso     []
 
 ***********************************************************************/
-void Sim_UtilGetRandom( unsigned * pPatRand, int nSimWords )
+void Sim_UtilSetRandom( unsigned * pPatRand, int nSimWords )
 {
     int k;
     for ( k = 0; k < nSimWords; k++ )
@@ -401,6 +450,104 @@ void Sim_UtilGetRandom( 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 []
@@ -460,6 +607,51 @@ 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;