Updating &gla_refine to perform suffic refinement.

5 files changed, 424 insertions, 214 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 2180e9a4..89ec3bce 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3419,6 +3419,10 @@ SOURCE=.\src\aig\gia\giaAbsIter.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaAbsOut.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaAbsRef.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 9b33c066..822a55dd 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -24,7 +24,6 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satSolver2.h"
 #include "base/main/main.h"
-#include "aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -130,7 +129,7 @@ static inline void        Gla_ObjClearRef( Rfn_Obj_t * p )                     {
     for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
 
 // some lessons learned from debugging mismatches between GIA and mapped CNF
-// - inputs/output of AND-node maybe PPIs (have SAT vars), but the node is not included in the abstraction
+// - inputs/output of AND-node may be PPIs (have SAT vars), but the node is not included in the abstraction
 // - some logic node can be a PPI of one LUT and an internal node of another LUT
 
 ////////////////////////////////////////////////////////////////////////
@@ -139,213 +138,6 @@ static inline void        Gla_ObjClearRef( Rfn_Obj_t * p )                     {
 
 /**Function*************************************************************
 
-  Synopsis    [Derive a new counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
-{
-    Abc_Cex_t * pCex;
-    int i, f, iPiNum;
-    assert( pCexAbs->iPo == 0 );
-    // start the counter-example
-    pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
-    pCex->iFrame = pCexAbs->iFrame;
-    pCex->iPo    = pCexAbs->iPo;
-    // copy the bit data
-    for ( f = 0; f <= pCexAbs->iFrame; f++ )
-        for ( i = 0; i < Vec_IntSize(vPis); i++ )
-        {
-            if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
-            {
-                iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
-                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
-            }
-        }
-    // verify the counter example
-    if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
-    {
-        Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
-        Abc_CexFree( pCex );
-        pCex = NULL;
-    }
-    else
-    {
-        Abc_Print( 1, "Counter-example verification is successful.\n" );
-        Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
-    }
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines gate-level abstraction using the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
-{
-    extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
-//    extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
-    int fAddOneLayer = 1;
-    Abc_Cex_t * pCexNew = NULL;
-    Gia_Man_t * pAbs;
-    Aig_Man_t * pAig;
-    Abc_Cex_t * pCare;
-    Vec_Int_t * vPis, * vPPis;
-    int f, i, iObjId;
-    clock_t clk = clock();
-    int nOnes = 0, Counter = 0;
-    if ( p->vGateClasses == NULL )
-    {
-        Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
-        return -1;
-    }
-    // derive abstraction
-    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
-    Gia_ManStop( pAbs );
-    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
-    if ( Gia_ManPiNum(pAbs) != pCex->nPis )
-    {
-        Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
-        Gia_ManStop( pAbs );
-        return -1;
-    }
-    if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
-    {
-        Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
-//        Gia_ManStop( pAbs );
-//        return -1;
-    }
-//    else
-//        Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
-    // get inputs
-    Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
-    assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
-    // add missing logic
-    if ( fAddOneLayer )
-    {
-        Gia_Obj_t * pObj;
-        // check if this is a real counter-example
-        Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
-        for ( f = 0; f <= pCex->iFrame; f++ )
-        {
-            Gia_ManForEachPi( pAbs, pObj, i )
-            {
-                if ( i >= Vec_IntSize(vPis) ) // PPIs
-                    Gia_ObjTerSimSetX( pObj );
-                else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
-                    Gia_ObjTerSimSet1( pObj );
-                else
-                    Gia_ObjTerSimSet0( pObj );
-            }
-            Gia_ManForEachRo( pAbs, pObj, i )
-            {
-                if ( f == 0 )
-                    Gia_ObjTerSimSet0( pObj );
-                else
-                    Gia_ObjTerSimRo( pAbs, pObj );
-            }
-            Gia_ManForEachAnd( pAbs, pObj, i )
-                Gia_ObjTerSimAnd( pObj );
-            Gia_ManForEachCo( pAbs, pObj, i )
-                Gia_ObjTerSimCo( pObj );
-        }
-        pObj = Gia_ManPo( pAbs, 0 );
-        if ( Gia_ObjTerSimGet1(pObj) )
-        {
-            pCexNew = Gia_ManCexRemap( p, pCex, vPis );
-            Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
-        }
-//        else
-//            Abc_Print( 1, "CEX is not real.\n" );
-        Gia_ManForEachObj( pAbs, pObj, i )
-            Gia_ObjTerSimSetC( pObj );
-        if ( pCexNew == NULL )
-        {
-            // grow one layer
-            Vec_IntForEachEntry( vPPis, iObjId, i )
-            {
-                assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
-                Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
-            }
-            if ( fVerbose )
-            {
-                Abc_Print( 1, "Additional objects = %d.  ", Vec_IntSize(vPPis) );
-                Abc_PrintTime( 1, "Time", clock() - clk );
-            }
-        }
-    }
-    else
-    {
-        // minimize the CEX
-        pAig = Gia_ManToAigSimple( pAbs );
-        pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
-        Aig_ManStop( pAig );
-        if ( pCare == NULL )
-            Abc_Print( 1, "Counter-example minimization has failed.\n" );
-        // add new objects to the map
-        iObjId = -1;
-        for ( f = 0; f <= pCare->iFrame; f++ )
-            for ( i = 0; i < pCare->nPis; i++ )
-                if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
-                {
-                    nOnes++;
-                    assert( i >= Vec_IntSize(vPis) );
-                    iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
-                    assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
-                    if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
-                        continue;
-                    assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
-                    Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
-    //                Abc_Print( 1, "Adding object %d.\n", iObjId );
-    //                Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
-                    Counter++;
-                }
-        Abc_CexFree( pCare );
-        if ( fVerbose )
-        {
-            Abc_Print( 1, "Essential bits = %d.  Additional objects = %d.  ", nOnes, Counter );
-            Abc_PrintTime( 1, "Time", clock() - clk );
-        }
-        // consider the case of SAT
-        if ( iObjId == -1 )
-        {
-            pCexNew = Gia_ManCexRemap( p, pCex, vPis );
-            Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
-        }
-    }
-    Vec_IntFree( vPis );
-    Vec_IntFree( vPPis );
-    Gia_ManStop( pAbs );
-    if ( pCexNew )
-    {
-        ABC_FREE( p->pCexSeq );
-        p->pCexSeq = pCexNew;
-        return 0;
-    }
-    // extract abstraction to include min-cut
-    if ( fMinCut )
-        Nwk_ManDeriveMinCut( p, fVerbose );
-    return -1;
-}
-
-
-
-
-
-/**Function*************************************************************
-
   Synopsis    [Prepares CEX and vMap for refinement.]
 
   Description []
diff --git a/src/aig/gia/giaAbsOut.c b/src/aig/gia/giaAbsOut.c
new file mode 100644
index 00000000..7d0837ec
--- /dev/null
+++ b/src/aig/gia/giaAbsOut.c
@@ -0,0 +1,400 @@
+/**CFile****************************************************************
+
+  FileName    [giaAbsOut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Abstraction refinement outside of abstraction engines.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAbsOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "giaAig.h"
+#include "aig/saig/saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derive a new counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
+{
+    Abc_Cex_t * pCex;
+    int i, f, iPiNum;
+    assert( pCexAbs->iPo == 0 );
+    // start the counter-example
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
+    pCex->iFrame = pCexAbs->iFrame;
+    pCex->iPo    = pCexAbs->iPo;
+    // copy the bit data
+    for ( f = 0; f <= pCexAbs->iFrame; f++ )
+        for ( i = 0; i < Vec_IntSize(vPis); i++ )
+        {
+            if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
+            {
+                iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
+            }
+        }
+    // verify the counter example
+    if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
+    {
+        Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
+    }
+    else
+    {
+        Abc_Print( 1, "Counter-example verification is successful.\n" );
+        Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines gate-level abstraction using the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
+{
+    extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
+//    extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
+    int fAddOneLayer = 1;
+    Abc_Cex_t * pCexNew = NULL;
+    Gia_Man_t * pAbs;
+    Aig_Man_t * pAig;
+    Abc_Cex_t * pCare;
+    Vec_Int_t * vPis, * vPPis;
+    int f, i, iObjId;
+    clock_t clk = clock();
+    int nOnes = 0, Counter = 0;
+    if ( p->vGateClasses == NULL )
+    {
+        Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
+        return -1;
+    }
+    // derive abstraction
+    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    Gia_ManStop( pAbs );
+    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    if ( Gia_ManPiNum(pAbs) != pCex->nPis )
+    {
+        Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
+        Gia_ManStop( pAbs );
+        return -1;
+    }
+    if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
+    {
+        Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
+//        Gia_ManStop( pAbs );
+//        return -1;
+    }
+//    else
+//        Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
+    // get inputs
+    Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
+    assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
+    // add missing logic
+    if ( fAddOneLayer )
+    {
+        Gia_Obj_t * pObj;
+        // check if this is a real counter-example
+        Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
+        for ( f = 0; f <= pCex->iFrame; f++ )
+        {
+            Gia_ManForEachPi( pAbs, pObj, i )
+            {
+                if ( i >= Vec_IntSize(vPis) ) // PPIs
+                    Gia_ObjTerSimSetX( pObj );
+                else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
+                    Gia_ObjTerSimSet1( pObj );
+                else
+                    Gia_ObjTerSimSet0( pObj );
+            }
+            Gia_ManForEachRo( pAbs, pObj, i )
+            {
+                if ( f == 0 )
+                    Gia_ObjTerSimSet0( pObj );
+                else
+                    Gia_ObjTerSimRo( pAbs, pObj );
+            }
+            Gia_ManForEachAnd( pAbs, pObj, i )
+                Gia_ObjTerSimAnd( pObj );
+            Gia_ManForEachCo( pAbs, pObj, i )
+                Gia_ObjTerSimCo( pObj );
+        }
+        pObj = Gia_ManPo( pAbs, 0 );
+        if ( Gia_ObjTerSimGet1(pObj) )
+        {
+            pCexNew = Gia_ManCexRemap( p, pCex, vPis );
+            Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
+        }
+//        else
+//            Abc_Print( 1, "CEX is not real.\n" );
+        Gia_ManForEachObj( pAbs, pObj, i )
+            Gia_ObjTerSimSetC( pObj );
+        if ( pCexNew == NULL )
+        {
+            // grow one layer
+            Vec_IntForEachEntry( vPPis, iObjId, i )
+            {
+                assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
+                Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
+            }
+            if ( fVerbose )
+            {
+                Abc_Print( 1, "Additional objects = %d.  ", Vec_IntSize(vPPis) );
+                Abc_PrintTime( 1, "Time", clock() - clk );
+            }
+        }
+    }
+    else
+    {
+        // minimize the CEX
+        pAig = Gia_ManToAigSimple( pAbs );
+        pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
+        Aig_ManStop( pAig );
+        if ( pCare == NULL )
+            Abc_Print( 1, "Counter-example minimization has failed.\n" );
+        // add new objects to the map
+        iObjId = -1;
+        for ( f = 0; f <= pCare->iFrame; f++ )
+            for ( i = 0; i < pCare->nPis; i++ )
+                if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
+                {
+                    nOnes++;
+                    assert( i >= Vec_IntSize(vPis) );
+                    iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
+                    assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
+                    if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
+                        continue;
+                    assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
+                    Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
+    //                Abc_Print( 1, "Adding object %d.\n", iObjId );
+    //                Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
+                    Counter++;
+                }
+        Abc_CexFree( pCare );
+        if ( fVerbose )
+        {
+            Abc_Print( 1, "Essential bits = %d.  Additional objects = %d.  ", nOnes, Counter );
+            Abc_PrintTime( 1, "Time", clock() - clk );
+        }
+        // consider the case of SAT
+        if ( iObjId == -1 )
+        {
+            pCexNew = Gia_ManCexRemap( p, pCex, vPis );
+            Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
+        }
+    }
+    Vec_IntFree( vPis );
+    Vec_IntFree( vPPis );
+    Gia_ManStop( pAbs );
+    if ( pCexNew )
+    {
+        ABC_FREE( p->pCexSeq );
+        p->pCexSeq = pCexNew;
+        return 0;
+    }
+    // extract abstraction to include min-cut
+    if ( fMinCut )
+        Nwk_ManDeriveMinCut( p, fVerbose );
+    return -1;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example and returns flop values.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManGetStateAndCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame )
+{
+    Vec_Int_t * vInit = Vec_IntAlloc( Gia_ManRegNum(pAig) );
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    assert( iFrame >= 0 && iFrame <= p->iFrame );
+    Gia_ManCleanMark0(pAig);
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        if ( i == iFrame )
+        {
+            Gia_ManForEachRo( pAig, pObjRo, k )
+                Vec_IntPush( vInit, pObjRo->fMark0 );
+        }
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
+    if ( RetValue != 1 )
+        Vec_IntFreeP( &vInit );
+    Gia_ManCleanMark0(pAig);
+    return vInit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManTransformFlops( Gia_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vInit )
+{
+    Vec_Int_t * vInitNew;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i, iFlopId;
+    vInitNew = Vec_IntStart( Gia_ManRegNum(p) );
+    Gia_ManForEachObjVec( vFlops, p, pObj, i )
+    {
+        assert( Gia_ObjIsRo(p, pObj) );
+        if ( Vec_IntEntry(vInit, i) == 0 )
+            continue;
+        iFlopId = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
+        assert( iFlopId >= 0 && iFlopId < Gia_ManRegNum(p) );
+        Vec_IntWriteEntry( vInitNew, iFlopId, 1 );
+    }
+    pNew = Gia_ManDupFlip( p, Vec_IntArray(vInitNew) );
+    Vec_IntFree( vInitNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose )
+{
+    Gia_Man_t * pAbs, * pNew;
+    Vec_Int_t * vPis, * vPPis, * vFlops, * vInit;
+    clock_t clk = clock();
+    int RetValue;
+    ABC_FREE( p->pCexSeq );
+    if ( p->vGateClasses == NULL )
+    {
+        Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" );
+        return -1;
+    }
+    // derive abstraction
+    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    Gia_ManStop( pAbs );
+    pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    if ( Gia_ManPiNum(pAbs) != pCex->nPis )
+    {
+        Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" );
+        Gia_ManStop( pAbs );
+        return -1;
+    }
+    // get the state in frame iFrameStart
+    vInit = Gia_ManGetStateAndCheckCex( pAbs, pCex, iFrameStart );
+    if ( vInit == NULL )
+    {
+        Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" );
+        Gia_ManStop( pAbs );
+        return -1;
+    }
+    if ( fVerbose )
+        Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" );
+    // get inputs
+    Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, NULL );
+    assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
+    // transform the manager to have new init state
+    pNew = Gia_ManTransformFlops( p, vFlops, vInit );
+    assert( pNew->vGateClasses == NULL );
+    pNew->vGateClasses = Vec_IntDup( p->vGateClasses );
+    Vec_IntFree( vPis );
+    Vec_IntFree( vPPis );
+    Vec_IntFree( vFlops );
+    Vec_IntFree( vInit );
+    // perform abstraction for the new AIG
+    {
+        Gia_ParVta_t Pars, * pPars = &Pars;
+        Gia_VtaSetDefaultParams( pPars );
+        pPars->nFramesMax = pCex->iFrame - iFrameStart + 1;
+        pPars->fVerbose = fVerbose;
+        RetValue = Ga2_ManPerform( pNew, pPars );
+    }
+    // move the abstraction map
+    Vec_IntFreeP( &p->vGateClasses );
+    p->vGateClasses = pNew->vGateClasses;
+    pNew->vGateClasses = NULL;
+    // cleanup
+    Gia_ManStop( pNew );
+    Gia_ManStop( pAbs );
+    return -1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index cac2986e..17684032 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -3,6 +3,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAbsGla.c \
     src/aig/gia/giaAbsGla2.c \
     src/aig/gia/giaAbsIter.c \
+    src/aig/gia/giaAbsOut.c \
     src/aig/gia/giaAbsRef.c \
     src/aig/gia/giaAbsRef2.c \
     src/aig/gia/giaAbsVta.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 25c77048..f24f9e12 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27820,14 +27820,26 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose );
+    extern int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose );
+    int iFrameStart = 0;
     int fMinCut = 1;
     int c, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrameStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrameStart < 0 ) 
+                goto usage;
+            break;
         case 'm':
             fMinCut ^= 1;
             break;
@@ -27855,14 +27867,15 @@ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" );
         return 1;
     } 
-    pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose );
+    pAbc->Status = Gia_ManNewRefine( pAbc->pGia, pAbc->pCex, iFrameStart, fVerbose );
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla_refine [-mvh]\n" );
+    Abc_Print( -2, "usage: &gla_refine [-F num] [-vh]\n" );
     Abc_Print( -2, "\t         refines the pre-computed gate map using the counter-example\n" );
-    Abc_Print( -2, "\t-m     : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
+    Abc_Print( -2, "\t-F num : starting timeframe for suffix refinement [default = %d]\n", iFrameStart );
+//    Abc_Print( -2, "\t-m     : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;