Version abc71002

14 files changed, 726 insertions, 121 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 096e04e7..313406c7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -139,6 +139,7 @@ struct Aig_Man_t_
     Aig_TMan_t *     pManTime;       // the timing manager
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
+    void *           pSeqModel;
     // timing statistics
     int              time1;
     int              time2;
@@ -175,6 +176,14 @@ static inline int          Aig_WordCountOnes( unsigned uWord )
     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
     return  (uWord & 0x0000FFFF) + (uWord>>16);
 }
+static inline int          Aig_WordFindFirstBit( unsigned uWord )
+{
+    int i;
+    for ( i = 0; i < 32; i++ )
+        if ( uWord & (1 << i) )
+            return i;
+    return -1;
+}
 
 static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
 static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((unsigned long)(p) ^  01); }
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index fed6aebd..71ec389e 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -251,6 +251,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
     if ( p->vLevels )  Vec_VecFree( p->vLevels );
     if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
+    FREE( p->pSeqModel );
     FREE( p->pName );
     FREE( p->pObjCopies );
     FREE( p->pReprs );
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 45a3efad..a46069e6 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -324,8 +324,8 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
   Synopsis    [Derives a simple CNF for the AIG.]
 
   Description [The last argument shows the number of last outputs
-  of the manager, which will not be converted into clauses but the
-  new variables for which will be introduced.]
+  of the manager, which will not be converted into clauses. 
+  New variables will be introduced for these outputs.]
                
   SideEffects []
 
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 0de803ed..8cd677d1 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -53,6 +53,7 @@ typedef struct Fra_Par_t_   Fra_Par_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
+typedef struct Fra_Cex_t_   Fra_Cex_t;
 typedef struct Fra_Bmc_t_   Fra_Bmc_t;
 
 // FRAIG parameters
@@ -118,6 +119,17 @@ struct Fra_Sml_t_
     unsigned         pData[0];          // simulation data for the nodes
 };
 
+// simulation manager
+struct Fra_Cex_t_
+{
+    int              iPo;               // the zero-based number of PO, for which verification failed
+    int              iFrame;            // the zero-based number of the time-frame, for which verificaiton failed
+    int              nRegs;             // the number of registers in the miter 
+    int              nPis;              // the number of primary inputs in the miter
+    int              nBits;             // the number of words of bit data used
+    unsigned         pData[0];          // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
+};
+
 // FRAIG manager
 struct Fra_Man_t_
 {
@@ -227,6 +239,7 @@ extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
 extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern void                Fra_BmcStop( Fra_Bmc_t * p );
 extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
+extern void                Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
 /*=== fraClass.c ========================================================*/
 extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
@@ -247,9 +260,10 @@ extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO
 /*=== fraCore.c ========================================================*/
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
+extern int                 Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
 extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
-extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
+extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
 /*=== fraImp.c ========================================================*/
 extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
 extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
@@ -291,7 +305,11 @@ extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrame
 extern void                Fra_SmlStop( Fra_Sml_t * p );
 extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
-
+extern Fra_Cex_t *         Fra_SmlGetCounterExample( Fra_Sml_t * p );
+extern Fra_Cex_t *         Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
+extern void                Fra_SmlFreeCounterExample( Fra_Cex_t * p );
+extern int                 Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
+extern Fra_Cex_t *         Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index eebafaf6..cf026fac 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -213,7 +213,8 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
 void Fra_BmcStop( Fra_Bmc_t * p )
 {
     Aig_ManStop( p->pAigFrames );
-    Aig_ManStop( p->pAigFraig );
+    if ( p->pAigFraig )
+        Aig_ManStop( p->pAigFraig );
     free( p->pObjToFrames );
     free( p->pObjToFraig );
     free( p );
@@ -230,7 +231,7 @@ void Fra_BmcStop( Fra_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
+Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
 {
     Aig_Man_t * pAigFrames;
     Aig_Obj_t * pObj, * pObjNew;
@@ -274,11 +275,20 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
         assert( k == Aig_ManRegNum(p->pAig) );
     }
     free( pLatches );
-    // add POs to all the dangling nodes
-    Aig_ManForEachObj( pAigFrames, pObjNew, i )
-        if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
-            Aig_ObjCreatePo( pAigFrames, pObjNew );
-
+    if ( fKeepPos )
+    {
+        for ( f = 0; f < p->nFramesAll; f++ )
+            Aig_ManForEachPoSeq( p->pAig, pObj, i )
+                Aig_ObjCreatePo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
+        Aig_ManCleanup( pAigFrames );
+    }
+    else
+    {
+        // add POs to all the dangling nodes
+        Aig_ManForEachObj( pAigFrames, pObjNew, i )
+            if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
+                Aig_ObjCreatePo( pAigFrames, pObjNew );
+    }
     // return the new manager
     return pAigFrames;
 }
@@ -301,7 +311,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
     assert( p->pBmc == NULL );
     // derive and fraig the frames
     p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
-    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
+    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
     // if implications are present, configure the AIG manager to check them
     if ( p->pCla->vImps )
     {
@@ -310,7 +320,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
         p->pBmc->vImps = p->pCla->vImps;
         nImpsOld = Vec_IntSize(p->pCla->vImps);
     } 
-    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
+    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
     p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
     p->pBmc->pAigFrames->pObjCopies = NULL;
     // annotate frames nodes with pointers to the manager
@@ -354,6 +364,56 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
     p->pBmc = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs BMC for the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
+{
+    extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
+    Fra_Man_t * pTemp;
+    Fra_Bmc_t * pBmc;
+    Aig_Man_t * pAigTemp;
+    int iOutput;
+    // derive and fraig the frames
+    pBmc = Fra_BmcStart( pAig, 0, nFrames );
+    pTemp = Fra_LcrAigPrepare( pAig );
+    pTemp->pBmc = pBmc;
+    pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
+    if ( fRewrite )
+    {
+        pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
+        Aig_ManStop( pAigTemp );
+    }
+    iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
+    if ( iOutput >= 0 )
+        pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
+    else
+    {
+        pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
+        iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
+        if ( pBmc->pAigFraig->pData )
+        {
+            pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData );
+            FREE( pBmc->pAigFraig->pData );
+        }
+        else if ( iOutput >= 0 )
+            pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
+    }
+    if ( fVerbose )
+        printf( "nFrames = %3d. Aig = %6d. Init frames = %6d. Fraiged init frames = %6d.\n", 
+            nFrames, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pBmc->pAigFrames), pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1 );
+    Fra_BmcStop( pBmc );  
+    free( pTemp );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index ad73501f..7400b3f9 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -58,27 +58,27 @@
 ***********************************************************************/
 int Fra_FraigMiterStatus( Aig_Man_t * p )
 {
-    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t * pObj, * pChild;
     int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
     if ( p->pData )
         return 0;
     Aig_ManForEachPoSeq( p, pObj, i )
     {
-        pObjNew = Aig_ObjChild0(pObj);
+        pChild = Aig_ObjChild0(pObj);
         // check if the output is constant 0
-        if ( pObjNew == Aig_ManConst0(p) )
+        if ( pChild == Aig_ManConst0(p) )
         {
             CountConst0++;
             continue;
         }
         // check if the output is constant 1
-        if ( pObjNew == Aig_ManConst1(p) )
+        if ( pChild == Aig_ManConst1(p) )
         {
             CountNonConst0++;
             continue;
         }
         // check if the output can be not constant 0
-        if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
+        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
         {
             CountNonConst0++;
             continue;
@@ -104,6 +104,37 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Reports the status of the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_FraigMiterAssertedOutput( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pChild;
+    int i;
+    Aig_ManForEachPoSeq( p, pObj, i )
+    {
+        pChild = Aig_ObjChild0(pObj);
+        // check if the output is constant 0
+        if ( pChild == Aig_ManConst0(p) )
+            continue;
+        // check if the output is constant 1
+        if ( pChild == Aig_ManConst1(p) )
+            return i;
+        // check if the output can be not constant 0
+        if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
+            return i;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Write speculative miter for one node.]
 
   Description []
@@ -410,7 +441,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
+Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve )
 {
     Aig_Man_t * pFraig;
     Fra_Par_t Pars, * pPars = &Pars; 
@@ -419,7 +450,7 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
     pPars->fChoicing    = 0;
     pPars->fDoSparse    = 1;
     pPars->fSpeculate   = 0;
-    pPars->fProve       = 0;
+    pPars->fProve       = fProve;
     pPars->fVerbose     = 0;
     pPars->fDontShowBar = 1;
     pFraig = Fra_FraigPerform( pManAig, pPars );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 597dda71..daa789a8 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -159,7 +159,8 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
     int i;
     p = ALLOC( Fra_Man_t, 1 );
     memset( p, 0, sizeof(Fra_Man_t) );
-    Aig_ManForEachPi( pAig, pObj, i )
+//    Aig_ManForEachPi( pAig, pObj, i )
+    Aig_ManForEachObj( pAig, pObj, i )
         pObj->pData = p;
     return p;
 }
@@ -532,6 +533,7 @@ timeSim = clock() - clk2;
     // check if simulation discovered non-constant-0 POs
     if ( fProve && pSml->fNonConstOut )
     {
+        pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
         Fra_SmlStop( pSml );
         return NULL;
     }
@@ -587,7 +589,7 @@ clk2 = clock();
             pAigPart = Fra_LcrCreatePart( p, vPart );
 p->timeTrav += clock() - clk2;
 clk2 = clock();
-            pAigNew  = Fra_FraigEquivence( pAigPart, nConfMax );
+            pAigNew  = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
 p->timeFraig += clock() - clk2;
             Vec_PtrPush( p->vFraigs, pAigNew );
             Aig_ManStop( pAigPart );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 15206a4d..573d3570 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -150,6 +150,7 @@ clk = clock();
     pNew = Aig_ManDup( pTemp = pNew, 1 );
     Aig_ManStop( pTemp );
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
+    p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
     Aig_ManStop( pTemp );
     if ( pNew == NULL )
     {
@@ -169,7 +170,7 @@ PRT( "Time", clock() - clk );
 
     // perform fraiging
 clk = clock();
-    pNew = Fra_FraigEquivence( pTemp = pNew, 100 );
+    pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
     Aig_ManStop( pTemp );
     if ( fVerbose )
     {
@@ -240,6 +241,7 @@ PRT( "Time", clock() - clk );
         }
         if ( pSml->fNonConstOut )
         {
+            p->pSeqModel = Fra_SmlGetCounterExample( pSml );
             Fra_SmlStop( pSml );
             Aig_ManStop( pNew );
             RetValue = 0;
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b77c775a..3e8f2da1 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -252,12 +252,14 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
+void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
 { 
+    Aig_Obj_t * pFanin, * pObjPi;
     unsigned * pSims;
     int i, k, BestPat, * pModel;
     // find the word of the pattern
-    pSims = Fra_ObjSim(p->pSml, pObj->Id);
+    pFanin = Aig_ObjFanin0(pObjPo);
+    pSims = Fra_ObjSim(p->pSml, pFanin->Id);
     for ( i = 0; i < p->pSml->nWordsTotal; i++ )
         if ( pSims[i] )
             break;
@@ -270,12 +272,13 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
-    Aig_ManForEachPi( p->pManAig, pObj, i )
+    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
+    Aig_ManForEachPi( p->pManAig, pObjPi, i )
     {
-        pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObj->Id), BestPat);
+        pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
     }
+    pModel[Aig_ManPiNum(p->pManAig)] = pObjPo->Id;
 //    printf( "\n" );
     // set the model
     assert( p->pManFraig->pData == NULL );
@@ -306,7 +309,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p )
         if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
         {
             // create the counter-example from this pattern
-            Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) );
+            Fra_SmlCheckOutputSavePattern( p, pObj );
             return 1;
         }
     }
@@ -680,6 +683,8 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
     // start the classes
     Fra_SmlInitialize( p->pSml, fInit );
     Fra_SmlSimulateOne( p->pSml );
+    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
+        return;
     Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
 //    Fra_ClassesPrint( p->pCla, 0 );
 if ( fVerbose )
@@ -816,6 +821,244 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
     return p;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
+{
+    Fra_Sml_t * pSml;
+    Aig_Obj_t * pObj;
+    int RetValue, i, k, iBit;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
+    // start a new sequential simulator
+    pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
+    // assign simulation info for the registers
+    iBit = 0;
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+    // assign simulation info for the primary inputs
+    for ( i = 0; i <= p->iFrame; i++ )
+        Aig_ManForEachPiSeq( pAig, pObj, k )
+            Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+    assert( iBit == p->nBits );
+    // run random simulation
+    Fra_SmlSimulateOne( pSml );
+    // check if the given output has failed
+    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
+    Fra_SmlStop( pSml );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
+{
+    Fra_Cex_t * pCex;
+    int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
+    pCex = (Fra_Cex_t *)malloc( sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
+    memset( pCex, 0, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
+    pCex->nRegs  = nRegs;
+    pCex->nPis   = nRealPis;
+    pCex->nBits  = nRegs + nRealPis * nFrames;
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex )
+{
+    free( pCex );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates sequential counter-example from the simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
+{
+    Fra_Cex_t * pCex;
+    Aig_Obj_t * pObj;
+    unsigned * pSims;
+    int iPo, iFrame, iBit, i, k;
+
+    // make sure the simulation manager has it
+    assert( p->fNonConstOut );
+
+    // find the first output that failed
+    iPo = -1;
+    iBit = -1;
+    iFrame = -1;
+    Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
+    {
+        if ( Fra_SmlNodeIsZero(p, pObj) )
+            continue;
+        pSims = Fra_ObjSim( p, pObj->Id );
+        for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
+            if ( pSims[i] )
+            {
+                iFrame = i / p->nWordsFrame;
+                iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
+                break;
+            }
+        break;
+    }
+    assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
+    assert( iFrame < p->nFrames );
+    assert( iBit < 32 * p->nWordsFrame );
+
+    // allocate the counter example
+    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
+    pCex->iPo    = iPo;
+    pCex->iFrame = iFrame;
+
+    // copy the bit data
+    Aig_ManForEachLoSeq( p->pAig, pObj, k )
+    {
+        pSims = Fra_ObjSim( p, pObj->Id );
+        if ( Aig_InfoHasBit( pSims, iBit ) )
+            Aig_InfoSetBit( pCex->pData, k );
+    }
+    for ( i = 0; i <= iFrame; i++ )
+    {
+        Aig_ManForEachPiSeq( p->pAig, pObj, k )
+        {
+            pSims = Fra_ObjSim( p, pObj->Id );
+            if ( Aig_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
+                Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
+        }
+    }
+    // verify the counter example
+    if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) )
+    {
+        printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
+        Fra_SmlFreeCounterExample( pCex );
+        pCex = NULL;
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generates seq counter-example from the combinational one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
+{
+    Fra_Cex_t * pCex;
+    Aig_Obj_t * pObj;
+    int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
+    // get the number of frames
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pFrames) == 0 );
+    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
+    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
+    nFrames = Aig_ManPiNum(pFrames) / nTruePis;
+    assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) );
+    assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) );
+    // find the PO that failed
+    iPo = -1;
+    iFrame = -1;
+    Aig_ManForEachPo( pFrames, pObj, i )
+        if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
+        {
+            iPo = i % nTruePos;
+            iFrame = i / nTruePos;
+            break;
+        }
+    assert( iPo >= 0 );
+    // allocate the counter example
+    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
+    pCex->iPo    = iPo;
+    pCex->iFrame = iFrame;
+
+    // copy the bit data
+    for ( i = 0; i < Aig_ManPiNum(pFrames); i++ )
+    {
+        if ( pModel[i] )
+            Aig_InfoSetBit( pCex->pData, pCex->nRegs + i );
+        if ( pCex->nRegs + i == pCex->nBits - 1 )
+            break;
+    }
+
+    // verify the counter example
+    if ( !Fra_SmlRunCounterExample( pAig, pCex ) )
+    {
+        printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
+        Fra_SmlFreeCounterExample( pCex );
+        pCex = NULL;
+    }
+    return pCex;
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
+{
+    Fra_Cex_t * pCex;
+    int nTruePis, nTruePos, iPo, iFrame;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
+    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
+    iPo = iFrameOut % nTruePos;
+    iFrame = iFrameOut / nTruePos;
+    // allocate the counter example
+    pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
+    pCex->iPo    = iPo;
+    pCex->iFrame = iFrame;
+    return pCex;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f7739b91..11161698 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -197,6 +197,7 @@ struct Abc_Ntk_t_
     Vec_Int_t *       vLevelsR;      // level in the reverse topological order (for AIGs)
     Vec_Ptr_t *       vSupps;        // CO support information
     int *             pModel;        // counter-example (for miters)
+    void *            pSeqModel;     // counter-example (for sequential miters)
     Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index adaaf7be..d78a3a6a 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -979,7 +979,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     Vec_PtrFree( pNtk->vObjs );
     Vec_PtrFree( pNtk->vBoxes );
     if ( pNtk->vLevelsR ) Vec_IntFree( pNtk->vLevelsR );
-    if ( pNtk->pModel ) free( pNtk->pModel );
+    FREE( pNtk->pModel );
+    FREE( pNtk->pSeqModel );
     TotalMemory  = 0;
     TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj)  : 0;
     TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7d9b8be2..3f9ffb40 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -123,11 +123,9 @@ static int Abc_CommandISat           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCSweep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandQbf            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -173,6 +171,7 @@ static int Abc_CommandLcorr          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCycle          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXsim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCec           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -181,7 +180,9 @@ static int Abc_CommandDSec           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -294,10 +295,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "ifraig",        Abc_CommandIFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "dfraig",        Abc_CommandDFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "csweep",        Abc_CommandCSweep,           1 );
-    Cmd_CommandAdd( pAbc, "New AIG",      "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
-    Cmd_CommandAdd( pAbc, "New AIG",      "_bmc",           Abc_CommandBmc,              0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -341,6 +340,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "sim",           Abc_CommandSim,              0 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
@@ -350,7 +350,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
+    Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
+    Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
 
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
@@ -6337,8 +6339,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 //    pNtkRes = Abc_NtkDar( pNtk );
 //    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
-    pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
-//    pNtkRes = NULL;
+//    pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8100,89 +8102,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int nFrames;
-    int fInit;
-    int fVerbose;
-
-    extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    nFrames  = 5;
-    fInit    = 0;
-    fVerbose = 1;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'K':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFrames = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFrames < 0 ) 
-                goto usage;
-            break;
-        case 'i':
-            fInit ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-    if ( Abc_NtkIsStrash(pNtk) )
-        Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
-    else
-    {
-        pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
-        Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
-        Abc_NtkDelete( pNtk );
-    }
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: _bmc [-K num] [-ivh]\n" );
-    fprintf( pErr, "\t         perform bounded model checking\n" );
-    fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames );
-    fprintf( pErr, "\t-i     : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -11659,6 +11578,103 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int nWords;
+    int fVerbose;
+    extern int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames    = 32;
+    nWords     =  8;
+    fVerbose   =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
+
+    FREE( pNtk->pSeqModel );
+    Abc_NtkDarSeqSim( pNtk, nFrames, nWords, fVerbose );        
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: sim [-F num] [-W num] [-vh]\n" );
+    fprintf( pErr, "\t         performs random simulation of the sequentail miter\n" );
+    fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
 
 /**Function*************************************************************
 
@@ -12787,6 +12803,102 @@ usage:
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int nBTLimit;
+    int fRewrite;
+    int fVerbose;
+
+//    extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames  = 5;
+    nBTLimit = 1000000;
+    fRewrite = 0;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCrvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            fRewrite ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+    Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: bmc [-F num] [-C num] [-rvh]\n" );
+    fprintf( pErr, "\t         perform bounded model checking\n" );
+    fprintf( pErr, "\t-F num : number of time frames [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
+    fprintf( pErr, "\t-r     : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index abf79a82..ab8614fb 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1070,6 +1070,44 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    int clk = clock();
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+    // perform verification
+    Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    if ( pNtk->pSeqModel )
+    {
+        Fra_Cex_t * pCex = pNtk->pSeqModel;
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+    }
+    else
+        printf( "No output was asserted after BMC with %d frames. ", nFrames );
+PRT( "Time", clock() - clk );
+    Aig_ManStop( pMan );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pMan;
@@ -1084,6 +1122,12 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo
     assert( pMan->nRegs > 0 );
     // perform verification
     RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+    if ( pNtk->pSeqModel )
+    {
+        Fra_Cex_t * pCex = pNtk->pSeqModel;
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
+    }
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -1238,6 +1282,46 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    Fra_Sml_t * pSml;
+    Fra_Cex_t * pCex;
+    int RetValue, clk = clock();
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
+    if ( pSml->fNonConstOut )
+    {
+        pCex = Fra_SmlGetCounterExample( pSml );
+        if ( pCex )
+            printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ", 
+                nFrames, nWords, pCex->iPo, pCex->iFrame );
+        pNtk->pSeqModel = pCex;
+        RetValue = 1;
+    }
+    else
+    {
+        RetValue = 0;
+        printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+            nFrames, nWords );
+    }
+    PRT( "Time", clock() - clk );
+    Fra_SmlStop( pSml );
+    Aig_ManStop( pMan );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 7a5e4a5d..941ef7a7 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1569,6 +1569,8 @@ usage:
     return 1;
 }
 
+#include "fra.h"
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1617,13 +1619,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the input file name
     pFileName = argv[globalUtilOptind];
 
-    if ( pNtk->pModel == NULL )
+    if ( pNtk->pModel == NULL && pNtk->pSeqModel == NULL )
     {
         fprintf( pAbc->Out, "Counter-example is not available.\n" );
         return 0;
     }
 
     // write the counter-example into the file
+    if ( pNtk->pModel )
     {
         Abc_Obj_t * pObj;
         FILE * pFile = fopen( pFileName, "w" );
@@ -1646,12 +1649,50 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( pFile, "\n" );
         fclose( pFile );
     }
+    else
+    {
+        Fra_Cex_t * pCex = pNtk->pSeqModel;
+        Abc_Obj_t * pObj;
+        FILE * pFile;
+        int i, f;
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( !Abc_LatchIsInit0(pObj) )
+            {
+                fprintf( stdout, "IoCommandWriteCounter(): The init-state should be all-0 for counter-example to work.\n" );
+                fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
+                return 1;
+            }
+
+        pFile = fopen( pFileName, "w" );
+        if ( pFile == NULL )
+        {
+            fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
+            return 1;
+        }
+        if ( fNames )
+        {
+            Abc_NtkForEachLatch( pNtk, pObj, i )
+                fprintf( pFile, "%s@0=%c ", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+            for ( f = 0; f <= pCex->iFrame; f++ )
+                Abc_NtkForEachPi( pNtk, pObj, i )
+                    fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+        }
+        else
+        {
+            Abc_NtkForEachLatch( pNtk, pObj, i )
+                fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
+            for ( i = pCex->nRegs; i < pCex->nBits; i++ )
+                fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) );
+        }
+        fprintf( pFile, "\n" );
+        fclose( pFile );
+    }
 
     return 0;
 
 usage:
     fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
-    fprintf( pAbc->Err, "\t         writes the counter-example derived by \"prove\" or \"sat\"\n" );
+    fprintf( pAbc->Err, "\t         saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
     fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
     fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );