Memory abstraction.

4 files changed, 284 insertions, 154 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 5498d9da..ca6b836a 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -395,6 +395,7 @@ extern void           Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
 extern void           Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray );
 extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
+extern void           Wlc_NtkPrintObjects( Wlc_Ntk_t * p );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
 extern char *         Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index b8853dda..3fbe1ba8 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -309,9 +309,10 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fShowMem     = 0;
     int fDistrib     = 0;
     int fTwoSides    = 0;
+    int fAllObjects  = 0;
     int c, fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cmardtvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cmardtovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -333,6 +334,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             fTwoSides ^= 1;
             break;
+        case 'o':
+            fAllObjects ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -356,9 +360,11 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD );
     if ( fShowMem )
         Wlc_NtkPrintMemory( pNtk );
+    if ( fAllObjects )
+        Wlc_NtkPrintObjects( pNtk );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%ps [-cmardtvh]\n" );
+    Abc_Print( -2, "usage: %%ps [-cmardtovh]\n" );
     Abc_Print( -2, "\t         prints statistics\n" );
     Abc_Print( -2, "\t-c     : toggle printing cones [default = %s]\n",                 fShowCones? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle printing multipliers [default = %s]\n",           fShowMulti? "yes": "no" );
@@ -366,6 +372,7 @@ usage:
     Abc_Print( -2, "\t-r     : toggle printing memories [default = %s]\n",              fShowMem?   "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle printing distrubition [default = %s]\n",          fDistrib?   "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides?  "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle printing all objects [default = %s]\n",           fAllObjects?"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;
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
index 52cb2e2d..328484bd 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -75,7 +75,7 @@ Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p )
 void Wlc_NtkPrintMemory( Wlc_Ntk_t * p )
 {
     Vec_Int_t * vMemory;
-    vMemory = Wlc_NtkCollectMemSizes( p );
+    vMemory = Wlc_NtkCollectMemory( p );
     Vec_IntSort( vMemory, 0 );
     Wlc_NtkPrintNodeArray( p, vMemory );
     Vec_IntFree( vMemory );
@@ -130,15 +130,20 @@ int Wlc_CountDcs( char * pInit )
 }
 int Wlc_NtkDupOneObject( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int TypeNew, Vec_Int_t * vFanins )
 {
+    int iObj = Wlc_ObjId(p, pObj);
     unsigned Type = pObj->Type;
     int iObjNew, nFanins = Wlc_ObjFaninNum(pObj);
+    int iObjCopy = Wlc_ObjCopy(p, iObj);
     pObj->Type = TypeNew;
     pObj->nFanins = 0;
-    iObjNew = Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    iObjNew = Wlc_ObjDup( pNew, p, iObj, vFanins );
     pObj->Type = Type;
     pObj->nFanins = (unsigned)nFanins;
     if ( TypeNew == WLC_OBJ_FO )
+    {
         Vec_IntPush( pNew->vInits, -Wlc_ObjRange(pObj) );
+        Wlc_ObjSetCopy( p, iObj, iObjCopy );
+    }
     return iObjNew;
 }
 void Wlc_NtkDupOneBuffer( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins, int fIsFi )
@@ -164,8 +169,8 @@ Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_In
     int i, Entry, iObj, iFrame;
     Vec_IntForEachEntry( vNodeFrames, Entry, i )
     {
-        iObj   = Entry >> 10;
-        iFrame = Entry & 0x3FF;
+        iObj   = Entry >> 11;
+        iFrame = (Entry >> 1) & 0x3FF;
         pObj   = Wlc_NtkObj( p, iObj );
         // address
         if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
@@ -184,23 +189,78 @@ Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_In
         else assert( 0 );
         Vec_IntPush( vNewObjs, pFanin ? Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) : 0 );
     }
-    assert( Vec_IntSize(vNewObjs) == Vec_IntCap(vNewObjs) );
+    assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) );
     return vNewObjs;
 }
-Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Vec_Wec_t * vConstrs ) 
+void Wlc_NtkAbsCreateFlopInputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Wlc_Obj_t * pCounter, int AdderBits ) 
 {
-    Vec_Int_t * vLevel; 
+    Wlc_Obj_t * pObj, * pFanin, * pFlop, * pCond, * pMux, * pConst;
+    int i, n, Entry, Value, iObj, iFrame;
+    Vec_IntForEachEntry( vNodeFrames, Entry, i )
+    {
+        Value  = Entry & 1;
+        iObj   = Entry >> 11;
+        iFrame = (Entry >> 1) & 0x3FF;
+        pObj   = Wlc_NtkObj( p, iObj );
+        for ( n = 0; n < 2; n++ ) // n=0 -- address   n=1 -- data
+        {
+            pFlop = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*i+n) );
+            if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
+                pFanin = Wlc_ObjCopyObj( pNew, p, n ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj) );
+            else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
+                pFanin = n ? Wlc_NtkObj(pNew, Wlc_ObjCopy(p, iObj)) : Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin1(p, pObj) );
+            else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
+            {
+                if ( n ) continue;
+                pFanin = Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin0(p, pObj) );
+                if ( Value )
+                {
+                    Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pFanin) );
+                    pFanin = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_NOT, 0, 0, 0));
+                    Wlc_ObjAddFanins( pNew, pFanin, vFanins );
+                }
+            }
+            else assert( 0 );
+            assert( Wlc_ObjRange(pFlop) == Wlc_ObjRange(pFanin) );
+            // create constant
+            pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0));
+            Vec_IntFill( vFanins, 1, iFrame );
+            Wlc_ObjAddFanins( pNew, pConst, vFanins );
+            // create equality
+            pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0));
+            Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pConst), Wlc_ObjId(pNew, pCounter) );
+            Wlc_ObjAddFanins( pNew, pCond, vFanins );
+            // create MUX
+            pMux = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pFlop)-1, 0));
+            Vec_IntClear( vFanins );
+            Vec_IntPush( vFanins, Wlc_ObjId(pNew, pCond) );
+            Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFlop) );
+            Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFanin) );
+            Wlc_ObjAddFanins( pNew, pMux, vFanins );
+            Wlc_ObjSetCo( pNew, pMux, 1 );
+        }
+    }
+}
+void Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Vec_Wec_t * vConstrs, Wlc_Obj_t * pConstrOut ) 
+{
+    Vec_Int_t * vTrace; 
     Vec_Int_t * vBitConstr = Vec_IntAlloc( 100 );
     Vec_Int_t * vLevConstr = Vec_IntAlloc( 100 );
     Wlc_Obj_t * pAddrs[2], * pDatas[2], * pCond, * pConstr = NULL;
-    int i, k, Entry, Index[2];
-    Vec_WecForEachLevel( vConstrs, vLevel, i )
+    int i, k, Entry, Index[2], iFrameLast, iFrameThis;
+    assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) );
+    Vec_WecForEachLevel( vConstrs, vTrace, i )
     {
-        assert( Vec_IntSize(vLevel) >= 2 );
+        if ( Vec_IntSize(vTrace) == 0 ) 
+            continue;
+        assert( Vec_IntSize(vTrace) >= 2 );
         Vec_IntClear( vLevConstr );
 
-        Index[0] = Vec_IntFind( vNodeFrames, Vec_IntEntry(vLevel, 0) );
-        Index[1] = Vec_IntFind( vNodeFrames, Vec_IntEntryLast(vLevel) );
+        iFrameThis = (Vec_IntEntry(vTrace, 0)  >> 1) & 0x3FF;
+        iFrameLast = (Vec_IntEntryLast(vTrace) >> 1) & 0x3FF;
+
+        Index[0] = Vec_IntFind( vNodeFrames, Vec_IntEntry(vTrace, 0) );
+        Index[1] = Vec_IntFind( vNodeFrames, Vec_IntEntryLast(vTrace) );
         assert( Index[0] >= 0 && Index[1] >= 0 );
 
         pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
@@ -209,6 +269,17 @@ Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t *
         pDatas[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]+1) );
         pDatas[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]+1) );
 
+        // redirect the source in the last time frame to point to FOs
+        if ( iFrameThis == iFrameLast )
+        {
+            pAddrs[0] = Wlc_ObjFo2Fi(pNew, pAddrs[0]);
+            pDatas[0] = Wlc_ObjFo2Fi(pNew, pDatas[0]);
+        }
+
+        // redirect the sink in the last time frame to point to FOs
+        pAddrs[1] = Wlc_ObjFo2Fi(pNew, pAddrs[1]);
+        pDatas[1] = Wlc_ObjFo2Fi(pNew, pDatas[1]);
+
         // equal addresses
         pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0));
         Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pAddrs[0]), Wlc_ObjId(pNew, pAddrs[1]) );
@@ -221,12 +292,20 @@ Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t *
         Wlc_ObjAddFanins( pNew, pCond, vFanins );
         Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
 
-        Vec_IntForEachEntryStartStop( vLevel, Entry, k, 0, Vec_IntSize(vLevel)-1 )
+        Vec_IntForEachEntryStartStop( vTrace, Entry, k, 1, Vec_IntSize(vTrace)-1 )
         {
-            Index[0]  = Vec_IntFind( vNodeFrames, Entry );            
-            pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
+            iFrameThis = (Entry >> 1) & 0x3FF;
+            Index[0]   = Vec_IntFind( vNodeFrames, Entry );            
+            assert( Index[0] >= 0 );
+            pAddrs[0]  = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) );
+            // redirect the middle in the last time frame to point to FOs
+            if ( iFrameThis == iFrameLast )
+                pAddrs[0] = Wlc_ObjFo2Fi(pNew, pAddrs[0]);
             if ( Vec_IntEntry(vNewObjs, 2*Index[0]+1) == 0 ) // MUX
+            {
+                assert( Wlc_ObjType(Wlc_NtkObj(p, Entry >> 11)) == WLC_OBJ_MUX );
                 Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pAddrs[0]) );
+            }
             else // different addresses
             {
                 assert( Wlc_ObjRange(pAddrs[0]) == Wlc_ObjRange(pAddrs[1]) );
@@ -266,64 +345,17 @@ Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t *
     // cleanup
     Vec_IntFree( vBitConstr );
     Vec_IntFree( vLevConstr );
-    return pConstr;
-}
-void Wlc_NtkAbsCreateFlopInputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Wlc_Obj_t * pCounter, int AdderBits, Vec_Bit_t * vMuxVal ) 
-{
-    Wlc_Obj_t * pObj, * pFanin, * pFlop, * pCond, * pMux, * pConst;
-    int i, n, Entry, iObj, iFrame, Index;
-    Vec_IntForEachEntry( vNodeFrames, Entry, i )
-    {
-        iObj   = Entry >> 10;
-        iFrame = Entry & 0x3FF;
-        pObj   = Wlc_NtkObj( p, iObj );
-        Index  = Vec_IntFind( vNodeFrames, Entry );
-        for ( n = 0; n < 2; n++ ) // n=0 -- address   n=1 -- data
-        {
-            pFlop = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index+n) );
-            if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
-                pFanin = Wlc_ObjCopyObj( pNew, p, n ? Wlc_ObjFanin2(pNew, pObj) : Wlc_ObjFanin1(pNew, pObj) );
-            else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
-                pFanin = n ? Wlc_NtkObj(pNew, Wlc_ObjCopy(p, iObj)) : Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin1(pNew, pObj) );
-            else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
-            {
-                if ( n ) continue;
-                pFanin = Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin0(p, pObj) );
-                if ( Vec_BitEntry( vMuxVal, iFrame * Wlc_NtkObjNum(p) + iObj ) )
-                {
-                    Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pFanin) );
-                    pFanin = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_NOT, 0, 0, 0));
-                    Wlc_ObjAddFanins( pNew, pFanin, vFanins );
-                }
-            }
-            else assert( 0 );
-            assert( Wlc_ObjRange(pFlop) == Wlc_ObjRange(pFanin) );
-            // create constant
-            pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0));
-            Vec_IntFill( vFanins, 1, iFrame );
-            Wlc_ObjAddFanins( pNew, pConst, vFanins );
-            // create equality
-            pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0));
-            Vec_IntFillTwo( vFanins, 1, Wlc_ObjId(pNew, pConst), Wlc_ObjId(pNew, pCounter) );
-            Wlc_ObjAddFanins( pNew, pCond, vFanins );
-            // create MUX
-            pMux = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pFlop)-1, 0));
-            Vec_IntClear( vFanins );
-            Vec_IntPush( vFanins, Wlc_ObjId(pNew, pCond) );
-            Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFlop) );
-            Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFanin) );
-            Wlc_ObjAddFanins( pNew, pMux, vFanins );
-            Wlc_ObjSetCo( pNew, pMux, 1 );
-        }
-    }
+    // add the constraint as fanin to the output
+    Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
+    Wlc_ObjAddFanins( pNew, pConstrOut, vFanins );
 }
-Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int * piFirstMemPi, int * piFirstCi, int * piFirstMemCi, Vec_Wec_t * vConstrs, Vec_Int_t * vNodeFrames, Vec_Bit_t * vMuxVal )
+Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int * piFirstMemPi, int * piFirstCi, int * piFirstMemCi, Vec_Wec_t * vConstrs, Vec_Int_t * vNodeFrames )
 {
-    Wlc_Ntk_t * pNew;
+    Wlc_Ntk_t * pNew, * pTemp;
     Wlc_Obj_t * pObj, * pCounter, * pConst, * pAdder, * pConstr = NULL;
     Vec_Int_t * vNewObjs = NULL;
     Vec_Int_t * vFanins  = Vec_IntAlloc( 100 );
-    int i, Po0, Po1, AdderBits = 20, nBits = 0;
+    int i, Po0, Po1, AdderBits = 4, nBits = 0;
 
     // mark memory nodes
     Wlc_NtkCleanMarks( p );
@@ -349,7 +381,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
     Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
         if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
         {
-            int iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
+            Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
             nBits += Wlc_ObjRange(pObj);
         }
 
@@ -383,10 +415,6 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
         if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
             Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
 
-    // create logic nodes for constraints
-    if ( vConstrs )
-        pConstr = Wlc_NtkAbsCreateLogic( pNew, p, vNodeFrames, vFanins, vNewObjs, vConstrs );
-
     if ( Vec_IntSize(&p->vPoPairs) )
     {
         // create miter for the PO pairs
@@ -407,7 +435,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
 
         // create constraint output
         if ( vConstrs )
-            Wlc_ObjSetCo( pNew, pConstr, 0 );
+            Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 );
     }
     else
     {
@@ -416,8 +444,8 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
             if ( !pObj->Mark )
                 Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
         // create constraint output
-        if ( pConstr )
-            Wlc_ObjSetCo( pNew, pConstr, 0 );
+        if ( vConstrs )
+            Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 );
         // duplicate FIs
         Wlc_NtkForEachCo( p, pObj, i )
             if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
@@ -441,7 +469,11 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
 
     // create flop inputs for constraint objects
     if ( vConstrs )
-        Wlc_NtkAbsCreateFlopInputs( pNew, p, vNodeFrames, vFanins, vNewObjs, pCounter, AdderBits, vMuxVal );
+        Wlc_NtkAbsCreateFlopInputs( pNew, p, vNodeFrames, vFanins, vNewObjs, pCounter, AdderBits );
+
+    // create constraint logic nodes
+    if ( vConstrs )
+        Wlc_NtkAbsCreateLogic( pNew, p, vNodeFrames, vFanins, vNewObjs, vConstrs, pConstr );
 
     // append init states
     pNew->pInits = Wlc_PrsConvertInitValues( pNew );
@@ -451,6 +483,9 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
     Vec_IntFree( vFanins );
     Vec_IntFreeP( &vNewObjs );
     Wlc_NtkCleanMarks( p );
+    // derive topological order
+    pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
+    Wlc_NtkFree( pTemp );
     return pNew;
 }
 
@@ -465,7 +500,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int iFirstMemPi, int iFirstMemCi )
+Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int iFirstMemPi, int iFirstMemCi, int fVerbose )
 {
     Vec_Int_t * vFirstTotal = Vec_IntStart( 3 * Vec_IntSize(vMemObjs) ); // contains pairs of (first CO bit: range) for each input/output of a node
     Wlc_Obj_t * pObj, * pFanin; int i, k, iFanin, nMemFanins = 0;
@@ -499,15 +534,19 @@ Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_In
         }
     }
     assert( nMemFanins == Vec_IntSize(vMemFanins) );
-//    Vec_IntForEachEntry( vFirstTotal, iFanin, i )
-//        printf( "%16s : %d(%d)\n", Wlc_ObjName(p, Vec_IntEntry(vMemObjs, i/3)), iFanin >> 10, iFanin & 0x3FF );
+    if ( fVerbose )
+    Vec_IntForEachEntry( vFirstTotal, iFanin, i )
+    {
+        printf( "Obj %5d  Fanin %5d : ", i/3, i%3 );
+        printf( "%16s : %d(%d)\n", Wlc_ObjName(p, Vec_IntEntry(vMemObjs, i/3)), iFanin >> 10, iFanin & 0x3FF );
+    }
     return vFirstTotal;
 }
 int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, int iBit, Vec_Wrd_t * vRes, int iFrame )
 {
     Gia_Obj_t * pObj, * pObjRi, * pObjRo; 
     int k, b, Entry, First, nBits; word Value;
-    // assuming that flop inputs have been assigned from previous timeframe
+    // assuming that flop outputs have been assigned in the previous timeframe
     // assign primary inputs
     Gia_ManForEachPi( pAbs, pObj, k )
         pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
@@ -527,7 +566,7 @@ int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, i
     {
         if ( Entry == 0 )
         {
-            Vec_WrdPush( vRes, ~(word)0 );
+            Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, ~(word)0 );
             continue;
         }
         First = Entry >> 10;
@@ -542,19 +581,28 @@ int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, i
     }
     return iBit;
 }
-Vec_Wrd_t * Wlc_NtkConvertCex( Wlc_Ntk_t * p, Vec_Int_t * vFirstTotal, Gia_Man_t * pAbs, Abc_Cex_t * pCex )
+Vec_Wrd_t * Wlc_NtkConvertCex( Vec_Int_t * vFirstTotal, Gia_Man_t * pAbs, Abc_Cex_t * pCex, int fVerbose )
 {
     Vec_Wrd_t * vValues = Vec_WrdStartFull( Vec_IntSize(vFirstTotal) * (pCex->iFrame + 1) );
-    int f, nBits = pCex->nRegs;
+    int k, f, nBits = pCex->nRegs; word Value;
     Gia_ManCleanMark0(pAbs); // init FOs to zero
     for ( f = 0; f <= pCex->iFrame; f++ )
         nBits = Wlc_NtkCexResim( pAbs, pCex, vFirstTotal, nBits, vValues, f );
+    if ( fVerbose )
+    Vec_WrdForEachEntry( vValues, Value, k )
+    {
+        if ( k % Vec_IntSize(vFirstTotal) == 0 )
+            printf( "Frame %d:\n", k/Vec_IntSize(vFirstTotal) );
+        printf( "Obj %5d  Fanin %5d : ", k/3, k%3 );
+        Extra_PrintBinary( stdout, (unsigned *)&Value, 32 );
+        printf( "\n" );
+    }
     return vValues;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives refinement.]
+  Synopsis    [Derives the reason for failure in terms of memory values.]
 
   Description []
                
@@ -570,46 +618,54 @@ void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t *
     assert( iObj == Vec_IntEntry(vMemObjs, iNum) );
     assert( iFrame >= 0 );
     if ( Wlc_ObjIsPi(pObj) ) 
-        Vec_IntPush( vRes, (iObj << 10) | iFrame );
-    else if ( Wlc_ObjIsCo(pObj) )
+        Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) );
+    else if ( Wlc_ObjIsCi(pObj) && iFrame == 0 ) 
+    {
+        int PiId = Vec_IntEntry(p->vInits, Wlc_ObjCiId(pObj)-Wlc_NtkPiNum(p) );
+        int iPiObj = Wlc_ObjId( p, Wlc_NtkPi(p, PiId) );
+        Vec_IntPush( vRes, (iPiObj << 11) | (iFrame << 1) );
+    }
+    else if ( Wlc_ObjIsCi(pObj) )
         Wlc_NtkTrace_rec( p, Wlc_ObjFo2Fi(p, pObj), iFrame - 1, vMemObjs, vValues, ValueA, vRes );
     else if ( Wlc_ObjType(pObj) == WLC_OBJ_BUF )
         Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
     else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
     {
         int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum);
-        Wlc_NtkTrace_rec( p, Vec_WrdEntry(vValues, Index) ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
-        Vec_IntPush( vRes, (iObj << 10) | iFrame );
+        int Value = (int)Vec_WrdEntry( vValues, Index );
+        assert( Value == 0 && Value == 1 );
+        Wlc_NtkTrace_rec( p, Value ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
+        Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) | Value );
     }
     else if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
     {
         int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum);
         if ( Vec_WrdEntry(vValues, Index + 1) != ValueA ) // address 
             Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes );
-        Vec_IntPush( vRes, (iObj << 10) | iFrame );
+        Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) );
     }
     else assert( 0 );
 }
 Vec_Int_t * Wlc_NtkTrace( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues )
 {
-    int iObj = Wlc_ObjId(p, pObj);
+    int iObj = Wlc_ObjId( p, pObj );
     int iNum = Wlc_ObjCopy( p, iObj );
     Vec_Int_t * vTrace = Vec_IntAlloc( 10 );
     assert( Wlc_ObjType(pObj) == WLC_OBJ_READ );
     assert( iObj == Vec_IntEntry(vMemObjs, iNum) );
     Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, Vec_WrdEntry(vValues, 3*(iFrame*Vec_IntSize(vMemObjs) + iNum) + 1), vTrace );
-    Vec_IntPush( vTrace, (iObj << 10) | iFrame );
+    Vec_IntPush( vTrace, (iObj << 11) | (iFrame << 1) );
     return vTrace;
 }
 int Wlc_NtkTraceCheckConfict( Wlc_Ntk_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues )
 {
     Wlc_Obj_t * pObjLast, * pObjFirst; 
-    int iFrmLast = Vec_IntEntryLast(vTrace) & 0x3FF;
-    int iObjLast = Vec_IntEntryLast(vTrace) >> 10;
+    int iObjLast = Vec_IntEntryLast(vTrace) >> 11;
+    int iFrmLast =(Vec_IntEntryLast(vTrace) >> 1) & 0x3FF;
     int iNumLast = Wlc_ObjCopy( p, iObjLast );
     int iIndLast = 3*(iFrmLast*Vec_IntSize(vMemObjs) + iNumLast);
-    int iFrmFirst = Vec_IntEntry(vTrace, 0) & 0x3FF;
-    int iObjFirst = Vec_IntEntry(vTrace, 0) >> 10;
+    int iObjFirst = Vec_IntEntry(vTrace, 0) >> 11;
+    int iFrmFirst =(Vec_IntEntry(vTrace, 0) >> 1) & 0x3FF;
     int iNumFirst = Wlc_ObjCopy( p, iObjFirst );
     int iIndFirst = 3*(iFrmFirst*Vec_IntSize(vMemObjs) + iNumFirst);
     assert( Vec_IntSize(vTrace) >= 2 );
@@ -621,22 +677,25 @@ int Wlc_NtkTraceCheckConfict( Wlc_Ntk_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMe
     assert( Wlc_ObjType(pObjFirst) == WLC_OBJ_WRITE || Wlc_ObjIsPi(pObjFirst) );
     if ( Wlc_ObjIsPi(pObjFirst) )
         return 0;
-    assert( Vec_WrdEntry(vValues, iIndLast + 1) == Vec_WrdEntry(vValues, iIndFirst + 1) );
+    assert( Vec_WrdEntry(vValues, iIndLast + 1) == Vec_WrdEntry(vValues, iIndFirst + 1) ); // equal addr
     return Vec_WrdEntry(vValues, iIndLast + 2) != Vec_WrdEntry(vValues, iIndFirst + 2); // diff data
 }
 Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, int nFrames )
 {
     Wlc_Obj_t * pObj; int i, f, Entry;
-    Vec_Wec_t * vTraces = Vec_WecStart( 100 );
+    Vec_Wec_t * vTraces = Vec_WecAlloc( 100 );
     Vec_Int_t * vTrace, * vTrace1, * vTrace2;
     assert( 3 * nFrames * Vec_IntSize(vMemObjs) == Vec_WrdSize(vValues) );
+    Wlc_NtkCleanCopy( p );
+    Vec_IntForEachEntry( vMemObjs, Entry, i )
+        Wlc_ObjSetCopy( p, Entry, i );
     for ( f = 0; f < nFrames; f++ )
     {
         Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
         {
             if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
                 continue;
-            vTrace = Wlc_NtkTrace( p, pObj, nFrames, vMemObjs, vValues );
+            vTrace = Wlc_NtkTrace( p, pObj, f, vMemObjs, vValues );
             if ( Wlc_NtkTraceCheckConfict( p, vTrace, vMemObjs, vValues ) )
             {
                 Vec_WecFree( vTraces );
@@ -652,20 +711,26 @@ Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t
     Vec_WecForEachLevelStop( vTraces, vTrace2, f, i )
         if ( Vec_IntEntry(vTrace1, 0) == Vec_IntEntry(vTrace2, 0) )
         {
-            int iObj1 = Vec_IntEntryLast(vTrace1);
+            int iObj1 = Vec_IntEntryLast(vTrace1) >> 11;
+            int iFrm1 =(Vec_IntEntryLast(vTrace1) >> 1) & 0x3FF;
             int iNum1 = Wlc_ObjCopy( p, iObj1 );
-            int iObj2 = Vec_IntEntryLast(vTrace2);
+            int iInd1 = 3*(iFrm1*Vec_IntSize(vMemObjs) + iNum1);
+
+            int iObj2 = Vec_IntEntryLast(vTrace2) >> 11;
+            int iFrm2 =(Vec_IntEntryLast(vTrace2) >> 1) & 0x3FF;
             int iNum2 = Wlc_ObjCopy( p, iObj2 );
+            int iInd2 = 3*(iFrm2*Vec_IntSize(vMemObjs) + iNum2);
+
             assert( iObj1 == Vec_IntEntry(vMemObjs, iNum1) );
             assert( iObj2 == Vec_IntEntry(vMemObjs, iNum2) );
-            if ( Vec_WrdEntry(vValues, 3*iNum1 + 1) == Vec_WrdEntry(vValues, 3*iNum2 + 1) &&  // same address
-                 Vec_WrdEntry(vValues, 3*iNum2 + 1) != Vec_WrdEntry(vValues, 3*iNum2 + 1) )   // different data
+            if ( Vec_WrdEntry(vValues, iInd1 + 1) == Vec_WrdEntry(vValues, iInd2 + 1) &&  // equal address
+                 Vec_WrdEntry(vValues, iInd1 + 2) != Vec_WrdEntry(vValues, iInd2 + 2) )   // diff data
             {
                 vTrace = Vec_IntAlloc( 100 );
                 Vec_IntPush( vTrace, Vec_IntPop(vTrace1) );
-                Vec_IntForEachEntry( vTrace1, Entry, i )
+                Vec_IntForEachEntryStart( vTrace1, Entry, i, 1 )
                     Vec_IntPushUnique( vTrace, Entry );
-                Vec_IntForEachEntry( vTrace2, Entry, i )
+                Vec_IntForEachEntryStart( vTrace2, Entry, i, 1 )
                     Vec_IntPushUnique( vTrace, Entry );
                 Vec_WecFree( vTraces );
                 return vTrace;
@@ -674,16 +739,38 @@ Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t
     Vec_WecFree( vTraces );
     return NULL;
 }
-Vec_Bit_t * Wlc_NtkCollectMuxValues( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, int nFrames )
+void Wlc_NtkPrintConflict( Wlc_Ntk_t * p, Vec_Int_t * vTrace )
 {
-    Vec_Bit_t * vBitValues = Vec_BitStart( nFrames * Wlc_NtkObjNum(p) );
-    Wlc_Obj_t * pObj; int i, f;
-    Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
-        if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
-            for ( f = 0; f < nFrames; f++ )
-                if ( Vec_WrdEntry(vValues, 3*f*Vec_IntSize(vMemObjs) + i) )
-                    Vec_BitWriteEntry( vBitValues, f*Wlc_NtkObjNum(p) + Wlc_ObjId(p, pObj), 1 );
-    return vBitValues;
+    int Entry, i;
+    printf( "Memory semantics failure trace:\n" );
+    Vec_IntForEachEntry( vTrace, Entry, i )
+        printf( "%3d: entry %9d : obj %5d with name %16s in frame %d\n", i, Entry, Entry >> 11, Wlc_ObjName(p, Entry>>11), (Entry >> 1) & 0x3FF );
+}
+void Wlc_NtkPrintCex( Wlc_Ntk_t * p, Wlc_Ntk_t * pAbs, Abc_Cex_t * pCex )
+{
+    Wlc_Obj_t * pObj; int i, k, f, nBits = pCex ? pCex->nRegs : 0;
+    if ( pCex == NULL )
+    {
+        printf( "The CEX is NULL.\n" );
+        return;
+    }
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        printf( "Frame%02d ", f );
+        Wlc_NtkForEachPi( pAbs, pObj, i )
+        {
+            printf( "PI%d:", i );
+            //printf( "%d(%d):", nBits, Wlc_ObjRange(pObj) );
+            for ( k = 0; k < Wlc_ObjRange(pObj); k++ )
+                printf( "%d", Abc_InfoHasBit(pCex->pData,  nBits++) );
+            printf( " " );
+        }
+        printf( "FF:" );
+        for ( k = 0; nBits < pCex->nPis; k++ )
+            printf( "%d", Abc_InfoHasBit(pCex->pData, nBits++) );
+        printf( "\n" );
+    }
+
 }
 
 /**Function*************************************************************
@@ -700,32 +787,41 @@ Vec_Bit_t * Wlc_NtkCollectMuxValues( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wr
 Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p )
 {
     int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits;
-    Vec_Int_t * vFirstTotal;
+    Vec_Int_t * vRefine;
     Vec_Int_t * vMemObjs    = Wlc_NtkCollectMemory( p );
     Vec_Int_t * vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
 
     Vec_Wec_t * vRefines    = Vec_WecAlloc( 100 );
     Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
-//    Wlc_Ntk_t * pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL, NULL );
-    Wlc_Ntk_t * pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames, NULL );
+    Wlc_Ntk_t * pNewFull;
+
+    vRefine     = Vec_WecPushLevel(vRefines);
+    Vec_IntPush( vRefine,  (11 << 11) | 0 );
+    Vec_IntPush( vRefine,  (10 << 11) | 0 );
+    Vec_IntPush( vRefine,  ( 8 << 11) | 0 );
+    Vec_IntPush( vRefine,  ( 9 << 11) | 0 );
+    Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
+
+//    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
+    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
+
     Vec_WecFree( vRefines );
     Vec_IntFree( vNodeFrames );
 
     nDcBits     = Wlc_CountDcs( pNewFull->pInits );
-    vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi );
     printf( "iFirstMemPi = %d  iFirstCi = %d  iFirstMemCi = %d  nDcBits = %d\n", iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits );
+
     Vec_IntFreeP( &vMemObjs );
     Vec_IntFreeP( &vMemFanins );
-    Vec_IntFreeP( &vFirstTotal );
     return pNewFull;
 }
 
 int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbose )
 {
     abctime clk = Abc_Clock();
-    Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig;
-    Gia_Man_t * pAbsFull, * pAbs, * pTemp;
-    Abc_Cex_t * pCex = NULL;  Vec_Wrd_t * vValues = NULL; Vec_Bit_t * vMuxVal = NULL;
+    Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig, * pTempAig;
+    Gia_Man_t * pAbsFull, * pAbs;
+    Abc_Cex_t * pCex = NULL;  Vec_Wrd_t * vValues = NULL; 
     Vec_Wec_t * vRefines = Vec_WecAlloc( 100 );
     Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 );
     Vec_Int_t * vMemObjs, * vMemFanins, * vFirstTotal, * vRefine; 
@@ -733,15 +829,16 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbo
 
     vMemObjs    = Wlc_NtkCollectMemory( p );
     vMemFanins  = Wlc_NtkCollectMemFanins( p, vMemObjs );
-    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL, NULL );
+    pNewFull    = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL );
     nDcBits     = Wlc_CountDcs( pNewFull->pInits );
-    vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi );
+    vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi, fVerbose );
 
     pAbsFull    = Wlc_NtkBitBlast( pNewFull, NULL );
     assert( Gia_ManPiNum(pAbsFull) == iFirstCi + nDcBits );
+    Wlc_NtkFree( pNewFull );
 
     // perform abstraction
-    for ( nIters = 1; nIters < 10000; nIters++ )
+    for ( nIters = 0; nIters < nIterMax; nIters++ )
     {
         // set up parameters to run PDR
         Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
@@ -750,64 +847,80 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbo
         pPdrPars->fVerbose   = fVerbose;
 
         // derive specific abstraction
-        pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames, vMuxVal );
+        pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
         pAbs = Wlc_NtkBitBlast( pNew, NULL );
-        Wlc_NtkFree( pNew );
         // simplify the AIG
-        pAbs = Gia_ManSeqStructSweep( pTemp = pAbs, 1, 1, 0 );
-        Gia_ManStop( pTemp );
+        //pAbs = Gia_ManSeqStructSweep( pGiaTemp = pAbs, 1, 1, 0 );
+        //Gia_ManStop( pGiaTemp );
 
-        // try to prove abstracted GIA by converting it to AIG and calling PDR
+        // roll in the constraints
         pAig = Gia_ManToAigSimple( pAbs );
         Gia_ManStop( pAbs );
+        pAig->nConstrs = 1;
+        pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 );
+        Aig_ManStop( pTempAig );
+        pAbs = Gia_ManFromAigSimple( pAig );
+        Aig_ManStop( pAig );
+        //Gia_AigerWrite( pAbs, "mem_abs.aig", 0, 0 );
+
+        // try to prove abstracted GIA by converting it to AIG and calling PDR
+        pAig = Gia_ManToAigSimple( pAbs );
         RetValue = Pdr_ManSolve( pAig, pPdrPars );
         pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
         Aig_ManStop( pAig );
 
+        if ( fVerbose )
+            printf( "\nITERATIONS %d:\n", nIters );
+        if ( fVerbose )
+            Wlc_NtkPrintCex( p, pNew, pCex );
+        Wlc_NtkFree( pNew );
+
         // check if proved or undecided
         if ( pCex == NULL ) 
         {
             assert( RetValue );
+            Gia_ManStop( pAbs );
             break;
         }
 
         // analyze counter-example
-        Vec_BitFreeP( &vMuxVal );
-        vValues = Wlc_NtkConvertCex( p, vFirstTotal, pAbs, pCex );
-        vMuxVal = Wlc_NtkCollectMuxValues( p, vMemObjs, vValues, pCex->iFrame + 1 );
+        vValues = Wlc_NtkConvertCex( vFirstTotal, pAbsFull, pCex, fVerbose );
+        Gia_ManStop( pAbs );
         vRefine = Wlc_NtkFindConflict( p, vMemObjs, vValues, pCex->iFrame + 1 );
         Vec_WrdFree( vValues );
-        Abc_CexFree( pCex ); // return CEX in the future
-        if ( vRefine == NULL )
+        if ( vRefine == NULL ) // cannot refine
             break;
+        Abc_CexFreeP( &pCex );
 
         // save refinement for the future
+        if ( fVerbose )
+            Wlc_NtkPrintConflict( p, vRefine );
         Vec_WecPushLevel( vRefines );
         Vec_IntAppend( Vec_WecEntryLast(vRefines), vRefine );
         Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine );
         Vec_IntFree( vRefine );
     }
     // cleanup
-    Wlc_NtkFree( pNew );
+    Gia_ManStop( pAbsFull );
     Vec_WecFree( vRefines );
     Vec_IntFreeP( &vMemObjs );
     Vec_IntFreeP( &vMemFanins );
     Vec_IntFreeP( &vFirstTotal );
     Vec_IntFreeP( &vNodeFrames );
-    Vec_BitFreeP( &vMuxVal );
 
     // report the result
     if ( fVerbose )
         printf( "\n" );
     printf( "Abstraction " );
-    if ( RetValue == 0 )
-        printf( "resulted in a real CEX" );
+    if ( RetValue == 0 && pCex )
+        printf( "resulted in a real CEX in frame %d", pCex->iFrame );
     else if ( RetValue == 1 )
         printf( "is successfully proved" );
     else 
         printf( "timed out" );
     printf( " after %d iterations. ", nIters );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    Abc_CexFreeP( &pCex ); // return CEX in the future
     return RetValue;
 }
 
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index b65558e6..b3b87f9e 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -334,6 +334,8 @@ int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p )
         Vec_IntWriteEntry( &p->vLevels, i, LevelMax - Wlc_ObjLevelId(p, i) );
     Wlc_NtkForEachCi( p, pObj, i )
         Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), 0 );
+    //Wlc_NtkForEachObj( p, pObj, i )
+    //    printf( "%d -> %d\n", i, Wlc_ObjLevelId(p, i) );
     return LevelMax;
 }
 
@@ -624,36 +626,36 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose )
 void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 {
     printf( "%8d  :  ", Wlc_ObjId(p, pObj) );
-    printf( "%3d%s",    Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
+    printf( "%6d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
     if ( pObj->Type == WLC_OBJ_PI )
     {
-        printf( "                          PI\n" );
+        printf( "PI\n" );
         return;
     }
     if ( pObj->Type == WLC_OBJ_FO )
     {
-        printf( "                          FO\n" );
+        printf( "FO\n" );
         return;
     }
-    if ( pObj->Type == WLC_OBJ_CONST )
-        printf( "                          " );
-    else
+    if ( pObj->Type != WLC_OBJ_CONST )
     {
-        printf( " = %3d%s  %5s  ",  Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] );
+        printf( "%6d%s  %5s  ",  Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] );
         if ( Wlc_ObjFaninNum(pObj) > 1 )
-            printf( "%3d%s ",       Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
+            printf( "%6d%s ",       Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
         else
-            printf( "     " );
+            printf( "        " );
         if ( Wlc_ObjFaninNum(pObj) > 2 )
-            printf( "%3d%s ",       Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " );
+            printf( "%6d%s ",       Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " );
         else
-            printf( "     " );
+            printf( "        " );
     }
+    else
+        printf( "                                " );
     printf( " :    " );
     printf( "%-12s",   Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
     if ( pObj->Type == WLC_OBJ_CONST )
     {
-        printf( " =  %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" );
+        printf( " = %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" );
         if ( pObj->fXConst )
         {
             int k;
@@ -723,6 +725,12 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose
             printf( "%2d  :  %-8s  %6d\n", i, Wlc_Names[i], p->nObjs[i] );
     }
 }
+void Wlc_NtkPrintObjects( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj; int i;
+    Wlc_NtkForEachObj( p, pObj, i )
+        Wlc_NtkPrintNode( p, pObj );
+}
 
 /**Function*************************************************************
 
@@ -928,7 +936,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
     }
     if ( p->pSpec )
         pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    Wlc_NtkTransferNames( pNew, p );
+    if ( Wlc_NtkHasNameId(p) )
+        Wlc_NtkTransferNames( pNew, p );
     if ( Vec_IntSize(&p->vPoPairs) )
         Vec_IntAppend( &pNew->vPoPairs, &p->vPoPairs );
     return pNew;