Version abc80527

11 files changed, 408 insertions, 106 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7cb846fa..7549dfca 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -370,8 +370,9 @@ 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 );
+extern int                 Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
+extern int                 Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index a8de5e37..00a35fcd 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -846,44 +846,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
 
 /**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 []
@@ -1082,6 +1044,115 @@ Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
     return pCex;
 }
 
+/**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    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
+{
+    Fra_Sml_t * pSml;
+    Aig_Obj_t * pObj;
+    int RetValue, i, k, iBit;
+    unsigned * pSims;
+    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 );
+        Fra_SmlAssignConst( pSml, pObj, 0, 0 );
+    // assign simulation info for the primary inputs
+    iBit = p->nRegs;
+    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) );
+
+    // write the output file
+    fprintf( pFile, "1\n" );
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Aig_ManForEachLoSeq( pAig, pObj, k )
+        {
+            pSims = Fra_ObjSim(pSml, pObj->Id);
+            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+        }
+        fprintf( pFile, " " );
+        Aig_ManForEachPiSeq( pAig, pObj, k )
+        {
+            pSims = Fra_ObjSim(pSml, pObj->Id);
+            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+        }
+        fprintf( pFile, " " );
+        Aig_ManForEachPoSeq( pAig, pObj, k )
+        {
+            pSims = Fra_ObjSim(pSml, pObj->Id);
+            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+        }
+        fprintf( pFile, " " );
+        Aig_ManForEachLiSeq( pAig, pObj, k )
+        {
+            pSims = Fra_ObjSim(pSml, pObj->Id);
+            fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+        }
+        fprintf( pFile, "\n" );
+    }
+
+    Fra_SmlStop( pSml );
+    return RetValue;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index c5c62433..d5100312 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -123,8 +123,11 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
     }
     // check models
     Ntl_ManForEachModel( pMan, pMod1, i )
+    {
         if ( !Ntl_ModelCheck( pMod1 ) )
             fStatus = 0;
+        break;
+    }
     return fStatus;
 }
 
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 3574b61e..a291f8a0 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -534,6 +534,18 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) );
             break;
         }
+        else if ( !strncmp(pCur, "no_merge", 8) ) 
+        {
+        }
+        else if ( !strncmp(pCur, "attribute", 9) ) 
+        {
+        }
+        else if ( !strncmp(pCur, "input_required", 14) ) 
+        {
+        }
+        else if ( !strncmp(pCur, "output_arrival", 14) ) 
+        {
+        }
         else
         {
             pCur--;
@@ -682,7 +694,8 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
     char * pToken;
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry( vTokens, 0 );
-    assert( !strcmp(pToken, "attrib") );
+    assert( !strncmp(pToken, "attrib", 6) );
+/*
     if ( Vec_PtrSize(vTokens) != 2 )
     {
         sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
@@ -695,6 +708,7 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
         sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
         return 0;
     }
+*/
     return 1;
 }
 
@@ -864,12 +878,28 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
         sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName );
         return 0;
     }
-
+/*
+    // temporary fix for splitting the .subckt line
+    if ( nEquals < Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
+    { 
+        Vec_Ptr_t * vTokens2 = Vec_PtrAlloc( 10 );
+        // get one additional token
+        pToken = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - 1 );
+        for ( ; *pToken; pToken++ );
+        for ( ; *pToken == 0; pToken++ );
+        Ioa_ReadSplitIntoTokensAndClear( vTokens2, pToken, '\0', '=' );
+//        assert( Vec_PtrSize( vTokens2 ) == 2 );
+        Vec_PtrForEachEntry( vTokens2, pToken, i )
+            Vec_PtrPush( vTokens, pToken );
+        nEquals += Vec_PtrSize(vTokens2)/2;
+        Vec_PtrFree( vTokens2 );
+    }
+*/    
     // check if the number of tokens is correct
     if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
     {
-        sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).", 
-            Ioa_ReadGetLine(p->pMan, pToken), nEquals, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
+        sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt %s differs from the sum of PIs and POs of the model (%d).", 
+            Ioa_ReadGetLine(p->pMan, pToken), nEquals, pName, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
         return 0;
     }
 
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 49d3f5ef..67f38758 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -89,6 +89,7 @@ extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
+extern void              Saig_ManMarkAutonomous( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
 /*=== saigRetMin.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 2d5af2d3..32b2d186 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -191,7 +191,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     }
     else
         pFrames = Saig_ManFramesBmc( pAig, nFrames );
-    *piFrame = nFrames;
+    if ( piFrame )
+        *piFrame = nFrames;
     if ( fVerbose )
     {
         printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
@@ -281,7 +282,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             }
             else
             {
-                *piFrame = i / Saig_ManPoNum(pAig);
+                if ( piFrame )
+                    *piFrame = i / Saig_ManPoNum(pAig);
                 RetValue = -1;
                 break;
             }
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index 4250ca79..8a75ae1f 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -195,7 +195,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth )
 {
     int nBTLimit = 0;
     Aig_Man_t * pFrames, * pTemp;
@@ -203,7 +203,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n
     sat_solver * pSat;
     Aig_Obj_t * pObj1, * pObj2;
     int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
-    int clk = clock();
+    int clk = clock(), clkVerif;
 
     nOvers = Aig_ManMapHaigNodes( pHaig );
 
@@ -226,57 +226,6 @@ clk = clock();
 //    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
     pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
 
-/*
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        Aig_Man_t * pTemp, * pHaig2;
-
-        pHaig2 = pAig->pManHaig; 
-        pAig->pManHaig = NULL;
-        pTemp = Aig_ManDupDfs( pAig );
-        pAig->pManHaig = pHaig2;
-
-        Aig_ManSeqCleanup( pTemp );
-
-        pTable = fopen( "stats.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pName );
-        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
-        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-
-        pTable = fopen( "stats2.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pSpec );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
-
-        fprintf( pTable, "%d ", pCnf->nVars );
-        fprintf( pTable, "%d ", pCnf->nClauses );
-        fprintf( pTable, "%d ", pCnf->nLiterals );
-
-        fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-        Aig_ManStop( pTemp );
-    }
-*/
 
 
 //    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
@@ -375,11 +324,66 @@ clk = clock();
     }
     printf( "                                                          \r" );
 PRT( "Solving    ", clock() - clk );
+clkVerif = clock() - clk;
     if ( Counter )
         printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
     else
         printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
 
+    // print the statistic into a file
+    {
+        FILE * pTable;
+        Aig_Man_t * pTemp, * pHaig2;
+
+        pHaig2 = pAig->pManHaig; 
+        pAig->pManHaig = NULL;
+        pTemp = Aig_ManDupDfs( pAig );
+        pAig->pManHaig = pHaig2;
+
+        Aig_ManSeqCleanup( pTemp );
+
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  p->pName );
+        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
+        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
+
+        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
+
+        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
+
+        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
+
+        fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+
+
+        pTable = fopen( "stats2.txt", "a+" );
+        fprintf( pTable, "%s ",  p->pName );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
+
+        fprintf( pTable, "%d ", pCnf->nVars );
+        fprintf( pTable, "%d ", pCnf->nClauses );
+        fprintf( pTable, "%d ", pCnf->nLiterals );
+
+        fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
+        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
+        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
+
+        fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+
+        Aig_ManStop( pTemp );
+    }
+
     // clean up
     Aig_ManStop( pFrames );
     Cnf_DataFree( pCnf );
@@ -617,7 +621,7 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Aig_Man_t * pNew, * pTemp;
     Aig_Obj_t * pObj;
-    int i, k, nStepsReal, clk = clock();
+    int i, k, nStepsReal, clk = clock(), clkSynth;
     Dar_ManDefaultRwrParams( pParsRwr );
 
 clk = clock();
@@ -679,6 +683,7 @@ clk = clock();
         }
     } 
 PRT( "Synthesis time ", clock() - clk );
+clkSynth = clock() - clk;
 
     // use the haig for verification
 //    Aig_ManAntiCleanup( pNew->pManHaig );
@@ -699,7 +704,7 @@ PRT( "Synthesis time ", clock() - clk );
     }
     else
     {
-        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
+        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
             printf( "Constructing SAT solver has failed.\n" );         
     }
 
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index fe726702..e2502761 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -62,6 +62,10 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
     assert( Aig_ObjPioNum(pFanin0) > 0 );
     assert( Aig_ObjPioNum(pFanin1) > 0 );
 
+    // skip latch guns
+    if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) )
+        return NULL;
+
     // get the inputs of these registers
     pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) );
     pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) );
@@ -90,6 +94,9 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
     pObjLo->PioNum = Aig_ManPiNum(p) - 1;
     p->nRegs++;
 
+    // make sure the register is retimable.
+    Aig_ObjSetTravIdCurrent(p, pObjLo);
+
 //printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", 
 //       pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
 
@@ -177,6 +184,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
     p->fCreatePios = 1;
     if ( fForward )
     {
+        Saig_ManMarkAutonomous( p );
         for ( s = 0; s < nSteps; s++ )
         {
             Aig_ManForEachNode( p, pObj, i )
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index b66c3f32..4d543547 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -522,7 +522,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
     int i, k;
 
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
-    assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pNode))  ); 
+    assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && (Abc_AigNodeIsConst(pNode) || Abc_ObjIsCi(pNode)))  ); 
     
     // start the network
     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 39fdb9fb..d9defa1b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14291,9 +14291,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     Fra_SecSetDefaultParams( pSecPar );
-    pSecPar->TimeLimit = 600;
+    pSecPar->TimeLimit = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FTarmfwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14308,6 +14308,17 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pSecPar->nFramesMax < 0 ) 
                 goto usage;
             break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pSecPar->TimeLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pSecPar->TimeLimit < 0 ) 
+                goto usage;
+            break;
         case 'a':
             pSecPar->fPhaseAbstract ^= 1;
             break;
@@ -14350,9 +14361,10 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs inductive sequential equivalence checking\n" );
     fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
+    fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit );
     fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
     fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
     fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
@@ -14459,6 +14471,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform verification
     Abc_NtkDarProve( pNtk, pSecPar );
+
+    // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
+
     return 0;
 
 usage:
@@ -15617,20 +15632,25 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     int c;
     int fMapped;
+    int fTest;
     extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
     extern Aig_Man_t * Ntl_ManExtract( void * p );
     extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
 
     // set defaults
     fMapped = 0;
+    fTest   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mth" ) ) != EOF )
     {
         switch ( c )
         {
         case 'm':
             fMapped ^= 1;
             break;
+        case 't':
+            fTest ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -15650,6 +15670,19 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     fclose( pFile );
 
+    if ( fTest )
+    {
+        extern void Ntl_ManFree( void * p );
+        extern void Ntl_ManPrintStats( void * p );
+        void * pTemp = Ioa_ReadBlif( pFileName, 1 );
+        if ( pTemp )
+        {
+        Ntl_ManPrintStats( pTemp );
+        Ntl_ManFree( pTemp );
+        }
+        return 0;
+    }
+
     Abc_FrameClearDesign(); 
     pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 );
     if ( pAbc->pAbc8Ntl == NULL )
@@ -15672,9 +15705,10 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *r [-mh]\n" );
+    fprintf( stdout, "usage: *r [-mth]\n" );
     fprintf( stdout, "\t        reads the design with whiteboxes\n" );
     fprintf( stdout, "\t-m    : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" );
+    fprintf( stdout, "\t-t    : toggle reading in the test mode [default = %s]\n", fTest? "yes": "no" );
     fprintf( stdout, "\t-h    : print the command usage\n");
     return 1;
 }
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
new file mode 100644
index 00000000..3f6b81a4
--- /dev/null
+++ b/src/base/main/mainMC.c
@@ -0,0 +1,147 @@
+/**CFile****************************************************************
+
+  FileName    [mainMC.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The main package.]
+
+  Synopsis    [The main file for the model checker.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+#include "aig.h"
+#include "saig.h"
+#include "fra.h"
+#include "ioa.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [The main() procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int main( int argc, char * argv[] )
+{
+    Fra_Sec_t SecPar, * pSecPar = &SecPar;
+    FILE * pFile;
+    Aig_Man_t * pAig;
+    int RetValue;
+    // BMC parameters
+    int nFrames  = 30;
+    int nSizeMax = 200000;
+    int nBTLimit = 10000;
+    int fRewrite = 0;
+    int fNewAlgo = 1;
+    int fVerbose = 0;
+
+    if ( argc != 2 )
+    {
+        printf( "  Expecting one command-line argument (an input file in AIGER format).\n" );
+        printf( "  usage: %s <file.aig>", argv[0] );
+        return 0;
+    }
+    pFile = fopen( argv[1], "r" );
+    if ( pFile == NULL )
+    {
+        printf( "  Cannot open input AIGER file \"%s\".\n", argv[1] );
+        printf( "  usage: %s <file.aig>", argv[0] );
+        return 0;
+    }
+    fclose( pFile );
+    pAig = Ioa_ReadAiger( argv[1], 1 );
+    if ( pAig == NULL )
+    {
+        printf( "  Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
+        printf( "  usage: %s <file.aig>", argv[0] );
+        return 0;
+    }
+
+    // perform BMC
+    Aig_ManSetRegNum( pAig, pAig->nRegs );
+    RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
+
+    // perform full-blown SEC
+    if ( RetValue != 0 )
+    {
+        extern void Dar_LibStart();
+        extern void Dar_LibStop();
+        extern void Cnf_ClearMemory();
+
+        Fra_SecSetDefaultParams( pSecPar );
+        pSecPar->nFramesMax      =   2;  // the max number of frames used for induction
+
+        Dar_LibStart();
+        RetValue = Fra_FraigSec( pAig, pSecPar );
+        Dar_LibStop();
+        Cnf_ClearMemory();
+    }
+
+    // perform BMC again
+    if ( RetValue == -1 )
+    {
+    }
+
+    // decide how to report the output
+    pFile = stdout;
+
+    // report the result
+    if ( RetValue == 0 ) 
+    {
+//        fprintf(stdout, "s SATIFIABLE\n");
+        Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
+        if ( pFile != stdout )
+            fclose(pFile);
+        Aig_ManStop( pAig );
+        exit(10);
+    } 
+    else if ( RetValue == 1 ) 
+    {
+//    fprintf(stdout, "s UNSATISFIABLE\n");
+        fprintf( pFile, "0\n" );
+        if ( pFile != stdout )
+            fclose(pFile);
+        Aig_ManStop( pAig );
+        exit(20);
+    } 
+    else // if ( RetValue == -1 ) 
+    {
+//    fprintf(stdout, "s UNKNOWN\n");
+        if ( pFile != stdout )
+            fclose(pFile);
+        Aig_ManStop( pAig );
+        exit(0);
+    }
+    return 0;
+}
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+