Version abc80910

9 files changed, 393 insertions, 95 deletions

diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 2619751e..b176d4db 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -3,6 +3,7 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswCnf.c \
     src/aig/ssw/sswCore.c \
     src/aig/ssw/sswMan.c \
+    src/aig/ssw/sswPart.c \
     src/aig/ssw/sswSat.c \
     src/aig/ssw/sswSim.c \
     src/aig/ssw/sswSimSat.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index aaaa6407..f76664ec 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -44,11 +44,14 @@ struct Ssw_Pars_t_
     int              nPartSize;     // size of the partition
     int              nOverSize;     // size of the overlap between partitions
     int              nFramesK;      // the induction depth
+    int              nFramesAddSim; // the number of additional frames to simulate
     int              nConstrs;      // treat the last nConstrs POs as seq constraints
     int              nMaxLevs;      // the max number of levels of nodes to consider
     int              nBTLimit;      // conflict limit at a node
+    int              nMinDomSize;   // min clock domain considered for optimization
     int              fPolarFlip;    // uses polarity adjustment
     int              fLatchCorr;    // perform register correspondence
+    int              fSkipCheck;    // does not run equivalence check for unaffected cones
     int              fVerbose;      // verbose stats
     // internal parameters
     int              nIters;        // the number of iterations performed
@@ -77,6 +80,8 @@ struct Ssw_Cex_t_
 /*=== sswCore.c ==========================================================*/
 extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
 extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
+/*=== sswPart.c ==========================================================*/
+extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 66b86009..d06cce49 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -46,6 +46,7 @@ struct Ssw_Cla_t_
     // temporary data
     Vec_Ptr_t *      vClassOld;        // old equivalence class after splitting
     Vec_Ptr_t *      vClassNew;        // new equivalence class(es) after splitting
+    Vec_Ptr_t *      vRefined;         // the nodes refined since the last iteration
     // procedures used for class refinement
     void *           pManData;
     unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns hash key of the node
@@ -141,6 +142,7 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
     p->pClassSizes  = CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->vClassOld    = Vec_PtrAlloc( 100 );
     p->vClassNew    = Vec_PtrAlloc( 100 );
+    p->vRefined     = Vec_PtrAlloc( 1000 );
     assert( pAig->pReprs == NULL );
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
     return p;
@@ -183,6 +185,7 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
 {
     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
+    Vec_PtrFree( p->vRefined );
     FREE( p->pId2Class );
     FREE( p->pClassSizes );
     FREE( p->pMemClasses );
@@ -191,6 +194,38 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
+{
+    return p->vRefined;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
+{
+    Vec_PtrClear( p->vRefined );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stop representation of equivalence classes.]
 
   Description []
@@ -368,12 +403,14 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
     assert( p->pId2Class[pObj->Id] == NULL );
     pRepr = Aig_ObjRepr( p->pAig, pObj );
     assert( pRepr != NULL );
+    Vec_PtrPush( p->vRefined, pObj );
     if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
     {
         Aig_ObjSetRepr( p->pAig, pObj, NULL );
         p->nCands1--;
         return;
     }
+    Vec_PtrPush( p->vRefined, pRepr );
     Aig_ObjSetRepr( p->pAig, pObj, NULL );
     assert( p->pId2Class[pRepr->Id][0] == pRepr );
     assert( p->pClassSizes[pRepr->Id] >= 2 );
@@ -409,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
 {
     Ssw_Cla_t * p;
     Ssw_Sml_t * pSml;
@@ -424,7 +461,10 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
     // perform sequential simulation
 clk = clock();
     pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 4 );
+if ( fVerbose )
+{
 PRT( "Simulation of 32 frames with 4 words", clock() - clk );
+}
 
     // set comparison procedures
 clk = clock();
@@ -441,7 +481,7 @@ clk = clock();
     {
         if ( fLatchCorr )
         {
-            if ( !Saig_ObjIsPi(p->pAig, pObj) )
+            if ( !Saig_ObjIsLo(p->pAig, pObj) )
                 continue;
         }
         else
@@ -521,7 +561,10 @@ clk = clock();
     Ssw_ClassesCheck( p );
     Ssw_SmlStop( pSml );
 //    Ssw_ClassesPrint( p, 0 );
+if ( fVerbose )
+{
 PRT( "Collecting candidate equival classes", clock() - clk );
+}
     return p;
 }
 
@@ -597,8 +640,6 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
     }
     // allocate room for classes
     p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
-    // set comparison procedures
-    Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
 //    Ssw_ClassesPrint( p, 0 );
     return p;
 }
@@ -631,6 +672,9 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
     // check if splitting happened
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
+    // remember that this class is refined
+    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
+        Vec_PtrPush( p->vRefined, pObj );
 
     // get the new representative
     pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
@@ -751,7 +795,10 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
         {
             pObj = Aig_ManObj( p->pAig, i );
             if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
+            {
                 Vec_PtrPush( p->vClassNew, pObj );
+                Vec_PtrPush( p->vRefined, pObj );
+            }
         }
     // check if there is a new class
     if ( Vec_PtrSize(p->vClassNew) == 0 )
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 409a1ebe..e6096c54 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -45,8 +45,10 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nPartSize      =     0;  // size of the partition
     p->nOverSize      =     0;  // size of the overlap between partitions
     p->nFramesK       =     1;  // the induction depth
+    p->nFramesAddSim  =     2;  // additional frames to simulate
     p->nConstrs       =     0;  // treat the last nConstrs POs as seq constraints
     p->nBTLimit       =  1000;  // conflict limit at a node
+    p->nMinDomSize    =   100;  // min clock domain considered for optimization
     p->fPolarFlip     =     0;  // uses polarity adjustment
     p->fLatchCorr     =     0;  // performs register correspondence
     p->fVerbose       =     0;  // verbose stats
@@ -71,21 +73,44 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     int RetValue, nIter, clk, clkTotal = clock();
     // reset random numbers
     Aig_ManRandom( 1 );
+
+    // consider the case of empty AIG
+    if ( Aig_ManNodeNum(pAig) == 0 )
+    {
+        pPars->nIters = 0;
+        // Ntl_ManFinalize() needs the following to satisfy an assertion
+        Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
+        return Aig_ManDupOrdered(pAig);
+    }
+
+    // check and update parameters
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( pPars->nFramesK > 0 );
+    if ( pPars->nFramesK > 1 )
+        pPars->fSkipCheck = 0;
+
+    // perform partitioning
+    if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
+         || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
+        return Ssw_SignalCorrespondencePart( pAig, pPars );
+
     // start the choicing manager
     p = Ssw_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
+//    p->pPars->nConstrs = 1;
     if ( p->pPars->nConstrs == 0 )
     {
-        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
-        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 );
+        // perform one round of seq simulation and generate candidate equivalence classes
+        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
         Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
     }
     else
     {
-        assert( 0 );
+        // create trivial equivalence classes with all nodes being candidates for constant 1
         p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
+        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
     }
-//    Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
 
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
@@ -111,9 +136,11 @@ clk = clock();
         RetValue = Ssw_ManSweep( p );
         if ( pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Cl = %6d.  L = %6d. LR = %6d.  NR = %6d. ", 
+            printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
                 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
-                p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
+                p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+            printf( "Use = %5d. Skip = %5d. ", 
+                p->nRefUse, p->nRefSkip );
             PRT( "T", clock() - clk );
         } 
         Ssw_ManCleanup( p );
@@ -133,6 +160,8 @@ p->timeTotal = clock() - clkTotal;
     return pAigNew;
 }
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 009c09c4..c9dd1958 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -57,6 +57,8 @@ struct Ssw_Man_t_
     // equivalence classes
     Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
     int              fRefined;       // is set to 1 when refinement happens
+    int              nRefUse;
+    int              nRefSkip;  
     // SAT solving
     sat_solver *     pSat;           // recyclable SAT solver
     int              nSatVars;       // the counter of SAT variables
@@ -77,8 +79,8 @@ struct Ssw_Man_t_
     // SAT calls statistics
     int              nSatCalls;      // the number of SAT calls
     int              nSatProof;      // the number of proofs
-    int              nSatFails;      // the number of timeouts
     int              nSatFailsReal;  // the number of timeouts
+    int              nSatFailsTotal; // the number of timeouts
     int              nSatCallsUnsat; // the number of unsat SAT calls
     int              nSatCallsSat;   // the number of sat SAT calls
     // node/register/lit statistics
@@ -91,6 +93,7 @@ struct Ssw_Man_t_
     // runtime stats
     int              timeBmc;        // bounded model checking
     int              timeReduce;     // speculative reduction
+    int              timeMarkCones;  // marking the cones not to be refined
     int              timeSimSat;     // simulation of the counter-examples
     int              timeSat;        // solving SAT
     int              timeSatSat;     // sat
@@ -136,6 +139,8 @@ extern void          Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
                          int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
                          int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
 extern void          Ssw_ClassesStop( Ssw_Cla_t * p );
+extern Vec_Ptr_t *   Ssw_ClassesGetRefined( Ssw_Cla_t * p );
+extern void          Ssw_ClassesClearRefined( Ssw_Cla_t * p );
 extern int           Ssw_ClassesCand1Num( Ssw_Cla_t * p );
 extern int           Ssw_ClassesClassNum( Ssw_Cla_t * p );
 extern int           Ssw_ClassesLitNum( Ssw_Cla_t * p );
@@ -143,7 +148,7 @@ extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int
 extern void          Ssw_ClassesCheck( Ssw_Cla_t * p );
 extern void          Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
 extern void          Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
-extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
 extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
@@ -171,6 +176,7 @@ extern int           Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig
 extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
 extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
 /*=== sswSimSat.c ===================================================*/
+extern int           Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
 extern void          Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
 extern void          Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
 extern void          Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index a6e02125..f25cee45 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -99,27 +99,28 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
 
-    printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d. Max lev = %d. Mem = %0.2f Mb.\n", 
-        p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
+    printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
+        p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
     printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.  Ave SAT vars = %d.\n", 
         Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), 
         p->nSatVarsTotal/p->pPars->nIters );
-    printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. FailReal = %d.  Equivs = %d. Str = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStrangers );
+    printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
 
-    p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
-    PRTP( "BMC        ", p->timeBmc,      p->timeTotal );
-    PRTP( "Spec reduce", p->timeReduce,   p->timeTotal );
-    PRTP( "Sim SAT    ", p->timeSimSat,   p->timeTotal );
-    PRTP( "SAT solving", p->timeSat,      p->timeTotal );
-    PRTP( "  unsat    ", p->timeSatUnsat, p->timeTotal );
-    PRTP( "  sat      ", p->timeSatSat,   p->timeTotal );
-    PRTP( "  undecided", p->timeSatUndec, p->timeTotal );
-    PRTP( "Other      ", p->timeOther,    p->timeTotal );
-    PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+    p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
+    PRTP( "BMC        ", p->timeBmc,       p->timeTotal );
+    PRTP( "Spec reduce", p->timeReduce,    p->timeTotal );
+    PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
+    PRTP( "Sim SAT    ", p->timeSimSat,    p->timeTotal );
+    PRTP( "SAT solving", p->timeSat,       p->timeTotal );
+    PRTP( "  unsat    ", p->timeSatUnsat,  p->timeTotal );
+    PRTP( "  sat      ", p->timeSatSat,    p->timeTotal );
+    PRTP( "  undecided", p->timeSatUndec,  p->timeTotal );
+    PRTP( "Other      ", p->timeOther,     p->timeTotal );
+    PRTP( "TOTAL      ", p->timeTotal,     p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -167,6 +168,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
 ***********************************************************************/
 void Ssw_ManStop( Ssw_Man_t * p )
 {
+    Aig_ManCleanMarkA( p->pAig );
     if ( p->pPars->fVerbose )
         Ssw_ManPrintStats( p );
     if ( p->ppClasses )
diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c
new file mode 100644
index 00000000..7eb6b8fe
--- /dev/null
+++ b/src/aig/ssw/sswPart.c
@@ -0,0 +1,129 @@
+/**CFile****************************************************************
+
+  FileName    [sswPart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Partitioned signal correspondence.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioned sequential SAT sweepingG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    int fPrintParts = 0;
+    char Buffer[100];
+    Aig_Man_t * pTemp, * pNew;
+    Vec_Ptr_t * vResult;
+    Vec_Int_t * vPart;
+    int * pMapBack;
+    int i, nCountPis, nCountRegs;
+    int nClasses, nPartSize, fVerbose;
+    int clk = clock();
+
+    // save parameters
+    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+    fVerbose  = pPars->fVerbose;  pPars->fVerbose = 0;
+    // generate partitions
+    if ( pAig->vClockDoms )
+    {
+        // divide large clock domains into separate partitions
+        vResult = Vec_PtrAlloc( 100 );
+        Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
+        {
+            if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
+                Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+            else
+                Vec_PtrPush( vResult, Vec_IntDup(vPart) );
+        }
+    }
+    else
+        vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
+//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+    if ( fPrintParts )
+    {
+        // print partitions
+        printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+        Vec_PtrForEachEntry( vResult, vPart, i )
+        {
+            extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+            sprintf( Buffer, "part%03d.aig", i );
+            pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
+            Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+            printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+            Aig_ManStop( pTemp );
+        }
+    }
+
+    // perform SSW with partitions
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Vec_PtrForEachEntry( vResult, vPart, i )
+    {
+        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        Aig_ManSetRegNum( pTemp, pTemp->nRegs );
+        // create the projection of 1-hot registers
+        if ( pAig->vOnehots )
+            pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
+        // run SSW
+        pNew = Ssw_SignalCorrespondence( pTemp, pPars );
+        nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+        if ( fVerbose )
+            printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+        Aig_ManStop( pNew );
+        Aig_ManStop( pTemp );
+        free( pMapBack );
+    }
+    // remap the AIG
+    pNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pNew );
+//    Aig_ManPrintStats( pAig );
+//    Aig_ManPrintStats( pNew );
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+    pPars->nPartSize = nPartSize;
+    pPars->fVerbose = fVerbose;
+    if ( fVerbose )
+    {
+        PRT( "Total time", clock() - clk );
+    }
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 547755f0..6ef5ec20 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -234,7 +234,8 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
     Aig_ManForEachPi( p->pAig, pObj, i )
-        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+//        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+        pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
     // simulate internal nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
         pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
@@ -253,27 +254,6 @@ p->timeSimSat += clock() - clk;
 
 /**Function*************************************************************
 
-  Synopsis    [Copy pattern from the solver into the internal storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
-            Aig_InfoSetBit( p->pPatWords, i );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Handle the counter-example.]
 
   Description []
@@ -287,7 +267,7 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
 {
     int RetValue1, RetValue2, clk = clock();
     // save the counter-example
-    Ssw_SmlSavePatternAig( p, f );
+//    Ssw_SmlSavePatternAig( p, f );
     // set the PI simulation information
     Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     // simulate internal nodes
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 7c99fad2..5ad6d78e 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -31,6 +31,95 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Mark nodes affected by sweep in the previous iteration.]
+
+  Description [Assumes that affected nodes are in p->ppClasses->vRefined.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
+{
+    Vec_Ptr_t * vRefined, * vSupp;
+    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
+    int i, k;
+    vRefined = Ssw_ClassesGetRefined( p->ppClasses );
+    if ( Vec_PtrSize(vRefined) == 0 )
+    {
+        Aig_ManForEachObj( p->pAig, pObj, i )
+            pObj->fMarkA = 1;
+        return;
+    }
+    // mark the nodes to be refined
+    Aig_ManCleanMarkA( p->pAig );
+    Vec_PtrForEachEntry( vRefined, pObj, i )
+    {
+        if ( Aig_ObjIsPi(pObj) )
+        {
+            pObj->fMarkA = 1;
+            continue;
+        }
+        assert( Aig_ObjIsNode(pObj) );
+        vSupp = Aig_Support( p->pAig, pObj );
+        Vec_PtrForEachEntry( vSupp, pObjLo, k )
+            pObjLo->fMarkA = 1;
+        Vec_PtrFree( vSupp );
+    }
+    // mark refinement
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
+    Saig_ManForEachLi( p->pAig, pObj, i )
+        pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA;
+    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        pObjLo->fMarkA |= pObjLi->fMarkA;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        if ( Ssw_ManOriginalPiValue( p, pObj, f ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -40,7 +129,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
@@ -50,59 +139,58 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
         return;
     // get the fraiged node
     pObjFraig = Ssw_ObjFraig( p, pObj, f );
-    assert( pObjFraig != NULL );
     // get the fraiged representative
     pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
-    assert( pObjReprFraig != NULL );
     // check if constant 0 pattern distinquishes these nodes
+    assert( pObjFraig != NULL && pObjReprFraig != NULL );
     if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
     {
-        Aig_Obj_t * pObj;
-        int i;
-        if ( p->pSat->model.cap < p->pSat->size )
-        {
-            veci_resize(&p->pSat->model, 0);
-            for ( i = 0; i < p->pSat->size; i++ ) 
-                veci_push( &p->pSat->model, (int)l_False );
-        }
-        // set the values of SAT vars to be equal to the phase of the nodes
-        Aig_ManForEachObj( p->pFrames, pObj, i )
-            if ( Ssw_ObjSatNum( p, pObj ) )
-            {
-                int iVar = Ssw_ObjSatNum( p, pObj );
-                assert( iVar < p->pSat->size );
-                p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False));
-                p->pSat->model.size = p->pSat->size;
-            }
         p->nStrangers++;
-        return;
+        Ssw_SmlSavePatternAigPhase( p, f );
     }
-    // if the fraiged nodes are the same, return
-    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-        return;
-//    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
-    if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
-        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
     else
-        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
-
-    if ( RetValue == -1 ) // timed out
-    {
-//        assert( 0 );
-        Ssw_ClassesRemoveNode( p->ppClasses, pObj );
-        p->fRefined = 1;
-        return;
-    }
-    if ( RetValue == 1 )  // proved equivalent
     {
-        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-        Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
-        return;
+        // if the fraiged nodes are the same, return
+        if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+            return;
+        // count the number of skipped calls
+        if ( !pObj->fMarkA && !pObjRepr->fMarkA )
+            p->nRefSkip++;
+        else
+            p->nRefUse++;
+        // call equivalence checking
+        if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
+            RetValue = 1;
+        else if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
+            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+        else
+            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
+        if ( RetValue == 1 )  // proved equivalent
+        {
+            pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+            Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
+            return;
+        }
+        if ( RetValue == -1 ) // timed out
+        {
+            Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+            p->fRefined = 1;
+            return;
+        }
+        // check if skipping calls works correctly
+        if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
+        {
+            assert( 0 );
+            printf( "\nMistake!!!\n" );
+        }
+        // disproved the equivalence
+        Ssw_SmlSavePatternAig( p, f );
     }
-    // disproved the equivalence
 //    Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
-//    Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
-    Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+    if ( p->pPars->nConstrs == 0 )
+        Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+    else
+        Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
     assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
     p->fRefined = 1;
 }
@@ -147,7 +235,7 @@ clk = clock();
                 Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFraig( p, pObj, f, pObjNew );
-            Ssw_ManSweepNode( p, pObj, f );
+            Ssw_ManSweepNode( p, pObj, f, 1 );
         }
         // quit if this is the last timeframe
         if ( f == p->pPars->nFramesK - 1 )
@@ -205,6 +293,12 @@ clk = clock();
     sat_solver_simplify( p->pSat );
 p->timeReduce += clock() - clk;
 
+    // mark nodes that do not have to be refined
+clk = clock();
+    if ( p->pPars->fSkipCheck )
+        Ssw_ManSweepMarkRefinement( p );
+p->timeMarkCones += clock() - clk;
+
     // map constants and PIs of the last frame
     f = p->pPars->nFramesK;
     Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
@@ -215,6 +309,9 @@ p->timeReduce += clock() - clk;
         assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
     // sweep internal nodes
     p->fRefined = 0;
+    p->nSatFailsReal = 0;
+    p->nRefUse = p->nRefSkip = 0;
+    Ssw_ClassesClearRefined( p->ppClasses );
     if ( p->pPars->fVerbose )
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
@@ -222,14 +319,16 @@ p->timeReduce += clock() - clk;
         if ( p->pPars->fVerbose )
             Bar_ProgressUpdate( pProgress, i, NULL );
         if ( Saig_ObjIsLo(p->pAig, pObj) )
-            Ssw_ManSweepNode( p, pObj, f );
+            Ssw_ManSweepNode( p, pObj, f, 0 );
         else if ( Aig_ObjIsNode(pObj) )
         { 
+            pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFraig( p, pObj, f, pObjNew );
-            Ssw_ManSweepNode( p, pObj, f );
+            Ssw_ManSweepNode( p, pObj, f, 0 );
         }
     }
+    p->nSatFailsTotal += p->nSatFailsReal;
     if ( p->pPars->fVerbose )
         Bar_ProgressStop( pProgress );