Version abc80919

10 files changed, 442 insertions, 11 deletions

diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index daf69370..c5668d6d 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -2,6 +2,7 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswClass.c \
     src/aig/ssw/sswCnf.c \
     src/aig/ssw/sswCore.c \
+    src/aig/ssw/sswLcorr.c \
     src/aig/ssw/sswMan.c \
     src/aig/ssw/sswPart.c \
     src/aig/ssw/sswPairs.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 91c2165a..2917f6d4 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -51,6 +51,9 @@ struct Ssw_Pars_t_
     int              nMinDomSize;   // min clock domain considered for optimization
     int              fPolarFlip;    // uses polarity adjustment
     int              fLatchCorr;    // perform register correspondence
+    int              fLatchCorrOpt; // perform register correspondence (optimized)
+    int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
+    int              nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only)
     int              fSkipCheck;    // does not run equivalence check for unaffected cones
     int              fVerbose;      // verbose stats
     // internal parameters
@@ -86,6 +89,12 @@ extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t
 extern int           Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
+/*=== sswSim.c ===================================================*/
+extern Ssw_Cex_t *   Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
+extern void          Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex );
+extern int           Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
+extern int           Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p );
+extern Ssw_Cex_t *   Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index e186946a..81e8de8b 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -294,6 +294,28 @@ Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSiz
 
 /**Function*************************************************************
 
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass )
+{
+    int i;
+    Vec_PtrClear( vClass );
+    if ( p->pId2Class[pRepr->Id] == NULL )
+        return;
+    assert( p->pClassSizes[pRepr->Id] > 1 );
+    for ( i = 1; i < p->pClassSizes[pRepr->Id]; i++ )
+        Vec_PtrPush( vClass, p->pId2Class[pRepr->Id][i] );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks candidate equivalence classes.]
 
   Description []
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index b047a312..e4b8f9f6 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -264,6 +264,12 @@ void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
     assert( Ssw_ObjSatNum(p,pObj) == 0 );
     if ( Aig_ObjIsConst1(pObj) )
         return;
+    if ( p->pPars->fLatchCorrOpt )
+    {
+        Vec_PtrPush( p->vUsedNodes, pObj );
+        if ( Aig_ObjIsPi(pObj) )
+            Vec_PtrPush( p->vUsedPis, pObj );
+    }
     Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
     sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
     if ( Aig_ObjIsNode(pObj) )
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 8e3ab01a..6a3e9264 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -52,6 +52,11 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->fPolarFlip     =     0;  // uses polarity adjustment
     p->fLatchCorr     =     0;  // performs register correspondence
     p->fVerbose       =     0;  // verbose stats
+    // latch correspondence
+    p->fLatchCorrOpt  =     0;  // performs optimized register correspondence
+    p->nSatVarMax     =  5000;  // the max number of SAT variables
+    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
+    // return values
     p->nIters         =     0;  // the number of iterations performed
 }
 
@@ -81,8 +86,11 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
         printf( "Before BMC: " );
         Ssw_ClassesPrint( p->ppClasses, 0 );
     }
-    Ssw_ManSweepBmc( p );
-    Ssw_ManCleanup( p );
+    if ( !p->pPars->fLatchCorr )
+    { 
+        Ssw_ManSweepBmc( p );
+        Ssw_ManCleanup( p );
+    }
     if ( p->pPars->fVerbose )
     {
         printf( "After  BMC: " );
@@ -92,7 +100,10 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     for ( nIter = 0; ; nIter++ )
     {
 clk = clock();
-        RetValue = Ssw_ManSweep( p );
+        if ( p->pPars->fLatchCorrOpt )
+            RetValue = Ssw_ManSweepLatch( p );
+        else
+            RetValue = Ssw_ManSweep( p );
         if ( p->pPars->fVerbose )
         {
             printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
@@ -134,6 +145,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     Ssw_Pars_t Pars;
     Aig_Man_t * pAigNew;
     Ssw_Man_t * p;
+    assert( Aig_ManRegNum(pAig) > 0 );
     // reset random numbers
     Aig_ManRandom( 1 );
     // if parameters are not given, create them
@@ -148,14 +160,18 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
         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 );
+    if ( pPars->fLatchCorrOpt )
+        pPars->fLatchCorr = 1;
+    else
+    {
+        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 induction manager
     p = Ssw_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 6824e239..5b4377c7 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -67,6 +67,11 @@ struct Ssw_Man_t_
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
     Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
     Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
+    // SAT solving (latch corr only)
+    int              nCallsSince;    // the number of calls since last recycling
+    int              nRecycles;      // the number of time SAT solver was recycled
+    Vec_Ptr_t *      vUsedNodes;     // the nodes with SAT variables
+    Vec_Ptr_t *      vUsedPis;       // the PIs with SAT variables
     // sequential simulator
     Ssw_Sml_t *      pSml;
     // counter example storage
@@ -145,6 +150,7 @@ extern int           Ssw_ClassesCand1Num( Ssw_Cla_t * p );
 extern int           Ssw_ClassesClassNum( Ssw_Cla_t * p );
 extern int           Ssw_ClassesLitNum( Ssw_Cla_t * p );
 extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
+extern void          Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass );
 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 );
@@ -161,6 +167,8 @@ extern int           Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_
 extern void          Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
 /*=== sswCore.c ===================================================*/
 extern Aig_Man_t *   Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
+/*=== sswLcorr.c ==========================================================*/
+extern int           Ssw_ManSweepLatch( Ssw_Man_t * p );
 /*=== sswMan.c ===================================================*/
 extern Ssw_Man_t *   Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 extern void          Ssw_ManCleanup( Ssw_Man_t * p );
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
new file mode 100644
index 00000000..dcc4f245
--- /dev/null
+++ b/src/aig/ssw/sswLcorr.c
@@ -0,0 +1,286 @@
+/**CFile****************************************************************
+
+  FileName    [sswLcorr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Latch correspondence.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswLcorr.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "bar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
+{
+    int Lit;
+    if ( p->pSat )
+    {
+        Aig_Obj_t * pObj;
+        int i;
+        Vec_PtrForEachEntry( p->vUsedNodes, pObj, i )
+            Ssw_ObjSetSatNum( p, pObj, 0 );
+        Vec_PtrClear( p->vUsedNodes );
+        Vec_PtrClear( p->vUsedPis );
+//        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAigTotal) );
+        sat_solver_delete( p->pSat );
+    }
+    p->pSat = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 1000 );
+    // var 0 is not used
+    // var 1 is reserved for const1 node - add the clause
+    p->nSatVars = 1;
+//    p->nSatVars = 0;
+    Lit = toLit( p->nSatVars );
+    if ( p->pPars->fPolarFlip )
+        Lit = lit_neg( Lit );
+    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
+
+    p->nRecycles++;
+    p->nCallsSince = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
+{
+    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, 0 ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlSavePatternLatchPhase( 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    [Builds fraiged logic cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Ssw_ObjFraig( p, pObj, 0 ) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) );
+    Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) );
+    pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
+    Ssw_ObjSetFraig( p, pObj, 0, pObjNew );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recycles the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjFraig, * pObjFraig2, * pObjReprFraig, * pObjLi;
+    int RetValue;
+    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
+    // get the fraiged node
+    pObjLi = Saig_ObjLoToLi( p->pAig, pObj ); 
+    Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
+    pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
+    // get the fraiged representative
+    if ( Aig_ObjIsPi(pObjRepr) )
+    {
+        pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); 
+        Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
+        pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
+    }
+    else 
+        pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, 0 );
+    // if the fraiged nodes are the same, return
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+        return;
+    p->nCallsSince++;
+    // check equivalence of the two nodes
+    if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
+    {
+        p->nStrangers++;
+        Ssw_SmlSavePatternLatchPhase( p, 0 );
+    }
+    else
+    { 
+        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+        if ( RetValue == 1 )  // proved equivalent
+        {
+            pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+            Ssw_ObjSetFraig( p, pObj, 0, pObjFraig2 );
+            return;
+        }
+        else if ( RetValue == -1 ) // timed out
+        {
+            Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+            p->fRefined = 1;
+            return;
+        }
+        else // disproved the equivalence
+        {       
+            Ssw_SmlSavePatternLatch( p );
+        }
+    }
+    if ( p->pPars->nConstrs == 0 )
+        Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, 0 );
+    else
+        Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, 0 );
+    assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
+    p->fRefined = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one iteration of sweeping latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepLatch( Ssw_Man_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Vec_Ptr_t * vClass;
+    Aig_Obj_t * pObj, * pRepr, * pTemp;
+    int i, k;
+
+    // start the timeframe
+    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
+    // map constants and PIs
+    Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
+
+    // implement equivalence classes
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        pRepr = Aig_ObjRepr( p->pAig, pObj );
+        if ( pRepr == NULL )
+            pTemp = Aig_ObjCreatePi(p->pFrames);
+        else
+            pTemp = Aig_NotCond( Ssw_ObjFraig(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
+        Ssw_ObjSetFraig( p, pObj, 0, pTemp );
+    }
+
+    // go through the registers
+    if ( p->pPars->fVerbose )
+        pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
+    vClass = Vec_PtrAlloc( 100 );
+    p->fRefined = 0;
+    Saig_ManForEachLo( p->pAig, pObj, i )
+    {
+        if ( p->pPars->fVerbose )
+            Bar_ProgressUpdate( pProgress, i, NULL );
+        // consider the case of constant candidate
+        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
+            Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
+        else
+        {
+            // consider the case of equivalence class
+            Ssw_ClassesCollectClass( p->ppClasses, pObj, vClass );
+            if ( Vec_PtrSize(vClass) == 0 )
+                continue;
+            // try to prove equivalences in this class
+            Vec_PtrForEachEntry( vClass, pTemp, k )
+                if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
+                    Ssw_ManSweepLatchOne( p, pObj, pTemp );
+        }
+        // attempt recycling the SAT solver
+        if ( p->pPars->nSatVarMax && 
+             p->nSatVars > p->pPars->nSatVarMax &&
+             p->nCallsSince > p->pPars->nCallsRecycle )
+             Ssw_ManSatSolverRecycle( p );
+    }
+    Vec_PtrFree( vClass );
+    p->nSatFailsTotal += p->nSatFailsReal;
+    if ( p->pPars->fVerbose )
+        Bar_ProgressStop( pProgress );
+
+    // cleanup
+    Ssw_ClassesCheck( p->ppClasses );
+    return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 559f7b6c..33c716ce 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -58,6 +58,9 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     p->vFanins       = Vec_PtrAlloc( 100 );
     p->vSimRoots     = Vec_PtrAlloc( 1000 );
     p->vSimClasses   = Vec_PtrAlloc( 1000 );
+    // SAT solving (latch corr only)
+    p->vUsedNodes    = Vec_PtrAlloc( 1000 );
+    p->vUsedPis      = Vec_PtrAlloc( 1000 );
     // allocate storage for sim pattern
     p->nPatWords     = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
     p->pPatWords     = ALLOC( unsigned, p->nPatWords ); 
@@ -178,6 +181,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vSimRoots );
     Vec_PtrFree( p->vSimClasses );
+    Vec_PtrFree( p->vUsedNodes );
+    Vec_PtrFree( p->vUsedPis );
     FREE( p->pNodeToFraig );
     FREE( p->pSatVars );
     FREE( p->pPatWords );
@@ -209,6 +214,9 @@ void Ssw_ManStartSolver( Ssw_Man_t * p )
         Lit = lit_neg( Lit );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
     Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
+
+    Vec_PtrClear( p->vUsedNodes );
+    Vec_PtrClear( p->vUsedPis );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 64175b40..769e923c 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -1021,6 +1021,49 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
+{
+    Ssw_Sml_t * pSml;
+    Aig_Obj_t * pObj;
+    int i, k, iBit, iOut;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
+    // start a new sequential simulator
+    pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
+    // assign simulation info for the registers
+    iBit = 0;
+    Saig_ManForEachLo( pAig, pObj, i )
+        Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+    // assign simulation info for the primary inputs
+    for ( i = 0; i <= p->iFrame; i++ )
+        Saig_ManForEachPi( pAig, pObj, k )
+            Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+    assert( iBit == p->nBits );
+    // run random simulation
+    Ssw_SmlSimulateOne( pSml );
+    // check if the given output has failed
+    iOut = -1;
+    Saig_ManForEachPo( pAig, pObj, k )
+        if ( !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) )
+        {
+            iOut = k;
+            break;
+        }
+    Ssw_SmlStop( pSml );
+    return iOut;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates sequential counter-example from the simulation info.]
 
   Description []
@@ -1182,6 +1225,30 @@ Ssw_Cex_t * Ssw_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
 
 /**Function*************************************************************
 
+  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cex_t * Ssw_SmlDupCounterExample( Ssw_Cex_t * p, int nRegsNew )
+{
+    Ssw_Cex_t * pCex;
+    int i;
+    pCex = Ssw_SmlAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
+    pCex->iPo    = p->iPo;
+    pCex->iFrame = p->iFrame;
+    for ( i = p->nRegs; i < p->nBits; i++ )
+        if ( Aig_InfoHasBit(p->pData, i) )
+            Aig_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
+    return pCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resimulates the counter-example.]
 
   Description []
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 3fa39612..715750ca 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -113,6 +113,14 @@ int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
     {
         if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
     }
+/*
+    if ( nVarNum==0 )
+        printf( "x" );
+    else if ( Value == 0 )
+        printf( "0" );
+    else
+        printf( "1" );
+*/
     return Value;
 }