Version abc80517

7 files changed, 511 insertions, 18 deletions

diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index ea122bbf..50d6db49 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigCone.c \
+    src/aig/saig/saigHaig.c \
     src/aig/saig/saigInter.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigPhase.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index c8efab40..8ec680b8 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -79,6 +79,8 @@ static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
+/*=== saigHaig.c ==========================================================*/
+extern void              Saig_ManHaigRecord( Aig_Man_t * p );
 /*=== saigIoa.c ==========================================================*/
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 952094ce..2d5af2d3 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -145,11 +145,11 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
         {
             pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
             Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
-            if ( Counter >= nSizeMax )
-            {
-                Aig_ManCleanup( pFrames );
-                return pFrames;
-            }
+        }
+        if ( Counter >= nSizeMax )
+        {
+            Aig_ManCleanup( pFrames );
+            return pFrames;
         }
         if ( f == nFrames - 1 )
             break;
@@ -201,6 +201,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
             Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
         PRT( "Time", clock() - clk );
+        fflush( stdout );
     }
     // rewrite the timeframes
     if ( fRewrite )
@@ -214,6 +215,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                 Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
             PRT( "Time", clock() - clk );
+            fflush( stdout );
         }
     }
     // create the SAT solver
@@ -230,15 +232,20 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     {
         printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
         PRT( "Time", clock() - clk );
+        fflush( stdout );
     }
     status = sat_solver_simplify(pSat);
     if ( status == 0 )
     {
         if ( fVerbose )
+        {
             printf( "The BMC problem is trivially UNSAT\n" );
+            fflush( stdout );
+        }
     }
     else
     {
+        int clkPart = clock();
         Aig_ManForEachPo( pFrames, pObj, i )
         {
             Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
@@ -247,12 +254,14 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                     i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
             clk = clock();
             status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( fVerbose )
+            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
             {
-                printf( "Solved  output %2d of frame %3d.  ", 
-                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+                printf( "Solved %2d outputs of frame %3d.  ", 
+                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                 printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
-                PRT( "Time", clock() - clk );
+                PRT( "Time", clock() - clkPart );
+                clkPart = clock();
+                fflush( stdout );
             }
             if ( status == l_False )
             {
@@ -272,7 +281,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             }
             else
             {
-                *piFrame = i;
+                *piFrame = i / Saig_ManPoNum(pAig);
                 RetValue = -1;
                 break;
             }
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
new file mode 100644
index 00000000..64f4e943
--- /dev/null
+++ b/src/aig/saig/saigHaig.c
@@ -0,0 +1,472 @@
+/**CFile****************************************************************
+
+  FileName    [saigHaig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Experiments with history AIG recording.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "satSolver.h"
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+    // skip nodes without representative
+    pObjRepr = pObj->pHaig;
+    if ( pObjRepr == NULL )
+        return;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = pObj->pData;
+    // get the new node of the representative
+    pObjReprNew = pObjRepr->pData;
+    // if this is the same node, no need to add constraints
+    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+        return;
+    // these are different nodes - perform speculative reduction
+    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+    // set the new node
+    pObj->pData = pObjNew2;
+    // add the constraint
+    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
+    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+    assert( Aig_ObjPhaseReal(pMiter) == 1 );
+    Aig_ObjCreatePo( pFrames, pMiter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f, nAssumptions = 0;
+    assert( nFrames == 1 || nFrames == 2 );
+    assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
+    // start AIG manager for timeframes
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pHaig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
+    // map the constant node
+    Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pHaig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+    // add timeframes
+    Aig_ManSetPioNumbers( pHaig );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Aig_ManForEachObj( pHaig, pObj, i )
+        {
+            if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) )
+                continue;
+            if ( Saig_ObjIsPi(pHaig, pObj) )
+            {
+                pObj->pData = Aig_ObjCreatePi( pFrames );
+                continue;
+            }
+            if ( Saig_ObjIsLo(pHaig, pObj) )
+            {
+                Aig_ManHaigSpeculate( pFrames, pObj );
+                continue;
+            }
+            if ( Aig_ObjIsNode(pObj) )
+            {
+                pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+                Aig_ManHaigSpeculate( pFrames, pObj );
+                continue;
+            }
+            assert( 0 );
+        }
+        if ( f == nFrames - 2 )
+            nAssumptions = Aig_ManPoNum(pFrames);
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pHaig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pHaig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    Aig_ManCleanup( pFrames );
+    pFrames->nAsserts = Aig_ManPoNum(pFrames) - nAssumptions;
+    Aig_ManSetRegNum( pFrames, 0 );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+    int nBTLimit = 0;
+    Aig_Man_t * pFrames;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int i, Lit, RetValue, Counter;
+    int clk = clock();
+
+    // create time frames with speculative reduction and convert them into CNF
+clk = clock();
+    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
+Aig_ManShow( pFrames, 0, NULL ); 
+
+    printf( "AIG:    " );
+    Aig_ManPrintStats( pAig );
+    printf( "HAIG:   " );
+    Aig_ManPrintStats( pHaig );
+    printf( "Frames: " );
+    Aig_ManPrintStats( pFrames );
+    printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n", 
+        Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts );
+    pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts );
+PRT( "Preparation", clock() - clk );
+
+//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+    // create the SAT solver to be used for this problem
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat == NULL )
+    {
+        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+        return -1;
+    }
+    
+    // solve each output
+clk = clock();
+    if ( pFrames->nAsserts == 0 )
+    {
+        RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue != l_False )
+            printf( "SAT solver is wrong\n" );
+    }
+    else
+    {
+        Counter = 0;
+        Aig_ManForEachPo( pFrames, pObj, i )
+        {
+            if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+                continue;
+            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
+            RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+        }
+PRT( "Solving    ", clock() - clk );
+        if ( Counter )
+            printf( "Verification failed for %d classes.\n", Counter );
+        else
+            printf( "Verification is successful.\n" );
+    }
+
+    // clean up
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+    int nBTLimit = 0;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj, * pRepr;
+    int i, RetValue, Counter, Lits[2];
+    int nClasses = 0;
+    int clk = clock();
+
+    assert( nFrames == 1 || nFrames == 2 );
+
+clk = clock();
+    pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
+    // create the SAT solver to be used for this problem
+    pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
+    if ( pSat == NULL )
+    {
+        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+        return -1;
+    }
+
+    if ( nFrames == 2 )
+    {
+        // add clauses for the first frame
+        Aig_ManForEachObj( pHaig, pObj, i )
+        {
+            pRepr = pObj->pHaig;
+            if ( pRepr == NULL )
+                continue;
+            if ( pRepr->fPhase ^ pObj->fPhase )
+            {
+                Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+                Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+                Lits[0]++;
+                Lits[1]++;
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+            }
+            else
+            {
+                Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+                Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+                Lits[0]++;
+                Lits[1]--;
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+            }
+        }
+
+        // add clauses for the next timeframe
+        { 
+            int nLitsAll = 2 * pCnf->nVars;
+            int * pLits = pCnf->pClauses[0];
+            for ( i = 0; i < pCnf->nLiterals; i++ )
+                pLits[i] += nLitsAll;
+        }
+    }
+PRT( "Preparation", clock() - clk );
+
+
+    // check in the second timeframe
+clk = clock();
+    Counter = 0;
+    nClasses = 0;
+    Aig_ManForEachObj( pHaig, pObj, i )
+    {
+        pRepr = pObj->pHaig;
+        if ( pRepr == NULL )
+            continue;
+        nClasses++;
+        if ( pRepr->fPhase ^ pObj->fPhase )
+        {
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+
+            Lits[0]++;
+            Lits[1]++;
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+        }
+        else
+        {
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+
+            Lits[0]++;
+            Lits[1]--;
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+        }
+    }
+PRT( "Solving    ", clock() - clk );
+    if ( Counter )
+        printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses );
+    else
+        printf( "Verification is successful for all %d classes.\n", nClasses );
+
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManHaigRecord( Aig_Man_t * p )
+{
+    extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
+    int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 );
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Aig_Man_t * pNew, * pTemp;
+    Aig_Obj_t * pObj;
+    int i;
+    Dar_ManDefaultRwrParams( pParsRwr );
+    // duplicate this manager
+    pNew = Aig_ManDupSimple( p );
+
+    // create its history AIG
+    pNew->pManHaig = Aig_ManDupSimple( pNew );
+    Aig_ManForEachObj( pNew, pObj, i )
+        pObj->pHaig = pObj->pData;
+    // remove structural hashing table
+    Aig_TableClear( pNew->pManHaig );
+
+    // perform retiming
+    if ( fUseRetiming )
+    {
+/*
+        // perform balancing
+        pNew = Dar_ManBalance( pTemp = pNew, 0 );
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+
+        // perform rewriting
+        Dar_ManRewrite( pNew, pParsRwr );
+        pNew = Aig_ManDupDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+*/
+        // perform retiming
+        Saig_ManRetimeSteps( pNew, 1000, 1 ); 
+        pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+
+        // perform balancing
+        pNew = Dar_ManBalance( pTemp = pNew, 0 );
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+
+        // perform rewriting
+        Dar_ManRewrite( pNew, pParsRwr );
+        pNew = Aig_ManDupDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+    }
+    else
+    {
+        // perform balancing
+        pNew = Dar_ManBalance( pTemp = pNew, 0 );
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+/*
+        // perform rewriting
+        Dar_ManRewrite( pNew, pParsRwr );
+        pNew = Aig_ManDupDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+*/
+    } 
+
+    // use the haig for verification
+    Aig_ManAntiCleanup( pNew->pManHaig );
+    Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
+//Aig_ManShow( pNew->pManHaig, 0, NULL ); 
+
+    printf( "AIG:    " );
+    Aig_ManPrintStats( pNew );
+    printf( "HAIG:   " );
+    Aig_ManPrintStats( pNew->pManHaig );
+
+    if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) )
+        printf( "Constructing SAT solver has failed.\n" );         
+
+    // cleanup
+    Aig_ManStop( pNew->pManHaig );
+    pNew->pManHaig = NULL;
+    Aig_ManStop( pNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index f19a27b6..323a230f 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -885,7 +885,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
         pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
     Saig_TsiStop( pTsi );
     if ( pNew == NULL )
-        pNew = Aig_ManDup( p );
+        pNew = Aig_ManDupSimple( p );
     return pNew;
 }
 
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 3935db6c..0ad6c314 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -622,7 +622,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     Vec_Ptr_t * vCut;
     Aig_Man_t * pNew, * pTemp, * pCopy;
     int i, fChanges;
-    pNew = Aig_ManDup( p );
+    pNew = Aig_ManDupSimple( p );
     // perform several iterations of forward retiming
     fChanges = 0;
     if ( !fBackwardOnly )
@@ -672,7 +672,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     {
         if ( Saig_ManRegNum(pNew) == 0 )
             break;
-        pCopy = Aig_ManDup( pNew );
+        pCopy = Aig_ManDupSimple( pNew );
         pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
         Aig_ManStop( pCopy );
         if ( pTemp == NULL )
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index e7ec3c08..f7c27a93 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -44,6 +44,7 @@ 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;
+    int fCompl;
 
     assert( Saig_ManRegNum(p) > 0 );
     assert( Aig_ObjIsNode(pObj) );
@@ -68,22 +69,26 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
     pInput1 = Aig_ObjChild0( pInput1 );
     pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
     pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) );
+    // get the condition when the register should be complemetned
+    fCompl = Aig_ObjFaninC0(pObj) && 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 = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) );
     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++;
 
+//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", 
+//       pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
+
     // return register output
-    return Aig_NotCond( pObjLo, pObjNew->fPhase );
+    return Aig_NotCond( pObjLo, fCompl );
 }
 
 /**Function*************************************************************
@@ -163,6 +168,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
     int RetValue, s, i;
     Aig_ManSetPioNumbers( p );
     Aig_ManFanoutStart( p );
+    p->fCreatePios = 1;
     if ( fForward )
     {
         for ( s = 0; s < nSteps; s++ )
@@ -172,7 +178,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
                 pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
                 if ( pObjNew == NULL )
                     continue;
-                Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+                Aig_ObjReplace( p, pObj, pObjNew, 0 );
                 break;
             }
         }
@@ -186,13 +192,16 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
                 pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
                 if ( pObjNew == NULL )
                     continue;
-                Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+                Aig_ObjReplace( p, pObj, pObjNew, 0 );
                 break;
             }
         }
     }
+    p->fCreatePios = 0;
+    Aig_ManFanoutStop( p );
     RetValue = Aig_ManCleanup( p );
     assert( RetValue == 0 );
+    Aig_ManSetRegNum( p, p->nRegs ); 
 }
 
 ////////////////////////////////////////////////////////////////////////