Version abc80922

14 files changed, 512 insertions, 28 deletions

diff --git a/abc.dsp b/abc.dsp
index 6ec33bcd..936445cf 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3438,6 +3438,10 @@ SOURCE=.\src\aig\ssw\sswAig.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ssw\sswBmc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ssw\sswClass.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index c5668d6d..6b748598 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/aig/ssw/sswAig.c \
+    src/aig/ssw/sswBmc.c \
     src/aig/ssw/sswClass.c \
     src/aig/ssw/sswCnf.c \
     src/aig/ssw/sswCore.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 8d74f16b..98e8c9d7 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -52,11 +52,12 @@ struct Ssw_Pars_t_
     int              fPolarFlip;    // uses polarity adjustment
     int              fSkipCheck;    // do not run equivalence check for unaffected cones
     int              fLatchCorr;    // perform register correspondence
+    int              fSemiFormal;   // enable semiformal filtering
+    int              fVerbose;      // verbose stats
     // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
     int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
     int              nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
-    int              fVerbose;      // verbose stats
     // internal parameters
     int              nIters;        // the number of iterations performed
 };
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 5a47ba5f..0d0fdbee 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -39,9 +39,9 @@
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame )
+static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame, int fTwoPos )
 {
-    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
     // skip nodes without representative
     pObjRepr = Aig_ObjRepr(pAig, pObj);
     if ( pObjRepr == NULL )
@@ -71,8 +71,16 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // set the new node
     Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
     // add the constraint
-    Aig_ObjCreatePo( pFrames, pObjNew2 );
-    Aig_ObjCreatePo( pFrames, pObjNew );
+    if ( fTwoPos )
+    {
+        Aig_ObjCreatePo( pFrames, pObjNew2 );
+        Aig_ObjCreatePo( pFrames, pObjNew );
+    }
+    else
+    {
+        pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
+        Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
+    }
 }
 
 /**Function*************************************************************
@@ -94,6 +102,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     assert( p->pFrames == NULL );
     assert( Aig_ManRegNum(p->pAig) > 0 );
     assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    p->nConstrTotal = p->nConstrReduced = 0;
 
     // start the fraig package
     pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
@@ -101,22 +110,21 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     Saig_ManForEachLo( p->pAig, pObj, i )
         Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
     // add timeframes
-    p->nConstrTotal = p->nConstrReduced = 0;
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+        Saig_ManForEachPi( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
         // set the constraints on the latch outputs
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
+        Saig_ManForEachLo( p->pAig, pObj, i )
+            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
         // add internal nodes of this frame
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
             pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
-            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
+            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
         }
         // transfer latch input to the latch outputs 
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -134,6 +142,59 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     return pFrames;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( p->pFrames == NULL );
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    p->nConstrTotal = p->nConstrReduced = 0;
+
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
+    // map constants and PIs
+    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+    // create latches for the first frame
+    Saig_ManForEachLo( p->pAig, pObj, i )
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+    // set the constraints on the latch outputs
+    Saig_ManForEachLo( p->pAig, pObj, i )
+        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
+        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
+        Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
+    }
+    // add the POs for the latch outputs of the last frame
+    Saig_ManForEachLi( p->pAig, pObj, i )
+        Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
+    // remove dangling nodes
+    Aig_ManCleanup( pFrames );
+    Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
+    printf( "SpecRed: Total constraints = %d. Reduced constraints = %d.\n", 
+        p->nConstrTotal, p->nConstrReduced );
+    return pFrames;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswBmc.c b/src/aig/ssw/sswBmc.c
new file mode 100644
index 00000000..e2d47440
--- /dev/null
+++ b/src/aig/ssw/sswBmc.c
@@ -0,0 +1,315 @@
+/**CFile****************************************************************
+
+  FileName    [sswBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Bounded model checker for equivalence clases.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswBmc.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ssw_Bmc_t_ Ssw_Bmc_t; // BMC manager
+
+struct Ssw_Bmc_t_
+{
+    // parameters
+    int              nConfMaxStart;  // the starting conflict limit
+    int              nConfMax;       // the intermediate conflict limit
+    int              nFramesSweep;   // the number of frames to sweep
+    int              fVerbose;       // prints output statistics
+    // equivalences considered
+    Ssw_Man_t *      pMan;           // SAT sweeping manager
+    Vec_Ptr_t *      vTargets;       // the nodes that are watched
+    // storage for patterns
+    int              nPatternsAlloc; // the max number of interesting states
+    int              nPatterns;      // the number of patterns
+    Vec_Ptr_t *      vPatterns;      // storage for the interesting states
+    Vec_Int_t *      vHistory;       // what state and how many steps
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Bmc_t * Ssw_BmcManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
+{
+    Ssw_Bmc_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    // create interpolation manager
+    p = ALLOC( Ssw_Bmc_t, 1 ); 
+    memset( p, 0, sizeof(Ssw_Bmc_t) );
+    p->nConfMaxStart  = nConfMax;
+    p->nConfMax       = nConfMax;
+    p->nFramesSweep   = AIG_MAX( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
+    p->fVerbose       = fVerbose;
+    // equivalences considered
+    p->pMan           = pMan;
+    p->vTargets       = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
+    Saig_ManForEachPo( p->pMan->pAig, pObj, i )
+        Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
+    // storage for patterns
+    p->nPatternsAlloc = 512;
+    p->nPatterns      = 1;
+    p->vPatterns      = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Aig_BitWordNum(p->nPatternsAlloc) );
+    Vec_PtrCleanSimInfo( p->vPatterns, 0, Aig_BitWordNum(p->nPatternsAlloc) );
+    p->vHistory       = Vec_IntAlloc( 100 );
+    Vec_IntPush( p->vHistory, 0 );
+    // update arrays of the manager
+    free( p->pMan->pNodeToFrames );
+    Vec_IntFree( p->pMan->vSatVars );
+    p->pMan->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
+    p->pMan->vSatVars      = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_BmcManStop( Ssw_Bmc_t * p )
+{
+    Vec_PtrFree( p->vTargets );
+    Vec_PtrFree( p->vPatterns );
+    Vec_IntFree( p->vHistory );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_BmcCheckTargets( Ssw_Bmc_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( p->vTargets, pObj, i )
+        if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManFilterBmcSavePattern( Ssw_Bmc_t * p )
+{
+    unsigned * pInfo;
+    Aig_Obj_t * pObj;
+    int i;
+    if ( p->nPatterns >= p->nPatternsAlloc )
+        return;
+    Saig_ManForEachLo( p->pMan->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( p->vPatterns, i );
+        if ( Aig_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
+            Aig_InfoSetBit( pInfo, p->nPatterns );
+    }
+    p->nPatterns++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManFilterBmc( Ssw_Bmc_t * pBmc, int iPat, int fCheckTargets )
+{
+    Ssw_Man_t * p = pBmc->pMan;
+    Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
+    unsigned * pInfo;
+    int i, f, clk, RetValue, fFirst = 0;
+clk = clock();
+
+    // start initialized timeframes
+    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        pInfo = Vec_PtrEntry( pBmc->vPatterns, i );
+        pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Aig_InfoHasBit(pInfo, iPat) );
+        Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
+    }
+
+    // sweep internal nodes
+    Ssw_ManStartSolver( p );
+    RetValue = pBmc->nFramesSweep;
+    for ( f = 0; f < pBmc->nFramesSweep; f++ )
+    {
+        // map constants and PIs
+        Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+        Saig_ManForEachPi( p->pAig, pObj, i )
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+        // sweep internal nodes
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+            if ( Ssw_ManSweepNode( p, pObj, f, 1 ) )
+            {
+                Ssw_ManFilterBmcSavePattern( pBmc );
+                if ( fFirst == 0 )
+                {
+                    fFirst = 1;
+                    pBmc->nConfMax *= 10;
+                } 
+            }
+            if ( f > 0 && p->pSat->stats.conflicts >= pBmc->nConfMax )
+            {
+                RetValue = -1;
+                break;
+            }
+        }
+        // quit if this is the last timeframe
+        if ( p->pSat->stats.conflicts >= pBmc->nConfMax )
+        {
+            RetValue += f + 1;
+            break;
+        }
+        if ( fCheckTargets && Ssw_BmcCheckTargets( pBmc ) )
+            break;
+        // transfer latch input to the latch outputs 
+        // build logic cones for register outputs
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        {
+            pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
+            Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
+            Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
+        }
+//printf( "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
+    }
+    if ( fFirst )
+        pBmc->nConfMax /= 10;
+
+    // cleanup
+    Ssw_ClassesCheck( p->ppClasses );
+p->timeBmc += clock() - clk;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if one of the targets has failed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
+{
+    Ssw_Bmc_t * p;
+    int RetValue, Frames, Iter, clk = clock();
+    p = Ssw_BmcManStart( pMan, nConfMax, fVerbose );
+    if ( fCheckTargets && Ssw_BmcCheckTargets( p ) )
+    {
+        assert( 0 );
+        Ssw_BmcManStop( p );
+        return 1;
+    }
+    if ( fVerbose )
+    {
+        printf( "AIG : Const = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n", 
+            Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), 
+            Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
+    } 
+    RetValue = 0;
+    for ( Iter = 0; Iter < p->nPatterns; Iter++ )
+    {
+clk = clock();
+        Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
+        if ( fVerbose )
+        {
+            printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", 
+                Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), 
+                Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pSat->stats.conflicts, p->nPatterns, 
+                p->pMan->nSatFailsReal? "f" : " " );
+            PRT( "T", clock() - clk );
+        } 
+        Ssw_ManCleanup( p->pMan );
+        if ( fCheckTargets && Ssw_BmcCheckTargets( p ) )
+        {
+            printf( "Target is hit!!!\n" );
+            RetValue = 1;
+        }
+        if ( p->nPatterns >= p->nPatternsAlloc )
+            break;
+    }
+    Ssw_BmcManStop( p );
+
+    pMan->nStrangers = 0;
+    pMan->nSatCalls = 0;
+    pMan->nSatProof = 0;
+    pMan->nSatFailsReal = 0; 
+    pMan->nSatFailsTotal = 0;
+    pMan->nSatCallsUnsat = 0;
+    pMan->nSatCallsSat = 0;  
+    pMan->timeSimSat = 0;    
+    pMan->timeSat = 0;       
+    pMan->timeSatSat = 0;    
+    pMan->timeSatUnsat = 0;  
+    pMan->timeSatUndec = 0;  
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index db593311..cfbb138c 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -195,6 +195,22 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_ClassesReadAig( Ssw_Cla_t * p )
+{
+    return p->pAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -643,6 +659,37 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
 
 /**Function*************************************************************
 
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig )
+{
+    Ssw_Cla_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    // start the classes
+    p = Ssw_ClassesStart( pAig );
+    // go through the nodes
+    p->nCands1 = 0;
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        Ssw_ObjSetConst1Cand( pAig, Aig_ObjFanin0(pObj) );
+        p->nCands1++;
+    }
+    // allocate room for classes
+    p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
+//    Ssw_ClassesPrint( p, 0 );
+    return p;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates classes from the temporary representation.]
 
   Description []
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index fc9f5672..424e3531 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -52,6 +52,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->fPolarFlip     =     0;  // uses polarity adjustment
     p->fSkipCheck     =     0;  // do not run equivalence check for unaffected cones
     p->fLatchCorr     =     0;  // performs register correspondence
+    p->fSemiFormal    =     0;  // enable semiformal filtering
     p->fVerbose       =     0;  // verbose stats
     // latch correspondence
     p->fLatchCorrOpt  =     0;  // performs optimized register correspondence
@@ -116,6 +117,16 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
         printf( "After  BMC: " );
         Ssw_ClassesPrint( p->ppClasses, 0 );
     }
+    // apply semi-formal filtering
+    if ( p->pPars->fSemiFormal )
+    {
+        Aig_Man_t * pSRed;
+        Ssw_FilterUsingBmc( p, 0, 2000, p->pPars->fVerbose );
+//        Ssw_FilterUsingBmc( p, 1, 100000, p->pPars->fVerbose );
+        pSRed = Ssw_SpeculativeReduction( p );
+        Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
+        Aig_ManStop( pSRed );
+    }
     // refine classes using induction
     nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
     for ( nIter = 0; ; nIter++ )
@@ -154,6 +165,18 @@ clk = clock();
         Ssw_ManCleanup( p );
         if ( !RetValue )
             break;
+
+        {
+            static int Flag = 0;
+            if ( Flag++ == 4 && nIter == 4 )
+            {
+                Aig_Man_t * pSRed;
+                pSRed = Ssw_SpeculativeReduction( p );
+                Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL );
+                Aig_ManStop( pSRed );
+            }
+        }
+
     } 
     p->pPars->nIters = nIter + 1;
 p->timeTotal = clock() - clkTotal;
@@ -220,6 +243,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     {
         // perform one round of seq simulation and generate candidate equivalence classes
         p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+//        p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
         p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
         Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
     }
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index faa3a87d..5daffc75 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -62,7 +62,7 @@ struct Ssw_Man_t_
     // SAT solving
     sat_solver *     pSat;           // recyclable SAT solver
     int              nSatVars;       // the counter of SAT variables
-    int *            pSatVars;       // mapping of each node into its SAT var
+    Vec_Int_t *      vSatVars;       // mapping of each node into its SAT var
     int              nSatVarsTotal;  // the total number of SAT vars created
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
     // SAT solving (latch corr only)
@@ -118,8 +118,8 @@ struct Ssw_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int  Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
-static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }
+static inline int  Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj )             { return Vec_IntEntry( p->vSatVars, pObj->Id );         }
+static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntWriteEntryFill( p->vSatVars, pObj->Id, Num );  }
 
 static inline int  Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
 {
@@ -143,6 +143,9 @@ static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int
 
 /*=== sswAig.c ===================================================*/
 extern Aig_Man_t *   Ssw_FramesWithClasses( Ssw_Man_t * p );
+extern Aig_Man_t *   Ssw_SpeculativeReduction( Ssw_Man_t * p );
+/*=== sswBmc.c ===================================================*/
+extern int           Ssw_FilterUsingBmc( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose );
 /*=== sswClass.c =================================================*/
 extern Ssw_Cla_t *   Ssw_ClassesStart( Aig_Man_t * pAig );
 extern void          Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
@@ -150,6 +153,7 @@ 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 Aig_Man_t *   Ssw_ClassesReadAig( 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 );
@@ -162,6 +166,7 @@ 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, int fVerbose );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t *   Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
 extern Ssw_Cla_t *   Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
 extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
@@ -200,6 +205,7 @@ extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrame
 extern void          Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
 extern void          Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
 /*=== sswSweep.c ===================================================*/
+extern int           Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
 extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
 extern int           Ssw_ManSweep( Ssw_Man_t * p );
 
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 8d2c8c24..ba19d46e 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -54,7 +54,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     p->nFrames       = pPars->nFramesK + 1;
     p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // SAT solving
-    p->pSatVars      = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
+    p->vSatVars      = Vec_IntStart( Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
     p->vFanins       = Vec_PtrAlloc( 100 );
     // SAT solving (latch corr only)
     p->vUsedNodes    = Vec_PtrAlloc( 1000 );
@@ -147,11 +147,14 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
     }
     if ( p->pSat )
     {
+        int i;
 //        printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
         p->nSatVarsTotal += p->pSat->size;
         sat_solver_delete( p->pSat );
         p->pSat = NULL;
-        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
+//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
+        for ( i = 0; i < Vec_IntSize(p->vSatVars); i++ )
+            p->vSatVars->pArray[i] = 0;
     }
     if ( p->vSimInfo )  
     {
@@ -186,8 +189,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vUsedNodes );
     Vec_PtrFree( p->vUsedPis );
+    Vec_IntFree( p->vSatVars );
     FREE( p->pNodeToFrames );
-    FREE( p->pSatVars );
     FREE( p->pPatWords );
     free( p );
 }
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 9330dafa..add00a88 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -156,14 +156,14 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
+int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
     // get representative of this class
     pObjRepr = Aig_ObjRepr( p->pAig, pObj );
     if ( pObjRepr == NULL )
-        return;
+        return 0;
     // get the fraiged node
     pObjFraig = Ssw_ObjFrame( p, pObj, f );
     // get the fraiged representative
@@ -179,7 +179,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
     { 
         // if the fraiged nodes are the same, return
         if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-            return;
+            return 0;
         // count the number of skipped calls
         if ( !pObj->fMarkA && !pObjRepr->fMarkA )
             p->nRefSkip++;
@@ -196,13 +196,12 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
         {
             pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
             Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
-            return;
+            return 0;
         }
         if ( RetValue == -1 ) // timed out
         {
             Ssw_ClassesRemoveNode( p->ppClasses, pObj );
-            p->fRefined = 1;
-            return;
+            return 1;
         }
         // check if skipping calls works correctly
         if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
@@ -218,7 +217,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
     else
         Ssw_ManResimulateBit( p, pObj, pObjRepr );
     assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
-    p->fRefined = 1;
+    return 1;
 }
 
 /**Function*************************************************************
@@ -262,7 +261,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_ObjSetFrame( p, pObj, f, pObjNew );
-            Ssw_ManSweepNode( p, pObj, f, 1 );
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1 );
         }
         // quit if this is the last timeframe
         if ( f == p->pPars->nFramesK - 1 )
@@ -351,13 +350,13 @@ p->timeMarkCones += clock() - clk;
         if ( p->pPars->fVerbose )
             Bar_ProgressUpdate( pProgress, i, NULL );
         if ( Saig_ObjIsLo(p->pAig, pObj) )
-            Ssw_ManSweepNode( p, pObj, f, 0 );
+            p->fRefined |= 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_ObjSetFrame( p, pObj, f, pObjNew );
-            Ssw_ManSweepNode( p, pObj, f, 0 );
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
         }
     }
     p->nSatFailsTotal += p->nSatFailsReal;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4944a43f..5d5ccb46 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13535,7 +13535,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Ssw_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13625,6 +13625,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             pPars->fSkipCheck ^= 1;
             break;
+        case 'f':
+            pPars->fSemiFormal ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -13677,7 +13680,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsvh]\n" );
+    fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsfvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
     fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -13689,6 +13692,7 @@ usage:
     fprintf( pErr, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
     fprintf( pErr, "\t-s     : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index f20c7cc8..437b4d8e 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -424,6 +424,25 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntWriteEntryFill( Vec_Int_t * p, int i, int Entry )
+{
+    assert( i >= 0 );
+    if ( i >= p->nSize )
+        Vec_IntFillExtra( p, 2 * i, 0 );
+    Vec_IntWriteEntry( p, i, Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
 {
     assert( p->nSize >= nSizeNew );