Version abc90311

10 files changed, 586 insertions, 23 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 16748233..a97bd958 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -57,7 +57,7 @@ struct Cec_ParSim_t_
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
     int              TimeLimit;     // the runtime limit in seconds
-    int              fDoubleOuts;   // miter with separate outputs
+    int              fDualOut;      // miter with separate outputs
     int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
     int              fSeqSimulate;  // performs sequential simulation
@@ -65,6 +65,21 @@ struct Cec_ParSim_t_
     int              fVerbose;      // verbose stats
 };
 
+// semiformal parameters
+typedef struct Cec_ParSmf_t_ Cec_ParSmf_t;
+struct Cec_ParSmf_t_
+{
+    int              nWords;        // the number of simulation words
+    int              nRounds;       // the number of simulation rounds
+    int              nFrames;       // the number of time frames
+    int              nBTLimit;      // conflict limit at a node
+    int              TimeLimit;     // the runtime limit in seconds
+    int              fDualOut;      // miter with separate outputs
+    int              fCheckMiter;   // the circuit is the miter
+    int              fFirstStop;    // stop on the first sat output
+    int              fVerbose;      // verbose stats
+};
+
 // combinational SAT sweeping parameters
 typedef struct Cec_ParFra_t_ Cec_ParFra_t;
 struct Cec_ParFra_t_
@@ -79,7 +94,7 @@ struct Cec_ParFra_t_
     int              fRewriting;    // enables AIG rewriting
     int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
-    int              fDoubleOuts;   // miter with separate outputs
+    int              fDualOut;      // miter with separate outputs
     int              fColorDiff;    // miter with separate outputs
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
@@ -112,11 +127,15 @@ extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerb
 /*=== cecCore.c ==========================================================*/
 extern void          Cec_ManSatSetDefaultParams( Cec_ParSat_t * p );
 extern void          Cec_ManSimSetDefaultParams( Cec_ParSim_t * p );
+extern void          Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p );
 extern void          Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
 extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
 extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
 extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern void          Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
+/*=== cecSeq.c ==========================================================*/
+extern int           Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex );
+extern int           Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index ea730693..96bddbcb 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -134,7 +134,7 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
     pParsFra->fVerbose     = pPars->fVerbose;
     pParsFra->fCheckMiter  = 1;
     pParsFra->fFirstStop   = 1;
-    pParsFra->fDoubleOuts  = 1;
+    pParsFra->fDualOut     = 1;
     pNew = Cec_ManSatSweeping( p, pParsFra );
     if ( pNew == NULL )
     {
@@ -192,7 +192,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
     int RetValue;
     Cec_ManCecSetDefaultParams( pPars );
     pPars->fVerbose = fVerbose;
-    pMiter = Gia_ManMiter( p0, p1, 0, 1, pPars->fVerbose );
+    pMiter = Gia_ManMiter( p0, p1, 1, 0, pPars->fVerbose );
     if ( pMiter == NULL )
         return -1;
     RetValue = Cec_ManVerify( pMiter, pPars );
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index aaa85ffa..0cac88af 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -155,6 +155,70 @@ int Cec_ManSimCompareEqualFirstBit( unsigned * p0, unsigned * p1, int nWords )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of the first non-equal bit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimCompareConstScore( unsigned * p, int nWords, int * pScores )
+{
+    int w, b;
+    if ( p[0] & 1 )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p[w] != ~0 )
+                for ( b = 0; b < 32; b++ )
+                    if ( ((~p[w]) >> b ) & 1 )
+                        pScores[32*w + b]++;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p[w] != 0 )
+                for ( b = 0; b < 32; b++ )
+                    if ( ((p[w]) >> b ) & 1 )
+                        pScores[32*w + b]++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares simulation info of two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimCompareEqualScore( unsigned * p0, unsigned * p1, int nWords, int * pScores )
+{
+    int w, b;
+    if ( (p0[0] & 1) == (p1[0] & 1) )
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != p1[w] )
+                for ( b = 0; b < 32; b++ )
+                    if ( ((p0[w] ^ p1[w]) >> b ) & 1 )
+                        pScores[32*w + b]++;
+    }
+    else
+    {
+        for ( w = 0; w < nWords; w++ )
+            if ( p0[w] != ~p1[w] )
+                for ( b = 0; b < 32; b++ )
+                    if ( ((p0[w] ^ ~p1[w]) >> b ) & 1 )
+                        pScores[32*w + b]++;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates equivalence class.]
 
   Description []
@@ -211,7 +275,11 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
         if ( Cec_ManSimCompareEqual( pSim0, pSim1, p->nWords ) )
             Vec_IntPush( p->vClassOld, Ent );
         else
+        {
             Vec_IntPush( p->vClassNew, Ent );
+            if ( p->pBestState )
+                Cec_ManSimCompareEqualScore( pSim0, pSim1, p->nWords, p->pScores );
+        }
     }
     if ( Vec_IntSize( p->vClassNew ) == 0 )
         return 0;
@@ -422,6 +490,42 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
 
 /**Function*************************************************************
 
+  Synopsis    [Find the best pattern using the scores.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
+{
+    unsigned * pInfo;
+    int i, ScoreBest = 0, iPatBest = 1;
+    // find the best pattern
+    for ( i = 0; i < 32 * p->nWords; i++ )
+        if ( ScoreBest < p->pScores[i] )
+        {
+            ScoreBest = p->pScores[i];
+            iPatBest = i;
+        }
+    // compare this with the available patterns - and save
+    if ( p->pBestState->iPo <= ScoreBest )
+    {
+        assert( p->pBestState->nRegs == Gia_ManRegNum(p->pAig) );
+        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+        {
+            pInfo = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
+            if ( Aig_InfoHasBit(p->pBestState->pData, i) != Aig_InfoHasBit(pInfo, iPatBest) )
+                Aig_InfoXorBit( p->pBestState->pData, i );
+        }
+        p->pBestState->iPo = ScoreBest;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if computation should stop.]
 
   Description []
@@ -435,10 +539,11 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
 {
     unsigned * pInfo, * pInfo2;
     int i;
-    if ( p->vCoSimInfo == NULL )
+    if ( !p->pPars->fCheckMiter )
         return 0;
+    assert( p->vCoSimInfo != NULL );
     // compare outputs with 0
-    if ( p->pPars->fDoubleOuts )
+    if ( p->pPars->fDualOut )
     {
         assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
         for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
@@ -507,6 +612,10 @@ int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t *
     if ( p->nWordsOld != p->nWords )
         Cec_ManSimMemRelink( p );
     p->nMemsMax = 0;
+    // allocate score counters
+    ABC_FREE( p->pScores );
+    if ( p->pBestState )
+        p->pScores = ABC_CALLOC( int, 32 * p->nWords );
     // simulate nodes
     Vec_IntClear( p->vRefinedC );
     if ( Gia_ObjValue(Gia_ManConst0(p->pAig)) )
@@ -583,6 +692,8 @@ references:
         {
             pRes[0]++;
             Vec_IntPush( p->vRefinedC, i );
+            if ( p->pBestState )
+                Cec_ManSimCompareConstScore( pRes + 1, p->nWords, p->pScores );
         }
         // if the node belongs to a class, save it
         if ( Gia_ObjIsClass(p->pAig, i) )
@@ -607,6 +718,8 @@ references:
         printf( "Cec_ManSimSimulateRound(): Memory management error!\n" );
     if ( p->pPars->fVeryVerbose )
         Gia_ManEquivPrintClasses( p->pAig, 0, Cec_MemUsage(p) );
+    if ( p->pBestState )
+        Cec_ManSimFindBestPattern( p );
 /*
     if ( p->nMems > 1 ) {
         for ( i = 1; i < p->nObjs; i++ )
@@ -682,8 +795,13 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p )
     // allocate representation
     p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) );
     p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) );
+    // set starting representative of internal nodes to be constant 0
     Gia_ManForEachObj( p->pAig, pObj, i )
-        Gia_ObjSetRepr( p->pAig, i, (Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj)) ? 0 : GIA_VOID );
+        Gia_ObjSetRepr( p->pAig, i, Gia_ObjIsAnd(pObj) ? 0 : GIA_VOID );
+    // if sequential simulation, set starting representative of ROs to be constant 0
+    if ( p->pPars->fSeqSimulate )
+        Gia_ManForEachRo( p->pAig, pObj, i )
+            Gia_ObjSetRepr( p->pAig, Gia_ObjId(p->pAig, pObj), 0 );
     // perform simulation
     Gia_ManSetRefs( p->pAig );
     p->nWords = 1;
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index e25ddc90..061c3a7d 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -70,12 +70,37 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
     p->TimeLimit      =       0;  // the runtime limit in seconds
     p->fCheckMiter    =       0;  // the circuit is the miter
     p->fFirstStop     =       0;  // stop on the first sat output
-    p->fDoubleOuts    =       0;  // miter with separate outputs
+    p->fDualOut       =       0;  // miter with separate outputs
     p->fSeqSimulate   =       0;  // performs sequential simulation
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
 } 
-  
+
+/**Function************  *************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
+{
+    memset( p, 0, sizeof(Cec_ParSmf_t) );
+    p->nWords         =      15;  // the number of simulation words
+    p->nRounds        =      15;  // the number of simulation rounds
+    p->nFrames        =       2;  // the number of time frames
+    p->nBTLimit       =    1000;  // conflict limit at a node
+    p->TimeLimit      =       0;  // the runtime limit in seconds
+    p->fDualOut       =       0;  // miter with separate outputs
+    p->fCheckMiter    =       0;  // the circuit is the miter
+    p->fFirstStop     =       0;  // stop on the first sat output
+    p->fVerbose       =       0;  // verbose stats
+} 
+
 /**Function************  *************************************************
 
   Synopsis    [This procedure sets default parameters.]
@@ -100,7 +125,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
     p->fRewriting     =       0;  // enables AIG rewriting
     p->fCheckMiter    =       0;  // the circuit is the miter
     p->fFirstStop     =       0;  // stop on the first sat output
-    p->fDoubleOuts    =       0;  // miter with separate outputs
+    p->fDualOut       =       0;  // miter with separate outputs
     p->fColorDiff     =       0;  // miter with separate outputs
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
@@ -177,7 +202,8 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
     if ( pPars->fCheckMiter )
         printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", 
             pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds );
-    ABC_PRT( "Time", clock() - clkTotal );
+    if ( pPars->fVerbose )
+        ABC_PRT( "Time", clock() - clkTotal );
     Cec_ManSimStop( pSim );
 }
 
@@ -213,7 +239,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     // prepare the managers
     // SAT sweeping
     p = Cec_ManFraStart( pIni, pPars );
-    if ( pPars->fDoubleOuts )
+    if ( pPars->fDualOut )
         pPars->fColorDiff = 1;
     // simulation
     Cec_ManSimSetDefaultParams( pParsSim );
@@ -221,10 +247,9 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     pParsSim->nRounds     = pPars->nRounds;
     pParsSim->fCheckMiter = pPars->fCheckMiter;
     pParsSim->fFirstStop  = pPars->fFirstStop;
-    pParsSim->fDoubleOuts = pPars->fDoubleOuts;
+    pParsSim->fDualOut = pPars->fDualOut;
     pParsSim->fVerbose    = pPars->fVerbose;
     pSim = Cec_ManSimStart( p->pAig, pParsSim );
-    pSim->nWords = p->pPars->nWords;
     // SAT solving
     Cec_ManSatSetDefaultParams( pParsSat );
     pParsSat->nBTLimit = pPars->nBTLimit;
@@ -250,7 +275,7 @@ p->timeSim += clock() - clk;
     {
         clk2 = clock();
         nMatches = 0;
-        if ( pPars->fDoubleOuts )
+        if ( pPars->fDualOut )
         {
             nMatches = Gia_ManEquivSetColors( p->pAig, pPars->fVeryVerbose );
 //            p->pAig->pIso = Cec_ManDetectIsomorphism( p->pAig );
@@ -264,7 +289,7 @@ p->timeSim += clock() - clk;
             Gia_ManStop( pSrm );
             if ( p->pPars->fVerbose )
                 printf( "Considered all available candidate equivalences.\n" );
-            if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) > 0 )
+            if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) > 0 )
             {
                 if ( pPars->fColorDiff )
                 {
@@ -276,7 +301,7 @@ p->timeSim += clock() - clk;
                 {
                     if ( p->pPars->fVerbose )
                         printf( "Switching into normal mode.\n" );
-                    pPars->fDoubleOuts = 0;
+                    pPars->fDualOut = 0;
                 }
                 continue;
             }
@@ -295,7 +320,7 @@ p->timeSat += clock() - clk;
         Gia_ManStop( pSrm );
 
         // update the manager
-        pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDoubleOuts );
+        pSim->pAig = p->pAig = Gia_ManEquivReduceAndRemap( pTemp = p->pAig, 0, pParsSim->fDualOut );
         Gia_ManStop( pTemp );
         if ( p->pPars->fVerbose )
         {
@@ -332,18 +357,18 @@ p->timeSat += clock() - clk;
                 }
             }
         }
-        if ( pPars->fDoubleOuts && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 )
+        if ( pPars->fDualOut && pPars->fColorDiff && Gia_ManAndNum(p->pAig) < 100000 )
         {
             if ( p->pPars->fVerbose )
                 printf( "Switching into reduced mode.\n" );
             pPars->fColorDiff = 0;
         }
-        if ( pPars->fDoubleOuts && Gia_ManAndNum(p->pAig) < 20000 )
+        if ( pPars->fDualOut && Gia_ManAndNum(p->pAig) < 20000 )
         {
             if ( p->pPars->fVerbose )
                 printf( "Switching into normal mode.\n" );
             pPars->fColorDiff = 0;
-            pPars->fDoubleOuts = 0;
+            pPars->fDualOut = 0;
         }
     }
 finalize:
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 1898b07c..ae4c6ff4 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -117,13 +117,17 @@ struct Cec_ManSim_t_
     int              nMemsMax;       // the max number of used entries 
     int              MemFree;        // next free entry
     int              nWordsOld;      // the number of simulation words after previous relink
-    // bug catcher
+    // internal simulation info
     Vec_Ptr_t *      vCiSimInfo;     // CI simulation info  
     Vec_Ptr_t *      vCoSimInfo;     // CO simulation info  
+    // counter examples
     void **          pCexes;         // counter-examples for each output
     int              iOut;           // first failed output
     int              nOuts;          // the number of failed outputs
     Gia_Cex_t *      pCexComb;       // counter-example for the first failed output
+    Gia_Cex_t *      pBestState;     // the state that led to most of the refinements
+    // scoring simulation patterns
+    int *            pScores;        // counters of refinement for each pattern
     // temporaries
     Vec_Int_t *      vClassOld;      // old class numbers
     Vec_Int_t *      vClassNew;      // new class numbers
@@ -182,6 +186,7 @@ extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
+extern void                 Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
 /*=== ceFraeep.c ============================================================*/
 extern Gia_Man_t *          Cec_ManFraSpecReduction( Cec_ManFra_t * p );
 extern int                  Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index 1a94409f..14f2493e 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -193,6 +193,7 @@ Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t *  pPars )
     memset( p, 0, sizeof(Cec_ManSim_t) );
     p->pAig  = pAig;
     p->pPars = pPars;
+    p->nWords = pPars->nWords;
     p->pSimInfo = ABC_CALLOC( int, Gia_ManObjNum(pAig) );
     p->vClassOld  = Vec_IntAlloc( 1000 );
     p->vClassNew  = Vec_IntAlloc( 1000 );
@@ -229,6 +230,7 @@ void Cec_ManSimStop( Cec_ManSim_t * p )
         Vec_PtrFree( p->vCiSimInfo );
     if ( p->vCoSimInfo ) 
         Vec_PtrFree( p->vCoSimInfo );
+    ABC_FREE( p->pScores );
     ABC_FREE( p->pCexComb );
     ABC_FREE( p->pCexes );
     ABC_FREE( p->pMems );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
new file mode 100644
index 00000000..6cb229ae
--- /dev/null
+++ b/src/aig/cec/cecSeq.c
@@ -0,0 +1,314 @@
+/**CFile****************************************************************
+
+  FileName    [cecSeq.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinatinoal equivalence checking.]
+
+  Synopsis    [Refinement of sequential equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cecInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Sets register values from the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSeqDeriveInfoFromCex( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
+{
+    unsigned * pInfo;
+    int k, w, nWords;
+    assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
+    assert( pCex->nBits <= Vec_PtrSize(vInfo) );
+    nWords = Vec_PtrReadWordsSimInfo( vInfo );
+    for ( k = 0; k < pCex->nRegs; k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+    }
+    for ( ; k < pCex->nBits; k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Aig_ManRandom(0);
+        // set simulation pattern and make sure it is second (first will be erased during simulation)
+        pInfo[0] = (pInfo[0] << 1) | Aig_InfoHasBit( pCex->pData, k ); 
+        pInfo[0] <<= 1;
+    }
+    for ( ; k < Vec_PtrSize(vInfo); k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Aig_ManRandom(0);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets register values from the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex )
+{
+    unsigned * pInfo;
+    int k, w, nWords;
+    nWords = Vec_PtrReadWordsSimInfo( vInfo );
+    assert( Gia_ManRegNum(pAig) == pCex->nRegs );
+    assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
+    for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Aig_InfoHasBit( pCex->pData, k )? ~0 : 0;
+    }
+
+    for ( ; k < Vec_PtrSize(vInfo); k++ )
+    {
+        pInfo = Vec_PtrEntry( vInfo, k );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = Aig_ManRandom( 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the classes using sequential simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
+{
+    unsigned * pInfo0, * pInfo1;
+    int f, i, k, w, RetValue = 0;
+    assert( Gia_ManRegNum(p->pAig) > 0 );
+    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
+    for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
+    {
+        pInfo0 = Vec_PtrEntry( vInfo, k );
+        pInfo1 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
+        for ( w = 0; w < p->nWords; w++ )
+            pInfo1[w] = pInfo0[w];
+    }
+    for ( f = 0; f < p->pPars->nRounds; f++ )
+    {
+        for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+        {
+            pInfo0 = Vec_PtrEntry( vInfo, k++ );
+            pInfo1 = Vec_PtrEntry( p->vCiSimInfo, i );
+            for ( w = 0; w < p->nWords; w++ )
+                pInfo1[w] = pInfo0[w];
+        }
+        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+        {
+            pInfo0 = Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
+            pInfo1 = Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
+            for ( w = 0; w < p->nWords; w++ )
+                pInfo1[w] = pInfo0[w];
+        }
+        if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
+        {
+            printf( "One of the outputs of the miter is asserted.\n" );
+            RetValue = 1;
+        }
+    }
+    assert( k == Vec_PtrSize(vInfo) );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates information to refine equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState )
+{
+    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+    Cec_ManSim_t * pSim;
+    int RetValue, clkTotal = clock();
+    assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
+    Cec_ManSimSetDefaultParams( pParsSim );
+    pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
+    pParsSim->nWords  = Vec_PtrReadWordsSimInfo( vSimInfo );
+    Gia_ManSetRefs( pAig );
+    pSim = Cec_ManSimStart( pAig, pParsSim );
+    if ( pBestState )
+        pSim->pBestState = pBestState;
+    RetValue = Cec_ManSeqResimulate( pSim, vSimInfo );
+    pSim->pBestState = NULL;
+    Cec_ManSimStop( pSim );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimuates one counter-example to refine equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex_t * pCex )
+{
+    Vec_Ptr_t * vSimInfo;
+    int RetValue, clkTotal = clock();
+    if ( pCex == NULL )
+    {
+        printf( "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
+        return -1;
+    }
+    if ( pAig->pReprs == NULL )
+    {
+        printf( "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
+        return -1;
+    }
+    if ( Gia_ManRegNum(pAig) == 0 )
+    {
+        printf( "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
+        return -1;
+    }
+    if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
+    {
+        printf( "Cec_ManSeqResimulateCounter(): Parameters of the ccounter-example differ.\n" );
+        return -1;
+    }
+    if ( pPars->fVerbose )
+        printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
+    Aig_ManRandom( 1 );
+    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
+        Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
+    Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
+    if ( pPars->fVerbose )
+        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL );
+    if ( pPars->fVerbose )
+        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+    Vec_PtrFree( vSimInfo );
+    if ( pPars->fVerbose )
+        ABC_PRT( "Time", clock() - clkTotal );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs semiformal refinement of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
+{ 
+    int nAddFrames = 10; // additional timeframes to simulate
+    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+    Vec_Ptr_t * vSimInfo; 
+    Gia_Cex_t * pState;
+    Gia_Man_t * pSrm;
+    int r, nPats, RetValue = -1;
+    if ( pAig->pReprs == NULL )
+    {
+        printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
+        return -1;
+    }
+    if ( Gia_ManRegNum(pAig) == 0 )
+    {
+        printf( "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
+        return -1;
+    }
+    Aig_ManRandom( 1 );
+    // prepare starting pattern
+    pState = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), 0, 0 );
+    pState->iFrame = -1;
+    pState->iPo = -1;
+    // prepare SAT solving
+    Cec_ManSatSetDefaultParams( pParsSat );
+    pParsSat->nBTLimit = pPars->nBTLimit;
+    pParsSat->fVerbose = pPars->fVerbose;
+    if ( pParsSat->fVerbose )
+    {
+        printf( "Starting: " );
+        Gia_ManEquivPrintClasses( pAig, 0, 0 );
+    }
+    // perform the given number of BMC rounds
+    for ( r = 0; r < pPars->nRounds; r++ )
+    {
+//        Gia_ManPrintCounterExample( pState );
+        // derive speculatively reduced model
+        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManPiNum(pAig) * pPars->nFrames );
+        // allocate room for simulation info
+        vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
+            Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
+        Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
+        // fill in simulation info with counter-examples
+        Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
+        Gia_ManStop( pSrm );
+        // resimulate and refine the classes
+        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );
+        Vec_PtrFree( vSimInfo );
+        assert( pState->iPo >= 0 ); // hit counter
+        pState->iPo = -1;
+        if ( pPars->fVerbose )
+        {
+            printf( "BMC = %3d ", nPats );
+            Gia_ManEquivPrintClasses( pAig, 0, 0 );
+        }
+    }
+    ABC_FREE( pState );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index ba4b0477..2b6997e1 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -630,6 +630,85 @@ ABC_PRT( "time", clock() - clk2 );
     Cec_ManSatStop( p );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Save values in the cone of influence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
+        if ( Cec_ObjSatVarValue( pSat, pObj ) != Aig_InfoHasBit( pInfo, iPat ) )
+            Aig_InfoXorBit( pInfo, iPat );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin0(pObj), vInfo, iPat, nRegs );
+    Cec_ManSatSolveSeq_rec( pSat, p, Gia_ObjFanin1(pObj), vInfo, iPat, nRegs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of solving for the POs of the AIG.]
+
+  Description [Labels the nodes that have been proved (pObj->fMark1) 
+  and returns the set of satisfying assignments.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Cec_ManSat_t * p;
+    Gia_Obj_t * pObj;
+    int iPat = 1, nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
+    int i, status, clk = clock();
+    Gia_ManSetPhase( pAig );
+    Gia_ManLevelNum( pAig );
+    Gia_ManResetTravId( pAig );
+    p = Cec_ManSatCreate( pAig, pPars );
+    pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
+    Gia_ManForEachCo( pAig, pObj, i )
+    {
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+            continue;
+        Bar_ProgressUpdate( pProgress, i, "BMC..." );
+        status = Cec_ManSatCheckNode( p, pObj );
+        if ( status != 0 )
+            continue;
+        // save the pattern
+        Gia_ManIncrementTravId( pAig );
+        Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
+        if ( iPat == nPats )
+            break;
+        // quit if one of them is solved
+        if ( pPars->fFirstStop )
+            break;
+    }
+    p->timeTotal = clock() - clk;
+    Bar_ProgressStop( pProgress );
+//    Cec_ManSatPrintStats( p );
+    Cec_ManSatStop( p );
+    if ( pnPats )
+        *pnPats = iPat-1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecSweep.c b/src/aig/cec/cecSweep.c
index 20a668bd..3024ac24 100644
--- a/src/aig/cec/cecSweep.c
+++ b/src/aig/cec/cecSweep.c
@@ -83,7 +83,7 @@ Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p )
             (Gia_ObjLevel(p->pAig, pObj)  > p->pPars->nLevelMax || 
              Gia_ObjLevel(p->pAig, pRepr) > p->pPars->nLevelMax) )
             continue;
-        if ( p->pPars->fDoubleOuts )
+        if ( p->pPars->fDualOut )
         {
 //            if ( i % 1000 == 0 && Gia_ObjRepr(p->pAig, i) )
 //                Gia_ManEquivPrintOne( p->pAig, Gia_ObjRepr(p->pAig, i), 0 );
diff --git a/src/aig/cec/module.make b/src/aig/cec/module.make
index 4618c424..1fc9861c 100644
--- a/src/aig/cec/module.make
+++ b/src/aig/cec/module.make
@@ -4,6 +4,7 @@ SRC +=    src/aig/cec/cecCec.c \
     src/aig/cec/cecIso.c \
     src/aig/cec/cecMan.c \
     src/aig/cec/cecPat.c \
+    src/aig/cec/cecSeq.c \
     src/aig/cec/cecSim.c \
     src/aig/cec/cecSolve.c \
     src/aig/cec/cecSweep.c