Version abc80508

23 files changed, 396 insertions, 37 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 47696a41..6ecec3f8 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -622,6 +622,7 @@ extern void            Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
 extern void            Aig_ManSetPioNumbers( Aig_Man_t * p );
 extern void            Aig_ManCleanPioNumbers( Aig_Man_t * p );
 extern int             Aig_ManCountChoices( Aig_Man_t * p );
+extern unsigned        Aig_ManRandom( int fReset );
 
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index e7623739..9dfa2ddf 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -118,6 +118,8 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nRegs = p->nRegs;
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = p->nTruePos;
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 47ee8d4d..2e68e93c 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -216,7 +216,7 @@ void Aig_ManStop( Aig_Man_t * p )
     FREE( p->pObjCopies );
     FREE( p->pReprs );
     FREE( p->pEquivs );
-    free( p->pTable );
+//    free( p->pTable );
     free( p );
 }
 
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 9c7cf2c4..88fb9c9d 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -361,7 +361,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     // the object to be replaced cannot be complemented
     assert( !Aig_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
-    assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
+//    assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
+    assert( !Aig_ObjIsPo(pObjOld) );
     // the object to be used cannot be a buffer or a PO
     assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) );
     // the object cannot be the same
@@ -371,7 +372,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
-    Aig_ObjDelete_rec( p, pObjOld, 0 );
+    if ( !Aig_ObjIsPi(pObjOld) )
+        Aig_ObjDelete_rec( p, pObjOld, 0 );
     pObjNewR->nRefs--;
     // if the new object is complemented or already used, create a buffer
     p->nObjs[pObjOld->Type]--;
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index d3f78902..7b48a73d 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -53,13 +53,13 @@ static inline int  Aig_XsimAnd( int Value0, int Value1 )
 }
 static inline int  Aig_XsimRand2()   
 {
-    return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
+    return (Aig_ManRandom(0) & 1) ? AIG_XVS1 : AIG_XVS0;
 }
 static inline int  Aig_XsimRand3()   
 {
     int RetValue;
     do { 
-        RetValue = rand() & 3; 
+        RetValue = Aig_ManRandom(0) & 3; 
     } while ( RetValue == 0 );
     return RetValue;
 }
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 00e0311d..a01e9582 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -990,6 +990,94 @@ void Aig_ManPrintControlFanouts( Aig_Man_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates a sequence or random numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [http://en.wikipedia.org/wiki/LFSR]
+
+***********************************************************************/
+void Aig_ManRandomTest2()
+{
+    FILE * pFile;
+    unsigned int lfsr = 1;
+    unsigned int period = 0; 
+    pFile = fopen( "rand.txt", "w" );
+    do {
+//        lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1 
+        lfsr = 1; // to prevent the warning
+        ++period;
+        fprintf( pFile, "%10d : %10d ", period, lfsr );
+//        Extra_PrintBinary( pFile, &lfsr, 32 );
+        fprintf( pFile, "\n" );
+        if ( period == 20000 )
+            break;
+    } while(lfsr != 1u);
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a sequence or random numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
+
+***********************************************************************/
+void Aig_ManRandomTest1()
+{
+    FILE * pFile;
+    unsigned int lfsr;
+    unsigned int period = 0; 
+    pFile = fopen( "rand.txt", "w" );
+    do {
+        lfsr = Aig_ManRandom( 0 );
+        ++period;
+        fprintf( pFile, "%10d : %10d ", period, lfsr );
+//        Extra_PrintBinary( pFile, &lfsr, 32 );
+        fprintf( pFile, "\n" );
+        if ( period == 20000 )
+            break;
+    } while(lfsr != 1u);
+    fclose( pFile );
+}
+
+ 
+#define NUMBER1  3716960521
+#define NUMBER2  2174103536
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a sequence or random numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
+
+***********************************************************************/
+unsigned Aig_ManRandom( int fReset )
+{
+    static unsigned int m_z = NUMBER1;
+    static unsigned int m_w = NUMBER2;
+    if ( fReset )
+    {
+        m_z = NUMBER1;
+        m_w = NUMBER2;
+    }
+    m_z = 36969 * (m_z & 65535) + (m_z >> 16);
+    m_w = 18000 * (m_w & 65535) + (m_w >> 16);
+    return (m_z << 16) + m_w;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
index cfe70d15..234ae3f8 100644
--- a/src/aig/bbr/bbrImage.c
+++ b/src/aig/bbr/bbrImage.c
@@ -89,7 +89,7 @@ struct Bbr_ImageVar_t_
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
-#define BDD_BLOW_UP  1000000
+#define BDD_BLOW_UP  2000000
 
 #define     b0     Cudd_Not((dd)->one)
 #define     b1              (dd)->one
@@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
         if ( pTree->nNodesMax < nNodes )
             pTree->nNodesMax = nNodes;
     }
-    if ( dd->keys > BDD_BLOW_UP )
+    if ( dd->keys-dd->dead > BDD_BLOW_UP )
         return 0;
     return 1;
 }
@@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
     }
 
     *pfStop = 0;
-    if ( dd->keys > BDD_BLOW_UP )
+    if ( dd->keys-dd->dead > BDD_BLOW_UP )
     {
         *pfStop = 1;
         return 0;
diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make
index 52a824b9..07a05869 100644
--- a/src/aig/bbr/module.make
+++ b/src/aig/bbr/module.make
@@ -1,3 +1,3 @@
 SRC +=    src/aig/bbr/bbrImage.c \
     src/aig/bbr/bbrNtbdd.c \
-    src/aig/bdr/bbrReach.c
+    src/aig/bbr/bbrReach.c
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index cf763e67..9a49805b 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -138,6 +138,7 @@ extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
+extern void            Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 2ee66916..934aab1c 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -326,6 +326,30 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
     return pSat;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the OR-clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
+{
+    sat_solver * pSat = p;
+    Aig_Obj_t * pObj;
+    int i, * pLits;
+    pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    Aig_ManForEachPo( pCnf->pMan, pObj, i )
+        pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+    if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+        assert( 0 );
+    free( pLits );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 23b3e8f0..5556ac2e 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -221,9 +221,18 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     Number = 1;
     if ( nOutputs )
     {
-        assert( nOutputs == Aig_ManRegNum(p->pManAig) );
-        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
-            pCnf->pVarNums[pObj->Id] = Number++;
+        if ( Aig_ManRegNum(p->pManAig) == 0 )
+        {
+            assert( nOutputs == Aig_ManPoNum(p->pManAig) );
+            Aig_ManForEachPo( p->pManAig, pObj, i )
+                pCnf->pVarNums[pObj->Id] = Number++;
+        }
+        else
+        {
+            assert( nOutputs == Aig_ManRegNum(p->pManAig) );
+            Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+                pCnf->pVarNums[pObj->Id] = Number++;
+        }
     }
     // assign variables to the internal nodes
     Vec_PtrForEachEntry( vMapped, pObj, i )
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 5c9a144f..07685c98 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -220,7 +220,7 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
 /*
     // we did not find the node to share, randomize choice
     {
-        int Choice = rand() % (RightBound - LeftBound + 1);
+        int Choice = Aig_ManRandom(0) % (RightBound - LeftBound + 1);
         pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
         if ( pObj3 == pObj2 )
             return;
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 44cfe847..7311d414 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -226,7 +226,7 @@ struct Fra_Man_t_
 ////////////////////////////////////////////////////////////////////////
 
 static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
-static inline unsigned     Fra_ObjRandomSim()                                            { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
+static inline unsigned     Fra_ObjRandomSim()                                            { return Aig_ManRandom(0);               }
 
 static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
 static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 05f2493a..e91478a4 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -47,14 +47,16 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     int status, RetValue, clk = clock();
     Vec_Int_t * vCiIds;
 
-    assert( Aig_ManPoNum(pMan) == 1 );
+    assert( Aig_ManRegNum(pMan) == 0 );
     pMan->pData = NULL;
 
     // derive CNF
-    pCnf = Cnf_Derive( pMan, 0 );
-//    pCnf = Cnf_DeriveSimple( pMan, 0 );
+    pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+//    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
     // convert into the SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    // add the OR clause for the outputs
+    Cnf_DataWriteOrClause( pSat, pCnf );
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
     Cnf_DataFree( pCnf );
     // solve SAT
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index c9ea4907..6f0a2012 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -606,7 +606,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
 
     // simulate the AIG
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
     if ( p->fTarget && pSeq->fNonConstOut )
     {
@@ -661,7 +662,8 @@ PRT( "Infoseq", clock() - clk );
 
     // perform combinational simulation
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
 if ( p->fVerbose )
 {
@@ -728,7 +730,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
 
     // simulate the AIG
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
     if ( p->fTarget && pSeq->fNonConstOut )
     {
@@ -743,7 +746,8 @@ if ( p->fVerbose )
 
     // perform combinational simulation
 clk = clock();
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
 if ( p->fVerbose )
 {
@@ -1614,7 +1618,8 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
     int * pStart, * pVar2Id; 
     int clk = clock();
     // simulate the circuit with nCombSimWords * 32 = 64K patterns
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
     // create mapping from SAT vars to node IDs
     pVar2Id = ALLOC( int, p->pCnf->nVars );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 222f5bcc..b2156193 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -333,7 +333,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
 
     // generate random sim-info at register outputs
     vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
-    srand( 0xAABBAABB );
+//    srand( 0xAABBAABB );
+    Aig_ManRandom(1);
     for ( i = 0; i < nRegs; i++ )
     {
         pSim1 = Vec_PtrEntry( vSimInfo, i );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index da7c37a3..b8cf13c5 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -120,7 +120,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
     // set random number generator
-    srand( 0xABCABC );
+//    srand( 0xABCABC );
+    Aig_ManRandom(1);
     // set the pointer to the manager
     Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->pData = p;
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 64222a47..9a500680 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -44,21 +44,20 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
-    Aig_Man_t * pNew = NULL, * pTemp;
+    Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
 
     // try the miter before solving
-    RetValue = Fra_FraigMiterStatus( p );
-    if ( RetValue == 0 || RetValue == 1 )
+    pNew = Aig_ManDup( p );
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue >= 0 )
         goto finish;
 
     // prepare parameters
     memset( pPars, 0, sizeof(Fra_Ssw_t) );
     pPars->fLatchCorr  = fLatchCorr;
     pPars->fVerbose = fVeryVerbose;
-
-    pNew = Aig_ManDup( p );
     if ( fVerbose )
     {
         printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
@@ -78,6 +77,9 @@ clk = clock();
             Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
     }
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue >= 0 )
+        goto finish;
 
     // perform phase abstraction
 clk = clock();
@@ -150,6 +152,13 @@ PRT( "Time", clock() - clk );
     }
     }
 
+    if ( pNew->nRegs == 0 )
+        RetValue = Fra_FraigCec( &pNew, 0 );
+
+    RetValue = Fra_FraigMiterStatus( pNew );
+    if ( RetValue >= 0 )
+        goto finish;
+
     // perform min-area retiming
     if ( fRetimeRegs && pNew->nRegs )
     {
@@ -262,9 +271,7 @@ PRT( "Time", clock() - clkTotal );
         assert( Aig_ManRegNum(pNew) > 0 );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-clk = clock();
         RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
-PRT( "Time", clock() - clk );
     }
 
 finish:
@@ -289,8 +296,7 @@ PRT( "Time", clock() - clkTotal );
         Ioa_WriteAiger( pNew, pFileName, 0, 0 );
         printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
     }
-    if ( pNew )
-        Aig_ManStop( pNew );
+    Aig_ManStop( pNew );
     return RetValue;
 }
 
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 7de3ccdc..c9172024 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -2,4 +2,5 @@ SRC +=    src/aig/saig/saig_.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRetFwd.c \
     src/aig/saig/saigRetMin.c \
+    src/aig/saig/saigRetStep.c \
     src/aig/saig/saigScl.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f9677cb0..7f6bb292 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -82,6 +82,8 @@ extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, in
 /*=== saigRetMin.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
 extern Aig_Man_t *       Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+/*=== saigRetStep.c ==========================================================*/
+extern void              Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
 /*=== saigScl.c ==========================================================*/
 extern void              Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
 
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index f98bb49b..f19a27b6 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -58,13 +58,13 @@ static inline int  Saig_XsimAnd( int Value0, int Value1 )
 }
 static inline int  Saig_XsimRand2()   
 {
-    return (rand() & 1) ? SAIG_XVS1 : SAIG_XVS0;
+    return (Aig_ManRandom(0) & 1) ? SAIG_XVS1 : SAIG_XVS0;
 }
 static inline int  Saig_XsimRand3()   
 {
     int RetValue;
     do { 
-        RetValue = rand() & 3; 
+        RetValue = Aig_ManRandom(0) & 3; 
     } while ( RetValue == 0 );
     return RetValue;
 }
@@ -601,11 +601,11 @@ void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
 ***********************************************************************/
 int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
 {
-    int Values[256];
+    int Values[257];
     unsigned * pState;
     int r, i, k, Reg, Value;
     int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
-    assert( nFrames < 256 );
+    assert( nFrames <= 256 );
     r = 0;
     Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
     {
@@ -800,6 +800,8 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
         printf( "Print-out finished. Phase assignment is not performed.\n" );
     else if ( nFrames < 2 )
         printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
+    else if ( nFrames > 256 )
+        printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
     else if ( pTsi->nCycle == 1 )
         printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
     else if ( pTsi->nCycle % nFrames != 0 )
@@ -859,6 +861,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
     {
 //        printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
     }
+    else if ( nFrames > 256 )
+    {
+//        printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
+    }
     else if ( pTsi->nCycle == 1 )
     {
 //        printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 324d8867..3935db6c 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -628,6 +628,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     if ( !fBackwardOnly )
     for ( i = 0; i < nMaxIters; i++ )
     {
+        if ( Saig_ManRegNum(pNew) == 0 )
+            break;
         vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
         if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
         {
@@ -648,6 +650,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     if ( !fForwardOnly && !fInitial )
     for ( i = 0; i < nMaxIters; i++ )
     {
+        if ( Saig_ManRegNum(pNew) == 0 )
+            break;
         vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
         if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
         {
@@ -666,6 +670,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     else if ( !fForwardOnly && fInitial )
     for ( i = 0; i < nMaxIters; i++ )
     {
+        if ( Saig_ManRegNum(pNew) == 0 )
+            break;
         pCopy = Aig_ManDup( pNew );
         pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
         Aig_ManStop( pCopy );
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
new file mode 100644
index 00000000..e7ec3c08
--- /dev/null
+++ b/src/aig/saig/saigRetStep.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+  FileName    [saigRetStep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Implementation of retiming steps.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigRetStep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one retiming step forward.]
+
+  Description [Returns the pointer to the register output after retiming.]
+               
+  SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanin0, * pFanin1;
+    Aig_Obj_t * pInput0, * pInput1;
+    Aig_Obj_t * pObjNew, * pObjLi, * pObjLo;
+
+    assert( Saig_ManRegNum(p) > 0 );
+    assert( Aig_ObjIsNode(pObj) );
+
+    // get the fanins
+    pFanin0 = Aig_ObjFanin0(pObj);
+    pFanin1 = Aig_ObjFanin1(pObj);
+    // skip of they are not primary inputs
+    if ( !Aig_ObjIsPi(pFanin0) || !Aig_ObjIsPi(pFanin1) )
+        return NULL;
+
+    // skip of they are not register outputs
+    if ( !Saig_ObjIsLo(p, pFanin0) || !Saig_ObjIsLo(p, pFanin1) )
+        return NULL;
+    assert( Aig_ObjPioNum(pFanin0) > 0 );
+    assert( Aig_ObjPioNum(pFanin1) > 0 );
+
+    // 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) );
+    pInput0 = Aig_ObjChild0( pInput0 );
+    pInput1 = Aig_ObjChild0( pInput1 );
+    pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
+    pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) );
+
+    // create new node
+    pObjNew = Aig_And( p, pInput0, pInput1 );
+
+    // create new register input
+    pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, pObjNew->fPhase) );
+    pObjLi->PioNum = Aig_ManPoNum(p) - 1;
+    assert( pObjLi->fPhase == 0 );
+
+    // create new register output
+    pObjLo = Aig_ObjCreatePi( p );
+    pObjLo->PioNum = Aig_ManPiNum(p) - 1;
+    p->nRegs++;
+
+    // return register output
+    return Aig_NotCond( pObjLo, pObjNew->fPhase );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one retiming step backward.]
+
+  Description [Returns the pointer to node after retiming.]
+               
+  SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
+{
+    Aig_Obj_t * pFanin0, * pFanin1;
+    Aig_Obj_t * pLo0New, * pLo1New;
+    Aig_Obj_t * pLi0New, * pLi1New;
+    Aig_Obj_t * pObj, * pObjNew, * pObjLi;
+    int fCompl0, fCompl1;
+
+    assert( Saig_ManRegNum(p) > 0 );
+    assert( Aig_ObjPioNum(pObjLo) > 0 );
+    assert( Saig_ObjIsLo(p, pObjLo) );
+
+    // get the corresponding latch input
+    pObjLi = Saig_ManLi( p, Aig_ObjPioNum(pObjLo) - Saig_ManPiNum(p) );
+
+    // get the node
+    pObj = Aig_ObjFanin0(pObjLi);
+    if ( !Aig_ObjIsNode(pObj) )
+        return NULL;
+
+    // get the fanins
+    pFanin0 = Aig_ObjFanin0(pObj);
+    pFanin1 = Aig_ObjFanin1(pObj);
+
+    // get the complemented attributes of the fanins
+    fCompl0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFaninC0(pObjLi);
+    fCompl1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFaninC0(pObjLi);
+
+    // create latch inputs
+    pLi0New = Aig_ObjCreatePo( p, Aig_NotCond(pFanin0, fCompl0) );
+    pLi0New->PioNum = Aig_ManPoNum(p) - 1;
+    pLi1New = Aig_ObjCreatePo( p, Aig_NotCond(pFanin1, fCompl1) );
+    pLi1New->PioNum = Aig_ManPoNum(p) - 1;
+
+    // create latch outputs
+    pLo0New = Aig_ObjCreatePi(p);
+    pLo0New->PioNum = Aig_ManPiNum(p) - 1;
+    pLo1New = Aig_ObjCreatePi(p);
+    pLo1New->PioNum = Aig_ManPiNum(p) - 1;
+    pLo0New = Aig_NotCond( pLo0New, fCompl0 );
+    pLo1New = Aig_NotCond( pLo1New, fCompl1 );
+    p->nRegs += 2;
+
+    // create node
+    pObjNew = Aig_And( p, pLo0New, pLo1New );
+//    assert( pObjNew->fPhase == 0 );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs the given number of retiming steps.]
+
+  Description [Returns the pointer to node after retiming.]
+               
+  SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.]
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
+{
+    Aig_Obj_t * pObj, * pObjNew;
+    int RetValue, s, i;
+    Aig_ManSetPioNumbers( p );
+    Aig_ManFanoutStart( p );
+    if ( fForward )
+    {
+        for ( s = 0; s < nSteps; s++ )
+        {
+            Aig_ManForEachNode( p, pObj, i )
+            {
+                pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
+                if ( pObjNew == NULL )
+                    continue;
+                Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+                break;
+            }
+        }
+    }
+    else
+    {
+        for ( s = 0; s < nSteps; s++ )
+        {
+            Saig_ManForEachLo( p, pObj, i )
+            {
+                pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
+                if ( pObjNew == NULL )
+                    continue;
+                Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+                break;
+            }
+        }
+    }
+    RetValue = Aig_ManCleanup( p );
+    assert( RetValue == 0 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+