Backward reachability using circuit cofactoring.

3 files changed, 250 insertions, 217 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c652f1a0..d97276f5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -174,6 +174,7 @@ struct Gia_ParFra_t_
 {
     int            nFrames;       // the number of frames to unroll
     int            fInit;         // initialize the timeframes
+    int            fSaveLastLit;  // adds POs for outputs of each frame
     int            fVerbose;      // enables verbose output
 };
 
@@ -700,6 +701,10 @@ extern void                Gia_ManFanoutStop( Gia_Man_t * p );
 /*=== giaForce.c =========================================================*/
 extern void                For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose );
 /*=== giaFrames.c =========================================================*/
+extern void *              Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
+extern void *              Gia_ManUnrollAdd( void * pMan, int fMax );
+extern void                Gia_ManUnrollStop( void * pMan );
+extern int                 Gia_ManUnrollLastLit( void * pMan );
 extern void                Gia_ManFraSetDefaultParams( Gia_ParFra_t * p );
 extern Gia_Man_t *         Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars );  
 /*=== giaFront.c ==========================================================*/
diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c
index 5819ee92..7a346030 100644
--- a/src/aig/gia/giaCCof.c
+++ b/src/aig/gia/giaCCof.c
@@ -32,131 +32,22 @@ typedef struct Ccf_Man_t_ Ccf_Man_t; // manager
 struct Ccf_Man_t_
 {
     // user data
-    Gia_Man_t *   pGia;         // single output AIG manager
-    int           nFrameMax;    // maximum number of frames
-    int           nConfMax;     // maximum number of conflicts
-    int           nTimeMax;     // maximum runtime in seconds
-    int           fVerbose;     // verbose flag
+    Gia_Man_t *  pGia;       // single-output AIG manager
+    int          nFrameMax;  // maximum number of frames
+    int          nConfMax;   // maximum number of conflicts
+    int          nTimeMax;   // maximum runtime in seconds
+    int          fVerbose;   // verbose flag
     // internal data
-    sat_solver *  pSat;         // SAT solver
-    Gia_Man_t *   pFrames;      // unrolled timeframes
-    Vec_Int_t *   vIdToFra;     // maps GIA obj IDs into frame obj IDs
-    Vec_Int_t *   vOrder;       // map Num to Id
-    Vec_Int_t *   vFraLims;     // frame limits
+    void *       pUnr;       // unrolling manager
+    Gia_Man_t *  pFrames;    // unrolled timeframes
+    Vec_Int_t *  vCopies;    // copy pointers of the AIG
+    sat_solver * pSat;       // SAT solver
 };
 
-extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots );
-
-static inline int  Gia_ObjFrames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj )             { assert( Vec_IntEntry(p->vIdToFra, f*Gia_ManObjNum(p->pGia)+Gia_ObjId(p->pGia,pObj)) >= 0 ); return Vec_IntEntry(p->vIdToFra, f*Gia_ManObjNum(p->pGia)+Gia_ObjId(p->pGia,pObj));     }
-static inline void Gia_ObjSetFrames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj, int Lit ) { Vec_IntWriteEntry(p->vIdToFra, f*Gia_ManObjNum(p->pGia)+Gia_ObjId(p->pGia,pObj), Lit);  }
-
-static inline int  Gia_ObjChild0Frames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj )       { return Gia_LitNotCond(Gia_ObjFrames(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
-static inline int  Gia_ObjChild1Frames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj )       { return Gia_LitNotCond(Gia_ObjFrames(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
-{
-    lit Lits[1];
-    int Cid;
-    assert( iVar >= 0 );
-
-    Lits[0] = toLitCond( iVar, fCompl );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 1 );
-    assert( Cid );
-    return 1;
-}
-static inline int sat_solver_add_buffer( sat_solver * pSat, int iVarA, int iVarB, int fCompl )
-{
-    lit Lits[2];
-    int Cid;
-    assert( iVarA >= 0 && iVarB >= 0 );
-
-    Lits[0] = toLitCond( iVarA, 0 );
-    Lits[1] = toLitCond( iVarB, !fCompl );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVarA, 1 );
-    Lits[1] = toLitCond( iVarB, fCompl );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
-    assert( Cid );
-    return 2;
-}
-static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
-{
-    lit Lits[3];
-    int Cid;
-
-    Lits[0] = toLitCond( iVar, 1 );
-    Lits[1] = toLitCond( iVar0, fCompl0 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVar, 1 );
-    Lits[1] = toLitCond( iVar1, fCompl1 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVar, 0 );
-    Lits[1] = toLitCond( iVar0, !fCompl0 );
-    Lits[2] = toLitCond( iVar1, !fCompl1 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
-    assert( Cid );
-    return 3;
-}
-static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
-{
-    lit Lits[3];
-    int Cid;
-    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
-
-    Lits[0] = toLitCond( iVarA, !fCompl );
-    Lits[1] = toLitCond( iVarB, 1 );
-    Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVarA, !fCompl );
-    Lits[1] = toLitCond( iVarB, 0 );
-    Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVarA, fCompl );
-    Lits[1] = toLitCond( iVarB, 1 );
-    Lits[2] = toLitCond( iVarC, 0 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVarA, fCompl );
-    Lits[1] = toLitCond( iVarB, 0 );
-    Lits[2] = toLitCond( iVarC, 1 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
-    assert( Cid );
-    return 4;
-}
-static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int fCompl )
-{
-    lit Lits[2];
-    int Cid;
-    assert( iVar >= 0 );
-
-    Lits[0] = toLitCond( iVar, fCompl );
-    Lits[1] = toLitCond( iVar+1, 0 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
-    assert( Cid );
-
-    Lits[0] = toLitCond( iVar, fCompl );
-    Lits[1] = toLitCond( iVar+1, 1 );
-    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
-    assert( Cid );
-    return 2;
-}
-
-
 /**Function*************************************************************
 
   Synopsis    [Create manager.]
@@ -170,21 +61,25 @@ static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int fC
 ***********************************************************************/
 Ccf_Man_t * Ccf_ManStart( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose )
 {
+    static Gia_ParFra_t Pars, * pPars = &Pars;
     Ccf_Man_t * p;
     assert( nFrameMax > 0 );
     p = ABC_CALLOC( Ccf_Man_t, 1 );
-    p->pGia       = pGia;
-    p->nFrameMax  = nFrameMax;    
-    p->nConfMax   = nConfMax;
-    p->nTimeMax   = nTimeMax;
-    p->fVerbose   = fVerbose;
+    p->pGia      = pGia;
+    p->nFrameMax = nFrameMax;    
+    p->nConfMax  = nConfMax;
+    p->nTimeMax  = nTimeMax;
+    p->fVerbose  = fVerbose;
+    // create unrolling manager
+    memset( pPars, 0, sizeof(Gia_ParFra_t) );
+    pPars->fVerbose     = fVerbose;
+    pPars->nFrames      = nFrameMax;
+    pPars->fSaveLastLit = 1;
+    p->pUnr = Gia_ManUnrollStart( pGia, pPars );
+    p->vCopies = Vec_IntAlloc( 1000 );
     // internal data
-    p->pFrames    = Gia_ManStart( 10000 );
-    Gia_ManHashAlloc( p->pFrames );
-    p->vOrder     = Gia_VtaCollect( pGia, &p->vFraLims, NULL );
-    p->vIdToFra   = Vec_IntAlloc( 0 );
-    p->pSat       = sat_solver_new();
-    sat_solver_setnvars( p->pSat, 10000 );
+    p->pSat = sat_solver_new();
+//    sat_solver_setnvars( p->pSat, 10000 );
     return p;
 }
 
@@ -201,9 +96,8 @@ Ccf_Man_t * Ccf_ManStart( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTi
 ***********************************************************************/
 void Ccf_ManStop( Ccf_Man_t * p )
 {
-    Vec_IntFreeP( &p->vIdToFra );
-    Vec_IntFreeP( &p->vOrder );
-    Vec_IntFreeP( &p->vFraLims );
+    Vec_IntFree( p->vCopies );
+    Gia_ManUnrollStop( p->pUnr );
     sat_solver_delete( p->pSat );
     Gia_ManStopP( &p->pFrames );
     ABC_FREE( p );
@@ -228,7 +122,7 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
     // add SAT clauses
     for ( i = sat_solver_nvars(p->pSat); i < Gia_ManObjNum(p->pFrames); i++ )
     {
-        pObj = Gia_ManObj( p->pGia, i );
+        pObj = Gia_ManObj( p->pFrames, i );
         if ( Gia_ObjIsAnd(pObj) )
             sat_solver_add_and( p->pSat, i, 
                 Gia_ObjFaninId0(pObj, i), 
@@ -238,54 +132,11 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
     }
 }
 
-/**Function*************************************************************
+static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, Gia_Man_t * pGia, Gia_Obj_t * pObj )  
+{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) ); }
 
-  Synopsis    [Adds logic of one timeframe to the manager.]
-
-  Description [Returns literal of the property output.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManCofAddTimeFrame( Ccf_Man_t * p, int fMax )
-{
-    Gia_Obj_t * pObj;
-    int i, f, Beg, End, Lit;
-    assert( fMax > 0 && fMax <= p->nFrameMax );
-    assert( Vec_IntSize(p->vIdToFra) == (fMax - 1) * Gia_ManObjNum(p->pGia) );
-    // add to the mapping of nodes
-    Vec_IntFillExtra( p->vIdToFra, fMax * Gia_ManObjNum(p->pGia), -1 );
-    // add nodes to each time-frame
-    for ( f = 0; f < fMax; f++ )
-    {
-        if ( Vec_IntSize(p->vFraLims) >= fMax-f )
-            continue;
-        Beg = Vec_IntEntry( p->vFraLims, fMax-f-1 );
-        End = Vec_IntEntry( p->vFraLims, fMax-f );
-        for ( i = Beg; i < End; i++ )
-        {
-            pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vOrder, i) );
-            if ( Gia_ObjIsAnd(pObj) )
-                Lit = Gia_ManHashAnd( p->pFrames, Gia_ObjChild0Frames(p, f, pObj), Gia_ObjChild1Frames(p, f, pObj) );
-            else if ( Gia_ObjIsRo(p->pGia, pObj) && f > 0 )
-                Lit = Gia_ObjChild0Frames(p, f-1, Gia_ObjRoToRi(p->pGia, pObj));
-            else if ( Gia_ObjIsCi(pObj) )
-            {
-                Lit = Gia_ManAppendCi(p->pFrames);
-                // mark primary input
-                Gia_ManObj(p->pFrames, Gia_Lit2Var(Lit))->fMark0 = Gia_ObjIsPi(p->pGia, pObj);
-            }
-            else assert( 0 );
-            Gia_ObjSetFrames( p, f, pObj, Lit );
-        }
-    }
-    // add SAT clauses
-    Gia_ManCofExtendSolver( p );
-    // return output literal
-    return Gia_ObjChild0Frames( p, fMax-1, Gia_ManPo(p->pGia, 0) );
-}
+static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, Gia_Man_t * pGia, Gia_Obj_t * pObj )  
+{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Gia_ObjFaninId1p(pGia, pObj)), Gia_ObjFaninC1(pObj) ); }
 
 /**Function*************************************************************
 
@@ -298,22 +149,25 @@ int Gia_ManCofAddTimeFrame( Ccf_Man_t * p, int fMax )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManCofOneDerive_rec( Ccf_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, Gia_Obj_t * pObj )
 {
-    if ( ~pObj->Value )
-        return pObj->Value;
+    int Res, Id = Gia_ObjId( p->pFrames, pObj );
+    if ( Vec_IntEntry(p->vCopies, Id) != -1 )
+        return;
     assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
     if ( Gia_ObjIsAnd(pObj) )
     {
         Gia_ManCofOneDerive_rec( p, Gia_ObjFanin0(pObj) );
         Gia_ManCofOneDerive_rec( p, Gia_ObjFanin1(pObj) );
-        pObj->Value = Gia_ManHashAnd( p->pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Res = Gia_ManHashAnd( p->pFrames, 
+            Gia_Obj0Copy(p->vCopies, p->pFrames, pObj), 
+            Gia_Obj1Copy(p->vCopies, p->pFrames, pObj) );
     }
-    else if ( pObj->fMark0 ) // PI
-        pObj->Value = sat_solver_var_value( p->pSat, Gia_ObjId(p->pGia, pObj) );
+    else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
+        Res = sat_solver_var_value( p->pSat, Id );
     else
-        pObj->Value = Gia_Var2Lit( Gia_ObjId(p->pGia, pObj), 0 );
-    return pObj->Value;
+        Res = Gia_Var2Lit( Id, 0 );
+    Vec_IntWriteEntry( p->vCopies, Id, Res );
 }
 
 /**Function*************************************************************
@@ -334,8 +188,9 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
     // get the property node
     pObj = Gia_ManObj( p->pFrames, Gia_Lit2Var(LitProp) );
     // derive the cofactor
-    Gia_ManFillValue( p->pFrames );
-    LitOut = Gia_ManCofOneDerive_rec( p, pObj );
+    Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
+    Gia_ManCofOneDerive_rec( p, pObj );
+    LitOut = Vec_IntEntry(p->vCopies, Gia_Lit2Var(LitProp));
     LitOut = Gia_LitNotCond(LitOut, Gia_LitIsCompl(LitProp));
     // add new PO for the cofactor
     Gia_ManAppendCo( p->pFrames, LitOut );
@@ -343,7 +198,7 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
     Gia_ManCofExtendSolver( p );
     // return negative literal of the cofactor
     return Gia_LitNot(LitOut);
-}
+} 
 
 /**Function*************************************************************
 
@@ -360,21 +215,32 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
 ***********************************************************************/
 int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
 {
-    int RetValue;
+    int ObjPrev = 0, ConfPrev = 0, clk;
+    int Count = 0, LitOut, RetValue;
     // try solving for the first time and quit if converged
     RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
     if ( RetValue == l_False )
         return 1;
     // iterate circuit cofactoring
-    while ( RetValue == 0 )
+    while ( RetValue == l_True )
     {
+        clk = clock();
         // derive cofactor
-        int LitOut = Gia_ManCofOneDerive( p, Lit );
+        LitOut = Gia_ManCofOneDerive( p, Lit );
         // add the blocking clause
         RetValue = sat_solver_addclause( p->pSat, &LitOut, &LitOut + 1 );
         assert( RetValue );
         // try solving again
         RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
+        // derive cofactors
+        if ( p->fVerbose ) 
+        {
+            printf( "%3d : AIG =%7d  Conf =%7d.  ", Count++, 
+                Gia_ManObjNum(p->pFrames) - ObjPrev, sat_solver_nconflicts(p->pSat) - ConfPrev );
+            Abc_PrintTime( 1, "Time", clock() - clk );
+            ObjPrev = Gia_ManObjNum(p->pFrames);
+            ConfPrev = sat_solver_nconflicts(p->pSat);
+        }
     }
     if ( RetValue == l_Undef )
         return -1;
@@ -397,16 +263,22 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     Gia_Man_t * pNew;
     Ccf_Man_t * p;
     int f, Lit, RetValue;
+    int clk = clock();
     assert( Gia_ManPoNum(pGia) == 1 );
+
     // create reachability manager
     p = Ccf_ManStart( pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
     // perform backward image computation
     for ( f = 0; f < nFrameMax; f++ )
     {
-        if ( fVerbose )
+        if ( fVerbose ) 
             printf( "ITER %3d :\n", f );
-        // derives new timeframe and returns the property literal
-        Lit = Gia_ManCofAddTimeFrame( p, f+1 );
+        // add to the mapping of nodes
+        p->pFrames = (Gia_Man_t *)Gia_ManUnrollAdd( p->pUnr, f+1 );
+        // add SAT clauses
+        Gia_ManCofExtendSolver( p );
+        // return output literal
+        Lit = Gia_ManUnrollLastLit( p->pUnr );
         // derives cofactors of the property literal till all states are blocked
         RetValue = Gia_ManCofGetReachable( p, Lit );
         if ( RetValue )
@@ -414,22 +286,27 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
     }
     // report the result
     if ( f == nFrameMax )
-        printf( "Completed %d frames without converging.\n", f );
+        printf( "Completed %d frames without converging.  ", f );
     else if ( RetValue == 1 )
-        printf( "Backward reachability converged after %d iterations.\n", f );
+        printf( "Backward reachability converged after %d iterations.  ", f-1 );
     else if ( RetValue == -1 )
-        printf( "Conflict limit or timeout is reached after %d frames.\n", f );
+        printf( "Conflict limit or timeout is reached after %d frames.  ", f-1 );
+    Abc_PrintTime( 1, "Runtime", clock() - clk );
 
     // get the resulting AIG manager
     Gia_ManHashStop( p->pFrames );
-    Gia_ManCleanMark0( p->pFrames );
     pNew = p->pFrames;  p->pFrames = NULL;
     Ccf_ManStop( p );
+
+    // cleanup
+//    if ( fVerbose )
+//        Gia_ManPrintStats( pNew, 0 );
+
     pNew = Gia_ManCleanup( pGia = pNew );
     Gia_ManStop( pGia );
 
 //    if ( fVerbose )
-        Gia_ManPrintStats( pNew, 0 );
+//        Gia_ManPrintStats( pNew, 0 );
     return pNew;   
 }
 
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index 4ab98229..06bea871 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -52,6 +52,9 @@ struct Gia_ManUnr_t_
     Vec_Int_t *     vDegDiff; // degree of each node
     Vec_Int_t *     vFirst;   // first entry in the store
     Vec_Int_t *     vStore;   // store for saved data
+    // the resulting AIG
+    Gia_Man_t *     pNew;     // the resulting AIG
+    int             LastLit;  // the place to store the last literal
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -153,6 +156,8 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     Gia_ManUnr_t * p;
     Gia_Obj_t * pObj;
     int i, k, iRank, iFanin, Degree, Shift;
+    int clk = clock();
+
     p = ABC_CALLOC( Gia_ManUnr_t, 1 );
     p->pAig   = pAig;
     p->pPars  = pPars;
@@ -207,6 +212,16 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     // cleanup
     Vec_IntFreeP( &p->vRank );
     Vec_IntFreeP( &p->vDegree );
+
+    // print verbose output
+    if ( pPars->fVerbose )
+    {
+        printf( "Convergence = %d.  Dangling objects = %d.  Average degree = %.3f   ", 
+            Vec_IntSize(p->vLimit) - 1,
+            Gia_ManObjNum(pAig) - Gia_ManObjNum(p->pOrder),
+            1.0*Vec_IntSize(p->vStore)/Gia_ManObjNum(p->pOrder) - 1.0  );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
     return p;
 }
 
@@ -221,8 +236,9 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManUnrStop( Gia_ManUnr_t * p )  
+void Gia_ManUnrollStop( void * pMan )  
 {
+    Gia_ManUnr_t * p = (Gia_ManUnr_t *)pMan;
     Gia_ManStopP( &p->pOrder );
     Vec_IntFreeP( &p->vLimit );
     Vec_IntFreeP( &p->vRank );
@@ -279,7 +295,10 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
     assert( Gia_ObjIsCi(pObjReal) );
     if ( Gia_ObjIsPi(p->pAig, pObjReal) )
     {
-        pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
+        if ( !p->pPars->fSaveLastLit ) 
+            pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
+        else
+            pObj = Gia_ManPi( pNew, Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
         return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
     }
     if ( f == 0 ) // initialize!
@@ -287,7 +306,10 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
         if ( p->pPars->fInit )
             return 0;
         assert( Gia_ObjCioId(pObjReal) >= Gia_ManPiNum(p->pAig) );
-        pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
+        if ( !p->pPars->fSaveLastLit ) 
+            pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
+        else
+            pObj = Gia_ManPi( pNew, Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
         return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
     }
     pObj = Gia_ManObj( p->pOrder, Gia_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) );
@@ -306,6 +328,144 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
   SeeAlso     []
 
 ***********************************************************************/
+void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
+{
+    Gia_ManUnr_t * p;
+    int f, i;
+    // start 
+    p = Gia_ManUnrStart( pAig, pPars );
+    // start timeframes
+    assert( p->pNew == NULL );
+    p->pNew = Gia_ManStart( 10000 );
+    p->pNew->pName = Gia_UtilStrsav( p->pAig->pName );
+    Gia_ManHashAlloc( p->pNew );
+    // create combinational inputs
+    if ( !p->pPars->fSaveLastLit ) // only in the case when unrolling depth is known
+        for ( f = 0; f < p->pPars->nFrames; f++ )
+            for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+                Gia_ManAppendCi(p->pNew);
+    // create flop outputs
+    if ( !p->pPars->fInit ) // only in the case when initialization is not performed
+        for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+            Gia_ManAppendCi(p->pNew);
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes init/non-init unrolling without flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Gia_ManUnrollAdd( void * pMan, int fMax )
+{
+    Gia_ManUnr_t * p = (Gia_ManUnr_t *)pMan;
+    Gia_Obj_t * pObj;
+    int f, i, Lit, Beg, End;
+    // create PIs on demand
+    if ( p->pPars->fSaveLastLit ) 
+        for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+            Gia_ManAppendCi(p->pNew);
+    // unroll another timeframe
+    for ( f = 0; f < fMax; f++ )
+    {
+        if ( Vec_IntSize(p->vLimit) <= fMax-f )
+            continue;
+        Beg = Vec_IntEntry( p->vLimit, fMax-f-1 );
+        End = Vec_IntEntry( p->vLimit, fMax-f );
+        for ( i = Beg; i < End; i++ )
+        {
+            pObj = Gia_ManObj( p->pOrder, i );
+            if ( Gia_ObjIsAnd(pObj) )
+                Lit = Gia_ManHashAnd( p->pNew, Gia_ObjUnrReadCopy0(p, pObj, i), Gia_ObjUnrReadCopy1(p, pObj, i) );
+            else if ( Gia_ObjIsCo(pObj) )
+            {
+                Lit = Gia_ObjUnrReadCopy0(p, pObj, i);
+                if ( f == fMax-1 )
+                {
+                    if ( p->pPars->fSaveLastLit )
+                        p->LastLit = Lit;
+                    else
+                        Gia_ManAppendCo( p->pNew, Lit );
+                }
+            }
+            else if ( Gia_ObjIsCi(pObj) )
+                Lit = Gia_ObjUnrReadCi( p, i, f, p->pNew );
+            else assert( 0 );
+            assert( Lit >= 0 );
+            Gia_ObjUnrWrite( p, i, Lit ); // should be exactly one call for each obj!
+        }
+    }
+    return p->pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Read the last literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManUnrollLastLit( void * pMan )
+{
+    Gia_ManUnr_t * p = (Gia_ManUnr_t *)pMan;
+    return p->LastLit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes init/non-init unrolling without flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManUnroll( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
+{
+    Gia_ManUnr_t * p;
+    Gia_Man_t * pNew, * pTemp;
+    int fMax;
+    p = (Gia_ManUnr_t *)Gia_ManUnrollStart( pAig, pPars );
+    for ( fMax = 1; fMax <= p->pPars->nFrames; fMax++ )
+        Gia_ManUnrollAdd( p, fMax );
+    assert( Gia_ManPoNum(p->pNew) == p->pPars->nFrames * Gia_ManPoNum(p->pAig) );
+    Gia_ManHashStop( p->pNew );
+    Gia_ManSetRegNum( p->pNew, 0 );
+//    Gia_ManPrintStats( pNew, 0 );
+    // cleanup
+    p->pNew = Gia_ManCleanup( pTemp = p->pNew );
+    Gia_ManStop( pTemp );
+//    Gia_ManPrintStats( pNew, 0 );
+    pNew = p->pNew;  p->pNew = NULL;
+    Gia_ManUnrollStop( p );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes init/non-init unrolling without flops.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
 Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
 {
     Gia_Man_t * pNew, * pTemp;
@@ -359,6 +519,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
 //    Gia_ManPrintStats( pNew, 0 );
     return pNew;
 } 
+*/
 
 /**Function*************************************************************
 
@@ -373,19 +534,9 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
 ***********************************************************************/
 Gia_Man_t * Gia_ManFrames2( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
 {
-    Gia_ManUnr_t * p;
-    Gia_Man_t * pNew = NULL;
+    Gia_Man_t * pNew;
     int clk = clock();
-    p = Gia_ManUnrStart( pAig, pPars );
-    pNew = Gia_ManUnroll( p );
-
-    if ( pPars->fVerbose )
-        printf( "Convergence = %d.  Dangling objects = %d.  Average degree = %.3f   ", 
-            Vec_IntSize(p->vLimit) - 1,
-            Gia_ManObjNum(pAig) - Gia_ManObjNum(p->pOrder),
-            1.0*Vec_IntSize(p->vStore)/Gia_ManObjNum(p->pOrder) - 1.0  );
-
-    Gia_ManUnrStop( p );
+    pNew = Gia_ManUnroll( pAig, pPars );
     if ( pPars->fVerbose )
         Abc_PrintTime( 1, "Time", clock() - clk );
     return pNew;