Word-level abstraction engine.

13 files changed, 1151 insertions, 246 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6677e0ad..c183432a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1229,6 +1229,7 @@ extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int f
 extern Gia_Man_t *         Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
+extern Gia_Man_t *         Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra );
 extern Gia_Man_t *         Gia_ManDupDfsClasses( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 56d1d29d..ee709df4 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2171,6 +2171,43 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
 
 /**Function*************************************************************
 
+  Synopsis    [Permute inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    for ( i = 0; i < Gia_ManPiNum(p) - nPpis - nExtra; i++ ) // regular PIs
+        Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+    for ( i = Gia_ManPiNum(p) - nExtra; i < Gia_ManPiNum(p); i++ ) // extra PIs due to DC values
+        Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+    for ( i = Gia_ManPiNum(p) - nPpis - nExtra; i < Gia_ManPiNum(p) - nExtra; i++ ) // pseudo-PIs
+        Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+    for ( i = Gia_ManPiNum(p); i < Gia_ManCiNum(p); i++ ) // flop outputs
+        Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew );
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates AIG in the DFS order.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bb0b8c8d..af5d0ccf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26171,7 +26171,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmuyfsipdegonctvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegonctvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26219,10 +26219,10 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nConfGenLimit < 0 )
                 goto usage;
             break;
-        case 'R':
+        case 'Q':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
                 goto usage;
             }
             pPars->nRestLimit = atoi(argv[globalUtilOptind]);
@@ -26366,7 +26366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmuyfsipdegonctvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegonctvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -26374,7 +26374,7 @@ usage:
     Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n",           pPars->nFrameMax );
     Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n",          pPars->nConfLimit );
     Abc_Print( -2, "\t-D num : limit on conflicts during ind-generalization (0 = no limit) [default = %d]\n",pPars->nConfGenLimit );
-    Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
+    Abc_Print( -2, "\t-Q num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
     Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n",                   pPars->nTimeOut );
     Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n",     pPars->nTimeOutOne );
     Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n",              pPars->nTimeOutGap );
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 3485bd4d..c4330264 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -10,5 +10,6 @@ SRC +=    src/base/wlc/wlcAbs.c \
     src/base/wlc/wlcSim.c \
     src/base/wlc/wlcShow.c \
     src/base/wlc/wlcStdin.c \
+    src/base/wlc/wlcUif.c \
     src/base/wlc/wlcWin.c \
     src/base/wlc/wlcWriteVer.c 
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 21ba73a3..91dc0573 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -158,6 +158,7 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vCopies;            // object first bits
     Vec_Int_t              vBits;              // object mapping into AIG nodes
     Vec_Int_t              vLevels;            // object levels
+    Vec_Int_t              vRefs;              // object reference counters
 };
 
 typedef struct Wlc_Par_t_ Wlc_Par_t;
@@ -167,7 +168,10 @@ struct Wlc_Par_t_
     int                    nBitsMul;           // multiplier bit-widht 
     int                    nBitsMux;           // MUX bit-width
     int                    nBitsFlop;          // flop bit-width
-    int                    fVerbose;           // verbose output`
+    int                    nIterMax;           // the max number of iterations
+    int                    fXorOutput;         // XOR outputs of word-level miter
+    int                    fVerbose;           // verbose output
+    int                    fPdrVerbose;        // verbose output
 };
 
 static inline int          Wlc_NtkObjNum( Wlc_Ntk_t * p )                           { return p->iObj - 1;                                                      }
@@ -272,19 +276,15 @@ static inline Wlc_Obj_t *  Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
 ////////////////////////////////////////////////////////////////////////
 
 /*=== wlcAbs.c ========================================================*/
-extern int            Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
-extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
-extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
-extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
-extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
+extern int            Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcAbs2.c ========================================================*/
-extern void           Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
-extern Wlc_Ntk_t *    Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
+extern int            Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcBlast.c ========================================================*/
 extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth );
 /*=== wlcCom.c ========================================================*/
 extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 /*=== wlcNtk.c ========================================================*/
+extern void           Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
 extern char *         Wlc_ObjTypeName( Wlc_Obj_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
@@ -311,6 +311,9 @@ extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int
 extern void           Wlc_NtkProfileCones( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
 extern void           Wlc_NtkShortNames( Wlc_Ntk_t * p );
+extern int            Wlc_NtkDcFlopNum( Wlc_Ntk_t * p );
+extern void           Wlc_NtkSetRefs( Wlc_Ntk_t * p );
+extern int            Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew );
 /*=== wlcReadSmt.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
 extern Wlc_Ntk_t *    Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
@@ -321,6 +324,12 @@ extern void           Wlc_NtkDeleteSim( Vec_Ptr_t * p );
 extern int            Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
 /*=== wlcReadVer.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName, char * pStr );
+/*=== wlcUif.c ========================================================*/
+extern int            Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
+extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
+extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
+extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
+extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
 /*=== wlcWin.c =============================================================*/
 extern void           Wlc_WinProfileArith( Wlc_Ntk_t * p );
 /*=== wlcWriteVer.c ========================================================*/
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index ce6b8de9..318df4dd 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [wlcAbs.c]
+  FileName    [wlcAbs1.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,11 +14,14 @@
 
   Date        [Ver. 1.0. Started - August 22, 2014.]
 
-  Revision    [$Id: wlcAbs.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+  Revision    [$Id: wlcAbs1.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
 #include "wlc.h"
+#include "proof/pdr/pdr.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -32,253 +35,370 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Check if two objects have the same input/output signatures.]
+  Synopsis    [Mark operators that meet the abstraction criteria.]
 
-  Description []
+  Description [This procedure returns the array of objects (vLeaves) that 
+  should be abstracted because of their high bit-width. It uses input array (vUnmark)
+  to not abstract those objects that have been refined in the previous rounds.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
 {
-    Wlc_Obj_t * pFanin, * pFanin2;  int k;
-    if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
-        return 0;
-    if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
-        return 0;
-    if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
-        return 0;
-    for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+    Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+    Wlc_Obj_t * pObj; int i, Count[4] = {0};
+    Wlc_NtkForEachObj( p, pObj, i )
     {
-        pFanin = Wlc_ObjFanin(p, pObj, k);
-        pFanin2 = Wlc_ObjFanin(p, pObj2, k);
-        if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
-            return 0;
-        if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
-            return 0;
+        if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
+            continue;
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++;
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++;
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_MUX )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++;
+            continue;
+        }
+        if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+                Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++;
+            continue;
+        }
     }
-    return 1;
+    if ( fVerbose )
+        printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+    return vLeaves;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collect IDs of the multipliers.]
+  Synopsis    [Marks nodes to be included in the abstracted network.]
 
-  Description []
+  Description [Marks all objects that will be included in the abstracted model.  
+  Stops at the objects (vLeaves) that are abstracted away. Returns three arrays:
+  a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the
+  set of flops present as flops in the abstracted network.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+    int i, iFanin;
+    if ( pObj->Mark )
+        return;
+    pObj->Mark = 1;
+    if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) )
+    {
+        assert( !Wlc_ObjIsPi(pObj) );
+        Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) );
+        return;
+    }
+    if ( Wlc_ObjIsCi(pObj) )
+    {
+        if ( Wlc_ObjIsPi(pObj) )
+            Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) );
+        else
+            Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
+        return;
+    }
+    Wlc_ObjForEachFanin( pObj, iFanin, i )
+        Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
+}
+static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
 {
-    Wlc_Obj_t * pObj;  int i;
-    Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+    Wlc_Obj_t * pObj;
+    int i, Count = 0;
+    Wlc_NtkCleanMarks( p );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
+    Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+        Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
     Wlc_NtkForEachObj( p, pObj, i )
-        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
-            Vec_IntPush( vBoxIds, i );
-    if ( Vec_IntSize( vBoxIds ) > 0 )
-        return vBoxIds;
-    Vec_IntFree( vBoxIds );
-    return NULL;
+        Count += pObj->Mark;
+//    printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n", 
+//        Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops), 
+//        Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) );
+    Vec_IntSort( vPisOld, 0 );
+    Vec_IntSort( vPisNew, 0 );
+    Vec_IntSort( vFlops, 0 );
+    Wlc_NtkCleanMarks( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns all pairs of uifable multipliers.]
+  Synopsis    [Derive word-level abstracted model based on the parameter values.]
 
-  Description []
+  Description [Retuns the word-level abstracted network and the set of pseudo-PIs 
+  (vPisNew), which were created during abstraction. If the abstraction is
+  satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs
+  and their MFFC cones will be listed in the array (vUnmark), which will
+  force the abstraction to not stop at these pseudo-PIs in the future.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
 {
-    Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
-    Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
-    Wlc_Obj_t * pObj, * pObj2;  int i, k;
-    // iterate through unique pairs
-    Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
-        Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
-        {
-            if ( k == i )  
-                break;
-            if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
-            {
-                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
-                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
-            }
-        }
-    Vec_IntFree( vMultis );
-    if ( Vec_IntSize( vPairs ) > 0 )
-        return vPairs;
-    Vec_IntFree( vPairs );
-    return NULL;
+    Wlc_Ntk_t * pNtkNew = NULL;
+    Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
+    Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
+    Vec_Int_t * vFlops  = Vec_IntAlloc( 100 );
+    Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose );
+    Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
+    Vec_BitFree( vLeaves );
+    pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
+    Vec_IntFree( vPisOld );
+    Vec_IntFree( vFlops );
+    if ( pvPisNew )
+        *pvPisNew = vPisNew;
+    else
+        Vec_IntFree( vPisNew );
+    return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Find what objects need to be un-abstracted.]
 
+  Description [Returns a subset of pseudo-PIs (vPisNew), which will be 
+  prevented from being abstracted in the future rounds of abstraction.
+  The AIG manager (pGia) is a bit-level view of the abstracted model.
+  The counter-example (pCex) is used to find waht PPIs to refine.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew )
+{
+    Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
+    Abc_Cex_t * pCexCare;
+    Wlc_Obj_t * pObj; 
+    // count the number of bit-level PPIs and map them into word-level objects they were derived from
+    int f, i, b, nRealPis, nPpiBits = 0;
+    Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis );
+    Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+        for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+            Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) );
+    // since PPIs are ordered last, the previous bits are real PIs
+    nRealPis = pCex->nPis - nPpiBits;
+    // find the care-set
+    pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 );
+    assert( pCexCare->nPis == pCex->nPis );
+    // detect care PPIs
+    for ( f = 0; f <= pCexCare->iFrame; f++ )
+        for ( i = nRealPis; i < pCexCare->nPis; i++ )
+            if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+                Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) );
+    Abc_CexFree( pCexCare );
+    Vec_IntFree( vMap );
+    if ( Vec_IntSize(vRefine) == 0 )// real CEX
+        Vec_IntFreeP( &vRefine );
+    return vRefine;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Abstracts nodes by replacing their outputs with new PIs.]
+  Synopsis    [Mark MFFC cones of the un-abstracted objects.]
 
-  Description [If array is NULL, abstract all multipliers.]
+  Description [The MFFC cones of the objects in vRefine are traversed
+  and all their nodes are marked in vUnmark.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
 {
-    Vec_Int_t * vNodes = vNodesInit;
-    Wlc_Ntk_t * pNew;
-    Wlc_Obj_t * pObj;
-    int i, k, iObj, iFanin;
-    // get multipliers if not given
-    if ( vNodes == NULL )
-        vNodes = Wlc_NtkCollectMultipliers( p );
-    if ( vNodes == NULL )
-        return NULL;
-    // mark nodes
-    Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
-        pObj->Mark = 1;
-    // iterate through the nodes in the DFS order
-    Wlc_NtkCleanCopy( p );
-    Wlc_NtkForEachObj( p, pObj, i )
+    int i, Fanin, Counter = 1;
+    if ( Wlc_ObjIsCi(pNode) )
+        return 0;
+    Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+    Wlc_ObjForEachFanin( pNode, Fanin, i )
     {
-        if ( i == Vec_IntSize(&p->vCopies) )
-            break;
-        if ( pObj->Mark ) {
-            // clean
-            pObj->Mark = 0;
-            // add fresh PI with the same number of bits
-            iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
-        }
-        else {
-            // update fanins 
-            Wlc_ObjForEachFanin( pObj, iFanin, k )
-                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
-            // node to remain
-            iObj = i;
-        }
-        Wlc_ObjSetCopy( p, i, iObj );
+        Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
+        if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+            Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
+    }
+    return Counter;
+}
+static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode )
+{
+    int i, Fanin, Counter = 1;
+    if ( Wlc_ObjIsCi(pNode) )
+        return 0;
+    Wlc_ObjForEachFanin( pNode, Fanin, i )
+    {
+        if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+            Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
+        Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
     }
-    // POs do not change in this procedure
-    if ( vNodes != vNodesInit )
-        Vec_IntFree( vNodes );
-    // reconstruct topological order
-    pNew = Wlc_NtkDupDfs( p, 0, 1 );
-    return pNew;
+    return Counter;
+}
+static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+    int Count1, Count2;
+    // if this is a flop output, compute MFFC of the corresponding flop input
+    while ( Wlc_ObjIsCi(pNode) )
+    {
+        Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+        pNode = Wlc_ObjFo2Fi(p, pNode);
+    }
+    assert( !Wlc_ObjIsCi(pNode) );
+    // dereference the node (and set the bits in vUnmark)
+    Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark );
+    // reference it back
+    Count2 = Wlc_NtkNodeRef_rec( p, pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+    Wlc_Obj_t * pObj; int i, nNodes = 0;
+    if ( Vec_IntSize(&p->vRefs) == 0 )
+        Wlc_NtkSetRefs( p );
+    Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+        nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark );
+    return nNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Adds UIF constraints to node pairs and updates POs.]
+  Synopsis    [Performs abstraction.]
 
-  Description []
+  Description [Derives initial abstraction based on user-specified
+  parameter values, which tell what is the smallest bit-width of a
+  primitive that is being abstracted away.  Currently only add/sub,
+  mul/div, mux, and flop are supported with individual parameters.
+  The second step is to refine the initial abstraction until the
+  point when the property is proved.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 {
-    Vec_Int_t * vPairs = vPairsInit;
-    Wlc_Ntk_t * pNew;
-    Wlc_Obj_t * pObj, * pObj2;
-    Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
-    int i, k, iObj, iObj2, iObjNew, iObjNew2;
-    int iFanin, iFanin2, iFaninNew;
-    // get multiplier pairs if not given
-    if ( vPairs == NULL )
-        vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
-    if ( vPairs == NULL )
-        return NULL;
-    // sanity checks
-    assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
-    // iterate through node pairs
-    vFanins = Vec_IntAlloc( 100 );
-    vCompares = Vec_IntAlloc( 100 );
-    vUifConstrs = Vec_IntAlloc( 100 );
-    Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+    abctime clk = Abc_Clock();
+    int nIters, nNodes, nDcFlops, RetValue = -1;
+    // start the bitmap to mark objects that cannot be abstracted because of refinement
+    // currently, this bitmap is empty because abstraction begins without refinement
+    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+    // set up parameters to run PDR
+    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+    Pdr_ManSetDefaultParams( pPdrPars );
+    pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
+    pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
+    pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
+    //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+    pPdrPars->fVerbose   = pPars->fPdrVerbose;
+    // perform refinement iterations
+    for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
     {
-        // get two nodes
-        pObj  = Wlc_NtkObj( p, iObj );
-        pObj2 = Wlc_NtkObj( p, iObj2 );
-        assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
-        // create fanin comparator nodes
-        Vec_IntClear( vCompares );
-        Wlc_ObjForEachFanin( pObj, iFanin, k )
+        Aig_Man_t * pAig;
+        Abc_Cex_t * pCex;
+        Vec_Int_t * vPisNew, * vRefine;  
+        Gia_Man_t * pGia, * pTemp;
+        Wlc_Ntk_t * pAbs;
+
+        if ( pPars->fVerbose )
+            printf( "\nIteration %d:\n", nIters );
+
+        // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+        // if the abstraction has flops with DC-init state,
+        // new PIs were introduced by bit-blasting at the end of the PI list
+        // here we move these variables to be *before* PPIs, because
+        // PPIs are supposed to be at the end of the PI list for refinement
+        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+        if ( nDcFlops > 0 ) // DC-init flops are present
         {
-            iFanin2 = Wlc_ObjFaninId( pObj2, k );
-            Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
-            iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
-            Vec_IntPush( vCompares, iFaninNew );
-            // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
-            // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
-            pObj = Wlc_NtkObj( p, iObj );
+            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+            Gia_ManStop( pTemp );
         }
-        // concatenate fanin comparators
-        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
-        // create reduction-OR node
-        Vec_IntFill( vFanins, 1, iObjNew );
-        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
-        // craete output comparator node
-        Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
-        iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
-        // create implication node (iObjNew is already complemented above)
-        Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
-        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
-        // save the constraint
-        Vec_IntPush( vUifConstrs, iObjNew );
-    }
-    // derive the AND of the UIF contraints
-    assert( Vec_IntSize(vUifConstrs) > 0 );
-    if ( Vec_IntSize(vUifConstrs) == 1 )
-        iObjNew = Vec_IntEntry( vUifConstrs, 0 );
-    else
-    {
-        // concatenate
-        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
-        // create reduction-AND node
-        Vec_IntFill( vFanins, 1, iObjNew );
-        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
-    }
-    // update each PO to point to the new node
-    Wlc_NtkForEachPo( p, pObj, i )
-    {
-        iObj = Wlc_ObjId(p, pObj);
-        Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
-        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
-        // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
-        // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
-        pObj = Wlc_NtkObj( p, iObj );
-        // update PO/CO arrays
-        assert( Vec_IntEntry(&p->vPos, i) == iObj );
-        assert( Vec_IntEntry(&p->vCos, i) == iObj );
-        Vec_IntWriteEntry( &p->vPos, i, iObjNew );
-        Vec_IntWriteEntry( &p->vCos, i, iObjNew );
-        // transfer the PO attribute
-        Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
-        assert( pObj->fIsPo );
-        pObj->fIsPo = 0;
+        // if the word-level outputs have to be XORs, this is a place to do it
+        if ( pPars->fXorOutput )
+        {
+            pGia = Gia_ManTransformMiter2( pTemp = pGia );
+            Gia_ManStop( pTemp );
+        }
+        if ( pPars->fVerbose )
+        {
+            printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); 
+            Gia_ManPrintStats( pGia, NULL );
+        }
+        Wlc_NtkFree( pAbs );
+
+        // try to prove abstracted GIA by converting it to AIG and calling PDR
+        pAig = Gia_ManToAigSimple( pGia );
+        RetValue = Pdr_ManSolve( pAig, pPdrPars );
+        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+        Aig_ManStop( pAig );
+
+        // consider outcomes
+        if ( pCex == NULL ) 
+        {
+            assert( RetValue ); // proved or undecided
+            Gia_ManStop( pGia );
+            Vec_IntFree( vPisNew );
+            break;
+        }
+
+        // perform refinement
+        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+        Gia_ManStop( pGia );
+        Vec_IntFree( vPisNew );
+        if ( vRefine == NULL ) // real CEX
+        {
+            Abc_CexFree( pCex ); // return CEX in the future
+            break;
+        }
+
+        // update the set of objects to be un-abstracted
+        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+        if ( pPars->fVerbose )
+            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+        Vec_IntFree( vRefine );
+        Abc_CexFree( pCex );
     }
-    // cleanup
-    Vec_IntFree( vUifConstrs );
-    Vec_IntFree( vCompares );
-    Vec_IntFree( vFanins );
-    if ( vPairs != vPairsInit )
-        Vec_IntFree( vPairs );
-    // reconstruct topological order
-    pNew = Wlc_NtkDupDfs( p, 0, 1 );
-    return pNew;
+    Vec_BitFree( vUnmark );
+    // report the result
+    if ( pPars->fVerbose )
+        printf( "\n" );
+    printf( "Abstraction " );
+    if ( RetValue == 0 )
+        printf( "resulted in a real CEX" );
+    else if ( RetValue == 1 )
+        printf( "is successfully proved" );
+    else 
+        printf( "timed out" );
+    printf( " after %d iterations. ", nIters );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c
index f5a7b46d..9bccdf62 100644
--- a/src/base/wlc/wlcAbs2.c
+++ b/src/base/wlc/wlcAbs2.c
@@ -19,6 +19,9 @@
 ***********************************************************************/
 
 #include "wlc.h"
+#include "proof/pdr/pdr.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -26,56 +29,31 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Wabs_Par_t_ Wabs_Par_t;
-struct Wabs_Par_t_
-{
-    Wlc_Ntk_t *            pNtk;
-    Wlc_Par_t *            pPars;
-    Vec_Bit_t *            vLeaves;
-};
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
-{
-    memset( pPars, 0, sizeof(Wlc_Par_t) );
-    pPars->nBitsAdd    = ABC_INFINITY;   // adder bit-width
-    pPars->nBitsMul    = ABC_INFINITY;   // multiplier bit-widht 
-    pPars->nBitsMux    = ABC_INFINITY;   // MUX bit-width
-    pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
-    pPars->fVerbose    =             0;  // verbose output`
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Mark operators that meet the criteria.]
+  Synopsis    [Mark operators that meet the abstraction criteria.]
 
-  Description []
+  Description [This procedure returns the array of objects (vLeaves) that 
+  should be abstracted because of their high bit-width. It uses input array (vUnmark)
+  to not abstract those objects that have been refined in the previous rounds.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
 {
     Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
     Wlc_Obj_t * pObj; int i, Count[4] = {0};
     Wlc_NtkForEachObj( p, pObj, i )
     {
+        if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
+            continue;
         if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
         {
             if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
@@ -101,7 +79,8 @@ Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             continue;
         }
     }
-    printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+    if ( fVerbose )
+        printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
     return vLeaves;
 }
 
@@ -109,14 +88,17 @@ Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 
   Synopsis    [Marks nodes to be included in the abstracted network.]
 
-  Description []
+  Description [Marks all objects that will be included in the abstracted model.  
+  Stops at the objects (vLeaves) that are abstracted away. Returns three arrays:
+  a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the
+  set of flops present as flops in the abstracted network.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
 {
     int i, iFanin;
     if ( pObj->Mark )
@@ -139,8 +121,7 @@ void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeav
     Wlc_ObjForEachFanin( pObj, iFanin, i )
         Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
 }
-
-void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
 {
     Wlc_Obj_t * pObj;
     int i, Count = 0;
@@ -162,31 +143,264 @@ void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOl
 
 /**Function*************************************************************
 
-  Synopsis    [Derive abstraction based on the parameter values.]
+  Synopsis    [Derive word-level abstracted model based on the parameter values.]
 
-  Description []
+  Description [Retuns the word-level abstracted network and the set of pseudo-PIs 
+  (vPisNew), which were created during abstraction. If the abstraction is
+  satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs
+  and their MFFC cones will be listed in the array (vUnmark), which will
+  force the abstraction to not stop at these pseudo-PIs in the future.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
 {
     Wlc_Ntk_t * pNtkNew = NULL;
     Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
     Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
     Vec_Int_t * vFlops  = Vec_IntAlloc( 100 );
-    Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars );
+    Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose );
     Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
     Vec_BitFree( vLeaves );
     pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
     Vec_IntFree( vPisOld );
-    Vec_IntFree( vPisNew );
     Vec_IntFree( vFlops );
+    if ( pvPisNew )
+        *pvPisNew = vPisNew;
+    else
+        Vec_IntFree( vPisNew );
     return pNtkNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Find what objects need to be un-abstracted.]
+
+  Description [Returns a subset of pseudo-PIs (vPisNew), which will be 
+  prevented from being abstracted in the future rounds of abstraction.
+  The AIG manager (pGia) is a bit-level view of the abstracted model.
+  The counter-example (pCex) is used to find waht PPIs to refine.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew )
+{
+    Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
+    Abc_Cex_t * pCexCare;
+    Wlc_Obj_t * pObj; 
+    // count the number of bit-level PPIs and map them into word-level objects they were derived from
+    int f, i, b, nRealPis, nPpiBits = 0;
+    Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis );
+    Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+        for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+            Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) );
+    // since PPIs are ordered last, the previous bits are real PIs
+    nRealPis = pCex->nPis - nPpiBits;
+    // find the care-set
+    pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 );
+    assert( pCexCare->nPis == pCex->nPis );
+    // detect care PPIs
+    for ( f = 0; f <= pCexCare->iFrame; f++ )
+        for ( i = nRealPis; i < pCexCare->nPis; i++ )
+            if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+                Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) );
+    Abc_CexFree( pCexCare );
+    Vec_IntFree( vMap );
+    if ( Vec_IntSize(vRefine) == 0 )// real CEX
+        Vec_IntFreeP( &vRefine );
+    return vRefine;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark MFFC cones of the un-abstracted objects.]
+
+  Description [The MFFC cones of the objects in vRefine are traversed
+  and all their nodes are marked in vUnmark.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+    int i, Fanin, Counter = 1;
+    if ( Wlc_ObjIsCi(pNode) )
+        return 0;
+    Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+    Wlc_ObjForEachFanin( pNode, Fanin, i )
+    {
+        Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
+        if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+            Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
+    }
+    return Counter;
+}
+static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode )
+{
+    int i, Fanin, Counter = 1;
+    if ( Wlc_ObjIsCi(pNode) )
+        return 0;
+    Wlc_ObjForEachFanin( pNode, Fanin, i )
+    {
+        if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+            Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
+        Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+    }
+    return Counter;
+}
+static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+    int Count1, Count2;
+    // if this is a flop output, compute MFFC of the corresponding flop input
+    while ( Wlc_ObjIsCi(pNode) )
+    {
+        Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+        pNode = Wlc_ObjFo2Fi(p, pNode);
+    }
+    assert( !Wlc_ObjIsCi(pNode) );
+    // dereference the node (and set the bits in vUnmark)
+    Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark );
+    // reference it back
+    Count2 = Wlc_NtkNodeRef_rec( p, pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+    Wlc_Obj_t * pObj; int i, nNodes = 0;
+    if ( Vec_IntSize(&p->vRefs) == 0 )
+        Wlc_NtkSetRefs( p );
+    Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+        nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark );
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs abstraction.]
+
+  Description [Derives initial abstraction based on user-specified
+  parameter values, which tell what is the smallest bit-width of a
+  primitive that is being abstracted away.  Currently only add/sub,
+  mul/div, mux, and flop are supported with individual parameters.
+  The second step is to refine the initial abstraction until the
+  point when the property is proved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    abctime clk = Abc_Clock();
+    int nIters, nNodes, nDcFlops, RetValue = -1;
+    // start the bitmap to mark objects that cannot be abstracted because of refinement
+    // currently, this bitmap is empty because abstraction begins without refinement
+    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+    // set up parameters to run PDR
+    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+    Pdr_ManSetDefaultParams( pPdrPars );
+    pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
+    pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
+    pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
+    //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+    pPdrPars->fVerbose   = pPars->fPdrVerbose;
+    // perform refinement iterations
+    for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
+    {
+        Aig_Man_t * pAig;
+        Abc_Cex_t * pCex;
+        Vec_Int_t * vPisNew, * vRefine;  
+        Gia_Man_t * pGia, * pTemp;
+        Wlc_Ntk_t * pAbs;
+
+        if ( pPars->fVerbose )
+            printf( "\nIteration %d:\n", nIters );
+
+        // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+        // if the abstraction has flops with DC-init state,
+        // new PIs were introduced by bit-blasting at the end of the PI list
+        // here we move these variables to be *before* PPIs, because
+        // PPIs are supposed to be at the end of the PI list for refinement
+        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+        if ( nDcFlops > 0 ) // DC-init flops are present
+        {
+            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+            Gia_ManStop( pTemp );
+        }
+        // if the word-level outputs have to be XORs, this is a place to do it
+        if ( pPars->fXorOutput )
+        {
+            pGia = Gia_ManTransformMiter2( pTemp = pGia );
+            Gia_ManStop( pTemp );
+        }
+        if ( pPars->fVerbose )
+        {
+            printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); 
+            Gia_ManPrintStats( pGia, NULL );
+        }
+        Wlc_NtkFree( pAbs );
+
+        // try to prove abstracted GIA by converting it to AIG and calling PDR
+        pAig = Gia_ManToAigSimple( pGia );
+        RetValue = Pdr_ManSolve( pAig, pPdrPars );
+        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+        Aig_ManStop( pAig );
+
+        // consider outcomes
+        if ( pCex == NULL ) 
+        {
+            assert( RetValue ); // proved or undecided
+            Gia_ManStop( pGia );
+            Vec_IntFree( vPisNew );
+            break;
+        }
+
+        // perform refinement
+        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+        Gia_ManStop( pGia );
+        Vec_IntFree( vPisNew );
+        if ( vRefine == NULL ) // real CEX
+        {
+            Abc_CexFree( pCex ); // return CEX in the future
+            break;
+        }
+
+        // update the set of objects to be un-abstracted
+        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+        if ( pPars->fVerbose )
+            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+        Vec_IntFree( vRefine );
+        Abc_CexFree( pCex );
+    }
+    Vec_BitFree( vUnmark );
+    // report the result
+    if ( pPars->fVerbose )
+        printf( "\n" );
+    printf( "Abstraction " );
+    if ( RetValue == 0 )
+        printf( "resulted in a real CEX" );
+    else if ( RetValue == 1 )
+        printf( "is successfully proved" );
+    else 
+        printf( "timed out" );
+    printf( " after %d iterations. ", nIters );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 67d7c902..f4de8ee6 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1418,7 +1418,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         }
         else
         {
-            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 );
+            pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 0 );
             Gia_ManDupRemapLiterals( vBits, pTemp );
             Gia_ManStop( pTemp );
         }
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 346a9076..97717b09 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -33,6 +33,7 @@ static int  Abc_CommandWriteWlc   ( Abc_Frame_t * pAbc, int argc, char ** argv )
 static int  Abc_CommandPs         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandCone       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandAbs        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandAbs2       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandProfile    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -74,6 +75,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%ps",          Abc_CommandPs,         0 );
     Cmd_CommandAdd( pAbc, "Word level", "%cone",        Abc_CommandCone,       0 );
     Cmd_CommandAdd( pAbc, "Word level", "%abs",         Abc_CommandAbs,        0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%abs2",        Abc_CommandAbs2,       0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",       Abc_CommandBlast,      0 );
     Cmd_CommandAdd( pAbc, "Word level", "%profile",     Abc_CommandProfile,    0 );
     Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 );
@@ -458,7 +460,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -506,9 +508,26 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBitsFlop < 0 )
                 goto usage;
             break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nIterMax < 0 )
+                goto usage;
+            break;
+        case 'x':
+            pPars->fXorOutput ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
+        case 'w':
+            pPars->fPdrVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -520,17 +539,133 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
         return 0;
     }
-    pNtk = Wlc_NtkAbs( pNtk, pPars );
-    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    Wlc_NtkAbsCore( pNtk, pPars );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" );
+    Abc_Print( -2, "\t         abstraction for word-level networks\n" );
+    Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+    Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
+    Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
+    Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
+    Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
+    Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandAbs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    Wlc_Par_t Pars, * pPars = &Pars;
+    int c;
+    Wlc_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'A':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsAdd < 0 )
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsMul < 0 )
+                goto usage;
+            break;
+        case 'X':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsMux < 0 )
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBitsFlop < 0 )
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nIterMax < 0 )
+                goto usage;
+            break;
+        case 'x':
+            pPars->fXorOutput ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fPdrVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+        return 0;
+    }
+    Wlc_NtkAbsCore2( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%abs [-AMXF num] [-vh]\n" );
+    Abc_Print( -2, "usage: %%abs2 [-AMXFI num] [-xvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
     Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
     Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
+    Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
+    Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 86b0c17e..e6ab0739 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -96,6 +96,30 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
+{
+    memset( pPars, 0, sizeof(Wlc_Par_t) );
+    pPars->nBitsAdd    = ABC_INFINITY;   // adder bit-width
+    pPars->nBitsMul    = ABC_INFINITY;   // multiplier bit-widht 
+    pPars->nBitsMux    = ABC_INFINITY;   // MUX bit-width
+    pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
+    pPars->nIterMax    =         1000;   // the max number of iterations
+    pPars->fXorOutput  =            1;   // XOR outputs of word-level miter
+    pPars->fVerbose    =            0;   // verbose output`
+    pPars->fPdrVerbose =            0;   // show verbose PDR output
+}
+
+/**Function*************************************************************
+
   Synopsis    [Working with models.]
 
   Description []
@@ -227,6 +251,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
     ABC_FREE( p->vCopies.pArray );
     ABC_FREE( p->vBits.pArray );
     ABC_FREE( p->vLevels.pArray );
+    ABC_FREE( p->vRefs.pArray );
     ABC_FREE( p->pInits );
     ABC_FREE( p->pObjs );
     ABC_FREE( p->pName );
@@ -912,7 +937,7 @@ Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vP
 
     if ( p->pSpec )
         pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    Wlc_NtkTransferNames( pNew, p );
+    //Wlc_NtkTransferNames( pNew, p );
     return pNew;
 }
 
@@ -1129,6 +1154,70 @@ void Wlc_NtkShortNames( Wlc_Ntk_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Count the number of flops initialized to DC value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p )
+{
+    int i, nFlops, Count = 0;
+    if ( p->pInits == NULL )
+        return 0;
+    nFlops = strlen(p->pInits);
+    for ( i = 0; i < nFlops; i++ )
+        Count += (p->pInits[i] == 'x' || p->pInits[i] == 'X');
+    return Count;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create references.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Wlc_NtkSetRefs( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; int i, k, Fanin;
+    Vec_IntFill( &p->vRefs, Wlc_NtkObjNumMax(p), 0 );
+    Wlc_NtkForEachObj( p, pObj, i )
+        Wlc_ObjForEachFanin( pObj, Fanin, k )
+            Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Vec_IntAddToEntry( &p->vRefs, Wlc_ObjId(p, pObj), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure simply count the number of PPI bits.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew )
+{
+    Wlc_Obj_t * pObj; 
+    int i, Count = 0;
+    Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+        Count += Wlc_ObjRange(pObj);
+    return Count;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcUif.c b/src/base/wlc/wlcUif.c
new file mode 100644
index 00000000..78451c17
--- /dev/null
+++ b/src/base/wlc/wlcUif.c
@@ -0,0 +1,290 @@
+/**CFile****************************************************************
+
+  FileName    [wlcUif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Abstraction for word-level networks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcUif.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Check if two objects have the same input/output signatures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+{
+    Wlc_Obj_t * pFanin, * pFanin2;  int k;
+    if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
+        return 0;
+    if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
+        return 0;
+    if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
+        return 0;
+    for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+    {
+        pFanin = Wlc_ObjFanin(p, pObj, k);
+        pFanin2 = Wlc_ObjFanin(p, pObj2, k);
+        if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
+            return 0;
+        if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect IDs of the multipliers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;  int i;
+    Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+            Vec_IntPush( vBoxIds, i );
+    if ( Vec_IntSize( vBoxIds ) > 0 )
+        return vBoxIds;
+    Vec_IntFree( vBoxIds );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns all pairs of uifable multipliers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+{
+    Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
+    Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
+    Wlc_Obj_t * pObj, * pObj2;  int i, k;
+    // iterate through unique pairs
+    Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
+        Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
+        {
+            if ( k == i )  
+                break;
+            if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
+            {
+                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
+                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
+            }
+        }
+    Vec_IntFree( vMultis );
+    if ( Vec_IntSize( vPairs ) > 0 )
+        return vPairs;
+    Vec_IntFree( vPairs );
+    return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Abstracts nodes by replacing their outputs with new PIs.]
+
+  Description [If array is NULL, abstract all multipliers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+{
+    Vec_Int_t * vNodes = vNodesInit;
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    int i, k, iObj, iFanin;
+    // get multipliers if not given
+    if ( vNodes == NULL )
+        vNodes = Wlc_NtkCollectMultipliers( p );
+    if ( vNodes == NULL )
+        return NULL;
+    // mark nodes
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
+        pObj->Mark = 1;
+    // iterate through the nodes in the DFS order
+    Wlc_NtkCleanCopy( p );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( i == Vec_IntSize(&p->vCopies) )
+            break;
+        if ( pObj->Mark ) {
+            // clean
+            pObj->Mark = 0;
+            // add fresh PI with the same number of bits
+            iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
+        }
+        else {
+            // update fanins 
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+            // node to remain
+            iObj = i;
+        }
+        Wlc_ObjSetCopy( p, i, iObj );
+    }
+    // POs do not change in this procedure
+    if ( vNodes != vNodesInit )
+        Vec_IntFree( vNodes );
+    // reconstruct topological order
+    pNew = Wlc_NtkDupDfs( p, 0, 1 );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds UIF constraints to node pairs and updates POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+{
+    Vec_Int_t * vPairs = vPairsInit;
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj, * pObj2;
+    Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
+    int i, k, iObj, iObj2, iObjNew, iObjNew2;
+    int iFanin, iFanin2, iFaninNew;
+    // get multiplier pairs if not given
+    if ( vPairs == NULL )
+        vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
+    if ( vPairs == NULL )
+        return NULL;
+    // sanity checks
+    assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
+    // iterate through node pairs
+    vFanins = Vec_IntAlloc( 100 );
+    vCompares = Vec_IntAlloc( 100 );
+    vUifConstrs = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+    {
+        // get two nodes
+        pObj  = Wlc_NtkObj( p, iObj );
+        pObj2 = Wlc_NtkObj( p, iObj2 );
+        assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
+        // create fanin comparator nodes
+        Vec_IntClear( vCompares );
+        Wlc_ObjForEachFanin( pObj, iFanin, k )
+        {
+            iFanin2 = Wlc_ObjFaninId( pObj2, k );
+            Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
+            iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
+            Vec_IntPush( vCompares, iFaninNew );
+            // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
+            // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+            pObj = Wlc_NtkObj( p, iObj );
+        }
+        // concatenate fanin comparators
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
+        // create reduction-OR node
+        Vec_IntFill( vFanins, 1, iObjNew );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
+        // craete output comparator node
+        Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
+        iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
+        // create implication node (iObjNew is already complemented above)
+        Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
+        // save the constraint
+        Vec_IntPush( vUifConstrs, iObjNew );
+    }
+    // derive the AND of the UIF contraints
+    assert( Vec_IntSize(vUifConstrs) > 0 );
+    if ( Vec_IntSize(vUifConstrs) == 1 )
+        iObjNew = Vec_IntEntry( vUifConstrs, 0 );
+    else
+    {
+        // concatenate
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
+        // create reduction-AND node
+        Vec_IntFill( vFanins, 1, iObjNew );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
+    }
+    // update each PO to point to the new node
+    Wlc_NtkForEachPo( p, pObj, i )
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
+        // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
+        // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+        pObj = Wlc_NtkObj( p, iObj );
+        // update PO/CO arrays
+        assert( Vec_IntEntry(&p->vPos, i) == iObj );
+        assert( Vec_IntEntry(&p->vCos, i) == iObj );
+        Vec_IntWriteEntry( &p->vPos, i, iObjNew );
+        Vec_IntWriteEntry( &p->vCos, i, iObjNew );
+        // transfer the PO attribute
+        Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
+        assert( pObj->fIsPo );
+        pObj->fIsPo = 0;
+    }
+    // cleanup
+    Vec_IntFree( vUifConstrs );
+    Vec_IntFree( vCompares );
+    Vec_IntFree( vFanins );
+    if ( vPairs != vPairsInit )
+        Vec_IntFree( vPairs );
+    // reconstruct topological order
+    pNew = Wlc_NtkDupDfs( p, 0, 1 );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 554add9b..baade033 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -50,7 +50,16 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
     Vec_Ptr_t * vVec;
     int i, ThisSize, Length, LengthStart;
     if ( Vec_PtrSize(p->vSolvers) < 2 )
+    {
+        printf( "Frame " );
+        printf( "Clauses                                                     " );
+        printf( "Max Queue " );
+        printf( "Flops " );
+        printf( "Cex      " );
+        printf( "Time" );
+        printf( "\n" );
         return;
+    }
     if ( Abc_FrameIsBatchMode() && !fClose )
         return;
     // count the total length of the printout
@@ -81,9 +90,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
     for ( i = ThisSize; i < 70; i++ )
         Abc_Print( 1, " " );
     Abc_Print( 1, "%5d", p->nQueMax );
-    Abc_Print( 1, "%5d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
+    Abc_Print( 1, "%6d", p->vAbsFlops ? Vec_IntCountPositive(p->vAbsFlops) : p->nAbsFlops );
     if ( p->pPars->fUseAbs )
-    Abc_Print( 1, "%5d", p->nCexes );
+    Abc_Print( 1, "%4d", p->nCexes );
     Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     if ( p->pPars->fSolveAll )
         Abc_Print( 1, "  CEX =%4d", p->pPars->nFailOuts );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index c19041ee..abe8c0a8 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -455,7 +455,7 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
     int i, f, Lit, Flop, nFrames = 0;
     int nPis = Saig_ManPiNum(p->pAig);
     int nFfRefined = 0;
-    if ( !p->pPars->fUseAbs )
+    if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
         return Pdr_ManDeriveCex(p);
     // restore previous map
     Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )